src/prop/prop_engine.cpp

   1 /*********************                                                        */
   2 /*! \file prop_engine.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: dejan
   6  ** Minor contributors (to current version): barrett, taking, cconway, kshitij
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Implementation of the propositional engine of CVC4
  15  **
  16  ** Implementation of the propositional engine of CVC4.
  17  **/
  18
  19 #include "prop/cnf_stream.h"
  20 #include "prop/prop_engine.h"
  21 #include "prop/theory_proxy.h"
  22 #include "prop/sat_solver.h"
  23 #include "prop/sat_solver_factory.h"
  24
  25 #include "decision/decision_engine.h"
  26 #include "theory/theory_engine.h"
  27 #include "theory/theory_registrar.h"
  28 #include "util/Assert.h"
  29 #include "util/options.h"
  30 #include "util/output.h"
  31 #include "util/result.h"
  32 #include "expr/expr.h"
  33 #include "expr/command.h"
  34
  35 #include <utility>
  36 #include <map>
  37 #include <iomanip>
  38
  39 using namespace std;
  40 using namespace CVC4::context;
  41
  42 namespace CVC4 {
  43 namespace prop {
  44
  45 /** Keeps a boolean flag scoped */
  46 class ScopedBool {
  47
  48 private:
  49
  50   bool d_original;
  51   bool& d_reference;
  52
  53 public:
  54
  55   ScopedBool(bool& reference) :
  56     d_reference(reference) {
  57     d_original = reference;
  58   }
  59
  60   ~ScopedBool() {
  61     d_reference = d_original;
  62   }
  63 };
  64
  65 PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) :
  66   d_inCheckSat(false),
  67   d_theoryEngine(te),
  68   d_decisionEngine(de),
  69   d_context(context),
  70   d_satSolver(NULL),
  71   d_cnfStream(NULL),
  72   d_satTimer(*this),
  73   d_interrupted(false) {
  74
  75   Debug("prop") << "Constructing the PropEngine" << endl;
  76
  77   d_satSolver = SatSolverFactory::createDPLLMinisat();
  78
  79   theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine);
  80   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1);
  81
  82   d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream));
  83
  84   d_decisionEngine->setSatSolver(d_satSolver);
  85   d_decisionEngine->setCnfStream(d_cnfStream);
  86 }
  87
  88 PropEngine::~PropEngine() {
  89   Debug("prop") << "Destructing the PropEngine" << endl;
  90   delete d_cnfStream;
  91   delete d_satSolver;
  92 }
  93
  94 void PropEngine::assertFormula(TNode node) {
  95   Assert(!d_inCheckSat, "Sat solver in solve()!");
  96   Debug("prop") << "assertFormula(" << node << ")" << endl;
  97   // Assert as non-removable
  98   d_cnfStream->convertAndAssert(node, false, false);
  99 }
 100
 101 void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
 102   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
 103   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 104
 105   if(!d_inCheckSat && Dump.isOn("learned")) {
 106     Dump("learned") << AssertCommand(BoolExpr(node.toExpr()));
 107   } else if(Dump.isOn("lemmas")) {
 108     Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr()));
 109   }
 110
 111   /* Tell decision engine */
 112   // if(negated) {
 113   //   NodeBuilder<> nb(kind::NOT);
 114   //   nb << node;
 115   //   d_decisionEngine->addAssertion(nb.constructNode());
 116   // } else {
 117   //   d_decisionEngine->addAssertion(node);
 118   // }
 119
 120   //TODO This comment is now false
 121   // Assert as removable
 122   d_cnfStream->convertAndAssert(node, removable, negated);
 123 }
 124
 125 void PropEngine::printSatisfyingAssignment(){
 126   const CnfStream::TranslationCache& transCache =
 127     d_cnfStream->getTranslationCache();
 128   Debug("prop-value") << "Literal | Value | Expr" << endl
 129                       << "----------------------------------------"
 130                       << "-----------------" << endl;
 131   for(CnfStream::TranslationCache::const_iterator i = transCache.begin(),
 132       end = transCache.end();
 133       i != end;
 134       ++i) {
 135     pair<Node, CnfStream::TranslationInfo> curr = *i;
 136     SatLiteral l = curr.second.literal;
 137     if(!l.isNegated()) {
 138       Node n = curr.first;
 139       SatValue value = d_satSolver->modelValue(l);
 140       Debug("prop-value") << "'" << l << "' " << value << " " << n << endl;
 141     }
 142   }
 143 }
 144
 145 Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
 146   Assert(!d_inCheckSat, "Sat solver in solve()!");
 147   Debug("prop") << "PropEngine::checkSat()" << endl;
 148
 149   // Mark that we are in the checkSat
 150   ScopedBool scopedBool(d_inCheckSat);
 151   d_inCheckSat = true;
 152
 153   // TODO This currently ignores conflicts (a dangerous practice).
 154   d_theoryEngine->presolve();
 155
 156   if(Options::current()->preprocessOnly) {
 157     millis = resource = 0;
 158     return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
 159   }
 160
 161   // Set the timer
 162   d_satTimer.set(millis);
 163
 164   // Reset the interrupted flag
 165   d_interrupted = false;
 166
 167   // Check the problem
 168   SatValue result = d_satSolver->solve(resource);
 169
 170   millis = d_satTimer.elapsed();
 171
 172   if( result == SAT_VALUE_UNKNOWN ) {
 173     Result::UnknownExplanation why =
 174       d_satTimer.expired() ? Result::TIMEOUT :
 175         (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
 176     return Result(Result::SAT_UNKNOWN, why);
 177   }
 178
 179   if( result == SAT_VALUE_TRUE && Debug.isOn("prop") ) {
 180     printSatisfyingAssignment();
 181   }
 182
 183   Debug("prop") << "PropEngine::checkSat() => " << result << endl;
 184   if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) {
 185     return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
 186   }
 187   return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
 188 }
 189
 190 Node PropEngine::getValue(TNode node) const {
 191   Assert(node.getType().isBoolean());
 192   Assert(d_cnfStream->hasLiteral(node));
 193
 194   SatLiteral lit = d_cnfStream->getLiteral(node);
 195
 196   SatValue v = d_satSolver->value(lit);
 197   if(v == SAT_VALUE_TRUE) {
 198     return NodeManager::currentNM()->mkConst(true);
 199   } else if(v == SAT_VALUE_FALSE) {
 200     return NodeManager::currentNM()->mkConst(false);
 201   } else {
 202     Assert(v == SAT_VALUE_UNKNOWN);
 203     return Node::null();
 204   }
 205 }
 206
 207 bool PropEngine::isSatLiteral(TNode node) const {
 208   return d_cnfStream->hasLiteral(node);
 209 }
 210
 211 bool PropEngine::isTranslatedSatLiteral(TNode node) const {
 212   return d_cnfStream->isTranslated(node);
 213 }
 214
 215 bool PropEngine::hasValue(TNode node, bool& value) const {
 216   Assert(node.getType().isBoolean());
 217   Assert(d_cnfStream->hasLiteral(node));
 218
 219   SatLiteral lit = d_cnfStream->getLiteral(node);
 220
 221   SatValue v = d_satSolver->value(lit);
 222   if(v == SAT_VALUE_TRUE) {
 223     value = true;
 224     return true;
 225   } else if(v == SAT_VALUE_FALSE) {
 226     value = false;
 227     return true;
 228   } else {
 229     Assert(v == SAT_VALUE_UNKNOWN);
 230     return false;
 231   }
 232 }
 233
 234 void PropEngine::ensureLiteral(TNode n) {
 235   d_cnfStream->ensureLiteral(n);
 236 }
 237
 238 void PropEngine::push() {
 239   Assert(!d_inCheckSat, "Sat solver in solve()!");
 240   d_satSolver->push();
 241   Debug("prop") << "push()" << endl;
 242 }
 243
 244 void PropEngine::pop() {
 245   Assert(!d_inCheckSat, "Sat solver in solve()!");
 246   d_satSolver->pop();
 247   Debug("prop") << "pop()" << endl;
 248 }
 249
 250 bool PropEngine::isRunning() const {
 251   return d_inCheckSat;
 252 }
 253
 254 void PropEngine::interrupt() throw(ModalException) {
 255   if(! d_inCheckSat) {
 256     throw ModalException("SAT solver is not currently solving anything; "
 257                          "cannot interrupt it");
 258   }
 259
 260   d_interrupted = true;
 261   d_satSolver->interrupt();
 262   Debug("prop") << "interrupt()" << endl;
 263 }
 264
 265 void PropEngine::spendResource() throw() {
 266   // TODO implement me
 267 }
 268
 269 bool PropEngine::properExplanation(TNode node, TNode expl) const {
 270   if(! d_cnfStream->hasLiteral(node)) {
 271     Trace("properExplanation") << "properExplanation(): Failing because node "
 272                                << "being explained doesn't have a SAT literal ?!" << std::endl
 273                                << "properExplanation(): The node is: " << node << std::endl;
 274     return false;
 275   }
 276
 277   SatLiteral nodeLit = d_cnfStream->getLiteral(node);
 278
 279   for(TNode::kinded_iterator i = expl.begin(kind::AND),
 280         i_end = expl.end(kind::AND);
 281       i != i_end;
 282       ++i) {
 283     if(! d_cnfStream->hasLiteral(*i)) {
 284       Trace("properExplanation") << "properExplanation(): Failing because one of explanation "
 285                                  << "nodes doesn't have a SAT literal" << std::endl
 286                                  << "properExplanation(): The explanation node is: " << *i << std::endl;
 287       return false;
 288     }
 289
 290     SatLiteral iLit = d_cnfStream->getLiteral(*i);
 291
 292     if(iLit == nodeLit) {
 293       Trace("properExplanation") << "properExplanation(): Failing because the node" << std::endl
 294                                  << "properExplanation(): " << node << std::endl
 295                                  << "properExplanation(): cannot be made to explain itself!" << std::endl;
 296       return false;
 297     }
 298
 299     if(! d_satSolver->properExplanation(nodeLit, iLit)) {
 300       Trace("properExplanation") << "properExplanation(): SAT solver told us that node" << std::endl
 301                                  << "properExplanation(): " << *i << std::endl
 302                                  << "properExplanation(): is not part of a proper explanation node for" << std::endl
 303                                  << "properExplanation(): " << node << std::endl
 304                                  << "properExplanation(): Perhaps it one of the two isn't assigned or the explanation" << std::endl
 305                                  << "properExplanation(): node wasn't propagated before the node being explained" << std::endl;
 306       return false;
 307     }
 308   }
 309
 310   return true;
 311 }
 312
 313 }/* CVC4::prop namespace */
 314 }/* CVC4 namespace */