cprover
satcheck_smvsat.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "satcheck_smvsat.h"
10 
11 #include <cassert>
12 #include <stack>
13 
14 #include <satsolvercore.h>
15 #include <interpolator.h>
16 
18 {
19  satsolver=
20  sat_instance_new_type(SATSOLVERCORE1, no_variables(), true);
21 
22  // now we can do l_const
23  init_const();
24 }
25 
27 {
28 }
29 
31 {
32 }
33 
35 {
36  assert(status==SAT);
37 
38  if(a.is_true())
39  return tvt(true);
40  else if(a.is_false())
41  return tvt(false);
42 
43  tvt result;
44  unsigned v=a.var_no();
45 
46  switch(sat_instance_value(satsolver, v))
47  {
48  case 0: result=tvt(false); break;
49  case 1: result=tvt(true); break;
50  default: result=tvt(tvt::tv_enumt::TV_UNKNOWN); break;
51  }
52 
53  if(a.sign())
54  result=!result;
55 
56  return result;
57 }
58 
59 const std::string satcheck_smvsatt::solver_text()
60 {
61  return std::string("SMVSAT");
62 }
63 
64 void satcheck_smvsatt::lcnf(const bvt &bv)
65 {
66  bvt tmp;
67 
68  if(process_clause(bv, tmp))
69  return;
70 
71  int *lits=new int[tmp.size()+1];
72 
73  for(unsigned i=0; i<tmp.size(); i++)
74  lits[i]=tmp[i].dimacs();
75 
76  // zero-terminated
77  lits[tmp.size()]=0;
78 
79  sat_instance_add_clause(satsolver, lits);
80 
82 
83  delete[] lits;
84 }
85 
87 {
88  int result=sat_instance_solve(satsolver);
89 
90  {
91  std::string msg;
92 
93  switch(result)
94  {
95  case 0:
96  msg="SAT checker: instance is UNSATISFIABLE";
97  break;
98 
99  case 1:
100  msg="SAT checker: instance is SATISFIABLE";
101  break;
102 
103  default:
104  msg="SAT checker failed: unknown result";
105  break;
106  }
107 
108  messaget::status() << msg << messaget::eom;
109  }
110 
111  if(result==0)
112  {
113  status=UNSAT;
114  return P_UNSATISFIABLE;
115  }
116 
117  if(result==1)
118  {
119  status=SAT;
120  return P_SATISFIABLE;
121  }
122 
123  status=ERROR;
124 
125  return P_ERROR;
126 }
127 
129 {
131 
132  if(result==P_UNSATISFIABLE)
133  {
134  // TODO
135  }
136 
137  return result;
138 }
139 
141 {
142  bvt tmp;
143 
144  if(process_clause(bv, tmp))
145  return;
146 
147  int *lits=new int[tmp.size()+1];
148 
149  for(unsigned i=0; i<tmp.size(); i++)
150  lits[i]=tmp[i].dimacs();
151 
152  // zero-terminated
153  lits[tmp.size()]=0;
154 
155  unsigned clause_id=sat_instance_add_clause(satsolver, lits);
156 
157  if(partition_numbers.size()<=clause_id)
158  partition_numbers.resize(clause_id+1, -1);
159 
160  partition_numbers[clause_id]=partition_no;
161 
162  delete[] lits;
163 }
164 
166 {
167  // crate instance
168 
169  // NOLINTNEXTLINE(readability/identifiers)
170  struct interpolator *interpolator_satsolver=
171  new_interpolator(satsolver);
172 
173  // set partition numbers
174 
175  for(unsigned i=0; i<partition_numbers.size(); i++)
176  {
177  short p=partition_numbers[i];
178  if(p!=-1)
179  interpolator_satsolver->set_clause_partition(i, p);
180  }
181 
182  int output=interpolator_satsolver->interpolate(0, 0);
183 
184  build_aig(*interpolator_satsolver, output, dest);
185 
186  delete interpolator_satsolver;
187 }
188 
190  // NOLINTNEXTLINE(readability/identifiers)
191  struct interpolator &interpolator_satsolver,
192  int output,
193  exprt &dest)
194 {
195  std::stack<entryt> stack;
196 
197  stack.push(entryt(output, &dest));
198 
199  while(!stack.empty())
200  {
201  entryt x=stack.top();
202  stack.pop();
203 
204  bool invert=x.g<0;
205  int n=invert?-x.g:x.g;
206 
207  assert(n!=0);
208 
209  exprt &e=*x.e;
210 
211  if(n==INT_MAX)
212  e.make_true();
213  else if(n<=satsolver->num_variables())
214  { // a SAT variable
215  e.id(ID_symbol);
216  e.set(ID_identifier, n);
217  }
218  else
219  {
220  e.id(ID_and);
221  e.operands().resize(2);
222 
223  unsigned g0=interpolator_satsolver.aig_arg(n, 0);
224  unsigned g1=interpolator_satsolver.aig_arg(n, 1);
225 
226  stack.push(entryt(g0, &e.op0()));
227  stack.push(entryt(g1, &e.op1()));
228  }
229 
230  if(invert)
231  e.make_not();
232  }
233 }
mstreamt & result()
Definition: message.h:233
size_t clause_counter
Definition: cnf.h:81
exprt & op0()
Definition: expr.h:84
mstreamt & status()
Definition: message.h:238
bool process_clause(const bvt &bv, bvt &dest)
filter &#39;true&#39; from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition: cnf.cpp:416
std::vector< short > partition_numbers
virtual resultt prop_solve()
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual ~satcheck_smvsatt()
void make_true()
Definition: expr.cpp:153
const irep_idt & id() const
Definition: irep.h:189
virtual const std::string solver_text()
bool is_true() const
Definition: literal.h:155
Definition: threeval.h:19
exprt & op1()
Definition: expr.h:87
virtual void lcnf(const bvt &bv)
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
void make_not()
Definition: expr.cpp:100
Base class for all expressions.
Definition: expr.h:46
bool sign() const
Definition: literal.h:87
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
struct sat_instance * satsolver
virtual size_t no_variables() const override
Definition: cnf.h:38
operandst & operands()
Definition: expr.h:70
#define stack(x)
Definition: parser.h:144
void build_aig(struct interpolator &interpolator_satsolver, int output, exprt &dest)
std::vector< literalt > bvt
Definition: literal.h:197
virtual void lcnf(const bvt &bv)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool is_false() const
Definition: literal.h:160