src/smt/smt_engine.cpp

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