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 <stack>
15 
16 #include <util/exception_utils.h>
17 #include <util/invariant.h>
18 #include <util/threeval.h>
19 
20 #include "satcheck_ipasir.h"
21 
22 #ifdef HAVE_IPASIR
23 
24 extern "C"
25 {
26 #include <ipasir.h>
27 }
28 
29 /*
30 
31 Interface description:
32 https://github.com/biotomas/ipasir/blob/master/ipasir.h
33 
34 Representation:
35 Variables for a formula start with 1! 0 is used as termination symbol.
36 
37 */
38 
40 {
41  if(a.is_true())
42  return tvt(true);
43  else if(a.is_false())
44  return tvt(false);
45 
46  tvt result;
47 
48  // compare to internal no_variables number
49  if(a.var_no()>=(unsigned)no_variables())
50  return tvt::unknown();
51 
52  const int val=ipasir_val(solver, a.var_no());
53 
54  if(val>0)
55  result=tvt(true);
56  else if(val<0)
57  result=tvt(false);
58  else
59  return tvt::unknown();
60 
61  if(a.sign())
62  result=!result;
63 
64  return result;
65 }
66 
67 const std::string satcheck_ipasirt::solver_text()
68 {
69  return std::string(ipasir_signature());
70 }
71 
72 void satcheck_ipasirt::lcnf(const bvt &bv)
73 {
74  forall_literals(it, bv)
75  {
76  if(it->is_true())
77  return;
78  else if(!it->is_false())
79  INVARIANT(it->var_no()<(unsigned)no_variables(),
80  "reject out of bound variables");
81  }
82 
83  forall_literals(it, bv)
84  {
85  if(!it->is_false())
86  {
87  // add literal with correct sign
88  ipasir_add(solver, it->dimacs());
89  }
90  }
91  ipasir_add(solver, 0); // terminate clause
92 
94 }
95 
97 {
98  INVARIANT(status!=statust::ERROR, "there cannot be an error");
99 
100  {
101  messaget::status() <<
102  (no_variables()-1) << " variables, " <<
103  clause_counter << " clauses" << eom;
104  }
105 
106  // use the internal representation, as ipasir does not support reporting the
107  // status
109  {
110  messaget::status() <<
111  "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
112  }
113  else
114  {
115  // if assumptions contains false, we need this to be UNSAT
116  bvt::const_iterator it = std::find_if(assumptions.begin(),
117  assumptions.end(), is_false);
118  const bool has_false = it != assumptions.end();
119 
120  if(has_false)
121  {
122  messaget::status() <<
123  "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
124  }
125  else
126  {
128  if(!it->is_false())
129  ipasir_assume(solver, it->dimacs());
130 
131  // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
132  int solver_state=ipasir_solve(solver);
133  if(10==solver_state)
134  {
135  messaget::status() <<
136  "SAT checker: instance is SATISFIABLE" << eom;
138  return resultt::P_SATISFIABLE;
139  }
140  else if(20==solver_state)
141  {
142  messaget::status() <<
143  "SAT checker: instance is UNSATISFIABLE" << eom;
144  }
145  else
146  {
147  messaget::status() <<
148  "SAT checker: solving returned without solution" << eom;
149  throw analysis_exceptiont(
150  "solving inside IPASIR SAT solver has been interrupted");
151  }
152  }
153  }
154 
157 }
158 
159 void satcheck_ipasirt::set_assignment(literalt a, bool value)
160 {
161  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
162  INVARIANT(false, "method not supported");
163 }
164 
166 : solver(nullptr)
167 {
168  INVARIANT(!solver, "there cannot be a solver already");
169  solver=ipasir_init();
170 }
171 
173 {
174  if(solver)
175  ipasir_release(solver);
176  solver=nullptr;
177 }
178 
180 {
181  return ipasir_failed(solver, a.var_no());
182 }
183 
185 {
186  bvt::const_iterator it = std::find_if(bv.begin(), bv.end(), is_true);
187  const bool has_true = it != bv.end();
188 
189  if(has_true)
190  {
191  assumptions.clear();
192  return;
193  }
194  // only copy assertions, if there is no false in bt parameter
195  assumptions=bv;
196 }
197 
198 #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.
#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.
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
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
resultt
Definition: prop.h:96
virtual void set_assignment(literalt a, bool value) override
static eomt eom
Definition: message.h:284
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
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