cprover
satcheck_cadical.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 #include "satcheck_cadical.h"
10 
11 #include <util/exception_utils.h>
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 
41 const std::string satcheck_cadicalt::solver_text()
42 {
43  return std::string("CaDiCaL ") + solver->version();
44 }
45 
46 void 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 
66  with_solver_hardness([this, &bv](solver_hardnesst &hardness) {
67  // To map clauses to lines of program code, track clause indices in the
68  // dimacs cnf output. Dimacs output is generated after processing
69  // clauses to remove duplicates and clauses that are trivially true.
70  // Here, a clause is checked to see if it can be thus eliminated. If
71  // not, add the clause index to list of clauses in
72  // solver_hardnesst::register_clause().
73  static size_t cnf_clause_index = 0;
74  bvt cnf;
75  bool clause_removed = process_clause(bv, cnf);
76 
77  if(!clause_removed)
78  cnf_clause_index++;
79 
80  hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
81  });
82 
84 }
85 
87 {
88  INVARIANT(status != statust::ERROR, "there cannot be an error");
89 
90  log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
91  << " clauses" << messaget::eom;
92 
93  // if assumptions contains false, we need this to be UNSAT
94  for(const auto &a : assumptions)
95  {
96  if(a.is_false())
97  {
98  log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
99  << messaget::eom;
102  }
103  }
104 
105  for(const auto &a : assumptions)
106  solver->assume(a.dimacs());
107 
108  switch(solver->solve())
109  {
110  case 10:
111  log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
113  return resultt::P_SATISFIABLE;
114  case 20:
115  log.status() << "SAT checker: instance is UNSATISFIABLE" << messaget::eom;
116  break;
117  default:
118  log.status() << "SAT checker: solving returned without solution"
119  << messaget::eom;
120  throw analysis_exceptiont(
121  "solving inside CaDiCaL SAT solver has been interrupted");
122  }
123 
126 }
127 
129 {
130  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
131  INVARIANT(false, "method not supported");
132 }
133 
135  : cnf_solvert(message_handler), solver(new CaDiCaL::Solver())
136 {
137  solver->set("quiet", 1);
138 }
139 
141 {
142  delete solver;
143 }
144 
146 {
147  // We filter out 'true' assumptions which cause spurious results with CaDiCaL.
148  assumptions.clear();
149  for(const auto &assumption : bv)
150  {
151  if(!assumption.is_true())
152  {
153  assumptions.push_back(assumption);
154  }
155  }
156 }
157 
159 {
160  return solver->failed(a.dimacs());
161 }
162 
163 #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:416
exception_utils.h
satcheck_cadicalt::set_assignment
void set_assignment(literalt a, bool value) override
cnf_solvert::statust::SAT
@ SAT
satcheck_cadicalt::with_solver_hardness
void with_solver_hardness(std::function< void(solver_hardnesst &)> handler) override
Definition: satcheck_cadical.h:46
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_cadicalt::is_in_conflict
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
literalt::dimacs
int dimacs() const
Definition: literal.h:117
invariant.h
CaDiCaL
Definition: satcheck_cadical.h:18
messaget::eom
static eomt eom
Definition: message.h:297
literalt::var_no
var_not var_no() const
Definition: literal.h:83
satcheck_cadicalt::solver
CaDiCaL::Solver * solver
Definition: satcheck_cadical.h:63
satcheck_cadicalt::set_assumptions
void set_assumptions(const bvt &_assumptions) override
satcheck_cadicalt::satcheck_cadicalt
satcheck_cadicalt(message_handlert &message_handler)
satcheck_cadical.h
cnf_solvert
Definition: cnf.h:72
cnf_solvert::statust::ERROR
@ ERROR
narrow.h
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:92
satcheck_cadicalt::~satcheck_cadicalt
virtual ~satcheck_cadicalt()
cnf_solvert::statust::UNSAT
@ UNSAT
satcheck_cadicalt::do_prop_solve
resultt do_prop_solve() override
cnf_solvert::status
statust status
Definition: cnf.h:86
propt::resultt::P_SATISFIABLE
@ P_SATISFIABLE
literalt::is_false
bool is_false() const
Definition: literal.h:161
satcheck_cadicalt::lcnf
void lcnf(const bvt &bv) override
cnf_solvert::clause_counter
size_t clause_counter
Definition: cnf.h:87
message_handlert
Definition: message.h:28
propt::resultt
resultt
Definition: prop.h:99
satcheck_cadicalt::l_get
tvt l_get(literalt a) const 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:45
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:368
literalt
Definition: literal.h:26
tvt::tv_enumt::TV_UNKNOWN
@ TV_UNKNOWN
propt::log
messaget log
Definition: prop.h:130
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:424
cnft::no_variables
virtual size_t no_variables() const override
Definition: cnf.h:41
satcheck_cadicalt::assumptions
bvt assumptions
Definition: satcheck_cadical.h:65
satcheck_cadicalt::solver_text
const std::string solver_text() 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