cprover
satcheck_zchaff.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "satcheck_zchaff.h"
10
11#include <util/invariant.h>
12
13#include <zchaff_solver.h>
14
16{
18 solver->set_randomness(0);
19 solver->set_variable_number(0);
20}
21
23{
24}
25
27{
29
30 if(a.is_true())
31 return tvt(true);
32 else if(a.is_false())
33 return tvt(false);
34
35 tvt result;
36
38 a.var_no() < solver->variables().size(),
39 "variable number shall be within bounds");
40
41 switch(solver->variable(a.var_no()).value())
42 {
43 case 0: result=tvt(false); break;
44 case 1: result=tvt(true); break;
45 default: result=tvt(tvt::tv_enumt::TV_UNKNOWN); break;
46 }
47
48 if(a.sign())
49 result=!result;
50
51 return result;
52}
53
55{
56 return solver->version();
57}
58
60{
62
63 // this can only be called once
64 solver->set_variable_number(no_variables());
65
66 for(clausest::const_iterator it=clauses.begin();
67 it!=clauses.end();
68 it++)
69 solver->add_orig_clause(
70 reinterpret_cast<int*>(&((*it)[0])), it->size());
71}
72
74{
75 // this is *not* incremental
77
78 copy_cnf();
79
80 {
81 std::string msg=
82 std::to_string(solver->num_variables())+" variables, "+
83 std::to_string(solver->clauses().size())+" clauses";
84 log.statistics() << msg << messaget::eom;
85 }
86
87 SAT_StatusT result=(SAT_StatusT)solver->solve();
88
89 {
90 std::string msg;
91
92 switch(result)
93 {
94 case UNSATISFIABLE:
95 msg="SAT checker: instance is UNSATISFIABLE";
96 break;
97
98 case SATISFIABLE:
99 msg="SAT checker: instance is SATISFIABLE";
100 break;
101
102 case UNDETERMINED:
103 msg="SAT checker failed: UNDETERMINED";
104 break;
105
106 case TIME_OUT:
107 msg="SAT checker failed: Time out";
108 break;
109
110 case MEM_OUT:
111 msg="SAT checker failed: Out of memory";
112 break;
113
114 case ABORTED:
115 msg="SAT checker failed: ABORTED";
116 break;
117
118 default:
119 msg="SAT checker failed: unknown result";
120 break;
121 }
122
123 log.status() << msg << messaget::eom;
124 }
125
126 if(result==SATISFIABLE)
127 {
128 // see if it is complete
129 for(unsigned i=1; i<solver->variables().size(); i++)
130 INVARIANT(
131 solver->variables()[i].value() == 0 ||
132 solver->variables()[i].value() == 1,
133 "all variables shall have been assigned");
134 }
135
136 #ifdef DEBUG
137 if(result==SATISFIABLE)
138 {
139 for(unsigned i=2; i<(_no_variables*2); i+=2)
140 cout << "DEBUG L" << i << ":" << get(i) << '\n';
141 }
142 #endif
143
144 if(result==UNSATISFIABLE)
145 {
147 return P_UNSATISFIABLE;
148 }
149
150 if(result==SATISFIABLE)
151 {
152 status=SAT;
153 return P_SATISFIABLE;
154 }
155
157
158 return P_ERROR;
159}
160
162{
163 unsigned v=a.var_no();
164 bool sign=a.sign();
165 value^=sign;
166 solver->variables()[v].set_value(value);
167}
168
170 satcheck_zchaff_baset(new CSolver)
171{
172}
173
175{
176 delete solver;
177}
virtual size_t no_variables() const override
Definition: cnf.h:42
size_t _no_variables
Definition: cnf.h:57
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 & statistics() const
Definition: message.h:419
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
resultt
Definition: prop.h:97
messaget log
Definition: prop.h:128
resultt do_prop_solve() override
const std::string solver_text() override
void set_assignment(literalt a, bool value) override
satcheck_zchaff_baset(CSolver *_solver)
tvt l_get(literalt a) const override
virtual ~satcheck_zchafft()
Definition: threeval.h:20
int solver(std::istream &in)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.