cprover
Loading...
Searching...
No Matches
satcheck_booleforce.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
11#include <util/invariant.h>
12
13extern "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{
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{
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 {
112 return P_UNSATISFIABLE;
113 }
114
115 if(result==BOOLEFORCE_SATISFIABLE)
116 {
117 status=SAT;
118 return P_SATISFIABLE;
119 }
120
122
123 return P_ERROR;
124}
125
127{
128 return booleforce_var_in_core(l.var_no());
129}
statust status
Definition: cnf.h:87
size_t clause_counter
Definition: cnf.h:88
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
Definition: cnf.cpp:425
virtual size_t no_variables() const override
Definition: cnf.h:42
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
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
resultt
Definition: prop.h:98
messaget log
Definition: prop.h:129
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:60
std::vector< literalt > bvt
Definition: literal.h:201
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463