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 <cassert>
12 
13 #include <zchaff_solver.h>
14 
15 satcheck_zchaff_baset::satcheck_zchaff_baset(CSolver *_solver):solver(_solver)
16 {
17  status=INIT;
18  solver->set_randomness(0);
19  solver->set_variable_number(0);
20 }
21 
23 {
24 }
25 
27 {
28  assert(status==SAT);
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  assert(a.var_no()<solver->variables().size());
38 
39  switch(solver->variable(a.var_no()).value())
40  {
41  case 0: result=tvt(false); break;
42  case 1: result=tvt(true); break;
43  default: result=tvt(tvt::tv_enumt::TV_UNKNOWN); break;
44  }
45 
46  if(a.sign())
47  result=!result;
48 
49  return result;
50 }
51 
53 {
54  return solver->version();
55 }
56 
58 {
59  assert(status==INIT);
60 
61  // this can only be called once
62  solver->set_variable_number(no_variables());
63 
64  for(clausest::const_iterator it=clauses.begin();
65  it!=clauses.end();
66  it++)
67  solver->add_orig_clause(
68  reinterpret_cast<int*>(&((*it)[0])), it->size());
69 }
70 
72 {
73  // this is *not* incremental
74  assert(status==INIT);
75 
76  copy_cnf();
77 
78  {
79  std::string msg=
80  std::to_string(solver->num_variables())+" variables, "+
81  std::to_string(solver->clauses().size())+" clauses";
82  messaget::status() << msg << messaget::eom;
83  }
84 
85  SAT_StatusT result=(SAT_StatusT)solver->solve();
86 
87  {
88  std::string msg;
89 
90  switch(result)
91  {
92  case UNSATISFIABLE:
93  msg="SAT checker: instance is UNSATISFIABLE";
94  break;
95 
96  case SATISFIABLE:
97  msg="SAT checker: instance is SATISFIABLE";
98  break;
99 
100  case UNDETERMINED:
101  msg="SAT checker failed: UNDETERMINED";
102  break;
103 
104  case TIME_OUT:
105  msg="SAT checker failed: Time out";
106  break;
107 
108  case MEM_OUT:
109  msg="SAT checker failed: Out of memory";
110  break;
111 
112  case ABORTED:
113  msg="SAT checker failed: ABORTED";
114  break;
115 
116  default:
117  msg="SAT checker failed: unknown result";
118  break;
119  }
120 
121  messaget::status() << msg << messaget::eom;
122  }
123 
124  if(result==SATISFIABLE)
125  {
126  // see if it is complete
127  for(unsigned i=1; i<solver->variables().size(); i++)
128  assert(solver->variables()[i].value()==0 ||
129  solver->variables()[i].value()==1);
130  }
131 
132  #ifdef DEBUG
133  if(result==SATISFIABLE)
134  {
135  for(unsigned i=2; i<(_no_variables*2); i+=2)
136  cout << "DEBUG L" << i << ":" << get(i) << '\n';
137  }
138  #endif
139 
140  if(result==UNSATISFIABLE)
141  {
142  status=UNSAT;
143  return P_UNSATISFIABLE;
144  }
145 
146  if(result==SATISFIABLE)
147  {
148  status=SAT;
149  return P_SATISFIABLE;
150  }
151 
152  status=ERROR;
153 
154  return P_ERROR;
155 }
156 
158 {
159  unsigned v=a.var_no();
160  bool sign=a.sign();
161  value^=sign;
162  solver->variables()[v].set_value(value);
163 }
164 
166  satcheck_zchaff_baset(new CSolver)
167 {
168 }
169 
171 {
172  delete solver;
173 }
mstreamt & result()
Definition: message.h:233
size_t _no_variables
Definition: cnf.h:53
virtual const std::string solver_text()
mstreamt & status()
Definition: message.h:238
satcheck_zchaff_baset(CSolver *_solver)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void set_assignment(literalt a, bool value)
bool is_true() const
Definition: literal.h:155
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
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