cprover
satcheck_ipasir.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: External SAT Solver Binding
4 
5 Author: Norbert Manthey, nmanthey@amazon.com
6 
7 \*******************************************************************/
8 
9 #ifndef _MSC_VER
10 #include <inttypes.h>
11 #endif
12 
13 #include <algorithm>
14 #include <cassert>
15 #include <stack>
16 
17 #include <util/threeval.h>
18 
19 #include "satcheck_ipasir.h"
20 
21 #ifdef HAVE_IPASIR
22 
23 extern "C"
24 {
25 #include <ipasir.h>
26 }
27 
28 /*
29 
30 Interface description:
31 https://github.com/biotomas/ipasir/blob/master/ipasir.h
32 
33 Representation:
34 Variables for a formula start with 1! 0 is used as termination symbol.
35 
36 */
37 
39 {
40  if(a.is_true())
41  return tvt(true);
42  else if(a.is_false())
43  return tvt(false);
44 
45  tvt result;
46 
47  // compare to internal no_variables number
48  if(a.var_no()>=(unsigned)no_variables())
49  return tvt::unknown();
50 
51  const int val=ipasir_val(solver, a.var_no());
52 
53  if(val>0)
54  result=tvt(true);
55  else if(val<0)
56  result=tvt(false);
57  else
58  return tvt::unknown();
59 
60  if(a.sign())
61  result=!result;
62 
63  return result;
64 }
65 
66 const std::string satcheck_ipasirt::solver_text()
67 {
68  return std::string(ipasir_signature());
69 }
70 
71 void satcheck_ipasirt::lcnf(const bvt &bv)
72 {
73  forall_literals(it, bv)
74  {
75  if(it->is_true())
76  return;
77  else if(!it->is_false())
78  INVARIANT(it->var_no()<(unsigned)no_variables(),
79  "reject out of bound variables");
80  }
81 
82  forall_literals(it, bv)
83  {
84  if(!it->is_false())
85  {
86  // add literal with correct sign
87  ipasir_add(solver, it->dimacs());
88  }
89  }
90  ipasir_add(solver, 0); // terminate clause
91 
93 }
94 
96 {
97  INVARIANT(status!=statust::ERROR, "there cannot be an error");
98 
99  {
100  messaget::status() <<
101  (no_variables()-1) << " variables, " <<
102  clause_counter << " clauses" << eom;
103  }
104 
105  // use the internal representation, as ipasir does not support reporting the
106  // status
108  {
109  messaget::status() <<
110  "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
111  }
112  else
113  {
114  // if assumptions contains false, we need this to be UNSAT
115  bvt::const_iterator it = std::find_if(assumptions.begin(),
116  assumptions.end(), is_false);
117  const bool has_false = it != assumptions.end();
118 
119  if(has_false)
120  {
121  messaget::status() <<
122  "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
123  }
124  else
125  {
127  if(!it->is_false())
128  ipasir_assume(solver, it->dimacs());
129 
130  // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
131  int solver_state=ipasir_solve(solver);
132  if(10==solver_state)
133  {
134  messaget::status() <<
135  "SAT checker: instance is SATISFIABLE" << eom;
137  return resultt::P_SATISFIABLE;
138  }
139  else if(20==solver_state)
140  {
141  messaget::status() <<
142  "SAT checker: instance is UNSATISFIABLE" << eom;
143  }
144  else
145  {
146  messaget::status() <<
147  "SAT checker: solving returned without solution" << eom;
148  throw "solving inside IPASIR SAT solver has been interrupted";
149  }
150  }
151  }
152 
155 }
156 
157 void satcheck_ipasirt::set_assignment(literalt a, bool value)
158 {
159  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
160  INVARIANT(false, "method not supported");
161 }
162 
164 : solver(nullptr)
165 {
166  INVARIANT(!solver, "there cannot be a solver already");
167  solver=ipasir_init();
168 }
169 
171 {
172  if(solver)
173  ipasir_release(solver);
174  solver=nullptr;
175 }
176 
178 {
179  return ipasir_failed(solver, a.var_no());
180 }
181 
183 {
184  bvt::const_iterator it = std::find_if(bv.begin(), bv.end(), is_true);
185  const bool has_true = it != bv.end();
186 
187  if(has_true)
188  {
189  assumptions.clear();
190  return;
191  }
192  // only copy assertions, if there is no false in bt parameter
193  assumptions=bv;
194 }
195 
196 #endif
bool is_true(const literalt &l)
Definition: literal.h:197
size_t clause_counter
Definition: cnf.h:81
virtual resultt prop_solve() override
virtual bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
static tvt unknown()
Definition: threeval.h:33
virtual void lcnf(const bvt &bv) override final
virtual const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
#define forall_literals(it, bv)
Definition: literal.h:202
virtual tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
bool is_false(const literalt &l)
Definition: literal.h:196
virtual void set_assumptions(const bvt &_assumptions) override
int solver(std::istream &in)
virtual ~satcheck_ipasirt() override
bool is_true() const
Definition: literal.h:155
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:96
virtual void set_assignment(literalt a, bool value) override
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
bool is_constant() const
Definition: literal.h:165
bool sign() const
Definition: literal.h:87
virtual size_t no_variables() const override
Definition: cnf.h:38
std::vector< literalt > bvt
Definition: literal.h:200
bool is_false() const
Definition: literal.h:160