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
22
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
78
80}
81
83{
85
86 int result=booleforce_sat();
87
88 {
89 std::string msg;
90
91 switch(result)
92 {
94 msg="SAT checker: instance is UNSATISFIABLE";
95 break;
96
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
var_not var_no() const
Definition literal.h:83
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
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