cprover
satcheck_picosat.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
9 #include "satcheck_picosat.h"
10 
11 #include <algorithm>
12 
13 #include <util/invariant.h>
14 #include <util/threeval.h>
15 
16 extern "C"
17 {
18 #include <picosat.h>
19 }
20 
21 #ifndef HAVE_PICOSAT
22 #error "Expected HAVE_PICOSAT"
23 #endif
24 
26 {
27  if(a.is_constant())
28  return tvt(a.sign());
29 
30  tvt result;
31 
32  if(static_cast<int>(a.var_no())>picosat_variables(picosat))
34 
35  const int val=picosat_deref(picosat, a.dimacs());
36  if(val>0)
37  result=tvt(true);
38  else if(val<0)
39  result=tvt(false);
40  else
42 
43  return result;
44 }
45 
46 const std::string satcheck_picosatt::solver_text()
47 {
48  return "PicoSAT";
49 }
50 
52 {
53  bvt new_bv;
54 
55  if(process_clause(bv, new_bv))
56  return;
57 
58  picosat_adjust(picosat, _no_variables);
59 
60  forall_literals(it, new_bv)
61  picosat_add(picosat, it->dimacs());
62 
63  picosat_add(picosat, 0);
64 
66 }
67 
69 {
70  PRECONDITION(status != ERROR);
71 
72  {
73  std::string msg=
74  std::to_string(_no_variables-1)+" variables, "+
75  std::to_string(picosat_added_original_clauses(picosat))+" clauses";
76  messaget::status() << msg << messaget::eom;
77  }
78 
79  std::string msg;
80 
82  picosat_assume(picosat, it->dimacs());
83 
84  const int res=picosat_sat(picosat, -1);
85  if(res==PICOSAT_SATISFIABLE)
86  {
87  msg="SAT checker: instance is SATISFIABLE";
88  messaget::status() << msg << messaget::eom;
89  status=SAT;
90  return P_SATISFIABLE;
91  }
92  else
93  {
94  INVARIANT(
95  res == PICOSAT_UNSATISFIABLE,
96  "picosat result should report either sat or unsat");
97  msg="SAT checker: instance is UNSATISFIABLE";
98  messaget::status() << msg << messaget::eom;
99  }
100 
101  status=UNSAT;
102  return P_UNSATISFIABLE;
103 }
104 
106 {
107  UNREACHABLE;
108 }
109 
111 {
112  picosat = picosat_init();
113 }
114 
116 {
117  picosat_reset(picosat);
118 }
119 
121 {
123 
124  return picosat_failed_assumption(picosat, a.dimacs())!=0;
125 }
126 
128 {
129  assumptions=bv;
130 
131  INVARIANT(
132  std::all_of(
133  assumptions.begin(),
134  assumptions.end(),
135  [](const literalt &l) { return !l.is_constant(); }),
136  "assumptions should be non-constant");
137 }
virtual void set_assumptions(const bvt &_assumptions)
size_t _no_variables
Definition: cnf.h:53
size_t clause_counter
Definition: cnf.h:81
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:416
int dimacs() const
Definition: literal.h:116
#define forall_literals(it, bv)
Definition: literal.h:202
virtual const std::string solver_text()
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
resultt
Definition: prop.h:96
virtual tvt l_get(literalt a) const
virtual resultt prop_solve()
static eomt eom
Definition: message.h:284
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
bool is_constant() const
Definition: literal.h:165
virtual bool is_in_conflict(literalt a) const
Returns true if an assumption is in the final conflict.
bool sign() const
Definition: literal.h:87
virtual void lcnf(const bvt &bv)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
virtual void set_assignment(literalt a, bool value)
std::vector< literalt > bvt
Definition: literal.h:200