cprover
Loading...
Searching...
No Matches
satcheck_ipasir.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: External SAT Solver Binding
4
5Author: Norbert Manthey, nmanthey@amazon.com
6
7\*******************************************************************/
8
9#include <algorithm>
10
12#include <util/invariant.h>
13#include <util/threeval.h>
14
15#include "satcheck_ipasir.h"
16
17#ifdef HAVE_IPASIR
18
19extern "C"
20{
21#include <ipasir.h>
22}
23
24/*
25
26Interface description:
27https://github.com/biotomas/ipasir/blob/master/ipasir.h
28
29Representation:
30Variables 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
62const std::string satcheck_ipasirt::solver_text()
63{
64 return std::string(ipasir_signature());
65}
66
67void 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 {
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
92 {
93 // To map clauses to lines of program code, track clause indices in the
94 // dimacs cnf output. Dimacs output is generated after processing
95 // clauses to remove duplicates and clauses that are trivially true.
96 // Here, a clause is checked to see if it can be thus eliminated. If
97 // not, add the clause index to list of clauses in
98 // solver_hardnesst::register_clause().
99 static size_t cnf_clause_index = 0;
100 bvt cnf;
101 bool clause_removed = process_clause(bv, cnf);
102
103 if(!clause_removed)
104 cnf_clause_index++;
105
106 solver_hardness->register_clause(
107 bv, cnf, cnf_clause_index, !clause_removed);
108 }
109
111}
112
114{
115 INVARIANT(status!=statust::ERROR, "there cannot be an error");
116
117 log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
118 << " clauses" << messaget::eom;
119
120 // if assumptions contains false, we need this to be UNSAT
121 bvt::const_iterator it =
122 std::find_if(assumptions.begin(), assumptions.end(), is_false);
123 const bool has_false = it != assumptions.end();
124
125 if(has_false)
126 {
127 log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
128 << messaget::eom;
129 }
130 else
131 {
132 for(const auto &literal : assumptions)
133 {
134 if(!literal.is_false())
135 ipasir_assume(solver, literal.dimacs());
136 }
137
138 // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
139 int solver_state = ipasir_solve(solver);
140 if(10 == solver_state)
141 {
142 log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
145 }
146 else if(20 == solver_state)
147 {
148 log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
149 }
150 else
151 {
152 log.status() << "SAT checker: solving returned without solution"
153 << messaget::eom;
155 "solving inside IPASIR SAT solver has been interrupted");
156 }
157 }
158
161}
162
164{
165 INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
166 INVARIANT(false, "method not supported");
167}
168
170 : cnf_solvert(message_handler), solver(nullptr)
171{
172 INVARIANT(!solver, "there cannot be a solver already");
173 solver=ipasir_init();
174}
175
177{
178 if(solver)
179 ipasir_release(solver);
180 solver=nullptr;
181}
182
184{
185 return ipasir_failed(solver, a.var_no());
186}
187
189{
190 bvt::const_iterator it = std::find_if(bv.begin(), bv.end(), is_true);
191 const bool has_true = it != bv.end();
192
193 if(has_true)
194 {
195 assumptions.clear();
196 return;
197 }
198 // only copy assertions, if there is no false in bt parameter
199 assumptions=bv;
200}
201
202#endif
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
statust status
Definition cnf.h:87
size_t clause_counter
Definition cnf.h:88
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition cnf.cpp:425
virtual size_t no_variables() const override
Definition cnf.h:42
std::unique_ptr< clause_hardness_collectort > solver_hardness
bool is_true() const
Definition literal.h:156
bool sign() const
Definition literal.h:88
bool is_constant() const
Definition literal.h:166
var_not var_no() const
Definition literal.h:83
bool is_false() const
Definition literal.h:161
mstreamt & statistics() const
Definition message.h:419
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
resultt
Definition prop.h:98
messaget log
Definition prop.h:129
void set_assumptions(const bvt &_assumptions) override
tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
resultt do_prop_solve() override
virtual ~satcheck_ipasirt() override
satcheck_ipasirt(message_handlert &message_handler)
void lcnf(const bvt &bv) override final
void set_assignment(literalt a, bool value) override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
Definition threeval.h:20
static tvt unknown()
Definition threeval.h:33
bool is_false(const literalt &l)
Definition literal.h:197
bool is_true(const literalt &l)
Definition literal.h:198
std::vector< literalt > bvt
Definition literal.h:201
int solver(std::istream &in)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423