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 <util/invariant.h>
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  PRECONDITION(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();
45 
46  int r=booleforce_deref(v);
47 
48  if(r>0)
49  result=tvt(true);
50  else if(r<0)
51  result=tvt(false);
52  else
54 
55  if(a.sign())
56  result=!result;
57 
58  return result;
59 }
60 
62 {
63  return std::string("Booleforce version ")+booleforce_version();
64 }
65 
67 {
68  bvt tmp;
69 
70  if(process_clause(bv, tmp))
71  return;
72 
73  for(unsigned j=0; j<tmp.size(); j++)
74  booleforce_add(tmp[j].dimacs());
75 
76  // zero-terminated
77  booleforce_add(0);
78 
80 }
81 
83 {
84  PRECONDITION(status == SAT || status == INIT);
85 
86  int result=booleforce_sat();
87 
88  {
89  std::string msg;
90 
91  switch(result)
92  {
93  case BOOLEFORCE_UNSATISFIABLE:
94  msg="SAT checker: instance is UNSATISFIABLE";
95  break;
96 
97  case BOOLEFORCE_SATISFIABLE:
98  msg="SAT checker: instance is SATISFIABLE";
99  break;
100 
101  default:
102  msg="SAT checker failed: unknown result";
103  break;
104  }
105 
106  log.status() << msg << messaget::eom;
107  }
108 
109  if(result==BOOLEFORCE_UNSATISFIABLE)
110  {
111  status=UNSAT;
112  return P_UNSATISFIABLE;
113  }
114 
115  if(result==BOOLEFORCE_SATISFIABLE)
116  {
117  status=SAT;
118  return P_SATISFIABLE;
119  }
120 
121  status=ERROR;
122 
123  return P_ERROR;
124 }
125 
127 {
128  return booleforce_var_in_core(l.var_no());
129 }
statust status
Definition: cnf.h:86
size_t clause_counter
Definition: cnf.h:87
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:416
virtual size_t no_variables() const override
Definition: cnf.h:41
bool is_true() const
Definition: literal.h:156
bool sign() const
Definition: literal.h:88
var_not var_no() const
Definition: literal.h:83
bool is_false() const
Definition: literal.h:161
mstreamt & status() const
Definition: message.h:414
static eomt eom
Definition: message.h:297
resultt
Definition: prop.h:99
messaget log
Definition: prop.h:130
void lcnf(const bvt &bv) override
tvt l_get(literalt a) const override
resultt do_prop_solve() override
const std::string solver_text() override
bool is_in_core(literalt l) const
Definition: threeval.h:20
static int8_t r
Definition: irep_hash.h:59
std::vector< literalt > bvt
Definition: literal.h:201
@ ERROR
An error occurred during goto checking.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define PRECONDITION(CONDITION)
Definition: invariant.h:464