src/smt/smt_engine.cpp

   1 /*********************                                                        */
   2 /*! \file smt_engine.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: dejan
   6  ** Minor contributors (to current version): 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 The main entry point into the CVC4 library's SMT interface
  15  **
  16  ** The main entry point into the CVC4 library's SMT interface.
  17  **/
  18
  19 #include <vector>
  20 #include <string>
  21 #include <iterator>
  22 #include <utility>
  23 #include <sstream>
  24 #include <stack>
  25 #include <ext/hash_map>
  26
  27 #include "context/cdlist.h"
  28 #include "context/cdhashset.h"
  29 #include "context/context.h"
  30 #include "decision/decision_engine.h"
  31 #include "expr/command.h"
  32 #include "expr/expr.h"
  33 #include "expr/kind.h"
  34 #include "expr/metakind.h"
  35 #include "expr/node_builder.h"
  36 #include "prop/prop_engine.h"
  37 #include "smt/bad_option_exception.h"
  38 #include "smt/modal_exception.h"
  39 #include "smt/no_such_function_exception.h"
  40 #include "smt/smt_engine.h"
  41 #include "theory/theory_engine.h"
  42 #include "proof/proof_manager.h"
  43 #include "util/proof.h"
  44 #include "util/boolean_simplification.h"
  45 #include "util/configuration.h"
  46 #include "util/exception.h"
  47 #include "util/options.h"
  48 #include "util/output.h"
  49 #include "util/hash.h"
  50 #include "theory/substitutions.h"
  51 #include "theory/builtin/theory_builtin.h"
  52 #include "theory/booleans/theory_bool.h"
  53 #include "theory/booleans/circuit_propagator.h"
  54 #include "theory/uf/theory_uf.h"
  55 #include "theory/arith/theory_arith.h"
  56 #include "theory/arrays/theory_arrays.h"
  57 #include "theory/bv/theory_bv.h"
  58 #include "theory/datatypes/theory_datatypes.h"
  59 #include "theory/theory_traits.h"
  60 #include "theory/logic_info.h"
  61 #include "util/ite_removal.h"
  62
  63 using namespace std;
  64 using namespace CVC4;
  65 using namespace CVC4::smt;
  66 using namespace CVC4::prop;
  67 using namespace CVC4::context;
  68 using namespace CVC4::theory;
  69
  70 namespace CVC4 {
  71
  72 namespace smt {
  73
  74 /**
  75  * Representation of a defined function.  We keep these around in
  76  * SmtEngine to permit expanding definitions late (and lazily), to
  77  * support getValue() over defined functions, to support user output
  78  * in terms of defined functions, etc.
  79  */
  80 class DefinedFunction {
  81   Node d_func;
  82   vector<Node> d_formals;
  83   Node d_formula;
  84 public:
  85   DefinedFunction() {}
  86   DefinedFunction(Node func, vector<Node> formals, Node formula) :
  87     d_func(func),
  88     d_formals(formals),
  89     d_formula(formula) {
  90   }
  91   Node getFunction() const { return d_func; }
  92   vector<Node> getFormals() const { return d_formals; }
  93   Node getFormula() const { return d_formula; }
  94 };/* class DefinedFunction */
  95
  96 /**
  97  * This is an inelegant solution, but for the present, it will work.
  98  * The point of this is to separate the public and private portions of
  99  * the SmtEngine class, so that smt_engine.h doesn't
 100  * include "expr/node.h", which is a private CVC4 header (and can lead
 101  * to linking errors due to the improper inlining of non-visible symbols
 102  * into user code!).
 103  *
 104  * The "real" solution (that which is usually implemented) is to move
 105  * ALL the implementation to SmtEnginePrivate and maintain a
 106  * heap-allocated instance of it in SmtEngine.  SmtEngine (the public
 107  * one) becomes an "interface shell" which simply acts as a forwarder
 108  * of method calls.
 109  */
 110 class SmtEnginePrivate {
 111   SmtEngine& d_smt;
 112
 113   /** The assertions yet to be preprocessed */
 114   vector<Node> d_assertionsToPreprocess;
 115
 116   /** Learned literals */
 117   vector<Node> d_nonClausalLearnedLiterals;
 118
 119   /** A circuit propagator for non-clausal propositional deduction */
 120   booleans::CircuitPropagator d_propagator;
 121
 122   /** Assertions to push to sat */
 123   vector<Node> d_assertionsToCheck;
 124
 125   /** Map from skolem variables to index in d_assertionsToCheck containing
 126    * corresponding introduced Boolean ite */
 127   IteSkolemMap d_iteSkolemMap;
 128
 129   /** The top level substitutions */
 130   theory::SubstitutionMap d_topLevelSubstitutions;
 131
 132   /**
 133    * The last substitution that the SAT layer was told about.
 134    * In incremental settings, substitutions cannot be performed
 135    * "backward," only forward.  So SAT needs to be told of all
 136    * substitutions that are going to be done.  This iterator
 137    * holds the last substitution from d_topLevelSubstitutions
 138    * that was pushed out to SAT.
 139    * If d_lastSubstitutionPos == d_topLevelSubstitutions.end(),
 140    * then nothing has been pushed out yet. */
 141   context::CDO<theory::SubstitutionMap::iterator> d_lastSubstitutionPos;
 142
 143   /**
 144    * Runs the nonclausal solver and tries to solve all the assigned
 145    * theory literals.
 146    */
 147   void nonClausalSimplify();
 148
 149   /**
 150    * Performs static learning on the assertions.
 151    */
 152   void staticLearning();
 153
 154   /**
 155    * Remove ITEs from the assertions.
 156    */
 157   void removeITEs();
 158
 159   // Simplify ITE structure
 160   void simpITE();
 161
 162   // Simplify based on unconstrained values
 163   void unconstrainedSimp();
 164
 165   /**
 166    * Any variable in a assertion that is declared as a subtype type
 167    * (predicate subtype or integer subrange type) must be constrained
 168    * to be in that type.
 169    */
 170   void constrainSubtypes(TNode n, std::vector<Node>& assertions)
 171     throw(AssertionException);
 172
 173   /**
 174    * Perform non-clausal simplification of a Node.  This involves
 175    * Theory implementations, but does NOT involve the SAT solver in
 176    * any way.
 177    */
 178   void simplifyAssertions() throw(NoSuchFunctionException, AssertionException);
 179
 180 public:
 181
 182   SmtEnginePrivate(SmtEngine& smt) :
 183     d_smt(smt),
 184     d_nonClausalLearnedLiterals(),
 185     d_propagator(smt.d_userContext, d_nonClausalLearnedLiterals, true, true),
 186     d_topLevelSubstitutions(smt.d_userContext),
 187     d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) {
 188   }
 189
 190   Node applySubstitutions(TNode node) const {
 191     return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
 192   }
 193
 194   /**
 195    * Process the assertions that have been asserted.
 196    */
 197   void processAssertions();
 198
 199   /**
 200    * Process a user pop.  Clears out the non-context-dependent stuff in this
 201    * SmtEnginePrivate.  Necessary to clear out our assertion vectors in case
 202    * someone does a push-assert-pop without a check-sat.
 203    */
 204   void notifyPop() {
 205     d_assertionsToPreprocess.clear();
 206     d_nonClausalLearnedLiterals.clear();
 207     d_assertionsToCheck.clear();
 208   }
 209
 210   /**
 211    * Adds a formula to the current context.  Action here depends on
 212    * the SimplificationMode (in the current Options scope); the
 213    * formula might be pushed out to the propositional layer
 214    * immediately, or it might be simplified and kept, or it might not
 215    * even be simplified.
 216    */
 217   void addFormula(TNode n)
 218     throw(NoSuchFunctionException, AssertionException);
 219
 220   /**
 221    * Expand definitions in n.
 222    */
 223   Node expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache)
 224     throw(NoSuchFunctionException, AssertionException);
 225
 226 };/* class SmtEnginePrivate */
 227
 228 }/* namespace CVC4::smt */
 229
 230 using namespace CVC4::smt;
 231
 232 SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 233   d_context(em->getContext()),
 234   d_userLevels(),
 235   d_userContext(new UserContext()),
 236   d_exprManager(em),
 237   d_nodeManager(d_exprManager->getNodeManager()),
 238   d_decisionEngine(NULL),
 239   d_theoryEngine(NULL),
 240   d_propEngine(NULL),
 241   d_definedFunctions(NULL),
 242   d_assertionList(NULL),
 243   d_assignments(NULL),
 244   d_logic(),
 245   d_logicIsSet(false),
 246   d_problemExtended(false),
 247   d_queryMade(false),
 248   d_needPostsolve(false),
 249   d_timeBudgetCumulative(0),
 250   d_timeBudgetPerCall(0),
 251   d_resourceBudgetCumulative(0),
 252   d_resourceBudgetPerCall(0),
 253   d_cumulativeTimeUsed(0),
 254   d_cumulativeResourceUsed(0),
 255   d_status(),
 256   d_private(new smt::SmtEnginePrivate(*this)),
 257   d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
 258   d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
 259   d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
 260   d_simpITETime("smt::SmtEngine::simpITETime"),
 261   d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
 262   d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
 263   d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
 264   d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
 265   d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
 266   d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
 267   d_statResultSource("smt::resultSource", "unknown") {
 268
 269   NodeManagerScope nms(d_nodeManager);
 270
 271   StatisticsRegistry::registerStat(&d_definitionExpansionTime);
 272   StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
 273   StatisticsRegistry::registerStat(&d_staticLearningTime);
 274   StatisticsRegistry::registerStat(&d_simpITETime);
 275   StatisticsRegistry::registerStat(&d_unconstrainedSimpTime);
 276   StatisticsRegistry::registerStat(&d_iteRemovalTime);
 277   StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
 278   StatisticsRegistry::registerStat(&d_cnfConversionTime);
 279   StatisticsRegistry::registerStat(&d_numAssertionsPre);
 280   StatisticsRegistry::registerStat(&d_numAssertionsPost);
 281   StatisticsRegistry::registerStat(&d_statResultSource);
 282
 283   // We have mutual dependency here, so we add the prop engine to the theory
 284   // engine later (it is non-essential there)
 285   d_theoryEngine = new TheoryEngine(d_context, d_userContext, const_cast<const LogicInfo&>(d_logic));
 286
 287   // Add the theories
 288 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 289 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 290 #endif
 291 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 292     d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
 293   CVC4_FOR_EACH_THEORY;
 294
 295   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
 296   d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
 297   d_theoryEngine->setPropEngine(d_propEngine);
 298   d_theoryEngine->setDecisionEngine(d_decisionEngine);
 299   // d_decisionEngine->setPropEngine(d_propEngine);
 300
 301   // global push/pop around everything, to ensure proper destruction
 302   // of context-dependent data structures
 303   d_userContext->push();
 304   d_context->push();
 305
 306   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 307
 308   // [MGD 10/20/2011] keep around in incremental mode, due to a
 309   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
 310   // first, some user-context-dependent TNodes might still exist
 311   // with rc == 0.
 312   if(Options::current()->interactive ||
 313      Options::current()->incrementalSolving) {
 314     // In the case of incremental solving, we appear to need these to
 315     // ensure the relevant Nodes remain live.
 316     d_assertionList = new(true) AssertionList(d_userContext);
 317   }
 318
 319   if(Options::current()->perCallResourceLimit != 0) {
 320     setResourceLimit(Options::current()->perCallResourceLimit, false);
 321   }
 322   if(Options::current()->cumulativeResourceLimit != 0) {
 323     setResourceLimit(Options::current()->cumulativeResourceLimit, true);
 324   }
 325   if(Options::current()->perCallMillisecondLimit != 0) {
 326     setTimeLimit(Options::current()->perCallMillisecondLimit, false);
 327   }
 328   if(Options::current()->cumulativeMillisecondLimit != 0) {
 329     setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
 330   }
 331
 332   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
 333   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
 334 }
 335
 336 void SmtEngine::shutdown() {
 337   if(Dump.isOn("benchmark")) {
 338     Dump("benchmark") << QuitCommand();
 339   }
 340
 341   // check to see if a postsolve() is pending
 342   if(d_needPostsolve) {
 343     d_theoryEngine->postsolve();
 344     d_needPostsolve = false;
 345   }
 346
 347   d_propEngine->shutdown();
 348   d_theoryEngine->shutdown();
 349   d_decisionEngine->shutdown();
 350 }
 351
 352 SmtEngine::~SmtEngine() throw() {
 353   NodeManagerScope nms(d_nodeManager);
 354
 355   try {
 356     while(Options::current()->incrementalSolving && d_userContext->getLevel() > 1) {
 357       internalPop();
 358     }
 359
 360     shutdown();
 361
 362     // global push/pop around everything, to ensure proper destruction
 363     // of context-dependent data structures
 364     d_context->pop();
 365     d_userContext->pop();
 366
 367     if(d_assignments != NULL) {
 368       d_assignments->deleteSelf();
 369     }
 370
 371     if(d_assertionList != NULL) {
 372       d_assertionList->deleteSelf();
 373     }
 374
 375     d_definedFunctions->deleteSelf();
 376
 377     StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
 378     StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
 379     StatisticsRegistry::unregisterStat(&d_staticLearningTime);
 380     StatisticsRegistry::unregisterStat(&d_simpITETime);
 381     StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime);
 382     StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
 383     StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
 384     StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
 385     StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
 386     StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
 387     StatisticsRegistry::unregisterStat(&d_statResultSource);
 388
 389     delete d_private;
 390     delete d_userContext;
 391
 392     delete d_theoryEngine;
 393     delete d_propEngine;
 394     //delete d_decisionEngine;
 395   } catch(Exception& e) {
 396     Warning() << "CVC4 threw an exception during cleanup." << endl
 397               << e << endl;
 398   }
 399 }
 400
 401 void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
 402   NodeManagerScope nms(d_nodeManager);
 403
 404   if(d_logicIsSet) {
 405     throw ModalException("logic already set");
 406   }
 407
 408   if(Dump.isOn("benchmark")) {
 409     Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
 410   }
 411
 412   setLogicInternal(logic);
 413 }
 414
 415 void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
 416   NodeManagerScope nms(d_nodeManager);
 417
 418   setLogic(LogicInfo(s));
 419 }
 420
 421 void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
 422   d_logic = logic;
 423
 424   // by default, symmetry breaker is on only for QF_UF
 425   if(! Options::current()->ufSymmetryBreakerSetByUser) {
 426     bool qf_uf = logic.isPure(theory::THEORY_UF) && !logic.isQuantified();
 427     Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
 428     NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf;
 429   }
 430   // by default, nonclausal simplification is off for QF_SAT
 431   if(! Options::current()->simplificationModeSetByUser) {
 432     bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
 433     Trace("smt") << "setting simplification mode to <" << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
 434     NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
 435   }
 436
 437   // If in arrays, set the UF handler to arrays
 438   if(logic.isPure(theory::THEORY_ARRAY) && !logic.isQuantified()) {
 439     theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
 440   } else {
 441     theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
 442   }
 443   // Turn on ite simplification for QF_LIA and QF_AUFBV
 444   if(! Options::current()->doITESimpSetByUser) {
 445     bool iteSimp = !logic.isQuantified() &&
 446       ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() &&  !logic.areRealsUsed()) ||
 447        (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV)));
 448     Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
 449     NodeManager::currentNM()->getOptions()->doITESimp = iteSimp;
 450   }
 451   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
 452   if(! Options::current()->repeatSimpSetByUser) {
 453     bool repeatSimp = !logic.isQuantified() &&
 454       (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV));
 455     Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
 456     NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
 457   }
 458   // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode
 459   if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) {
 460     bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
 461     bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
 462     Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
 463     NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp;
 464   }
 465   // Turn on arith rewrite equalities only for pure arithmetic
 466   if(! Options::current()->arithRewriteEqSetByUser) {
 467     bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified();
 468     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
 469     NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq;
 470   }
 471
 472 }
 473
 474 void SmtEngine::setInfo(const std::string& key, const SExpr& value)
 475   throw(BadOptionException, ModalException) {
 476   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
 477   if(Dump.isOn("benchmark")) {
 478     if(key == ":status") {
 479       std::string s = value.getValue();
 480       BenchmarkStatus status =
 481         (s == "sat") ? SMT_SATISFIABLE :
 482           ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN);
 483       Dump("benchmark") << SetBenchmarkStatusCommand(status);
 484     } else {
 485       Dump("benchmark") << SetInfoCommand(key, value);
 486     }
 487   }
 488
 489   // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
 490   if(key.length() > 6) {
 491     string prefix = key.substr(0, 6);
 492     if(prefix == ":cvc4-" || prefix == ":cvc4_") {
 493       string cvc4key = key.substr(6);
 494       if(cvc4key == "logic") {
 495         if(! value.isAtom()) {
 496           throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
 497         }
 498         NodeManagerScope nms(d_nodeManager);
 499         setLogicInternal(value.getValue());
 500         return;
 501       }
 502     }
 503   }
 504
 505   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
 506   if(key == ":name" ||
 507      key == ":source" ||
 508      key == ":category" ||
 509      key == ":difficulty" ||
 510      key == ":smt-lib-version" ||
 511      key == ":notes") {
 512     // ignore these
 513     return;
 514   } else if(key == ":status") {
 515     string s;
 516     if(value.isAtom()) {
 517       s = value.getValue();
 518     }
 519     if(s != "sat" && s != "unsat" && s != "unknown") {
 520       throw BadOptionException("argument to (set-info :status ..) must be "
 521                                "`sat' or `unsat' or `unknown'");
 522     }
 523     d_status = Result(s);
 524     return;
 525   }
 526   throw BadOptionException();
 527 }
 528
 529 SExpr SmtEngine::getInfo(const std::string& key) const
 530   throw(BadOptionException) {
 531   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
 532   if(key == ":all-statistics") {
 533     vector<SExpr> stats;
 534     for(StatisticsRegistry::const_iterator i = StatisticsRegistry::begin();
 535         i != StatisticsRegistry::end();
 536         ++i) {
 537       vector<SExpr> v;
 538       v.push_back((*i)->getName());
 539       v.push_back((*i)->getValue());
 540       stats.push_back(v);
 541     }
 542     return stats;
 543   } else if(key == ":error-behavior") {
 544     return SExpr("immediate-exit");
 545   } else if(key == ":name") {
 546     return Configuration::getName();
 547   } else if(key == ":version") {
 548     return Configuration::getVersionString();
 549   } else if(key == ":authors") {
 550     return Configuration::about();
 551   } else if(key == ":status") {
 552     return d_status.asSatisfiabilityResult().toString();
 553   } else if(key == ":reason-unknown") {
 554     if(d_status.isUnknown()) {
 555       stringstream ss;
 556       ss << d_status.whyUnknown();
 557       return ss.str();
 558     } else {
 559       throw ModalException("Can't get-info :reason-unknown when the "
 560                            "last result wasn't unknown!");
 561     }
 562   } else {
 563     throw BadOptionException();
 564   }
 565 }
 566
 567 void SmtEngine::setOption(const std::string& key, const SExpr& value)
 568   throw(BadOptionException, ModalException) {
 569   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 570   if(Dump.isOn("benchmark")) {
 571     Dump("benchmark") << SetOptionCommand(key, value);
 572   }
 573
 574   if(key == ":print-success") {
 575     if(value.isAtom() && value.getValue() == "false") {
 576       // fine; don't need to do anything
 577     } else {
 578       throw BadOptionException();
 579     }
 580   } else if(key == ":expand-definitions") {
 581     throw BadOptionException();
 582   } else if(key == ":interactive-mode") {
 583     throw BadOptionException();
 584   } else if(key == ":regular-output-channel") {
 585     throw BadOptionException();
 586   } else if(key == ":diagnostic-output-channel") {
 587     throw BadOptionException();
 588   } else if(key == ":random-seed") {
 589     throw BadOptionException();
 590   } else if(key == ":verbosity") {
 591     throw BadOptionException();
 592   } else {
 593     // The following options can only be set at the beginning; we throw
 594     // a ModalException if someone tries.
 595     if(d_logicIsSet) {
 596       throw ModalException("logic already set; cannot set options");
 597     }
 598
 599     if(key == ":produce-proofs") {
 600       throw BadOptionException();
 601     } else if(key == ":produce-unsat-cores") {
 602       throw BadOptionException();
 603     } else if(key == ":produce-models") {
 604       throw BadOptionException();
 605     } else if(key == ":produce-assignments") {
 606       throw BadOptionException();
 607     } else {
 608       throw BadOptionException();
 609     }
 610   }
 611 }
 612
 613 SExpr SmtEngine::getOption(const std::string& key) const
 614   throw(BadOptionException) {
 615   Trace("smt") << "SMT getOption(" << key << ")" << endl;
 616   if(Dump.isOn("benchmark")) {
 617     Dump("benchmark") << GetOptionCommand(key);
 618   }
 619   if(key == ":print-success") {
 620     return SExpr("true");
 621   } else if(key == ":expand-definitions") {
 622     throw BadOptionException();
 623   } else if(key == ":interactive-mode") {
 624     throw BadOptionException();
 625   } else if(key == ":produce-proofs") {
 626     throw BadOptionException();
 627   } else if(key == ":produce-unsat-cores") {
 628     throw BadOptionException();
 629   } else if(key == ":produce-models") {
 630     throw BadOptionException();
 631   } else if(key == ":produce-assignments") {
 632     throw BadOptionException();
 633   } else if(key == ":regular-output-channel") {
 634     return SExpr("stdout");
 635   } else if(key == ":diagnostic-output-channel") {
 636     return SExpr("stderr");
 637   } else if(key == ":random-seed") {
 638     throw BadOptionException();
 639   } else if(key == ":verbosity") {
 640     throw BadOptionException();
 641   } else {
 642     throw BadOptionException();
 643   }
 644 }
 645
 646 void SmtEngine::defineFunction(Expr func,
 647                                const std::vector<Expr>& formals,
 648                                Expr formula) {
 649   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
 650   if(Dump.isOn("declarations")) {
 651     stringstream ss;
 652     ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream()))
 653        << func;
 654     Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula);
 655   }
 656   NodeManagerScope nms(d_nodeManager);
 657
 658   // type check body
 659   Type formulaType = formula.getType(Options::current()->typeChecking);
 660
 661   Type funcType = func.getType();
 662   Type rangeType = funcType.isFunction() ?
 663     FunctionType(funcType).getRangeType() : funcType;
 664   if(formulaType != rangeType) {
 665     stringstream ss;
 666     ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
 667        << "Defined function's declared type does not match that of body\n"
 668        << "The function  : " << func << "\n"
 669        << "Its range type: " << rangeType << "\n"
 670        << "The body      : " << formula << "\n"
 671        << "Body type     : " << formulaType;
 672     throw TypeCheckingException(func, ss.str());
 673   }
 674   TNode funcNode = func.getTNode();
 675   vector<Node> formalsNodes;
 676   for(vector<Expr>::const_iterator i = formals.begin(),
 677         iend = formals.end();
 678       i != iend;
 679       ++i) {
 680     formalsNodes.push_back((*i).getNode());
 681   }
 682   TNode formulaNode = formula.getTNode();
 683   DefinedFunction def(funcNode, formalsNodes, formulaNode);
 684   // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
 685   // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
 686   // d_haveAdditions = true;
 687   d_definedFunctions->insert(funcNode, def);
 688 }
 689
 690 Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache)
 691   throw(NoSuchFunctionException, AssertionException) {
 692
 693   if(n.getKind() != kind::APPLY && n.getNumChildren() == 0) {
 694     // don't bother putting in the cache
 695     return n;
 696   }
 697
 698   // maybe it's in the cache
 699   hash_map<TNode, Node, TNodeHashFunction>::iterator cacheHit = cache.find(n);
 700   if(cacheHit != cache.end()) {
 701     TNode ret = (*cacheHit).second;
 702     return ret.isNull() ? n : ret;
 703   }
 704
 705   // otherwise expand it
 706   if(n.getKind() == kind::APPLY) {
 707     TNode func = n.getOperator();
 708     SmtEngine::DefinedFunctionMap::const_iterator i =
 709       d_smt.d_definedFunctions->find(func);
 710     DefinedFunction def = (*i).second;
 711     vector<Node> formals = def.getFormals();
 712
 713     if(Debug.isOn("expand")) {
 714       Debug("expand") << "found: " << n << endl;
 715       Debug("expand") << " func: " << func << endl;
 716       string name = func.getAttribute(expr::VarNameAttr());
 717       Debug("expand") << "     : \"" << name << "\"" << endl;
 718     }
 719     if(i == d_smt.d_definedFunctions->end()) {
 720       throw NoSuchFunctionException(Expr(d_smt.d_exprManager, new Node(func)));
 721     }
 722     if(Debug.isOn("expand")) {
 723       Debug("expand") << " defn: " << def.getFunction() << endl
 724                       << "       [";
 725       if(formals.size() > 0) {
 726         copy( formals.begin(), formals.end() - 1,
 727               ostream_iterator<Node>(Debug("expand"), ", ") );
 728         Debug("expand") << formals.back();
 729       }
 730       Debug("expand") << "]" << endl
 731                       << "       " << def.getFunction().getType() << endl
 732                       << "       " << def.getFormula() << endl;
 733     }
 734
 735     TNode fm = def.getFormula();
 736     Node instance = fm.substitute(formals.begin(), formals.end(),
 737                                   n.begin(), n.end());
 738     Debug("expand") << "made : " << instance << endl;
 739
 740     Node expanded = expandDefinitions(instance, cache);
 741     cache[n] = (n == expanded ? Node::null() : expanded);
 742     return expanded;
 743   } else {
 744     Debug("expand") << "cons : " << n << endl;
 745     NodeBuilder<> nb(n.getKind());
 746     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
 747       Debug("expand") << "op   : " << n.getOperator() << endl;
 748       nb << n.getOperator();
 749     }
 750     for(TNode::iterator i = n.begin(),
 751           iend = n.end();
 752         i != iend;
 753         ++i) {
 754       Node expanded = expandDefinitions(*i, cache);
 755       Debug("expand") << "exchld: " << expanded << endl;
 756       nb << expanded;
 757     }
 758     Node node = nb;
 759     cache[n] = n == node ? Node::null() : node;
 760     return node;
 761   }
 762 }
 763
 764
 765 void SmtEnginePrivate::removeITEs() {
 766   Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
 767
 768   // Remove all of the ITE occurrences and normalize
 769   RemoveITE::run(d_assertionsToCheck, d_iteSkolemMap);
 770   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
 771     d_assertionsToCheck[i] = theory::Rewriter::rewrite(d_assertionsToCheck[i]);
 772   }
 773
 774 }
 775
 776 void SmtEnginePrivate::staticLearning() {
 777
 778   TimerStat::CodeTimer staticLearningTimer(d_smt.d_staticLearningTime);
 779
 780   Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl;
 781
 782   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
 783
 784     NodeBuilder<> learned(kind::AND);
 785     learned << d_assertionsToCheck[i];
 786     d_smt.d_theoryEngine->ppStaticLearn(d_assertionsToCheck[i], learned);
 787     if(learned.getNumChildren() == 1) {
 788       learned.clear();
 789     } else {
 790       d_assertionsToCheck[i] = learned;
 791     }
 792   }
 793 }
 794
 795 void SmtEnginePrivate::nonClausalSimplify() {
 796
 797   TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime);
 798
 799   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
 800
 801   // Apply the substitutions we already have, and normalize
 802   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 803                     << "applying substitutions" << endl;
 804   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
 805     Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl;
 806     d_assertionsToPreprocess[i] =
 807       theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
 808     Trace("simplify") << "  got " << d_assertionsToPreprocess[i] << endl;
 809   }
 810
 811   // Assert all the assertions to the propagator
 812   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 813                     << "asserting to propagator" << endl;
 814   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
 815     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl;
 816     d_propagator.assert(d_assertionsToPreprocess[i]);
 817   }
 818
 819   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 820                     << "propagating" << endl;
 821   if (d_propagator.propagate()) {
 822     // If in conflict, just return false
 823     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 824                       << "conflict in non-clausal propagation" << endl;
 825     d_assertionsToPreprocess.clear();
 826     d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
 827     return;
 828   } else {
 829     // No, conflict, go through the literals and solve them
 830     unsigned j = 0;
 831     for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals.size(); i < i_end; ++ i) {
 832       // Simplify the literal we learned wrt previous substitutions
 833       Node learnedLiteral =
 834         theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i]));
 835       // It might just simplify to a constant
 836       if (learnedLiteral.isConst()) {
 837         if (learnedLiteral.getConst<bool>()) {
 838           // If the learned literal simplifies to true, it's redundant
 839           continue;
 840         } else {
 841           // If the learned literal simplifies to false, we're in conflict
 842           Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 843                             << "conflict with "
 844                             << d_nonClausalLearnedLiterals[i] << endl;
 845           d_assertionsToPreprocess.clear();
 846           d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
 847           return;
 848         }
 849       }
 850       // Solve it with the corresponding theory
 851       Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 852                         << "solving " << learnedLiteral << endl;
 853       Theory::PPAssertStatus solveStatus =
 854         d_smt.d_theoryEngine->solve(learnedLiteral, d_topLevelSubstitutions);
 855
 856       switch (solveStatus) {
 857       case Theory::PP_ASSERT_STATUS_CONFLICT:
 858         // If in conflict, we return false
 859         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 860                           << "conflict while solving "
 861                           << learnedLiteral << endl;
 862         d_assertionsToPreprocess.clear();
 863         d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
 864         return;
 865       case Theory::PP_ASSERT_STATUS_SOLVED:
 866         // The literal should rewrite to true
 867         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 868                           << "solved " << learnedLiteral << endl;
 869         Assert(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(learnedLiteral)).isConst());
 870         break;
 871       default:
 872         // Keep the literal
 873         d_nonClausalLearnedLiterals[j++] = d_nonClausalLearnedLiterals[i];
 874         break;
 875       }
 876
 877       if( Options::current()->incrementalSolving ||
 878           Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL ) {
 879         // Tell PropEngine about new substitutions
 880         SubstitutionMap::iterator pos = d_lastSubstitutionPos;
 881         if(pos == d_topLevelSubstitutions.end()) {
 882            pos = d_topLevelSubstitutions.begin();
 883         } else {
 884           ++pos;
 885         }
 886
 887         while(pos != d_topLevelSubstitutions.end()) {
 888           // Push out this substitution
 889           TNode lhs = (*pos).first, rhs = (*pos).second;
 890           Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs);
 891           d_assertionsToCheck.push_back(n);
 892           Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
 893           d_lastSubstitutionPos = pos;
 894           ++pos;
 895         }
 896       }
 897     }
 898     // Resize the learnt
 899     d_nonClausalLearnedLiterals.resize(j);
 900   }
 901
 902   hash_set<TNode, TNodeHashFunction> s;
 903   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
 904     Node assertion = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
 905     s.insert(assertion);
 906     d_assertionsToCheck.push_back(assertion);
 907     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 908                       << "non-clausal preprocessed: "
 909                       << assertion << endl;
 910   }
 911   d_assertionsToPreprocess.clear();
 912
 913   for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
 914     Node learned = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i]));
 915     if (s.find(learned) != s.end()) {
 916       continue;
 917     }
 918     s.insert(learned);
 919     d_assertionsToCheck.push_back(learned);
 920     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
 921                       << "non-clausal learned : "
 922                       << d_assertionsToCheck.back() << endl;
 923   }
 924   d_nonClausalLearnedLiterals.clear();
 925
 926 }
 927
 928 void SmtEnginePrivate::simpITE()
 929 {
 930   TimerStat::CodeTimer simpITETimer(d_smt.d_simpITETime);
 931
 932   Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
 933
 934   for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
 935
 936     d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
 937   }
 938 }
 939
 940
 941 void SmtEnginePrivate::unconstrainedSimp()
 942 {
 943   TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_unconstrainedSimpTime);
 944
 945   Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
 946   d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertionsToCheck);
 947 }
 948
 949
 950 void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
 951   throw(AssertionException) {
 952
 953   Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
 954
 955   set<TNode> done;
 956   stack<TNode> worklist;
 957   worklist.push(top);
 958   done.insert(top);
 959
 960   do {
 961     TNode n = worklist.top();
 962     worklist.pop();
 963
 964     TypeNode t = n.getType();
 965     if(t.isPredicateSubtype()) {
 966       WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl;
 967       Node pred = t.getSubtypePredicate();
 968       Kind k;
 969       // pred can be a LAMBDA, a function constant, or a datatype tester
 970       Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl;
 971       if(d_smt.d_definedFunctions->find(pred) != d_smt.d_definedFunctions->end()) {
 972         k = kind::APPLY;
 973       } else if(pred.getType().isTester()) {
 974         k = kind::APPLY_TESTER;
 975       } else {
 976         k = kind::APPLY_UF;
 977       }
 978       Node app = NodeManager::currentNM()->mkNode(k, pred, n);
 979       Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl;
 980       assertions.push_back(app);
 981     } else if(t.isSubrange()) {
 982       SubrangeBounds bounds = t.getSubrangeBounds();
 983       Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl;
 984       if(bounds.lower.hasBound()) {
 985         Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
 986         Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n);
 987         Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl;
 988         assertions.push_back(lb);
 989       }
 990       if(bounds.upper.hasBound()) {
 991         Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
 992         Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c);
 993         Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl;
 994         assertions.push_back(ub);
 995       }
 996     }
 997
 998     for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
 999       if(done.find(*i) == done.end()) {
1000         worklist.push(*i);
1001         done.insert(*i);
1002       }
1003     }
1004   } while(! worklist.empty());
1005 }
1006
1007 void SmtEnginePrivate::simplifyAssertions()
1008   throw(NoSuchFunctionException, AssertionException) {
1009   try {
1010
1011     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
1012
1013     if(!Options::current()->lazyDefinitionExpansion) {
1014       Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
1015       TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime);
1016       hash_map<TNode, Node, TNodeHashFunction> cache;
1017       for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
1018         d_assertionsToPreprocess[i] =
1019           expandDefinitions(d_assertionsToPreprocess[i], cache);
1020       }
1021     }
1022
1023     if(Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) {
1024       // Perform non-clausal simplification
1025       Trace("simplify") << "SmtEnginePrivate::simplify(): "
1026                         << "performing non-clausal simplification" << endl;
1027       // Abuse the user context to make sure circuit propagator gets backtracked
1028       d_smt.d_userContext->push();
1029       nonClausalSimplify();
1030       d_smt.d_userContext->pop();
1031     } else {
1032       Assert(d_assertionsToCheck.empty());
1033       d_assertionsToCheck.swap(d_assertionsToPreprocess);
1034     }
1035
1036     if(Options::current()->doITESimp) {
1037       // ite simplification
1038       simpITE();
1039     }
1040
1041     if(Options::current()->unconstrainedSimp) {
1042       unconstrainedSimp();
1043     }
1044
1045     if(Options::current()->repeatSimp && Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) {
1046       d_assertionsToCheck.swap(d_assertionsToPreprocess);
1047       // Abuse the user context to make sure circuit propagator gets backtracked
1048       d_smt.d_userContext->push();
1049       nonClausalSimplify();
1050       d_smt.d_userContext->pop();
1051     }
1052
1053     if(Options::current()->doStaticLearning) {
1054       // Perform static learning
1055       Trace("simplify") << "SmtEnginePrivate::simplify(): "
1056                         << "performing static learning" << endl;
1057       staticLearning();
1058     }
1059
1060   } catch(TypeCheckingExceptionPrivate& tcep) {
1061     // Calls to this function should have already weeded out any
1062     // typechecking exceptions via (e.g.) ensureBoolean().  But a
1063     // theory could still create a new expression that isn't
1064     // well-typed, and we don't want the C++ runtime to abort our
1065     // process without any error notice.
1066     stringstream ss;
1067     ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
1068        << "A bad expression was produced.  Original exception follows:\n"
1069        << tcep;
1070     InternalError(ss.str().c_str());
1071   }
1072 }
1073
1074 Result SmtEngine::check() {
1075   Trace("smt") << "SmtEngine::check()" << endl;
1076
1077   // Make sure the prop layer has all of the assertions
1078   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
1079   d_private->processAssertions();
1080
1081   unsigned long millis = 0;
1082   if(d_timeBudgetCumulative != 0) {
1083     millis = getTimeRemaining();
1084     if(millis == 0) {
1085       return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT);
1086     }
1087   }
1088   if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) {
1089     millis = d_timeBudgetPerCall;
1090   }
1091
1092   unsigned long resource = 0;
1093   if(d_resourceBudgetCumulative != 0) {
1094     resource = getResourceRemaining();
1095     if(resource == 0) {
1096       return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT);
1097     }
1098   }
1099   if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
1100     resource = d_resourceBudgetPerCall;
1101   }
1102
1103   Trace("smt") << "SmtEngine::check(): running check" << endl;
1104   Result result = d_propEngine->checkSat(millis, resource);
1105   d_statResultSource.setData("satSolver");
1106
1107   // PropEngine::checkSat() returns the actual amount used in these
1108   // variables.
1109   d_cumulativeTimeUsed += millis;
1110   d_cumulativeResourceUsed += resource;
1111
1112   Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
1113                  << ", conflicts " << d_cumulativeResourceUsed << endl;
1114
1115   if(result.isUnknown() and d_decisionEngine != NULL) {
1116     Result deResult = d_decisionEngine->getResult();
1117     if(not deResult.isUnknown()) {
1118       d_statResultSource.setData("decisionEngine");
1119       result = deResult;
1120     }
1121   }
1122
1123   return result;
1124 }
1125
1126 Result SmtEngine::quickCheck() {
1127   Trace("smt") << "SMT quickCheck()" << endl;
1128   return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK);
1129 }
1130
1131 void SmtEnginePrivate::processAssertions() {
1132
1133   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
1134
1135   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
1136   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
1137
1138   // Any variables of subtype types need to be constrained properly.
1139   // Careful, here: constrainSubtypes() adds to the back of
1140   // d_assertionsToPreprocess, but we don't need to reprocess those.
1141   // We also can't use an iterator, because the vector may be moved in
1142   // memory during this loop.
1143   for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
1144     constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess);
1145   }
1146
1147   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
1148   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
1149
1150   // Simplify the assertions
1151   simplifyAssertions();
1152
1153   // any assertions beyond realAssertionsEnd _must_ be introduced by
1154   // removeITEs().
1155   int realAssertionsEnd = d_assertionsToCheck.size();
1156
1157   {
1158     TimerStat::CodeTimer codeTimer(d_smt.d_iteRemovalTime);
1159     // Remove ITEs
1160     d_smt.d_numAssertionsPre += d_assertionsToCheck.size();
1161     // Remove ITEs, updating d_iteSkolemMap
1162     removeITEs();
1163     d_smt.d_numAssertionsPost += d_assertionsToCheck.size();
1164     // This may need to be in a try-catch
1165     // block. make regress is passing, so
1166     // skipping for now --K
1167   }
1168
1169   if(Options::current()->repeatSimp) {
1170     d_assertionsToCheck.swap(d_assertionsToPreprocess);
1171     simplifyAssertions();
1172     removeITEs();
1173   }
1174
1175   // begin: INVARIANT to maintain: no reordering of assertions or
1176   // introducing new ones
1177 #ifdef CVC4_ASSERTIONS
1178   unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size();
1179 #endif
1180
1181   Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
1182   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
1183   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
1184
1185   if(Dump.isOn("assertions")) {
1186     // Push the simplified assertions to the dump output stream
1187     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
1188       Dump("assertions")
1189         << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr()));
1190     }
1191   }
1192
1193   {
1194     TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime);
1195     // Call the theory preprocessors
1196     d_smt.d_theoryEngine->preprocessStart();
1197     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
1198       d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
1199     }
1200   }
1201
1202   // Push the formula to decision engine
1203   Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
1204   d_smt.d_decisionEngine->addAssertions
1205     (d_assertionsToCheck, realAssertionsEnd, d_iteSkolemMap);
1206
1207   // end: INVARIANT to maintain: no reordering of assertions or
1208   // introducing new ones
1209
1210   // Push the formula to SAT
1211   {
1212     TimerStat::CodeTimer codeTimer(d_smt.d_cnfConversionTime);
1213     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
1214       d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
1215     }
1216   }
1217
1218   d_assertionsToCheck.clear();
1219   d_iteSkolemMap.clear();
1220 }
1221
1222 void SmtEnginePrivate::addFormula(TNode n)
1223   throw(NoSuchFunctionException, AssertionException) {
1224
1225   Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
1226
1227   // Add the normalized formula to the queue
1228   d_assertionsToPreprocess.push_back(theory::Rewriter::rewrite(n));
1229
1230   // If the mode of processing is incremental prepreocess and assert immediately
1231   if (Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL) {
1232     processAssertions();
1233   }
1234 }
1235
1236 void SmtEngine::ensureBoolean(const BoolExpr& e) {
1237   Type type = e.getType(Options::current()->typeChecking);
1238   Type boolType = d_exprManager->booleanType();
1239   if(type != boolType) {
1240     stringstream ss;
1241     ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
1242        << "Expected " << boolType << "\n"
1243        << "The assertion : " << e << "\n"
1244        << "Its type      : " << type;
1245     throw TypeCheckingException(e, ss.str());
1246   }
1247 }
1248
1249 Result SmtEngine::checkSat(const BoolExpr& e) {
1250
1251   Assert(e.isNull() || e.getExprManager() == d_exprManager);
1252
1253   NodeManagerScope nms(d_nodeManager);
1254
1255   Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl;
1256
1257   if(d_queryMade && !Options::current()->incrementalSolving) {
1258     throw ModalException("Cannot make multiple queries unless "
1259                          "incremental solving is enabled "
1260                          "(try --incremental)");
1261   }
1262
1263   // Ensure that the expression is type-checked at this point, and Boolean
1264   if(!e.isNull()) {
1265     ensureBoolean(e);
1266   }
1267
1268   // check to see if a postsolve() is pending
1269   if(d_needPostsolve) {
1270     d_theoryEngine->postsolve();
1271     d_needPostsolve = false;
1272   }
1273
1274   // Push the context
1275   internalPush();
1276
1277   // Note that a query has been made
1278   d_queryMade = true;
1279
1280   // Add the formula
1281   if(!e.isNull()) {
1282     d_problemExtended = true;
1283     d_private->addFormula(e.getNode());
1284   }
1285
1286   // Run the check
1287   Result r = check().asSatisfiabilityResult();
1288   d_needPostsolve = true;
1289
1290   // Dump the query if requested
1291   if(Dump.isOn("benchmark")) {
1292     // the expr already got dumped out if assertion-dumping is on
1293     Dump("benchmark") << CheckSatCommand();
1294   }
1295
1296   // Pop the context
1297   internalPop();
1298
1299   // Remember the status
1300   d_status = r;
1301
1302   d_problemExtended = false;
1303
1304   Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
1305
1306   return r;
1307 }
1308
1309 Result SmtEngine::query(const BoolExpr& e) {
1310
1311   Assert(!e.isNull());
1312   Assert(e.getExprManager() == d_exprManager);
1313
1314   NodeManagerScope nms(d_nodeManager);
1315
1316   Trace("smt") << "SMT query(" << e << ")" << endl;
1317
1318   if(d_queryMade && !Options::current()->incrementalSolving) {
1319     throw ModalException("Cannot make multiple queries unless "
1320                          "incremental solving is enabled "
1321                          "(try --incremental)");
1322   }
1323
1324   // Ensure that the expression is type-checked at this point, and Boolean
1325   ensureBoolean(e);
1326
1327   // check to see if a postsolve() is pending
1328   if(d_needPostsolve) {
1329     d_theoryEngine->postsolve();
1330     d_needPostsolve = false;
1331   }
1332
1333   // Push the context
1334   internalPush();
1335
1336   // Note that a query has been made
1337   d_queryMade = true;
1338
1339   // Add the formula
1340   d_problemExtended = true;
1341   d_private->addFormula(e.getNode().notNode());
1342
1343   // Run the check
1344   Result r = check().asValidityResult();
1345   d_needPostsolve = true;
1346
1347   // Dump the query if requested
1348   if(Dump.isOn("benchmark")) {
1349     // the expr already got dumped out if assertion-dumping is on
1350     Dump("benchmark") << CheckSatCommand();
1351   }
1352
1353   // Pop the context
1354   internalPop();
1355
1356   // Remember the status
1357   d_status = r;
1358
1359   d_problemExtended = false;
1360
1361   Trace("smt") << "SMT query(" << e << ") ==> " << r << endl;
1362
1363   return r;
1364 }
1365
1366 Result SmtEngine::assertFormula(const BoolExpr& e) {
1367   Assert(e.getExprManager() == d_exprManager);
1368   NodeManagerScope nms(d_nodeManager);
1369   Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl;
1370   ensureBoolean(e);
1371   if(d_assertionList != NULL) {
1372     d_assertionList->push_back(e);
1373   }
1374   d_private->addFormula(e.getNode());
1375   return quickCheck().asValidityResult();
1376 }
1377
1378 Expr SmtEngine::simplify(const Expr& e) {
1379   Assert(e.getExprManager() == d_exprManager);
1380   NodeManagerScope nms(d_nodeManager);
1381   if( Options::current()->typeChecking ) {
1382     e.getType(true);// ensure expr is type-checked at this point
1383   }
1384   Trace("smt") << "SMT simplify(" << e << ")" << endl;
1385   if(Dump.isOn("benchmark")) {
1386     Dump("benchmark") << SimplifyCommand(e);
1387   }
1388   return d_private->applySubstitutions(e).toExpr();
1389 }
1390
1391 Expr SmtEngine::getValue(const Expr& e)
1392   throw(ModalException, AssertionException) {
1393   Assert(e.getExprManager() == d_exprManager);
1394   NodeManagerScope nms(d_nodeManager);
1395
1396   // ensure expr is type-checked at this point
1397   Type type = e.getType(Options::current()->typeChecking);
1398
1399   Trace("smt") << "SMT getValue(" << e << ")" << endl;
1400   if(Dump.isOn("benchmark")) {
1401     Dump("benchmark") << GetValueCommand(e);
1402   }
1403   if(!Options::current()->produceModels) {
1404     const char* msg =
1405       "Cannot get value when produce-models options is off.";
1406     throw ModalException(msg);
1407   }
1408   if(d_status.isNull() ||
1409      d_status.asSatisfiabilityResult() != Result::SAT ||
1410      d_problemExtended) {
1411     const char* msg =
1412       "Cannot get value unless immediately preceded by SAT/INVALID response.";
1413     throw ModalException(msg);
1414   }
1415   if(type.isFunction() || type.isPredicate() ||
1416      type.isKind() || type.isSortConstructor()) {
1417     const char* msg =
1418       "Cannot get value of a function, predicate, or sort.";
1419     throw ModalException(msg);
1420   }
1421
1422   // Apply what was learned from preprocessing
1423   Node n = d_private->applySubstitutions(e.getNode());
1424
1425   // Normalize for the theories
1426   n = theory::Rewriter::rewrite(n);
1427
1428   Trace("smt") << "--- getting value of " << n << endl;
1429   Node resultNode = d_theoryEngine->getValue(n);
1430
1431   // type-check the result we got
1432   Assert(resultNode.isNull() || resultNode.getType() == n.getType());
1433   return Expr(d_exprManager, new Node(resultNode));
1434 }
1435
1436 bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
1437   NodeManagerScope nms(d_nodeManager);
1438   Type type = e.getType(Options::current()->typeChecking);
1439   // must be Boolean
1440   CheckArgument( type.isBoolean(), e,
1441                  "expected Boolean-typed variable or function application "
1442                  "in addToAssignment()" );
1443   Node n = e.getNode();
1444   // must be an APPLY of a zero-ary defined function, or a variable
1445   CheckArgument( ( ( n.getKind() == kind::APPLY &&
1446                      ( d_definedFunctions->find(n.getOperator()) !=
1447                        d_definedFunctions->end() ) &&
1448                      n.getNumChildren() == 0 ) ||
1449                    n.getMetaKind() == kind::metakind::VARIABLE ), e,
1450                  "expected variable or defined-function application "
1451                  "in addToAssignment(),\ngot %s", e.toString().c_str() );
1452   if(!Options::current()->produceAssignments) {
1453     return false;
1454   }
1455   if(d_assignments == NULL) {
1456     d_assignments = new(true) AssignmentSet(d_context);
1457   }
1458   d_assignments->insert(n);
1459
1460   return true;
1461 }
1462
1463 SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
1464   Trace("smt") << "SMT getAssignment()" << endl;
1465   NodeManagerScope nms(d_nodeManager);
1466   if(Dump.isOn("benchmark")) {
1467     Dump("benchmark") << GetAssignmentCommand();
1468   }
1469   if(!Options::current()->produceAssignments) {
1470     const char* msg =
1471       "Cannot get the current assignment when "
1472       "produce-assignments option is off.";
1473     throw ModalException(msg);
1474   }
1475   if(d_status.isNull() ||
1476      d_status.asSatisfiabilityResult() != Result::SAT ||
1477      d_problemExtended) {
1478     const char* msg =
1479       "Cannot get the current assignment unless immediately "
1480       "preceded by SAT/INVALID response.";
1481     throw ModalException(msg);
1482   }
1483
1484   if(d_assignments == NULL) {
1485     return SExpr();
1486   }
1487
1488   vector<SExpr> sexprs;
1489   TypeNode boolType = d_nodeManager->booleanType();
1490   for(AssignmentSet::const_iterator i = d_assignments->begin(),
1491         iend = d_assignments->end();
1492       i != iend;
1493       ++i) {
1494     Assert((*i).getType() == boolType);
1495
1496     // Normalize
1497     Node n = theory::Rewriter::rewrite(*i);
1498
1499     Trace("smt") << "--- getting value of " << n << endl;
1500     Node resultNode = d_theoryEngine->getValue(n);
1501
1502     // type-check the result we got
1503     Assert(resultNode.isNull() || resultNode.getType() == boolType);
1504
1505     vector<SExpr> v;
1506     if((*i).getKind() == kind::APPLY) {
1507       Assert((*i).getNumChildren() == 0);
1508       v.push_back((*i).getOperator().toString());
1509     } else {
1510       Assert((*i).getMetaKind() == kind::metakind::VARIABLE);
1511       v.push_back((*i).toString());
1512     }
1513     v.push_back(resultNode.toString());
1514     sexprs.push_back(v);
1515   }
1516   return SExpr(sexprs);
1517 }
1518
1519 Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
1520   Trace("smt") << "SMT getProof()" << endl;
1521   NodeManagerScope nms(d_nodeManager);
1522   if(Dump.isOn("benchmark")) {
1523     Dump("benchmark") << GetProofCommand();
1524   }
1525 #ifdef CVC4_PROOF
1526   if(!Options::current()->proof) {
1527     const char* msg =
1528       "Cannot get a proof when produce-proofs option is off.";
1529     throw ModalException(msg);
1530   }
1531   if(d_status.isNull() ||
1532      d_status.asSatisfiabilityResult() != Result::UNSAT ||
1533      d_problemExtended) {
1534     const char* msg =
1535       "Cannot get a proof unless immediately preceded by UNSAT/VALID response.";
1536     throw ModalException(msg);
1537   }
1538
1539   return ProofManager::getProof();
1540 #else /* CVC4_PROOF */
1541   throw ModalException("This build of CVC4 doesn't have proof support.");
1542 #endif /* CVC4_PROOF */
1543 }
1544
1545 vector<Expr> SmtEngine::getAssertions()
1546   throw(ModalException, AssertionException) {
1547   if(Dump.isOn("benchmark")) {
1548     Dump("benchmark") << GetAssertionsCommand();
1549   }
1550   NodeManagerScope nms(d_nodeManager);
1551   Trace("smt") << "SMT getAssertions()" << endl;
1552   if(!Options::current()->interactive) {
1553     const char* msg =
1554       "Cannot query the current assertion list when not in interactive mode.";
1555     throw ModalException(msg);
1556   }
1557   Assert(d_assertionList != NULL);
1558   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
1559 }
1560
1561 size_t SmtEngine::getStackLevel() const {
1562   NodeManagerScope nms(d_nodeManager);
1563   Trace("smt") << "SMT getStackLevel()" << endl;
1564   return d_context->getLevel();
1565 }
1566
1567 void SmtEngine::push() {
1568   NodeManagerScope nms(d_nodeManager);
1569   Trace("smt") << "SMT push()" << endl;
1570   d_private->processAssertions();
1571   if(Dump.isOn("benchmark")) {
1572     Dump("benchmark") << PushCommand();
1573   }
1574   if(!Options::current()->incrementalSolving) {
1575     throw ModalException("Cannot push when not solving incrementally (use --incremental)");
1576   }
1577
1578   // check to see if a postsolve() is pending
1579   if(d_needPostsolve) {
1580     d_theoryEngine->postsolve();
1581     d_needPostsolve = false;
1582   }
1583
1584   d_userLevels.push_back(d_userContext->getLevel());
1585   internalPush();
1586   Trace("userpushpop") << "SmtEngine: pushed to level "
1587                        << d_userContext->getLevel() << endl;
1588 }
1589
1590 void SmtEngine::pop() {
1591   NodeManagerScope nms(d_nodeManager);
1592   Trace("smt") << "SMT pop()" << endl;
1593   if(Dump.isOn("benchmark")) {
1594     Dump("benchmark") << PopCommand();
1595   }
1596   if(!Options::current()->incrementalSolving) {
1597     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
1598   }
1599   if(d_userContext->getLevel() == 0) {
1600     throw ModalException("Cannot pop beyond the first user frame");
1601   }
1602
1603   // check to see if a postsolve() is pending
1604   if(d_needPostsolve) {
1605     d_theoryEngine->postsolve();
1606     d_needPostsolve = false;
1607   }
1608
1609   AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
1610   while (d_userLevels.back() < d_userContext->getLevel()) {
1611     internalPop();
1612   }
1613   d_userLevels.pop_back();
1614
1615   // Clear out assertion queues etc., in case anything is still in there
1616   d_private->notifyPop();
1617
1618   Trace("userpushpop") << "SmtEngine: popped to level "
1619                        << d_userContext->getLevel() << endl;
1620   // FIXME: should we reset d_status here?
1621   // SMT-LIBv2 spec seems to imply no, but it would make sense to..
1622   // Still, we want the right exit status after any final sequence
1623   // of pops... hm.
1624 }
1625
1626 void SmtEngine::internalPush() {
1627   Trace("smt") << "SmtEngine::internalPush()" << endl;
1628   if(Options::current()->incrementalSolving) {
1629     d_private->processAssertions();
1630     d_userContext->push();
1631     d_context->push();
1632     d_propEngine->push();
1633   }
1634 }
1635
1636 void SmtEngine::internalPop() {
1637   Trace("smt") << "SmtEngine::internalPop()" << endl;
1638   if(Options::current()->incrementalSolving) {
1639     d_propEngine->pop();
1640     d_context->pop();
1641     d_userContext->pop();
1642   }
1643 }
1644
1645 void SmtEngine::interrupt() throw(ModalException) {
1646   d_propEngine->interrupt();
1647 }
1648
1649 void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
1650   if(cumulative) {
1651     Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << endl;
1652     d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
1653   } else {
1654     Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << endl;
1655     d_resourceBudgetPerCall = units;
1656   }
1657 }
1658
1659 void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) {
1660   if(cumulative) {
1661     Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << endl;
1662     d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
1663   } else {
1664     Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << endl;
1665     d_timeBudgetPerCall = millis;
1666   }
1667 }
1668
1669 unsigned long SmtEngine::getResourceUsage() const {
1670   return d_cumulativeResourceUsed;
1671 }
1672
1673 unsigned long SmtEngine::getTimeUsage() const {
1674   return d_cumulativeTimeUsed;
1675 }
1676
1677 unsigned long SmtEngine::getResourceRemaining() const throw(ModalException) {
1678   if(d_resourceBudgetCumulative == 0) {
1679     throw ModalException("No cumulative resource limit is currently set");
1680   }
1681
1682   return d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 :
1683     d_resourceBudgetCumulative - d_cumulativeResourceUsed;
1684 }
1685
1686 unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) {
1687   if(d_timeBudgetCumulative == 0) {
1688     throw ModalException("No cumulative time limit is currently set");
1689   }
1690
1691   return d_timeBudgetCumulative <= d_cumulativeTimeUsed ? 0 :
1692     d_timeBudgetCumulative - d_cumulativeTimeUsed;
1693 }
1694
1695 StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
1696   return d_exprManager->d_nodeManager->getStatisticsRegistry();
1697 }
1698
1699 }/* CVC4 namespace */