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 #include <algorithm>
10 
11 #include <util/exception_utils.h>
12 #include <util/invariant.h>
13 #include <util/threeval.h>
14 
15 #include "satcheck_ipasir.h"
16 
17 #ifdef HAVE_IPASIR
18 
19 extern "C"
20 {
21 #include <ipasir.h>
22 }
23 
24 /*
25 
26 Interface description:
27 https://github.com/biotomas/ipasir/blob/master/ipasir.h
28 
29 Representation:
30 Variables for a formula start with 1! 0 is used as termination symbol.
31 
32 */
33 
35 {
36  if(a.is_true())
37  return tvt(true);
38  else if(a.is_false())
39  return tvt(false);
40 
41  tvt result;
42 
43  // compare to internal no_variables number
44  if(a.var_no()>=(unsigned)no_variables())
45  return tvt::unknown();
46 
47  const int val=ipasir_val(solver, a.var_no());
48 
49  if(val>0)
50  result=tvt(true);
51  else if(val<0)
52  result=tvt(false);
53  else
54  return tvt::unknown();
55 
56  if(a.sign())
57  result=!result;
58 
59  return result;
60 }
61 
62 const std::string satcheck_ipasirt::solver_text()
63 {
64  return std::string(ipasir_signature());
65 }
66 
67 void satcheck_ipasirt::lcnf(const bvt &bv)
68 {
69  for(const auto &literal : bv)
70  {
71  if(literal.is_true())
72  return;
73  else if(!literal.is_false())
74  {
75  INVARIANT(
76  literal.var_no() < (unsigned)no_variables(),
77  "reject out of bound variables");
78  }
79  }
80 
81  for(const auto &literal : bv)
82  {
83  if(!literal.is_false())
84  {
85  // add literal with correct sign
86  ipasir_add(solver, literal.dimacs());
87  }
88  }
89  ipasir_add(solver, 0); // terminate clause
90 
91  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
92  // To map clauses to lines of program code, track clause indices in the
93  // dimacs cnf output. Dimacs output is generated after processing
94  // clauses to remove duplicates and clauses that are trivially true.
95  // Here, a clause is checked to see if it can be thus eliminated. If
96  // not, add the clause index to list of clauses in
97  // solver_hardnesst::register_clause().
98  static size_t cnf_clause_index = 0;
99  bvt cnf;
100  bool clause_removed = process_clause(bv, cnf);
101 
102  if(!clause_removed)
103  cnf_clause_index++;
104 
105  hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
106  });
107 
108  clause_counter++;
109 }
110 
112 {
113  INVARIANT(status!=statust::ERROR, "there cannot be an error");
114 
115  log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
116  << " clauses" << messaget::eom;
117 
118  // if assumptions contains false, we need this to be UNSAT
119  bvt::const_iterator it =
120  std::find_if(assumptions.begin(), assumptions.end(), is_false);
121  const bool has_false = it != assumptions.end();
122 
123  if(has_false)
124  {
125  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
126  << messaget::eom;
127  }
128  else
129  {
130  for(const auto &literal : assumptions)
131  {
132  if(!literal.is_false())
133  ipasir_assume(solver, literal.dimacs());
134  }
135 
136  // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
137  int solver_state = ipasir_solve(solver);
138  if(10 == solver_state)
139  {
140  log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
142  return resultt::P_SATISFIABLE;
143  }
144  else if(20 == solver_state)
145  {
146  log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
147  }
148  else
149  {
150  log.status() << "SAT checker: solving returned without solution"
151  << messaget::eom;
152  throw analysis_exceptiont(
153  "solving inside IPASIR SAT solver has been interrupted");
154  }
155  }
156 
159 }
160 
161 void satcheck_ipasirt::set_assignment(literalt a, bool value)
162 {
163  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
164  INVARIANT(false, "method not supported");
165 }
166 
168  : cnf_solvert(message_handler), solver(nullptr)
169 {
170  INVARIANT(!solver, "there cannot be a solver already");
171  solver=ipasir_init();
172 }
173 
175 {
176  if(solver)
177  ipasir_release(solver);
178  solver=nullptr;
179 }
180 
182 {
183  return ipasir_failed(solver, a.var_no());
184 }
185 
187 {
188  bvt::const_iterator it = std::find_if(bv.begin(), bv.end(), is_true);
189  const bool has_true = it != bv.end();
190 
191  if(has_true)
192  {
193  assumptions.clear();
194  return;
195  }
196  // only copy assertions, if there is no false in bt parameter
197  assumptions=bv;
198 }
199 
200 #endif
cnft::process_clause
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:425
exception_utils.h
cnf_solvert::statust::SAT
@ SAT
satcheck_ipasirt::set_assignment
void set_assignment(literalt a, bool value) override
bvt
std::vector< literalt > bvt
Definition: literal.h:201
threeval.h
messaget::status
mstreamt & status() const
Definition: message.h:414
propt::resultt::P_UNSATISFIABLE
@ P_UNSATISFIABLE
satcheck_ipasirt::assumptions
bvt assumptions
Definition: satcheck_ipasir.h:68
invariant.h
satcheck_ipasirt::satcheck_ipasirt
satcheck_ipasirt(message_handlert &message_handler)
satcheck_ipasir.h
satcheck_ipasirt::with_solver_hardness
void with_solver_hardness(std::function< void(solver_hardnesst &)> handler) override
Definition: satcheck_ipasir.h:50
satcheck_ipasirt::solver_text
const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
messaget::eom
static eomt eom
Definition: message.h:297
literalt::var_no
var_not var_no() const
Definition: literal.h:83
satcheck_glucose_baset< Glucose::SimpSolver >::solver
std::unique_ptr< Glucose::SimpSolver > solver
Definition: satcheck_glucose.h:77
cnf_solvert
Definition: cnf.h:73
cnf_solvert::statust::ERROR
@ ERROR
is_false
bool is_false(const literalt &l)
Definition: literal.h:197
solver_hardnesst::register_clause
void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
Called e.g.
Definition: solver_hardness.cpp:87
literalt::is_true
bool is_true() const
Definition: literal.h:156
satcheck_ipasirt::is_in_conflict
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
satcheck_ipasirt::l_get
tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
cnf_solvert::statust::UNSAT
@ UNSAT
cnf_solvert::status
statust status
Definition: cnf.h:87
propt::resultt::P_SATISFIABLE
@ P_SATISFIABLE
literalt::is_false
bool is_false() const
Definition: literal.h:161
satcheck_ipasirt::lcnf
void lcnf(const bvt &bv) override final
cnf_solvert::clause_counter
size_t clause_counter
Definition: cnf.h:88
message_handlert
Definition: message.h:28
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
propt::resultt
resultt
Definition: prop.h:97
satcheck_ipasirt::~satcheck_ipasirt
virtual ~satcheck_ipasirt() override
tvt
Definition: threeval.h:20
literalt::sign
bool sign() const
Definition: literal.h:88
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:42
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:407
satcheck_ipasirt::set_assumptions
void set_assumptions(const bvt &_assumptions) override
literalt
Definition: literal.h:26
propt::log
messaget log
Definition: prop.h:128
literalt::is_constant
bool is_constant() const
Definition: literal.h:166
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
cnft::no_variables
virtual size_t no_variables() const override
Definition: cnf.h:42
is_true
bool is_true(const literalt &l)
Definition: literal.h:198
satcheck_ipasirt::do_prop_solve
resultt do_prop_solve() override
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
analysis_exceptiont
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Definition: exception_utils.h:157
satcheck_ipasirt::solver
void * solver
Definition: satcheck_ipasir.h:66