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/invariant.h>
12 #include <util/threeval.h>
13 
14 #ifdef HAVE_CADICAL
15 
16 #include <cadical.hpp>
17 
19 {
20  if(a.is_constant())
21  return tvt(a.sign());
22 
23  tvt result;
24 
25  if(a.var_no() > static_cast<unsigned>(solver->max()))
27 
28  const int val = solver->val(a.dimacs());
29  if(val>0)
30  result = tvt(true);
31  else if(val<0)
32  result = tvt(false);
33  else
35 
36  return result;
37 }
38 
39 const std::string satcheck_cadicalt::solver_text()
40 {
41  return std::string("CaDiCaL ") + solver->version();
42 }
43 
44 void satcheck_cadicalt::lcnf(const bvt &bv)
45 {
46  for(const auto &lit : bv)
47  {
48  if(lit.is_true())
49  return;
50  else if(!lit.is_false())
51  INVARIANT(lit.var_no() < no_variables(), "reject out of bound variables");
52  }
53 
54  for(const auto &lit : bv)
55  {
56  if(!lit.is_false())
57  {
58  // add literal with correct sign
59  solver->add(lit.dimacs());
60  }
61  }
62  solver->add(0); // terminate clause
63 
65 }
66 
68 {
69  INVARIANT(status != statust::ERROR, "there cannot be an error");
70 
71  messaget::status() << (no_variables() - 1) << " variables, " << clause_counter
72  << " clauses" << eom;
73 
74  if(status == statust::UNSAT)
75  {
76  messaget::status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
77  << eom;
78  }
79  else
80  {
81  switch(solver->solve())
82  {
83  case 10:
84  messaget::status() << "SAT checker: instance is SATISFIABLE" << eom;
87  case 20:
88  messaget::status() << "SAT checker: instance is UNSATISFIABLE" << eom;
89  break;
90  default:
91  messaget::status() << "SAT checker: solving returned without solution"
92  << eom;
93  throw "solving inside CaDiCaL SAT solver has been interrupted";
94  }
95  }
96 
99 }
100 
102 {
103  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
104  INVARIANT(false, "method not supported");
105 }
106 
108  solver(new CaDiCaL::Solver())
109 {
110  solver->set("quiet", 1);
111 }
112 
114 {
115  delete solver;
116 }
117 
119 {
120  INVARIANT(false, "method not supported");
121 }
122 
124 {
125  INVARIANT(false, "method not supported");
126  return false;
127 }
128 
129 #endif
virtual void set_assumptions(const bvt &_assumptions) override
size_t clause_counter
Definition: cnf.h:81
int dimacs() const
Definition: literal.h:116
virtual ~satcheck_cadicalt()
virtual const std::string solver_text() override
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
virtual resultt prop_solve() override
CaDiCaL::Solver * solver
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
virtual void lcnf(const bvt &bv) override
int solver(std::istream &in)
virtual tvt l_get(literalt a) const override
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:96
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
bool is_constant() const
Definition: literal.h:165
virtual void set_assignment(literalt a, bool value) override
bool sign() const
Definition: literal.h:87
virtual bool is_in_conflict(literalt a) const override
virtual size_t no_variables() const override
Definition: cnf.h:38
std::vector< literalt > bvt
Definition: literal.h:200