src/smt/smt_engine.cpp

   1 /*********************                                                        */
   2 /*! \file smt_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The main entry point into the CVC4 library's SMT interface
  13  **
  14  ** The main entry point into the CVC4 library's SMT interface.
  15  **/
  16
  17 #include "smt/smt_engine.h"
  18
  19 #include <algorithm>
  20 #include <cctype>
  21 #include <iterator>
  22 #include <memory>
  23 #include <sstream>
  24 #include <stack>
  25 #include <string>
  26 #include <unordered_map>
  27 #include <unordered_set>
  28 #include <utility>
  29 #include <vector>
  30
  31 #include "base/configuration.h"
  32 #include "base/configuration_private.h"
  33 #include "base/exception.h"
  34 #include "base/listener.h"
  35 #include "base/modal_exception.h"
  36 #include "base/output.h"
  37 #include "context/cdhashmap.h"
  38 #include "context/cdhashset.h"
  39 #include "context/cdlist.h"
  40 #include "context/context.h"
  41 #include "decision/decision_engine.h"
  42 #include "expr/attribute.h"
  43 #include "expr/expr.h"
  44 #include "expr/kind.h"
  45 #include "expr/metakind.h"
  46 #include "expr/node.h"
  47 #include "expr/node_builder.h"
  48 #include "expr/node_self_iterator.h"
  49 #include "options/arith_options.h"
  50 #include "options/arrays_options.h"
  51 #include "options/base_options.h"
  52 #include "options/booleans_options.h"
  53 #include "options/bv_options.h"
  54 #include "options/datatypes_options.h"
  55 #include "options/decision_mode.h"
  56 #include "options/decision_options.h"
  57 #include "options/language.h"
  58 #include "options/main_options.h"
  59 #include "options/open_ostream.h"
  60 #include "options/option_exception.h"
  61 #include "options/printer_options.h"
  62 #include "options/proof_options.h"
  63 #include "options/prop_options.h"
  64 #include "options/quantifiers_options.h"
  65 #include "options/sep_options.h"
  66 #include "options/set_language.h"
  67 #include "options/smt_options.h"
  68 #include "options/strings_options.h"
  69 #include "options/theory_options.h"
  70 #include "options/uf_options.h"
  71 #include "preprocessing/passes/bv_gauss.h"
  72 #include "preprocessing/passes/int_to_bv.h"
  73 #include "preprocessing/passes/pseudo_boolean_processor.h"
  74 #include "preprocessing/passes/symmetry_detect.h"
  75 #include "preprocessing/preprocessing_pass.h"
  76 #include "preprocessing/preprocessing_pass_context.h"
  77 #include "preprocessing/preprocessing_pass_registry.h"
  78 #include "printer/printer.h"
  79 #include "proof/proof.h"
  80 #include "proof/proof_manager.h"
  81 #include "proof/theory_proof.h"
  82 #include "proof/unsat_core.h"
  83 #include "prop/prop_engine.h"
  84 #include "smt/command.h"
  85 #include "smt/command_list.h"
  86 #include "smt/logic_request.h"
  87 #include "smt/managed_ostreams.h"
  88 #include "smt/smt_engine_scope.h"
  89 #include "smt/term_formula_removal.h"
  90 #include "smt/update_ostream.h"
  91 #include "smt_util/boolean_simplification.h"
  92 #include "smt_util/nary_builder.h"
  93 #include "smt_util/node_visitor.h"
  94 #include "theory/arith/arith_msum.h"
  95 #include "theory/booleans/circuit_propagator.h"
  96 #include "theory/bv/bvintropow2.h"
  97 #include "theory/bv/theory_bv_rewriter.h"
  98 #include "theory/logic_info.h"
  99 #include "theory/quantifiers/fun_def_process.h"
 100 #include "theory/quantifiers/global_negate.h"
 101 #include "theory/quantifiers/macros.h"
 102 #include "theory/quantifiers/quantifiers_rewriter.h"
 103 #include "theory/quantifiers/single_inv_partition.h"
 104 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 105 #include "theory/quantifiers/sygus_inference.h"
 106 #include "theory/quantifiers/term_util.h"
 107 #include "theory/sort_inference.h"
 108 #include "theory/strings/theory_strings.h"
 109 #include "theory/substitutions.h"
 110 #include "theory/theory_engine.h"
 111 #include "theory/theory_model.h"
 112 #include "theory/theory_traits.h"
 113 #include "util/hash.h"
 114 #include "util/proof.h"
 115 #include "util/random.h"
 116 #include "util/resource_manager.h"
 117
 118 using namespace std;
 119 using namespace CVC4;
 120 using namespace CVC4::smt;
 121 using namespace CVC4::preprocessing;
 122 using namespace CVC4::preprocessing::passes;
 123 using namespace CVC4::prop;
 124 using namespace CVC4::context;
 125 using namespace CVC4::theory;
 126
 127 namespace CVC4 {
 128 namespace smt {
 129
 130 struct DeleteCommandFunction : public std::unary_function<const Command*, void>
 131 {
 132   void operator()(const Command* command) { delete command; }
 133 };
 134
 135 void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
 136   std::for_each(commands.begin(), commands.end(), DeleteCommandFunction());
 137   commands.clear();
 138 }
 139
 140 /** Useful for counting the number of recursive calls. */
 141 class ScopeCounter {
 142 private:
 143   unsigned& d_depth;
 144 public:
 145   ScopeCounter(unsigned& d) : d_depth(d) {
 146     ++d_depth;
 147   }
 148   ~ScopeCounter(){
 149     --d_depth;
 150   }
 151 };
 152
 153 /**
 154  * Representation of a defined function.  We keep these around in
 155  * SmtEngine to permit expanding definitions late (and lazily), to
 156  * support getValue() over defined functions, to support user output
 157  * in terms of defined functions, etc.
 158  */
 159 class DefinedFunction {
 160   Node d_func;
 161   vector<Node> d_formals;
 162   Node d_formula;
 163 public:
 164   DefinedFunction() {}
 165   DefinedFunction(Node func, vector<Node> formals, Node formula) :
 166     d_func(func),
 167     d_formals(formals),
 168     d_formula(formula) {
 169   }
 170   Node getFunction() const { return d_func; }
 171   vector<Node> getFormals() const { return d_formals; }
 172   Node getFormula() const { return d_formula; }
 173 };/* class DefinedFunction */
 174
 175 struct SmtEngineStatistics {
 176   /** time spent in gaussian elimination */
 177   TimerStat d_gaussElimTime;
 178   /** time spent in definition-expansion */
 179   TimerStat d_definitionExpansionTime;
 180   /** time spent in non-clausal simplification */
 181   TimerStat d_nonclausalSimplificationTime;
 182   /** time spent in miplib pass */
 183   TimerStat d_miplibPassTime;
 184   /** number of assertions removed by miplib pass */
 185   IntStat d_numMiplibAssertionsRemoved;
 186   /** number of constant propagations found during nonclausal simp */
 187   IntStat d_numConstantProps;
 188   /** time spent in static learning */
 189   TimerStat d_staticLearningTime;
 190   /** time spent in simplifying ITEs */
 191   TimerStat d_simpITETime;
 192   /** time spent in simplifying ITEs */
 193   TimerStat d_unconstrainedSimpTime;
 194   /** time spent removing ITEs */
 195   TimerStat d_iteRemovalTime;
 196   /** time spent in theory preprocessing */
 197   TimerStat d_theoryPreprocessTime;
 198   /** time spent in theory preprocessing */
 199   TimerStat d_rewriteApplyToConstTime;
 200   /** time spent converting to CNF */
 201   TimerStat d_cnfConversionTime;
 202   /** Num of assertions before ite removal */
 203   IntStat d_numAssertionsPre;
 204   /** Num of assertions after ite removal */
 205   IntStat d_numAssertionsPost;
 206   /** time spent in checkModel() */
 207   TimerStat d_checkModelTime;
 208   /** time spent in checkProof() */
 209   TimerStat d_checkProofTime;
 210   /** time spent in checkUnsatCore() */
 211   TimerStat d_checkUnsatCoreTime;
 212   /** time spent in PropEngine::checkSat() */
 213   TimerStat d_solveTime;
 214   /** time spent in pushing/popping */
 215   TimerStat d_pushPopTime;
 216   /** time spent in processAssertions() */
 217   TimerStat d_processAssertionsTime;
 218
 219   /** Has something simplified to false? */
 220   IntStat d_simplifiedToFalse;
 221   /** Number of resource units spent. */
 222   ReferenceStat<uint64_t> d_resourceUnitsUsed;
 223
 224   SmtEngineStatistics() :
 225     d_gaussElimTime("smt::SmtEngine::gaussElimTime"),
 226     d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
 227     d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
 228     d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
 229     d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
 230     d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
 231     d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
 232     d_simpITETime("smt::SmtEngine::simpITETime"),
 233     d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
 234     d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
 235     d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
 236     d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
 237     d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
 238     d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
 239     d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
 240     d_checkModelTime("smt::SmtEngine::checkModelTime"),
 241     d_checkProofTime("smt::SmtEngine::checkProofTime"),
 242     d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
 243     d_solveTime("smt::SmtEngine::solveTime"),
 244     d_pushPopTime("smt::SmtEngine::pushPopTime"),
 245     d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
 246     d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
 247     d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
 248  {
 249
 250     smtStatisticsRegistry()->registerStat(&d_gaussElimTime);
 251     smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
 252     smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime);
 253     smtStatisticsRegistry()->registerStat(&d_miplibPassTime);
 254     smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
 255     smtStatisticsRegistry()->registerStat(&d_numConstantProps);
 256     smtStatisticsRegistry()->registerStat(&d_staticLearningTime);
 257     smtStatisticsRegistry()->registerStat(&d_simpITETime);
 258     smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime);
 259     smtStatisticsRegistry()->registerStat(&d_iteRemovalTime);
 260     smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime);
 261     smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime);
 262     smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
 263     smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
 264     smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
 265     smtStatisticsRegistry()->registerStat(&d_checkModelTime);
 266     smtStatisticsRegistry()->registerStat(&d_checkProofTime);
 267     smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
 268     smtStatisticsRegistry()->registerStat(&d_solveTime);
 269     smtStatisticsRegistry()->registerStat(&d_pushPopTime);
 270     smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
 271     smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
 272     smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
 273   }
 274
 275   ~SmtEngineStatistics() {
 276     smtStatisticsRegistry()->unregisterStat(&d_gaussElimTime);
 277     smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
 278     smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime);
 279     smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime);
 280     smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
 281     smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
 282     smtStatisticsRegistry()->unregisterStat(&d_staticLearningTime);
 283     smtStatisticsRegistry()->unregisterStat(&d_simpITETime);
 284     smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime);
 285     smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime);
 286     smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime);
 287     smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime);
 288     smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
 289     smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
 290     smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
 291     smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
 292     smtStatisticsRegistry()->unregisterStat(&d_checkProofTime);
 293     smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
 294     smtStatisticsRegistry()->unregisterStat(&d_solveTime);
 295     smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
 296     smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
 297     smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
 298     smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
 299   }
 300 };/* struct SmtEngineStatistics */
 301
 302
 303 class SoftResourceOutListener : public Listener {
 304  public:
 305   SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
 306   void notify() override
 307   {
 308     SmtScope scope(d_smt);
 309     Assert(smt::smtEngineInScope());
 310     d_smt->interrupt();
 311   }
 312  private:
 313   SmtEngine* d_smt;
 314 }; /* class SoftResourceOutListener */
 315
 316
 317 class HardResourceOutListener : public Listener {
 318  public:
 319   HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
 320   void notify() override
 321   {
 322     SmtScope scope(d_smt);
 323     theory::Rewriter::clearCaches();
 324   }
 325  private:
 326   SmtEngine* d_smt;
 327 }; /* class HardResourceOutListener */
 328
 329 class SetLogicListener : public Listener {
 330  public:
 331   SetLogicListener(SmtEngine& smt) : d_smt(&smt) {}
 332   void notify() override
 333   {
 334     LogicInfo inOptions(options::forceLogicString());
 335     d_smt->setLogic(inOptions);
 336   }
 337  private:
 338   SmtEngine* d_smt;
 339 }; /* class SetLogicListener */
 340
 341 class BeforeSearchListener : public Listener {
 342  public:
 343   BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
 344   void notify() override { d_smt->beforeSearch(); }
 345
 346  private:
 347   SmtEngine* d_smt;
 348 }; /* class BeforeSearchListener */
 349
 350 class UseTheoryListListener : public Listener {
 351  public:
 352   UseTheoryListListener(TheoryEngine* theoryEngine)
 353       : d_theoryEngine(theoryEngine)
 354   {}
 355
 356   void notify() override
 357   {
 358     std::stringstream commaList(options::useTheoryList());
 359     std::string token;
 360
 361     Debug("UseTheoryListListener") << "UseTheoryListListener::notify() "
 362                                    << options::useTheoryList() << std::endl;
 363
 364     while(std::getline(commaList, token, ',')){
 365       if(token == "help") {
 366         puts(theory::useTheoryHelp);
 367         exit(1);
 368       }
 369       if(theory::useTheoryValidate(token)) {
 370         d_theoryEngine->enableTheoryAlternative(token);
 371       } else {
 372         throw OptionException(
 373             std::string("unknown option for --use-theory : `") + token +
 374             "'.  Try --use-theory=help.");
 375       }
 376     }
 377   }
 378
 379  private:
 380   TheoryEngine* d_theoryEngine;
 381 }; /* class UseTheoryListListener */
 382
 383
 384 class SetDefaultExprDepthListener : public Listener {
 385  public:
 386   void notify() override
 387   {
 388     int depth = options::defaultExprDepth();
 389     Debug.getStream() << expr::ExprSetDepth(depth);
 390     Trace.getStream() << expr::ExprSetDepth(depth);
 391     Notice.getStream() << expr::ExprSetDepth(depth);
 392     Chat.getStream() << expr::ExprSetDepth(depth);
 393     Message.getStream() << expr::ExprSetDepth(depth);
 394     Warning.getStream() << expr::ExprSetDepth(depth);
 395     // intentionally exclude Dump stream from this list
 396   }
 397 };
 398
 399 class SetDefaultExprDagListener : public Listener {
 400  public:
 401   void notify() override
 402   {
 403     int dag = options::defaultDagThresh();
 404     Debug.getStream() << expr::ExprDag(dag);
 405     Trace.getStream() << expr::ExprDag(dag);
 406     Notice.getStream() << expr::ExprDag(dag);
 407     Chat.getStream() << expr::ExprDag(dag);
 408     Message.getStream() << expr::ExprDag(dag);
 409     Warning.getStream() << expr::ExprDag(dag);
 410     Dump.getStream() << expr::ExprDag(dag);
 411   }
 412 };
 413
 414 class SetPrintExprTypesListener : public Listener {
 415  public:
 416   void notify() override
 417   {
 418     bool value = options::printExprTypes();
 419     Debug.getStream() << expr::ExprPrintTypes(value);
 420     Trace.getStream() << expr::ExprPrintTypes(value);
 421     Notice.getStream() << expr::ExprPrintTypes(value);
 422     Chat.getStream() << expr::ExprPrintTypes(value);
 423     Message.getStream() << expr::ExprPrintTypes(value);
 424     Warning.getStream() << expr::ExprPrintTypes(value);
 425     // intentionally exclude Dump stream from this list
 426   }
 427 };
 428
 429 class DumpModeListener : public Listener {
 430  public:
 431   void notify() override
 432   {
 433     const std::string& value = options::dumpModeString();
 434     Dump.setDumpFromString(value);
 435   }
 436 };
 437
 438 class PrintSuccessListener : public Listener {
 439  public:
 440   void notify() override
 441   {
 442     bool value = options::printSuccess();
 443     Debug.getStream() << Command::printsuccess(value);
 444     Trace.getStream() << Command::printsuccess(value);
 445     Notice.getStream() << Command::printsuccess(value);
 446     Chat.getStream() << Command::printsuccess(value);
 447     Message.getStream() << Command::printsuccess(value);
 448     Warning.getStream() << Command::printsuccess(value);
 449     *options::out() << Command::printsuccess(value);
 450   }
 451 };
 452
 453
 454
 455 /**
 456  * This is an inelegant solution, but for the present, it will work.
 457  * The point of this is to separate the public and private portions of
 458  * the SmtEngine class, so that smt_engine.h doesn't
 459  * include "expr/node.h", which is a private CVC4 header (and can lead
 460  * to linking errors due to the improper inlining of non-visible symbols
 461  * into user code!).
 462  *
 463  * The "real" solution (that which is usually implemented) is to move
 464  * ALL the implementation to SmtEnginePrivate and maintain a
 465  * heap-allocated instance of it in SmtEngine.  SmtEngine (the public
 466  * one) becomes an "interface shell" which simply acts as a forwarder
 467  * of method calls.
 468  */
 469 class SmtEnginePrivate : public NodeManagerListener {
 470   SmtEngine& d_smt;
 471
 472   typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
 473   typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 474
 475   /**
 476    * Manager for limiting time and abstract resource usage.
 477    */
 478   ResourceManager* d_resourceManager;
 479
 480   /** Manager for the memory of regular-output-channel. */
 481   ManagedRegularOutputChannel d_managedRegularChannel;
 482
 483   /** Manager for the memory of diagnostic-output-channel. */
 484   ManagedDiagnosticOutputChannel d_managedDiagnosticChannel;
 485
 486   /** Manager for the memory of --dump-to. */
 487   ManagedDumpOStream d_managedDumpChannel;
 488
 489   /** Manager for --replay-log. */
 490   ManagedReplayLogOstream d_managedReplayLog;
 491
 492   /**
 493    * This list contains:
 494    *  softResourceOut
 495    *  hardResourceOut
 496    *  setForceLogic
 497    *  beforeSearchListener
 498    *  UseTheoryListListener
 499    *
 500    * This needs to be deleted before both NodeManager's Options,
 501    * SmtEngine, d_resourceManager, and TheoryEngine.
 502    */
 503   ListenerRegistrationList* d_listenerRegistrations;
 504
 505   /** Learned literals */
 506   vector<Node> d_nonClausalLearnedLiterals;
 507
 508   /** Size of assertions array when preprocessing starts */
 509   unsigned d_realAssertionsEnd;
 510
 511   /** A circuit propagator for non-clausal propositional deduction */
 512   booleans::CircuitPropagator d_propagator;
 513   bool d_propagatorNeedsFinish;
 514   std::vector<Node> d_boolVars;
 515
 516   /** Assertions in the preprocessing pipeline */
 517   AssertionPipeline d_assertions;
 518
 519   /** Whether any assertions have been processed */
 520   CDO<bool> d_assertionsProcessed;
 521
 522   /** Index for where to store substitutions */
 523   CDO<unsigned> d_substitutionsIndex;
 524
 525   // Cached true value
 526   Node d_true;
 527
 528   /**
 529    * A context that never pushes/pops, for use by CD structures (like
 530    * SubstitutionMaps) that should be "global".
 531    */
 532   context::Context d_fakeContext;
 533
 534   /**
 535    * A map of AbsractValues to their actual constants.  Only used if
 536    * options::abstractValues() is on.
 537    */
 538   SubstitutionMap d_abstractValueMap;
 539
 540   /**
 541    * A mapping of all abstract values (actual value |-> abstract) that
 542    * we've handed out.  This is necessary to ensure that we give the
 543    * same AbstractValues for the same real constants.  Only used if
 544    * options::abstractValues() is on.
 545    */
 546   NodeToNodeHashMap d_abstractValues;
 547
 548   /** Number of calls of simplify assertions active.
 549    */
 550   unsigned d_simplifyAssertionsDepth;
 551
 552   /** TODO: whether certain preprocess steps are necessary */
 553   //bool d_needsExpandDefs;
 554
 555   //------------------------------- expression names
 556   /** mapping from expressions to name */
 557   context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
 558   //------------------------------- end expression names
 559 public:
 560   /**
 561    * Map from skolem variables to index in d_assertions containing
 562    * corresponding introduced Boolean ite
 563    */
 564   IteSkolemMap d_iteSkolemMap;
 565
 566   /** Instance of the ITE remover */
 567   RemoveTermFormulas d_iteRemover;
 568
 569   /* Finishes the initialization of the private portion of SMTEngine. */
 570   void finishInit();
 571
 572  private:
 573   std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
 574   PreprocessingPassRegistry d_preprocessingPassRegistry;
 575
 576   /** The top level substitutions */
 577   SubstitutionMap d_topLevelSubstitutions;
 578
 579   static const bool d_doConstantProp = true;
 580
 581   /**
 582    * Runs the nonclausal solver and tries to solve all the assigned
 583    * theory literals.
 584    *
 585    * Returns false if the formula simplifies to "false"
 586    */
 587   bool nonClausalSimplify();
 588
 589   /**
 590    * Performs static learning on the assertions.
 591    */
 592   void staticLearning();
 593
 594   /**
 595    * Remove ITEs from the assertions.
 596    */
 597   void removeITEs();
 598
 599   Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq);
 600   Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false);
 601
 602   /**
 603    * Helper function to fix up assertion list to restore invariants needed after
 604    * ite removal.
 605    */
 606   void collectSkolems(TNode n, set<TNode>& skolemSet, NodeToBoolHashMap& cache);
 607
 608   /**
 609    * Helper function to fix up assertion list to restore invariants needed after
 610    * ite removal.
 611    */
 612   bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
 613
 614   // Lift bit-vectors of size 1 to booleans
 615   void bvToBool();
 616
 617   // Convert booleans to bit-vectors of size 1
 618   void boolToBv();
 619
 620   // Abstract common structure over small domains to UF
 621   // return true if changes were made.
 622   void bvAbstraction();
 623
 624   // Simplify ITE structure
 625   bool simpITE();
 626
 627   // Simplify based on unconstrained values
 628   void unconstrainedSimp();
 629
 630   /**
 631    * Ensures the assertions asserted after before now effectively come before
 632    * d_realAssertionsEnd.
 633    */
 634   void compressBeforeRealAssertions(size_t before);
 635
 636   /**
 637    * Trace nodes back to their assertions using CircuitPropagator's
 638    * BackEdgesMap.
 639    */
 640   void traceBackToAssertions(const std::vector<Node>& nodes,
 641                              std::vector<TNode>& assertions);
 642
 643   /**
 644    * Remove conjuncts in toRemove from conjunction n. Return # of removed
 645    * conjuncts.
 646    */
 647   size_t removeFromConjunction(Node& n,
 648                                const std::unordered_set<unsigned long>& toRemove);
 649
 650   /** Scrub miplib encodings. */
 651   void doMiplibTrick();
 652
 653   /**
 654    * Perform non-clausal simplification of a Node.  This involves
 655    * Theory implementations, but does NOT involve the SAT solver in
 656    * any way.
 657    *
 658    * Returns false if the formula simplifies to "false"
 659    */
 660   bool simplifyAssertions();
 661
 662  public:
 663
 664   SmtEnginePrivate(SmtEngine& smt) :
 665     d_smt(smt),
 666     d_managedRegularChannel(),
 667     d_managedDiagnosticChannel(),
 668     d_managedDumpChannel(),
 669     d_managedReplayLog(),
 670     d_listenerRegistrations(new ListenerRegistrationList()),
 671     d_nonClausalLearnedLiterals(),
 672     d_realAssertionsEnd(0),
 673     d_propagator(d_nonClausalLearnedLiterals, true, true),
 674     d_propagatorNeedsFinish(false),
 675     d_assertions(),
 676     d_assertionsProcessed(smt.d_userContext, false),
 677     d_substitutionsIndex(smt.d_userContext, 0),
 678     d_fakeContext(),
 679     d_abstractValueMap(&d_fakeContext),
 680     d_abstractValues(),
 681     d_simplifyAssertionsDepth(0),
 682     //d_needsExpandDefs(true),  //TODO?
 683     d_exprNames(smt.d_userContext),
 684     d_iteSkolemMap(),
 685     d_iteRemover(smt.d_userContext),
 686     d_topLevelSubstitutions(smt.d_userContext)
 687   {
 688     d_smt.d_nodeManager->subscribeEvents(this);
 689     d_true = NodeManager::currentNM()->mkConst(true);
 690     d_resourceManager = NodeManager::currentResourceManager();
 691
 692     d_listenerRegistrations->add(d_resourceManager->registerSoftListener(
 693         new SoftResourceOutListener(d_smt)));
 694
 695     d_listenerRegistrations->add(d_resourceManager->registerHardListener(
 696         new HardResourceOutListener(d_smt)));
 697
 698     Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
 699     d_listenerRegistrations->add(
 700         nodeManagerOptions.registerForceLogicListener(
 701             new SetLogicListener(d_smt), true));
 702
 703     // Multiple options reuse BeforeSearchListener so registration requires an
 704     // extra bit of care.
 705     // We can safely not call notify on this before search listener at
 706     // registration time. This d_smt cannot be beforeSearch at construction
 707     // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
 708     // not have to be called.
 709     d_listenerRegistrations->add(
 710         nodeManagerOptions.registerBeforeSearchListener(
 711             new BeforeSearchListener(d_smt)));
 712
 713     // These do need registration calls.
 714     d_listenerRegistrations->add(
 715         nodeManagerOptions.registerSetDefaultExprDepthListener(
 716             new SetDefaultExprDepthListener(), true));
 717     d_listenerRegistrations->add(
 718         nodeManagerOptions.registerSetDefaultExprDagListener(
 719             new SetDefaultExprDagListener(), true));
 720     d_listenerRegistrations->add(
 721         nodeManagerOptions.registerSetPrintExprTypesListener(
 722             new SetPrintExprTypesListener(), true));
 723     d_listenerRegistrations->add(
 724         nodeManagerOptions.registerSetDumpModeListener(
 725             new DumpModeListener(), true));
 726     d_listenerRegistrations->add(
 727         nodeManagerOptions.registerSetPrintSuccessListener(
 728             new PrintSuccessListener(), true));
 729     d_listenerRegistrations->add(
 730         nodeManagerOptions.registerSetRegularOutputChannelListener(
 731             new SetToDefaultSourceListener(&d_managedRegularChannel), true));
 732     d_listenerRegistrations->add(
 733         nodeManagerOptions.registerSetDiagnosticOutputChannelListener(
 734             new SetToDefaultSourceListener(&d_managedDiagnosticChannel), true));
 735     d_listenerRegistrations->add(
 736         nodeManagerOptions.registerDumpToFileNameListener(
 737             new SetToDefaultSourceListener(&d_managedDumpChannel), true));
 738     d_listenerRegistrations->add(
 739         nodeManagerOptions.registerSetReplayLogFilename(
 740             new SetToDefaultSourceListener(&d_managedReplayLog), true));
 741   }
 742
 743   ~SmtEnginePrivate()
 744   {
 745     delete d_listenerRegistrations;
 746
 747     if(d_propagatorNeedsFinish) {
 748       d_propagator.finish();
 749       d_propagatorNeedsFinish = false;
 750     }
 751     d_smt.d_nodeManager->unsubscribeEvents(this);
 752   }
 753
 754   ResourceManager* getResourceManager() { return d_resourceManager; }
 755   void spendResource(unsigned amount)
 756   {
 757     d_resourceManager->spendResource(amount);
 758   }
 759
 760   void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
 761   {
 762     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
 763                          0,
 764                          tn.toType());
 765     if((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) {
 766       d_smt.addToModelCommandAndDump(c, flags);
 767     }
 768   }
 769
 770   void nmNotifyNewSortConstructor(TypeNode tn) override
 771   {
 772     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
 773                          tn.getAttribute(expr::SortArityAttr()),
 774                          tn.toType());
 775     d_smt.addToModelCommandAndDump(c);
 776   }
 777
 778   void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override
 779   {
 780     DatatypeDeclarationCommand c(dtts);
 781     d_smt.addToModelCommandAndDump(c);
 782   }
 783
 784   void nmNotifyNewVar(TNode n, uint32_t flags) override
 785   {
 786     DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
 787                              n.toExpr(),
 788                              n.getType().toType());
 789     if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
 790       d_smt.addToModelCommandAndDump(c, flags);
 791     }
 792     if(n.getType().isBoolean() && !options::incrementalSolving()) {
 793       d_boolVars.push_back(n);
 794     }
 795   }
 796
 797   void nmNotifyNewSkolem(TNode n,
 798                          const std::string& comment,
 799                          uint32_t flags) override
 800   {
 801     string id = n.getAttribute(expr::VarNameAttr());
 802     DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
 803     if(Dump.isOn("skolems") && comment != "") {
 804       Dump("skolems") << CommentCommand(id + " is " + comment);
 805     }
 806     if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
 807       d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
 808     }
 809     if(n.getType().isBoolean() && !options::incrementalSolving()) {
 810       d_boolVars.push_back(n);
 811     }
 812   }
 813
 814   void nmNotifyDeleteNode(TNode n) override {}
 815
 816   Node applySubstitutions(TNode node) const {
 817     return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
 818   }
 819
 820   /**
 821    * Apply the substitutions in d_topLevelAssertions and the rewriter to each of
 822    * the assertions in d_assertions, and store the result back in d_assertions.
 823    */
 824   void applySubstitutionsToAssertions();
 825
 826   /**
 827    * Process the assertions that have been asserted.
 828    */
 829   void processAssertions();
 830
 831   /** Process a user push.
 832   */
 833   void notifyPush() {
 834
 835   }
 836
 837   /**
 838    * Process a user pop.  Clears out the non-context-dependent stuff in this
 839    * SmtEnginePrivate.  Necessary to clear out our assertion vectors in case
 840    * someone does a push-assert-pop without a check-sat. It also pops the
 841    * last map of expression names from notifyPush.
 842    */
 843   void notifyPop() {
 844     d_assertions.clear();
 845     d_nonClausalLearnedLiterals.clear();
 846     d_realAssertionsEnd = 0;
 847     d_iteSkolemMap.clear();
 848   }
 849
 850   /**
 851    * Adds a formula to the current context.  Action here depends on
 852    * the SimplificationMode (in the current Options scope); the
 853    * formula might be pushed out to the propositional layer
 854    * immediately, or it might be simplified and kept, or it might not
 855    * even be simplified.
 856    * the 2nd and 3rd arguments added for bookkeeping for proofs
 857    */
 858   void addFormula(TNode n, bool inUnsatCore, bool inInput = true);
 859
 860   /** Expand definitions in n. */
 861   Node expandDefinitions(TNode n,
 862                          NodeToNodeHashMap& cache,
 863                          bool expandOnly = false);
 864
 865   /**
 866    * Simplify node "in" by expanding definitions and applying any
 867    * substitutions learned from preprocessing.
 868    */
 869   Node simplify(TNode in) {
 870     // Substitute out any abstract values in ex.
 871     // Expand definitions.
 872     NodeToNodeHashMap cache;
 873     Node n = expandDefinitions(in, cache).toExpr();
 874     // Make sure we've done all preprocessing, etc.
 875     Assert(d_assertions.size() == 0);
 876     return applySubstitutions(n).toExpr();
 877   }
 878
 879   /**
 880    * Substitute away all AbstractValues in a node.
 881    */
 882   Node substituteAbstractValues(TNode n) {
 883     // We need to do this even if options::abstractValues() is off,
 884     // since the setting might have changed after we already gave out
 885     // some abstract values.
 886     return d_abstractValueMap.apply(n);
 887   }
 888
 889   /**
 890    * Make a new (or return an existing) abstract value for a node.
 891    * Can only use this if options::abstractValues() is on.
 892    */
 893   Node mkAbstractValue(TNode n) {
 894     Assert(options::abstractValues());
 895     Node& val = d_abstractValues[n];
 896     if(val.isNull()) {
 897       val = d_smt.d_nodeManager->mkAbstractValue(n.getType());
 898       d_abstractValueMap.addSubstitution(val, n);
 899     }
 900     // We are supposed to ascribe types to all abstract values that go out.
 901     NodeManager* current = d_smt.d_nodeManager;
 902     Node ascription = current->mkConst(AscriptionType(n.getType().toType()));
 903     Node retval = current->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val);
 904     return retval;
 905   }
 906
 907   NodeToNodeHashMap d_rewriteApplyToConstCache;
 908   Node rewriteApplyToConst(TNode n) {
 909     Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl;
 910
 911     if(n.getMetaKind() == kind::metakind::CONSTANT ||
 912        n.getMetaKind() == kind::metakind::VARIABLE ||
 913        n.getMetaKind() == kind::metakind::NULLARY_OPERATOR)
 914     {
 915       return n;
 916     }
 917
 918     if(d_rewriteApplyToConstCache.find(n) != d_rewriteApplyToConstCache.end()) {
 919       Trace("rewriteApplyToConst") << "in cache :: "
 920                                    << d_rewriteApplyToConstCache[n]
 921                                    << std::endl;
 922       return d_rewriteApplyToConstCache[n];
 923     }
 924
 925     if(n.getKind() == kind::APPLY_UF) {
 926       if(n.getNumChildren() == 1 && n[0].isConst() &&
 927          n[0].getType().isInteger())
 928       {
 929         stringstream ss;
 930         ss << n.getOperator() << "_";
 931         if(n[0].getConst<Rational>() < 0) {
 932           ss << "m" << -n[0].getConst<Rational>();
 933         } else {
 934           ss << n[0];
 935         }
 936         Node newvar = NodeManager::currentNM()->mkSkolem(
 937             ss.str(), n.getType(), "rewriteApplyToConst skolem",
 938             NodeManager::SKOLEM_EXACT_NAME);
 939         d_rewriteApplyToConstCache[n] = newvar;
 940         Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl;
 941         return newvar;
 942       } else {
 943         stringstream ss;
 944         ss << "The rewrite-apply-to-const preprocessor is currently limited;"
 945            << std::endl
 946            << "it only works if all function symbols are unary and with Integer"
 947            << std::endl
 948            << "domain, and all applications are to integer values." << std::endl
 949            << "Found application: " << n;
 950         Unhandled(ss.str());
 951       }
 952     }
 953
 954     NodeBuilder<> builder(n.getKind());
 955     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
 956       builder << n.getOperator();
 957     }
 958     for(unsigned i = 0; i < n.getNumChildren(); ++i) {
 959       builder << rewriteApplyToConst(n[i]);
 960     }
 961     Node rewr = builder;
 962     d_rewriteApplyToConstCache[n] = rewr;
 963     Trace("rewriteApplyToConst") << "built :: " << rewr << std::endl;
 964     return rewr;
 965   }
 966
 967   void addUseTheoryListListener(TheoryEngine* theoryEngine){
 968     Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
 969     d_listenerRegistrations->add(
 970         nodeManagerOptions.registerUseTheoryListListener(
 971             new UseTheoryListListener(theoryEngine), true));
 972   }
 973
 974   std::ostream* getReplayLog() const {
 975     return d_managedReplayLog.getReplayLog();
 976   }
 977
 978   //------------------------------- expression names
 979   // implements setExpressionName, as described in smt_engine.h
 980   void setExpressionName(Expr e, std::string name) {
 981     d_exprNames[Node::fromExpr(e)] = name;
 982   }
 983
 984   // implements getExpressionName, as described in smt_engine.h
 985   bool getExpressionName(Expr e, std::string& name) const {
 986     context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e);
 987     if(it!=d_exprNames.end()) {
 988       name = (*it).second;
 989       return true;
 990     }else{
 991       return false;
 992     }
 993   }
 994   //------------------------------- end expression names
 995
 996 };/* class SmtEnginePrivate */
 997
 998 }/* namespace CVC4::smt */
 999
