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/threeval.h>
14 
15 #ifdef HAVE_CADICAL
16 
17 #include <cadical.hpp>
18 
20 {
21  if(a.is_constant())
22  return tvt(a.sign());
23 
24  tvt result;
25 
26  if(a.var_no() > static_cast<unsigned>(solver->max()))
28 
29  const int val = solver->val(a.dimacs());
30  if(val>0)
31  result = tvt(true);
32  else if(val<0)
33  result = tvt(false);
34  else
36 
37  return result;
38 }
39 
40 const std::string satcheck_cadicalt::solver_text()
41 {
42  return std::string("CaDiCaL ") + solver->version();
43 }
44 
45 void satcheck_cadicalt::lcnf(const bvt &bv)
46 {
47  for(const auto &lit : bv)
48  {
49  if(lit.is_true())
50  return;
51  else if(!lit.is_false())
52  INVARIANT(lit.var_no() < no_variables(), "reject out of bound variables");
53  }
54 
55  for(const auto &lit : bv)
56  {
57  if(!lit.is_false())
58  {
59  // add literal with correct sign
60  solver->add(lit.dimacs());
61  }
62  }
63  solver->add(0); // terminate clause
64 
66 }
67 
69 {
70  INVARIANT(status != statust::ERROR, "there cannot be an error");
71 
72  log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
73  << " clauses" << messaget::eom;
74 
75  if(status == statust::UNSAT)
76  {
77  log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
78  << messaget::eom;
79  }
80  else
81  {
82  switch(solver->solve())
83  {
84  case 10:
85  log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
88  case 20:
89  log.status() << "SAT checker: instance is UNSATISFIABLE"
90  << messaget::eom;
91  break;
92  default:
93  log.status() << "SAT checker: solving returned without solution"
94  << messaget::eom;
95  throw analysis_exceptiont(
96  "solving inside CaDiCaL SAT solver has been interrupted");
97  }
98  }
99 
102 }
103 
105 {
106  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
107  INVARIANT(false, "method not supported");
108 }
109 
111  solver(new CaDiCaL::Solver())
112 {
113  solver->set("quiet", 1);
114 }
115 
117 {
118  delete solver;
119 }
120 
122 {
123  INVARIANT(false, "method not supported");
124 }
125 
127 {
128  INVARIANT(false, "method not supported");
129  return false;
130 }
131 
132 #endif
exception_utils.h
satcheck_cadicalt::set_assignment
void set_assignment(literalt a, bool value) override
cnf_solvert::statust::SAT
@ SAT
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:16
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:47
satcheck_cadicalt::set_assumptions
void set_assumptions(const bvt &_assumptions) override
satcheck_cadical.h
cnf_solvert::statust::ERROR
@ ERROR
satcheck_cadicalt::satcheck_cadicalt
satcheck_cadicalt()
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:84
propt::resultt::P_SATISFIABLE
@ P_SATISFIABLE
satcheck_cadicalt::lcnf
void lcnf(const bvt &bv) override
cnf_solvert::clause_counter
size_t clause_counter
Definition: cnf.h:85
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
int solver(std::istream &in)
Definition: smt2_solver.cpp:364
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
cnft::no_variables
virtual size_t no_variables() const override
Definition: cnf.h:41
validation_modet::INVARIANT
@ INVARIANT
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