CVC3  2.4.1
dpllt_minisat.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file dpllt_minisat.cpp
4  *\brief Implementation of dpllt module using MiniSat
5  *
6  * Author: Alexander Fuchs
7  *
8  * Created: Fri Sep 08 11:04:00 2006
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 //we need this to use newPf
21 #define _CVC3_TRUSTED_
22 
23 #include "dpllt_minisat.h"
24 #include "minisat_solver.h"
25 #include "sat_proof.h"
26 #include "theorem_producer.h"
27 #include "exception.h"
28 
29 using namespace std;
30 using namespace CVC3;
31 using namespace SAT;
32 
33 
34 DPLLTMiniSat::DPLLTMiniSat(TheoryAPI* theoryAPI, Decider* decider,
35  bool printStats, bool createProof)
36  : DPLLT(theoryAPI, decider), d_printStats(printStats),
37  d_createProof(createProof), d_proof(NULL) {
38  pushSolver();
39 }
40 
42  while (!d_solvers.empty()) {
43  // don't pop theories, this is not allowed when cvc shuts down.
44  delete (d_solvers.top());
45  d_solvers.pop();
46  }
47  delete d_proof;
48 }
49 
51  DebugAssert(!d_solvers.empty(), "DPLLTMiniSat::getActiveSolver: no solver");
52  return d_solvers.top();
53 }
54 
55 
57  if (d_solvers.empty()) {
59  }
60  else {
62  }
63 }
64 
66 {
67  DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::search: no solver");
68  DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::search: solver not pushed");
69 
70  // search
71  MiniSat::Solver* solver = getActiveSolver();
72  QueryResult result = solver->search();
73 
74  // print statistics
75  if (d_printStats) {
76  switch (result) {
77  case SATISFIABLE:
78  break;
79  case UNSATISFIABLE:
80  cout << "Instance unsatisfiable" << endl;
81  break;
82  case ABORT:
83  cout << "aborted, unable to determine the satisfiablility of the instance" << endl;
84  break;
85  case UNKNOWN:
86  cout << "unknown, unable to determing the satisfiablility of the instance" << endl;
87  break;
88  default:
89  FatalAssert(false, "DPLTBasic::handle_result: Unknown outcome");
90  }
91 
92  cout << "Number of Decisions\t\t\t" << solver->getStats().decisions << endl;
93  cout << "Number of Propagations\t\t\t" << solver->getStats().propagations << endl;
94  cout << "Number of Propositional Conflicts\t"
95  << (solver->getStats().conflicts - solver->getStats().theory_conflicts) << endl;
96  cout << "Number of Theory Conflicts\t\t" << solver->getStats().theory_conflicts << endl;
97  cout << "Number of Variables\t\t\t" << solver->nVars() << endl;
98  cout << "Number of Literals\t\t\t"
99  << (solver->getStats().clauses_literals + solver->getStats().learnts_literals) << endl;
100  cout << "Max. Number of Literals\t\t\t" << solver->getStats().max_literals << endl;
101  cout << "Number of Clauses\t\t\t" << solver->getClauses().size() << endl;
102  cout << "Number of Lemmas\t\t\t" << solver->getLemmas().size() << endl;
103  cout << "Max. Decision Level\t\t\t" << solver->getStats().max_level << endl;
104  cout << "Number of Deleted Clauses\t\t" << solver->getStats().del_clauses << endl;
105  cout << "Number of Deleted Lemmas\t\t" << solver->getStats().del_lemmas << endl;
106  cout << "Number of Database Simplifications\t" << solver->getStats().db_simpl << endl;
107  cout << "Number of Lemma Cleanups\t\t" << solver->getStats().lm_simpl << endl;
108 
109  cout << "Debug\t\t\t\t\t" << solver->getStats().debug << endl;
110  }
111 
112  // the dpllt interface requires that for an unsat result
113  // all theory pops are undone right away.
114  if (result == UNSATISFIABLE) {
115  // cout << "unsat" <<endl;
116  // return result;
117  if (d_createProof ) {
118  delete d_proof;
119  // cout<<"creating proof" << endl;
120  DebugAssert(d_solvers.top()->getDerivation() != NULL, "DplltMiniSat::search: no proof");
121  d_proof = d_solvers.top()->getDerivation()->createProof();
122  }
123  d_solvers.top()->popTheories();
124  d_theoryAPI->pop();
125  }
126 
127  return result;
128 }
129 
130 
132 {
133  DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::checkSat: no solver");
134 
135  // perform any requested solver pops
136  getActiveSolver()->doPops();
137 
138  DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::checkSat: solver already in search");
139 
140  // required by dpllt interface: theory push before search
141  d_theoryAPI->push();
142 
143  // solver already in use, so create a new solver
144  if (getActiveSolver()->inSearch()) {
145  pushSolver();
146  }
147 
148  // add new formula and search
149  getActiveSolver()->addFormula(cnf, false);
150  return search();
151 }
152 
153 
155 {
156  DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::continueCheck: no solver");
157 
158  // if the current solver has no push, all its pushes have already been undone,
159  // so remove it
160  if (!getActiveSolver()->inPush()) {
161  DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::continueCheck: solver without push in search");
162  delete getActiveSolver();
163  d_solvers.pop();
164  }
165 
166  // perform any requested solver pops
167  getActiveSolver()->doPops();
168 
169  DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::continueCheck: no solver (2)");
170  DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::continueCheck: solver not in push");
171  DebugAssert(getActiveSolver()->inSearch(), "DPLLTMiniSat::continueCheck: solver not in search");
172 
173  // add new formula and search
174  getActiveSolver()->addFormula(cnf, false);
175  return search();
176 }
177 
178 
180  // perform any requested solver pops
181  getActiveSolver()->doPops();
182 
183  // if the current solver is already in a search, then create a new one
184  if (getActiveSolver()->inSearch()) {
185  pushSolver();
186  }
187 
188  getActiveSolver()->push();
189  d_theoryAPI->push();
190 }
191 
193  DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::pop: no solver");
194 
195  // if the current solver has no push, all its pushes have already been undone,
196  // so remove it
197  if (!getActiveSolver()->inPush()) {
198  DebugAssert(!getActiveSolver()->inSearch(), "DPLLTMiniSat::pop: solver without push in search");
199  delete getActiveSolver();
200  d_solvers.pop();
201  }
202 
203  DebugAssert(d_solvers.size() > 0, "DPLLTMiniSat::pop: no solver 2");
204  DebugAssert(getActiveSolver()->inPush(), "DPLLTMiniSat::pop: solver not in push");
205 
206  // undo checkSat theory push for an invalid query.
207  // for a valid query this is done in search right away.
208  if (getActiveSolver()->inSearch() && getActiveSolver()->isConsistent()) {
209  d_theoryAPI->pop();
210  }
212  d_theoryAPI->pop();
213 }
214 
215 std::vector<SAT::Lit> DPLLTMiniSat::getCurAssignments(){
216  return getActiveSolver()->curAssigns();
217 }
218 
219 std::vector<std::vector<SAT::Lit> > DPLLTMiniSat::getCurClauses(){
220  return getActiveSolver()->curClauses();
221 }
222 
224  // perform any requested solver pops
225  getActiveSolver()->doPops();
226 
227  // if the current solver is already performing a search create a new solver
228  if (getActiveSolver()->inSearch()) {
229  pushSolver();
230  }
231 
232  getActiveSolver()->addFormula(cnf, false);
233 
234  // Immediately assert unit clauses -
235  // the intention is to make these immediately available for interactive use
236  for (CNF_Formula::const_iterator i = cnf.begin(); i != cnf.end(); ++i) {
237  if ((*i).isUnit() && getActiveSolver()->isConsistent()) {
238  d_theoryAPI->assertLit(*(*i).begin());
239  }
240  }
241 }
242 
243 
245  DebugAssert(d_solvers.size() > 0,
246  "DPLLTMiniSat::getValue: should be called after a previous satisfiable result");
247 
249  if (value == MiniSat::l_True)
250  return Var::TRUE_VAL;
251  else if (value == MiniSat::l_False)
252  return Var::FALSE_VAL;
253  else
254  return Var::UNKNOWN;
255 }
256 
257 
259  if(node->hasNodeProof()) {
260  return node->getNodeProof();
261  }
262  if (node->isLeaf()){
263 
264  /*
265 //<<<<<<< dpllt_minisat.cpp
266 
267  SAT::Clause curClause = *(node->getLeaf());
268 
269  DebugAssert(!curClause.isNull(), "Null clause found in generateSatProof");
270 
271  cout << "get leaf clause " << curClause.getId() << endl;
272 
273  const CVC3::Theorem clauseThm = curClause.getClauseTheorem();
274 //=======
275  */
276 
277  const CVC3::Theorem clauseThm = node->getLeaf();
278 
279  /*
280 //>>>>>>> 1.14
281  */
282 
283  DebugAssert(!clauseThm.isNull(), "Null thm found in generateSatProof");
284  node->setNodeProof(clauseThm.getProof());
285 // cout<<"set proof " << clauseThm.getProof() << endl;
286 // cout<<"set proof for theorem " << clauseThm << endl;
287  return clauseThm.getProof();
288  }
289  else{
290  CVC3::Proof leftProof = generateSatProof(node->getLeftParent(), cnfManager, thmProducer);
291  CVC3::Proof rightProof = generateSatProof(node->getRightParent(), cnfManager, thmProducer);
292 
293  if(node->getLeftParent() == node->getRightParent() ) cout<<"***error ********"<<endl;
294  vector<Proof> pfs;
295  pfs.push_back(leftProof);
296  pfs.push_back(rightProof);
297  // if(leftProof == rightProof) cout<<"***********"<<endl;
298 
299  Lit lit = node->getLit();
300  Expr e = cnfManager->concreteLit(lit);
301  Expr e_trans = cnfManager->concreteLit(lit,false);
302 // cout<<"set lit "<<lit.getVar()<<endl << e_trans <<endl << e << endl;
303 // cout<<"set lit "<<lit.getVar()<<endl << e_trans.getIndex() <<endl ;
304  if(e != e_trans){
305 // cout<<"-diff e "<<e<<endl<<flush;
306 // cout<<"-diff e_trans " <<e_trans <<endl <<flush;
307  }
308  // {
309  // cout<<"Lit "<<lit.getID() << " " ;
310  // if (lit.isNull()) cout << "NULL";
311  // else if (lit.isFalse()) cout << "F";
312  // else if (lit.isTrue()) cout << "T";
313  // else {
314  // if (!lit.isPositive()) cout << "-";
315  // cout << lit.getVar();
316  // }
317  // cout<<endl;
318  // }
319 
320  // cout<<"e "<<e<<endl<<flush;
321  Proof pf;
322  pf = thmProducer->newPf("bool_resolution", e_trans, pfs);
323  node->setNodeProof(pf);
324  return pf;
325 
326  }
327 
328 }
329 
331  if (node->isLeaf()){
332  CVC3::Theorem theorem = node->getLeaf();
333 
334  if(theorem.isNull()){
335  cout<<"theorem null"<<endl;
336  }
337  else{
338  cout<<"====================" << endl;
339  /*
340 //<<<<<<< dpllt_minisat.cpp
341  clause.print();
342  cout<<"--------------------" << endl;
343  */
344  /*
345  const CVC3::Theorem clauseThm = clause.getClauseTheorem();
346  cout<<"====================" << endl;
347  clause.print();
348 //=======
349  theorem.print();
350 //>>>>>>> 1.14
351  cout<<"--------------------" << endl;
352 //<<<<<<< dpllt_minisat.cpp
353  if(clauseThm.isNull()){
354  cout<<"leaf id " << clause.getId() << " # " << "NULL" << endl;
355  }
356  else{
357  cout<<"leaf id " << clause.getId() << " # " << clauseThm << endl;
358  }
359  */
360  /*
361 //=======
362 //>>>>>>> 1.14
363  */
364  }
365  }
366  else{
367  SAT::SatProofNode * leftNode = node->getLeftParent();
368  SAT::SatProofNode * rightNode = node->getRightParent();
369 
370  printSatProof(leftNode);
371  printSatProof(rightNode);
372  }
373 
374 }
375 
376 
377 
379  SAT::SatProof* proof = getProof();
380  SAT::SatProofNode * rootNode = proof->getRoot();
381 
382  // printSatProof(rootNode);
383 
384  CVC3::TheoremProducer* thmProducer = new TheoremProducer(core->getTM());
385 
386  return generateSatProof(rootNode, cnfManager, thmProducer);
387 }
388 
Data structure of expressions in CVC3.
Definition: expr.h:133
TheoremManager * getTM() const
Definition: theory_core.h:349
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
QueryResult
Definition: queryresult.h:32
std::vector< std::vector< SAT::Lit > > curClauses()
CVC3::QueryResult search()
bool inPush() const
TheoryAPI * d_theoryAPI
Definition: dpllt.h:104
void addFormula(const SAT::CNF_Formula &cnf, bool isTheoryClause)
Implementation of dpllt module based on minisat.
CVC3::Theorem getLeaf()
Definition: sat_proof.h:59
bool hasNodeProof()
Definition: sat_proof.h:63
STL namespace.
SatProofNode * getRoot()
Definition: sat_proof.h:108
virtual ~DPLLTMiniSat()
std::deque< Clause >::const_iterator const_iterator
Definition: cnf.h:123
bool isConsistent() const
#define DebugAssert(cond, str)
Definition: debug.h:408
Decider * d_decider
Definition: dpllt.h:105
const std::vector< Clause * > & getLemmas() const
virtual std::vector< std::vector< SAT::Lit > > getCurClauses()
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
int nVars() const
const SolverStats & getStats() const
Statistics.
Sat solver proof representation.
SatProof * getProof()
Definition: dpllt_minisat.h:99
CVC3::Proof getNodeProof()
Definition: sat_proof.h:64
void printSatProof(SAT::SatProofNode *node)
virtual void addAssertion(const CNF_Formula &cnf)
Add new clauses to the SAT solver.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
CVC3::Proof getSatProof(CNF_Manager *, CVC3::TheoryCore *)
Get the proof from SAT engine.
const lbool l_False
Val
Definition: cnf.h:37
Definition: cnf.h:51
virtual std::vector< SAT::Lit > getCurAssignments()
Var cvcToMiniSat(const SAT::Var &var)
Proof getProof() const
Definition: theorem.cpp:402
virtual CVC3::QueryResult checkSat(const CNF_Formula &cnf)
Check the satisfiability of a set of clauses in the current context.
bool isNull() const
Definition: theorem.h:164
virtual void push()
Set a checkpoint for backtracking.
std::vector< SAT::Lit > curAssigns()
virtual void pop()
Restore checkpoint.
SatProofNode * getLeftParent()
Definition: sat_proof.h:60
CVC3::QueryResult search()
search
SAT::Lit getLit()
Definition: sat_proof.h:62
virtual Var::Val getValue(Var v)
Get value of variable: unassigned, false, or true.
CVC3::Expr concreteLit(Lit l, bool checkTranslated=true)
Convert a CNF literal to an Expr literal.
Definition: cnf_manager.h:223
SatProofNode * getRightParent()
Definition: sat_proof.h:61
const lbool l_True
virtual const_iterator begin() const =0
Definition: cnf.h:32
virtual void push()=0
Set a checkpoint for backtracking.
SatProof * d_proof
Definition: dpllt_minisat.h:55
virtual CVC3::QueryResult continueCheck(const CNF_Formula &cnf)
Continue checking the last check with additional constraints.
void setNodeProof(CVC3::Proof pf)
Definition: sat_proof.h:65
Proof newPf(const std::string &name)
virtual const_iterator end() const =0
Definition: expr.cpp:35
static Solver * createFrom(const Solver *solver)
CVC3::Proof generateSatProof(SAT::SatProofNode *node, CNF_Manager *cnfManager, TheoremProducer *thmProducer)
virtual void pop()=0
Restore most recent checkpoint.
void push()
Push / Pop.
virtual void assertLit(Lit l)=0
Notify theory when a literal is set to true.
MiniSat::Solver * getActiveSolver()
Adaptation of MiniSat to DPLL(T)
std::stack< MiniSat::Solver * > d_solvers
Definition: dpllt_minisat.h:61
const std::vector< Clause * > & getClauses() const
Definition: cnf.h:34
lbool getValue(Var x) const
clauses / assignment