1000 SmtEngine::SmtEngine(ExprManager* em)
1001     : d_context(new Context()),
1002       d_userLevels(),
1003       d_userContext(new UserContext()),
1004       d_exprManager(em),
1005       d_nodeManager(d_exprManager->getNodeManager()),
1006       d_decisionEngine(NULL),
1007       d_theoryEngine(NULL),
1008       d_propEngine(NULL),
1009       d_proofManager(NULL),
1010       d_definedFunctions(NULL),
1011       d_fmfRecFunctionsDefined(NULL),
1012       d_assertionList(NULL),
1013       d_assignments(NULL),
1014       d_modelGlobalCommands(),
1015       d_modelCommands(NULL),
1016       d_dumpCommands(),
1017       d_defineCommands(),
1018       d_logic(),
1019       d_originalOptions(),
1020       d_pendingPops(0),
1021       d_fullyInited(false),
1022       d_problemExtended(false),
1023       d_queryMade(false),
1024       d_needPostsolve(false),
1025       d_earlyTheoryPP(true),
1026       d_globalNegation(false),
1027       d_status(),
1028       d_replayStream(NULL),
1029       d_private(NULL),
1030       d_statisticsRegistry(NULL),
1031       d_stats(NULL),
1032       d_channels(new LemmaChannels())
1033 {
1034   SmtScope smts(this);
1035   d_originalOptions.copyValues(em->getOptions());
1036   d_private = new smt::SmtEnginePrivate(*this);
1037   d_statisticsRegistry = new StatisticsRegistry();
1038   d_stats = new SmtEngineStatistics();
1039   d_stats->d_resourceUnitsUsed.setData(
1040       d_private->getResourceManager()->getResourceUsage());
1041
1042   // The ProofManager is constructed before any other proof objects such as
1043   // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
1044   // initialized in TheoryEngine and PropEngine respectively.
1045   Assert(d_proofManager == NULL);
1046
1047   // d_proofManager must be created before Options has been finished
1048   // being parsed from the input file. Because of this, we cannot trust
1049   // that options::proof() is set correctly yet.
1050 #ifdef CVC4_PROOF
1051   d_proofManager = new ProofManager(d_userContext);
1052 #endif
1053
1054   // We have mutual dependency here, so we add the prop engine to the theory
1055   // engine later (it is non-essential there)
1056   d_theoryEngine = new TheoryEngine(d_context, d_userContext,
1057                                     d_private->d_iteRemover,
1058                                     const_cast<const LogicInfo&>(d_logic),
1059                                     d_channels);
1060
1061   // Add the theories
1062   for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
1063     TheoryConstructor::addTheory(d_theoryEngine, id);
1064     //register with proof engine if applicable
1065 #ifdef CVC4_PROOF
1066     ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id));
1067 #endif
1068   }
1069
1070   d_private->addUseTheoryListListener(d_theoryEngine);
1071
1072   // global push/pop around everything, to ensure proper destruction
1073   // of context-dependent data structures
1074   d_userContext->push();
1075   d_context->push();
1076
1077   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
1078   d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext);
1079   d_modelCommands = new(true) smt::CommandList(d_userContext);
1080 }
1081
1082 void SmtEngine::finishInit() {
1083   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
1084   // ensure that our heuristics are properly set up
1085   setDefaults();
1086
1087   Trace("smt-debug") << "Making decision engine..." << std::endl;
1088
1089   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
1090   d_decisionEngine->init();   // enable appropriate strategies
1091
1092   Trace("smt-debug") << "Making prop engine..." << std::endl;
1093   d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context,
1094                                 d_userContext, d_private->getReplayLog(),
1095                                 d_replayStream, d_channels);
1096
1097   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
1098   d_theoryEngine->setPropEngine(d_propEngine);
1099   d_theoryEngine->setDecisionEngine(d_decisionEngine);
1100   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
1101   d_theoryEngine->finishInit();
1102
1103   Trace("smt-debug") << "Set up assertion list..." << std::endl;
1104   // [MGD 10/20/2011] keep around in incremental mode, due to a
1105   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
1106   // first, some user-context-dependent TNodes might still exist
1107   // with rc == 0.
1108   if(options::produceAssertions() ||
1109      options::incrementalSolving()) {
1110     // In the case of incremental solving, we appear to need these to
1111     // ensure the relevant Nodes remain live.
1112     d_assertionList = new(true) AssertionList(d_userContext);
1113   }
1114
1115   // dump out a set-logic command
1116   if(Dump.isOn("benchmark")) {
1117     if (Dump.isOn("raw-benchmark")) {
1118       Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic.getLogicString());
1119     } else {
1120       LogicInfo everything;
1121       everything.lock();
1122       Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.")
1123                         << SetBenchmarkLogicCommand(everything.getLogicString());
1124     }
1125   }
1126
1127   Trace("smt-debug") << "Dump declaration commands..." << std::endl;
1128   // dump out any pending declaration commands
1129   for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
1130     Dump("declarations") << *d_dumpCommands[i];
1131     delete d_dumpCommands[i];
1132   }
1133   d_dumpCommands.clear();
1134
1135   PROOF( ProofManager::currentPM()->setLogic(d_logic); );
1136   PROOF({
1137       for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
1138         ProofManager::currentPM()->getTheoryProofEngine()->
1139           finishRegisterTheory(d_theoryEngine->theoryOf(id));
1140       }
1141     });
1142   d_private->finishInit();
1143   Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
1144 }
1145
1146 void SmtEngine::finalOptionsAreSet() {
1147   if(d_fullyInited) {
1148     return;
1149   }
1150
1151   if(! d_logic.isLocked()) {
1152     setLogicInternal();
1153   }
1154
1155   // finish initialization, create the prop engine, etc.
1156   finishInit();
1157
1158   AlwaysAssert( d_propEngine->getAssertionLevel() == 0,
1159                 "The PropEngine has pushed but the SmtEngine "
1160                 "hasn't finished initializing!" );
1161
1162   d_fullyInited = true;
1163   Assert(d_logic.isLocked());
1164
1165   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
1166   d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
1167 }
1168
1169 void SmtEngine::shutdown() {
1170   doPendingPops();
1171
1172   while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
1173     internalPop(true);
1174   }
1175
1176   // check to see if a postsolve() is pending
1177   if(d_needPostsolve) {
1178     d_theoryEngine->postsolve();
1179     d_needPostsolve = false;
1180   }
1181
1182   if(d_propEngine != NULL) {
1183     d_propEngine->shutdown();
1184   }
1185   if(d_theoryEngine != NULL) {
1186     d_theoryEngine->shutdown();
1187   }
1188   if(d_decisionEngine != NULL) {
1189     d_decisionEngine->shutdown();
1190   }
1191 }
1192
1193 SmtEngine::~SmtEngine()
1194 {
1195   SmtScope smts(this);
1196
1197   try {
1198     shutdown();
1199
1200     // global push/pop around everything, to ensure proper destruction
1201     // of context-dependent data structures
1202     d_context->popto(0);
1203     d_userContext->popto(0);
1204
1205     if(d_assignments != NULL) {
1206       d_assignments->deleteSelf();
1207     }
1208
1209     if(d_assertionList != NULL) {
1210       d_assertionList->deleteSelf();
1211     }
1212
1213     for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
1214       delete d_dumpCommands[i];
1215       d_dumpCommands[i] = NULL;
1216     }
1217     d_dumpCommands.clear();
1218
1219     DeleteAndClearCommandVector(d_modelGlobalCommands);
1220
1221     if(d_modelCommands != NULL) {
1222       d_modelCommands->deleteSelf();
1223     }
1224
1225     d_definedFunctions->deleteSelf();
1226     d_fmfRecFunctionsDefined->deleteSelf();
1227
1228     delete d_theoryEngine;
1229     d_theoryEngine = NULL;
1230     delete d_propEngine;
1231     d_propEngine = NULL;
1232     delete d_decisionEngine;
1233     d_decisionEngine = NULL;
1234
1235
1236 // d_proofManager is always created when proofs are enabled at configure time.
1237 // Becuase of this, this code should not be wrapped in PROOF() which
1238 // additionally checks flags such as options::proof().
1239 #ifdef CVC4_PROOF
1240     delete d_proofManager;
1241     d_proofManager = NULL;
1242 #endif
1243
1244     delete d_stats;
1245     d_stats = NULL;
1246     delete d_statisticsRegistry;
1247     d_statisticsRegistry = NULL;
1248
1249     delete d_private;
1250     d_private = NULL;
1251
1252     delete d_userContext;
1253     d_userContext = NULL;
1254     delete d_context;
1255     d_context = NULL;
1256
1257     delete d_channels;
1258     d_channels = NULL;
1259
1260   } catch(Exception& e) {
1261     Warning() << "CVC4 threw an exception during cleanup." << endl
1262               << e << endl;
1263   }
1264 }
1265
1266 void SmtEngine::setLogic(const LogicInfo& logic)
1267 {
1268   SmtScope smts(this);
1269   if(d_fullyInited) {
1270     throw ModalException("Cannot set logic in SmtEngine after the engine has "
1271                          "finished initializing.");
1272   }
1273   d_logic = logic;
1274   setLogicInternal();
1275 }
1276
1277 void SmtEngine::setLogic(const std::string& s)
1278 {
1279   SmtScope smts(this);
1280   try {
1281     setLogic(LogicInfo(s));
1282   } catch(IllegalArgumentException& e) {
1283     throw LogicException(e.what());
1284   }
1285 }
1286
1287 void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
1288 LogicInfo SmtEngine::getLogicInfo() const {
1289   return d_logic;
1290 }
1291 void SmtEngine::setLogicInternal()
1292 {
1293   Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already"
1294          " finished initializing for this run");
1295   d_logic.lock();
1296 }
1297
1298 void SmtEngine::setDefaults() {
1299   Random::getRandom().setSeed(options::seed());
1300   // Language-based defaults
1301   if (!options::bitvectorDivByZeroConst.wasSetByUser())
1302   {
1303     options::bitvectorDivByZeroConst.set(options::inputLanguage()
1304                                          == language::input::LANG_SMTLIB_V2_6);
1305   }
1306   if (options::inputLanguage() == language::input::LANG_SYGUS)
1307   {
1308     if (!options::ceGuidedInst.wasSetByUser())
1309     {
1310       options::ceGuidedInst.set(true);
1311     }
1312     // must use Ferrante/Rackoff for real arithmetic
1313     if (!options::cbqiMidpoint.wasSetByUser())
1314     {
1315       options::cbqiMidpoint.set(true);
1316     }
1317   }
1318
1319   if(options::forceLogicString.wasSetByUser()) {
1320     d_logic = LogicInfo(options::forceLogicString());
1321   }else if (options::solveIntAsBV() > 0) {
1322     d_logic = LogicInfo("QF_BV");
1323   }else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt()) {
1324     d_logic = LogicInfo("QF_NIA");
1325   } else if ((d_logic.getLogicString() == "QF_UFBV" ||
1326               d_logic.getLogicString() == "QF_ABV") &&
1327              options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
1328     d_logic = LogicInfo("QF_BV");
1329   }
1330
1331   // set strings-exp
1332   /* - disabled for 1.4 release [MGD 2014.06.25]
1333   if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
1334     if(! options::stringExp.wasSetByUser()) {
1335       options::stringExp.set( true );
1336       Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
1337     }
1338   }
1339   */
1340   // for strings
1341   if(options::stringExp()) {
1342     if( !d_logic.isQuantified() ) {
1343       d_logic = d_logic.getUnlockedCopy();
1344       d_logic.enableQuantifiers();
1345       d_logic.lock();
1346       Trace("smt") << "turning on quantifier logic, for strings-exp"
1347                    << std::endl;
1348     }
1349     if(! options::fmfBound.wasSetByUser()) {
1350       options::fmfBound.set( true );
1351       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
1352     }
1353     if(! options::fmfInstEngine.wasSetByUser()) {
1354       options::fmfInstEngine.set( true );
1355       Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl;
1356     }
1357     /*
1358     if(! options::rewriteDivk.wasSetByUser()) {
1359       options::rewriteDivk.set( true );
1360       Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
1361     }*/
1362     /*
1363     if(! options::stringFMF.wasSetByUser()) {
1364       options::stringFMF.set( true );
1365       Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl;
1366     }
1367     */
1368   }
1369
1370   // sygus inference may require datatypes
1371   if (options::sygusInference())
1372   {
1373     d_logic = d_logic.getUnlockedCopy();
1374     d_logic.enableTheory(THEORY_DATATYPES);
1375     d_logic.lock();
1376   }
1377
1378   if ((options::checkModels() || options::checkSynthSol())
1379       && !options::produceAssertions())
1380   {
1381       Notice() << "SmtEngine: turning on produce-assertions to support "
1382                << "check-models or check-synth-sol." << endl;
1383       setOption("produce-assertions", SExpr("true"));
1384     }
1385
1386   if(options::unsatCores()) {
1387     if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
1388       if(options::simplificationMode.wasSetByUser()) {
1389         throw OptionException("simplification not supported with unsat cores");
1390       }
1391       Notice() << "SmtEngine: turning off simplification to support unsat-cores"
1392                << endl;
1393       options::simplificationMode.set(SIMPLIFICATION_MODE_NONE);
1394     }
1395
1396     if(options::unconstrainedSimp()) {
1397       if(options::unconstrainedSimp.wasSetByUser()) {
1398         throw OptionException("unconstrained simplification not supported with unsat cores");
1399       }
1400       Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl;
1401       options::unconstrainedSimp.set(false);
1402     }
1403
1404     if(options::pbRewrites()) {
1405       if(options::pbRewrites.wasSetByUser()) {
1406         throw OptionException("pseudoboolean rewrites not supported with unsat cores");
1407       }
1408       Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl;
1409       setOption("pb-rewrites", false);
1410     }
1411
1412     if(options::sortInference()) {
1413       if(options::sortInference.wasSetByUser()) {
1414         throw OptionException("sort inference not supported with unsat cores");
1415       }
1416       Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl;
1417       options::sortInference.set(false);
1418     }
1419
1420     if(options::preSkolemQuant()) {
1421       if(options::preSkolemQuant.wasSetByUser()) {
1422         throw OptionException("pre-skolemization not supported with unsat cores");
1423       }
1424       Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl;
1425       options::preSkolemQuant.set(false);
1426     }
1427
1428     if(options::bitvectorToBool()) {
1429       if(options::bitvectorToBool.wasSetByUser()) {
1430         throw OptionException("bv-to-bool not supported with unsat cores");
1431       }
1432       Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat-cores" << endl;
1433       options::bitvectorToBool.set(false);
1434     }
1435
1436     if(options::boolToBitvector()) {
1437       if(options::boolToBitvector.wasSetByUser()) {
1438         throw OptionException("bool-to-bv not supported with unsat cores");
1439       }
1440       Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat-cores" << endl;
1441       options::boolToBitvector.set(false);
1442     }
1443
1444     if(options::bvIntroducePow2()) {
1445       if(options::bvIntroducePow2.wasSetByUser()) {
1446         throw OptionException("bv-intro-pow2 not supported with unsat cores");
1447       }
1448       Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat-cores" << endl;
1449       setOption("bv-intro-pow2", false);
1450     }
1451
1452     if(options::repeatSimp()) {
1453       if(options::repeatSimp.wasSetByUser()) {
1454         throw OptionException("repeat-simp not supported with unsat cores");
1455       }
1456       Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl;
1457       setOption("repeat-simp", false);
1458     }
1459
1460     if (options::globalNegate())
1461     {
1462       if (options::globalNegate.wasSetByUser())
1463       {
1464         throw OptionException("global-negate not supported with unsat cores");
1465       }
1466       Notice() << "SmtEngine: turning off global-negate to support unsat-cores"
1467                << endl;
1468       setOption("global-negate", false);
1469     }
1470   }
1471
1472   if (options::cbqiBv() && d_logic.isQuantified())
1473   {
1474     if(options::boolToBitvector.wasSetByUser()) {
1475       throw OptionException(
1476           "bool-to-bv not supported with CBQI BV for quantified logics");
1477     }
1478     Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
1479              << endl;
1480     options::boolToBitvector.set(false);
1481   }
1482
1483   // cases where we need produce models
1484   if (!options::produceModels()
1485       && (options::produceAssignments() || options::sygusRewSynthCheck()))
1486   {
1487     Notice() << "SmtEngine: turning on produce-models" << endl;
1488     setOption("produce-models", SExpr("true"));
1489   }
1490
1491   // Set the options for the theoryOf
1492   if(!options::theoryOfMode.wasSetByUser()) {
1493     if(d_logic.isSharingEnabled() &&
1494        !d_logic.isTheoryEnabled(THEORY_BV) &&
1495        !d_logic.isTheoryEnabled(THEORY_STRINGS) &&
1496        !d_logic.isTheoryEnabled(THEORY_SETS) ) {
1497       Trace("smt") << "setting theoryof-mode to term-based" << endl;
1498       options::theoryOfMode.set(THEORY_OF_TERM_BASED);
1499     }
1500   }
1501
1502   // strings require LIA, UF; widen the logic
1503   if(d_logic.isTheoryEnabled(THEORY_STRINGS)) {
1504     LogicInfo log(d_logic.getUnlockedCopy());
1505     // Strings requires arith for length constraints, and also UF
1506     if(!d_logic.isTheoryEnabled(THEORY_UF)) {
1507       Trace("smt") << "because strings are enabled, also enabling UF" << endl;
1508       log.enableTheory(THEORY_UF);
1509     }
1510     if(!d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isDifferenceLogic() || !d_logic.areIntegersUsed()) {
1511       Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl;
1512       log.enableTheory(THEORY_ARITH);
1513       log.enableIntegers();
1514       log.arithOnlyLinear();
1515     }
1516     d_logic = log;
1517     d_logic.lock();
1518   }
1519   if(d_logic.isTheoryEnabled(THEORY_ARRAYS) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
1520     if(!d_logic.isTheoryEnabled(THEORY_UF)) {
1521       LogicInfo log(d_logic.getUnlockedCopy());
1522       Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl;
1523       log.enableTheory(THEORY_UF);
1524       d_logic = log;
1525       d_logic.lock();
1526     }
1527   }
1528
1529   // by default, symmetry breaker is on only for QF_UF
1530   if(! options::ufSymmetryBreaker.wasSetByUser()) {
1531     bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified() && !options::proof();
1532     Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
1533     options::ufSymmetryBreaker.set(qf_uf);
1534   }
1535   // by default, nonclausal simplification is off for QF_SAT
1536   if(! options::simplificationMode.wasSetByUser()) {
1537     bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
1538     Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << endl;
1539     //simplification=none works better for SMT LIB benchmarks with quantifiers, not others
1540     //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
1541     options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
1542   }
1543
1544   // If in arrays, set the UF handler to arrays
1545   if(d_logic.isTheoryEnabled(THEORY_ARRAYS) && ( !d_logic.isQuantified() ||
1546      (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) {
1547     Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
1548   } else {
1549     Theory::setUninterpretedSortOwner(THEORY_UF);
1550   }
1551
1552   // Turn on ite simplification for QF_LIA and QF_AUFBV
1553   // WARNING: These checks match much more than just QF_AUFBV and
1554   // QF_LIA logics. --K [2014/10/15]
1555   if(! options::doITESimp.wasSetByUser()) {
1556     bool qf_aufbv = !d_logic.isQuantified() &&
1557       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1558       d_logic.isTheoryEnabled(THEORY_UF) &&
1559       d_logic.isTheoryEnabled(THEORY_BV);
1560     bool qf_lia = !d_logic.isQuantified() &&
1561       d_logic.isPure(THEORY_ARITH) &&
1562       d_logic.isLinear() &&
1563       !d_logic.isDifferenceLogic() &&
1564       !d_logic.areRealsUsed();
1565
1566     bool iteSimp = (qf_aufbv || qf_lia);
1567     Trace("smt") << "setting ite simplification to " << iteSimp << endl;
1568     options::doITESimp.set(iteSimp);
1569   }
1570   if(! options::compressItes.wasSetByUser() ){
1571     bool qf_lia = !d_logic.isQuantified() &&
1572       d_logic.isPure(THEORY_ARITH) &&
1573       d_logic.isLinear() &&
1574       !d_logic.isDifferenceLogic() &&
1575       !d_logic.areRealsUsed();
1576
1577     bool compressIte = qf_lia;
1578     Trace("smt") << "setting ite compression to " << compressIte << endl;
1579     options::compressItes.set(compressIte);
1580   }
1581   if(! options::simplifyWithCareEnabled.wasSetByUser() ){
1582     bool qf_aufbv = !d_logic.isQuantified() &&
1583       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1584       d_logic.isTheoryEnabled(THEORY_UF) &&
1585       d_logic.isTheoryEnabled(THEORY_BV);
1586
1587     bool withCare = qf_aufbv;
1588     Trace("smt") << "setting ite simplify with care to " << withCare << endl;
1589     options::simplifyWithCareEnabled.set(withCare);
1590   }
1591   // Turn off array eager index splitting for QF_AUFLIA
1592   if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
1593     if (not d_logic.isQuantified() &&
1594         d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1595         d_logic.isTheoryEnabled(THEORY_UF) &&
1596         d_logic.isTheoryEnabled(THEORY_ARITH)) {
1597       Trace("smt") << "setting array eager index splitting to false" << endl;
1598       options::arraysEagerIndexSplitting.set(false);
1599     }
1600   }
1601   // Turn on model-based arrays for QF_AX (unless models are enabled)
1602   // if(! options::arraysModelBased.wasSetByUser()) {
1603   //   if (not d_logic.isQuantified() &&
1604   //       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1605   //       d_logic.isPure(THEORY_ARRAYS) &&
1606   //       !options::produceModels() &&
1607   //       !options::checkModels()) {
1608   //     Trace("smt") << "turning on model-based array solver" << endl;
1609   //     options::arraysModelBased.set(true);
1610   //   }
1611   // }
1612   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
1613   if(! options::repeatSimp.wasSetByUser()) {
1614     bool repeatSimp = !d_logic.isQuantified() &&
1615                       (d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1616                       d_logic.isTheoryEnabled(THEORY_UF) &&
1617                       d_logic.isTheoryEnabled(THEORY_BV)) &&
1618                       !options::unsatCores();
1619     Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
1620     options::repeatSimp.set(repeatSimp);
1621   }
1622   // Turn on unconstrained simplification for QF_AUFBV
1623   if(!options::unconstrainedSimp.wasSetByUser() ||
1624       options::incrementalSolving()) {
1625     //    bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
1626     //    bool uncSimp = false && !qf_sat && !options::incrementalSolving();
1627     bool uncSimp = !options::incrementalSolving() &&
1628                    !d_logic.isQuantified() &&
1629                    !options::produceModels() &&
1630                    !options::produceAssignments() &&
1631                    !options::checkModels() &&
1632                    !options::unsatCores() &&
1633                    (d_logic.isTheoryEnabled(THEORY_ARRAYS) && d_logic.isTheoryEnabled(THEORY_BV));
1634     Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl;
1635     options::unconstrainedSimp.set(uncSimp);
1636   }
1637   // Unconstrained simp currently does *not* support model generation
1638   if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) {
1639     if (options::produceModels()) {
1640       if (options::produceModels.wasSetByUser()) {
1641         throw OptionException("Cannot use unconstrained-simp with model generation.");
1642       }
1643       Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl;
1644       setOption("produce-models", SExpr("false"));
1645     }
1646     if (options::produceAssignments()) {
1647       if (options::produceAssignments.wasSetByUser()) {
1648         throw OptionException("Cannot use unconstrained-simp with model generation (produce-assignments).");
1649       }
1650       Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl;
1651       setOption("produce-assignments", SExpr("false"));
1652     }
1653     if (options::checkModels()) {
1654       if (options::checkModels.wasSetByUser()) {
1655         throw OptionException("Cannot use unconstrained-simp with model generation (check-models).");
1656       }
1657       Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl;
1658       setOption("check-models", SExpr("false"));
1659     }
1660   }
1661
1662
1663   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
1664       options::incrementalSolving()) {
1665     if (options::incrementalSolving.wasSetByUser()) {
1666       throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
1667                                          Try --bitblast=lazy"));
1668     }
1669     Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl;
1670     setOption("incremental", SExpr("false"));
1671   }
1672
1673   if (! options::bvEagerExplanations.wasSetByUser() &&
1674       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1675       d_logic.isTheoryEnabled(THEORY_BV)) {
1676     Trace("smt") << "enabling eager bit-vector explanations " << endl;
1677     options::bvEagerExplanations.set(true);
1678   }
1679
1680   if( !options::bitvectorEqualitySolver() ){
1681     Trace("smt") << "disabling bvLazyRewriteExtf since equality solver is disabled" << endl;
1682     options::bvLazyRewriteExtf.set(false);
1683   }
1684
1685   // Turn on arith rewrite equalities only for pure arithmetic
1686   if(! options::arithRewriteEq.wasSetByUser()) {
1687     bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isQuantified();
1688     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << endl;
1689     options::arithRewriteEq.set(arithRewriteEq);
1690   }
1691   if(!  options::arithHeuristicPivots.wasSetByUser()) {
1692     int16_t heuristicPivots = 5;
1693     if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()) {
1694       if(d_logic.isDifferenceLogic()) {
1695         heuristicPivots = -1;
1696       } else if(!d_logic.areIntegersUsed()) {
1697         heuristicPivots = 0;
1698       }
1699     }
1700     Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots << endl;
1701     options::arithHeuristicPivots.set(heuristicPivots);
1702   }
1703   if(! options::arithPivotThreshold.wasSetByUser()){
1704     uint16_t pivotThreshold = 2;
1705     if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
1706       if(d_logic.isDifferenceLogic()){
1707         pivotThreshold = 16;
1708       }
1709     }
1710     Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold << endl;
1711     options::arithPivotThreshold.set(pivotThreshold);
1712   }
1713   if(! options::arithStandardCheckVarOrderPivots.wasSetByUser()){
1714     int16_t varOrderPivots = -1;
1715     if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
1716       varOrderPivots = 200;
1717     }
1718     Trace("smt") << "setting arithStandardCheckVarOrderPivots  " << varOrderPivots << endl;
1719     options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
1720   }
1721   // Turn off early theory preprocessing if arithRewriteEq is on
1722   if (options::arithRewriteEq()) {
1723     d_earlyTheoryPP = false;
1724   }
1725
1726   // Set decision mode based on logic (if not set by user)
1727   if(!options::decisionMode.wasSetByUser()) {
1728     decision::DecisionMode decMode =
1729       // ALL
1730       d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION :
1731       ( // QF_BV
1732         (not d_logic.isQuantified() &&
1733           d_logic.isPure(THEORY_BV)
1734           ) ||
1735         // QF_AUFBV or QF_ABV or QF_UFBV
1736         (not d_logic.isQuantified() &&
1737          (d_logic.isTheoryEnabled(THEORY_ARRAYS) ||
1738           d_logic.isTheoryEnabled(THEORY_UF)) &&
1739          d_logic.isTheoryEnabled(THEORY_BV)
1740          ) ||
1741         // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
1742         (not d_logic.isQuantified() &&
1743          d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1744          d_logic.isTheoryEnabled(THEORY_UF) &&
1745          d_logic.isTheoryEnabled(THEORY_ARITH)
1746          ) ||
1747         // QF_LRA
1748         (not d_logic.isQuantified() &&
1749          d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
1750          ) ||
1751         // Quantifiers
1752         d_logic.isQuantified() ||
1753         // Strings
1754         d_logic.isTheoryEnabled(THEORY_STRINGS)
1755         ? decision::DECISION_STRATEGY_JUSTIFICATION
1756         : decision::DECISION_STRATEGY_INTERNAL
1757       );
1758
1759     bool stoponly =
1760       // ALL
1761       d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
1762       ( // QF_AUFLIA
1763         (not d_logic.isQuantified() &&
1764          d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
1765          d_logic.isTheoryEnabled(THEORY_UF) &&
1766          d_logic.isTheoryEnabled(THEORY_ARITH)
1767          ) ||
1768         // QF_LRA
1769         (not d_logic.isQuantified() &&
1770          d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
1771          )
1772         ? true : false
1773       );
1774
1775     Trace("smt") << "setting decision mode to " << decMode << endl;
1776     options::decisionMode.set(decMode);
1777     options::decisionStopOnly.set(stoponly);
1778   }
1779   if( options::incrementalSolving() ){
1780     //disable modes not supported by incremental
1781     options::sortInference.set( false );
1782     options::ufssFairnessMonotone.set( false );
1783     options::quantEpr.set( false );
1784     options::globalNegate.set(false);
1785   }
1786   if( d_logic.hasCardinalityConstraints() ){
1787     //must have finite model finding on
1788     options::finiteModelFind.set( true );
1789   }
1790
1791   //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
1792   if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){
1793     if( !options::instWhenStrictInterleave.wasSetByUser() ){
1794       options::instWhenStrictInterleave.set( false );
1795     }
1796   }
1797
1798   //local theory extensions
1799   if( options::localTheoryExt() ){
1800     if( !options::instMaxLevel.wasSetByUser() ){
1801       options::instMaxLevel.set( 0 );
1802     }
1803   }
1804   if( options::instMaxLevel()!=-1 ){
1805     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
1806     options::cbqi.set(false);
1807   }
1808   //track instantiations?
1809   if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas.wasSetByUser() ) ){
1810     options::trackInstLemmas.set( true );
1811   }
1812
1813   if( ( options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy() ) ||
1814       ( options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt() ) ) {
1815     options::fmfBound.set( true );
1816   }
1817   //now have determined whether fmfBoundInt is on/off
1818   //apply fmfBoundInt options
1819   if( options::fmfBound() ){
1820     //must have finite model finding on
1821     options::finiteModelFind.set( true );
1822     if( ! options::mbqiMode.wasSetByUser() ||
1823         ( options::mbqiMode()!=quantifiers::MBQI_NONE &&
1824           options::mbqiMode()!=quantifiers::MBQI_FMC &&
1825           options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ) ){
1826       //if bounded integers are set, use no MBQI by default
1827       options::mbqiMode.set( quantifiers::MBQI_NONE );
1828     }
1829     if( ! options::prenexQuant.wasSetByUser() ){
1830       options::prenexQuant.set( quantifiers::PRENEX_QUANT_NONE );
1831     }
1832   }
1833   if( options::ufHo() ){
1834     //if higher-order, then current variants of model-based instantiation cannot be used
1835     if( options::mbqiMode()!=quantifiers::MBQI_NONE ){
1836       options::mbqiMode.set( quantifiers::MBQI_NONE );
1837     }
1838   }
1839   if( options::mbqiMode()==quantifiers::MBQI_ABS ){
1840     if( !d_logic.isPure(THEORY_UF) ){
1841       //MBQI_ABS is only supported in pure quantified UF
1842       options::mbqiMode.set( quantifiers::MBQI_FMC );
1843     }
1844   }
1845   if( options::ufssSymBreak() ){
1846     options::sortInference.set( true );
1847   }
1848   if( options::fmfFunWellDefinedRelevant() ){
1849     if( !options::fmfFunWellDefined.wasSetByUser() ){
1850       options::fmfFunWellDefined.set( true );
1851     }
1852   }
1853   if( options::fmfFunWellDefined() ){
1854     if( !options::finiteModelFind.wasSetByUser() ){
1855       options::finiteModelFind.set( true );
1856     }
1857   }
1858   //EPR
1859   if( options::quantEpr() ){
1860     if( !options::preSkolemQuant.wasSetByUser() ){
1861       options::preSkolemQuant.set( true );
1862     }
1863   }
1864
1865   //now, have determined whether finite model find is on/off
1866   //apply finite model finding options
1867   if( options::finiteModelFind() ){
1868     //apply conservative quantifiers splitting
1869     if( !options::quantDynamicSplit.wasSetByUser() ){
1870       options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_DEFAULT );
1871     }
1872     //do not eliminate extended arithmetic symbols from quantified formulas
1873     if( !options::elimExtArithQuant.wasSetByUser() ){
1874       options::elimExtArithQuant.set( false );
1875     }
1876     if( !options::eMatching.wasSetByUser() ){
1877       options::eMatching.set( options::fmfInstEngine() );
1878     }
1879     if( !options::instWhenMode.wasSetByUser() ){
1880       //instantiate only on last call
1881       if( options::eMatching() ){
1882         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
1883       }
1884     }
1885     if( options::mbqiMode()==quantifiers::MBQI_ABS ){
1886       if( !options::preSkolemQuant.wasSetByUser() ){
1887         options::preSkolemQuant.set( true );
1888       }
1889       if( !options::preSkolemQuantNested.wasSetByUser() ){
1890         options::preSkolemQuantNested.set( true );
1891       }
1892       if( !options::fmfOneInstPerRound.wasSetByUser() ){
1893         options::fmfOneInstPerRound.set( true );
1894       }
1895     }
1896   }
1897
1898   //apply counterexample guided instantiation options
1899   // if we are attempting to rewrite everything to SyGuS, use ceGuidedInst
1900   if (options::sygusInference())
1901   {
1902     if (!options::ceGuidedInst.wasSetByUser())
1903     {
1904       options::ceGuidedInst.set(true);
1905     }
1906     // optimization: apply preskolemization, makes it succeed more often
1907     if (!options::preSkolemQuant.wasSetByUser())
1908     {
1909       options::preSkolemQuant.set(true);
1910     }
1911     if (!options::preSkolemQuantNested.wasSetByUser())
1912     {
1913       options::preSkolemQuantNested.set(true);
1914     }
1915   }
1916   if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){
1917     if( !options::ceGuidedInst.wasSetByUser() ){
1918       options::ceGuidedInst.set( true );
1919     }
1920   }
1921   if( options::ceGuidedInst() ){
1922     //counterexample-guided instantiation for sygus
1923     if( !options::cegqiSingleInvMode.wasSetByUser() ){
1924       options::cegqiSingleInvMode.set( quantifiers::CEGQI_SI_MODE_USE );
1925     }
1926     if( !options::quantConflictFind.wasSetByUser() ){
1927       options::quantConflictFind.set( false );
1928     }
1929     if( !options::instNoEntail.wasSetByUser() ){
1930       options::instNoEntail.set( false );
1931     }
1932     if (options::sygusRew())
1933     {
1934       options::sygusRewSynth.set(true);
1935       options::sygusRewVerify.set(true);
1936     }
1937     if (options::sygusRewSynth() || options::sygusRewVerify())
1938     {
1939       // rewrite rule synthesis implies that sygus stream must be true
1940       options::sygusStream.set(true);
1941     }
1942     if (options::sygusStream())
1943     {
1944       // PBE and streaming modes are incompatible
1945       if (!options::sygusPbe.wasSetByUser())
1946       {
1947         options::sygusPbe.set(false);
1948       }
1949     }
1950     //do not allow partial functions
1951     if( !options::bitvectorDivByZeroConst.wasSetByUser() ){
1952       options::bitvectorDivByZeroConst.set( true );
1953     }
1954     if( !options::dtRewriteErrorSel.wasSetByUser() ){
1955       options::dtRewriteErrorSel.set( true );
1956     }
1957     //do not miniscope
1958     if( !options::miniscopeQuant.wasSetByUser() ){
1959       options::miniscopeQuant.set( false );
1960     }
1961     if( !options::miniscopeQuantFreeVar.wasSetByUser() ){
1962       options::miniscopeQuantFreeVar.set( false );
1963     }
1964     //rewrite divk
1965     if( !options::rewriteDivk.wasSetByUser()) {
1966       options::rewriteDivk.set( true );
1967     }
1968     //do not do macros
1969     if( !options::macrosQuant.wasSetByUser()) {
1970       options::macrosQuant.set( false );
1971     }
1972     if( !options::cbqiPreRegInst.wasSetByUser()) {
1973       options::cbqiPreRegInst.set( true );
1974     }
1975   }
1976   //counterexample-guided instantiation for non-sygus
1977   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
1978   if( d_logic.isQuantified() &&
1979       ( ( options::decisionMode()!=decision::DECISION_STRATEGY_INTERNAL &&
1980           ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
1981         d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV) ||
1982         options::cbqiAll() ) ){
1983     if( !options::cbqi.wasSetByUser() ){
1984       options::cbqi.set( true );
1985     }
1986     // check whether we should apply full cbqi
1987     if (d_logic.isPure(THEORY_BV))
1988     {
1989       if (!options::cbqiFullEffort.wasSetByUser())
1990       {
1991         options::cbqiFullEffort.set(true);
1992       }
1993     }
1994   }
1995   if( options::cbqi() ){
1996     //must rewrite divk
1997     if( !options::rewriteDivk.wasSetByUser()) {
1998       options::rewriteDivk.set( true );
1999     }
2000     if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
2001     {
2002       options::cbqiAll.set( false );
2003       if( !options::quantConflictFind.wasSetByUser() ){
2004         options::quantConflictFind.set( false );
2005       }
2006       if( !options::instNoEntail.wasSetByUser() ){
2007         options::instNoEntail.set( false );
2008       }
2009       if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){
2010         //only instantiation should happen at last call when model is avaiable
2011         options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
2012       }
2013     }else{
2014       // only supported in pure arithmetic or pure BV
2015       options::cbqiNestedQE.set(false);
2016     }
2017     // prenexing
2018     if (options::cbqiNestedQE()
2019         || options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL)
2020     {
2021       // only complete with prenex = disj_normal or normal
2022       if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL)
2023       {
2024         options::prenexQuant.set(quantifiers::PRENEX_QUANT_DISJ_NORMAL);
2025       }
2026     }
2027     else if (options::globalNegate())
2028     {
2029       if (!options::prenexQuant.wasSetByUser())
2030       {
2031         options::prenexQuant.set(quantifiers::PRENEX_QUANT_NONE);
2032       }
2033     }
2034   }
2035   //implied options...
2036   if( options::strictTriggers() ){
2037     if( !options::userPatternsQuant.wasSetByUser() ){
2038       options::userPatternsQuant.set( quantifiers::USER_PAT_MODE_TRUST );
2039     }
2040   }
2041   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
2042     options::quantConflictFind.set( true );
2043   }
2044   if( options::cbqiNestedQE() ){
2045     options::prenexQuantUser.set( true );
2046     if( !options::preSkolemQuant.wasSetByUser() ){
2047       options::preSkolemQuant.set( true );
2048     }
2049   }
2050   //for induction techniques
2051   if( options::quantInduction() ){
2052     if( !options::dtStcInduction.wasSetByUser() ){
2053       options::dtStcInduction.set( true );
2054     }
2055     if( !options::intWfInduction.wasSetByUser() ){
2056       options::intWfInduction.set( true );
2057     }
2058   }
2059   if( options::dtStcInduction() ){
2060     //leads to unfairness FIXME
2061     if( !options::dtForceAssignment.wasSetByUser() ){
2062       options::dtForceAssignment.set( true );
2063     }
2064     //try to remove ITEs from quantified formulas
2065     if( !options::iteDtTesterSplitQuant.wasSetByUser() ){
2066       options::iteDtTesterSplitQuant.set( true );
2067     }
2068     if( !options::iteLiftQuant.wasSetByUser() ){
2069       options::iteLiftQuant.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL );
2070     }
2071   }
2072   if( options::intWfInduction() ){
2073     if( !options::purifyTriggers.wasSetByUser() ){
2074       options::purifyTriggers.set( true );
2075     }
2076   }
2077   if( options::conjectureNoFilter() ){
2078     if( !options::conjectureFilterActiveTerms.wasSetByUser() ){
2079       options::conjectureFilterActiveTerms.set( false );
2080     }
2081     if( !options::conjectureFilterCanonical.wasSetByUser() ){
2082       options::conjectureFilterCanonical.set( false );
2083     }
2084     if( !options::conjectureFilterModel.wasSetByUser() ){
2085       options::conjectureFilterModel.set( false );
2086     }
2087   }
2088   if( options::conjectureGenPerRound.wasSetByUser() ){
2089     if( options::conjectureGenPerRound()>0 ){
2090       options::conjectureGen.set( true );
2091     }else{
2092       options::conjectureGen.set( false );
2093     }
2094   }
2095   //can't pre-skolemize nested quantifiers without UF theory
2096   if( !d_logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant() ){
2097     if( !options::preSkolemQuantNested.wasSetByUser() ){
2098       options::preSkolemQuantNested.set( false );
2099     }
2100   }
2101   if( !d_logic.isTheoryEnabled(THEORY_DATATYPES) ){
2102     options::quantDynamicSplit.set( quantifiers::QUANT_DSPLIT_MODE_NONE );
2103   }
2104
2105   //until bugs 371,431 are fixed
2106   if( ! options::minisatUseElim.wasSetByUser()){
2107     //AJR: cannot use minisat elim for new implementation of sets TODO: why?
2108     if( d_logic.isTheoryEnabled(THEORY_SETS) || d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){
2109       options::minisatUseElim.set( false );
2110     }
2111   }
2112   else if (options::minisatUseElim()) {
2113     if (options::produceModels()) {
2114       Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl;
2115       setOption("produce-models", SExpr("false"));
2116     }
2117     if (options::produceAssignments()) {
2118       Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl;
2119       setOption("produce-assignments", SExpr("false"));
2120     }
2121     if (options::checkModels()) {
2122       Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl;
2123       setOption("check-models", SExpr("false"));
2124     }
2125   }
2126
2127   // For now, these array theory optimizations do not support model-building
2128   if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
2129     options::arraysOptimizeLinear.set(false);
2130     options::arraysLazyRIntro1.set(false);
2131   }
2132
2133   // Non-linear arithmetic does not support models unless nlExt is enabled
2134   if ((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()
2135        && !options::nlExt())
2136       || options::globalNegate())
2137   {
2138     std::string reason =
2139         options::globalNegate() ? "--global-negate" : "nonlinear arithmetic";
2140     if (options::produceModels()) {
2141       if(options::produceModels.wasSetByUser()) {
2142         throw OptionException(
2143             std::string("produce-model not supported with " + reason));
2144       }
2145       Warning()
2146           << "SmtEngine: turning off produce-models because unsupported for "
2147           << reason << endl;
2148       setOption("produce-models", SExpr("false"));
2149     }
2150     if (options::produceAssignments()) {
2151       if(options::produceAssignments.wasSetByUser()) {
2152         throw OptionException(
2153             std::string("produce-assignments not supported with " + reason));
2154       }
2155       Warning() << "SmtEngine: turning off produce-assignments because "
2156                    "unsupported for "
2157                 << reason << endl;
2158       setOption("produce-assignments", SExpr("false"));
2159     }
2160     if (options::checkModels()) {
2161       if(options::checkModels.wasSetByUser()) {
2162         throw OptionException(
2163             std::string("check-models not supported with " + reason));
2164       }
2165       Warning()
2166           << "SmtEngine: turning off check-models because unsupported for "
2167           << reason << endl;
2168       setOption("check-models", SExpr("false"));
2169     }
2170   }
2171
2172   if(options::incrementalSolving() && options::proof()) {
2173     Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl;
2174     setOption("incremental", SExpr("false"));
2175   }
2176
2177   if (options::proof())
2178   {
2179     if (options::bitvectorAlgebraicSolver())
2180     {
2181       if (options::bitvectorAlgebraicSolver.wasSetByUser())
2182       {
2183         throw OptionException(
2184             "--bv-algebraic-solver is not supported with proofs");
2185       }
2186       Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
2187                << std::endl;
2188       options::bitvectorAlgebraicSolver.set(false);
2189     }
2190     if (options::bitvectorEqualitySolver())
2191     {
2192       if (options::bitvectorEqualitySolver.wasSetByUser())
2193       {
2194         throw OptionException("--bv-eq-solver is not supported with proofs");
2195       }
2196       Notice() << "SmtEngine: turning off bv eq solver to support proofs"
2197                << std::endl;
2198       options::bitvectorEqualitySolver.set(false);
2199     }
2200     if (options::bitvectorInequalitySolver())
2201     {
2202       if (options::bitvectorInequalitySolver.wasSetByUser())
2203       {
2204         throw OptionException(
2205             "--bv-inequality-solver is not supported with proofs");
2206       }
2207       Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
2208                << std::endl;
2209       options::bitvectorInequalitySolver.set(false);
2210     }
2211   }
2212 }
2213
2214 void SmtEngine::setProblemExtended(bool value)
2215 {
2216   d_problemExtended = value;
2217   if (value) { d_assumptions.clear(); }
2218 }
2219
2220 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
2221 {
2222   SmtScope smts(this);
2223
2224   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
2225
2226   if(Dump.isOn("benchmark")) {
2227     if(key == "status") {
2228       string s = value.getValue();
2229       BenchmarkStatus status =
2230         (s == "sat") ? SMT_SATISFIABLE :
2231           ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN);
2232       Dump("benchmark") << SetBenchmarkStatusCommand(status);
2233     } else {
2234       Dump("benchmark") << SetInfoCommand(key, value);
2235     }
2236   }
2237
2238   // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_")
2239   if(key.length() > 5) {
2240     string prefix = key.substr(0, 5);
2241     if(prefix == "cvc4-" || prefix == "cvc4_") {
2242       string cvc4key = key.substr(5);
2243       if(cvc4key == "logic") {
2244         if(! value.isAtom()) {
2245           throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
2246         }
2247         SmtScope smts(this);
2248         d_logic = value.getValue();
2249         setLogicInternal();
2250         return;
2251       } else {
2252         throw UnrecognizedOptionException();
2253       }
2254     }
2255   }
2256
2257   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
2258   if(key == "source" ||
2259      key == "category" ||
2260      key == "difficulty" ||
2261      key == "notes") {
2262     // ignore these
2263     return;
2264   } else if(key == "name") {
2265     d_filename = value.getValue();
2266     return;
2267   } else if(key == "smt-lib-version") {
2268     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
2269         (value.isRational() && value.getRationalValue() == Rational(2)) ||
2270         value.getValue() == "2" ||
2271         value.getValue() == "2.0" ) {
2272       options::inputLanguage.set(language::input::LANG_SMTLIB_V2_0);
2273
2274       // supported SMT-LIB version
2275       if(!options::outputLanguage.wasSetByUser() &&
2276          ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5 || options::outputLanguage() == language::output::LANG_SMTLIB_V2_6 )) {
2277         options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
2278         *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0);
2279       }
2280       return;
2281     } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
2282                value.getValue() == "2.5" ) {
2283       options::inputLanguage.set(language::input::LANG_SMTLIB_V2_5);
2284
2285       // supported SMT-LIB version
2286       if(!options::outputLanguage.wasSetByUser() &&
2287          options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
2288         options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
2289         *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
2290       }
2291       return;
2292     } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) ||
2293                value.getValue() == "2.6" ) {
2294       options::inputLanguage.set(language::input::LANG_SMTLIB_V2_6);
2295
2296       // supported SMT-LIB version
2297       if(!options::outputLanguage.wasSetByUser() &&
2298          options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
2299         options::outputLanguage.set(language::output::LANG_SMTLIB_V2_6);
2300         *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_6);
2301       }
2302       return;
2303     }
2304     Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
2305     throw UnrecognizedOptionException();
2306   } else if(key == "status") {
2307     string s;
2308     if(value.isAtom()) {
2309       s = value.getValue();
2310     }
2311     if(s != "sat" && s != "unsat" && s != "unknown") {
2312       throw OptionException("argument to (set-info :status ..) must be "
2313                             "`sat' or `unsat' or `unknown'");
2314     }
2315     d_status = Result(s, d_filename);
2316     return;
2317   }
2318   throw UnrecognizedOptionException();
2319 }
2320
2321 CVC4::SExpr SmtEngine::getInfo(const std::string& key) const {
2322
2323   SmtScope smts(this);
2324
2325   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
2326   if(key == "all-statistics") {
2327     vector<SExpr> stats;
2328     for(StatisticsRegistry::const_iterator i = NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->begin();
2329         i != NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->end();
2330         ++i) {
2331       vector<SExpr> v;
2332       v.push_back((*i).first);
2333       v.push_back((*i).second);
2334       stats.push_back(v);
2335     }
2336     for(StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin();
2337         i != d_statisticsRegistry->end();
2338         ++i) {
2339       vector<SExpr> v;
2340       v.push_back((*i).first);
2341       v.push_back((*i).second);
2342       stats.push_back(v);
2343     }
2344     return SExpr(stats);
2345   } else if(key == "error-behavior") {
2346     // immediate-exit | continued-execution
2347     if( options::continuedExecution() || options::interactive() ) {
2348       return SExpr(SExpr::Keyword("continued-execution"));
2349     } else {
2350       return SExpr(SExpr::Keyword("immediate-exit"));
2351     }
2352   } else if(key == "name") {
2353     return SExpr(Configuration::getName());
2354   } else if(key == "version") {
2355     return SExpr(Configuration::getVersionString());
2356   } else if(key == "authors") {
2357     return SExpr(Configuration::about());
2358   } else if(key == "status") {
2359     // sat | unsat | unknown
2360     switch(d_status.asSatisfiabilityResult().isSat()) {
2361     case Result::SAT:
2362       return SExpr(SExpr::Keyword("sat"));
2363     case Result::UNSAT:
2364       return SExpr(SExpr::Keyword("unsat"));
2365     default:
2366       return SExpr(SExpr::Keyword("unknown"));
2367     }
2368   } else if(key == "reason-unknown") {
2369     if(!d_status.isNull() && d_status.isUnknown()) {
2370       stringstream ss;
2371       ss << d_status.whyUnknown();
2372       string s = ss.str();
2373       transform(s.begin(), s.end(), s.begin(), ::tolower);
2374       return SExpr(SExpr::Keyword(s));
2375     } else {
2376       throw ModalException("Can't get-info :reason-unknown when the "
2377                            "last result wasn't unknown!");
2378     }
2379   } else if(key == "assertion-stack-levels") {
2380     AlwaysAssert(d_userLevels.size() <=
2381                  std::numeric_limits<unsigned long int>::max());
2382     return SExpr(static_cast<unsigned long int>(d_userLevels.size()));
2383   } else if(key == "all-options") {
2384     // get the options, like all-statistics
2385     std::vector< std::vector<std::string> > current_options =
2386       Options::current()->getOptions();
2387     return SExpr::parseListOfListOfAtoms(current_options);
2388   } else {
2389     throw UnrecognizedOptionException();
2390   }
2391 }
2392
2393 void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func)
2394 {
2395   for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
2396     if((*i).getKind() != kind::BOUND_VARIABLE) {
2397       stringstream ss;
2398       ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
2399          << "definition of function " << func << ", formal\n"
2400          << "  " << *i << "\n"
2401          << "has kind " << (*i).getKind();
2402       throw TypeCheckingException(func, ss.str());
2403     }
2404   }
2405 }
2406
2407 void SmtEngine::debugCheckFunctionBody(Expr formula,
2408                                        const std::vector<Expr>& formals,
2409                                        Expr func)
2410 {
2411   Type formulaType = formula.getType(options::typeChecking());
2412   Type funcType = func.getType();
2413   // We distinguish here between definitions of constants and functions,
2414   // because the type checking for them is subtly different.  Perhaps we
2415   // should instead have SmtEngine::defineFunction() and
2416   // SmtEngine::defineConstant() for better clarity, although then that
2417   // doesn't match the SMT-LIBv2 standard...
2418   if(formals.size() > 0) {
2419     Type rangeType = FunctionType(funcType).getRangeType();
2420     if(! formulaType.isComparableTo(rangeType)) {
2421       stringstream ss;
2422       ss << "Type of defined function does not match its declaration\n"
2423          << "The function  : " << func << "\n"
2424          << "Declared type : " << rangeType << "\n"
2425          << "The body      : " << formula << "\n"
2426          << "Body type     : " << formulaType;
2427       throw TypeCheckingException(func, ss.str());
2428     }
2429   } else {
2430     if(! formulaType.isComparableTo(funcType)) {
2431       stringstream ss;
2432       ss << "Declared type of defined constant does not match its definition\n"
2433          << "The constant   : " << func << "\n"
2434          << "Declared type  : " << funcType << " " << Type::getTypeNode(funcType)->getId() << "\n"
2435          << "The definition : " << formula << "\n"
2436          << "Definition type: " << formulaType << " " << Type::getTypeNode(formulaType)->getId();
2437       throw TypeCheckingException(func, ss.str());
2438     }
2439   }
2440 }
2441
2442 void SmtEngine::defineFunction(Expr func,
2443                                const std::vector<Expr>& formals,
2444                                Expr formula)
2445 {
2446   SmtScope smts(this);
2447   doPendingPops();
2448   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
2449   debugCheckFormals(formals, func);
2450
2451   stringstream ss;
2452   ss << language::SetLanguage(
2453             language::SetLanguage::getLanguage(Dump.getStream()))
2454      << func;
2455   DefineFunctionCommand c(ss.str(), func, formals, formula);
2456   addToModelCommandAndDump(
2457       c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
2458
2459   PROOF(if (options::checkUnsatCores()) {
2460     d_defineCommands.push_back(c.clone());
2461   });
2462
2463   // type check body
2464   debugCheckFunctionBody(formula, formals, func);
2465
2466   // Substitute out any abstract values in formula
2467   Expr form =
2468       d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
2469
2470   TNode funcNode = func.getTNode();
2471   vector<Node> formalsNodes;
2472   for(vector<Expr>::const_iterator i = formals.begin(),
2473         iend = formals.end();
2474       i != iend;
2475       ++i) {
2476     formalsNodes.push_back((*i).getNode());
2477   }
2478   TNode formNode = form.getTNode();
2479   DefinedFunction def(funcNode, formalsNodes, formNode);
2480   // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
2481   // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
2482   // d_haveAdditions = true;
2483   Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << endl;
2484   d_definedFunctions->insert(funcNode, def);
2485 }
2486
2487 void SmtEngine::defineFunctionsRec(
2488     const std::vector<Expr>& funcs,
2489     const std::vector<std::vector<Expr> >& formals,
2490     const std::vector<Expr>& formulas)
2491 {
2492   SmtScope smts(this);
2493   finalOptionsAreSet();
2494   doPendingPops();
2495   Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
2496
2497   if (funcs.size() != formals.size() && funcs.size() != formulas.size())
2498   {
2499     stringstream ss;
2500     ss << "Number of functions, formals, and function bodies passed to "
2501           "defineFunctionsRec do not match:"
2502        << "\n"
2503        << "        #functions : " << funcs.size() << "\n"
2504        << "        #arg lists : " << formals.size() << "\n"
2505        << "  #function bodies : " << formulas.size() << "\n";
2506     throw ModalException(ss.str());
2507   }
2508   for (unsigned i = 0, size = funcs.size(); i < size; i++)
2509   {
2510     // check formal argument list
2511     debugCheckFormals(formals[i], funcs[i]);
2512     // type check body
2513     debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
2514   }
2515
2516   if (Dump.isOn("raw-benchmark"))
2517   {
2518     Dump("raw-benchmark") << DefineFunctionRecCommand(funcs, formals, formulas);
2519   }
2520
2521   ExprManager* em = getExprManager();
2522   for (unsigned i = 0, size = funcs.size(); i < size; i++)
2523   {
2524     // we assert a quantified formula
2525     Expr func_app;
2526     // make the function application
2527     if (formals[i].empty())
2528     {
2529       // it has no arguments
2530       func_app = funcs[i];
2531     }
2532     else
2533     {
2534       std::vector<Expr> children;
2535       children.push_back(funcs[i]);
2536       children.insert(children.end(), formals[i].begin(), formals[i].end());
2537       func_app = em->mkExpr(kind::APPLY_UF, children);
2538     }
2539     Expr lem = em->mkExpr(kind::EQUAL, func_app, formulas[i]);
2540     if (!formals[i].empty())
2541     {
2542       // set the attribute to denote this is a function definition
2543       std::string attr_name("fun-def");
2544       Expr aexpr = em->mkExpr(kind::INST_ATTRIBUTE, func_app);
2545       aexpr = em->mkExpr(kind::INST_PATTERN_LIST, aexpr);
2546       std::vector<Expr> expr_values;
2547       std::string str_value;
2548       setUserAttribute(attr_name, func_app, expr_values, str_value);
2549       // make the quantified formula
2550       Expr boundVars = em->mkExpr(kind::BOUND_VAR_LIST, formals[i]);
2551       lem = em->mkExpr(kind::FORALL, boundVars, lem, aexpr);
2552     }
2553     // assert the quantified formula
2554     //   notice we don't call assertFormula directly, since this would
2555     //   duplicate the output on raw-benchmark.
2556     Expr e = d_private->substituteAbstractValues(Node::fromExpr(lem)).toExpr();
2557     if (d_assertionList != NULL)
2558     {
2559       d_assertionList->push_back(e);
2560     }
2561     d_private->addFormula(e.getNode(), false);
2562   }
2563 }
2564
2565 void SmtEngine::defineFunctionRec(Expr func,
2566                                   const std::vector<Expr>& formals,
2567                                   Expr formula)
2568 {
2569   std::vector<Expr> funcs;
2570   funcs.push_back(func);
2571   std::vector<std::vector<Expr> > formals_multi;
2572   formals_multi.push_back(formals);
2573   std::vector<Expr> formulas;
2574   formulas.push_back(formula);
2575   defineFunctionsRec(funcs, formals_multi, formulas);
2576 }
2577
2578 bool SmtEngine::isDefinedFunction( Expr func ){
2579   Node nf = Node::fromExpr( func );
2580   Debug("smt") << "isDefined function " << nf << "?" << std::endl;
2581   return d_definedFunctions->find(nf) != d_definedFunctions->end();
2582 }
2583
2584 void SmtEnginePrivate::finishInit() {
2585   d_preprocessingPassContext.reset(new PreprocessingPassContext(&d_smt));
2586   // TODO: register passes here (this will likely change when we add support for
2587   // actually assembling preprocessing pipelines).
2588   std::unique_ptr<BVGauss> bvGauss(new BVGauss(d_preprocessingPassContext.get()));
2589   std::unique_ptr<IntToBV> intToBV(new IntToBV(d_preprocessingPassContext.get()));
2590   std::unique_ptr<PseudoBooleanProcessor> pbProc(
2591       new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
2592
2593   d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss));
2594   d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
2595   d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
2596                                            std::move(pbProc));
2597 }
2598
2599 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
2600 {
2601   stack< triple<Node, Node, bool> > worklist;
2602   stack<Node> result;
2603   worklist.push(make_triple(Node(n), Node(n), false));
2604   // The worklist is made of triples, each is input / original node then the output / rewritten node
2605   // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
2606   // or upward pass).
2607
2608   do {
2609     spendResource(options::preprocessStep());
2610     n = worklist.top().first;                      // n is the input / original
2611     Node node = worklist.top().second;             // node is the output / result
2612     bool childrenPushed = worklist.top().third;
2613     worklist.pop();
2614
2615     // Working downwards
2616     if(!childrenPushed) {
2617       Kind k = n.getKind();
2618
2619       // we can short circuit (variable) leaves
2620       if(n.isVar()) {
2621         SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
2622         if(i != d_smt.d_definedFunctions->end()) {
2623           // replacement must be closed
2624           if((*i).second.getFormals().size() > 0) {
2625             result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula()));
2626             continue;
2627           }
2628           // don't bother putting in the cache
2629           result.push((*i).second.getFormula());
2630           continue;
2631         }
2632         // don't bother putting in the cache
2633         result.push(n);
2634         continue;
2635       }
2636
2637       // maybe it's in the cache
2638       unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
2639       if(cacheHit != cache.end()) {
2640         TNode ret = (*cacheHit).second;
2641         result.push(ret.isNull() ? n : ret);
2642         continue;
2643       }
2644
2645       // otherwise expand it
2646       bool doExpand = k == kind::APPLY;
2647       if( !doExpand ){
2648         if( options::macrosQuant() ){
2649           //expand if we have inferred an operator corresponds to a defined function
2650           doExpand = k==kind::APPLY_UF && d_smt.isDefinedFunction( n.getOperator().toExpr() );
2651         }
2652       }
2653       if (doExpand) {
2654         vector<Node> formals;
2655         TNode fm;
2656         if( n.getOperator().getKind() == kind::LAMBDA ){
2657           TNode op = n.getOperator();
2658           // lambda
2659           for( unsigned i=0; i<op[0].getNumChildren(); i++ ){
2660             formals.push_back( op[0][i] );
2661           }
2662           fm = op[1];
2663         }else{
2664           // application of a user-defined symbol
2665           TNode func = n.getOperator();
2666           SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(func);
2667           if(i == d_smt.d_definedFunctions->end()) {
2668             throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
2669           }
2670           DefinedFunction def = (*i).second;
2671           formals = def.getFormals();
2672
2673           if(Debug.isOn("expand")) {
2674             Debug("expand") << "found: " << n << endl;
2675             Debug("expand") << " func: " << func << endl;
2676             string name = func.getAttribute(expr::VarNameAttr());
2677             Debug("expand") << "     : \"" << name << "\"" << endl;
2678           }
2679           if(Debug.isOn("expand")) {
2680             Debug("expand") << " defn: " << def.getFunction() << endl
2681                             << "       [";
2682             if(formals.size() > 0) {
2683               copy( formals.begin(), formals.end() - 1,
2684                     ostream_iterator<Node>(Debug("expand"), ", ") );
2685               Debug("expand") << formals.back();
2686             }
2687             Debug("expand") << "]" << endl
2688                             << "       " << def.getFunction().getType() << endl
2689                             << "       " << def.getFormula() << endl;
2690           }
2691
2692           fm = def.getFormula();
2693         }
2694
2695         Node instance = fm.substitute(formals.begin(),
2696                                       formals.end(),
2697                                       n.begin(),
2698                                       n.begin() + formals.size());
2699         Debug("expand") << "made : " << instance << endl;
2700
2701         Node expanded = expandDefinitions(instance, cache, expandOnly);
2702         cache[n] = (n == expanded ? Node::null() : expanded);
2703         result.push(expanded);
2704         continue;
2705
2706       } else if(! expandOnly) {
2707         // do not do any theory stuff if expandOnly is true
2708
2709         theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
2710
2711         Assert(t != NULL);
2712         LogicRequest req(d_smt);
2713         node = t->expandDefinition(req, n);
2714       }
2715
2716       // the partial functions can fall through, in which case we still
2717       // consider their children
2718       worklist.push(make_triple(Node(n), node, true));            // Original and rewritten result
2719
2720       for(size_t i = 0; i < node.getNumChildren(); ++i) {
2721         worklist.push(make_triple(node[i], node[i], false));      // Rewrite the children of the result only
2722       }
2723
2724     } else {
2725       // Working upwards
2726       // Reconstruct the node from it's (now rewritten) children on the stack
2727
2728       Debug("expand") << "cons : " << node << endl;
2729       if(node.getNumChildren()>0) {
2730         //cout << "cons : " << node << endl;
2731         NodeBuilder<> nb(node.getKind());
2732         if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
2733           Debug("expand") << "op   : " << node.getOperator() << endl;
2734           //cout << "op   : " << node.getOperator() << endl;
2735           nb << node.getOperator();
2736         }
2737         for(size_t i = 0; i < node.getNumChildren(); ++i) {
2738           Assert(!result.empty());
2739           Node expanded = result.top();
2740           result.pop();
2741           //cout << "exchld : " << expanded << endl;
2742           Debug("expand") << "exchld : " << expanded << endl;
2743           nb << expanded;
2744         }
2745         node = nb;
2746       }
2747       cache[n] = n == node ? Node::null() : node;           // Only cache once all subterms are expanded
2748       result.push(node);
2749     }
2750   } while(!worklist.empty());
2751
2752   AlwaysAssert(result.size() == 1);
2753
2754   return result.top();
2755 }
2756
2757 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
2758
2759 Node SmtEnginePrivate::realToInt(TNode n, NodeMap& cache, std::vector< Node >& var_eq) {
2760   Trace("real-as-int-debug") << "Convert : " << n << std::endl;
2761   NodeMap::iterator find = cache.find(n);
2762   if (find != cache.end()) {
2763     return (*find).second;
2764   }else{
2765     Node ret = n;
2766     if( n.getNumChildren()>0 ){
2767       if( n.getKind()==kind::EQUAL || n.getKind()==kind::GEQ || n.getKind()==kind::LT || n.getKind()==kind::GT || n.getKind()==kind::LEQ ){
2768         ret = Rewriter::rewrite( n );
2769         Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl;
2770         if( !ret.isConst() ){
2771           Node ret_lit = ret.getKind()==kind::NOT ? ret[0] : ret;
2772           bool ret_pol = ret.getKind()!=kind::NOT;
2773           std::map< Node, Node > msum;
2774           if (ArithMSum::getMonomialSumLit(ret_lit, msum))
2775           {
2776             //get common coefficient
2777             std::vector< Node > coeffs;
2778             for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
2779               Node v = itm->first;
2780               Node c = itm->second;
2781               if( !c.isNull() ){
2782                 Assert( c.isConst() );
2783                 coeffs.push_back( NodeManager::currentNM()->mkConst( Rational( c.getConst<Rational>().getDenominator() ) ) );
2784               }
2785             }
2786             Node cc = coeffs.empty() ? Node::null() : ( coeffs.size()==1 ? coeffs[0] : Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, coeffs ) ) );
2787             std::vector< Node > sum;
2788             for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
2789               Node v = itm->first;
2790               Node c = itm->second;
2791               Node s;
2792               if( c.isNull() ){
2793                 c = cc.isNull() ? NodeManager::currentNM()->mkConst( Rational( 1 ) ) : cc;
2794               }else{
2795                 if( !cc.isNull() ){
2796                   c = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, c, cc ) );
2797                 }
2798               }
2799               Assert( c.getType().isInteger() );
2800               if( v.isNull() ){
2801                 sum.push_back( c );
2802               }else{
2803                 Node vv = realToInt( v, cache, var_eq );
2804                 if( vv.getType().isInteger() ){
2805                   sum.push_back( NodeManager::currentNM()->mkNode( kind::MULT, c, vv ) );
2806                 }else{
2807                   throw TypeCheckingException(v.toExpr(), string("Cannot translate to Int: ") + v.toString());
2808                 }
2809               }
2810             }
2811             Node sumt = sum.empty() ? NodeManager::currentNM()->mkConst( Rational( 0 ) ) : ( sum.size()==1 ? sum[0] : NodeManager::currentNM()->mkNode( kind::PLUS, sum ) );
2812             ret = NodeManager::currentNM()->mkNode( ret_lit.getKind(), sumt, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
2813             if( !ret_pol ){
2814               ret = ret.negate();
2815             }
2816             Trace("real-as-int") << "Convert : " << std::endl;
2817             Trace("real-as-int") << "   " << n << std::endl;
2818             Trace("real-as-int") << "   " << ret << std::endl;
2819           }else{
2820             throw TypeCheckingException(n.toExpr(), string("Cannot translate to Int: ") + n.toString());
2821           }
2822         }
2823       }else{
2824         bool childChanged = false;
2825         std::vector< Node > children;
2826         for( unsigned i=0; i<n.getNumChildren(); i++ ){
2827           Node nc = realToInt( n[i], cache, var_eq );
2828           childChanged = childChanged || nc!=n[i];
2829           children.push_back( nc );
2830         }
2831         if( childChanged ){
2832           ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
2833         }
2834       }
2835     }else{
2836       if( n.isVar() ){
2837         if( !n.getType().isInteger() ){
2838           ret = NodeManager::currentNM()->mkSkolem("__realToInt_var", NodeManager::currentNM()->integerType(), "Variable introduced in realToInt pass");
2839           var_eq.push_back( n.eqNode( ret ) );
2840           TheoryModel* m = d_smt.d_theoryEngine->getModel();
2841           m->addSubstitution(n,ret);
2842         }
2843       }
2844     }
2845     cache[n] = ret;
2846     return ret;
2847   }
2848 }
2849
2850 Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector< Node >& var_eq, bool beneathMult) {
2851   if( beneathMult ){
2852     NodeMap::iterator find = bcache.find(n);
2853     if (find != bcache.end()) {
2854       return (*find).second;
2855     }
2856   }else{
2857     NodeMap::iterator find = cache.find(n);
2858     if (find != cache.end()) {
2859       return (*find).second;
2860     }
2861   }
2862   Node ret = n;
2863   if( n.getNumChildren()>0 ){
2864     if( beneathMult && n.getKind()!=kind::MULT ){
2865       //new variable
2866       ret = NodeManager::currentNM()->mkSkolem("__purifyNl_var", n.getType(), "Variable introduced in purifyNl pass");
2867       Node np = purifyNlTerms( n, cache, bcache, var_eq, false );
2868       var_eq.push_back( np.eqNode( ret ) );
2869     }else{
2870       bool beneathMultNew = beneathMult || n.getKind()==kind::MULT;
2871       bool childChanged = false;
2872       std::vector< Node > children;
2873       for( unsigned i=0; i<n.getNumChildren(); i++ ){
2874         Node nc = purifyNlTerms( n[i], cache, bcache, var_eq, beneathMultNew );
2875         childChanged = childChanged || nc!=n[i];
2876         children.push_back( nc );
2877       }
2878       if( childChanged ){
2879         ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
2880       }
2881     }
2882   }
2883   if( beneathMult ){
2884     bcache[n] = ret;
2885   }else{
2886     cache[n] = ret;
2887   }
2888   return ret;
2889 }
2890
2891 void SmtEnginePrivate::removeITEs() {
2892   d_smt.finalOptionsAreSet();
2893   spendResource(options::preprocessStep());
2894   Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
2895
2896   // Remove all of the ITE occurrences and normalize
2897   d_iteRemover.run(d_assertions.ref(), d_iteSkolemMap, true);
2898   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
2899     d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
2900   }
2901 }
2902
2903 void SmtEnginePrivate::staticLearning() {
2904   d_smt.finalOptionsAreSet();
2905   spendResource(options::preprocessStep());
2906
2907   TimerStat::CodeTimer staticLearningTimer(d_smt.d_stats->d_staticLearningTime);
2908
2909   Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl;
2910
2911   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
2912
2913     NodeBuilder<> learned(kind::AND);
2914     learned << d_assertions[i];
2915     d_smt.d_theoryEngine->ppStaticLearn(d_assertions[i], learned);
2916     if(learned.getNumChildren() == 1) {
2917       learned.clear();
2918     } else {
2919       d_assertions.replace(i, learned);
2920     }
2921   }
2922 }
2923
2924 // do dumping (before/after any preprocessing pass)
2925 static void dumpAssertions(const char* key,
2926                            const AssertionPipeline& assertionList) {
2927   if( Dump.isOn("assertions") &&
2928       Dump.isOn(string("assertions:") + key) ) {
2929     // Push the simplified assertions to the dump output stream
2930     for(unsigned i = 0; i < assertionList.size(); ++ i) {
2931       TNode n = assertionList[i];
2932       Dump("assertions") << AssertCommand(Expr(n.toExpr()));
2933     }
2934   }
2935 }
2936
2937 // returns false if it learns a conflict
2938 bool SmtEnginePrivate::nonClausalSimplify() {
2939   spendResource(options::preprocessStep());
2940   d_smt.finalOptionsAreSet();
2941
2942   if(options::unsatCores() || options::fewerPreprocessingHoles()) {
2943     return true;
2944   }
2945
2946   TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
2947
2948   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
2949   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
2950     Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl;
2951   }
2952
2953   if(d_propagatorNeedsFinish) {
2954     d_propagator.finish();
2955     d_propagatorNeedsFinish = false;
2956   }
2957   d_propagator.initialize();
2958
2959   // Assert all the assertions to the propagator
2960   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2961                     << "asserting to propagator" << endl;
2962   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
2963     Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
2964     // Don't reprocess substitutions
2965     if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) {
2966       continue;
2967     }
2968     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl;
2969     Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl;
2970     d_propagator.assertTrue(d_assertions[i]);
2971   }
2972
2973   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2974                     << "propagating" << endl;
2975   if (d_propagator.propagate()) {
2976     // If in conflict, just return false
2977     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
2978                       << "conflict in non-clausal propagation" << endl;
2979     Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
2980     Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
2981     d_assertions.clear();
2982     addFormula(falseNode, false, false);
2983     d_propagatorNeedsFinish = true;
2984     return false;
2985   }
2986
2987
2988   Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl;
2989   // No conflict, go through the literals and solve them
2990   SubstitutionMap constantPropagations(d_smt.d_context);
2991   SubstitutionMap newSubstitutions(d_smt.d_context);
2992   SubstitutionMap::iterator pos;
2993   unsigned j = 0;
2994   for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals.size(); i < i_end; ++ i) {
2995     // Simplify the literal we learned wrt previous substitutions
2996     Node learnedLiteral = d_nonClausalLearnedLiterals[i];
2997     Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
2998     Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral);
2999     Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl;
3000     Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
3001     if (learnedLiteral != learnedLiteralNew) {
3002       learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
3003     }
3004     Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral << std::endl;
3005     for (;;) {
3006       learnedLiteralNew = constantPropagations.apply(learnedLiteral);
3007       if (learnedLiteralNew == learnedLiteral) {
3008         break;
3009       }
3010       ++d_smt.d_stats->d_numConstantProps;
3011       learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
3012     }
3013     Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral << std::endl;
3014     // It might just simplify to a constant
3015     if (learnedLiteral.isConst()) {
3016       if (learnedLiteral.getConst<bool>()) {
3017         // If the learned literal simplifies to true, it's redundant
3018         continue;
3019       } else {
3020         // If the learned literal simplifies to false, we're in conflict
3021         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3022                           << "conflict with "
3023                           << d_nonClausalLearnedLiterals[i] << endl;
3024         Assert(!options::unsatCores());
3025         d_assertions.clear();
3026         addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
3027         d_propagatorNeedsFinish = true;
3028         return false;
3029       }
3030     }
3031
3032     // Solve it with the corresponding theory, possibly adding new
3033     // substitutions to newSubstitutions
3034     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3035                       << "solving " << learnedLiteral << endl;
3036
3037     Theory::PPAssertStatus solveStatus =
3038       d_smt.d_theoryEngine->solve(learnedLiteral, newSubstitutions);
3039
3040     switch (solveStatus) {
3041       case Theory::PP_ASSERT_STATUS_SOLVED: {
3042         // The literal should rewrite to true
3043         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3044                           << "solved " << learnedLiteral << endl;
3045         Assert(Rewriter::rewrite(newSubstitutions.apply(learnedLiteral)).isConst());
3046         //        vector<pair<Node, Node> > equations;
3047         //        constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
3048         //        if (equations.empty()) {
3049         //          break;
3050         //        }
3051         //        Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
3052         // else fall through
3053         break;
3054       }
3055       case Theory::PP_ASSERT_STATUS_CONFLICT:
3056         // If in conflict, we return false
3057         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3058                           << "conflict while solving "
3059                           << learnedLiteral << endl;
3060         Assert(!options::unsatCores());
3061         d_assertions.clear();
3062         addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
3063         d_propagatorNeedsFinish = true;
3064         return false;
3065       default:
3066         if (d_doConstantProp && learnedLiteral.getKind() == kind::EQUAL && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) {
3067           // constant propagation
3068           TNode t;
3069           TNode c;
3070           if (learnedLiteral[0].isConst()) {
3071             t = learnedLiteral[1];
3072             c = learnedLiteral[0];
3073           }
3074           else {
3075             t = learnedLiteral[0];
3076             c = learnedLiteral[1];
3077           }
3078           Assert(!t.isConst());
3079           Assert(constantPropagations.apply(t) == t);
3080           Assert(d_topLevelSubstitutions.apply(t) == t);
3081           Assert(newSubstitutions.apply(t) == t);
3082           constantPropagations.addSubstitution(t, c);
3083           // vector<pair<Node,Node> > equations;
3084           // constantPropagations.simplifyLHS(t, c, equations, true);
3085           // if (!equations.empty()) {
3086           //   Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
3087           //   d_assertions.clear();
3088           //   addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
3089           //   return;
3090           // }
3091           // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
3092         }
3093         else {
3094           // Keep the literal
3095           d_nonClausalLearnedLiterals[j++] = d_nonClausalLearnedLiterals[i];
3096         }
3097         break;
3098     }
3099   }
3100
3101 #ifdef CVC4_ASSERTIONS
3102   // NOTE: When debugging this code, consider moving this check inside of the
3103   // loop over d_nonClausalLearnedLiterals. This check has been moved outside
3104   // because it is costly for certain inputs (see bug 508).
3105   //
3106   // Check data structure invariants:
3107   // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations
3108   // 2. each lhs of constantPropagations rewrites to itself
3109   // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
3110   //    constant propagation too
3111   // 4. each lhs of constantPropagations is different from each rhs
3112   for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
3113     Assert((*pos).first.isVar());
3114     Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first);
3115     Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
3116     Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second));
3117   }
3118   for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
3119     Assert((*pos).second.isConst());
3120     Assert(Rewriter::rewrite((*pos).first) == (*pos).first);
3121     // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
3122     // if (newLeft != (*pos).first) {
3123     //   newLeft = Rewriter::rewrite(newLeft);
3124     //   Assert(newLeft == (*pos).second ||
3125     //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
3126     // }
3127     // newLeft = constantPropagations.apply((*pos).first);
3128     // if (newLeft != (*pos).first) {
3129     //   newLeft = Rewriter::rewrite(newLeft);
3130     //   Assert(newLeft == (*pos).second ||
3131     //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
3132     // }
3133     Assert(constantPropagations.apply((*pos).second) == (*pos).second);
3134   }
3135 #endif /* CVC4_ASSERTIONS */
3136
3137   // Resize the learnt
3138   Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
3139   d_nonClausalLearnedLiterals.resize(j);
3140
3141   unordered_set<TNode, TNodeHashFunction> s;
3142   Trace("debugging") << "NonClausal simplify pre-preprocess\n";
3143   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
3144     Node assertion = d_assertions[i];
3145     Node assertionNew = newSubstitutions.apply(assertion);
3146     Trace("debugging") << "assertion = " << assertion << endl;
3147     Trace("debugging") << "assertionNew = " << assertionNew << endl;
3148     if (assertion != assertionNew) {
3149       assertion = Rewriter::rewrite(assertionNew);
3150       Trace("debugging") << "rewrite(assertion) = " << assertion << endl;
3151     }
3152     Assert(Rewriter::rewrite(assertion) == assertion);
3153     for (;;) {
3154       assertionNew = constantPropagations.apply(assertion);
3155       if (assertionNew == assertion) {
3156         break;
3157       }
3158       ++d_smt.d_stats->d_numConstantProps;
3159       Trace("debugging") << "assertionNew = " << assertionNew << endl;
3160       assertion = Rewriter::rewrite(assertionNew);
3161       Trace("debugging") << "assertionNew = " << assertionNew << endl;
3162     }
3163     Trace("debugging") << "\n";
3164     s.insert(assertion);
3165     d_assertions.replace(i, assertion);
3166     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3167                       << "non-clausal preprocessed: "
3168                       << assertion << endl;
3169   }
3170
3171   // If in incremental mode, add substitutions to the list of assertions
3172   if (d_substitutionsIndex > 0) {
3173     NodeBuilder<> substitutionsBuilder(kind::AND);
3174     substitutionsBuilder << d_assertions[d_substitutionsIndex];
3175     pos = newSubstitutions.begin();
3176     for (; pos != newSubstitutions.end(); ++pos) {
3177       // Add back this substitution as an assertion
3178       TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second);
3179       Node n = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs);
3180       substitutionsBuilder << n;
3181       Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
3182     }
3183     if (substitutionsBuilder.getNumChildren() > 1) {
3184       d_assertions.replace(d_substitutionsIndex,
3185         Rewriter::rewrite(Node(substitutionsBuilder)));
3186     }
3187   } else {
3188     // If not in incremental mode, must add substitutions to model
3189     TheoryModel* m = d_smt.d_theoryEngine->getModel();
3190     if(m != NULL) {
3191       for(pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
3192         Node n = (*pos).first;
3193         Node v = newSubstitutions.apply((*pos).second);
3194         Trace("model") << "Add substitution : " << n << " " << v << endl;
3195         m->addSubstitution( n, v );
3196       }
3197     }
3198   }
3199
3200   NodeBuilder<> learnedBuilder(kind::AND);
3201   Assert(d_realAssertionsEnd <= d_assertions.size());
3202   learnedBuilder << d_assertions[d_realAssertionsEnd - 1];
3203
3204   for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
3205     Node learned = d_nonClausalLearnedLiterals[i];
3206     Assert(d_topLevelSubstitutions.apply(learned) == learned);
3207     Node learnedNew = newSubstitutions.apply(learned);
3208     if (learned != learnedNew) {
3209       learned = Rewriter::rewrite(learnedNew);
3210     }
3211     Assert(Rewriter::rewrite(learned) == learned);
3212     for (;;) {
3213       learnedNew = constantPropagations.apply(learned);
3214       if (learnedNew == learned) {
3215         break;
3216       }
3217       ++d_smt.d_stats->d_numConstantProps;
3218       learned = Rewriter::rewrite(learnedNew);
3219     }
3220     if (s.find(learned) != s.end()) {
3221       continue;
3222     }
3223     s.insert(learned);
3224     learnedBuilder << learned;
3225     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3226                       << "non-clausal learned : "
3227                       << learned << endl;
3228   }
3229   d_nonClausalLearnedLiterals.clear();
3230
3231   for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
3232     Node cProp = (*pos).first.eqNode((*pos).second);
3233     Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
3234     Node cPropNew = newSubstitutions.apply(cProp);
3235     if (cProp != cPropNew) {
3236       cProp = Rewriter::rewrite(cPropNew);
3237       Assert(Rewriter::rewrite(cProp) == cProp);
3238     }
3239     if (s.find(cProp) != s.end()) {
3240       continue;
3241     }
3242     s.insert(cProp);
3243     learnedBuilder << cProp;
3244     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
3245                       << "non-clausal constant propagation : "
3246                       << cProp << endl;
3247   }
3248
3249   // Add new substitutions to topLevelSubstitutions
3250   // Note that we don't have to keep rhs's in full solved form
3251   // because SubstitutionMap::apply does a fixed-point iteration when substituting
3252   d_topLevelSubstitutions.addSubstitutions(newSubstitutions);
3253
3254   if(learnedBuilder.getNumChildren() > 1) {
3255     d_assertions.replace(d_realAssertionsEnd - 1,
3256       Rewriter::rewrite(Node(learnedBuilder)));
3257   }
3258
3259   d_propagatorNeedsFinish = true;
3260   return true;
3261 }
3262
3263 void SmtEnginePrivate::bvAbstraction() {
3264   Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl;
3265   std::vector<Node> new_assertions;
3266   bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertions.ref(), new_assertions);
3267   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
3268     d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
3269   }
3270   // if we are using the lazy solver and the abstraction
3271   // applies, then UF symbols were introduced
3272   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
3273       changed) {
3274     LogicRequest req(d_smt);
3275     req.widenLogic(THEORY_UF);
3276   }
3277 }
3278
3279
3280 void SmtEnginePrivate::bvToBool() {
3281   Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
3282   spendResource(options::preprocessStep());
3283   std::vector<Node> new_assertions;
3284   d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
3285   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
3286     d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
3287   }
3288 }
3289
3290 void SmtEnginePrivate::boolToBv() {
3291   Trace("bool-to-bv") << "SmtEnginePrivate::boolToBv()" << endl;
3292   spendResource(options::preprocessStep());
3293   std::vector<Node> new_assertions;
3294   d_smt.d_theoryEngine->ppBoolToBv(d_assertions.ref(), new_assertions);
3295   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
3296     d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
3297   }
3298 }
3299
3300 bool SmtEnginePrivate::simpITE() {
3301   TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
3302
3303   spendResource(options::preprocessStep());
3304
3305   Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
3306
3307   unsigned numAssertionOnEntry = d_assertions.size();
3308   for (unsigned i = 0; i < d_assertions.size(); ++i) {
3309     spendResource(options::preprocessStep());
3310     Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
3311     d_assertions.replace(i, result);
3312     if(result.isConst() && !result.getConst<bool>()){
3313       return false;
3314     }
3315   }
3316   bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref());
3317   if(numAssertionOnEntry < d_assertions.size()){
3318     compressBeforeRealAssertions(numAssertionOnEntry);
3319   }
3320   return result;
3321 }
3322
3323 void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
3324   size_t curr = d_assertions.size();
3325   if(before >= curr ||
3326      d_realAssertionsEnd <= 0 ||
3327      d_realAssertionsEnd >= curr){
3328     return;
3329   }
3330
3331   // assertions
3332   // original: [0 ... d_realAssertionsEnd)
3333   //  can be modified
3334   // ites skolems [d_realAssertionsEnd, before)
3335   //  cannot be moved
3336   // added [before, curr)
3337   //  can be modified
3338   Assert(0 < d_realAssertionsEnd);
3339   Assert(d_realAssertionsEnd <= before);
3340   Assert(before < curr);
3341
3342   std::vector<Node> intoConjunction;
3343   for(size_t i = before; i<curr; ++i){
3344     intoConjunction.push_back(d_assertions[i]);
3345   }
3346   d_assertions.resize(before);
3347   size_t lastBeforeItes = d_realAssertionsEnd - 1;
3348   intoConjunction.push_back(d_assertions[lastBeforeItes]);
3349   Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
3350   d_assertions.replace(lastBeforeItes, newLast);
3351   Assert(d_assertions.size() == before);
3352 }
3353
3354 void SmtEnginePrivate::unconstrainedSimp() {
3355   TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
3356   spendResource(options::preprocessStep());
3357   Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
3358   d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
3359 }
3360
3361 void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) {
3362   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
3363   for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) {
3364     booleans::CircuitPropagator::BackEdgesMap::const_iterator j = backEdges.find(*i);
3365     // term must appear in map, otherwise how did we get here?!
3366     Assert(j != backEdges.end());
3367     // if term maps to empty, that means it's a top-level assertion
3368     if(!(*j).second.empty()) {
3369       traceBackToAssertions((*j).second, assertions);
3370     } else {
3371       assertions.push_back(*i);
3372     }
3373   }
3374 }
3375
3376 size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set<unsigned long>& toRemove) {
3377   Assert(n.getKind() == kind::AND);
3378   size_t removals = 0;
3379   for(Node::iterator j = n.begin(); j != n.end(); ++j) {
3380     size_t subremovals = 0;
3381     Node sub = *j;
3382     if(toRemove.find(sub.getId()) != toRemove.end() ||
3383        (sub.getKind() == kind::AND && (subremovals = removeFromConjunction(sub, toRemove)) > 0)) {
3384       NodeBuilder<> b(kind::AND);
3385       b.append(n.begin(), j);
3386       if(subremovals > 0) {
3387         removals += subremovals;
3388         b << sub;
3389       } else {
3390         ++removals;
3391       }
3392       for(++j; j != n.end(); ++j) {
3393         if(toRemove.find((*j).getId()) != toRemove.end()) {
3394           ++removals;
3395         } else if((*j).getKind() == kind::AND) {
3396           sub = *j;
3397           if((subremovals = removeFromConjunction(sub, toRemove)) > 0) {
3398             removals += subremovals;
3399             b << sub;
3400           } else {
3401             b << *j;
3402           }
3403         } else {
3404           b << *j;
3405         }
3406       }
3407       if(b.getNumChildren() == 0) {
3408         n = d_true;
3409         b.clear();
3410       } else if(b.getNumChildren() == 1) {
3411         n = b[0];
3412         b.clear();
3413       } else {
3414         n = b;
3415       }
3416       n = Rewriter::rewrite(n);
3417       return removals;
3418     }
3419   }
3420
3421   Assert(removals == 0);
3422   return 0;
3423 }
3424
3425 void SmtEnginePrivate::doMiplibTrick() {
3426   Assert(d_realAssertionsEnd == d_assertions.size());
3427   Assert(!options::incrementalSolving());
3428
3429   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
3430   unordered_set<unsigned long> removeAssertions;
3431
3432   NodeManager* nm = NodeManager::currentNM();
3433   Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
3434
3435   unordered_map<TNode, Node, TNodeHashFunction> intVars;
3436   for(vector<Node>::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) {
3437     if(d_propagator.isAssigned(*i)) {
3438       Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator.getAssignment(*i) << endl;
3439       continue;
3440     }
3441
3442     vector<TNode> assertions;
3443     booleans::CircuitPropagator::BackEdgesMap::const_iterator j = backEdges.find(*i);
3444     // if not in back edges map, the bool var is unconstrained, showing up in no assertions.
3445     // if maps to an empty vector, that means the bool var was asserted itself.
3446     if(j != backEdges.end()) {
3447       if(!(*j).second.empty()) {
3448         traceBackToAssertions((*j).second, assertions);
3449       } else {
3450         assertions.push_back(*i);
3451       }
3452     }
3453     Debug("miplib") << "for " << *i << endl;
3454     bool eligible = true;
3455     map<pair<Node, Node>, uint64_t> marks;
3456     map<pair<Node, Node>, vector<Rational> > coef;
3457     map<pair<Node, Node>, vector<Rational> > checks;
3458     map<pair<Node, Node>, vector<TNode> > asserts;
3459     for(vector<TNode>::const_iterator j = assertions.begin(); j != assertions.end(); ++j) {
3460       Debug("miplib") << "  found: " << *j << endl;
3461       if((*j).getKind() != kind::IMPLIES) {
3462         eligible = false;
3463         Debug("miplib") << "  -- INELIGIBLE -- (not =>)" << endl;
3464         break;
3465       }
3466       Node conj = BooleanSimplification::simplify((*j)[0]);
3467       if(conj.getKind() == kind::AND && conj.getNumChildren() > 6) {
3468         eligible = false;
3469         Debug("miplib") << "  -- INELIGIBLE -- (N-ary /\\ too big)" << endl;
3470         break;
3471       }
3472       if(conj.getKind() != kind::AND && !conj.isVar() && !(conj.getKind() == kind::NOT && conj[0].isVar())) {
3473         eligible = false;
3474         Debug("miplib") << "  -- INELIGIBLE -- (not /\\ or literal)" << endl;
3475         break;
3476       }
3477       if((*j)[1].getKind() != kind::EQUAL ||
3478          !( ( (*j)[1][0].isVar() &&
3479               (*j)[1][1].getKind() == kind::CONST_RATIONAL ) ||
3480             ( (*j)[1][0].getKind() == kind::CONST_RATIONAL &&
3481               (*j)[1][1].isVar() ) )) {
3482         eligible = false;
3483         Debug("miplib") << "  -- INELIGIBLE -- (=> (and X X) X)" << endl;
3484         break;
3485       }
3486       if(conj.getKind() == kind::AND) {
3487         vector<Node> posv;
3488         bool found_x = false;
3489         map<TNode, bool> neg;
3490         for(Node::iterator ii = conj.begin(); ii != conj.end(); ++ii) {
3491           if((*ii).isVar()) {
3492             posv.push_back(*ii);
3493             neg[*ii] = false;
3494             found_x = found_x || *i == *ii;
3495           } else if((*ii).getKind() == kind::NOT && (*ii)[0].isVar()) {
3496             posv.push_back((*ii)[0]);
3497             neg[(*ii)[0]] = true;
3498             found_x = found_x || *i == (*ii)[0];
3499           } else {
3500             eligible = false;
3501             Debug("miplib") << "  -- INELIGIBLE -- (non-var: " << *ii << ")" << endl;
3502             break;
3503           }
3504           if(d_propagator.isAssigned(posv.back())) {
3505             eligible = false;
3506             Debug("miplib") << "  -- INELIGIBLE -- (" << posv.back() << " asserted)" << endl;
3507             break;
3508           }
3509         }
3510         if(!eligible) {
3511           break;
3512         }
3513         if(!found_x) {
3514           eligible = false;
3515           Debug("miplib") << "  --INELIGIBLE -- (couldn't find " << *i << " in conjunction)" << endl;
3516           break;
3517         }
3518         sort(posv.begin(), posv.end());
3519         const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv);
3520         const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][1] : (*j)[1][0];
3521         const pair<Node, Node> pos_var(pos, var);
3522         const Rational& constant = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][0].getConst<Rational>() : (*j)[1][1].getConst<Rational>();
3523         uint64_t mark = 0;
3524         unsigned countneg = 0, thepos = 0;
3525         for(unsigned ii = 0; ii < pos.getNumChildren(); ++ii) {
3526           if(neg[pos[ii]]) {
3527             ++countneg;
3528           } else {
3529             thepos = ii;
3530             mark |= (0x1 << ii);
3531           }
3532         }
3533         if((marks[pos_var] & (1lu << mark)) != 0) {
3534           eligible = false;
3535           Debug("miplib") << "  -- INELIGIBLE -- (remarked)" << endl;
3536           break;
3537         }
3538         Debug("miplib") << "mark is " << mark << " -- " << (1lu << mark) << endl;
3539         marks[pos_var] |= (1lu << mark);
3540         Debug("miplib") << "marks[" << pos << "," << var << "] now " << marks[pos_var] << endl;
3541         if(countneg == pos.getNumChildren()) {
3542           if(constant != 0) {
3543             eligible = false;
3544             Debug("miplib") << "  -- INELIGIBLE -- (nonzero constant)" << endl;
3545             break;
3546           }
3547         } else if(countneg == pos.getNumChildren() - 1) {
3548           Assert(coef[pos_var].size() <= 6 && thepos < 6);
3549           if(coef[pos_var].size() <= thepos) {
3550             coef[pos_var].resize(thepos + 1);
3551           }
3552           coef[pos_var][thepos] = constant;
3553         } else {
3554           if(checks[pos_var].size() <= mark) {
3555             checks[pos_var].resize(mark + 1);
3556           }
3557           checks[pos_var][mark] = constant;
3558         }
3559         asserts[pos_var].push_back(*j);
3560       } else {
3561         TNode x = conj;
3562         if(x != *i && x != (*i).notNode()) {
3563           eligible = false;
3564           Debug("miplib") << "  -- INELIGIBLE -- (x not present where I expect it)" << endl;
3565           break;
3566         }
3567         const bool xneg = (x.getKind() == kind::NOT);
3568         x = xneg ? x[0] : x;
3569         Debug("miplib") << "  x:" << x << "  " << xneg << endl;
3570         const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][1] : (*j)[1][0];
3571         const pair<Node, Node> x_var(x, var);
3572         const Rational& constant = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][0].getConst<Rational>() : (*j)[1][1].getConst<Rational>();
3573         unsigned mark = (xneg ? 0 : 1);
3574         if((marks[x_var] & (1u << mark)) != 0) {
3575           eligible = false;
3576           Debug("miplib") << "  -- INELIGIBLE -- (remarked)" << endl;
3577           break;
3578         }
3579         marks[x_var] |= (1u << mark);
3580         if(xneg) {
3581           if(constant != 0) {
3582             eligible = false;
3583             Debug("miplib") << "  -- INELIGIBLE -- (nonzero constant)" << endl;
3584             break;
3585           }
3586         } else {
3587           Assert(coef[x_var].size() <= 6);
3588           coef[x_var].resize(6);
3589           coef[x_var][0] = constant;
3590         }
3591         asserts[x_var].push_back(*j);
3592       }
3593     }
3594     if(eligible) {
3595       for(map<pair<Node, Node>, uint64_t>::const_iterator j = marks.begin(); j != marks.end(); ++j) {
3596         const TNode pos = (*j).first.first;
3597         const TNode var = (*j).first.second;
3598         const pair<Node, Node>& pos_var = (*j).first;
3599         const uint64_t mark = (*j).second;
3600         const unsigned numVars = pos.getKind() == kind::AND ? pos.getNumChildren() : 1;
3601         uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1;
3602         expected = (expected == 0) ? -1 : expected; // fix for overflow
3603         Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " << expected << dec << endl;
3604         Assert(pos.getKind() == kind::AND || pos.isVar());
3605         if(mark != expected) {
3606           Debug("miplib") << "  -- INELIGIBLE " << pos << " -- (insufficiently marked, got " << mark << " for " << numVars << " vars, expected " << expected << endl;
3607         } else {
3608           if(mark != 3) { // exclude single-var case; nothing to check there
3609             uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1;
3610             sz = (sz == 0) ? -1 : sz; // fix for overflow
3611             Assert(sz == mark, "expected size %u == mark %u", sz, mark);
3612             for(size_t k = 0; k < checks[pos_var].size(); ++k) {
3613               if((k & (k - 1)) != 0) {
3614                 Rational sum = 0;
3615                 Debug("miplib") << k << " => " << checks[pos_var][k] << endl;
3616                 for(size_t v = 1, kk = k; kk != 0; ++v, kk >>= 1) {
3617                   if((kk & 0x1) == 1) {
3618                     Assert(pos.getKind() == kind::AND);
3619                     Debug("miplib") << "var " << v << " : " << pos[v - 1] << " coef:" << coef[pos_var][v - 1] << endl;
3620                     sum += coef[pos_var][v - 1];
3621                   }
3622                 }
3623                 Debug("miplib") << "checkSum is " << sum << " input says " << checks[pos_var][k] << endl;
3624                 if(sum != checks[pos_var][k]) {
3625                   eligible = false;
3626                   Debug("miplib") << "  -- INELIGIBLE " << pos << " -- (nonlinear combination)" << endl;
3627                   break;
3628                 }
3629               } else {
3630                 Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str()); // we never set for single-positive-var
3631               }
3632             }
3633           }
3634           if(!eligible) {
3635             eligible = true; // next is still eligible
3636             continue;
3637           }
3638
3639           Debug("miplib") << "  -- ELIGIBLE " << *i << " , " << pos << " --" << endl;
3640           vector<Node> newVars;
3641           expr::NodeSelfIterator ii, iiend;
3642           if(pos.getKind() == kind::AND) {
3643             ii = pos.begin();
3644             iiend = pos.end();
3645           } else {
3646             ii = expr::NodeSelfIterator::self(pos);
3647             iiend = expr::NodeSelfIterator::selfEnd(pos);
3648           }
3649           for(; ii != iiend; ++ii) {
3650             Node& varRef = intVars[*ii];
3651             if(varRef.isNull()) {
3652               stringstream ss;
3653               ss << "mipvar_" << *ii;
3654               Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME);
3655               Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
3656               Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
3657               addFormula(Rewriter::rewrite(geq.andNode(leq)), false, false);
3658               SubstitutionMap nullMap(&d_fakeContext);
3659               Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
3660               status = d_smt.d_theoryEngine->solve(geq, nullMap);
3661               Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED,
3662                      "unexpected solution from arith's ppAssert()");
3663               Assert(nullMap.empty(),
3664                      "unexpected substitution from arith's ppAssert()");
3665               status = d_smt.d_theoryEngine->solve(leq, nullMap);
3666               Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED,
3667                      "unexpected solution from arith's ppAssert()");
3668               Assert(nullMap.empty(),
3669                      "unexpected substitution from arith's ppAssert()");
3670               d_smt.d_theoryEngine->getModel()->addSubstitution(*ii, newVar.eqNode(one));
3671               newVars.push_back(newVar);
3672               varRef = newVar;
3673             } else {
3674               newVars.push_back(varRef);
3675             }
3676             if(!d_smt.d_logic.areIntegersUsed()) {
3677               d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
3678               d_smt.d_logic.enableIntegers();
3679               d_smt.d_logic.lock();
3680             }
3681           }
3682           Node sum;
3683           if(pos.getKind() == kind::AND) {
3684             NodeBuilder<> sumb(kind::PLUS);
3685             for(size_t ii = 0; ii < pos.getNumChildren(); ++ii) {
3686               sumb << nm->mkNode(kind::MULT, nm->mkConst(coef[pos_var][ii]), newVars[ii]);
3687             }
3688             sum = sumb;
3689           } else {
3690             sum = nm->mkNode(kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]);
3691           }
3692           Debug("miplib") << "vars[] " << var << endl
3693                           << "    eq " << Rewriter::rewrite(sum) << endl;
3694           Node newAssertion = var.eqNode(Rewriter::rewrite(sum));
3695           if(d_topLevelSubstitutions.hasSubstitution(newAssertion[0])) {
3696             //Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
3697             //Warning() << "REPLACE         " << newAssertion[1] << endl;
3698             //Warning() << "ORIG            " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl;
3699             Assert(d_topLevelSubstitutions.getSubstitution(newAssertion[0]) == newAssertion[1]);
3700           } else if(pos.getNumChildren() <= options::arithMLTrickSubstitutions()) {
3701             d_topLevelSubstitutions.addSubstitution(newAssertion[0], newAssertion[1]);
3702             Debug("miplib") << "addSubs: " << newAssertion[0] << " to " << newAssertion[1] << endl;
3703           } else {
3704             Debug("miplib") << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl;
3705           }
3706           newAssertion = Rewriter::rewrite(newAssertion);
3707           Debug("miplib") << "  " << newAssertion << endl;
3708           addFormula(newAssertion, false, false);
3709           Debug("miplib") << "  assertions to remove: " << endl;
3710           for(vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) {
3711             Debug("miplib") << "    " << *k << endl;
3712             removeAssertions.insert((*k).getId());
3713           }
3714         }
3715       }
3716     }
3717   }
3718   if(!removeAssertions.empty()) {
3719     Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl;
3720     for(size_t i = 0; i < d_realAssertionsEnd; ++i) {
3721       if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) {
3722         Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl;
3723         d_assertions[i] = d_true;
3724         ++d_smt.d_stats->d_numMiplibAssertionsRemoved;
3725       } else if(d_assertions[i].getKind() == kind::AND) {
3726         size_t removals = removeFromConjunction(d_assertions[i], removeAssertions);
3727         if(removals > 0) {
3728           Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions[i] << endl;
3729           Debug("miplib") << "SmtEnginePrivate::simplify(): -      by " << removals << " conjuncts" << endl;
3730           d_smt.d_stats->d_numMiplibAssertionsRemoved += removals;
3731         }
3732       }
3733       Debug("miplib") << "had: " << d_assertions[i] << endl;
3734       d_assertions[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]));
3735       Debug("miplib") << "now: " << d_assertions[i] << endl;
3736     }
3737   } else {
3738     Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl;
3739   }
3740   d_realAssertionsEnd = d_assertions.size();
3741 }
3742
3743
3744 // returns false if simplification led to "false"
3745 bool SmtEnginePrivate::simplifyAssertions()
3746 {
3747   spendResource(options::preprocessStep());
3748   Assert(d_smt.d_pendingPops == 0);
3749   try {
3750     ScopeCounter depth(d_simplifyAssertionsDepth);
3751
3752     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
3753
3754     dumpAssertions("pre-nonclausal", d_assertions);
3755
3756     if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
3757       // Perform non-clausal simplification
3758       Chat() << "...performing nonclausal simplification..." << endl;
3759       Trace("simplify") << "SmtEnginePrivate::simplify(): "
3760                         << "performing non-clausal simplification" << endl;
3761       bool noConflict = nonClausalSimplify();
3762       if(!noConflict) {
3763         return false;
3764       }
3765
3766       // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
3767       // do the miplib trick.
3768       if( // check that option is on
3769           options::arithMLTrick() &&
3770           // miplib rewrites aren't safe in incremental mode
3771           ! options::incrementalSolving() &&
3772           // only useful in arith
3773           d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
3774           // we add new assertions and need this (in practice, this
3775           // restriction only disables miplib processing during
3776           // re-simplification, which we don't expect to be useful anyway)
3777           d_realAssertionsEnd == d_assertions.size() ) {
3778         Chat() << "...fixing miplib encodings..." << endl;
3779         Trace("simplify") << "SmtEnginePrivate::simplify(): "
3780                           << "looking for miplib pseudobooleans..." << endl;
3781
3782         TimerStat::CodeTimer miplibTimer(d_smt.d_stats->d_miplibPassTime);
3783
3784         doMiplibTrick();
3785       } else {
3786         Trace("simplify") << "SmtEnginePrivate::simplify(): "
3787                           << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;
3788       }
3789     }
3790
3791     dumpAssertions("post-nonclausal", d_assertions);
3792     Trace("smt") << "POST nonClausalSimplify" << endl;
3793     Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
3794
3795     // before ppRewrite check if only core theory for BV theory
3796     d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref());
3797
3798     dumpAssertions("pre-theorypp", d_assertions);
3799
3800     // Theory preprocessing
3801     if (d_smt.d_earlyTheoryPP) {
3802       Chat() << "...doing early theory preprocessing..." << endl;
3803       TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
3804       // Call the theory preprocessors
3805       d_smt.d_theoryEngine->preprocessStart();
3806       for (unsigned i = 0; i < d_assertions.size(); ++ i) {
3807         Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
3808         d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
3809         Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
3810       }
3811     }
3812
3813     dumpAssertions("post-theorypp", d_assertions);
3814     Trace("smt") << "POST theoryPP" << endl;
3815     Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
3816
3817     // ITE simplification
3818     if(options::doITESimp() &&
3819        (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) {
3820       Chat() << "...doing ITE simplification..." << endl;
3821       bool noConflict = simpITE();
3822       if(!noConflict){
3823         Chat() << "...ITE simplification found unsat..." << endl;
3824         return false;
3825       }
3826     }
3827
3828     dumpAssertions("post-itesimp", d_assertions);
3829     Trace("smt") << "POST iteSimp" << endl;
3830     Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
3831
3832     // Unconstrained simplification
3833     if(options::unconstrainedSimp()) {
3834       Chat() << "...doing unconstrained simplification..." << endl;
3835       unconstrainedSimp();
3836     }
3837
3838     dumpAssertions("post-unconstrained", d_assertions);
3839     Trace("smt") << "POST unconstrainedSimp" << endl;
3840     Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
3841
3842     if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
3843       Chat() << "...doing another round of nonclausal simplification..." << endl;
3844       Trace("simplify") << "SmtEnginePrivate::simplify(): "
3845                         << " doing repeated simplification" << endl;
3846       bool noConflict = nonClausalSimplify();
3847       if(!noConflict) {
3848         return false;
3849       }
3850     }
3851
3852     dumpAssertions("post-repeatsimp", d_assertions);
3853     Trace("smt") << "POST repeatSimp" << endl;
3854     Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
3855
3856   } catch(TypeCheckingExceptionPrivate& tcep) {
3857     // Calls to this function should have already weeded out any
3858     // typechecking exceptions via (e.g.) ensureBoolean().  But a
3859     // theory could still create a new expression that isn't
3860     // well-typed, and we don't want the C++ runtime to abort our
3861     // process without any error notice.
3862     stringstream ss;
3863     ss << "A bad expression was produced.  Original exception follows:\n"
3864        << tcep;
3865     InternalError(ss.str().c_str());
3866   }
3867   return true;
3868 }
3869
3870 Result SmtEngine::check() {
3871   Assert(d_fullyInited);
3872   Assert(d_pendingPops == 0);
3873
3874   Trace("smt") << "SmtEngine::check()" << endl;
3875
3876   ResourceManager* resourceManager = d_private->getResourceManager();
3877
3878   resourceManager->beginCall();
3879
3880   // Only way we can be out of resource is if cumulative budget is on
3881   if (resourceManager->cumulativeLimitOn() &&
3882       resourceManager->out()) {
3883     Result::UnknownExplanation why = resourceManager->outOfResources() ?
3884                              Result::RESOURCEOUT : Result::TIMEOUT;
3885     return Result(Result::VALIDITY_UNKNOWN, why, d_filename);
3886   }
3887
3888   // Make sure the prop layer has all of the assertions
3889   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
3890   d_private->processAssertions();
3891   Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
3892
3893   // Turn off stop only for QF_LRA
3894   // TODO: Bring up in a meeting where to put this
3895   if(options::decisionStopOnly() && !options::decisionMode.wasSetByUser() ){
3896     if( // QF_LRA
3897        (not d_logic.isQuantified() &&
3898         d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
3899         )){
3900       if(d_private->d_iteSkolemMap.empty()){
3901         options::decisionStopOnly.set(false);
3902         d_decisionEngine->clearStrategies();
3903         Trace("smt") << "SmtEngine::check(): turning off stop only" << endl;
3904       }
3905     }
3906   }
3907
3908   TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
3909
3910   Chat() << "solving..." << endl;
3911   Trace("smt") << "SmtEngine::check(): running check" << endl;
3912   Result result = d_propEngine->checkSat();
3913
3914   resourceManager->endCall();
3915   Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager->getTimeUsage()
3916                  << ", resources " << resourceManager->getResourceUsage() << endl;
3917
3918
3919   return Result(result, d_filename);
3920 }
3921
3922 Result SmtEngine::quickCheck() {
3923   Assert(d_fullyInited);
3924   Trace("smt") << "SMT quickCheck()" << endl;
3925   return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
3926 }
3927
3928
3929 void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
3930 {
3931   unordered_map<Node, bool, NodeHashFunction>::iterator it;
3932   it = cache.find(n);
3933   if (it != cache.end()) {
3934     return;
3935   }
3936
3937   size_t sz = n.getNumChildren();
3938   if (sz == 0) {
3939     IteSkolemMap::iterator it = d_iteSkolemMap.find(n);
3940     if (it != d_iteSkolemMap.end()) {
3941       skolemSet.insert(n);
3942     }
3943     cache[n] = true;
3944     return;
3945   }
3946
3947   size_t k = 0;
3948   for (; k < sz; ++k) {
3949     collectSkolems(n[k], skolemSet, cache);
3950   }
3951   cache[n] = true;
3952 }
3953
3954
3955 bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
3956 {
3957   unordered_map<Node, bool, NodeHashFunction>::iterator it;
3958   it = cache.find(n);
3959   if (it != cache.end()) {
3960     return (*it).second;
3961   }
3962
3963   size_t sz = n.getNumChildren();
3964   if (sz == 0) {
3965     IteSkolemMap::iterator it = d_iteSkolemMap.find(n);
3966     bool bad = false;
3967     if (it != d_iteSkolemMap.end()) {
3968       if (!((*it).first < n)) {
3969         bad = true;
3970       }
3971     }
3972     cache[n] = bad;
3973     return bad;
3974   }
3975
3976   size_t k = 0;
3977   for (; k < sz; ++k) {
3978     if (checkForBadSkolems(n[k], skolem, cache)) {
3979       cache[n] = true;
3980       return true;
3981     }
3982   }
3983
3984   cache[n] = false;
3985   return false;
3986 }
3987
3988 void SmtEnginePrivate::applySubstitutionsToAssertions() {
3989   if(!options::unsatCores()) {
3990     Chat() << "applying substitutions..." << endl;
3991     Trace("simplify") << "SmtEnginePrivate::processAssertions(): "
3992                       << "applying substitutions" << endl;
3993     // TODO(b/1255): Substitutions in incremental mode should be managed with a
3994     // proper data structure.
3995
3996     // When solving incrementally, all substitutions are piled into the
3997     // assertion at d_substitutionsIndex: we don't want to apply substitutions
3998     // to this assertion or information will be lost.
3999     unsigned substitutionAssertion = d_substitutionsIndex > 0 ? d_substitutionsIndex : d_assertions.size();
4000     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4001       if (i == substitutionAssertion) {
4002         continue;
4003       }
4004       Trace("simplify") << "applying to " << d_assertions[i] << endl;
4005       spendResource(options::preprocessStep());
4006       d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
4007       Trace("simplify") << "  got " << d_assertions[i] << endl;
4008     }
4009   }
4010 }
4011
4012 void SmtEnginePrivate::processAssertions() {
4013   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
4014   spendResource(options::preprocessStep());
4015   Assert(d_smt.d_fullyInited);
4016   Assert(d_smt.d_pendingPops == 0);
4017
4018   // Dump the assertions
4019   dumpAssertions("pre-everything", d_assertions);
4020
4021   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl;
4022   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
4023
4024   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
4025
4026   if (d_assertions.size() == 0) {
4027     // nothing to do
4028     return;
4029   }
4030
4031   if (options::bvGaussElim())
4032   {
4033     TimerStat::CodeTimer gaussElimTimer(d_smt.d_stats->d_gaussElimTime);
4034     d_preprocessingPassRegistry.getPass("bv-gauss")->apply(&d_assertions);
4035   }
4036
4037   if (d_assertionsProcessed && options::incrementalSolving()) {
4038     // TODO(b/1255): Substitutions in incremental mode should be managed with a
4039     // proper data structure.
4040
4041     // Placeholder for storing substitutions
4042     d_substitutionsIndex = d_assertions.size();
4043     d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
4044   }
4045
4046   // Add dummy assertion in last position - to be used as a
4047   // placeholder for any new assertions to get added
4048   d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
4049   // any assertions added beyond realAssertionsEnd must NOT affect the
4050   // equisatisfiability
4051   d_realAssertionsEnd = d_assertions.size();
4052
4053   // Assertions are NOT guaranteed to be rewritten by this point
4054
4055   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl;
4056   dumpAssertions("pre-definition-expansion", d_assertions);
4057   {
4058     Chat() << "expanding definitions..." << endl;
4059     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
4060     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
4061     unordered_map<Node, Node, NodeHashFunction> cache;
4062     for(unsigned i = 0; i < d_assertions.size(); ++ i) {
4063       d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
4064     }
4065   }
4066   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
4067   dumpAssertions("post-definition-expansion", d_assertions);
4068
4069   // save the assertions now
4070   THEORY_PROOF
4071     (
4072      for (unsigned i = 0; i < d_assertions.size(); ++i) {
4073        ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr());
4074      }
4075      );
4076
4077   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
4078
4079   if (options::sygusInference())
4080   {
4081     // try recast as sygus
4082     quantifiers::SygusInference si;
4083     if (si.simplify(d_assertions.ref()))
4084     {
4085       Trace("smt-proc") << "...converted to sygus conjecture." << std::endl;
4086       d_smt.d_globalNegation = !d_smt.d_globalNegation;
4087     }
4088   }
4089   else if (options::globalNegate())
4090   {
4091     // global negation of the formula
4092     quantifiers::GlobalNegate gn;
4093     gn.simplify(d_assertions.ref());
4094     d_smt.d_globalNegation = !d_smt.d_globalNegation;
4095   }
4096
4097   if( options::nlExtPurify() ){
4098     unordered_map<Node, Node, NodeHashFunction> cache;
4099     unordered_map<Node, Node, NodeHashFunction> bcache;
4100     std::vector< Node > var_eq;
4101     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4102       d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq));
4103     }
4104     if( !var_eq.empty() ){
4105       unsigned lastIndex = d_assertions.size()-1;
4106       var_eq.insert( var_eq.begin(), d_assertions[lastIndex] );
4107       d_assertions.replace(lastIndex, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) );
4108     }
4109   }
4110
4111   if( options::ceGuidedInst() ){
4112     //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
4113     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4114       d_smt.d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions[i] );
4115     }
4116   }
4117
4118   if (options::solveRealAsInt()) {
4119     Chat() << "converting reals to ints..." << endl;
4120     unordered_map<Node, Node, NodeHashFunction> cache;
4121     std::vector< Node > var_eq;
4122     for(unsigned i = 0; i < d_assertions.size(); ++ i) {
4123       d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq));
4124     }
4125    /*
4126     if( !var_eq.empty() ){
4127       unsigned lastIndex = d_assertions.size()-1;
4128       var_eq.insert( var_eq.begin(), d_assertions[lastIndex] );
4129       d_assertions.replace(last_index, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) );
4130     }
4131     */
4132   }
4133
4134   if (options::solveIntAsBV() > 0)
4135   {
4136     d_preprocessingPassRegistry.getPass("int-to-bv")->apply(&d_assertions);
4137   }
4138
4139   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
4140       !d_smt.d_logic.isPure(THEORY_BV) &&
4141       d_smt.d_logic.getLogicString() != "QF_UFBV" &&
4142       d_smt.d_logic.getLogicString() != "QF_ABV") {
4143     throw ModalException("Eager bit-blasting does not currently support theory combination. "
4144                          "Note that in a QF_BV problem UF symbols can be introduced for division. "
4145                          "Try --bv-div-zero-const to interpret division by zero as a constant.");
4146   }
4147
4148   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
4149     d_smt.d_theoryEngine->mkAckermanizationAssertions(d_assertions.ref());
4150   }
4151
4152   if ( options::bvAbstraction() &&
4153       !options::incrementalSolving()) {
4154     dumpAssertions("pre-bv-abstraction", d_assertions);
4155     bvAbstraction();
4156     dumpAssertions("post-bv-abstraction", d_assertions);
4157   }
4158
4159   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
4160
4161   bool noConflict = true;
4162
4163   if (options::extRewPrep())
4164   {
4165     theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg());
4166     for (unsigned i = 0; i < d_assertions.size(); ++i)
4167     {
4168       Node a = d_assertions[i];
4169       d_assertions.replace(i, extr.extendedRewrite(a));
4170     }
4171   }
4172
4173   // Unconstrained simplification
4174   if(options::unconstrainedSimp()) {
4175     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl;
4176     dumpAssertions("pre-unconstrained-simp", d_assertions);
4177     Chat() << "...doing unconstrained simplification..." << endl;
4178     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4179       d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
4180     }
4181     unconstrainedSimp();
4182     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl;
4183     dumpAssertions("post-unconstrained-simp", d_assertions);
4184   }
4185
4186   if(options::bvIntroducePow2()){
4187     theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
4188   }
4189
4190   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl;
4191   dumpAssertions("pre-substitution", d_assertions);
4192
4193   if(options::unsatCores()) {
4194     // special rewriting pass for unsat cores, since many of the passes below are skipped
4195     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4196       d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
4197     }
4198   } else {
4199     applySubstitutionsToAssertions();
4200   }
4201   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl;
4202   dumpAssertions("post-substitution", d_assertions);
4203
4204   // Assertions ARE guaranteed to be rewritten by this point
4205 #ifdef CVC4_ASSERTIONS
4206   for (unsigned i = 0; i < d_assertions.size(); ++i)
4207   {
4208     Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
4209   }
4210 #endif
4211
4212   // Lift bit-vectors of size 1 to bool
4213   if(options::bitvectorToBool()) {
4214     dumpAssertions("pre-bv-to-bool", d_assertions);
4215     Chat() << "...doing bvToBool..." << endl;
4216     bvToBool();
4217     dumpAssertions("post-bv-to-bool", d_assertions);
4218     Trace("smt") << "POST bvToBool" << endl;
4219   }
4220   // Convert non-top-level Booleans to bit-vectors of size 1
4221   if(options::boolToBitvector()) {
4222     dumpAssertions("pre-bool-to-bv", d_assertions);
4223     Chat() << "...doing boolToBv..." << endl;
4224     boolToBv();
4225     dumpAssertions("post-bool-to-bv", d_assertions);
4226     Trace("smt") << "POST boolToBv" << endl;
4227   }
4228   if(options::sepPreSkolemEmp()) {
4229     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4230       Node prev = d_assertions[i];
4231       Node next = sep::TheorySepRewriter::preprocess( prev );
4232       if( next!=prev ){
4233         d_assertions.replace( i, Rewriter::rewrite( next ) );
4234         Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl;
4235         Trace("sep-preprocess") << "   ...got " << d_assertions[i] << endl;
4236       }
4237     }
4238   }
4239
4240   if( d_smt.d_logic.isQuantified() ){
4241     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
4242
4243     dumpAssertions("pre-skolem-quant", d_assertions);
4244     //remove rewrite rules, apply pre-skolemization to existential quantifiers
4245     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4246       Node prev = d_assertions[i];
4247       Node next = quantifiers::QuantifiersRewriter::preprocess( prev );
4248       if( next!=prev ){
4249         d_assertions.replace( i, Rewriter::rewrite( next ) );
4250         Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
4251         Trace("quantifiers-preprocess") << "   ...got " << d_assertions[i] << endl;
4252       }
4253     }
4254     dumpAssertions("post-skolem-quant", d_assertions);
4255     if( options::macrosQuant() ){
4256       //quantifiers macro expansion
4257       quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() );
4258       bool success;
4259       do{
4260         success = qm.simplify( d_assertions.ref(), true );
4261       }while( success );
4262       //finalize the definitions
4263       qm.finalizeDefinitions();
4264     }
4265
4266     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
4267     if( options::fmfFunWellDefined() ){
4268       quantifiers::FunDefFmf fdf;
4269       Assert( d_smt.d_fmfRecFunctionsDefined!=NULL );
4270       //must carry over current definitions (for incremental)
4271       for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin();
4272            fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {
4273         Node f = (*fit);
4274         Assert( d_smt.d_fmfRecFunctionsAbs.find( f )!=d_smt.d_fmfRecFunctionsAbs.end() );
4275         TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f];
4276         fdf.d_sorts[f] = ft;
4277         std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f );
4278         Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete.end() );
4279         for( unsigned j=0; j<fcit->second.size(); j++ ){
4280           fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
4281         }
4282       }
4283       fdf.simplify( d_assertions.ref() );
4284       //must store new definitions (for incremental)
4285       for( unsigned i=0; i<fdf.d_funcs.size(); i++ ){
4286         Node f = fdf.d_funcs[i];
4287         d_smt.d_fmfRecFunctionsAbs[f] = fdf.d_sorts[f];
4288         d_smt.d_fmfRecFunctionsConcrete[f].clear();
4289         for( unsigned j=0; j<fdf.d_input_arg_inj[f].size(); j++ ){
4290           d_smt.d_fmfRecFunctionsConcrete[f].push_back( fdf.d_input_arg_inj[f][j] );
4291         }
4292         d_smt.d_fmfRecFunctionsDefined->push_back( f );
4293       }
4294     }
4295     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;
4296   }
4297
4298   if( options::sortInference() || options::ufssFairnessMonotone() ){
4299     //sort inference technique
4300     SortInference * si = d_smt.d_theoryEngine->getSortInference();
4301     si->simplify( d_assertions.ref(), options::sortInference(), options::ufssFairnessMonotone() );
4302     for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
4303       d_smt.setPrintFuncInModel( it->first.toExpr(), false );
4304       d_smt.setPrintFuncInModel( it->second.toExpr(), true );
4305     }
4306   }
4307
4308   if( options::pbRewrites() ){
4309     d_preprocessingPassRegistry.getPass("pseudo-boolean-processor")
4310         ->apply(&d_assertions);
4311   }
4312
4313   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;
4314   dumpAssertions("pre-simplify", d_assertions);
4315   Chat() << "simplifying assertions..." << endl;
4316   noConflict = simplifyAssertions();
4317   if(!noConflict){
4318     ++(d_smt.d_stats->d_simplifiedToFalse);
4319   }
4320   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-simplify" << endl;
4321   dumpAssertions("post-simplify", d_assertions);
4322
4323   if (options::symmetryDetect())
4324   {
4325     SymmetryDetect symd;
4326     vector<vector<Node>> part;
4327     symd.getPartition(part, d_assertions.ref());
4328   }
4329
4330   dumpAssertions("pre-static-learning", d_assertions);
4331   if(options::doStaticLearning()) {
4332     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-static-learning" << endl;
4333     // Perform static learning
4334     Chat() << "doing static learning..." << endl;
4335     Trace("simplify") << "SmtEnginePrivate::simplify(): "
4336                       << "performing static learning" << endl;
4337     staticLearning();
4338     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-static-learning" << endl;
4339   }
4340   dumpAssertions("post-static-learning", d_assertions);
4341
4342   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
4343
4344
4345   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl;
4346   dumpAssertions("pre-ite-removal", d_assertions);
4347   {
4348     Chat() << "removing term ITEs..." << endl;
4349     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime);
4350     // Remove ITEs, updating d_iteSkolemMap
4351     d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
4352     removeITEs();
4353     // This is needed because when solving incrementally, removeITEs may introduce
4354     // skolems that were solved for earlier and thus appear in the substitution
4355     // map.
4356     applySubstitutionsToAssertions();
4357     d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
4358   }
4359   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl;
4360   dumpAssertions("post-ite-removal", d_assertions);
4361
4362   dumpAssertions("pre-repeat-simplify", d_assertions);
4363   if(options::repeatSimp()) {
4364     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
4365     Chat() << "re-simplifying assertions..." << endl;
4366     ScopeCounter depth(d_simplifyAssertionsDepth);
4367     noConflict &= simplifyAssertions();
4368     if (noConflict) {
4369       // Need to fix up assertion list to maintain invariants:
4370       // Let Sk be the set of Skolem variables introduced by ITE's.  Let <_sk be the order in which these variables were introduced
4371       // during ite removal.
4372       // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
4373
4374       // cache for expression traversal
4375       unordered_map<Node, bool, NodeHashFunction> cache;
4376
4377       // First, find all skolems that appear in the substitution map - their associated iteExpr will need
4378       // to be moved to the main assertion set
4379       set<TNode> skolemSet;
4380       SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin();
4381       for (; pos != d_topLevelSubstitutions.end(); ++pos) {
4382         collectSkolems((*pos).first, skolemSet, cache);
4383         collectSkolems((*pos).second, skolemSet, cache);
4384       }
4385
4386       // We need to ensure:
4387       // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
4388       // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
4389       // If either of these is violated, we must add iteExpr as a proper assertion
4390       IteSkolemMap::iterator it = d_iteSkolemMap.begin();
4391       IteSkolemMap::iterator iend = d_iteSkolemMap.end();
4392       NodeBuilder<> builder(kind::AND);
4393       builder << d_assertions[d_realAssertionsEnd - 1];
4394       vector<TNode> toErase;
4395       for (; it != iend; ++it) {
4396         if (skolemSet.find((*it).first) == skolemSet.end()) {
4397           TNode iteExpr = d_assertions[(*it).second];
4398           if (iteExpr.getKind() == kind::ITE &&
4399               iteExpr[1].getKind() == kind::EQUAL &&
4400               iteExpr[1][0] == (*it).first &&
4401               iteExpr[2].getKind() == kind::EQUAL &&
4402               iteExpr[2][0] == (*it).first) {
4403             cache.clear();
4404             bool bad = checkForBadSkolems(iteExpr[0], (*it).first, cache);
4405             bad = bad || checkForBadSkolems(iteExpr[1][1], (*it).first, cache);
4406             bad = bad || checkForBadSkolems(iteExpr[2][1], (*it).first, cache);
4407             if (!bad) {
4408               continue;
4409             }
4410           }
4411         }
4412         // Move this iteExpr into the main assertions
4413         builder << d_assertions[(*it).second];
4414         d_assertions[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
4415         toErase.push_back((*it).first);
4416       }
4417       if(builder.getNumChildren() > 1) {
4418         while (!toErase.empty()) {
4419           d_iteSkolemMap.erase(toErase.back());
4420           toErase.pop_back();
4421         }
4422         d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
4423       }
4424       // TODO(b/1256): For some reason this is needed for some benchmarks, such as
4425       // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
4426       removeITEs();
4427       applySubstitutionsToAssertions();
4428       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
4429     }
4430     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
4431   }
4432   dumpAssertions("post-repeat-simplify", d_assertions);
4433
4434   dumpAssertions("pre-rewrite-apply-to-const", d_assertions);
4435   if(options::rewriteApplyToConst()) {
4436     Chat() << "Rewriting applies to constants..." << endl;
4437     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteApplyToConstTime);
4438     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4439       d_assertions[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertions[i]));
4440     }
4441   }
4442   dumpAssertions("post-rewrite-apply-to-const", d_assertions);
4443
4444   // begin: INVARIANT to maintain: no reordering of assertions or
4445   // introducing new ones
4446 #ifdef CVC4_ASSERTIONS
4447   unsigned iteRewriteAssertionsEnd = d_assertions.size();
4448 #endif
4449
4450   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
4451
4452   Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
4453   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
4454
4455   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-theory-preprocessing" << endl;
4456   dumpAssertions("pre-theory-preprocessing", d_assertions);
4457   {
4458     Chat() << "theory preprocessing..." << endl;
4459     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
4460     // Call the theory preprocessors
4461     d_smt.d_theoryEngine->preprocessStart();
4462     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4463       d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
4464     }
4465   }
4466   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-theory-preprocessing" << endl;
4467   dumpAssertions("post-theory-preprocessing", d_assertions);
4468
4469   // If we are using eager bit-blasting wrap assertions in fake atom so that
4470   // everything gets bit-blasted to internal SAT solver
4471   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
4472     for (unsigned i = 0; i < d_assertions.size(); ++i) {
4473       TNode atom = d_assertions[i];
4474       Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
4475       d_assertions.replace(i, eager_atom);
4476       TheoryModel* m = d_smt.d_theoryEngine->getModel();
4477       m->addSubstitution(eager_atom, atom);
4478     }
4479   }
4480
4481   //notify theory engine new preprocessed assertions
4482   d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() );
4483
4484   // Push the formula to decision engine
4485   if(noConflict) {
4486     Chat() << "pushing to decision engine..." << endl;
4487     Assert(iteRewriteAssertionsEnd == d_assertions.size());
4488     d_smt.d_decisionEngine->addAssertions
4489       (d_assertions.ref(), d_realAssertionsEnd, d_iteSkolemMap);
4490   }
4491
4492   // end: INVARIANT to maintain: no reordering of assertions or
4493   // introducing new ones
4494
4495   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
4496   dumpAssertions("post-everything", d_assertions);
4497
4498   // Push the formula to SAT
4499   {
4500     Chat() << "converting to CNF..." << endl;
4501     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
4502     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
4503       Chat() << "+ " << d_assertions[i] << std::endl;
4504       d_smt.d_propEngine->assertFormula(d_assertions[i]);
4505     }
4506   }
4507
4508   d_assertionsProcessed = true;
4509
4510   d_assertions.clear();
4511   d_iteSkolemMap.clear();
4512 }
4513
4514 void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
4515 {
4516   if (n == d_true) {
4517     // nothing to do
4518     return;
4519   }
4520
4521   Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl;
4522
4523   // Give it to proof manager
4524   PROOF(
4525     if( inInput ){
4526       // n is an input assertion
4527       if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
4528
4529         ProofManager::currentPM()->addCoreAssertion(n.toExpr());
4530       }
4531     }else{
4532       // n is the result of an unknown preprocessing step, add it to dependency map to null
4533       ProofManager::currentPM()->addDependence(n, Node::null());
4534     }
4535     // rewrite rules are by default in the unsat core because
4536     // they need to be applied until saturation
4537     if(options::unsatCores() &&
4538        n.getKind() == kind::REWRITE_RULE ){
4539       ProofManager::currentPM()->addUnsatCore(n.toExpr());
4540     }
4541   );
4542
4543   // Add the normalized formula to the queue
4544   d_assertions.push_back(n);
4545   //d_assertions.push_back(Rewriter::rewrite(n));
4546 }
4547
4548 void SmtEngine::ensureBoolean(const Expr& e)
4549 {
4550   Type type = e.getType(options::typeChecking());
4551   Type boolType = d_exprManager->booleanType();
4552   if(type != boolType) {
4553     stringstream ss;
4554     ss << "Expected " << boolType << "\n"
4555        << "The assertion : " << e << "\n"
4556        << "Its type      : " << type;
4557     throw TypeCheckingException(e, ss.str());
4558   }
4559 }
4560
4561 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
4562 {
4563   return checkSatisfiability(assumption, inUnsatCore, false);
4564 }
4565
4566 Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
4567 {
4568   return checkSatisfiability(assumptions, inUnsatCore, false);
4569 }
4570
4571 Result SmtEngine::query(const Expr& assumption, bool inUnsatCore)
4572 {
4573   Assert(!assumption.isNull());
4574   return checkSatisfiability(assumption, inUnsatCore, true);
4575 }
4576
4577 Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore)
4578 {
4579   return checkSatisfiability(assumptions, inUnsatCore, true);
4580 }
4581
4582 Result SmtEngine::checkSatisfiability(const Expr& expr,
4583                                       bool inUnsatCore,
4584                                       bool isQuery)
4585 {
4586   return checkSatisfiability(
4587       expr.isNull() ? vector<Expr>() : vector<Expr>{expr},
4588       inUnsatCore,
4589       isQuery);
4590 }
4591
4592 Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
4593                                       bool inUnsatCore,
4594                                       bool isQuery)
4595 {
4596   try
4597   {
4598     SmtScope smts(this);
4599     finalOptionsAreSet();
4600     doPendingPops();
4601
4602     Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
4603                  << assumptions << ")" << endl;
4604
4605     if(d_queryMade && !options::incrementalSolving()) {
4606       throw ModalException("Cannot make multiple queries unless "
4607                            "incremental solving is enabled "
4608                            "(try --incremental)");
4609     }
4610
4611     // check to see if a postsolve() is pending
4612     if(d_needPostsolve) {
4613       d_theoryEngine->postsolve();
4614       d_needPostsolve = false;
4615     }
4616     // Note that a query has been made
4617     d_queryMade = true;
4618     // reset global negation
4619     d_globalNegation = false;
4620
4621     bool didInternalPush = false;
4622
4623     setProblemExtended(true);
4624
4625     if (isQuery)
4626     {
4627       size_t size = assumptions.size();
4628       if (size > 1)
4629       {
4630         /* Assume: not (BIGAND assumptions)  */
4631         d_assumptions.push_back(
4632             d_exprManager->mkExpr(kind::AND, assumptions).notExpr());
4633       }
4634       else if (size == 1)
4635       {
4636         /* Assume: not expr  */
4637         d_assumptions.push_back(assumptions[0].notExpr());
4638       }
4639     }
4640     else
4641     {
4642       /* Assume: BIGAND assumptions  */
4643       d_assumptions = assumptions;
4644     }
4645
4646     Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
4647     for (Expr e : d_assumptions)
4648     {
4649       // Substitute out any abstract values in ex.
4650       e = d_private->substituteAbstractValues(Node::fromExpr(e)).toExpr();
4651       Assert(e.getExprManager() == d_exprManager);
4652       // Ensure expr is type-checked at this point.
4653       ensureBoolean(e);
4654
4655       /* Add assumption  */
4656       internalPush();
4657       didInternalPush = true;
4658       if (d_assertionList != NULL)
4659       {
4660         d_assertionList->push_back(e);
4661       }
4662       d_private->addFormula(e.getNode(), inUnsatCore);
4663     }
4664
4665     r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult();
4666
4667     if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
4668         && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
4669     {
4670       r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
4671     }
4672     // flipped if we did a global negation
4673     if (d_globalNegation)
4674     {
4675       Trace("smt") << "SmtEngine::process global negate " << r << std::endl;
4676       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
4677       {
4678         r = Result(Result::SAT);
4679       }
4680       else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
4681       {
4682         // only if satisfaction complete
4683         if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
4684         {
4685           r = Result(Result::UNSAT);
4686         }
4687         else
4688         {
4689           r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
4690         }
4691       }
4692       Trace("smt") << "SmtEngine::global negate returned " << r << std::endl;
4693     }
4694
4695     d_needPostsolve = true;
4696
4697     // Dump the query if requested
4698     if (Dump.isOn("benchmark"))
4699     {
4700       size_t size = assumptions.size();
4701       // the expr already got dumped out if assertion-dumping is on
4702       if (isQuery && size == 1)
4703       {
4704         Dump("benchmark") << QueryCommand(assumptions[0]);
4705       }
4706       else if (size == 0)
4707       {
4708         Dump("benchmark") << CheckSatCommand();
4709       }
4710       else
4711       {
4712         Dump("benchmark") << CheckSatAssumingCommand(d_assumptions,
4713                                                      inUnsatCore);
4714       }
4715     }
4716
4717     // Pop the context
4718     if (didInternalPush)
4719     {
4720       internalPop();
4721     }
4722
4723     // Remember the status
4724     d_status = r;
4725
4726     setProblemExtended(false);
4727
4728     Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
4729                  << assumptions << ") => " << r << endl;
4730
4731     // Check that SAT results generate a model correctly.
4732     if(options::checkModels()) {
4733       // TODO (#1693) check model when unknown result?
4734       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
4735       {
4736         checkModel();
4737       }
4738     }
4739     // Check that UNSAT results generate a proof correctly.
4740     if(options::checkProofs()) {
4741       if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
4742         TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
4743         checkProof();
4744       }
4745     }
4746     // Check that UNSAT results generate an unsat core correctly.
4747     if(options::checkUnsatCores()) {
4748       if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
4749         TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
4750         checkUnsatCore();
4751       }
4752     }
4753     // Check that synthesis solutions satisfy the conjecture
4754     if (options::checkSynthSol()
4755         && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
4756     {
4757       checkSynthSolution();
4758     }
4759
4760     return r;
4761   } catch (UnsafeInterruptException& e) {
4762     AlwaysAssert(d_private->getResourceManager()->out());
4763     Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ?
4764       Result::RESOURCEOUT : Result::TIMEOUT;
4765     return Result(Result::SAT_UNKNOWN, why, d_filename);
4766   }
4767 }
4768
4769 vector<Expr> SmtEngine::getUnsatAssumptions(void)
4770 {
4771   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
4772   SmtScope smts(this);
4773   if (!options::unsatAssumptions())
4774   {
4775     throw ModalException(
4776         "Cannot get unsat assumptions when produce-unsat-assumptions option "
4777         "is off.");
4778   }
4779   if (d_status.isNull()
4780       || d_status.asSatisfiabilityResult() != Result::UNSAT
4781       || d_problemExtended)
4782   {
4783     throw RecoverableModalException(
4784         "Cannot get unsat assumptions unless immediately preceded by "
4785         "UNSAT/VALID response.");
4786   }
4787   finalOptionsAreSet();
4788   if (Dump.isOn("benchmark"))
4789   {
4790     Dump("benchmark") << GetUnsatCoreCommand();
4791   }
4792   UnsatCore core = getUnsatCore();
4793   vector<Expr> res;
4794   for (const Expr& e : d_assumptions)
4795   {
4796     if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); }
4797   }
4798   return res;
4799 }
4800
4801 Result SmtEngine::checkSynth(const Expr& e)
4802 {
4803   SmtScope smts(this);
4804   Trace("smt") << "Check synth: " << e << std::endl;
4805   Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
4806   Expr e_check = e;
4807   if (options::sygusQePreproc())
4808   {
4809     // the following does quantifier elimination as a preprocess step
4810     // for "non-ground single invocation synthesis conjectures":
4811     //   exists f. forall xy. P[ f(x), x, y ]
4812     // We run quantifier elimination:
4813     //   exists y. P[ z, x, y ] ----> Q[ z, x ]
4814     // Where we replace the original conjecture with:
4815     //   exists f. forall x. Q[ f(x), x ]
4816     // For more details, see Example 6 of Reynolds et al. SYNT 2017.
4817     Node conj = Node::fromExpr(e);
4818     if (conj.getKind() == kind::FORALL && conj[1].getKind() == kind::EXISTS)
4819     {
4820       Node conj_se = Node::fromExpr(expandDefinitions(conj[1][1].toExpr()));
4821
4822       Trace("smt-synth") << "Compute single invocation for " << conj_se << "..."
4823                          << std::endl;
4824       quantifiers::SingleInvocationPartition sip;
4825       std::vector<Node> funcs;
4826       funcs.insert(funcs.end(), conj[0].begin(), conj[0].end());
4827       sip.init(funcs, conj_se.negate());
4828       Trace("smt-synth") << "...finished, got:" << std::endl;
4829       sip.debugPrint("smt-synth");
4830
4831       if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
4832       {
4833         // create new smt engine to do quantifier elimination
4834         SmtEngine smt_qe(d_exprManager);
4835         smt_qe.setLogic(getLogicInfo());
4836         Trace("smt-synth") << "Property is non-ground single invocation, run "
4837                               "QE to obtain single invocation."
4838                            << std::endl;
4839         NodeManager* nm = NodeManager::currentNM();
4840         // partition variables
4841         std::vector<Node> all_vars;
4842         sip.getAllVariables(all_vars);
4843         std::vector<Node> si_vars;
4844         sip.getSingleInvocationVariables(si_vars);
4845         std::vector<Node> qe_vars;
4846         std::vector<Node> nqe_vars;
4847         for (unsigned i = 0, size = all_vars.size(); i < size; i++)
4848         {
4849           Node v = all_vars[i];
4850           if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
4851           {
4852             qe_vars.push_back(v);
4853           }
4854           else
4855           {
4856             nqe_vars.push_back(v);
4857           }
4858         }
4859         std::vector<Node> orig;
4860         std::vector<Node> subs;
4861         // skolemize non-qe variables
4862         for (unsigned i = 0; i < nqe_vars.size(); i++)
4863         {
4864           Node k = nm->mkSkolem("k",
4865                                 nqe_vars[i].getType(),
4866                                 "qe for non-ground single invocation");
4867           orig.push_back(nqe_vars[i]);
4868           subs.push_back(k);
4869           Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k
4870                              << std::endl;
4871         }
4872         std::vector<Node> funcs;
4873         sip.getFunctions(funcs);
4874         for (unsigned i = 0, size = funcs.size(); i < size; i++)
4875         {
4876           Node f = funcs[i];
4877           Node fi = sip.getFunctionInvocationFor(f);
4878           Node fv = sip.getFirstOrderVariableForFunction(f);
4879           Assert(!fi.isNull());
4880           orig.push_back(fi);
4881           Node k =
4882               nm->mkSkolem("k",
4883                            fv.getType(),
4884                            "qe for function in non-ground single invocation");
4885           subs.push_back(k);
4886           Trace("smt-synth") << "  subs : " << fi << " -> " << k << std::endl;
4887         }
4888         Node conj_se_ngsi = sip.getFullSpecification();
4889         Trace("smt-synth") << "Full specification is " << conj_se_ngsi
4890                            << std::endl;
4891         Node conj_se_ngsi_subs = conj_se_ngsi.substitute(
4892             orig.begin(), orig.end(), subs.begin(), subs.end());
4893         Assert(!qe_vars.empty());
4894         conj_se_ngsi_subs =
4895             nm->mkNode(kind::EXISTS,
4896                        nm->mkNode(kind::BOUND_VAR_LIST, qe_vars),
4897                        conj_se_ngsi_subs.negate());
4898
4899         Trace("smt-synth") << "Run quantifier elimination on "
4900                            << conj_se_ngsi_subs << std::endl;
4901         Expr qe_res = smt_qe.doQuantifierElimination(
4902             conj_se_ngsi_subs.toExpr(), true, false);
4903         Trace("smt-synth") << "Result : " << qe_res << std::endl;
4904
4905         // create single invocation conjecture
4906         Node qe_res_n = Node::fromExpr(qe_res);
4907         qe_res_n = qe_res_n.substitute(
4908             subs.begin(), subs.end(), orig.begin(), orig.end());
4909         if (!nqe_vars.empty())
4910         {
4911           qe_res_n = nm->mkNode(kind::EXISTS,
4912                                 nm->mkNode(kind::BOUND_VAR_LIST, nqe_vars),
4913                                 qe_res_n);
4914         }
4915         Assert(conj.getNumChildren() == 3);
4916         qe_res_n = nm->mkNode(kind::FORALL, conj[0], qe_res_n, conj[2]);
4917         Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n
4918                            << std::endl;
4919         e_check = qe_res_n.toExpr();
4920       }
4921     }
4922   }
4923
4924   return checkSatisfiability( e_check, true, false );
4925 }
4926
4927 Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
4928 {
4929   Assert(ex.getExprManager() == d_exprManager);
4930   SmtScope smts(this);
4931   finalOptionsAreSet();
4932   doPendingPops();
4933
4934   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
4935
4936   if (Dump.isOn("raw-benchmark")) {
4937     Dump("raw-benchmark") << AssertCommand(ex);
4938   }
4939
4940   // Substitute out any abstract values in ex
4941   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
4942
4943   ensureBoolean(e);
4944   if(d_assertionList != NULL) {
4945     d_assertionList->push_back(e);
4946   }
4947   d_private->addFormula(e.getNode(), inUnsatCore);
4948   return quickCheck().asValidityResult();
4949 }/* SmtEngine::assertFormula() */
4950
4951 Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
4952   return node;
4953 }
4954
4955 Expr SmtEngine::simplify(const Expr& ex)
4956 {
4957   Assert(ex.getExprManager() == d_exprManager);
4958   SmtScope smts(this);
4959   finalOptionsAreSet();
4960   doPendingPops();
4961   Trace("smt") << "SMT simplify(" << ex << ")" << endl;
4962
4963   if(Dump.isOn("benchmark")) {
4964     Dump("benchmark") << SimplifyCommand(ex);
4965   }
4966
4967   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
4968   if( options::typeChecking() ) {
4969     e.getType(true); // ensure expr is type-checked at this point
4970   }
4971
4972   // Make sure all preprocessing is done
4973   d_private->processAssertions();
4974   Node n = d_private->simplify(Node::fromExpr(e));
4975   n = postprocess(n, TypeNode::fromType(e.getType()));
4976   return n.toExpr();
4977 }
4978
4979 Expr SmtEngine::expandDefinitions(const Expr& ex)
4980 {
4981   d_private->spendResource(options::preprocessStep());
4982
4983   Assert(ex.getExprManager() == d_exprManager);
4984   SmtScope smts(this);
4985   finalOptionsAreSet();
4986   doPendingPops();
4987   Trace("smt") << "SMT expandDefinitions(" << ex << ")" << endl;
4988
4989   // Substitute out any abstract values in ex.
4990   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
4991   if(options::typeChecking()) {
4992     // Ensure expr is type-checked at this point.
4993     e.getType(true);
4994   }
4995   if(Dump.isOn("benchmark")) {
4996     Dump("benchmark") << ExpandDefinitionsCommand(e);
4997   }
4998   unordered_map<Node, Node, NodeHashFunction> cache;
4999   Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
5000   n = postprocess(n, TypeNode::fromType(e.getType()));
5001
5002   return n.toExpr();
5003 }
5004
5005 // TODO(#1108): Simplify the error reporting of this method.
5006 Expr SmtEngine::getValue(const Expr& ex) const
5007 {
5008   Assert(ex.getExprManager() == d_exprManager);
5009   SmtScope smts(this);
5010
5011   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
5012   if(Dump.isOn("benchmark")) {
5013     Dump("benchmark") << GetValueCommand(ex);
5014   }
5015
5016   if(!options::produceModels()) {
5017     const char* msg =
5018       "Cannot get value when produce-models options is off.";
5019     throw ModalException(msg);
5020   }
5021   if(d_status.isNull() ||
5022      d_status.asSatisfiabilityResult() == Result::UNSAT ||
5023      d_problemExtended) {
5024     const char* msg =
5025       "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
5026     throw RecoverableModalException(msg);
5027   }
5028
5029   // Substitute out any abstract values in ex.
5030   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
5031
5032   // Ensure expr is type-checked at this point.
5033   e.getType(options::typeChecking());
5034
5035   // do not need to apply preprocessing substitutions (should be recorded
5036   // in model already)
5037
5038   Node n = Node::fromExpr(e);
5039   Trace("smt") << "--- getting value of " << n << endl;
5040   TypeNode expectedType = n.getType();
5041
5042   // Expand, then normalize
5043   unordered_map<Node, Node, NodeHashFunction> cache;
5044   n = d_private->expandDefinitions(n, cache);
5045   // There are two ways model values for terms are computed (for historical
5046   // reasons).  One way is that used in check-model; the other is that
5047   // used by the Model classes.  It's not clear to me exactly how these
5048   // two are different, but they need to be unified.  This ugly hack here
5049   // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
5050
5051   //AJR : necessary?
5052   if(!n.getType().isFunction()) {
5053     n = Rewriter::rewrite(n);
5054   }
5055
5056   Trace("smt") << "--- getting value of " << n << endl;
5057   TheoryModel* m = d_theoryEngine->getModel();
5058   Node resultNode;
5059   if(m != NULL) {
5060     resultNode = m->getValue(n);
5061   }
5062   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
5063   resultNode = postprocess(resultNode, expectedType);
5064   Trace("smt") << "--- model-post returned " << resultNode << endl;
5065   Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
5066   Trace("smt") << "--- model-post expected " << expectedType << endl;
5067
5068   // type-check the result we got
5069   Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType),
5070          "Run with -t smt for details.");
5071
5072   // ensure it's a constant
5073   Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst());
5074
5075   if(options::abstractValues() && resultNode.getType().isArray()) {
5076     resultNode = d_private->mkAbstractValue(resultNode);
5077     Trace("smt") << "--- abstract value >> " << resultNode << endl;
5078   }
5079
5080   return resultNode.toExpr();
5081 }
5082
5083 bool SmtEngine::addToAssignment(const Expr& ex) {
5084   SmtScope smts(this);
5085   finalOptionsAreSet();
5086   doPendingPops();
5087   // Substitute out any abstract values in ex
5088   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
5089   Type type = e.getType(options::typeChecking());
5090   // must be Boolean
5091   PrettyCheckArgument(
5092       type.isBoolean(), e,
5093       "expected Boolean-typed variable or function application "
5094       "in addToAssignment()" );
5095   Node n = e.getNode();
5096   // must be an APPLY of a zero-ary defined function, or a variable
5097   PrettyCheckArgument(
5098       ( ( n.getKind() == kind::APPLY &&
5099           ( d_definedFunctions->find(n.getOperator()) !=
5100             d_definedFunctions->end() ) &&
5101           n.getNumChildren() == 0 ) ||
5102         n.isVar() ), e,
5103       "expected variable or defined-function application "
5104       "in addToAssignment(),\ngot %s", e.toString().c_str() );
5105   if(!options::produceAssignments()) {
5106     return false;
5107   }
5108   if(d_assignments == NULL) {
5109     d_assignments = new(true) AssignmentSet(d_context);
5110   }
5111   d_assignments->insert(n);
5112
5113   return true;
5114 }
5115
5116 // TODO(#1108): Simplify the error reporting of this method.
5117 vector<pair<Expr, Expr>> SmtEngine::getAssignment()
5118 {
5119   Trace("smt") << "SMT getAssignment()" << endl;
5120   SmtScope smts(this);
5121   finalOptionsAreSet();
5122   if(Dump.isOn("benchmark")) {
5123     Dump("benchmark") << GetAssignmentCommand();
5124   }
5125   if(!options::produceAssignments()) {
5126     const char* msg =
5127       "Cannot get the current assignment when "
5128       "produce-assignments option is off.";
5129     throw ModalException(msg);
5130   }
5131   if(d_status.isNull() ||
5132      d_status.asSatisfiabilityResult() == Result::UNSAT  ||
5133      d_problemExtended) {
5134     const char* msg =
5135       "Cannot get the current assignment unless immediately "
5136       "preceded by SAT/INVALID or UNKNOWN response.";
5137     throw RecoverableModalException(msg);
5138   }
5139
5140   vector<pair<Expr,Expr>> res;
5141   if (d_assignments != nullptr)
5142   {
5143     TypeNode boolType = d_nodeManager->booleanType();
5144     TheoryModel* m = d_theoryEngine->getModel();
5145     for (AssignmentSet::key_iterator i = d_assignments->key_begin(),
5146                                      iend = d_assignments->key_end();
5147          i != iend;
5148          ++i)
5149     {
5150       Node as = *i;
5151       Assert(as.getType() == boolType);
5152
5153       Trace("smt") << "--- getting value of " << as << endl;
5154
5155       // Expand, then normalize
5156       unordered_map<Node, Node, NodeHashFunction> cache;
5157       Node n = d_private->expandDefinitions(as, cache);
5158       n = Rewriter::rewrite(n);
5159
5160       Trace("smt") << "--- getting value of " << n << endl;
5161       Node resultNode;
5162       if (m != nullptr)
5163       {
5164         resultNode = m->getValue(n);
5165       }
5166
5167       // type-check the result we got
5168       Assert(resultNode.isNull() || resultNode.getType() == boolType);
5169
5170       // ensure it's a constant
5171       Assert(resultNode.isConst());
5172
5173       Assert(as.getKind() == kind::APPLY || as.isVar());
5174       Assert(as.getKind() != kind::APPLY || as.getNumChildren() == 0);
5175       res.emplace_back(as.toExpr(), resultNode.toExpr());
5176     }
5177   }
5178   return res;
5179 }
5180
5181 void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool userVisible, const char* dumpTag) {
5182   Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl;
5183   SmtScope smts(this);
5184   // If we aren't yet fully inited, the user might still turn on
5185   // produce-models.  So let's keep any commands around just in
5186   // case.  This is useful in two cases: (1) SMT-LIBv1 auto-declares
5187   // sort "U" in QF_UF before setLogic() is run and we still want to
5188   // support finding card(U) with --finite-model-find, and (2) to
5189   // decouple SmtEngine and ExprManager if the user does a few
5190   // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
5191   // and expects to find their cardinalities in the model.
5192   if(/* userVisible && */
5193      (!d_fullyInited || options::produceModels()) &&
5194      (flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
5195     doPendingPops();
5196     if(flags & ExprManager::VAR_FLAG_GLOBAL) {
5197       d_modelGlobalCommands.push_back(c.clone());
5198     } else {
5199       d_modelCommands->push_back(c.clone());
5200     }
5201   }
5202   if(Dump.isOn(dumpTag)) {
5203     if(d_fullyInited) {
5204       Dump(dumpTag) << c;
5205     } else {
5206       d_dumpCommands.push_back(c.clone());
5207     }
5208   }
5209 }
5210
5211 // TODO(#1108): Simplify the error reporting of this method.
5212 Model* SmtEngine::getModel() {
5213   Trace("smt") << "SMT getModel()" << endl;
5214   SmtScope smts(this);
5215
5216   finalOptionsAreSet();
5217
5218   if(Dump.isOn("benchmark")) {
5219     Dump("benchmark") << GetModelCommand();
5220   }
5221
5222   if(d_status.isNull() ||
5223      d_status.asSatisfiabilityResult() == Result::UNSAT ||
5224      d_problemExtended) {
5225     const char* msg =
5226       "Cannot get the current model unless immediately "
5227       "preceded by SAT/INVALID or UNKNOWN response.";
5228     throw RecoverableModalException(msg);
5229   }
5230   if(!options::produceModels()) {
5231     const char* msg =
5232       "Cannot get model when produce-models options is off.";
5233     throw ModalException(msg);
5234   }
5235   TheoryModel* m = d_theoryEngine->getModel();
5236   m->d_inputName = d_filename;
5237   return m;
5238 }
5239
5240 void SmtEngine::checkUnsatCore() {
5241   Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
5242
5243   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
5244   UnsatCore core = getUnsatCore();
5245
5246   SmtEngine coreChecker(d_exprManager);
5247   coreChecker.setLogic(getLogicInfo());
5248
5249   PROOF(
5250   std::vector<Command*>::const_iterator itg = d_defineCommands.begin();
5251   for (; itg != d_defineCommands.end();  ++itg) {
5252     (*itg)->invoke(&coreChecker);
5253   }
5254   );
5255
5256   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
5257   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
5258     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;
5259     coreChecker.assertFormula(*i);
5260   }
5261   const bool checkUnsatCores = options::checkUnsatCores();
5262   Result r;
5263   try {
5264     options::checkUnsatCores.set(false);
5265     options::checkProofs.set(false);
5266     r = coreChecker.checkSat();
5267   } catch(...) {
5268     options::checkUnsatCores.set(checkUnsatCores);
5269     throw;
5270   }
5271   Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
5272   if(r.asSatisfiabilityResult().isUnknown()) {
5273     InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
5274   }
5275
5276   if(r.asSatisfiabilityResult().isSat()) {
5277     InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
5278   }
5279 }
5280
5281 void SmtEngine::checkModel(bool hardFailure) {
5282   // --check-model implies --produce-assertions, which enables the
5283   // assertion list, so we should be ok.
5284   Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()");
5285
5286   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
5287
5288   // Throughout, we use Notice() to give diagnostic output.
5289   //
5290   // If this function is running, the user gave --check-model (or equivalent),
5291   // and if Notice() is on, the user gave --verbose (or equivalent).
5292
5293   Notice() << "SmtEngine::checkModel(): generating model" << endl;
5294   TheoryModel* m = d_theoryEngine->getModel();
5295
5296   // Check individual theory assertions
5297   d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure);
5298
5299   // Output the model
5300   Notice() << *m;
5301
5302   // We have a "fake context" for the substitution map (we don't need it
5303   // to be context-dependent)
5304   context::Context fakeContext;
5305   SubstitutionMap substitutions(&fakeContext, /* substituteUnderQuantifiers = */ false);
5306
5307   for(size_t k = 0; k < m->getNumCommands(); ++k) {
5308     const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k));
5309     Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl;
5310     if(c == NULL) {
5311       // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
5312       Notice() << "SmtEngine::checkModel(): skipping..." << endl;
5313     } else {
5314       // We have a DECLARE-FUN:
5315       //
5316       // We'll first do some checks, then add to our substitution map
5317       // the mapping: function symbol |-> value
5318
5319       Expr func = c->getFunction();
5320       Node val = m->getValue(func);
5321
5322       Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
5323
5324       // (1) if the value is a lambda, ensure the lambda doesn't contain the
5325       // function symbol (since then the definition is recursive)
5326       if (val.getKind() == kind::LAMBDA) {
5327         // first apply the model substitutions we have so far
5328         Debug("boolean-terms") << "applying subses to " << val[1] << endl;
5329         Node n = substitutions.apply(val[1]);
5330         Debug("boolean-terms") << "++ got " << n << endl;
5331         // now check if n contains func by doing a substitution
5332         // [func->func2] and checking equality of the Nodes.
5333         // (this just a way to check if func is in n.)
5334         SubstitutionMap subs(&fakeContext);
5335         Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY);
5336         subs.addSubstitution(func, func2);
5337         if(subs.apply(n) != n) {
5338           Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl;
5339           stringstream ss;
5340           ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5341              << "considering model value for " << func << endl
5342              << "body of lambda is:   " << val << endl;
5343           if(n != val[1]) {
5344             ss << "body substitutes to: " << n << endl;
5345           }
5346           ss << "so " << func << " is defined in terms of itself." << endl
5347              << "Run with `--check-models -v' for additional diagnostics.";
5348           InternalError(ss.str());
5349         }
5350       }
5351
5352       // (2) check that the value is actually a value
5353       else if (!val.isConst()) {
5354         Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
5355         stringstream ss;
5356         ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5357            << "model value for " << func << endl
5358            << "             is " << val << endl
5359            << "and that is not a constant (.isConst() == false)." << endl
5360            << "Run with `--check-models -v' for additional diagnostics.";
5361         InternalError(ss.str());
5362       }
5363
5364       // (3) check that it's the correct (sub)type
5365       // This was intended to be a more general check, but for now we can't do that because
5366       // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
5367       else if(func.getType().isInteger() && !val.getType().isInteger()) {
5368         Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl;
5369         stringstream ss;
5370         ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5371            << "model value for " << func << endl
5372            << "             is " << val << endl
5373            << "value type is     " << val.getType() << endl
5374            << "should be of type " << func.getType() << endl
5375            << "Run with `--check-models -v' for additional diagnostics.";
5376         InternalError(ss.str());
5377       }
5378
5379       // (4) checks complete, add the substitution
5380       Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl;
5381       substitutions.addSubstitution(func, val);
5382     }
5383   }
5384
5385   // Now go through all our user assertions checking if they're satisfied.
5386   for(AssertionList::const_iterator i = d_assertionList->begin(); i != d_assertionList->end(); ++i) {
5387     Notice() << "SmtEngine::checkModel(): checking assertion " << *i << endl;
5388     Node n = Node::fromExpr(*i);
5389
5390     // Apply any define-funs from the problem.
5391     {
5392       unordered_map<Node, Node, NodeHashFunction> cache;
5393       n = d_private->expandDefinitions(n, cache);
5394     }
5395     Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
5396
5397     // Apply our model value substitutions.
5398     Debug("boolean-terms") << "applying subses to " << n << endl;
5399     n = substitutions.apply(n);
5400     Debug("boolean-terms") << "++ got " << n << endl;
5401     Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
5402
5403     if( n.getKind() != kind::REWRITE_RULE ){
5404       // In case it's a quantifier (or contains one), look up its value before
5405       // simplifying, or the quantifier might be irreparably altered.
5406       n = m->getValue(n);
5407       Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
5408     } else {
5409       // Note this "skip" is done here, rather than above.  This is
5410       // because (1) the quantifier could in principle simplify to false,
5411       // which should be reported, and (2) checking for the quantifier
5412       // above, before simplification, doesn't catch buried quantifiers
5413       // anyway (those not at the top-level).
5414       Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
5415                << endl;
5416       continue;
5417     }
5418
5419     // Simplify the result.
5420     n = d_private->simplify(n);
5421     Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
5422
5423     // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
5424     n = d_private->d_iteRemover.replace(n);
5425     Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl;
5426
5427     // Apply our model value substitutions (again), as things may have been simplified.
5428     Debug("boolean-terms") << "applying subses to " << n << endl;
5429     n = substitutions.apply(n);
5430     Debug("boolean-terms") << "++ got " << n << endl;
5431     Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n << endl;
5432
5433     // As a last-ditch effort, ask model to simplify it.
5434     // Presently, this is only an issue for quantifiers, which can have a value
5435     // but don't show up in our substitution map above.
5436     n = m->getValue(n);
5437     Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl;
5438
5439     if( d_logic.isQuantified() ){
5440       // AJR: since quantified formulas are not checkable, we assign them to true/false based on the satisfying assignment.
5441       // however, quantified formulas can be modified during preprocess, so they may not correspond to those in the satisfying assignment.
5442       // hence we use a relaxed version of check model here.
5443       // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas
5444       if( hardFailure && !n.isConst() && n.getKind() != kind::LAMBDA ){
5445         Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl;
5446         AlwaysAssert( quantifiers::QuantifiersRewriter::containsQuantifiers( n ) );
5447         Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n << endl;
5448         continue;
5449       }
5450     }else{
5451       AlwaysAssert(!hardFailure || n.isConst() || n.getKind() == kind::LAMBDA);
5452     }
5453     // The result should be == true.
5454     if(n != NodeManager::currentNM()->mkConst(true)) {
5455       Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
5456                << endl;
5457       stringstream ss;
5458       ss << "SmtEngine::checkModel(): "
5459          << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
5460          << "assertion:     " << *i << endl
5461          << "simplifies to: " << n << endl
5462          << "expected `true'." << endl
5463          << "Run with `--check-models -v' for additional diagnostics.";
5464       if(hardFailure) {
5465         InternalError(ss.str());
5466       } else {
5467         Warning() << ss.str() << endl;
5468       }
5469     }
5470   }
5471   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
5472 }
5473
5474 void SmtEngine::checkSynthSolution()
5475 {
5476   NodeManager* nm = NodeManager::currentNM();
5477   Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl;
5478   map<Node, Node> sol_map;
5479   /* Get solutions and build auxiliary vectors for substituting */
5480   d_theoryEngine->getSynthSolutions(sol_map);
5481   Trace("check-synth-sol") << "Got solution map:\n";
5482   std::vector<Node> function_vars, function_sols;
5483   for (const auto& pair : sol_map)
5484   {
5485     Trace("check-synth-sol") << pair.first << " --> " << pair.second << "\n";
5486     function_vars.push_back(pair.first);
5487     function_sols.push_back(pair.second);
5488   }
5489   Trace("check-synth-sol") << "Starting new SMT Engine\n";
5490   /* Start new SMT engine to check solutions */
5491   SmtEngine solChecker(d_exprManager);
5492   solChecker.setLogic(getLogicInfo());
5493   setOption("check-synth-sol", SExpr("false"));
5494
5495   Trace("check-synth-sol") << "Retrieving assertions\n";
5496   // Build conjecture from original assertions
5497   if (d_assertionList == NULL)
5498   {
5499     Trace("check-synth-sol") << "No assertions to check\n";
5500     return;
5501   }
5502   for (AssertionList::const_iterator i = d_assertionList->begin();
5503        i != d_assertionList->end();
5504        ++i)
5505   {
5506     Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i << endl;
5507     Trace("check-synth-sol") << "Retrieving assertion " << *i << "\n";
5508     Node conj = Node::fromExpr(*i);
5509     // Apply any define-funs from the problem.
5510     {
5511       unordered_map<Node, Node, NodeHashFunction> cache;
5512       conj = d_private->expandDefinitions(conj, cache);
5513     }
5514     Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << conj << endl;
5515     Trace("check-synth-sol") << "Expanded assertion " << conj << "\n";
5516
5517     // Apply solution map to conjecture body
5518     Node conjBody;
5519     /* Whether property is quantifier free */
5520     if (conj[1].getKind() != kind::EXISTS)
5521     {
5522       conjBody = conj[1].substitute(function_vars.begin(),
5523                                     function_vars.end(),
5524                                     function_sols.begin(),
5525                                     function_sols.end());
5526     }
5527     else
5528     {
5529       conjBody = conj[1][1].substitute(function_vars.begin(),
5530                                        function_vars.end(),
5531                                        function_sols.begin(),
5532                                        function_sols.end());
5533
5534       /* Skolemize property */
5535       std::vector<Node> vars, skos;
5536       for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j)
5537       {
5538         vars.push_back(conj[1][0][j]);
5539         std::stringstream ss;
5540         ss << "sk_" << j;
5541         skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType()));
5542         Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
5543                                  << skos.back() << "\n";
5544       }
5545       conjBody = conjBody.substitute(
5546           vars.begin(), vars.end(), skos.begin(), skos.end());
5547     }
5548     Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
5549              << conjBody << endl;
5550     Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
5551                              << "\n";
5552     solChecker.assertFormula(conjBody.toExpr());
5553     Result r = solChecker.checkSat();
5554     Notice() << "SmtEngine::checkSynthSolution(): result is " << r << endl;
5555     Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
5556     if (r.asSatisfiabilityResult().isUnknown())
5557     {
5558       InternalError(
5559           "SmtEngine::checkSynthSolution(): could not check solution, result "
5560           "unknown.");
5561     }
5562     else if (r.asSatisfiabilityResult().isSat())
5563     {
5564       InternalError(
5565           "SmtEngine::checkSynhtSol(): produced solution allows satisfiable "
5566           "negated conjecture.");
5567     }
5568     solChecker.resetAssertions();
5569   }
5570 }
5571
5572 // TODO(#1108): Simplify the error reporting of this method.
5573 UnsatCore SmtEngine::getUnsatCore() {
5574   Trace("smt") << "SMT getUnsatCore()" << endl;
5575   SmtScope smts(this);
5576   finalOptionsAreSet();
5577   if(Dump.isOn("benchmark")) {
5578     Dump("benchmark") << GetUnsatCoreCommand();
5579   }
5580 #if IS_PROOFS_BUILD
5581   if(!options::unsatCores()) {
5582     throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off.");
5583   }
5584   if(d_status.isNull() ||
5585      d_status.asSatisfiabilityResult() != Result::UNSAT ||
5586      d_problemExtended) {
5587     throw RecoverableModalException(
5588         "Cannot get an unsat core unless immediately preceded by UNSAT/VALID "
5589         "response.");
5590   }
5591
5592   d_proofManager->traceUnsatCore();// just to trigger core creation
5593   return UnsatCore(this, d_proofManager->extractUnsatCore());
5594 #else /* IS_PROOFS_BUILD */
5595   throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
5596 #endif /* IS_PROOFS_BUILD */
5597 }
5598
5599 // TODO(#1108): Simplify the error reporting of this method.
5600 const Proof& SmtEngine::getProof()
5601 {
5602   Trace("smt") << "SMT getProof()" << endl;
5603   SmtScope smts(this);
5604   finalOptionsAreSet();
5605   if(Dump.isOn("benchmark")) {
5606     Dump("benchmark") << GetProofCommand();
5607   }
5608 #if IS_PROOFS_BUILD
5609   if(!options::proof()) {
5610     throw ModalException("Cannot get a proof when produce-proofs option is off.");
5611   }
5612   if(d_status.isNull() ||
5613      d_status.asSatisfiabilityResult() != Result::UNSAT ||
5614      d_problemExtended) {
5615     throw RecoverableModalException(
5616         "Cannot get a proof unless immediately preceded by UNSAT/VALID "
5617         "response.");
5618   }
5619
5620   return ProofManager::getProof(this);
5621 #else /* IS_PROOFS_BUILD */
5622   throw ModalException("This build of CVC4 doesn't have proof support.");
5623 #endif /* IS_PROOFS_BUILD */
5624 }
5625
5626 void SmtEngine::printInstantiations( std::ostream& out ) {
5627   SmtScope smts(this);
5628   if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
5629     out << "% SZS output start Proof for " << d_filename.c_str() << std::endl;
5630   }
5631   if( d_theoryEngine ){
5632     d_theoryEngine->printInstantiations( out );
5633   }else{
5634     Assert( false );
5635   }
5636   if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
5637     out << "% SZS output end Proof for " << d_filename.c_str() << std::endl;
5638   }
5639 }
5640
5641 void SmtEngine::printSynthSolution( std::ostream& out ) {
5642   SmtScope smts(this);
5643   if( d_theoryEngine ){
5644     d_theoryEngine->printSynthSolution( out );
5645   }else{
5646     Assert( false );
5647   }
5648 }
5649
5650 Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
5651 {
5652   SmtScope smts(this);
5653   if(!d_logic.isPure(THEORY_ARITH) && strict){
5654     Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
5655   }
5656   Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
5657   Node n_e = Node::fromExpr( e );
5658   if (n_e.getKind() != kind::EXISTS && n_e.getKind() != kind::FORALL)
5659   {
5660     throw ModalException(
5661         "Expecting a quantified formula as argument to get-qe.");
5662   }
5663   //tag the quantified formula with the quant-elim attribute
5664   TypeNode t = NodeManager::currentNM()->booleanType();
5665   Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
5666   std::vector< Node > node_values;
5667   d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
5668   n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr);
5669   n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr);
5670   std::vector< Node > e_children;
5671   e_children.push_back( n_e[0] );
5672   e_children.push_back(n_e.getKind() == kind::EXISTS ? n_e[1]
5673                                                      : n_e[1].negate());
5674   e_children.push_back( n_attr );
5675   Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
5676   Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl;
5677   Assert( nn_e.getNumChildren()==3 );
5678   Result r = checkSatisfiability(nn_e.toExpr(), true, true);
5679   Trace("smt-qe") << "Query returned " << r << std::endl;
5680   if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) {
5681     if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){
5682       stringstream ss;
5683       ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
5684       InternalError(ss.str().c_str());
5685     }
5686     std::vector< Node > inst_qs;
5687     d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs );
5688     Assert( inst_qs.size()<=1 );
5689     Node ret_n;
5690     if( inst_qs.size()==1 ){
5691       Node top_q = inst_qs[0];
5692       //Node top_q = Rewriter::rewrite( nn_e ).negate();
5693       Assert( top_q.getKind()==kind::FORALL );
5694       Trace("smt-qe") << "Get qe for " << top_q << std::endl;
5695       ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
5696       Trace("smt-qe") << "Returned : " << ret_n << std::endl;
5697       if (n_e.getKind() == kind::EXISTS)
5698       {
5699         ret_n = Rewriter::rewrite(ret_n.negate());
5700       }
5701     }else{
5702       ret_n = NodeManager::currentNM()->mkConst(n_e.getKind() != kind::EXISTS);
5703     }
5704     return ret_n.toExpr();
5705   }else {
5706     return NodeManager::currentNM()
5707         ->mkConst(n_e.getKind() == kind::EXISTS)
5708         .toExpr();
5709   }
5710 }
5711
5712 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
5713   SmtScope smts(this);
5714   if( d_theoryEngine ){
5715     std::vector< Node > qs_n;
5716     d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n );
5717     for( unsigned i=0; i<qs_n.size(); i++ ){
5718       qs.push_back( qs_n[i].toExpr() );
5719     }
5720   }else{
5721     Assert( false );
5722   }
5723 }
5724
5725 void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
5726   SmtScope smts(this);
5727   if( d_theoryEngine ){
5728     std::vector< Node > insts_n;
5729     d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n );
5730     for( unsigned i=0; i<insts_n.size(); i++ ){
5731       insts.push_back( insts_n[i].toExpr() );
5732     }
5733   }else{
5734     Assert( false );
5735   }
5736 }
5737
5738 void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) {
5739   SmtScope smts(this);
5740   Assert(options::trackInstLemmas());
5741   if( d_theoryEngine ){
5742     std::vector< std::vector< Node > > tvecs_n;
5743     d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n );
5744     for( unsigned i=0; i<tvecs_n.size(); i++ ){
5745       std::vector< Expr > tvec;
5746       for( unsigned j=0; j<tvecs_n[i].size(); j++ ){
5747         tvec.push_back( tvecs_n[i][j].toExpr() );
5748       }
5749       tvecs.push_back( tvec );
5750     }
5751   }else{
5752     Assert( false );
5753   }
5754 }
5755
5756 vector<Expr> SmtEngine::getAssertions() {
5757   SmtScope smts(this);
5758   finalOptionsAreSet();
5759   doPendingPops();
5760   if(Dump.isOn("benchmark")) {
5761     Dump("benchmark") << GetAssertionsCommand();
5762   }
5763   Trace("smt") << "SMT getAssertions()" << endl;
5764   if(!options::produceAssertions()) {
5765     const char* msg =
5766       "Cannot query the current assertion list when not in produce-assertions mode.";
5767     throw ModalException(msg);
5768   }
5769   Assert(d_assertionList != NULL);
5770   // copy the result out
5771   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
5772 }
5773
5774 void SmtEngine::push()
5775 {
5776   SmtScope smts(this);
5777   finalOptionsAreSet();
5778   doPendingPops();
5779   Trace("smt") << "SMT push()" << endl;
5780   d_private->notifyPush();
5781   d_private->processAssertions();
5782   if(Dump.isOn("benchmark")) {
5783     Dump("benchmark") << PushCommand();
5784   }
5785   if(!options::incrementalSolving()) {
5786     throw ModalException("Cannot push when not solving incrementally (use --incremental)");
5787   }
5788
5789   // check to see if a postsolve() is pending
5790   if(d_needPostsolve) {
5791     d_theoryEngine->postsolve();
5792     d_needPostsolve = false;
5793   }
5794
5795   // The problem isn't really "extended" yet, but this disallows
5796   // get-model after a push, simplifying our lives somewhat and
5797   // staying symmtric with pop.
5798   setProblemExtended(true);
5799
5800   d_userLevels.push_back(d_userContext->getLevel());
5801   internalPush();
5802   Trace("userpushpop") << "SmtEngine: pushed to level "
5803                        << d_userContext->getLevel() << endl;
5804 }
5805
5806 void SmtEngine::pop() {
5807   SmtScope smts(this);
5808   finalOptionsAreSet();
5809   Trace("smt") << "SMT pop()" << endl;
5810   if(Dump.isOn("benchmark")) {
5811     Dump("benchmark") << PopCommand();
5812   }
5813   if(!options::incrementalSolving()) {
5814     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
5815   }
5816   if(d_userLevels.size() == 0) {
5817     throw ModalException("Cannot pop beyond the first user frame");
5818   }
5819
5820   // check to see if a postsolve() is pending
5821   if(d_needPostsolve) {
5822     d_theoryEngine->postsolve();
5823     d_needPostsolve = false;
5824   }
5825
5826   // The problem isn't really "extended" yet, but this disallows
5827   // get-model after a pop, simplifying our lives somewhat.  It might
5828   // not be strictly necessary to do so, since the pops occur lazily,
5829   // but also it would be weird to have a legally-executed (get-model)
5830   // that only returns a subset of the assignment (because the rest
5831   // is no longer in scope!).
5832   setProblemExtended(true);
5833
5834   AlwaysAssert(d_userContext->getLevel() > 0);
5835   AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
5836   while (d_userLevels.back() < d_userContext->getLevel()) {
5837     internalPop(true);
5838   }
5839   d_userLevels.pop_back();
5840
5841   // Clear out assertion queues etc., in case anything is still in there
5842   d_private->notifyPop();
5843
5844   Trace("userpushpop") << "SmtEngine: popped to level "
5845                        << d_userContext->getLevel() << endl;
5846   // FIXME: should we reset d_status here?
5847   // SMT-LIBv2 spec seems to imply no, but it would make sense to..
5848 }
5849
5850 void SmtEngine::internalPush() {
5851   Assert(d_fullyInited);
5852   Trace("smt") << "SmtEngine::internalPush()" << endl;
5853   doPendingPops();
5854   if(options::incrementalSolving()) {
5855     d_private->processAssertions();
5856     TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
5857     d_userContext->push();
5858     // the d_context push is done inside of the SAT solver
5859     d_propEngine->push();
5860   }
5861 }
5862
5863 void SmtEngine::internalPop(bool immediate) {
5864   Assert(d_fullyInited);
5865   Trace("smt") << "SmtEngine::internalPop()" << endl;
5866   if(options::incrementalSolving()) {
5867     ++d_pendingPops;
5868   }
5869   if(immediate) {
5870     doPendingPops();
5871   }
5872 }
5873
5874 void SmtEngine::doPendingPops() {
5875   Assert(d_pendingPops == 0 || options::incrementalSolving());
5876   while(d_pendingPops > 0) {
5877     TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
5878     d_propEngine->pop();
5879     // the d_context pop is done inside of the SAT solver
5880     d_userContext->pop();
5881     --d_pendingPops;
5882   }
5883 }
5884
5885 void SmtEngine::reset()
5886 {
5887   SmtScope smts(this);
5888   ExprManager *em = d_exprManager;
5889   Trace("smt") << "SMT reset()" << endl;
5890   if(Dump.isOn("benchmark")) {
5891     Dump("benchmark") << ResetCommand();
5892   }
5893   Options opts;
5894   opts.copyValues(d_originalOptions);
5895   this->~SmtEngine();
5896   NodeManager::fromExprManager(em)->getOptions().copyValues(opts);
5897   new(this) SmtEngine(em);
5898 }
5899
5900 void SmtEngine::resetAssertions()
5901 {
5902   SmtScope smts(this);
5903   doPendingPops();
5904
5905   Trace("smt") << "SMT resetAssertions()" << endl;
5906   if(Dump.isOn("benchmark")) {
5907     Dump("benchmark") << ResetAssertionsCommand();
5908   }
5909
5910   while(!d_userLevels.empty()) {
5911     pop();
5912   }
5913
5914   // Also remember the global push/pop around everything.
5915   Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
5916   d_context->popto(0);
5917   d_userContext->popto(0);
5918   DeleteAndClearCommandVector(d_modelGlobalCommands);
5919   d_userContext->push();
5920   d_context->push();
5921 }
5922
5923 void SmtEngine::interrupt()
5924 {
5925   if(!d_fullyInited) {
5926     return;
5927   }
5928   d_propEngine->interrupt();
5929   d_theoryEngine->interrupt();
5930 }
5931
5932 void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
5933   d_private->getResourceManager()->setResourceLimit(units, cumulative);
5934 }
5935 void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) {
5936   d_private->getResourceManager()->setTimeLimit(milis, cumulative);
5937 }
5938
5939 unsigned long SmtEngine::getResourceUsage() const {
5940   return d_private->getResourceManager()->getResourceUsage();
5941 }
5942
5943 unsigned long SmtEngine::getTimeUsage() const {
5944   return d_private->getResourceManager()->getTimeUsage();
5945 }
5946
5947 unsigned long SmtEngine::getResourceRemaining() const
5948 {
5949   return d_private->getResourceManager()->getResourceRemaining();
5950 }
5951
5952 unsigned long SmtEngine::getTimeRemaining() const
5953 {
5954   return d_private->getResourceManager()->getTimeRemaining();
5955 }
5956
5957 Statistics SmtEngine::getStatistics() const
5958 {
5959   return Statistics(*d_statisticsRegistry);
5960 }
5961
5962 SExpr SmtEngine::getStatistic(std::string name) const
5963 {
5964   return d_statisticsRegistry->getStatistic(name);
5965 }
5966
5967 void SmtEngine::safeFlushStatistics(int fd) const {
5968   d_statisticsRegistry->safeFlushInformation(fd);
5969 }
5970
5971 void SmtEngine::setUserAttribute(const std::string& attr,
5972                                  Expr expr,
5973                                  const std::vector<Expr>& expr_values,
5974                                  const std::string& str_value)
5975 {
5976   SmtScope smts(this);
5977   std::vector<Node> node_values;
5978   for( unsigned i=0; i<expr_values.size(); i++ ){
5979     node_values.push_back( expr_values[i].getNode() );
5980   }
5981   d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
5982 }
5983
5984 void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
5985   Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
5986   for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){
5987     Command * c = d_modelGlobalCommands[i];
5988     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
5989     if(dfc != NULL) {
5990       if( dfc->getFunction()==f ){
5991         dfc->setPrintInModel( p );
5992       }
5993     }
5994   }
5995   for( unsigned i=0; i<d_modelCommands->size(); i++ ){
5996     Command * c = (*d_modelCommands)[i];
5997     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
5998     if(dfc != NULL) {
5999       if( dfc->getFunction()==f ){
6000         dfc->setPrintInModel( p );
6001       }
6002     }
6003   }
6004 }
6005
6006 void SmtEngine::beforeSearch()
6007 {
6008   if(d_fullyInited) {
6009     throw ModalException(
6010         "SmtEngine::beforeSearch called after initialization.");
6011   }
6012 }
6013
6014
6015 void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
6016 {
6017   NodeManagerScope nms(d_nodeManager);
6018   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
6019
6020   if(Dump.isOn("benchmark")) {
6021     Dump("benchmark") << SetOptionCommand(key, value);
6022   }
6023
6024   if(key == "command-verbosity") {
6025     if(!value.isAtom()) {
6026       const vector<SExpr>& cs = value.getChildren();
6027       if(cs.size() == 2 &&
6028          (cs[0].isKeyword() || cs[0].isString()) &&
6029          cs[1].isInteger()) {
6030         string c = cs[0].getValue();
6031         const Integer& v = cs[1].getIntegerValue();
6032         if(v < 0 || v > 2) {
6033           throw OptionException("command-verbosity must be 0, 1, or 2");
6034         }
6035         d_commandVerbosity[c] = v;
6036         return;
6037       }
6038     }
6039     throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
6040   }
6041
6042   if(!value.isAtom()) {
6043     throw OptionException("bad value for :" + key);
6044   }
6045
6046   string optionarg = value.getValue();
6047   Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
6048   nodeManagerOptions.setOption(key, optionarg);
6049 }
6050
6051 CVC4::SExpr SmtEngine::getOption(const std::string& key) const
6052 {
6053   NodeManagerScope nms(d_nodeManager);
6054
6055   Trace("smt") << "SMT getOption(" << key << ")" << endl;
6056
6057   if(key.length() >= 18 &&
6058      key.compare(0, 18, "command-verbosity:") == 0) {
6059     map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18);
6060     if(i != d_commandVerbosity.end()) {
6061       return SExpr((*i).second);
6062     }
6063     i = d_commandVerbosity.find("*");
6064     if(i != d_commandVerbosity.end()) {
6065       return SExpr((*i).second);
6066     }
6067     return SExpr(Integer(2));
6068   }
6069
6070   if(Dump.isOn("benchmark")) {
6071     Dump("benchmark") << GetOptionCommand(key);
6072   }
6073
6074   if(key == "command-verbosity") {
6075     vector<SExpr> result;
6076     SExpr defaultVerbosity;
6077     for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
6078         i != d_commandVerbosity.end();
6079         ++i) {
6080       vector<SExpr> v;
6081       v.push_back(SExpr((*i).first));
6082       v.push_back(SExpr((*i).second));
6083       if((*i).first == "*") {
6084         // put the default at the end of the SExpr
6085         defaultVerbosity = SExpr(v);
6086       } else {
6087         result.push_back(SExpr(v));
6088       }
6089     }
6090     // put the default at the end of the SExpr
6091     if(!defaultVerbosity.isAtom()) {
6092       result.push_back(defaultVerbosity);
6093     } else {
6094       // ensure the default is always listed
6095       vector<SExpr> v;
6096       v.push_back(SExpr("*"));
6097       v.push_back(SExpr(Integer(2)));
6098       result.push_back(SExpr(v));
6099     }
6100     return SExpr(result);
6101   }
6102
6103   Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
6104   return SExpr::parseAtom(nodeManagerOptions.getOption(key));
6105 }
6106
6107 void SmtEngine::setReplayStream(ExprStream* replayStream) {
6108   AlwaysAssert(!d_fullyInited,
6109                "Cannot set replay stream once fully initialized");
6110   d_replayStream = replayStream;
6111 }
6112
6113 bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
6114   return d_private->getExpressionName(e, name);
6115 }
6116
6117 void SmtEngine::setExpressionName(Expr e, const std::string& name) {
6118   Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl;
6119   d_private->setExpressionName(e,name);
6120 }
6121
6122 }/* CVC4 namespace */