src/theory/theory_engine.h

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