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