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