src/smt/smt_engine.cpp

   1 /*********************                                                        */
   2 /*! \file smt_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 <tuple>
  27 #include <unordered_map>
  28 #include <unordered_set>
  29 #include <utility>
  30 #include <vector>
  31
  32 #include "api/cvc4cpp.h"
  33 #include "base/check.h"
  34 #include "base/configuration.h"
  35 #include "base/configuration_private.h"
  36 #include "base/exception.h"
  37 #include "base/listener.h"
  38 #include "base/modal_exception.h"
  39 #include "base/output.h"
  40 #include "context/cdhashmap.h"
  41 #include "context/cdhashset.h"
  42 #include "context/cdlist.h"
  43 #include "context/context.h"
  44 #include "decision/decision_engine.h"
  45 #include "expr/attribute.h"
  46 #include "expr/expr.h"
  47 #include "expr/kind.h"
  48 #include "expr/metakind.h"
  49 #include "expr/node.h"
  50 #include "expr/node_algorithm.h"
  51 #include "expr/node_builder.h"
  52 #include "expr/node_self_iterator.h"
  53 #include "expr/node_visitor.h"
  54 #include "options/arith_options.h"
  55 #include "options/arrays_options.h"
  56 #include "options/base_options.h"
  57 #include "options/booleans_options.h"
  58 #include "options/bv_options.h"
  59 #include "options/datatypes_options.h"
  60 #include "options/decision_options.h"
  61 #include "options/language.h"
  62 #include "options/main_options.h"
  63 #include "options/open_ostream.h"
  64 #include "options/option_exception.h"
  65 #include "options/printer_options.h"
  66 #include "options/proof_options.h"
  67 #include "options/prop_options.h"
  68 #include "options/quantifiers_options.h"
  69 #include "options/sep_options.h"
  70 #include "options/set_language.h"
  71 #include "options/smt_options.h"
  72 #include "options/strings_options.h"
  73 #include "options/theory_options.h"
  74 #include "options/uf_options.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/abduction_solver.h"
  85 #include "smt/command.h"
  86 #include "smt/command_list.h"
  87 #include "smt/defined_function.h"
  88 #include "smt/logic_request.h"
  89 #include "smt/managed_ostreams.h"
  90 #include "smt/model_blocker.h"
  91 #include "smt/model_core_builder.h"
  92 #include "smt/process_assertions.h"
  93 #include "smt/set_defaults.h"
  94 #include "smt/smt_engine_scope.h"
  95 #include "smt/smt_engine_stats.h"
  96 #include "smt/term_formula_removal.h"
  97 #include "smt/update_ostream.h"
  98 #include "smt_util/boolean_simplification.h"
  99 #include "smt_util/nary_builder.h"
 100 #include "theory/booleans/circuit_propagator.h"
 101 #include "theory/bv/theory_bv_rewriter.h"
 102 #include "theory/logic_info.h"
 103 #include "theory/quantifiers/fun_def_process.h"
 104 #include "theory/quantifiers/single_inv_partition.h"
 105 #include "theory/quantifiers/sygus/synth_engine.h"
 106 #include "theory/quantifiers/term_util.h"
 107 #include "theory/quantifiers_engine.h"
 108 #include "theory/rewriter.h"
 109 #include "theory/sort_inference.h"
 110 #include "theory/strings/theory_strings.h"
 111 #include "theory/substitutions.h"
 112 #include "theory/theory_engine.h"
 113 #include "theory/theory_model.h"
 114 #include "theory/theory_traits.h"
 115 #include "util/hash.h"
 116 #include "util/proof.h"
 117 #include "util/random.h"
 118 #include "util/resource_manager.h"
 119
 120 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
 121 #include "lfscc.h"
 122 #endif
 123
 124 using namespace std;
 125 using namespace CVC4;
 126 using namespace CVC4::smt;
 127 using namespace CVC4::preprocessing;
 128 using namespace CVC4::prop;
 129 using namespace CVC4::context;
 130 using namespace CVC4::theory;
 131
 132 namespace CVC4 {
 133
 134 namespace proof {
 135 extern const char* const plf_signatures;
 136 }  // namespace proof
 137
 138 namespace smt {
 139
 140 struct DeleteCommandFunction : public std::unary_function<const Command*, void>
 141 {
 142   void operator()(const Command* command) { delete command; }
 143 };
 144
 145 void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
 146   std::for_each(commands.begin(), commands.end(), DeleteCommandFunction());
 147   commands.clear();
 148 }
 149
 150 class SoftResourceOutListener : public Listener {
 151  public:
 152   SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
 153   void notify() override
 154   {
 155     SmtScope scope(d_smt);
 156     Assert(smt::smtEngineInScope());
 157     d_smt->interrupt();
 158   }
 159  private:
 160   SmtEngine* d_smt;
 161 }; /* class SoftResourceOutListener */
 162
 163
 164 class HardResourceOutListener : public Listener {
 165  public:
 166   HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
 167   void notify() override
 168   {
 169     SmtScope scope(d_smt);
 170     theory::Rewriter::clearCaches();
 171   }
 172  private:
 173   SmtEngine* d_smt;
 174 }; /* class HardResourceOutListener */
 175
 176 class BeforeSearchListener : public Listener {
 177  public:
 178   BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
 179   void notify() override { d_smt->beforeSearch(); }
 180
 181  private:
 182   SmtEngine* d_smt;
 183 }; /* class BeforeSearchListener */
 184
 185 class SetDefaultExprDepthListener : public Listener {
 186  public:
 187   void notify() override
 188   {
 189     int depth = options::defaultExprDepth();
 190     Debug.getStream() << expr::ExprSetDepth(depth);
 191     Trace.getStream() << expr::ExprSetDepth(depth);
 192     Notice.getStream() << expr::ExprSetDepth(depth);
 193     Chat.getStream() << expr::ExprSetDepth(depth);
 194     Message.getStream() << expr::ExprSetDepth(depth);
 195     Warning.getStream() << expr::ExprSetDepth(depth);
 196     // intentionally exclude Dump stream from this list
 197   }
 198 };
 199
 200 class SetDefaultExprDagListener : public Listener {
 201  public:
 202   void notify() override
 203   {
 204     int dag = options::defaultDagThresh();
 205     Debug.getStream() << expr::ExprDag(dag);
 206     Trace.getStream() << expr::ExprDag(dag);
 207     Notice.getStream() << expr::ExprDag(dag);
 208     Chat.getStream() << expr::ExprDag(dag);
 209     Message.getStream() << expr::ExprDag(dag);
 210     Warning.getStream() << expr::ExprDag(dag);
 211     Dump.getStream() << expr::ExprDag(dag);
 212   }
 213 };
 214
 215 class SetPrintExprTypesListener : public Listener {
 216  public:
 217   void notify() override
 218   {
 219     bool value = options::printExprTypes();
 220     Debug.getStream() << expr::ExprPrintTypes(value);
 221     Trace.getStream() << expr::ExprPrintTypes(value);
 222     Notice.getStream() << expr::ExprPrintTypes(value);
 223     Chat.getStream() << expr::ExprPrintTypes(value);
 224     Message.getStream() << expr::ExprPrintTypes(value);
 225     Warning.getStream() << expr::ExprPrintTypes(value);
 226     // intentionally exclude Dump stream from this list
 227   }
 228 };
 229
 230 class DumpModeListener : public Listener {
 231  public:
 232   void notify() override
 233   {
 234     const std::string& value = options::dumpModeString();
 235     Dump.setDumpFromString(value);
 236   }
 237 };
 238
 239 class PrintSuccessListener : public Listener {
 240  public:
 241   void notify() override
 242   {
 243     bool value = options::printSuccess();
 244     Debug.getStream() << Command::printsuccess(value);
 245     Trace.getStream() << Command::printsuccess(value);
 246     Notice.getStream() << Command::printsuccess(value);
 247     Chat.getStream() << Command::printsuccess(value);
 248     Message.getStream() << Command::printsuccess(value);
 249     Warning.getStream() << Command::printsuccess(value);
 250     *options::out() << Command::printsuccess(value);
 251   }
 252 };
 253
 254
 255
 256 /**
 257  * This is an inelegant solution, but for the present, it will work.
 258  * The point of this is to separate the public and private portions of
 259  * the SmtEngine class, so that smt_engine.h doesn't
 260  * include "expr/node.h", which is a private CVC4 header (and can lead
 261  * to linking errors due to the improper inlining of non-visible symbols
 262  * into user code!).
 263  *
 264  * The "real" solution (that which is usually implemented) is to move
 265  * ALL the implementation to SmtEnginePrivate and maintain a
 266  * heap-allocated instance of it in SmtEngine.  SmtEngine (the public
 267  * one) becomes an "interface shell" which simply acts as a forwarder
 268  * of method calls.
 269  */
 270 class SmtEnginePrivate : public NodeManagerListener {
 271   SmtEngine& d_smt;
 272
 273   typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
 274   typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 275
 276   /** Manager for the memory of regular-output-channel. */
 277   ManagedRegularOutputChannel d_managedRegularChannel;
 278
 279   /** Manager for the memory of diagnostic-output-channel. */
 280   ManagedDiagnosticOutputChannel d_managedDiagnosticChannel;
 281
 282   /** Manager for the memory of --dump-to. */
 283   ManagedDumpOStream d_managedDumpChannel;
 284
 285   /**
 286    * This list contains:
 287    *  softResourceOut
 288    *  hardResourceOut
 289    *  beforeSearchListener
 290    *
 291    * This needs to be deleted before both NodeManager's Options,
 292    * SmtEngine, d_resourceManager, and TheoryEngine.
 293    */
 294   ListenerRegistrationList* d_listenerRegistrations;
 295
 296   /** A circuit propagator for non-clausal propositional deduction */
 297   booleans::CircuitPropagator d_propagator;
 298
 299   /** Assertions in the preprocessing pipeline */
 300   AssertionPipeline d_assertions;
 301
 302   /** Whether any assertions have been processed */
 303   CDO<bool> d_assertionsProcessed;
 304
 305   // Cached true value
 306   Node d_true;
 307
 308   /**
 309    * A context that never pushes/pops, for use by CD structures (like
 310    * SubstitutionMaps) that should be "global".
 311    */
 312   context::Context d_fakeContext;
 313
 314   /**
 315    * A map of AbsractValues to their actual constants.  Only used if
 316    * options::abstractValues() is on.
 317    */
 318   SubstitutionMap d_abstractValueMap;
 319
 320   /**
 321    * A mapping of all abstract values (actual value |-> abstract) that
 322    * we've handed out.  This is necessary to ensure that we give the
 323    * same AbstractValues for the same real constants.  Only used if
 324    * options::abstractValues() is on.
 325    */
 326   NodeToNodeHashMap d_abstractValues;
 327
 328   /** TODO: whether certain preprocess steps are necessary */
 329   //bool d_needsExpandDefs;
 330
 331   /** The preprocessing pass context */
 332   std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
 333
 334   /** Process assertions module */
 335   ProcessAssertions d_processor;
 336
 337   //------------------------------- expression names
 338   /** mapping from expressions to name */
 339   context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
 340   //------------------------------- end expression names
 341  public:
 342   IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); }
 343
 344   /** Instance of the ITE remover */
 345   RemoveTermFormulas d_iteRemover;
 346
 347   /* Finishes the initialization of the private portion of SMTEngine. */
 348   void finishInit();
 349
 350   /*------------------- sygus utils ------------------*/
 351   /**
 352    * sygus variables declared (from "declare-var" and "declare-fun" commands)
 353    *
 354    * The SyGuS semantics for declared variables is that they are implicitly
 355    * universally quantified in the constraints.
 356    */
 357   std::vector<Node> d_sygusVars;
 358   /** sygus constraints */
 359   std::vector<Node> d_sygusConstraints;
 360   /** functions-to-synthesize */
 361   std::vector<Node> d_sygusFunSymbols;
 362   /**
 363    * Whether we need to reconstruct the sygus conjecture.
 364    */
 365   CDO<bool> d_sygusConjectureStale;
 366   /*------------------- end of sygus utils ------------------*/
 367
 368  public:
 369   SmtEnginePrivate(SmtEngine& smt)
 370       : d_smt(smt),
 371         d_managedRegularChannel(),
 372         d_managedDiagnosticChannel(),
 373         d_managedDumpChannel(),
 374         d_listenerRegistrations(new ListenerRegistrationList()),
 375         d_propagator(true, true),
 376         d_assertions(),
 377         d_assertionsProcessed(smt.getUserContext(), false),
 378         d_fakeContext(),
 379         d_abstractValueMap(&d_fakeContext),
 380         d_abstractValues(),
 381         d_processor(smt, *smt.getResourceManager()),
 382         // d_needsExpandDefs(true),  //TODO?
 383         d_exprNames(smt.getUserContext()),
 384         d_iteRemover(smt.getUserContext()),
 385         d_sygusConjectureStale(smt.getUserContext(), true)
 386   {
 387     d_smt.d_nodeManager->subscribeEvents(this);
 388     d_true = NodeManager::currentNM()->mkConst(true);
 389     ResourceManager* rm = d_smt.getResourceManager();
 390
 391     d_listenerRegistrations->add(
 392         rm->registerSoftListener(new SoftResourceOutListener(d_smt)));
 393
 394     d_listenerRegistrations->add(
 395         rm->registerHardListener(new HardResourceOutListener(d_smt)));
 396
 397     try
 398     {
 399       Options& opts = d_smt.getOptions();
 400       // Multiple options reuse BeforeSearchListener so registration requires an
 401       // extra bit of care.
 402       // We can safely not call notify on this before search listener at
 403       // registration time. This d_smt cannot be beforeSearch at construction
 404       // time. Therefore the BeforeSearchListener is a no-op. Therefore it does
 405       // not have to be called.
 406       d_listenerRegistrations->add(
 407           opts.registerBeforeSearchListener(new BeforeSearchListener(d_smt)));
 408
 409       // These do need registration calls.
 410       d_listenerRegistrations->add(opts.registerSetDefaultExprDepthListener(
 411           new SetDefaultExprDepthListener(), true));
 412       d_listenerRegistrations->add(opts.registerSetDefaultExprDagListener(
 413           new SetDefaultExprDagListener(), true));
 414       d_listenerRegistrations->add(opts.registerSetPrintExprTypesListener(
 415           new SetPrintExprTypesListener(), true));
 416       d_listenerRegistrations->add(
 417           opts.registerSetDumpModeListener(new DumpModeListener(), true));
 418       d_listenerRegistrations->add(opts.registerSetPrintSuccessListener(
 419           new PrintSuccessListener(), true));
 420       d_listenerRegistrations->add(opts.registerSetRegularOutputChannelListener(
 421           new SetToDefaultSourceListener(&d_managedRegularChannel), true));
 422       d_listenerRegistrations->add(
 423           opts.registerSetDiagnosticOutputChannelListener(
 424               new SetToDefaultSourceListener(&d_managedDiagnosticChannel),
 425               true));
 426       d_listenerRegistrations->add(opts.registerDumpToFileNameListener(
 427           new SetToDefaultSourceListener(&d_managedDumpChannel), true));
 428     }
 429     catch (OptionException& e)
 430     {
 431       // Registering the option listeners can lead to OptionExceptions, e.g.
 432       // when the user chooses a dump tag that does not exist. In that case, we
 433       // have to make sure that we delete existing listener registrations and
 434       // that we unsubscribe from NodeManager events. Otherwise we will have
 435       // errors in the deconstructors of the NodeManager (because the
 436       // NodeManager tries to notify an SmtEnginePrivate that does not exist)
 437       // and the ListenerCollection (because not all registrations have been
 438       // removed before calling the deconstructor).
 439       delete d_listenerRegistrations;
 440       d_smt.d_nodeManager->unsubscribeEvents(this);
 441       throw OptionException(e.getRawMessage());
 442     }
 443   }
 444
 445   ~SmtEnginePrivate()
 446   {
 447     delete d_listenerRegistrations;
 448
 449     if(d_propagator.getNeedsFinish()) {
 450       d_propagator.finish();
 451       d_propagator.setNeedsFinish(false);
 452     }
 453     d_smt.d_nodeManager->unsubscribeEvents(this);
 454   }
 455
 456   void spendResource(ResourceManager::Resource r)
 457   {
 458     d_smt.getResourceManager()->spendResource(r);
 459   }
 460
 461   ProcessAssertions* getProcessAssertions() { return &d_processor; }
 462
 463   void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
 464   {
 465     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
 466                          0,
 467                          tn.toType());
 468     if((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) {
 469       d_smt.addToModelCommandAndDump(c, flags);
 470     }
 471   }
 472
 473   void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override
 474   {
 475     DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
 476                          tn.getAttribute(expr::SortArityAttr()),
 477                          tn.toType());
 478     if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
 479     {
 480       d_smt.addToModelCommandAndDump(c);
 481     }
 482   }
 483
 484   void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts,
 485                             uint32_t flags) override
 486   {
 487     if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
 488     {
 489       std::vector<Type> types(dtts.begin(), dtts.end());
 490       DatatypeDeclarationCommand c(types);
 491       d_smt.addToModelCommandAndDump(c);
 492     }
 493   }
 494
 495   void nmNotifyNewVar(TNode n, uint32_t flags) override
 496   {
 497     DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
 498                              n.toExpr(),
 499                              n.getType().toType());
 500     if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
 501       d_smt.addToModelCommandAndDump(c, flags);
 502     }
 503   }
 504
 505   void nmNotifyNewSkolem(TNode n,
 506                          const std::string& comment,
 507                          uint32_t flags) override
 508   {
 509     string id = n.getAttribute(expr::VarNameAttr());
 510     DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
 511     if(Dump.isOn("skolems") && comment != "") {
 512       Dump("skolems") << CommentCommand(id + " is " + comment);
 513     }
 514     if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
 515       d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
 516     }
 517   }
 518
 519   void nmNotifyDeleteNode(TNode n) override {}
 520
 521   Node applySubstitutions(TNode node)
 522   {
 523     return Rewriter::rewrite(
 524         d_preprocessingPassContext->getTopLevelSubstitutions().apply(node));
 525   }
 526
 527   /**
 528    * Process the assertions that have been asserted.
 529    */
 530   void processAssertions();
 531
 532   /** Process a user push.
 533   */
 534   void notifyPush() {
 535
 536   }
 537
 538   /**
 539    * Process a user pop.  Clears out the non-context-dependent stuff in this
 540    * SmtEnginePrivate.  Necessary to clear out our assertion vectors in case
 541    * someone does a push-assert-pop without a check-sat. It also pops the
 542    * last map of expression names from notifyPush.
 543    */
 544   void notifyPop() {
 545     d_assertions.clear();
 546     d_propagator.getLearnedLiterals().clear();
 547     getIteSkolemMap().clear();
 548   }
 549
 550   /**
 551    * Adds a formula to the current context.  Action here depends on
 552    * the SimplificationMode (in the current Options scope); the
 553    * formula might be pushed out to the propositional layer
 554    * immediately, or it might be simplified and kept, or it might not
 555    * even be simplified.
 556    * The arguments isInput and isAssumption are used for bookkeeping for proofs.
 557    * The argument maybeHasFv should be set to true if the assertion may have
 558    * free variables. By construction, assertions from the smt2 parser are
 559    * guaranteed not to have free variables. However, other cases such as
 560    * assertions from the SyGuS parser may have free variables (say if the
 561    * input contains an assert or define-fun-rec command).
 562    *
 563    * @param isAssumption If true, the formula is considered to be an assumption
 564    * (this is used to distinguish assertions and assumptions)
 565    */
 566   void addFormula(TNode n,
 567                   bool inUnsatCore,
 568                   bool inInput = true,
 569                   bool isAssumption = false,
 570                   bool maybeHasFv = false);
 571   /**
 572    * Simplify node "in" by expanding definitions and applying any
 573    * substitutions learned from preprocessing.
 574    */
 575   Node simplify(TNode in) {
 576     // Substitute out any abstract values in ex.
 577     // Expand definitions.
 578     NodeToNodeHashMap cache;
 579     Node n = d_processor.expandDefinitions(in, cache).toExpr();
 580     // Make sure we've done all preprocessing, etc.
 581     Assert(d_assertions.size() == 0);
 582     return applySubstitutions(n).toExpr();
 583   }
 584
 585   /**
 586    * Substitute away all AbstractValues in a node.
 587    */
 588   Node substituteAbstractValues(TNode n) {
 589     // We need to do this even if options::abstractValues() is off,
 590     // since the setting might have changed after we already gave out
 591     // some abstract values.
 592     return d_abstractValueMap.apply(n);
 593   }
 594
 595   /**
 596    * Make a new (or return an existing) abstract value for a node.
 597    * Can only use this if options::abstractValues() is on.
 598    */
 599   Node mkAbstractValue(TNode n) {
 600     Assert(options::abstractValues());
 601     Node& val = d_abstractValues[n];
 602     if(val.isNull()) {
 603       val = d_smt.d_nodeManager->mkAbstractValue(n.getType());
 604       d_abstractValueMap.addSubstitution(val, n);
 605     }
 606     // We are supposed to ascribe types to all abstract values that go out.
 607     NodeManager* current = d_smt.d_nodeManager;
 608     Node ascription = current->mkConst(AscriptionType(n.getType().toType()));
 609     Node retval = current->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val);
 610     return retval;
 611   }
 612
 613   //------------------------------- expression names
 614   // implements setExpressionName, as described in smt_engine.h
 615   void setExpressionName(Expr e, std::string name) {
 616     d_exprNames[Node::fromExpr(e)] = name;
 617   }
 618
 619   // implements getExpressionName, as described in smt_engine.h
 620   bool getExpressionName(Expr e, std::string& name) const {
 621     context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e);
 622     if(it!=d_exprNames.end()) {
 623       name = (*it).second;
 624       return true;
 625     }else{
 626       return false;
 627     }
 628   }
 629   //------------------------------- end expression names
 630 };/* class SmtEnginePrivate */
 631
 632 }/* namespace CVC4::smt */
 633
 634 SmtEngine::SmtEngine(ExprManager* em, Options* optr)
 635     : d_context(new Context()),
 636       d_userContext(new UserContext()),
 637       d_userLevels(),
 638       d_exprManager(em),
 639       d_nodeManager(d_exprManager->getNodeManager()),
 640       d_theoryEngine(nullptr),
 641       d_propEngine(nullptr),
 642       d_proofManager(nullptr),
 643       d_rewriter(new theory::Rewriter()),
 644       d_definedFunctions(nullptr),
 645       d_abductSolver(nullptr),
 646       d_assertionList(nullptr),
 647       d_assignments(nullptr),
 648       d_modelGlobalCommands(),
 649       d_modelCommands(nullptr),
 650       d_dumpCommands(),
 651       d_defineCommands(),
 652       d_logic(),
 653       d_originalOptions(),
 654       d_isInternalSubsolver(false),
 655       d_pendingPops(0),
 656       d_fullyInited(false),
 657       d_queryMade(false),
 658       d_needPostsolve(false),
 659       d_globalNegation(false),
 660       d_status(),
 661       d_expectedStatus(),
 662       d_smtMode(SMT_MODE_START),
 663       d_private(nullptr),
 664       d_statisticsRegistry(nullptr),
 665       d_stats(nullptr),
 666       d_resourceManager(nullptr),
 667       d_scope(nullptr)
 668 {
 669   // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine
 670   // we are constructing the current SmtEngine in scope for the lifetime of
 671   // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine
 672   // is then in scope during its lifetime). This is mostly to ensure that
 673   // options are always in scope, for e.g. printing expressions, which rely
 674   // on knowing the output language.
 675   // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally.
 676   // These are created, used, and deleted in a modular fashion while not
 677   // interleaving calls to the master SmtEngine. Thus the hack here does not
 678   // break this use case.
 679   // On the other hand, this hack breaks use cases where multiple SmtEngine
 680   // objects are created by the user.
 681   d_scope.reset(new SmtScope(this));
 682   if (optr != nullptr)
 683   {
 684     // if we provided a set of options, copy their values to the options
 685     // owned by this SmtEngine.
 686     d_options.copyValues(*optr);
 687   }
 688   d_statisticsRegistry.reset(new StatisticsRegistry());
 689   d_resourceManager.reset(
 690       new ResourceManager(*d_statisticsRegistry.get(), d_options));
 691   d_private.reset(new smt::SmtEnginePrivate(*this));
 692   d_stats.reset(new SmtEngineStatistics());
 693   d_stats->d_resourceUnitsUsed.setData(d_resourceManager->getResourceUsage());
 694
 695   // The ProofManager is constructed before any other proof objects such as
 696   // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
 697   // initialized in TheoryEngine and PropEngine respectively.
 698   Assert(d_proofManager == nullptr);
 699
 700   // d_proofManager must be created before Options has been finished
 701   // being parsed from the input file. Because of this, we cannot trust
 702   // that options::proof() is set correctly yet.
 703 #ifdef CVC4_PROOF
 704   d_proofManager.reset(new ProofManager(getUserContext()));
 705 #endif
 706
 707   d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
 708   d_modelCommands = new (true) smt::CommandList(getUserContext());
 709 }
 710
 711 void SmtEngine::finishInit()
 712 {
 713   // Notice that finishInit is called when options are finalized. If we are
 714   // parsing smt2, this occurs at the moment we enter "Assert mode", page 52
 715   // of SMT-LIB 2.6 standard.
 716
 717   // Inialize the resource manager based on the options.
 718   d_resourceManager->setHardLimit(options::hardLimit());
 719   if (options::perCallResourceLimit() != 0)
 720   {
 721     d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
 722   }
 723   if (options::cumulativeResourceLimit() != 0)
 724   {
 725     d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
 726                                         true);
 727   }
 728   if (options::perCallMillisecondLimit() != 0)
 729   {
 730     d_resourceManager->setTimeLimit(options::perCallMillisecondLimit(), false);
 731   }
 732   if (options::cumulativeMillisecondLimit() != 0)
 733   {
 734     d_resourceManager->setTimeLimit(options::cumulativeMillisecondLimit(),
 735                                     true);
 736   }
 737   if (options::cpuTime())
 738   {
 739     d_resourceManager->useCPUTime(true);
 740   }
 741
 742   // set the random seed
 743   Random::getRandom().setSeed(options::seed());
 744
 745   // ensure that our heuristics are properly set up
 746   setDefaults(d_logic, d_isInternalSubsolver);
 747
 748   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
 749   // We have mutual dependency here, so we add the prop engine to the theory
 750   // engine later (it is non-essential there)
 751   d_theoryEngine.reset(new TheoryEngine(getContext(),
 752                                         getUserContext(),
 753                                         getResourceManager(),
 754                                         d_private->d_iteRemover,
 755                                         const_cast<const LogicInfo&>(d_logic)));
 756
 757   // Add the theories
 758   for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
 759     TheoryConstructor::addTheory(getTheoryEngine(), id);
 760     //register with proof engine if applicable
 761 #ifdef CVC4_PROOF
 762     ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id));
 763 #endif
 764   }
 765
 766   Trace("smt-debug") << "Making decision engine..." << std::endl;
 767
 768   Trace("smt-debug") << "Making prop engine..." << std::endl;
 769   /* force destruction of referenced PropEngine to enforce that statistics
 770    * are unregistered by the obsolete PropEngine object before registered
 771    * again by the new PropEngine object */
 772   d_propEngine.reset(nullptr);
 773   d_propEngine.reset(new PropEngine(
 774       getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
 775
 776   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
 777   d_theoryEngine->setPropEngine(getPropEngine());
 778   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
 779   d_theoryEngine->finishInit();
 780
 781   // global push/pop around everything, to ensure proper destruction
 782   // of context-dependent data structures
 783   d_userContext->push();
 784   d_context->push();
 785
 786   Trace("smt-debug") << "Set up assertion list..." << std::endl;
 787   // [MGD 10/20/2011] keep around in incremental mode, due to a
 788   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
 789   // first, some user-context-dependent TNodes might still exist
 790   // with rc == 0.
 791   if(options::produceAssertions() ||
 792      options::incrementalSolving()) {
 793     // In the case of incremental solving, we appear to need these to
 794     // ensure the relevant Nodes remain live.
 795     d_assertionList = new (true) AssertionList(getUserContext());
 796     d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
 797   }
 798
 799   // dump out a set-logic command only when raw-benchmark is disabled to avoid
 800   // dumping the command twice.
 801   if (Dump.isOn("benchmark") && !Dump.isOn("raw-benchmark"))
 802   {
 803       LogicInfo everything;
 804       everything.lock();
 805       Dump("benchmark") << CommentCommand(
 806           "CVC4 always dumps the most general, all-supported logic (below), as "
 807           "some internals might require the use of a logic more general than "
 808           "the input.")
 809                         << SetBenchmarkLogicCommand(
 810                                everything.getLogicString());
 811   }
 812
 813   Trace("smt-debug") << "Dump declaration commands..." << std::endl;
 814   // dump out any pending declaration commands
 815   for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
 816     Dump("declarations") << *d_dumpCommands[i];
 817     delete d_dumpCommands[i];
 818   }
 819   d_dumpCommands.clear();
 820
 821   // subsolvers
 822   if (options::produceAbducts())
 823   {
 824     d_abductSolver.reset(new AbductionSolver(this));
 825   }
 826
 827   PROOF( ProofManager::currentPM()->setLogic(d_logic); );
 828   PROOF({
 829       for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
 830         ProofManager::currentPM()->getTheoryProofEngine()->
 831           finishRegisterTheory(d_theoryEngine->theoryOf(id));
 832       }
 833     });
 834   d_private->finishInit();
 835   Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
 836 }
 837
 838 void SmtEngine::finalOptionsAreSet() {
 839   if(d_fullyInited) {
 840     return;
 841   }
 842
 843   if(! d_logic.isLocked()) {
 844     setLogicInternal();
 845   }
 846
 847   // finish initialization, create the prop engine, etc.
 848   finishInit();
 849
 850   AlwaysAssert(d_propEngine->getAssertionLevel() == 0)
 851       << "The PropEngine has pushed but the SmtEngine "
 852          "hasn't finished initializing!";
 853
 854   d_fullyInited = true;
 855   Assert(d_logic.isLocked());
 856 }
 857
 858 void SmtEngine::shutdown() {
 859   doPendingPops();
 860
 861   while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
 862     internalPop(true);
 863   }
 864
 865   if (d_propEngine != nullptr)
 866   {
 867     d_propEngine->shutdown();
 868   }
 869   if (d_theoryEngine != nullptr)
 870   {
 871     d_theoryEngine->shutdown();
 872   }
 873 }
 874
 875 SmtEngine::~SmtEngine()
 876 {
 877   SmtScope smts(this);
 878
 879   try {
 880     shutdown();
 881
 882     // global push/pop around everything, to ensure proper destruction
 883     // of context-dependent data structures
 884     d_context->popto(0);
 885     d_userContext->popto(0);
 886
 887     if(d_assignments != NULL) {
 888       d_assignments->deleteSelf();
 889     }
 890
 891     d_globalDefineFunRecLemmas.reset();
 892
 893     if(d_assertionList != NULL) {
 894       d_assertionList->deleteSelf();
 895     }
 896
 897     for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
 898       delete d_dumpCommands[i];
 899       d_dumpCommands[i] = NULL;
 900     }
 901     d_dumpCommands.clear();
 902
 903     DeleteAndClearCommandVector(d_modelGlobalCommands);
 904
 905     if(d_modelCommands != NULL) {
 906       d_modelCommands->deleteSelf();
 907     }
 908
 909     d_definedFunctions->deleteSelf();
 910
 911     //destroy all passes before destroying things that they refer to
 912     d_private->getProcessAssertions()->cleanup();
 913
 914     // d_proofManager is always created when proofs are enabled at configure
 915     // time.  Because of this, this code should not be wrapped in PROOF() which
 916     // additionally checks flags such as options::proof().
 917     //
 918     // Note: the proof manager must be destroyed before the theory engine.
 919     // Because the destruction of the proofs depends on contexts owned be the
 920     // theory solvers.
 921 #ifdef CVC4_PROOF
 922     d_proofManager.reset(nullptr);
 923 #endif
 924
 925     d_theoryEngine.reset(nullptr);
 926     d_propEngine.reset(nullptr);
 927
 928     d_stats.reset(nullptr);
 929     d_private.reset(nullptr);
 930     // d_resourceManager must be destroyed before d_statisticsRegistry
 931     d_resourceManager.reset(nullptr);
 932     d_statisticsRegistry.reset(nullptr);
 933
 934
 935     d_userContext.reset(nullptr);
 936     d_context.reset(nullptr);
 937   } catch(Exception& e) {
 938     Warning() << "CVC4 threw an exception during cleanup." << endl
 939               << e << endl;
 940   }
 941 }
 942
 943 void SmtEngine::setLogic(const LogicInfo& logic)
 944 {
 945   SmtScope smts(this);
 946   if(d_fullyInited) {
 947     throw ModalException("Cannot set logic in SmtEngine after the engine has "
 948                          "finished initializing.");
 949   }
 950   d_logic = logic;
 951   d_userLogic = logic;
 952   setLogicInternal();
 953 }
 954
 955 void SmtEngine::setLogic(const std::string& s)
 956 {
 957   SmtScope smts(this);
 958   try
 959   {
 960     setLogic(LogicInfo(s));
 961     // dump out a set-logic command
 962     if (Dump.isOn("raw-benchmark"))
 963     {
 964       Dump("raw-benchmark")
 965           << SetBenchmarkLogicCommand(d_logic.getLogicString());
 966     }
 967   }
 968   catch (IllegalArgumentException& e)
 969   {
 970     throw LogicException(e.what());
 971   }
 972 }
 973
 974 void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
 975 LogicInfo SmtEngine::getLogicInfo() const {
 976   return d_logic;
 977 }
 978
 979 LogicInfo SmtEngine::getUserLogicInfo() const
 980 {
 981   // Lock the logic to make sure that this logic can be queried. We create a
 982   // copy of the user logic here to keep this method const.
 983   LogicInfo res = d_userLogic;
 984   res.lock();
 985   return res;
 986 }
 987
 988 void SmtEngine::notifyStartParsing(std::string filename)
 989 {
 990   d_filename = filename;
 991
 992   // Copy the original options. This is called prior to beginning parsing.
 993   // Hence reset should revert to these options, which note is after reading
 994   // the command line.
 995   d_originalOptions.copyValues(d_options);
 996 }
 997
 998 std::string SmtEngine::getFilename() const { return d_filename; }
 999 void SmtEngine::setLogicInternal()
