cprover
satcheck_zchaff.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_zchaff.h"
10 
11 #include <util/invariant.h>
12 
13 #include <zchaff_solver.h>
14 
16 {
17  status=INIT;
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 
37  INVARIANT(
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  messaget::status() << 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  messaget::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  {
146  status=UNSAT;
147  return P_UNSATISFIABLE;
148  }
149 
150  if(result==SATISFIABLE)
151  {
152  status=SAT;
153  return P_SATISFIABLE;
154  }
155 
156  status=ERROR;
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 }
size_t _no_variables
Definition: cnf.h:53
virtual const std::string solver_text()
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
satcheck_zchaff_baset(CSolver *_solver)
virtual void set_assignment(literalt a, bool value)
int solver(std::istream &in)
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 resultt prop_solve()
static eomt eom
Definition: message.h:284
virtual tvt l_get(literalt a) const
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
bool sign() const
Definition: literal.h:87
virtual ~satcheck_zchafft()
virtual size_t no_variables() const override
Definition: cnf.h:38
bool is_false() const
Definition: literal.h:160