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
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{
84 PRECONDITION(assumptions.empty());
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 log.status() << msg << messaget::eom;
108 }
109
110 if(result==BOOLEFORCE_UNSATISFIABLE)
111 {
113 return P_UNSATISFIABLE;
114 }
115
116 if(result==BOOLEFORCE_SATISFIABLE)
117 {
118 status=SAT;
119 return P_SATISFIABLE;
120 }
121
123
124 return P_ERROR;
125}
126
128{
129 return booleforce_var_in_core(l.var_no());
130}
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:424
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:289
mstreamt & status() const
Definition message.h:406
resultt
Definition prop.h:101
messaget log
Definition prop.h:134
void lcnf(const bvt &bv) override
std::string solver_text() const override
resultt do_prop_solve(const bvt &assumptions) override
tvt l_get(literalt a) const 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