1000 {
1001   Assert(!d_fullyInited)
1002       << "setting logic in SmtEngine but the engine has already"
1003          " finished initializing for this run";
1004   d_logic.lock();
1005   d_userLogic.lock();
1006 }
1007
1008 void SmtEngine::setProblemExtended()
1009 {
1010   d_smtMode = SMT_MODE_ASSERT;
1011   d_assumptions.clear();
1012 }
1013
1014 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
1015 {
1016   SmtScope smts(this);
1017
1018   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
1019
1020   if(Dump.isOn("benchmark")) {
1021     if(key == "status") {
1022       string s = value.getValue();
1023       BenchmarkStatus status =
1024         (s == "sat") ? SMT_SATISFIABLE :
1025           ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN);
1026       Dump("benchmark") << SetBenchmarkStatusCommand(status);
1027     } else {
1028       Dump("benchmark") << SetInfoCommand(key, value);
1029     }
1030   }
1031
1032   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
1033   if (key == "source" || key == "category" || key == "difficulty"
1034       || key == "notes" || key == "name" || key == "license")
1035   {
1036     // ignore these
1037     return;
1038   }
1039   else if (key == "filename")
1040   {
1041     d_filename = value.getValue();
1042     return;
1043   }
1044   else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser())
1045   {
1046     language::input::Language ilang = language::input::LANG_AUTO;
1047     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
1048         (value.isRational() && value.getRationalValue() == Rational(2)) ||
1049         value.getValue() == "2" ||
1050         value.getValue() == "2.0" ) {
1051       ilang = language::input::LANG_SMTLIB_V2_0;
1052     } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
1053                value.getValue() == "2.5" ) {
1054       ilang = language::input::LANG_SMTLIB_V2_5;
1055     } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) ||
1056                value.getValue() == "2.6" ) {
1057       ilang = language::input::LANG_SMTLIB_V2_6;
1058     }
1059     else
1060     {
1061       Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
1062       throw UnrecognizedOptionException();
1063     }
1064     options::inputLanguage.set(ilang);
1065     // also update the output language
1066     if (!options::outputLanguage.wasSetByUser())
1067     {
1068       language::output::Language olang = language::toOutputLanguage(ilang);
1069       if (options::outputLanguage() != olang)
1070       {
1071         options::outputLanguage.set(olang);
1072         *options::out() << language::SetLanguage(olang);
1073       }
1074     }
1075     return;
1076   } else if(key == "status") {
1077     string s;
1078     if(value.isAtom()) {
1079       s = value.getValue();
1080     }
1081     if(s != "sat" && s != "unsat" && s != "unknown") {
1082       throw OptionException("argument to (set-info :status ..) must be "
1083                             "`sat' or `unsat' or `unknown'");
1084     }
1085     d_expectedStatus = Result(s, d_filename);
1086     return;
1087   }
1088   throw UnrecognizedOptionException();
1089 }
1090
1091 bool SmtEngine::isValidGetInfoFlag(const std::string& key) const
1092 {
1093   if (key == "all-statistics" || key == "error-behavior" || key == "name"
1094       || key == "version" || key == "authors" || key == "status"
1095       || key == "reason-unknown" || key == "assertion-stack-levels"
1096       || key == "all-options")
1097   {
1098     return true;
1099   }
1100   return false;
1101 }
1102
1103 CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
1104 {
1105   SmtScope smts(this);
1106
1107   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
1108   if (!isValidGetInfoFlag(key))
1109   {
1110     throw UnrecognizedOptionException();
1111   }
1112   if (key == "all-statistics")
1113   {
1114     vector<SExpr> stats;
1115     for (StatisticsRegistry::const_iterator i =
1116              NodeManager::fromExprManager(d_exprManager)
1117                  ->getStatisticsRegistry()
1118                  ->begin();
1119          i
1120          != NodeManager::fromExprManager(d_exprManager)
1121                 ->getStatisticsRegistry()
1122                 ->end();
1123          ++i)
1124     {
1125       vector<SExpr> v;
1126       v.push_back((*i).first);
1127       v.push_back((*i).second);
1128       stats.push_back(v);
1129     }
1130     for (StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin();
1131          i != d_statisticsRegistry->end();
1132          ++i)
1133     {
1134       vector<SExpr> v;
1135       v.push_back((*i).first);
1136       v.push_back((*i).second);
1137       stats.push_back(v);
1138     }
1139     return SExpr(stats);
1140   }
1141   if (key == "error-behavior")
1142   {
1143     return SExpr(SExpr::Keyword("immediate-exit"));
1144   }
1145   if (key == "name")
1146   {
1147     return SExpr(Configuration::getName());
1148   }
1149   if (key == "version")
1150   {
1151     return SExpr(Configuration::getVersionString());
1152   }
1153   if (key == "authors")
1154   {
1155     return SExpr(Configuration::about());
1156   }
1157   if (key == "status")
1158   {
1159     // sat | unsat | unknown
1160     switch (d_status.asSatisfiabilityResult().isSat())
1161     {
1162       case Result::SAT: return SExpr(SExpr::Keyword("sat"));
1163       case Result::UNSAT: return SExpr(SExpr::Keyword("unsat"));
1164       default: return SExpr(SExpr::Keyword("unknown"));
1165     }
1166   }
1167   if (key == "reason-unknown")
1168   {
1169     if (!d_status.isNull() && d_status.isUnknown())
1170     {
1171       stringstream ss;
1172       ss << d_status.whyUnknown();
1173       string s = ss.str();
1174       transform(s.begin(), s.end(), s.begin(), ::tolower);
1175       return SExpr(SExpr::Keyword(s));
1176     }
1177     else
1178     {
1179       throw RecoverableModalException(
1180           "Can't get-info :reason-unknown when the "
1181           "last result wasn't unknown!");
1182     }
1183   }
1184   if (key == "assertion-stack-levels")
1185   {
1186     AlwaysAssert(d_userLevels.size()
1187                  <= std::numeric_limits<unsigned long int>::max());
1188     return SExpr(static_cast<unsigned long int>(d_userLevels.size()));
1189   }
1190   Assert(key == "all-options");
1191   // get the options, like all-statistics
1192   std::vector<std::vector<std::string>> current_options =
1193       Options::current()->getOptions();
1194   return SExpr::parseListOfListOfAtoms(current_options);
1195 }
1196
1197 void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func)
1198 {
1199   for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
1200     if((*i).getKind() != kind::BOUND_VARIABLE) {
1201       stringstream ss;
1202       ss << "All formal arguments to defined functions must be BOUND_VARIABLEs, but in the\n"
1203          << "definition of function " << func << ", formal\n"
1204          << "  " << *i << "\n"
1205          << "has kind " << (*i).getKind();
1206       throw TypeCheckingException(func, ss.str());
1207     }
1208   }
1209 }
1210
1211 void SmtEngine::debugCheckFunctionBody(Expr formula,
1212                                        const std::vector<Expr>& formals,
1213                                        Expr func)
1214 {
1215   Type formulaType = formula.getType(options::typeChecking());
1216   Type funcType = func.getType();
1217   // We distinguish here between definitions of constants and functions,
1218   // because the type checking for them is subtly different.  Perhaps we
1219   // should instead have SmtEngine::defineFunction() and
1220   // SmtEngine::defineConstant() for better clarity, although then that
1221   // doesn't match the SMT-LIBv2 standard...
1222   if(formals.size() > 0) {
1223     Type rangeType = FunctionType(funcType).getRangeType();
1224     if(! formulaType.isComparableTo(rangeType)) {
1225       stringstream ss;
1226       ss << "Type of defined function does not match its declaration\n"
1227          << "The function  : " << func << "\n"
1228          << "Declared type : " << rangeType << "\n"
1229          << "The body      : " << formula << "\n"
1230          << "Body type     : " << formulaType;
1231       throw TypeCheckingException(func, ss.str());
1232     }
1233   } else {
1234     if(! formulaType.isComparableTo(funcType)) {
1235       stringstream ss;
1236       ss << "Declared type of defined constant does not match its definition\n"
1237          << "The constant   : " << func << "\n"
1238          << "Declared type  : " << funcType << " " << Type::getTypeNode(funcType)->getId() << "\n"
1239          << "The definition : " << formula << "\n"
1240          << "Definition type: " << formulaType << " " << Type::getTypeNode(formulaType)->getId();
1241       throw TypeCheckingException(func, ss.str());
1242     }
1243   }
1244 }
1245
1246 void SmtEngine::defineFunction(Expr func,
1247                                const std::vector<Expr>& formals,
1248                                Expr formula,
1249                                bool global)
1250 {
1251   SmtScope smts(this);
1252   finalOptionsAreSet();
1253   doPendingPops();
1254   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
1255   debugCheckFormals(formals, func);
1256
1257   stringstream ss;
1258   ss << language::SetLanguage(
1259             language::SetLanguage::getLanguage(Dump.getStream()))
1260      << func;
1261   DefineFunctionCommand c(ss.str(), func, formals, formula, global);
1262   addToModelCommandAndDump(
1263       c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
1264
1265   PROOF(if (options::checkUnsatCores()) {
1266     d_defineCommands.push_back(c.clone());
1267   });
1268
1269   // type check body
1270   debugCheckFunctionBody(formula, formals, func);
1271
1272   // Substitute out any abstract values in formula
1273   Expr form =
1274       d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr();
1275
1276   TNode funcNode = func.getTNode();
1277   vector<Node> formalsNodes;
1278   for(vector<Expr>::const_iterator i = formals.begin(),
1279         iend = formals.end();
1280       i != iend;
1281       ++i) {
1282     formalsNodes.push_back((*i).getNode());
1283   }
1284   TNode formNode = form.getTNode();
1285   DefinedFunction def(funcNode, formalsNodes, formNode);
1286   // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
1287   // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
1288   // d_haveAdditions = true;
1289   Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << endl;
1290
1291   if (global)
1292   {
1293     d_definedFunctions->insertAtContextLevelZero(funcNode, def);
1294   }
1295   else
1296   {
1297     d_definedFunctions->insert(funcNode, def);
1298   }
1299 }
1300
1301 void SmtEngine::defineFunctionsRec(
1302     const std::vector<Expr>& funcs,
1303     const std::vector<std::vector<Expr>>& formals,
1304     const std::vector<Expr>& formulas,
1305     bool global)
1306 {
1307   SmtScope smts(this);
1308   finalOptionsAreSet();
1309   doPendingPops();
1310   Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
1311
1312   if (funcs.size() != formals.size() && funcs.size() != formulas.size())
1313   {
1314     stringstream ss;
1315     ss << "Number of functions, formals, and function bodies passed to "
1316           "defineFunctionsRec do not match:"
1317        << "\n"
1318        << "        #functions : " << funcs.size() << "\n"
1319        << "        #arg lists : " << formals.size() << "\n"
1320        << "  #function bodies : " << formulas.size() << "\n";
1321     throw ModalException(ss.str());
1322   }
1323   for (unsigned i = 0, size = funcs.size(); i < size; i++)
1324   {
1325     // check formal argument list
1326     debugCheckFormals(formals[i], funcs[i]);
1327     // type check body
1328     debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
1329   }
1330
1331   if (Dump.isOn("raw-benchmark"))
1332   {
1333     std::vector<api::Term> tFuncs = api::exprVectorToTerms(d_solver, funcs);
1334     std::vector<std::vector<api::Term>> tFormals;
1335     for (const std::vector<Expr>& formal : formals)
1336     {
1337       tFormals.emplace_back(api::exprVectorToTerms(d_solver, formal));
1338     }
1339     std::vector<api::Term> tFormulas =
1340         api::exprVectorToTerms(d_solver, formulas);
1341     Dump("raw-benchmark") << DefineFunctionRecCommand(
1342         d_solver, tFuncs, tFormals, tFormulas, global);
1343   }
1344
1345   ExprManager* em = getExprManager();
1346   bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
1347   for (unsigned i = 0, size = funcs.size(); i < size; i++)
1348   {
1349     // we assert a quantified formula
1350     Expr func_app;
1351     // make the function application
1352     if (formals[i].empty())
1353     {
1354       // it has no arguments
1355       func_app = funcs[i];
1356     }
1357     else
1358     {
1359       std::vector<Expr> children;
1360       children.push_back(funcs[i]);
1361       children.insert(children.end(), formals[i].begin(), formals[i].end());
1362       func_app = em->mkExpr(kind::APPLY_UF, children);
1363     }
1364     Expr lem = em->mkExpr(kind::EQUAL, func_app, formulas[i]);
1365     if (!formals[i].empty())
1366     {
1367       // set the attribute to denote this is a function definition
1368       std::string attr_name("fun-def");
1369       Expr aexpr = em->mkExpr(kind::INST_ATTRIBUTE, func_app);
1370       aexpr = em->mkExpr(kind::INST_PATTERN_LIST, aexpr);
1371       std::vector<Expr> expr_values;
1372       std::string str_value;
1373       setUserAttribute(attr_name, func_app, expr_values, str_value);
1374       // make the quantified formula
1375       Expr boundVars = em->mkExpr(kind::BOUND_VAR_LIST, formals[i]);
1376       lem = em->mkExpr(kind::FORALL, boundVars, lem, aexpr);
1377     }
1378     // assert the quantified formula
1379     //   notice we don't call assertFormula directly, since this would
1380     //   duplicate the output on raw-benchmark.
1381     Expr e = d_private->substituteAbstractValues(Node::fromExpr(lem)).toExpr();
1382     if (d_assertionList != nullptr)
1383     {
1384       d_assertionList->push_back(e);
1385     }
1386     if (global && d_globalDefineFunRecLemmas != nullptr)
1387     {
1388       // Global definitions are asserted at check-sat-time because we have to
1389       // make sure that they are always present
1390       Assert(!language::isInputLangSygus(options::inputLanguage()));
1391       d_globalDefineFunRecLemmas->emplace_back(Node::fromExpr(e));
1392     }
1393     else
1394     {
1395       d_private->addFormula(e.getNode(), false, true, false, maybeHasFv);
1396     }
1397   }
1398 }
1399
1400 void SmtEngine::defineFunctionRec(Expr func,
1401                                   const std::vector<Expr>& formals,
1402                                   Expr formula,
1403                                   bool global)
1404 {
1405   std::vector<Expr> funcs;
1406   funcs.push_back(func);
1407   std::vector<std::vector<Expr> > formals_multi;
1408   formals_multi.push_back(formals);
1409   std::vector<Expr> formulas;
1410   formulas.push_back(formula);
1411   defineFunctionsRec(funcs, formals_multi, formulas, global);
1412 }
1413
1414 bool SmtEngine::isDefinedFunction( Expr func ){
1415   Node nf = Node::fromExpr( func );
1416   Debug("smt") << "isDefined function " << nf << "?" << std::endl;
1417   return d_definedFunctions->find(nf) != d_definedFunctions->end();
1418 }
1419
1420 void SmtEnginePrivate::finishInit()
1421 {
1422   d_preprocessingPassContext.reset(
1423       new PreprocessingPassContext(&d_smt, &d_iteRemover, &d_propagator));
1424
1425   // initialize the preprocessing passes
1426   d_processor.finishInit(d_preprocessingPassContext.get());
1427 }
1428
1429 Result SmtEngine::check() {
1430   Assert(d_fullyInited);
1431   Assert(d_pendingPops == 0);
1432
1433   Trace("smt") << "SmtEngine::check()" << endl;
1434
1435   d_resourceManager->beginCall();
1436
1437   // Only way we can be out of resource is if cumulative budget is on
1438   if (d_resourceManager->cumulativeLimitOn() && d_resourceManager->out())
1439   {
1440     Result::UnknownExplanation why = d_resourceManager->outOfResources()
1441                                          ? Result::RESOURCEOUT
1442                                          : Result::TIMEOUT;
1443     return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename);
1444   }
1445
1446   // Make sure the prop layer has all of the assertions
1447   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
1448   d_private->processAssertions();
1449   Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
1450
1451   TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
1452
1453   Chat() << "solving..." << endl;
1454   Trace("smt") << "SmtEngine::check(): running check" << endl;
1455   Result result = d_propEngine->checkSat();
1456
1457   d_resourceManager->endCall();
1458   Trace("limit") << "SmtEngine::check(): cumulative millis "
1459                  << d_resourceManager->getTimeUsage() << ", resources "
1460                  << d_resourceManager->getResourceUsage() << endl;
1461
1462   return Result(result, d_filename);
1463 }
1464
1465 Result SmtEngine::quickCheck() {
1466   Assert(d_fullyInited);
1467   Trace("smt") << "SMT quickCheck()" << endl;
1468   return Result(
1469       Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
1470 }
1471
1472 theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
1473 {
1474   if (!options::assignFunctionValues())
1475   {
1476     std::stringstream ss;
1477     ss << "Cannot " << c << " when --assign-function-values is false.";
1478     throw RecoverableModalException(ss.str().c_str());
1479   }
1480
1481   if (d_smtMode != SMT_MODE_SAT && d_smtMode != SMT_MODE_SAT_UNKNOWN)
1482   {
1483     std::stringstream ss;
1484     ss << "Cannot " << c
1485        << " unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN "
1486           "response.";
1487     throw RecoverableModalException(ss.str().c_str());
1488   }
1489
1490   if (!options::produceModels())
1491   {
1492     std::stringstream ss;
1493     ss << "Cannot " << c << " when produce-models options is off.";
1494     throw ModalException(ss.str().c_str());
1495   }
1496
1497   TheoryModel* m = d_theoryEngine->getBuiltModel();
1498
1499   if (m == nullptr)
1500   {
1501     std::stringstream ss;
1502     ss << "Cannot " << c
1503        << " since model is not available. Perhaps the most recent call to "
1504           "check-sat was interupted?";
1505     throw RecoverableModalException(ss.str().c_str());
1506   }
1507
1508   return m;
1509 }
1510
1511 void SmtEnginePrivate::processAssertions() {
1512   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
1513   spendResource(ResourceManager::Resource::PreprocessStep);
1514   Assert(d_smt.d_fullyInited);
1515   Assert(d_smt.d_pendingPops == 0);
1516
1517   if (d_assertions.size() == 0) {
1518     // nothing to do
1519     return;
1520   }
1521   if (d_assertionsProcessed && options::incrementalSolving()) {
1522     // TODO(b/1255): Substitutions in incremental mode should be managed with a
1523     // proper data structure.
1524
1525     d_assertions.enableStoreSubstsInAsserts();
1526   }
1527   else
1528   {
1529     d_assertions.disableStoreSubstsInAsserts();
1530   }
1531
1532   // process the assertions
1533   bool noConflict = d_processor.apply(d_assertions);
1534
1535   //notify theory engine new preprocessed assertions
1536   d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() );
1537
1538   // Push the formula to decision engine
1539   if (noConflict)
1540   {
1541     Chat() << "pushing to decision engine..." << endl;
1542     d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions);
1543   }
1544
1545   // end: INVARIANT to maintain: no reordering of assertions or
1546   // introducing new ones
1547
1548   // if incremental, compute which variables are assigned
1549   if (options::incrementalSolving())
1550   {
1551     d_preprocessingPassContext->recordSymbolsInAssertions(d_assertions.ref());
1552   }
1553
1554   // Push the formula to SAT
1555   {
1556     Chat() << "converting to CNF..." << endl;
1557     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
1558     for (unsigned i = 0; i < d_assertions.size(); ++ i) {
1559       Chat() << "+ " << d_assertions[i] << std::endl;
1560       d_smt.d_propEngine->assertFormula(d_assertions[i]);
1561     }
1562   }
1563
1564   d_assertionsProcessed = true;
1565
1566   d_assertions.clear();
1567   getIteSkolemMap().clear();
1568 }
1569
1570 void SmtEnginePrivate::addFormula(
1571     TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
1572 {
1573   if (n == d_true) {
1574     // nothing to do
1575     return;
1576   }
1577
1578   Trace("smt") << "SmtEnginePrivate::addFormula(" << n
1579                << "), inUnsatCore = " << inUnsatCore
1580                << ", inInput = " << inInput
1581                << ", isAssumption = " << isAssumption << endl;
1582
1583   // Ensure that it does not contain free variables
1584   if (maybeHasFv)
1585   {
1586     if (expr::hasFreeVar(n))
1587     {
1588       std::stringstream se;
1589       se << "Cannot process assertion with free variable.";
1590       if (language::isInputLangSygus(options::inputLanguage()))
1591       {
1592         // Common misuse of SyGuS is to use top-level assert instead of
1593         // constraint when defining the synthesis conjecture.
1594         se << " Perhaps you meant `constraint` instead of `assert`?";
1595       }
1596       throw ModalException(se.str().c_str());
1597     }
1598   }
1599
1600   // Give it to proof manager
1601   PROOF(
1602     if( inInput ){
1603       // n is an input assertion
1604       if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
1605
1606         ProofManager::currentPM()->addCoreAssertion(n.toExpr());
1607       }
1608     }else{
1609       // n is the result of an unknown preprocessing step, add it to dependency map to null
1610       ProofManager::currentPM()->addDependence(n, Node::null());
1611     }
1612   );
1613
1614   // Add the normalized formula to the queue
1615   d_assertions.push_back(n, isAssumption);
1616   //d_assertions.push_back(Rewriter::rewrite(n));
1617 }
1618
1619 void SmtEngine::ensureBoolean(const Expr& e)
1620 {
1621   Type type = e.getType(options::typeChecking());
1622   Type boolType = d_exprManager->booleanType();
1623   if(type != boolType) {
1624     stringstream ss;
1625     ss << "Expected " << boolType << "\n"
1626        << "The assertion : " << e << "\n"
1627        << "Its type      : " << type;
1628     throw TypeCheckingException(e, ss.str());
1629   }
1630 }
1631
1632 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
1633 {
1634   Dump("benchmark") << CheckSatCommand(assumption);
1635   return checkSatisfiability(assumption, inUnsatCore, false);
1636 }
1637
1638 Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
1639 {
1640   if (assumptions.empty())
1641   {
1642     Dump("benchmark") << CheckSatCommand();
1643   }
1644   else
1645   {
1646     Dump("benchmark") << CheckSatAssumingCommand(assumptions);
1647   }
1648
1649   return checkSatisfiability(assumptions, inUnsatCore, false);
1650 }
1651
1652 Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore)
1653 {
1654   Dump("benchmark") << QueryCommand(expr, inUnsatCore);
1655   return checkSatisfiability(
1656              expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
1657              inUnsatCore,
1658              true)
1659       .asEntailmentResult();
1660 }
1661
1662 Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore)
1663 {
1664   return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult();
1665 }
1666
1667 Result SmtEngine::checkSatisfiability(const Expr& expr,
1668                                       bool inUnsatCore,
1669                                       bool isEntailmentCheck)
1670 {
1671   return checkSatisfiability(
1672       expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
1673       inUnsatCore,
1674       isEntailmentCheck);
1675 }
1676
1677 Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
1678                                       bool inUnsatCore,
1679                                       bool isEntailmentCheck)
1680 {
1681   try
1682   {
1683     SmtScope smts(this);
1684     finalOptionsAreSet();
1685     doPendingPops();
1686
1687     Trace("smt") << "SmtEngine::"
1688                  << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
1689                  << assumptions << ")" << endl;
1690
1691     if(d_queryMade && !options::incrementalSolving()) {
1692       throw ModalException("Cannot make multiple queries unless "
1693                            "incremental solving is enabled "
1694                            "(try --incremental)");
1695     }
1696
1697     // Note that a query has been made
1698     d_queryMade = true;
1699     // reset global negation
1700     d_globalNegation = false;
1701
1702     bool didInternalPush = false;
1703
1704     setProblemExtended();
1705
1706     if (isEntailmentCheck)
1707     {
1708       size_t size = assumptions.size();
1709       if (size > 1)
1710       {
1711         /* Assume: not (BIGAND assumptions)  */
1712         d_assumptions.push_back(
1713             d_exprManager->mkExpr(kind::AND, assumptions).notExpr());
1714       }
1715       else if (size == 1)
1716       {
1717         /* Assume: not expr  */
1718         d_assumptions.push_back(assumptions[0].notExpr());
1719       }
1720     }
1721     else
1722     {
1723       /* Assume: BIGAND assumptions  */
1724       d_assumptions = assumptions;
1725     }
1726
1727     if (!d_assumptions.empty())
1728     {
1729       internalPush();
1730       didInternalPush = true;
1731     }
1732
1733     Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
1734     for (Expr e : d_assumptions)
1735     {
1736       // Substitute out any abstract values in ex.
1737       e = d_private->substituteAbstractValues(Node::fromExpr(e)).toExpr();
1738       Assert(e.getExprManager() == d_exprManager);
1739       // Ensure expr is type-checked at this point.
1740       ensureBoolean(e);
1741
1742       /* Add assumption  */
1743       if (d_assertionList != NULL)
1744       {
1745         d_assertionList->push_back(e);
1746       }
1747       d_private->addFormula(e.getNode(), inUnsatCore, true, true);
1748     }
1749
1750     if (d_globalDefineFunRecLemmas != nullptr)
1751     {
1752       // Global definitions are asserted at check-sat-time because we have to
1753       // make sure that they are always present (they are essentially level
1754       // zero assertions)
1755       for (const Node& lemma : *d_globalDefineFunRecLemmas)
1756       {
1757         d_private->addFormula(lemma, false, true, false, false);
1758       }
1759     }
1760
1761     r = check();
1762
1763     if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
1764         && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
1765     {
1766       r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
1767     }
1768     // flipped if we did a global negation
1769     if (d_globalNegation)
1770     {
1771       Trace("smt") << "SmtEngine::process global negate " << r << std::endl;
1772       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
1773       {
1774         r = Result(Result::SAT);
1775       }
1776       else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
1777       {
1778         // only if satisfaction complete
1779         if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
1780         {
1781           r = Result(Result::UNSAT);
1782         }
1783         else
1784         {
1785           r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
1786         }
1787       }
1788       Trace("smt") << "SmtEngine::global negate returned " << r << std::endl;
1789     }
1790
1791     d_needPostsolve = true;
1792
1793     // Pop the context
1794     if (didInternalPush)
1795     {
1796       internalPop();
1797     }
1798
1799     // Remember the status
1800     d_status = r;
1801     // Check against expected status
1802     if (!d_expectedStatus.isUnknown() && !d_status.isUnknown()
1803         && d_status != d_expectedStatus)
1804     {
1805       CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got "
1806                    << d_status;
1807     }
1808     d_expectedStatus = Result();
1809     // Update the SMT mode
1810     if (d_status.asSatisfiabilityResult().isSat() == Result::UNSAT)
1811     {
1812       d_smtMode = SMT_MODE_UNSAT;
1813     }
1814     else if (d_status.asSatisfiabilityResult().isSat() == Result::SAT)
1815     {
1816       d_smtMode = SMT_MODE_SAT;
1817     }
1818     else
1819     {
1820       d_smtMode = SMT_MODE_SAT_UNKNOWN;
1821     }
1822
1823     Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
1824                  << "(" << assumptions << ") => " << r << endl;
1825
1826     // Check that SAT results generate a model correctly.
1827     if(options::checkModels()) {
1828       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
1829       {
1830         checkModel();
1831       }
1832     }
1833     // Check that UNSAT results generate a proof correctly.
1834     if(options::checkProofs()) {
1835       if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
1836         checkProof();
1837       }
1838     }
1839     // Check that UNSAT results generate an unsat core correctly.
1840     if(options::checkUnsatCores()) {
1841       if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
1842         TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
1843         checkUnsatCore();
1844       }
1845     }
1846
1847     return r;
1848   } catch (UnsafeInterruptException& e) {
1849     AlwaysAssert(d_resourceManager->out());
1850     Result::UnknownExplanation why = d_resourceManager->outOfResources()
1851                                          ? Result::RESOURCEOUT
1852                                          : Result::TIMEOUT;
1853     return Result(Result::SAT_UNKNOWN, why, d_filename);
1854   }
1855 }
1856
1857 vector<Expr> SmtEngine::getUnsatAssumptions(void)
1858 {
1859   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
1860   SmtScope smts(this);
1861   if (!options::unsatAssumptions())
1862   {
1863     throw ModalException(
1864         "Cannot get unsat assumptions when produce-unsat-assumptions option "
1865         "is off.");
1866   }
1867   if (d_smtMode != SMT_MODE_UNSAT)
1868   {
1869     throw RecoverableModalException(
1870         "Cannot get unsat assumptions unless immediately preceded by "
1871         "UNSAT/ENTAILED.");
1872   }
1873   finalOptionsAreSet();
1874   if (Dump.isOn("benchmark"))
1875   {
1876     Dump("benchmark") << GetUnsatAssumptionsCommand();
1877   }
1878   UnsatCore core = getUnsatCoreInternal();
1879   vector<Expr> res;
1880   for (const Expr& e : d_assumptions)
1881   {
1882     if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); }
1883   }
1884   return res;
1885 }
1886
1887 Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
1888 {
1889   Assert(ex.getExprManager() == d_exprManager);
1890   SmtScope smts(this);
1891   finalOptionsAreSet();
1892   doPendingPops();
1893
1894   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
1895
1896   if (Dump.isOn("raw-benchmark")) {
1897     Dump("raw-benchmark") << AssertCommand(ex);
1898   }
1899
1900   // Substitute out any abstract values in ex
1901   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
1902
1903   ensureBoolean(e);
1904   if(d_assertionList != NULL) {
1905     d_assertionList->push_back(e);
1906   }
1907   bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
1908   d_private->addFormula(e.getNode(), inUnsatCore, true, false, maybeHasFv);
1909   return quickCheck().asEntailmentResult();
1910 }/* SmtEngine::assertFormula() */
1911
1912 /*
1913    --------------------------------------------------------------------------
1914     Handling SyGuS commands
1915    --------------------------------------------------------------------------
1916 */
1917
1918 void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
1919 {
1920   SmtScope smts(this);
1921   finalOptionsAreSet();
1922   d_private->d_sygusVars.push_back(Node::fromExpr(var));
1923   Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n";
1924   Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
1925   // don't need to set that the conjecture is stale
1926 }
1927
1928 void SmtEngine::declareSygusFunctionVar(const std::string& id,
1929                                         Expr var,
1930                                         Type type)
1931 {
1932   SmtScope smts(this);
1933   finalOptionsAreSet();
1934   d_private->d_sygusVars.push_back(Node::fromExpr(var));
1935   Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n";
1936   Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
1937
1938   // don't need to set that the conjecture is stale
1939 }
1940
1941 void SmtEngine::declareSynthFun(const std::string& id,
1942                                 Expr func,
1943                                 Type sygusType,
1944                                 bool isInv,
1945                                 const std::vector<Expr>& vars)
1946 {
1947   SmtScope smts(this);
1948   finalOptionsAreSet();
1949   doPendingPops();
1950   Node fn = Node::fromExpr(func);
1951   d_private->d_sygusFunSymbols.push_back(fn);
1952   if (!vars.empty())
1953   {
1954     Expr bvl = d_exprManager->mkExpr(kind::BOUND_VAR_LIST, vars);
1955     std::vector<Expr> attr_val_bvl;
1956     attr_val_bvl.push_back(bvl);
1957     setUserAttribute("sygus-synth-fun-var-list", func, attr_val_bvl, "");
1958   }
1959   // whether sygus type encodes syntax restrictions
1960   if (sygusType.isDatatype()
1961       && static_cast<DatatypeType>(sygusType).getDatatype().isSygus())
1962   {
1963     TypeNode stn = TypeNode::fromType(sygusType);
1964     Node sym = d_nodeManager->mkBoundVar("sfproxy", stn);
1965     std::vector<Expr> attr_value;
1966     attr_value.push_back(sym.toExpr());
1967     setUserAttribute("sygus-synth-grammar", func, attr_value, "");
1968   }
1969   Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n";
1970   Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars);
1971   // sygus conjecture is now stale
1972   setSygusConjectureStale();
1973 }
1974
1975 void SmtEngine::assertSygusConstraint(Expr constraint)
1976 {
1977   SmtScope smts(this);
1978   finalOptionsAreSet();
1979   d_private->d_sygusConstraints.push_back(constraint);
1980
1981   Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
1982   Dump("raw-benchmark") << SygusConstraintCommand(constraint);
1983   // sygus conjecture is now stale
1984   setSygusConjectureStale();
1985 }
1986
1987 void SmtEngine::assertSygusInvConstraint(const Expr& inv,
1988                                          const Expr& pre,
1989                                          const Expr& trans,
1990                                          const Expr& post)
1991 {
1992   SmtScope smts(this);
1993   finalOptionsAreSet();
1994   // build invariant constraint
1995
1996   // get variables (regular and their respective primed versions)
1997   std::vector<Node> terms, vars, primed_vars;
1998   terms.push_back(Node::fromExpr(inv));
1999   terms.push_back(Node::fromExpr(pre));
2000   terms.push_back(Node::fromExpr(trans));
2001   terms.push_back(Node::fromExpr(post));
2002   // variables are built based on the invariant type
2003   FunctionType t = static_cast<FunctionType>(inv.getType());
2004   std::vector<Type> argTypes = t.getArgTypes();
2005   for (const Type& ti : argTypes)
2006   {
2007     TypeNode tn = TypeNode::fromType(ti);
2008     vars.push_back(d_nodeManager->mkBoundVar(tn));
2009     d_private->d_sygusVars.push_back(vars.back());
2010     std::stringstream ss;
2011     ss << vars.back() << "'";
2012     primed_vars.push_back(d_nodeManager->mkBoundVar(ss.str(), tn));
2013     d_private->d_sygusVars.push_back(primed_vars.back());
2014   }
2015
2016   // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
2017   for (unsigned i = 0; i < 4; ++i)
2018   {
2019     Node op = terms[i];
2020     Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
2021                        << " with type " << op.getType() << "...\n";
2022     std::vector<Node> children;
2023     children.push_back(op);
2024     // transition relation applied over both variable lists
2025     if (i == 2)
2026     {
2027       children.insert(children.end(), vars.begin(), vars.end());
2028       children.insert(children.end(), primed_vars.begin(), primed_vars.end());
2029     }
2030     else
2031     {
2032       children.insert(children.end(), vars.begin(), vars.end());
2033     }
2034     terms[i] = d_nodeManager->mkNode(kind::APPLY_UF, children);
2035     // make application of Inv on primed variables
2036     if (i == 0)
2037     {
2038       children.clear();
2039       children.push_back(op);
2040       children.insert(children.end(), primed_vars.begin(), primed_vars.end());
2041       terms.push_back(d_nodeManager->mkNode(kind::APPLY_UF, children));
2042     }
2043   }
2044   // make constraints
2045   std::vector<Node> conj;
2046   conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[1], terms[0]));
2047   Node term0_and_2 = d_nodeManager->mkNode(kind::AND, terms[0], terms[2]);
2048   conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, term0_and_2, terms[4]));
2049   conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[0], terms[3]));
2050   Node constraint = d_nodeManager->mkNode(kind::AND, conj);
2051
2052   d_private->d_sygusConstraints.push_back(constraint);
2053
2054   Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n";
2055   Dump("raw-benchmark") << SygusInvConstraintCommand(inv, pre, trans, post);
2056   // sygus conjecture is now stale
2057   setSygusConjectureStale();
2058 }
2059
2060 Result SmtEngine::checkSynth()
2061 {
2062   SmtScope smts(this);
2063
2064   if (options::incrementalSolving())
2065   {
2066     // TODO (project #7)
2067     throw ModalException(
2068         "Cannot make check-synth commands when incremental solving is enabled");
2069   }
2070   Expr query;
2071   if (d_private->d_sygusConjectureStale)
2072   {
2073     // build synthesis conjecture from asserted constraints and declared
2074     // variables/functions
2075     Node sygusVar =
2076         d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType());
2077     Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar);
2078     Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr);
2079     std::vector<Node> bodyv;
2080     Trace("smt") << "Sygus : Constructing sygus constraint...\n";
2081     unsigned n_constraints = d_private->d_sygusConstraints.size();
2082     Node body = n_constraints == 0
2083                     ? d_nodeManager->mkConst(true)
2084                     : (n_constraints == 1
2085                            ? d_private->d_sygusConstraints[0]
2086                            : d_nodeManager->mkNode(
2087                                kind::AND, d_private->d_sygusConstraints));
2088     body = body.notNode();
2089     Trace("smt") << "...constructed sygus constraint " << body << std::endl;
2090     if (!d_private->d_sygusVars.empty())
2091     {
2092       Node boundVars =
2093           d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars);
2094       body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body);
2095       Trace("smt") << "...constructed exists " << body << std::endl;
2096     }
2097     if (!d_private->d_sygusFunSymbols.empty())
2098     {
2099       Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST,
2100                                              d_private->d_sygusFunSymbols);
2101       body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr);
2102     }
2103     Trace("smt") << "...constructed forall " << body << std::endl;
2104
2105     // set attribute for synthesis conjecture
2106     setUserAttribute("sygus", sygusVar.toExpr(), {}, "");
2107
2108     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
2109     Dump("raw-benchmark") << CheckSynthCommand();
2110
2111     d_private->d_sygusConjectureStale = false;
2112
2113     if (options::incrementalSolving())
2114     {
2115       // we push a context so that this conjecture is removed if we modify it
2116       // later
2117       internalPush();
2118       assertFormula(body.toExpr(), true);
2119     }
2120     else
2121     {
2122       query = body.toExpr();
2123     }
2124   }
2125
2126   Result r = checkSatisfiability(query, true, false);
2127
2128   // Check that synthesis solutions satisfy the conjecture
2129   if (options::checkSynthSol()
2130       && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
2131   {
2132     checkSynthSolution();
2133   }
2134   return r;
2135 }
2136
2137 /*
2138    --------------------------------------------------------------------------
2139     End of Handling SyGuS commands
2140    --------------------------------------------------------------------------
2141 */
2142
2143 Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
2144   return node;
2145 }
2146
2147 Expr SmtEngine::simplify(const Expr& ex)
2148 {
2149   Assert(ex.getExprManager() == d_exprManager);
2150   SmtScope smts(this);
2151   finalOptionsAreSet();
2152   doPendingPops();
2153   Trace("smt") << "SMT simplify(" << ex << ")" << endl;
2154
2155   if(Dump.isOn("benchmark")) {
2156     Dump("benchmark") << SimplifyCommand(ex);
2157   }
2158
2159   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
2160   if( options::typeChecking() ) {
2161     e.getType(true); // ensure expr is type-checked at this point
2162   }
2163
2164   // Make sure all preprocessing is done
2165   d_private->processAssertions();
2166   Node n = d_private->simplify(Node::fromExpr(e));
2167   n = postprocess(n, TypeNode::fromType(e.getType()));
2168   return n.toExpr();
2169 }
2170
2171 Node SmtEngine::expandDefinitions(const Node& ex)
2172 {
2173   d_private->spendResource(ResourceManager::Resource::PreprocessStep);
2174
2175   SmtScope smts(this);
2176   finalOptionsAreSet();
2177   doPendingPops();
2178   Trace("smt") << "SMT expandDefinitions(" << ex << ")" << endl;
2179
2180   // Substitute out any abstract values in ex.
2181   Node e = d_private->substituteAbstractValues(ex);
2182   if(options::typeChecking()) {
2183     // Ensure expr is type-checked at this point.
2184     e.getType(true);
2185   }
2186
2187   unordered_map<Node, Node, NodeHashFunction> cache;
2188   Node n = d_private->getProcessAssertions()->expandDefinitions(
2189       e, cache, /* expandOnly = */ true);
2190   n = postprocess(n, e.getType());
2191
2192   return n;
2193 }
2194
2195 // TODO(#1108): Simplify the error reporting of this method.
2196 Expr SmtEngine::getValue(const Expr& ex) const
2197 {
2198   Assert(ex.getExprManager() == d_exprManager);
2199   SmtScope smts(this);
2200
2201   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
2202   if(Dump.isOn("benchmark")) {
2203     Dump("benchmark") << GetValueCommand(ex);
2204   }
2205
2206   // Substitute out any abstract values in ex.
2207   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
2208
2209   // Ensure expr is type-checked at this point.
2210   e.getType(options::typeChecking());
2211
2212   // do not need to apply preprocessing substitutions (should be recorded
2213   // in model already)
2214
2215   Node n = Node::fromExpr(e);
2216   Trace("smt") << "--- getting value of " << n << endl;
2217   TypeNode expectedType = n.getType();
2218
2219   // Expand, then normalize
2220   unordered_map<Node, Node, NodeHashFunction> cache;
2221   n = d_private->getProcessAssertions()->expandDefinitions(n, cache);
2222   // There are two ways model values for terms are computed (for historical
2223   // reasons).  One way is that used in check-model; the other is that
2224   // used by the Model classes.  It's not clear to me exactly how these
2225   // two are different, but they need to be unified.  This ugly hack here
2226   // is to fix bug 554 until we can revamp boolean-terms and models [MGD]
2227
2228   //AJR : necessary?
2229   if(!n.getType().isFunction()) {
2230     n = Rewriter::rewrite(n);
2231   }
2232
2233   Trace("smt") << "--- getting value of " << n << endl;
2234   TheoryModel* m = getAvailableModel("get-value");
2235   Node resultNode;
2236   if(m != NULL) {
2237     resultNode = m->getValue(n);
2238   }
2239   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
2240   resultNode = postprocess(resultNode, expectedType);
2241   Trace("smt") << "--- model-post returned " << resultNode << endl;
2242   Trace("smt") << "--- model-post returned " << resultNode.getType() << endl;
2243   Trace("smt") << "--- model-post expected " << expectedType << endl;
2244
2245   // type-check the result we got
2246   // Notice that lambdas have function type, which does not respect the subtype
2247   // relation, so we ignore them here.
2248   Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA
2249          || resultNode.getType().isSubtypeOf(expectedType))
2250       << "Run with -t smt for details.";
2251
2252   // Ensure it's a constant, or a lambda (for uninterpreted functions). This
2253   // assertion only holds for models that do not have approximate values.
2254   Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
2255          || resultNode.isConst());
2256
2257   if(options::abstractValues() && resultNode.getType().isArray()) {
2258     resultNode = d_private->mkAbstractValue(resultNode);
2259     Trace("smt") << "--- abstract value >> " << resultNode << endl;
2260   }
2261
2262   return resultNode.toExpr();
2263 }
2264
2265 vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs)
2266 {
2267   vector<Expr> result;
2268   for (const Expr& e : exprs)
2269   {
2270     result.push_back(getValue(e));
2271   }
2272   return result;
2273 }
2274
2275 bool SmtEngine::addToAssignment(const Expr& ex) {
2276   SmtScope smts(this);
2277   finalOptionsAreSet();
2278   doPendingPops();
2279   // Substitute out any abstract values in ex
2280   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
2281   Type type = e.getType(options::typeChecking());
2282   // must be Boolean
2283   PrettyCheckArgument(
2284       type.isBoolean(), e,
2285       "expected Boolean-typed variable or function application "
2286       "in addToAssignment()" );
2287   Node n = e.getNode();
2288   // must be a defined constant, or a variable
2289   PrettyCheckArgument(
2290       (((d_definedFunctions->find(n) != d_definedFunctions->end())
2291         && n.getNumChildren() == 0)
2292        || n.isVar()),
2293       e,
2294       "expected variable or defined-function application "
2295       "in addToAssignment(),\ngot %s",
2296       e.toString().c_str());
2297   if(!options::produceAssignments()) {
2298     return false;
2299   }
2300   if(d_assignments == NULL) {
2301     d_assignments = new (true) AssignmentSet(getContext());
2302   }
2303   d_assignments->insert(n);
2304
2305   return true;
2306 }
2307
2308 // TODO(#1108): Simplify the error reporting of this method.
2309 vector<pair<Expr, Expr>> SmtEngine::getAssignment()
2310 {
2311   Trace("smt") << "SMT getAssignment()" << endl;
2312   SmtScope smts(this);
2313   finalOptionsAreSet();
2314   if(Dump.isOn("benchmark")) {
2315     Dump("benchmark") << GetAssignmentCommand();
2316   }
2317   if(!options::produceAssignments()) {
2318     const char* msg =
2319       "Cannot get the current assignment when "
2320       "produce-assignments option is off.";
2321     throw ModalException(msg);
2322   }
2323
2324   // Get the model here, regardless of whether d_assignments is null, since
2325   // we should throw errors related to model availability whether or not
2326   // assignments is null.
2327   TheoryModel* m = getAvailableModel("get assignment");
2328
2329   vector<pair<Expr,Expr>> res;
2330   if (d_assignments != nullptr)
2331   {
2332     TypeNode boolType = d_nodeManager->booleanType();
2333     for (AssignmentSet::key_iterator i = d_assignments->key_begin(),
2334                                      iend = d_assignments->key_end();
2335          i != iend;
2336          ++i)
2337     {
2338       Node as = *i;
2339       Assert(as.getType() == boolType);
2340
2341       Trace("smt") << "--- getting value of " << as << endl;
2342
2343       // Expand, then normalize
2344       unordered_map<Node, Node, NodeHashFunction> cache;
2345       Node n = d_private->getProcessAssertions()->expandDefinitions(as, cache);
2346       n = Rewriter::rewrite(n);
2347
2348       Trace("smt") << "--- getting value of " << n << endl;
2349       Node resultNode;
2350       if (m != nullptr)
2351       {
2352         resultNode = m->getValue(n);
2353       }
2354
2355       // type-check the result we got
2356       Assert(resultNode.isNull() || resultNode.getType() == boolType);
2357
2358       // ensure it's a constant
2359       Assert(resultNode.isConst());
2360
2361       Assert(as.isVar());
2362       res.emplace_back(as.toExpr(), resultNode.toExpr());
2363     }
2364   }
2365   return res;
2366 }
2367
2368 void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool userVisible, const char* dumpTag) {
2369   Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl;
2370   SmtScope smts(this);
2371   // If we aren't yet fully inited, the user might still turn on
2372   // produce-models.  So let's keep any commands around just in
2373   // case.  This is useful in two cases: (1) SMT-LIBv1 auto-declares
2374   // sort "U" in QF_UF before setLogic() is run and we still want to
2375   // support finding card(U) with --finite-model-find, and (2) to
2376   // decouple SmtEngine and ExprManager if the user does a few
2377   // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
2378   // and expects to find their cardinalities in the model.
2379   if(/* userVisible && */
2380      (!d_fullyInited || options::produceModels()) &&
2381      (flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
2382     if(flags & ExprManager::VAR_FLAG_GLOBAL) {
2383       d_modelGlobalCommands.push_back(c.clone());
2384     } else {
2385       d_modelCommands->push_back(c.clone());
2386     }
2387   }
2388   if(Dump.isOn(dumpTag)) {
2389     if(d_fullyInited) {
2390       Dump(dumpTag) << c;
2391     } else {
2392       d_dumpCommands.push_back(c.clone());
2393     }
2394   }
2395 }
2396
2397 // TODO(#1108): Simplify the error reporting of this method.
2398 Model* SmtEngine::getModel() {
2399   Trace("smt") << "SMT getModel()" << endl;
2400   SmtScope smts(this);
2401
2402   finalOptionsAreSet();
2403
2404   if(Dump.isOn("benchmark")) {
2405     Dump("benchmark") << GetModelCommand();
2406   }
2407
2408   TheoryModel* m = getAvailableModel("get model");
2409
2410   // Since model m is being returned to the user, we must ensure that this
2411   // model object remains valid with future check-sat calls. Hence, we set
2412   // the theory engine into "eager model building" mode. TODO #2648: revisit.
2413   d_theoryEngine->setEagerModelBuilding();
2414
2415   if (options::modelCoresMode() != options::ModelCoresMode::NONE)
2416   {
2417     // If we enabled model cores, we compute a model core for m based on our
2418     // (expanded) assertions using the model core builder utility
2419     std::vector<Expr> eassertsProc = getExpandedAssertions();
2420     ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode());
2421   }
2422   m->d_inputName = d_filename;
2423   m->d_isKnownSat = (d_smtMode == SMT_MODE_SAT);
2424   return m;
2425 }
2426
2427 Result SmtEngine::blockModel()
2428 {
2429   Trace("smt") << "SMT blockModel()" << endl;
2430   SmtScope smts(this);
2431
2432   finalOptionsAreSet();
2433
2434   if (Dump.isOn("benchmark"))
2435   {
2436     Dump("benchmark") << BlockModelCommand();
2437   }
2438
2439   TheoryModel* m = getAvailableModel("block model");
2440
2441   if (options::blockModelsMode() == options::BlockModelsMode::NONE)
2442   {
2443     std::stringstream ss;
2444     ss << "Cannot block model when block-models is set to none.";
2445     throw ModalException(ss.str().c_str());
2446   }
2447
2448   // get expanded assertions
2449   std::vector<Expr> eassertsProc = getExpandedAssertions();
2450   Expr eblocker = ModelBlocker::getModelBlocker(
2451       eassertsProc, m, options::blockModelsMode());
2452   return assertFormula(eblocker);
2453 }
2454
2455 Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs)
2456 {
2457   Trace("smt") << "SMT blockModelValues()" << endl;
2458   SmtScope smts(this);
2459
2460   finalOptionsAreSet();
2461
2462   PrettyCheckArgument(
2463       !exprs.empty(),
2464       "block model values must be called on non-empty set of terms");
2465   if (Dump.isOn("benchmark"))
2466   {
2467     Dump("benchmark") << BlockModelValuesCommand(exprs);
2468   }
2469
2470   TheoryModel* m = getAvailableModel("block model values");
2471
2472   // get expanded assertions
2473   std::vector<Expr> eassertsProc = getExpandedAssertions();
2474   // we always do block model values mode here
2475   Expr eblocker = ModelBlocker::getModelBlocker(
2476       eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
2477   return assertFormula(eblocker);
2478 }
2479
2480 std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
2481 {
2482   if (!d_logic.isTheoryEnabled(THEORY_SEP))
2483   {
2484     const char* msg =
2485         "Cannot obtain separation logic expressions if not using the "
2486         "separation logic theory.";
2487     throw RecoverableModalException(msg);
2488   }
2489   NodeManagerScope nms(d_nodeManager);
2490   Expr heap;
2491   Expr nil;
2492   Model* m = getAvailableModel("get separation logic heap and nil");
2493   if (!m->getHeapModel(heap, nil))
2494   {
2495     InternalError()
2496         << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
2497            "expressions from theory model.";
2498   }
2499   return std::make_pair(heap, nil);
2500 }
2501
2502 std::vector<Expr> SmtEngine::getExpandedAssertions()
2503 {
2504   std::vector<Expr> easserts = getAssertions();
2505   // must expand definitions
2506   std::vector<Expr> eassertsProc;
2507   std::unordered_map<Node, Node, NodeHashFunction> cache;
2508   for (const Expr& e : easserts)
2509   {
2510     Node ea = Node::fromExpr(e);
2511     Node eae = d_private->getProcessAssertions()->expandDefinitions(ea, cache);
2512     eassertsProc.push_back(eae.toExpr());
2513   }
2514   return eassertsProc;
2515 }
2516
2517 Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
2518
2519 Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
2520
2521 void SmtEngine::checkProof()
2522 {
2523 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
2524
2525   Chat() << "generating proof..." << endl;
2526
2527   const Proof& pf = getProof();
2528
2529   Chat() << "checking proof..." << endl;
2530
2531   std::string logicString = d_logic.getLogicString();
2532
2533   std::stringstream pfStream;
2534
2535   pfStream << proof::plf_signatures << endl;
2536   int64_t sizeBeforeProof = static_cast<int64_t>(pfStream.tellp());
2537
2538   pf.toStream(pfStream);
2539   d_stats->d_proofsSize +=
2540       static_cast<int64_t>(pfStream.tellp()) - sizeBeforeProof;
2541
2542   {
2543     TimerStat::CodeTimer checkProofTimer(d_stats->d_lfscCheckProofTime);
2544     lfscc_init();
2545     lfscc_check_file(pfStream, false, false, false, false, false, false, false);
2546   }
2547   // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup
2548   // segfaults on regress0/bv/core/bitvec7.smt
2549   // lfscc_cleanup();
2550
2551 #else  /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
2552   Unreachable()
2553       << "This version of CVC4 was built without proof support; cannot check "
2554          "proofs.";
2555 #endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
2556 }
2557
2558 UnsatCore SmtEngine::getUnsatCoreInternal()
2559 {
2560 #if IS_PROOFS_BUILD
2561   if (!options::unsatCores())
2562   {
2563     throw ModalException(
2564         "Cannot get an unsat core when produce-unsat-cores option is off.");
2565   }
2566   if (d_smtMode != SMT_MODE_UNSAT)
2567   {
2568     throw RecoverableModalException(
2569         "Cannot get an unsat core unless immediately preceded by "
2570         "UNSAT/ENTAILED response.");
2571   }
2572
2573   d_proofManager->traceUnsatCore();  // just to trigger core creation
2574   return UnsatCore(this, d_proofManager->extractUnsatCore());
2575 #else  /* IS_PROOFS_BUILD */
2576   throw ModalException(
2577       "This build of CVC4 doesn't have proof support (required for unsat "
2578       "cores).");
2579 #endif /* IS_PROOFS_BUILD */
2580 }
2581
2582 void SmtEngine::checkUnsatCore() {
2583   Assert(options::unsatCores())
2584       << "cannot check unsat core if unsat cores are turned off";
2585
2586   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
2587   UnsatCore core = getUnsatCore();
2588
2589   SmtEngine coreChecker(d_exprManager, &d_options);
2590   coreChecker.setIsInternalSubsolver();
2591   coreChecker.setLogic(getLogicInfo());
2592   coreChecker.getOptions().set(options::checkUnsatCores, false);
2593   coreChecker.getOptions().set(options::checkProofs, false);
2594
2595   PROOF(
2596   std::vector<Command*>::const_iterator itg = d_defineCommands.begin();
2597   for (; itg != d_defineCommands.end();  ++itg) {
2598     (*itg)->invoke(&coreChecker);
2599   }
2600   );
2601
2602   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
2603   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
2604     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl;
2605     coreChecker.assertFormula(*i);
2606   }
2607   Result r;
2608   try {
2609     r = coreChecker.checkSat();
2610   } catch(...) {
2611     throw;
2612   }
2613   Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
2614   if(r.asSatisfiabilityResult().isUnknown()) {
2615     Warning()
2616         << "SmtEngine::checkUnsatCore(): could not check core result unknown."
2617         << std::endl;
2618   }
2619   else if (r.asSatisfiabilityResult().isSat())
2620   {
2621     InternalError()
2622         << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
2623   }
2624 }
2625
2626 void SmtEngine::checkModel(bool hardFailure) {
2627   // --check-model implies --produce-assertions, which enables the
2628   // assertion list, so we should be ok.
2629   Assert(d_assertionList != NULL)
2630       << "don't have an assertion list to check in SmtEngine::checkModel()";
2631
2632   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
2633
2634   // Throughout, we use Notice() to give diagnostic output.
2635   //
2636   // If this function is running, the user gave --check-model (or equivalent),
2637   // and if Notice() is on, the user gave --verbose (or equivalent).
2638
2639   Notice() << "SmtEngine::checkModel(): generating model" << endl;
2640   TheoryModel* m = getAvailableModel("check model");
2641
2642   // check-model is not guaranteed to succeed if approximate values were used.
2643   // Thus, we intentionally abort here.
2644   if (m->hasApproximations())
2645   {
2646     throw RecoverableModalException(
2647         "Cannot run check-model on a model with approximate values.");
2648   }
2649
2650   // Check individual theory assertions
2651   if (options::debugCheckModels())
2652   {
2653     d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure);
2654   }
2655
2656   // Output the model
2657   Notice() << *m;
2658
2659   // We have a "fake context" for the substitution map (we don't need it
2660   // to be context-dependent)
2661   context::Context fakeContext;
2662   SubstitutionMap substitutions(&fakeContext, /* substituteUnderQuantifiers = */ false);
2663
2664   for(size_t k = 0; k < m->getNumCommands(); ++k) {
2665     const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k));
2666     Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl;
2667     if(c == NULL) {
2668       // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
2669       Notice() << "SmtEngine::checkModel(): skipping..." << endl;
2670     } else {
2671       // We have a DECLARE-FUN:
2672       //
2673       // We'll first do some checks, then add to our substitution map
2674       // the mapping: function symbol |-> value
2675
2676       Expr func = c->getFunction();
2677       Node val = m->getValue(func);
2678
2679       Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << endl;
2680
2681       // (1) if the value is a lambda, ensure the lambda doesn't contain the
2682       // function symbol (since then the definition is recursive)
2683       if (val.getKind() == kind::LAMBDA) {
2684         // first apply the model substitutions we have so far
2685         Debug("boolean-terms") << "applying subses to " << val[1] << endl;
2686         Node n = substitutions.apply(val[1]);
2687         Debug("boolean-terms") << "++ got " << n << endl;
2688         // now check if n contains func by doing a substitution
2689         // [func->func2] and checking equality of the Nodes.
2690         // (this just a way to check if func is in n.)
2691         SubstitutionMap subs(&fakeContext);
2692         Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY);
2693         subs.addSubstitution(func, func2);
2694         if(subs.apply(n) != n) {
2695           Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl;
2696           stringstream ss;
2697           ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2698              << "considering model value for " << func << endl
2699              << "body of lambda is:   " << val << endl;
2700           if(n != val[1]) {
2701             ss << "body substitutes to: " << n << endl;
2702           }
2703           ss << "so " << func << " is defined in terms of itself." << endl
2704              << "Run with `--check-models -v' for additional diagnostics.";
2705           InternalError() << ss.str();
2706         }
2707       }
2708
2709       // (2) check that the value is actually a value
2710       else if (!val.isConst())
2711       {
2712         // This is only a warning since it could have been assigned an
2713         // unevaluable term (e.g. an application of a transcendental function).
2714         // This parallels the behavior (warnings for non-constant expressions)
2715         // when checking whether assertions are satisfied below.
2716         Warning() << "Warning : SmtEngine::checkModel(): "
2717                   << "model value for " << func << endl
2718                   << "             is " << val << endl
2719                   << "and that is not a constant (.isConst() == false)."
2720                   << std::endl
2721                   << "Run with `--check-models -v' for additional diagnostics."
2722                   << std::endl;
2723       }
2724
2725       // (3) check that it's the correct (sub)type
2726       // This was intended to be a more general check, but for now we can't do that because
2727       // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
2728       else if(func.getType().isInteger() && !val.getType().isInteger()) {
2729         Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl;
2730         InternalError()
2731             << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
2732                "MODEL:"
2733             << endl
2734             << "model value for " << func << endl
2735             << "             is " << val << endl
2736             << "value type is     " << val.getType() << endl
2737             << "should be of type " << func.getType() << endl
2738             << "Run with `--check-models -v' for additional diagnostics.";
2739       }
2740
2741       // (4) checks complete, add the substitution
2742       Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl;
2743       substitutions.addSubstitution(func, val);
2744     }
2745   }
2746
2747   // Now go through all our user assertions checking if they're satisfied.
2748   for(AssertionList::const_iterator i = d_assertionList->begin(); i != d_assertionList->end(); ++i) {
2749     Notice() << "SmtEngine::checkModel(): checking assertion " << *i << endl;
2750     Node n = Node::fromExpr(*i);
2751
2752     // Apply any define-funs from the problem.
2753     {
2754       unordered_map<Node, Node, NodeHashFunction> cache;
2755       n = d_private->getProcessAssertions()->expandDefinitions(n, cache);
2756     }
2757     Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
2758
2759     // Apply our model value substitutions.
2760     Debug("boolean-terms") << "applying subses to " << n << endl;
2761     n = substitutions.apply(n);
2762     Debug("boolean-terms") << "++ got " << n << endl;
2763     Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
2764
2765     // We look up the value before simplifying. If n contains quantifiers,
2766     // this may increases the chance of finding its value before the node is
2767     // altered by simplification below.
2768     n = m->getValue(n);
2769     Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
2770
2771     // Simplify the result.
2772     n = d_private->simplify(n);
2773     Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
2774
2775     // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
2776     n = d_private->d_iteRemover.replace(n);
2777     Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl;
2778
2779     // Apply our model value substitutions (again), as things may have been simplified.
2780     Debug("boolean-terms") << "applying subses to " << n << endl;
2781     n = substitutions.apply(n);
2782     Debug("boolean-terms") << "++ got " << n << endl;
2783     Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n << endl;
2784
2785     // As a last-ditch effort, ask model to simplify it.
2786     // Presently, this is only an issue for quantifiers, which can have a value
2787     // but don't show up in our substitution map above.
2788     n = m->getValue(n);
2789     Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl;
2790
2791     if (n.isConst())
2792     {
2793       if (n.getConst<bool>())
2794       {
2795         // assertion is true, everything is fine
2796         continue;
2797       }
2798     }
2799
2800     // Otherwise, we did not succeed in showing the current assertion to be
2801     // true. This may either indicate that our model is wrong, or that we cannot
2802     // check it. The latter may be the case for several reasons.
2803     // For example, quantified formulas are not checkable, although we assign
2804     // them to true/false based on the satisfying assignment. However,
2805     // quantified formulas can be modified during preprocess, so they may not
2806     // correspond to those in the satisfying assignment. Hence we throw
2807     // warnings for assertions that do not simplify to either true or false.
2808     // Other theories such as non-linear arithmetic (in particular,
2809     // transcendental functions) also have the property of not being able to
2810     // be checked precisely here.
2811     // Note that warnings like these can be avoided for quantified formulas
2812     // by making preprocessing passes explicitly record how they
2813     // rewrite quantified formulas (see cvc4-wishues#43).
2814     if (!n.isConst())
2815     {
2816       // Not constant, print a less severe warning message here.
2817       Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified "
2818                    "assertion : "
2819                 << n << endl;
2820       continue;
2821     }
2822     // Assertions that simplify to false result in an InternalError or
2823     // Warning being thrown below (when hardFailure is false).
2824     Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
2825              << endl;
2826     stringstream ss;
2827     ss << "SmtEngine::checkModel(): "
2828        << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
2829        << "assertion:     " << *i << endl
2830        << "simplifies to: " << n << endl
2831        << "expected `true'." << endl
2832        << "Run with `--check-models -v' for additional diagnostics.";
2833     if (hardFailure)
2834     {
2835       // internal error if hardFailure is true
2836       InternalError() << ss.str();
2837     }
2838     else
2839     {
2840       Warning() << ss.str() << endl;
2841     }
2842   }
2843   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
2844 }
2845
2846 void SmtEngine::checkSynthSolution()
2847 {
2848   NodeManager* nm = NodeManager::currentNM();
2849   Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl;
2850   std::map<Node, std::map<Node, Node>> sol_map;
2851   /* Get solutions and build auxiliary vectors for substituting */
2852   if (!d_theoryEngine->getSynthSolutions(sol_map))
2853   {
2854     InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!";
2855     return;
2856   }
2857   if (sol_map.empty())
2858   {
2859     InternalError() << "SmtEngine::checkSynthSolution(): Got empty solution!";
2860     return;
2861   }
2862   Trace("check-synth-sol") << "Got solution map:\n";
2863   // the set of synthesis conjectures in our assertions
2864   std::unordered_set<Node, NodeHashFunction> conjs;
2865   // For each of the above conjectures, the functions-to-synthesis and their
2866   // solutions. This is used as a substitution below.
2867   std::map<Node, std::vector<Node>> fvarMap;
2868   std::map<Node, std::vector<Node>> fsolMap;
2869   for (const std::pair<const Node, std::map<Node, Node>>& cmap : sol_map)
2870   {
2871     Trace("check-synth-sol") << "For conjecture " << cmap.first << ":\n";
2872     conjs.insert(cmap.first);
2873     std::vector<Node>& fvars = fvarMap[cmap.first];
2874     std::vector<Node>& fsols = fsolMap[cmap.first];
2875     for (const std::pair<const Node, Node>& pair : cmap.second)
2876     {
2877       Trace("check-synth-sol")
2878           << "  " << pair.first << " --> " << pair.second << "\n";
2879       fvars.push_back(pair.first);
2880       fsols.push_back(pair.second);
2881     }
2882   }
2883   Trace("check-synth-sol") << "Starting new SMT Engine\n";
2884   /* Start new SMT engine to check solutions */
2885   SmtEngine solChecker(d_exprManager, &d_options);
2886   solChecker.setIsInternalSubsolver();
2887   solChecker.setLogic(getLogicInfo());
2888   solChecker.getOptions().set(options::checkSynthSol, false);
2889   solChecker.getOptions().set(options::sygusRecFun, false);
2890
2891   Trace("check-synth-sol") << "Retrieving assertions\n";
2892   // Build conjecture from original assertions
2893   if (d_assertionList == NULL)
2894   {
2895     Trace("check-synth-sol") << "No assertions to check\n";
2896     return;
2897   }
2898   // auxiliary assertions
2899   std::vector<Node> auxAssertions;
2900   // expand definitions cache
2901   std::unordered_map<Node, Node, NodeHashFunction> cache;
2902   for (AssertionList::const_iterator i = d_assertionList->begin();
2903        i != d_assertionList->end();
2904        ++i)
2905   {
2906     Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i << endl;
2907     Trace("check-synth-sol") << "Retrieving assertion " << *i << "\n";
2908     Node assertion = Node::fromExpr(*i);
2909     // Apply any define-funs from the problem.
2910     assertion =
2911         d_private->getProcessAssertions()->expandDefinitions(assertion, cache);
2912     Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << assertion
2913              << endl;
2914     Trace("check-synth-sol") << "Expanded assertion " << assertion << "\n";
2915     if (conjs.find(assertion) == conjs.end())
2916     {
2917       Trace("check-synth-sol") << "It is an auxiliary assertion\n";
2918       auxAssertions.push_back(assertion);
2919     }
2920     else
2921     {
2922       Trace("check-synth-sol") << "It is a synthesis conjecture\n";
2923     }
2924   }
2925   // check all conjectures
2926   for (const Node& conj : conjs)
2927   {
2928     // get the solution for this conjecture
2929     std::vector<Node>& fvars = fvarMap[conj];
2930     std::vector<Node>& fsols = fsolMap[conj];
2931     // Apply solution map to conjecture body
2932     Node conjBody;
2933     /* Whether property is quantifier free */
2934     if (conj[1].getKind() != kind::EXISTS)
2935     {
2936       conjBody = conj[1].substitute(
2937           fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
2938     }
2939     else
2940     {
2941       conjBody = conj[1][1].substitute(
2942           fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
2943
2944       /* Skolemize property */
2945       std::vector<Node> vars, skos;
2946       for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j)
2947       {
2948         vars.push_back(conj[1][0][j]);
2949         std::stringstream ss;
2950         ss << "sk_" << j;
2951         skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType()));
2952         Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
2953                                  << skos.back() << "\n";
2954       }
2955       conjBody = conjBody.substitute(
2956           vars.begin(), vars.end(), skos.begin(), skos.end());
2957     }
2958     Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
2959              << conjBody << endl;
2960     Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
2961                              << "\n";
2962     solChecker.assertFormula(conjBody.toExpr());
2963     // Assert all auxiliary assertions. This may include recursive function
2964     // definitions that were added as assertions to the sygus problem.
2965     for (const Node& a : auxAssertions)
2966     {
2967       solChecker.assertFormula(a.toExpr());
2968     }
2969     Result r = solChecker.checkSat();
2970     Notice() << "SmtEngine::checkSynthSolution(): result is " << r << endl;
2971     Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
2972     if (r.asSatisfiabilityResult().isUnknown())
2973     {
2974       InternalError() << "SmtEngine::checkSynthSolution(): could not check "
2975                          "solution, result "
2976                          "unknown.";
2977     }
2978     else if (r.asSatisfiabilityResult().isSat())
2979     {
2980       InternalError()
2981           << "SmtEngine::checkSynthSolution(): produced solution leads to "
2982              "satisfiable negated conjecture.";
2983     }
2984     solChecker.resetAssertions();
2985   }
2986 }
2987
2988 void SmtEngine::checkInterpol(Expr interpol,
2989                               const std::vector<Expr>& easserts,
2990                               const Node& conj)
2991 {
2992 }
2993
2994 void SmtEngine::checkAbduct(Node a)
2995 {
2996   Assert(a.getType().isBoolean());
2997   // check it with the abduction solver
2998   return d_abductSolver->checkAbduct(a);
2999 }
3000
3001 // TODO(#1108): Simplify the error reporting of this method.
3002 UnsatCore SmtEngine::getUnsatCore() {
3003   Trace("smt") << "SMT getUnsatCore()" << endl;
3004   SmtScope smts(this);
3005   finalOptionsAreSet();
3006   if(Dump.isOn("benchmark")) {
3007     Dump("benchmark") << GetUnsatCoreCommand();
3008   }
3009   return getUnsatCoreInternal();
3010 }
3011
3012 // TODO(#1108): Simplify the error reporting of this method.
3013 const Proof& SmtEngine::getProof()
3014 {
3015   Trace("smt") << "SMT getProof()" << endl;
3016   SmtScope smts(this);
3017   finalOptionsAreSet();
3018   if(Dump.isOn("benchmark")) {
3019     Dump("benchmark") << GetProofCommand();
3020   }
3021 #if IS_PROOFS_BUILD
3022   if(!options::proof()) {
3023     throw ModalException("Cannot get a proof when produce-proofs option is off.");
3024   }
3025   if (d_smtMode != SMT_MODE_UNSAT)
3026   {
3027     throw RecoverableModalException(
3028         "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED "
3029         "response.");
3030   }
3031
3032   return ProofManager::getProof(this);
3033 #else /* IS_PROOFS_BUILD */
3034   throw ModalException("This build of CVC4 doesn't have proof support.");
3035 #endif /* IS_PROOFS_BUILD */
3036 }
3037
3038 void SmtEngine::printInstantiations( std::ostream& out ) {
3039   SmtScope smts(this);
3040   finalOptionsAreSet();
3041   if (options::instFormatMode() == options::InstFormatMode::SZS)
3042   {
3043     out << "% SZS output start Proof for " << d_filename.c_str() << std::endl;
3044   }
3045   if( d_theoryEngine ){
3046     d_theoryEngine->printInstantiations( out );
3047   }else{
3048     Assert(false);
3049   }
3050   if (options::instFormatMode() == options::InstFormatMode::SZS)
3051   {
3052     out << "% SZS output end Proof for " << d_filename.c_str() << std::endl;
3053   }
3054 }
3055
3056 void SmtEngine::printSynthSolution( std::ostream& out ) {
3057   SmtScope smts(this);
3058   finalOptionsAreSet();
3059   if( d_theoryEngine ){
3060     d_theoryEngine->printSynthSolution( out );
3061   }else{
3062     Assert(false);
3063   }
3064 }
3065
3066 bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
3067 {
3068   SmtScope smts(this);
3069   finalOptionsAreSet();
3070   std::map<Node, std::map<Node, Node>> sol_mapn;
3071   Assert(d_theoryEngine != nullptr);
3072   // fail if the theory engine does not have synthesis solutions
3073   if (!d_theoryEngine->getSynthSolutions(sol_mapn))
3074   {
3075     return false;
3076   }
3077   for (std::pair<const Node, std::map<Node, Node>>& cs : sol_mapn)
3078   {
3079     for (std::pair<const Node, Node>& s : cs.second)
3080     {
3081       sol_map[s.first.toExpr()] = s.second.toExpr();
3082     }
3083   }
3084   return true;
3085 }
3086
3087 Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
3088 {
3089   SmtScope smts(this);
3090   finalOptionsAreSet();
3091   if(!d_logic.isPure(THEORY_ARITH) && strict){
3092     Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
3093   }
3094   Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
3095   Node n_e = Node::fromExpr( e );
3096   if (n_e.getKind() != kind::EXISTS && n_e.getKind() != kind::FORALL)
3097   {
3098     throw ModalException(
3099         "Expecting a quantified formula as argument to get-qe.");
3100   }
3101   //tag the quantified formula with the quant-elim attribute
3102   TypeNode t = NodeManager::currentNM()->booleanType();
3103   Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
3104   std::vector< Node > node_values;
3105   d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
3106   n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr);
3107   n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr);
3108   std::vector< Node > e_children;
3109   e_children.push_back( n_e[0] );
3110   e_children.push_back(n_e.getKind() == kind::EXISTS ? n_e[1]
3111                                                      : n_e[1].negate());
3112   e_children.push_back( n_attr );
3113   Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
3114   Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl;
3115   Assert(nn_e.getNumChildren() == 3);
3116   Result r = checkSatisfiability(nn_e.toExpr(), true, true);
3117   Trace("smt-qe") << "Query returned " << r << std::endl;
3118   if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) {
3119     if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){
3120       Notice()
3121           << "While performing quantifier elimination, unexpected result : "
3122           << r << " for query.";
3123       // failed, return original
3124       return e;
3125     }
3126     std::vector< Node > inst_qs;
3127     d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs );
3128     Assert(inst_qs.size() <= 1);
3129     Node ret_n;
3130     if( inst_qs.size()==1 ){
3131       Node top_q = inst_qs[0];
3132       //Node top_q = Rewriter::rewrite( nn_e ).negate();
3133       Assert(top_q.getKind() == kind::FORALL);
3134       Trace("smt-qe") << "Get qe for " << top_q << std::endl;
3135       ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
3136       Trace("smt-qe") << "Returned : " << ret_n << std::endl;
3137       if (n_e.getKind() == kind::EXISTS)
3138       {
3139         ret_n = Rewriter::rewrite(ret_n.negate());
3140       }
3141     }else{
3142       ret_n = NodeManager::currentNM()->mkConst(n_e.getKind() != kind::EXISTS);
3143     }
3144     // do extended rewrite to minimize the size of the formula aggressively
3145     theory::quantifiers::ExtendedRewriter extr(true);
3146     ret_n = extr.extendedRewrite(ret_n);
3147     return ret_n.toExpr();
3148   }else {
3149     return NodeManager::currentNM()
3150         ->mkConst(n_e.getKind() == kind::EXISTS)
3151         .toExpr();
3152   }
3153 }
3154
3155 bool SmtEngine::getInterpol(const Expr& conj,
3156                             const Type& grammarType,
3157                             Expr& interpol)
3158 {
3159   return false;
3160 }
3161
3162 bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol)
3163 {
3164   Type grammarType;
3165   return getInterpol(conj, grammarType, interpol);
3166 }
3167
3168 bool SmtEngine::getAbduct(const Node& conj,
3169                           const TypeNode& grammarType,
3170                           Node& abd)
3171 {
3172   if (d_abductSolver->getAbduct(conj, grammarType, abd))
3173   {
3174     // successfully generated an abduct, update to abduct state
3175     d_smtMode = SMT_MODE_ABDUCT;
3176     return true;
3177   }
3178   // failed, we revert to the assert state
3179   d_smtMode = SMT_MODE_ASSERT;
3180   return false;
3181 }
3182
3183 bool SmtEngine::getAbduct(const Node& conj, Node& abd)
3184 {
3185   TypeNode grammarType;
3186   return getAbduct(conj, grammarType, abd);
3187 }
3188
3189 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
3190   SmtScope smts(this);
3191   if( d_theoryEngine ){
3192     std::vector< Node > qs_n;
3193     d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n );
3194     for( unsigned i=0; i<qs_n.size(); i++ ){
3195       qs.push_back( qs_n[i].toExpr() );
3196     }
3197   }else{
3198     Assert(false);
3199   }
3200 }
3201
3202 void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
3203   SmtScope smts(this);
3204   if( d_theoryEngine ){
3205     std::vector< Node > insts_n;
3206     d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n );
3207     for( unsigned i=0; i<insts_n.size(); i++ ){
3208       insts.push_back( insts_n[i].toExpr() );
3209     }
3210   }else{
3211     Assert(false);
3212   }
3213 }
3214
3215 void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) {
3216   SmtScope smts(this);
3217   Assert(options::trackInstLemmas());
3218   if( d_theoryEngine ){
3219     std::vector< std::vector< Node > > tvecs_n;
3220     d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n );
3221     for( unsigned i=0; i<tvecs_n.size(); i++ ){
3222       std::vector< Expr > tvec;
3223       for( unsigned j=0; j<tvecs_n[i].size(); j++ ){
3224         tvec.push_back( tvecs_n[i][j].toExpr() );
3225       }
3226       tvecs.push_back( tvec );
3227     }
3228   }else{
3229     Assert(false);
3230   }
3231 }
3232
3233 vector<Expr> SmtEngine::getAssertions() {
3234   SmtScope smts(this);
3235   finalOptionsAreSet();
3236   doPendingPops();
3237   if(Dump.isOn("benchmark")) {
3238     Dump("benchmark") << GetAssertionsCommand();
3239   }
3240   Trace("smt") << "SMT getAssertions()" << endl;
3241   if(!options::produceAssertions()) {
3242     const char* msg =
3243       "Cannot query the current assertion list when not in produce-assertions mode.";
3244     throw ModalException(msg);
3245   }
3246   Assert(d_assertionList != NULL);
3247   // copy the result out
3248   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
3249 }
3250
3251 void SmtEngine::push()
3252 {
3253   SmtScope smts(this);
3254   finalOptionsAreSet();
3255   doPendingPops();
3256   Trace("smt") << "SMT push()" << endl;
3257   d_private->notifyPush();
3258   d_private->processAssertions();
3259   if(Dump.isOn("benchmark")) {
3260     Dump("benchmark") << PushCommand();
3261   }
3262   if(!options::incrementalSolving()) {
3263     throw ModalException("Cannot push when not solving incrementally (use --incremental)");
3264   }
3265
3266
3267   // The problem isn't really "extended" yet, but this disallows
3268   // get-model after a push, simplifying our lives somewhat and
3269   // staying symmetric with pop.
3270   setProblemExtended();
3271
3272   d_userLevels.push_back(d_userContext->getLevel());
3273   internalPush();
3274   Trace("userpushpop") << "SmtEngine: pushed to level "
3275                        << d_userContext->getLevel() << endl;
3276 }
3277
3278 void SmtEngine::pop() {
3279   SmtScope smts(this);
3280   finalOptionsAreSet();
3281   Trace("smt") << "SMT pop()" << endl;
3282   if(Dump.isOn("benchmark")) {
3283     Dump("benchmark") << PopCommand();
3284   }
3285   if(!options::incrementalSolving()) {
3286     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
3287   }
3288   if(d_userLevels.size() == 0) {
3289     throw ModalException("Cannot pop beyond the first user frame");
3290   }
3291
3292   // The problem isn't really "extended" yet, but this disallows
3293   // get-model after a pop, simplifying our lives somewhat.  It might
3294   // not be strictly necessary to do so, since the pops occur lazily,
3295   // but also it would be weird to have a legally-executed (get-model)
3296   // that only returns a subset of the assignment (because the rest
3297   // is no longer in scope!).
3298   setProblemExtended();
3299
3300   AlwaysAssert(d_userContext->getLevel() > 0);
3301   AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
3302   while (d_userLevels.back() < d_userContext->getLevel()) {
3303     internalPop(true);
3304   }
3305   d_userLevels.pop_back();
3306
3307   // Clear out assertion queues etc., in case anything is still in there
3308   d_private->notifyPop();
3309
3310   Trace("userpushpop") << "SmtEngine: popped to level "
3311                        << d_userContext->getLevel() << endl;
3312   // FIXME: should we reset d_status here?
3313   // SMT-LIBv2 spec seems to imply no, but it would make sense to..
3314 }
3315
3316 void SmtEngine::internalPush() {
3317   Assert(d_fullyInited);
3318   Trace("smt") << "SmtEngine::internalPush()" << endl;
3319   doPendingPops();
3320   if(options::incrementalSolving()) {
3321     d_private->processAssertions();
3322     TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
3323     d_userContext->push();
3324     // the d_context push is done inside of the SAT solver
3325     d_propEngine->push();
3326   }
3327 }
3328
3329 void SmtEngine::internalPop(bool immediate) {
3330   Assert(d_fullyInited);
3331   Trace("smt") << "SmtEngine::internalPop()" << endl;
3332   if(options::incrementalSolving()) {
3333     ++d_pendingPops;
3334   }
3335   if(immediate) {
3336     doPendingPops();
3337   }
3338 }
3339
3340 void SmtEngine::doPendingPops() {
3341   Trace("smt") << "SmtEngine::doPendingPops()" << endl;
3342   Assert(d_pendingPops == 0 || options::incrementalSolving());
3343   // check to see if a postsolve() is pending
3344   if (d_needPostsolve)
3345   {
3346     d_propEngine->resetTrail();
3347   }
3348   while(d_pendingPops > 0) {
3349     TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
3350     d_propEngine->pop();
3351     // the d_context pop is done inside of the SAT solver
3352     d_userContext->pop();
3353     --d_pendingPops;
3354   }
3355   if (d_needPostsolve)
3356   {
3357     d_theoryEngine->postsolve();
3358     d_needPostsolve = false;
3359   }
3360 }
3361
3362 void SmtEngine::reset()
3363 {
3364   SmtScope smts(this);
3365   ExprManager *em = d_exprManager;
3366   Trace("smt") << "SMT reset()" << endl;
3367   if(Dump.isOn("benchmark")) {
3368     Dump("benchmark") << ResetCommand();
3369   }
3370   Options opts;
3371   opts.copyValues(d_originalOptions);
3372   this->~SmtEngine();
3373   new (this) SmtEngine(em, &opts);
3374 }
3375
3376 void SmtEngine::resetAssertions()
3377 {
3378   SmtScope smts(this);
3379
3380   if (!d_fullyInited)
3381   {
3382     // We're still in Start Mode, nothing asserted yet, do nothing.
3383     // (see solver execution modes in the SMT-LIB standard)
3384     Assert(d_context->getLevel() == 0);
3385     Assert(d_userContext->getLevel() == 0);
3386     DeleteAndClearCommandVector(d_modelGlobalCommands);
3387     return;
3388   }
3389
3390   doPendingPops();
3391
3392   Trace("smt") << "SMT resetAssertions()" << endl;
3393   if (Dump.isOn("benchmark"))
3394   {
3395     Dump("benchmark") << ResetAssertionsCommand();
3396   }
3397
3398   while (!d_userLevels.empty())
3399   {
3400     pop();
3401   }
3402
3403   // Remember the global push/pop around everything when beyond Start mode
3404   // (see solver execution modes in the SMT-LIB standard)
3405   Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
3406   d_context->popto(0);
3407   d_userContext->popto(0);
3408   DeleteAndClearCommandVector(d_modelGlobalCommands);
3409   d_userContext->push();
3410   d_context->push();
3411
3412   /* Create new PropEngine.
3413    * First force destruction of referenced PropEngine to enforce that
3414    * statistics are unregistered by the obsolete PropEngine object before
3415    * registered again by the new PropEngine object */
3416   d_propEngine.reset(nullptr);
3417   d_propEngine.reset(new PropEngine(
3418       getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
3419   d_theoryEngine->setPropEngine(getPropEngine());
3420 }
3421
3422 void SmtEngine::interrupt()
3423 {
3424   if(!d_fullyInited) {
3425     return;
3426   }
3427   d_propEngine->interrupt();
3428   d_theoryEngine->interrupt();
3429 }
3430
3431 void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
3432   d_resourceManager->setResourceLimit(units, cumulative);
3433 }
3434 void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) {
3435   d_resourceManager->setTimeLimit(milis, cumulative);
3436 }
3437
3438 unsigned long SmtEngine::getResourceUsage() const {
3439   return d_resourceManager->getResourceUsage();
3440 }
3441
3442 unsigned long SmtEngine::getTimeUsage() const {
3443   return d_resourceManager->getTimeUsage();
3444 }
3445
3446 unsigned long SmtEngine::getResourceRemaining() const
3447 {
3448   return d_resourceManager->getResourceRemaining();
3449 }
3450
3451 unsigned long SmtEngine::getTimeRemaining() const
3452 {
3453   return d_resourceManager->getTimeRemaining();
3454 }
3455
3456 NodeManager* SmtEngine::getNodeManager() const
3457 {
3458   return d_exprManager->getNodeManager();
3459 }
3460
3461 Statistics SmtEngine::getStatistics() const
3462 {
3463   return Statistics(*d_statisticsRegistry);
3464 }
3465
3466 SExpr SmtEngine::getStatistic(std::string name) const
3467 {
3468   return d_statisticsRegistry->getStatistic(name);
3469 }
3470
3471 void SmtEngine::safeFlushStatistics(int fd) const {
3472   d_statisticsRegistry->safeFlushInformation(fd);
3473 }
3474
3475 void SmtEngine::setUserAttribute(const std::string& attr,
3476                                  Expr expr,
3477                                  const std::vector<Expr>& expr_values,
3478                                  const std::string& str_value)
3479 {
3480   SmtScope smts(this);
3481   finalOptionsAreSet();
3482   std::vector<Node> node_values;
3483   for( unsigned i=0; i<expr_values.size(); i++ ){
3484     node_values.push_back( expr_values[i].getNode() );
3485   }
3486   d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
3487 }
3488
3489 void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
3490   Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
3491   for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){
3492     Command * c = d_modelGlobalCommands[i];
3493     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
3494     if(dfc != NULL) {
3495       if( dfc->getFunction()==f ){
3496         dfc->setPrintInModel( p );
3497       }
3498     }
3499   }
3500   for( unsigned i=0; i<d_modelCommands->size(); i++ ){
3501     Command * c = (*d_modelCommands)[i];
3502     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
3503     if(dfc != NULL) {
3504       if( dfc->getFunction()==f ){
3505         dfc->setPrintInModel( p );
3506       }
3507     }
3508   }
3509 }
3510
3511 void SmtEngine::beforeSearch()
3512 {
3513   if(d_fullyInited) {
3514     throw ModalException(
3515         "SmtEngine::beforeSearch called after initialization.");
3516   }
3517 }
3518
3519
3520 void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
3521 {
3522   NodeManagerScope nms(d_nodeManager);
3523   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
3524
3525   if(Dump.isOn("benchmark")) {
3526     Dump("benchmark") << SetOptionCommand(key, value);
3527   }
3528
3529   if(key == "command-verbosity") {
3530     if(!value.isAtom()) {
3531       const vector<SExpr>& cs = value.getChildren();
3532       if(cs.size() == 2 &&
3533          (cs[0].isKeyword() || cs[0].isString()) &&
3534          cs[1].isInteger()) {
3535         string c = cs[0].getValue();
3536         const Integer& v = cs[1].getIntegerValue();
3537         if(v < 0 || v > 2) {
3538           throw OptionException("command-verbosity must be 0, 1, or 2");
3539         }
3540         d_commandVerbosity[c] = v;
3541         return;
3542       }
3543     }
3544     throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
3545   }
3546
3547   if(!value.isAtom()) {
3548     throw OptionException("bad value for :" + key);
3549   }
3550
3551   string optionarg = value.getValue();
3552   d_options.setOption(key, optionarg);
3553 }
3554
3555 void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
3556
3557 bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
3558
3559 CVC4::SExpr SmtEngine::getOption(const std::string& key) const
3560 {
3561   NodeManagerScope nms(d_nodeManager);
3562
3563   Trace("smt") << "SMT getOption(" << key << ")" << endl;
3564
3565   if(key.length() >= 18 &&
3566      key.compare(0, 18, "command-verbosity:") == 0) {
3567     map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18);
3568     if(i != d_commandVerbosity.end()) {
3569       return SExpr((*i).second);
3570     }
3571     i = d_commandVerbosity.find("*");
3572     if(i != d_commandVerbosity.end()) {
3573       return SExpr((*i).second);
3574     }
3575     return SExpr(Integer(2));
3576   }
3577
3578   if(Dump.isOn("benchmark")) {
3579     Dump("benchmark") << GetOptionCommand(key);
3580   }
3581
3582   if(key == "command-verbosity") {
3583     vector<SExpr> result;
3584     SExpr defaultVerbosity;
3585     for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
3586         i != d_commandVerbosity.end();
3587         ++i) {
3588       vector<SExpr> v;
3589       v.push_back(SExpr((*i).first));
3590       v.push_back(SExpr((*i).second));
3591       if((*i).first == "*") {
3592         // put the default at the end of the SExpr
3593         defaultVerbosity = SExpr(v);
3594       } else {
3595         result.push_back(SExpr(v));
3596       }
3597     }
3598     // put the default at the end of the SExpr
3599     if(!defaultVerbosity.isAtom()) {
3600       result.push_back(defaultVerbosity);
3601     } else {
3602       // ensure the default is always listed
3603       vector<SExpr> v;
3604       v.push_back(SExpr("*"));
3605       v.push_back(SExpr(Integer(2)));
3606       result.push_back(SExpr(v));
3607     }
3608     return SExpr(result);
3609   }
3610
3611   return SExpr::parseAtom(d_options.getOption(key));
3612 }
3613
3614 bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
3615   return d_private->getExpressionName(e, name);
3616 }
3617
3618 void SmtEngine::setExpressionName(Expr e, const std::string& name) {
3619   Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl;
3620   d_private->setExpressionName(e,name);
3621 }
3622
3623 Options& SmtEngine::getOptions() { return d_options; }
3624
3625 const Options& SmtEngine::getOptions() const { return d_options; }
3626
3627 ResourceManager* SmtEngine::getResourceManager()
3628 {
3629   return d_resourceManager.get();
3630 }
3631
3632 void SmtEngine::setSygusConjectureStale()
3633 {
3634   if (d_private->d_sygusConjectureStale)
3635   {
3636     // already stale
3637     return;
3638   }
3639   d_private->d_sygusConjectureStale = true;
3640   if (options::incrementalSolving())
3641   {
3642     internalPop();
3643   }
3644 }
3645
3646 }/* CVC4 namespace */