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 <cassert>
12 
13 #include <util/threeval.h>
14 
15 extern "C"
16 {
17 #include <picosat.h>
18 }
19 
20 #ifndef HAVE_PICOSAT
21 #error "Expected HAVE_PICOSAT"
22 #endif
23 
25 {
26  if(a.is_constant())
27  return tvt(a.sign());
28 
29  tvt result;
30 
31  if(static_cast<int>(a.var_no())>picosat_variables(picosat))
33 
34  const int val=picosat_deref(picosat, a.dimacs());
35  if(val>0)
36  result=tvt(true);
37  else if(val<0)
38  result=tvt(false);
39  else
41 
42  return result;
43 }
44 
45 const std::string satcheck_picosatt::solver_text()
46 {
47  return "PicoSAT";
48 }
49 
51 {
52  bvt new_bv;
53 
54  if(process_clause(bv, new_bv))
55  return;
56 
57  picosat_adjust(picosat, _no_variables);
58 
59  forall_literals(it, new_bv)
60  picosat_add(picosat, it->dimacs());
61 
62  picosat_add(picosat, 0);
63 
65 }
66 
68 {
69  assert(status!=ERROR);
70 
71  {
72  std::string msg=
73  std::to_string(_no_variables-1)+" variables, "+
74  std::to_string(picosat_added_original_clauses(picosat))+" clauses";
75  messaget::status() << msg << messaget::eom;
76  }
77 
78  std::string msg;
79 
81  picosat_assume(picosat, it->dimacs());
82 
83  const int res=picosat_sat(picosat, -1);
84  if(res==PICOSAT_SATISFIABLE)
85  {
86  msg="SAT checker: instance is SATISFIABLE";
87  messaget::status() << msg << messaget::eom;
88  status=SAT;
89  return P_SATISFIABLE;
90  }
91  else
92  {
93  assert(res==PICOSAT_UNSATISFIABLE);
94  msg="SAT checker: instance is UNSATISFIABLE";
95  messaget::status() << msg << messaget::eom;
96  }
97 
98  status=UNSAT;
99  return P_UNSATISFIABLE;
100 }
101 
103 {
104  assert(false);
105 }
106 
108 {
109  picosat = picosat_init();
110 }
111 
113 {
114  picosat_reset(picosat);
115 }
116 
118 {
119  assert(!a.is_constant());
120 
121  return picosat_failed_assumption(picosat, a.dimacs())!=0;
122 }
123 
125 {
126  assumptions=bv;
127 
129  assert(!it->is_constant());
130 }
mstreamt & result()
Definition: message.h:233
virtual void set_assumptions(const bvt &_assumptions)
size_t _no_variables
Definition: cnf.h:53
size_t clause_counter
Definition: cnf.h:81
mstreamt & status()
Definition: message.h:238
bool process_clause(const bvt &bv, bvt &dest)
filter &#39;true&#39; from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition: cnf.cpp:416
int dimacs() const
Definition: literal.h:116
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
#define forall_literals(it, bv)
Definition: literal.h:199
virtual const std::string solver_text()
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
virtual tvt l_get(literalt a) const
virtual resultt prop_solve()
bool is_constant() const
Definition: literal.h:165
virtual bool is_in_conflict(literalt a) const
bool sign() const
Definition: literal.h:87
virtual void lcnf(const bvt &bv)
virtual void set_assignment(literalt a, bool value)
std::vector< literalt > bvt
Definition: literal.h:197