cprover
Loading...
Searching...
No Matches
satcheck_cadical.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
9#include "satcheck_cadical.h"
10
12#include <util/invariant.h>
13#include <util/narrow.h>
14#include <util/threeval.h>
15
16#ifdef HAVE_CADICAL
17
18#include <cadical.hpp>
19
21{
22 if(a.is_constant())
23 return tvt(a.sign());
24
25 tvt result;
26
27 if(a.var_no() > narrow<unsigned>(solver->vars()))
29
30 const int val = solver->val(a.dimacs());
31 if(val>0)
32 result = tvt(true);
33 else if(val<0)
34 result = tvt(false);
35 else
37
38 return result;
39}
40
41const std::string satcheck_cadicalt::solver_text()
42{
43 return std::string("CaDiCaL ") + solver->version();
44}
45
46void satcheck_cadicalt::lcnf(const bvt &bv)
47{
48 for(const auto &lit : bv)
49 {
50 if(lit.is_true())
51 return;
52 else if(!lit.is_false())
53 INVARIANT(lit.var_no() < no_variables(), "reject out of bound variables");
54 }
55
56 for(const auto &lit : bv)
57 {
58 if(!lit.is_false())
59 {
60 // add literal with correct sign
61 solver->add(lit.dimacs());
62 }
63 }
64 solver->add(0); // terminate clause
65
67 {
68 // To map clauses to lines of program code, track clause indices in the
69 // dimacs cnf output. Dimacs output is generated after processing
70 // clauses to remove duplicates and clauses that are trivially true.
71 // Here, a clause is checked to see if it can be thus eliminated. If
72 // not, add the clause index to list of clauses in
73 // solver_hardnesst::register_clause().
74 static size_t cnf_clause_index = 0;
75 bvt cnf;
76 bool clause_removed = process_clause(bv, cnf);
77
78 if(!clause_removed)
79 cnf_clause_index++;
80
81 solver_hardness->register_clause(
82 bv, cnf, cnf_clause_index, !clause_removed);
83 }
84
86}
87
89{
90 INVARIANT(status != statust::ERROR, "there cannot be an error");
91
92 log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
93 << " clauses" << messaget::eom;
94
95 // if assumptions contains false, we need this to be UNSAT
96 for(const auto &a : assumptions)
97 {
98 if(a.is_false())
99 {
100 log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
101 << messaget::eom;
104 }
105 }
106
107 for(const auto &a : assumptions)
108 solver->assume(a.dimacs());
109
110 switch(solver->solve())
111 {
112 case 10:
113 log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
116 case 20:
117 log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
118 break;
119 default:
120 log.status() << "SAT checker: solving returned without solution"
121 << messaget::eom;
123 "solving inside CaDiCaL SAT solver has been interrupted");
124 }
125
128}
129
131{
132 INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
133 INVARIANT(false, "method not supported");
134}
135
137 : cnf_solvert(message_handler), solver(new CaDiCaL::Solver())
138{
139 solver->set("quiet", 1);
140}
141
143{
144 delete solver;
145}
146
148{
149 // We filter out 'true' assumptions which cause spurious results with CaDiCaL.
150 assumptions.clear();
151 for(const auto &assumption : bv)
152 {
153 if(!assumption.is_true())
154 {
155 assumptions.push_back(assumption);
156 }
157 }
158}
159
161{
162 return solver->failed(a.dimacs());
163}
164
165#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 sign() const
Definition: literal.h:88
bool is_constant() const
Definition: literal.h:166
int dimacs() const
Definition: literal.h:117
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
virtual ~satcheck_cadicalt()
const std::string solver_text() override
resultt do_prop_solve() override
void set_assignment(literalt a, bool value) override
CaDiCaL::Solver * solver
void lcnf(const bvt &bv) override
satcheck_cadicalt(message_handlert &message_handler)
tvt l_get(literalt a) const override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
Definition: threeval.h:20
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