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  messaget::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 }
static int8_t r
Definition: irep_hash.h:59
size_t clause_counter
Definition: cnf.h:81
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
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
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
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
resultt
Definition: prop.h:96
virtual tvt l_get(literalt a) const
static eomt eom
Definition: message.h:284
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
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:200
bool is_false() const
Definition: literal.h:160