cprover
satcheck_booleforce.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "satcheck_booleforce.h"
10 
11 #include <cassert>
12 
13 extern "C"
14 {
15 #include "booleforce.h"
16 }
17 
19 {
20  booleforce_set_trace(false);
21 }
22 
24 {
25  booleforce_set_trace(true);
26 }
27 
29 {
30  booleforce_reset();
31 }
32 
34 {
35  assert(status==SAT);
36 
37  if(a.is_true())
38  return tvt(true);
39  else if(a.is_false())
40  return tvt(false);
41 
42  tvt result;
43  unsigned v=a.var_no();
44 
45  assert(v<no_variables());
46 
47  int r=booleforce_deref(v);
48 
49  if(r>0)
50  result=tvt(true);
51  else if(r<0)
52  result=tvt(false);
53  else
55 
56  if(a.sign())
57  result=!result;
58 
59  return result;
60 }
61 
63 {
64  return std::string("Booleforce version ")+booleforce_version();
65 }
66 
68 {
69  bvt tmp;
70 
71  if(process_clause(bv, tmp))
72  return;
73 
74  for(unsigned j=0; j<tmp.size(); j++)
75  booleforce_add(tmp[j].dimacs());
76 
77  // zero-terminated
78  booleforce_add(0);
79 
81 }
82 
84 {
85  assert(status==SAT || status==INIT);
86 
87  int result=booleforce_sat();
88 
89  {
90  std::string msg;
91 
92  switch(result)
93  {
94  case BOOLEFORCE_UNSATISFIABLE:
95  msg="SAT checker: instance is UNSATISFIABLE";
96  break;
97 
98  case BOOLEFORCE_SATISFIABLE:
99  msg="SAT checker: instance is SATISFIABLE";
100  break;
101 
102  default:
103  msg="SAT checker failed: unknown result";
104  break;
105  }
106 
107  messaget::status() << msg << messaget::eom;
108  }
109 
110  if(result==BOOLEFORCE_UNSATISFIABLE)
111  {
112  status=UNSAT;
113  return P_UNSATISFIABLE;
114  }
115 
116  if(result==BOOLEFORCE_SATISFIABLE)
117  {
118  status=SAT;
119  return P_SATISFIABLE;
120  }
121 
122  status=ERROR;
123 
124  return P_ERROR;
125 }
126 
128 {
129  return booleforce_var_in_core(l.var_no());
130 }
mstreamt & result()
Definition: message.h:233
static int8_t r
Definition: irep_hash.h:59
size_t clause_counter
Definition: cnf.h:81
mstreamt & status()
Definition: message.h:238
bool is_in_core(literalt l) const
bool process_clause(const bvt &bv, bvt &dest)
filter &#39;true&#39; from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition: cnf.cpp:416
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void lcnf(const bvt &bv)
virtual const std::string solver_text()
bool is_true() const
Definition: literal.h:155
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
bool sign() const
Definition: literal.h:87
virtual size_t no_variables() const override
Definition: cnf.h:38
std::vector< literalt > bvt
Definition: literal.h:197
bool is_false() const
Definition: literal.h:160