src/theory/theory_engine.h

   1 /*********************                                                        */
   2 /*! \file theory_engine.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The theory engine
  13  **
  14  ** The theory engine.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY_ENGINE_H
  20 #define CVC4__THEORY_ENGINE_H
  21
  22 #include <deque>
  23 #include <memory>
  24 #include <set>
  25 #include <unordered_map>
  26 #include <utility>
  27 #include <vector>
  28
  29 #include "base/check.h"
  30 #include "context/cdhashset.h"
  31 #include "expr/node.h"
  32 #include "options/options.h"
  33 #include "options/smt_options.h"
  34 #include "options/theory_options.h"
  35 #include "prop/prop_engine.h"
  36 #include "smt/command.h"
  37 #include "theory/atom_requests.h"
  38 #include "theory/decision_manager.h"
  39 #include "theory/engine_output_channel.h"
  40 #include "theory/interrupted.h"
  41 #include "theory/rewriter.h"
  42 #include "theory/shared_terms_database.h"
  43 #include "theory/sort_inference.h"
  44 #include "theory/substitutions.h"
  45 #include "theory/term_registration_visitor.h"
  46 #include "theory/theory.h"
  47 #include "theory/theory_preprocessor.h"
  48 #include "theory/uf/equality_engine.h"
  49 #include "theory/valuation.h"
  50 #include "util/hash.h"
  51 #include "util/resource_manager.h"
  52 #include "util/statistics_registry.h"
  53 #include "util/unsafe_interrupt_exception.h"
  54
  55 namespace CVC4 {
  56
  57 class ResourceManager;
  58 class LemmaProofRecipe;
  59
  60 /**
  61  * A pair of a theory and a node. This is used to mark the flow of
  62  * propagations between theories.
  63  */
  64 struct NodeTheoryPair {
  65   Node d_node;
  66   theory::TheoryId d_theory;
  67   size_t d_timestamp;
  68   NodeTheoryPair(TNode n, theory::TheoryId t, size_t ts = 0)
  69       : d_node(n), d_theory(t), d_timestamp(ts)
  70   {
  71   }
  72   NodeTheoryPair() : d_theory(theory::THEORY_LAST), d_timestamp() {}
  73   // Comparison doesn't take into account the timestamp
  74   bool operator == (const NodeTheoryPair& pair) const {
  75     return d_node == pair.d_node && d_theory == pair.d_theory;
  76   }
  77 };/* struct NodeTheoryPair */
  78
  79 struct NodeTheoryPairHashFunction {
  80   NodeHashFunction hashFunction;
  81   // Hash doesn't take into account the timestamp
  82   size_t operator()(const NodeTheoryPair& pair) const {
  83     uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node));
  84     return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash));
  85   }
  86 };/* struct NodeTheoryPairHashFunction */
  87
  88
  89 /* Forward declarations */
  90 namespace theory {
  91   class TheoryModel;
  92   class TheoryEngineModelBuilder;
  93   class EqEngineManagerDistributed;
  94
  95   namespace eq {
  96     class EqualityEngine;
  97   }/* CVC4::theory::eq namespace */
  98
  99   namespace quantifiers {
 100     class TermDb;
 101   }
 102
 103   class EntailmentCheckParameters;
 104   class EntailmentCheckSideEffects;
 105 }/* CVC4::theory namespace */
 106
 107 class RemoveTermFormulas;
 108
 109 /**
 110  * This is essentially an abstraction for a collection of theories.  A
 111  * TheoryEngine provides services to a PropEngine, making various
 112  * T-solvers look like a single unit to the propositional part of
 113  * CVC4.
 114  */
 115 class TheoryEngine {
 116
 117   /** Shared terms database can use the internals notify the theories */
 118   friend class SharedTermsDatabase;
 119   friend class theory::quantifiers::TermDb;
 120   friend class theory::EngineOutputChannel;
 121
 122   /** Associated PropEngine engine */
 123   prop::PropEngine* d_propEngine;
 124
 125   /** Our context */
 126   context::Context* d_context;
 127
 128   /** Our user context */
 129   context::UserContext* d_userContext;
 130
 131   /**
 132    * A table of from theory IDs to theory pointers. Never use this table
 133    * directly, use theoryOf() instead.
 134    */
 135   theory::Theory* d_theoryTable[theory::THEORY_LAST];
 136
 137   /**
 138    * A collection of theories that are "active" for the current run.
 139    * This set is provided by the user (as a logic string, say, in SMT-LIBv2
 140    * format input), or else by default it's all-inclusive.  This is important
 141    * because we can optimize for single-theory runs (no sharing), can reduce
 142    * the cost of walking the DAG on registration, etc.
 143    */
 144   const LogicInfo& d_logicInfo;
 145
 146   /**
 147    * The database of shared terms.
 148    */
 149   SharedTermsDatabase d_sharedTerms;
 150
 151   /**
 152    * The distributed equality manager. This class is responsible for
 153    * configuring the theories of this class for handling equalties
 154    * in a "distributed" fashion, i.e. each theory maintains a unique
 155    * instance of an equality engine. These equality engines are memory
 156    * managed by this class.
 157    */
 158   std::unique_ptr<theory::EqEngineManagerDistributed> d_eeDistributed;
 159
 160   /**
 161    * The quantifiers engine
 162    */
 163   theory::QuantifiersEngine* d_quantEngine;
 164   /**
 165    * The decision manager
 166    */
 167   std::unique_ptr<theory::DecisionManager> d_decManager;
 168
 169   /**
 170    * Default model object
 171    */
 172   theory::TheoryModel* d_curr_model;
 173   bool d_aloc_curr_model;
 174   /**
 175    * Model builder object
 176    */
 177   theory::TheoryEngineModelBuilder* d_curr_model_builder;
 178   bool d_aloc_curr_model_builder;
 179   /** are we in eager model building mode? (see setEagerModelBuilding). */
 180   bool d_eager_model_building;
 181
 182   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
 183   typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
 184
 185   /**
 186    * Used for "missed-t-propagations" dumping mode only.  A set of all
 187    * theory-propagable literals.
 188    */
 189   context::CDList<TNode> d_possiblePropagations;
 190
 191   /**
 192    * Used for "missed-t-propagations" dumping mode only.  A
 193    * context-dependent set of those theory-propagable literals that
 194    * have been propagated.
 195    */
 196   context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
 197
 198   /**
 199    * Output channels for individual theories.
 200    */
 201   theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
 202
 203   /**
 204    * Are we in conflict.
 205    */
 206   context::CDO<bool> d_inConflict;
 207
 208   /**
 209    * Are we in "SAT mode"? In this state, the user can query for the model.
 210    * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB
 211    * standard, version 2.6.
 212    */
 213   bool d_inSatMode;
 214
 215   /**
 216    * Called by the theories to notify of a conflict.
 217    */
 218   void conflict(TNode conflict, theory::TheoryId theoryId);
 219
 220   /**
 221    * Debugging flag to ensure that shutdown() is called before the
 222    * destructor.
 223    */
 224   bool d_hasShutDown;
 225
 226   /**
 227    * True if a theory has notified us of incompleteness (at this
 228    * context level or below).
 229    */
 230   context::CDO<bool> d_incomplete;
 231
 232   /**
 233    * Called by the theories to notify that the current branch is incomplete.
 234    */
 235   void setIncomplete(theory::TheoryId theory) {
 236     d_incomplete = true;
 237   }
 238
 239
 240   /**
 241    * Mapping of propagations from recievers to senders.
 242    */
 243   typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap;
 244   PropagationMap d_propagationMap;
 245
 246   /**
 247    * Timestamp of propagations
 248    */
 249   context::CDO<size_t> d_propagationMapTimestamp;
 250
 251   /**
 252    * Literals that are propagated by the theory. Note that these are TNodes.
 253    * The theory can only propagate nodes that have an assigned literal in the
 254    * SAT solver and are hence referenced in the SAT solver.
 255    */
 256   context::CDList<TNode> d_propagatedLiterals;
 257
 258   /**
 259    * The index of the next literal to be propagated by a theory.
 260    */
 261   context::CDO<unsigned> d_propagatedLiteralsIndex;
 262
 263   /**
 264    * Called by the output channel to propagate literals and facts
 265    * @return false if immediate conflict
 266    */
 267   bool propagate(TNode literal, theory::TheoryId theory);
 268
 269   /**
 270    * Internal method to call the propagation routines and collect the
 271    * propagated literals.
 272    */
 273   void propagate(theory::Theory::Effort effort);
 274
 275   /**
 276    * A variable to mark if we added any lemmas.
 277    */
 278   bool d_lemmasAdded;
 279
 280   /**
 281    * A variable to mark if the OutputChannel was "used" by any theory
 282    * since the start of the last check.  If it has been, we require
 283    * a FULL_EFFORT check before exiting and reporting SAT.
 284    *
 285    * See the documentation for the needCheck() function, below.
 286    */
 287   bool d_outputChannelUsed;
 288
 289   /** Atom requests from lemmas */
 290   AtomRequests d_atomRequests;
 291
 292   /**
 293    * Adds a new lemma, returning its status.
 294    * @param node the lemma
 295    * @param negated should the lemma be asserted negated
 296    * @param p the properties of the lemma.
 297    */
 298   theory::LemmaStatus lemma(TNode node,
 299                             ProofRule rule,
 300                             bool negated,
 301                             theory::LemmaProperty p,
 302                             theory::TheoryId atomsTo);
 303
 304   /** Enusre that the given atoms are send to the given theory */
 305   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
 306
 307   /** sort inference module */
 308   SortInference d_sortInfer;
 309
 310   /** The theory preprocessor */
 311   theory::TheoryPreprocessor d_tpp;
 312
 313   /** Time spent in theory combination */
 314   TimerStat d_combineTheoriesTime;
 315
 316   Node d_true;
 317   Node d_false;
 318
 319   /** Whether we were just interrupted (or not) */
 320   bool d_interrupted;
 321   ResourceManager* d_resourceManager;
 322
 323  public:
 324   /** Constructs a theory engine */
 325   TheoryEngine(context::Context* context,
 326                context::UserContext* userContext,
 327                ResourceManager* rm,
 328                RemoveTermFormulas& iteRemover,
 329                const LogicInfo& logic);
 330
 331   /** Destroys a theory engine */
 332   ~TheoryEngine();
 333
 334   void interrupt();
 335
 336   /** "Spend" a resource during a search or preprocessing.*/
 337   void spendResource(ResourceManager::Resource r);
 338
 339   /**
 340    * Adds a theory. Only one theory per TheoryId can be present, so if
 341    * there is another theory it will be deleted.
 342    */
 343   template <class TheoryClass>
 344   inline void addTheory(theory::TheoryId theoryId)
 345   {
 346     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
 347     d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
 348     d_theoryTable[theoryId] = new TheoryClass(d_context,
 349                                               d_userContext,
 350                                               *d_theoryOut[theoryId],
 351                                               theory::Valuation(this),
 352                                               d_logicInfo,
 353                                               nullptr);
 354     theory::Rewriter::registerTheoryRewriter(
 355         theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
 356   }
 357
 358   void setPropEngine(prop::PropEngine* propEngine)
 359   {
 360     d_propEngine = propEngine;
 361   }
 362
 363   /**
 364    * Called when all initialization of options/logic is done, after theory
 365    * objects have been created.
 366    *
 367    * This initializes the quantifiers engine, the "official" equality engines
 368    * of each theory as required, and the model and model builder utilities.
 369    */
 370   void finishInit();
 371
 372   /**
 373    * Get a pointer to the underlying propositional engine.
 374    */
 375   inline prop::PropEngine* getPropEngine() const {
 376     return d_propEngine;
 377   }
 378
 379   /**
 380    * Get a pointer to the underlying sat context.
 381    */
 382   inline context::Context* getSatContext() const {
 383     return d_context;
 384   }
 385
 386   /**
 387    * Get a pointer to the underlying user context.
 388    */
 389   inline context::Context* getUserContext() const {
 390     return d_userContext;
 391   }
 392
 393   /**
 394    * Get a pointer to the underlying quantifiers engine.
 395    */
 396   theory::QuantifiersEngine* getQuantifiersEngine() const {
 397     return d_quantEngine;
 398   }
 399   /**
 400    * Get a pointer to the underlying decision manager.
 401    */
 402   theory::DecisionManager* getDecisionManager() const
 403   {
 404     return d_decManager.get();
 405   }
 406
 407  private:
 408   /**
 409    * Queue of nodes for pre-registration.
 410    */
 411   std::queue<TNode> d_preregisterQueue;
 412
 413   /**
 414    * Boolean flag denoting we are in pre-registration.
 415    */
 416   bool d_inPreregister;
 417
 418   /**
 419    * Did the theories get any new facts since the last time we called
 420    * check()
 421    */
 422   context::CDO<bool> d_factsAsserted;
 423
 424   /**
 425    * Map from equality atoms to theories that would like to be notified about them.
 426    */
 427
 428
 429   /**
 430    * Assert the formula to the given theory.
 431    * @param assertion the assertion to send (not necesserily normalized)
 432    * @param original the assertion as it was sent in from the propagating theory
 433    * @param toTheoryId the theory to assert to
 434    * @param fromTheoryId the theory that sent it
 435    */
 436   void assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
 437
 438   /**
 439    * Marks a theory propagation from a theory to a theory where a
 440    * theory could be the THEORY_SAT_SOLVER for literals coming from
 441    * or being propagated to the SAT solver. If the receiving theory
 442    * already recieved the literal, the method returns false, otherwise
 443    * it returns true.
 444    *
 445    * @param assertion the normalized assertion being sent
 446    * @param originalAssertion the actual assertion that was sent
 447    * @param toTheoryId the theory that is on the receiving end
 448    * @param fromTheoryId the theory that sent the assertion
 449    * @return true if a new assertion, false if theory already got it
 450    */
 451   bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
 452
 453   /**
 454    * Computes the explanation by travarsing the propagation graph and
 455    * asking relevant theories to explain the propagations. Initially
 456    * the explanation vector should contain only the element (node, theory)
 457    * where the node is the one to be explained, and the theory is the
 458    * theory that sent the literal. The lemmaProofRecipe will contain a list
 459    * of the explanation steps required to produce the original node.
 460    */
 461   void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
 462
 463 public:
 464
 465   /**
 466    * Signal the start of a new round of assertion preprocessing
 467    */
 468   void preprocessStart();
 469
 470   /**
 471    * Runs theory specific preprocessing on the non-Boolean parts of
 472    * the formula.  This is only called on input assertions, after ITEs
 473    * have been removed.
 474    */
 475   Node preprocess(TNode node);
 476
 477   /** Notify (preprocessed) assertions. */
 478   void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
 479
 480   /** Return whether or not we are incomplete (in the current context). */
 481   inline bool isIncomplete() const { return d_incomplete; }
 482
 483   /**
 484    * Returns true if we need another round of checking.  If this
 485    * returns true, check(FULL_EFFORT) _must_ be called by the
 486    * propositional layer before reporting SAT.
 487    *
 488    * This is especially necessary for incomplete theories that lazily
 489    * output some lemmas on FULL_EFFORT check (e.g. quantifier reasoning
 490    * outputing quantifier instantiations).  In such a case, a lemma can
 491    * be asserted that is simplified away (perhaps it's already true).
 492    * However, we must maintain the invariant that, if a theory uses the
 493    * OutputChannel, it implicitly requests that another check(FULL_EFFORT)
 494    * be performed before exit, even if no new facts are on its fact queue,
 495    * as it might decide to further instantiate some lemmas, precluding
 496    * a SAT response.
 497    */
 498   inline bool needCheck() const {
 499     return d_outputChannelUsed || d_lemmasAdded;
 500   }
 501
 502   /**
 503    * This is called at shutdown time by the SmtEngine, just before
 504    * destruction.  It is important because there are destruction
 505    * ordering issues between PropEngine and Theory.
 506    */
 507   void shutdown();
 508
 509   /**
 510    * Solve the given literal with a theory that owns it.
 511    */
 512   theory::Theory::PPAssertStatus solve(TNode literal,
 513                                     theory::SubstitutionMap& substitutionOut);
 514
 515   /**
 516    * Preregister a Theory atom with the responsible theory (or
 517    * theories).
 518    */
 519   void preRegister(TNode preprocessed);
 520
 521   /**
 522    * Assert the formula to the appropriate theory.
 523    * @param node the assertion
 524    */
 525   void assertFact(TNode node);
 526
 527   /**
 528    * Check all (currently-active) theories for conflicts.
 529    * @param effort the effort level to use
 530    */
 531   void check(theory::Theory::Effort effort);
 532
 533   /**
 534    * Run the combination framework.
 535    */
 536   void combineTheories();
 537
 538   /**
 539    * Calls ppStaticLearn() on all theories, accumulating their
 540    * combined contributions in the "learned" builder.
 541    */
 542   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 543
 544   /**
 545    * Calls presolve() on all theories and returns true
 546    * if one of the theories discovers a conflict.
 547    */
 548   bool presolve();
 549
 550    /**
 551    * Calls postsolve() on all theories.
 552    */
 553   void postsolve();
 554
 555   /**
 556    * Calls notifyRestart() on all active theories.
 557    */
 558   void notifyRestart();
 559
 560   void getPropagatedLiterals(std::vector<TNode>& literals) {
 561     for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) {
 562       Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl;
 563       literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]);
 564     }
 565   }
 566
 567   /**
 568    * Returns the next decision request, or null if none exist. The next
 569    * decision request is a literal that this theory engine prefers the SAT
 570    * solver to make as its next decision. Decision requests are managed by
 571    * the decision manager d_decManager.
 572    */
 573   Node getNextDecisionRequest();
 574
 575   bool properConflict(TNode conflict) const;
 576   bool properPropagation(TNode lit) const;
 577   bool properExplanation(TNode node, TNode expl) const;
 578
 579   /**
 580    * Returns an explanation of the node propagated to the SAT solver.
 581    */
 582   Node getExplanation(TNode node);
 583
 584   /**
 585    * Returns an explanation of the node propagated to the SAT solver and the theory
 586    * that propagated it.
 587    */
 588   Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
 589
 590   /**
 591    * collect model info
 592    */
 593   bool collectModelInfo(theory::TheoryModel* m);
 594   /** post process model */
 595   void postProcessModel( theory::TheoryModel* m );
 596
 597   /**
 598    * Get the pointer to the model object used by this theory engine.
 599    */
 600   theory::TheoryModel* getModel();
 601   /**
 602    * Get the current model for the current set of assertions. This method
 603    * should only be called immediately after a satisfiable or unknown
 604    * response to a check-sat call, and only if produceModels is true.
 605    *
 606    * If the model is not already built, this will cause this theory engine
 607    * to build the model.
 608    *
 609    * If the model is not available (for instance, if the last call to check-sat
 610    * was interrupted), then this returns the null pointer.
 611    */
 612   theory::TheoryModel* getBuiltModel();
 613   /** set eager model building
 614    *
 615    * If this method is called, then this TheoryEngine will henceforth build
 616    * its model immediately after every satisfiability check that results
 617    * in a satisfiable or unknown result. The motivation for this mode is to
 618    * accomodate API users that get the model object from the TheoryEngine,
 619    * where we want to ensure that this model is always valid.
 620    * TODO (#2648): revisit this.
 621    */
 622   void setEagerModelBuilding() { d_eager_model_building = true; }
 623
 624   /** get synth solutions
 625    *
 626    * This method returns true if there is a synthesis solution available. This
 627    * is the case if the last call to check satisfiability originated in a
 628    * check-synth call, and the synthesis solver successfully found a solution
 629    * for all active synthesis conjectures.
 630    *
 631    * This method adds entries to sol_map that map functions-to-synthesize with
 632    * their solutions, for all active conjectures. This should be called
 633    * immediately after the solver answers unsat for sygus input.
 634    *
 635    * For details on what is added to sol_map, see
 636    * SynthConjecture::getSynthSolutions.
 637    */
 638   bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
 639
 640   /**
 641    * Get the model builder
 642    */
 643   theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; }
 644
 645   /**
 646    * Get the theory associated to a given Node.
 647    *
 648    * @returns the theory, or NULL if the TNode is
 649    * of built-in type.
 650    */
 651   inline theory::Theory* theoryOf(TNode node) const {
 652     return d_theoryTable[theory::Theory::theoryOf(node)];
 653   }
 654
 655   /**
 656    * Get the theory associated to a the given theory id.
 657    *
 658    * @returns the theory
 659    */
 660   inline theory::Theory* theoryOf(theory::TheoryId theoryId) const {
 661     Assert(theoryId < theory::THEORY_LAST);
 662     return d_theoryTable[theoryId];
 663   }
 664
 665   inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
 666     return d_logicInfo.isTheoryEnabled(theoryId);
 667   }
 668   /** get the logic info used by this theory engine */
 669   const LogicInfo& getLogicInfo() const;
 670   /**
 671    * Returns the equality status of the two terms, from the theory
 672    * that owns the domain type.  The types of a and b must be the same.
 673    */
 674   theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
 675
 676   /**
 677    * Returns the value that a theory that owns the type of var currently
 678    * has (or null if none);
 679    */
 680   Node getModelValue(TNode var);
 681
 682   /**
 683    * Takes a literal and returns an equivalent literal that is guaranteed to be a SAT literal
 684    */
 685   Node ensureLiteral(TNode n);
 686
 687   /**
 688    * Print all instantiations made by the quantifiers module.
 689    */
 690   void printInstantiations( std::ostream& out );
 691
 692   /**
 693    * Print solution for synthesis conjectures found by ce_guided_instantiation module
 694    */
 695   void printSynthSolution( std::ostream& out );
 696
 697   /**
 698    * Get list of quantified formulas that were instantiated
 699    */
 700   void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
 701
 702   /**
 703    * Get instantiation methods
 704    *   first inputs forall x.q[x] and returns ( q[a], ..., q[z] )
 705    *   second inputs forall x.q[x] and returns ( a, ..., z )
 706    *   third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) , ... , forall x.qn[x] -> ( qn[a]...qn[z] )
 707    */
 708   void getInstantiations( Node q, std::vector< Node >& insts );
 709   void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
 710   void getInstantiations( std::map< Node, std::vector< Node > >& insts );
 711   void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
 712
 713   /**
 714    * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q.
 715    *   Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q
 716    */
 717   Node getInstantiatedConjunction( Node q );
 718
 719   /**
 720    * Forwards an entailment check according to the given theoryOfMode.
 721    * See theory.h for documentation on entailmentCheck().
 722    */
 723   std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
 724
 725  private:
 726   /** Default visitor for pre-registration */
 727   PreRegisterVisitor d_preRegistrationVisitor;
 728
 729   /** Visitor for collecting shared terms */
 730   SharedTermsVisitor d_sharedTermsVisitor;
 731
 732   /** Dump the assertions to the dump */
 733   void dumpAssertions(const char* tag);
 734
 735   /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
 736 public:
 737
 738   SharedTermsDatabase* getSharedTermsDatabase();
 739
 740   SortInference* getSortInference() { return &d_sortInfer; }
 741
 742   /** Prints the assertions to the debug stream */
 743   void printAssertions(const char* tag);
 744
 745 private:
 746
 747   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 748
 749  public:
 750   /** Set user attribute.
 751    *
 752    * This function is called when an attribute is set by a user.  In SMT-LIBv2
 753    * this is done via the syntax (! n :attr)
 754    */
 755   void setUserAttribute(const std::string& attr,
 756                         Node n,
 757                         const std::vector<Node>& node_values,
 758                         const std::string& str_value);
 759
 760   /** Handle user attribute.
 761    *
 762    * Associates theory t with the attribute attr.  Theory t will be
 763    * notified whenever an attribute of name attr is set.
 764    */
 765   void handleUserAttribute(const char* attr, theory::Theory* t);
 766
 767   /**
 768    * Check that the theory assertions are satisfied in the model.
 769    * This function is called from the smt engine's checkModel routine.
 770    */
 771   void checkTheoryAssertionsWithModel(bool hardFailure);
 772
 773  private:
 774   IntStat d_arithSubstitutionsAdded;
 775
 776 };/* class TheoryEngine */
 777
 778 }/* CVC4 namespace */
 779
 780 #endif /* CVC4__THEORY_ENGINE_H */