Merge branch 'master' into macos11macos11

1 files changed, 290 insertions, 274 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e610adcf7..5c44f8968 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -78,11 +78,13 @@ struct NodeTheoryPairHashFunction {
 
 /* Forward declarations */
 namespace theory {
-class TheoryModel;
+
 class CombinationEngine;
-class SharedSolver;
 class DecisionManager;
 class RelevanceManager;
+class Rewriter;
+class SharedSolver;
+class TheoryModel;
 
 }  // namespace theory
 
@@ -96,203 +98,14 @@ class PropEngine;
  * T-solvers look like a single unit to the propositional part of
  * cvc5.
  */
-class TheoryEngine {
-
+class TheoryEngine
+{
   /** Shared terms database can use the internals notify the theories */
   friend class SharedTermsDatabase;
   friend class theory::EngineOutputChannel;
   friend class theory::CombinationEngine;
   friend class theory::SharedSolver;
 
-  /** Associated PropEngine engine */
-  prop::PropEngine* d_propEngine;
-
-  /**
-   * Reference to the environment.
-   */
-  Env& d_env;
-
-  /**
-   * A table of from theory IDs to theory pointers. Never use this table
-   * directly, use theoryOf() instead.
-   */
-  theory::Theory* d_theoryTable[theory::THEORY_LAST];
-
-  /**
-   * A collection of theories that are "active" for the current run.
-   * This set is provided by the user (as a logic string, say, in SMT-LIBv2
-   * format input), or else by default it's all-inclusive.  This is important
-   * because we can optimize for single-theory runs (no sharing), can reduce
-   * the cost of walking the DAG on registration, etc.
-   */
-  const LogicInfo& d_logicInfo;
-
-  /** The separation logic location and data types */
-  TypeNode d_sepLocType;
-  TypeNode d_sepDataType;
-
-  //--------------------------------- new proofs
-  /** Proof node manager used by this theory engine, if proofs are enabled */
-  ProofNodeManager* d_pnm;
-  /** The lazy proof object
-   *
-   * This stores instructions for how to construct proofs for all theory lemmas.
-   */
-  std::shared_ptr<LazyCDProof> d_lazyProof;
-  /** The proof generator */
-  std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
-  //--------------------------------- end new proofs
-  /** The combination manager we are using */
-  std::unique_ptr<theory::CombinationEngine> d_tc;
-  /** The shared solver of the above combination engine. */
-  theory::SharedSolver* d_sharedSolver;
-  /** The quantifiers engine, which is owned by the quantifiers theory */
-  theory::QuantifiersEngine* d_quantEngine;
-  /**
-   * The decision manager
-   */
-  std::unique_ptr<theory::DecisionManager> d_decManager;
-  /** The relevance manager */
-  std::unique_ptr<theory::RelevanceManager> d_relManager;
-  /**
-   * An empty set of relevant assertions, which is returned as a dummy value for
-   * getRelevantAssertions when relevance is disabled.
-   */
-  std::unordered_set<TNode> d_emptyRelevantSet;
-
-  /** are we in eager model building mode? (see setEagerModelBuilding). */
-  bool d_eager_model_building;
-
-  /**
-   * Output channels for individual theories.
-   */
-  theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
-
-  /**
-   * Are we in conflict.
-   */
-  context::CDO<bool> d_inConflict;
-
-  /**
-   * Are we in "SAT mode"? In this state, the user can query for the model.
-   * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB
-   * standard, version 2.6.
-   */
-  bool d_inSatMode;
-
-  /**
-   * Called by the theories to notify of a conflict.
-   *
-   * @param conflict The trust node containing the conflict and its proof
-   * generator (if it exists),
-   * @param theoryId The theory that sent the conflict
-   */
-  void conflict(TrustNode conflict, theory::TheoryId theoryId);
-
-  /** set in conflict */
-  void markInConflict();
-
-  /**
-   * Debugging flag to ensure that shutdown() is called before the
-   * destructor.
-   */
-  bool d_hasShutDown;
-
-  /**
-   * True if a theory has notified us of incompleteness (at this
-   * context level or below).
-   */
-  context::CDO<bool> d_incomplete;
-  /** The theory and identifier that (most recently) set incomplete */
-  context::CDO<theory::TheoryId> d_incompleteTheory;
-  context::CDO<theory::IncompleteId> d_incompleteId;
-
-  /**
-   * Called by the theories to notify that the current branch is incomplete.
-   */
-  void setIncomplete(theory::TheoryId theory, theory::IncompleteId id);
-
-  /**
-   * Mapping of propagations from recievers to senders.
-   */
-  typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap;
-  PropagationMap d_propagationMap;
-
-  /**
-   * Timestamp of propagations
-   */
-  context::CDO<size_t> d_propagationMapTimestamp;
-
-  /**
-   * Literals that are propagated by the theory. Note that these are TNodes.
-   * The theory can only propagate nodes that have an assigned literal in the
-   * SAT solver and are hence referenced in the SAT solver.
-   */
-  context::CDList<TNode> d_propagatedLiterals;
-
-  /**
-   * The index of the next literal to be propagated by a theory.
-   */
-  context::CDO<unsigned> d_propagatedLiteralsIndex;
-
-  /**
-   * Called by the output channel to propagate literals and facts
-   * @return false if immediate conflict
-   */
-  bool propagate(TNode literal, theory::TheoryId theory);
-
-  /**
-   * Internal method to call the propagation routines and collect the
-   * propagated literals.
-   */
-  void propagate(theory::Theory::Effort effort);
-
-  /**
-   * A variable to mark if we added any lemmas.
-   */
-  bool d_lemmasAdded;
-
-  /**
-   * A variable to mark if the OutputChannel was "used" by any theory
-   * since the start of the last check.  If it has been, we require
-   * a FULL_EFFORT check before exiting and reporting SAT.
-   *
-   * See the documentation for the needCheck() function, below.
-   */
-  bool d_outputChannelUsed;
-
-  /** Atom requests from lemmas */
-  AtomRequests d_atomRequests;
-
-  /**
-   * Adds a new lemma, returning its status.
-   * @param node the lemma
-   * @param p the properties of the lemma.
-   * @param atomsTo the theory that atoms of the lemma should be sent to
-   * @param from the theory that sent the lemma
-   */
-  void lemma(TrustNode node,
-             theory::LemmaProperty p,
-             theory::TheoryId from = theory::THEORY_LAST);
-
-  /** Ensure atoms from the given node are sent to the given theory */
-  void ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo);
-  /** Ensure that the given atoms are sent to the given theory */
-  void ensureLemmaAtoms(const std::vector<TNode>& atoms,
-                        theory::TheoryId atomsTo);
-
-  /** sort inference module */
-  std::unique_ptr<theory::SortInference> d_sortInfer;
-
-  /** Time spent in theory combination */
-  TimerStat d_combineTheoriesTime;
-
-  Node d_true;
-  Node d_false;
-
-  /** Whether we were just interrupted (or not) */
-  bool d_interrupted;
-
  public:
   /** Constructs a theory engine */
   TheoryEngine(Env& env);
@@ -310,13 +123,13 @@ class TheoryEngine {
    * there is another theory it will be deleted.
    */
   template <class TheoryClass>
-  inline void addTheory(theory::TheoryId theoryId)
+  void addTheory(theory::TheoryId theoryId)
   {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
     d_theoryTable[theoryId] =
         new TheoryClass(d_env, *d_theoryOut[theoryId], theory::Valuation(this));
-    theory::Rewriter::registerTheoryRewriter(
+    getRewriter()->registerTheoryRewriter(
         theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
   }
 
@@ -340,9 +153,7 @@ class TheoryEngine {
   /**
    * Get a pointer to the underlying propositional engine.
    */
-  inline prop::PropEngine* getPropEngine() const {
-    return d_propEngine;
-  }
+  prop::PropEngine* getPropEngine() const { return d_propEngine; }
 
   /** Get the proof node manager */
   ProofNodeManager* getProofNodeManager() const;
@@ -360,7 +171,8 @@ class TheoryEngine {
   /**
    * Get a pointer to the underlying quantifiers engine.
    */
-  theory::QuantifiersEngine* getQuantifiersEngine() const {
+  theory::QuantifiersEngine* getQuantifiersEngine() const
+  {
     return d_quantEngine;
   }
   /**
@@ -371,60 +183,6 @@ class TheoryEngine {
     return d_decManager.get();
   }
 
- private:
-  /**
-   * Queue of nodes for pre-registration.
-   */
-  std::queue<TNode> d_preregisterQueue;
-
-  /**
-   * Boolean flag denoting we are in pre-registration.
-   */
-  bool d_inPreregister;
-
-  /**
-   * Did the theories get any new facts since the last time we called
-   * check()
-   */
-  context::CDO<bool> d_factsAsserted;
-
-  /**
-   * Assert the formula to the given theory.
-   * @param assertion the assertion to send (not necesserily normalized)
-   * @param original the assertion as it was sent in from the propagating theory
-   * @param toTheoryId the theory to assert to
-   * @param fromTheoryId the theory that sent it
-   */
-  void assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
-
-  /**
-   * Marks a theory propagation from a theory to a theory where a
-   * theory could be the THEORY_SAT_SOLVER for literals coming from
-   * or being propagated to the SAT solver. If the receiving theory
-   * already recieved the literal, the method returns false, otherwise
-   * it returns true.
-   *
-   * @param assertion the normalized assertion being sent
-   * @param originalAssertion the actual assertion that was sent
-   * @param toTheoryId the theory that is on the receiving end
-   * @param fromTheoryId the theory that sent the assertion
-   * @return true if a new assertion, false if theory already got it
-   */
-  bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
-
-  /**
-   * Computes the explanation by traversing the propagation graph and
-   * asking relevant theories to explain the propagations. Initially
-   * the explanation vector should contain only the element (node, theory)
-   * where the node is the one to be explained, and the theory is the
-   * theory that sent the literal.
-   */
-  TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector);
-
-  /** Are proofs enabled? */
-  bool isProofEnabled() const;
-
- public:
   /**
    * Preprocess rewrite equality, called by the preprocessor to rewrite
    * equalities appearing in the input.
@@ -434,7 +192,7 @@ class TheoryEngine {
   void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
 
   /** Return whether or not we are incomplete (in the current context). */
-  inline bool isIncomplete() const { return d_incomplete; }
+  bool isIncomplete() const { return d_incomplete; }
 
   /**
    * Returns true if we need another round of checking.  If this
@@ -451,9 +209,7 @@ class TheoryEngine {
    * as it might decide to further instantiate some lemmas, precluding
    * a SAT response.
    */
-  inline bool needCheck() const {
-    return d_outputChannelUsed || d_lemmasAdded;
-  }
+  bool needCheck() const { return d_outputChannelUsed || d_lemmasAdded; }
   /**
    * Is the literal lit (possibly) critical for satisfying the input formula in
    * the current context? This call is applicable only during collectModelInfo
@@ -505,7 +261,7 @@ class TheoryEngine {
    */
   bool presolve();
 
-   /**
+  /**
    * Calls postsolve() on all theories.
    */
   void postsolve();
@@ -515,9 +271,14 @@ class TheoryEngine {
    */
   void notifyRestart();
 
-  void getPropagatedLiterals(std::vector<TNode>& literals) {
-    for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) {
-      Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl;
+  void getPropagatedLiterals(std::vector<TNode>& literals)
+  {
+    for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size();
+         d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1)
+    {
+      Debug("getPropagatedLiterals")
+          << "TheoryEngine::getPropagatedLiterals: propagating: "
+          << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl;
       literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]);
     }
   }
@@ -569,7 +330,8 @@ class TheoryEngine {
    * @returns the theory, or NULL if the TNode is
    * of built-in type.
    */
-  inline theory::Theory* theoryOf(TNode node) const {
+  theory::Theory* theoryOf(TNode node) const
+  {
     return d_theoryTable[theory::Theory::theoryOf(node)];
   }
 
@@ -578,12 +340,14 @@ class TheoryEngine {
    *
    * @returns the theory
    */
-  inline theory::Theory* theoryOf(theory::TheoryId theoryId) const {
+  theory::Theory* theoryOf(theory::TheoryId theoryId) const
+  {
     Assert(theoryId < theory::THEORY_LAST);
     return d_theoryTable[theoryId];
   }
 
-  inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
+  bool isTheoryEnabled(theory::TheoryId theoryId) const
+  {
     return d_logicInfo.isTheoryEnabled(theoryId);
   }
   /** get the logic info used by this theory engine */
@@ -648,26 +412,278 @@ class TheoryEngine {
    */
   bool isFiniteType(TypeNode tn) const;
   //---------------------- end information about cardinality of types
+
+  theory::SortInference* getSortInference() { return d_sortInfer.get(); }
+
+  /** Prints the assertions to the debug stream */
+  void printAssertions(const char* tag);
+
+  /**
+   * Check that the theory assertions are satisfied in the model.
+   * This function is called from the smt engine's checkModel routine.
+   */
+  void checkTheoryAssertionsWithModel(bool hardFailure);
+
  private:
+  typedef context::
+      CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction>
+          PropagationMap;
+
+  /**
+   * Called by the theories to notify of a conflict.
+   *
+   * @param conflict The trust node containing the conflict and its proof
+   * generator (if it exists),
+   * @param theoryId The theory that sent the conflict
+   */
+  void conflict(TrustNode conflict, theory::TheoryId theoryId);
+
+  /** set in conflict */
+  void markInConflict();
+
+  /**
+   * Called by the theories to notify that the current branch is incomplete.
+   */
+  void setIncomplete(theory::TheoryId theory, theory::IncompleteId id);
+
+  /**
+   * Called by the output channel to propagate literals and facts
+   * @return false if immediate conflict
+   */
+  bool propagate(TNode literal, theory::TheoryId theory);
+
+  /**
+   * Internal method to call the propagation routines and collect the
+   * propagated literals.
+   */
+  void propagate(theory::Theory::Effort effort);
+
+  /**
+   * Assert the formula to the given theory.
+   * @param assertion the assertion to send (not necesserily normalized)
+   * @param original the assertion as it was sent in from the propagating theory
+   * @param toTheoryId the theory to assert to
+   * @param fromTheoryId the theory that sent it
+   */
+  void assertToTheory(TNode assertion,
+                      TNode originalAssertion,
+                      theory::TheoryId toTheoryId,
+                      theory::TheoryId fromTheoryId);
+
+  /**
+   * Marks a theory propagation from a theory to a theory where a
+   * theory could be the THEORY_SAT_SOLVER for literals coming from
+   * or being propagated to the SAT solver. If the receiving theory
+   * already recieved the literal, the method returns false, otherwise
+   * it returns true.
+   *
+   * @param assertion the normalized assertion being sent
+   * @param originalAssertion the actual assertion that was sent
+   * @param toTheoryId the theory that is on the receiving end
+   * @param fromTheoryId the theory that sent the assertion
+   * @return true if a new assertion, false if theory already got it
+   */
+  bool markPropagation(TNode assertion,
+                       TNode originalAssertions,
+                       theory::TheoryId toTheoryId,
+                       theory::TheoryId fromTheoryId);
+
+  /**
+   * Computes the explanation by traversing the propagation graph and
+   * asking relevant theories to explain the propagations. Initially
+   * the explanation vector should contain only the element (node, theory)
+   * where the node is the one to be explained, and the theory is the
+   * theory that sent the literal.
+   */
+  TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector);
+
+  /** Are proofs enabled? */
+  bool isProofEnabled() const;
+
+  /**
+   * Get a pointer to the rewriter owned by the associated Env.
+   */
+  theory::Rewriter* getRewriter();
+
+  /**
+   * Adds a new lemma, returning its status.
+   * @param node the lemma
+   * @param p the properties of the lemma.
+   * @param atomsTo the theory that atoms of the lemma should be sent to
+   * @param from the theory that sent the lemma
+   */
+  void lemma(TrustNode node,
+             theory::LemmaProperty p,
+             theory::TheoryId from = theory::THEORY_LAST);
+
+  /** Ensure atoms from the given node are sent to the given theory */
+  void ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo);
+  /** Ensure that the given atoms are sent to the given theory */
+  void ensureLemmaAtoms(const std::vector<TNode>& atoms,
+                        theory::TheoryId atomsTo);
 
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
 
-  /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
-public:
- theory::SortInference* getSortInference() { return d_sortInfer.get(); }
+  /** Associated PropEngine engine */
+  prop::PropEngine* d_propEngine;
 
- /** Prints the assertions to the debug stream */
- void printAssertions(const char* tag);
+  /**
+   * Reference to the environment.
+   */
+  Env& d_env;
 
- public:
+  /**
+   * A table of from theory IDs to theory pointers. Never use this table
+   * directly, use theoryOf() instead.
+   */
+  theory::Theory* d_theoryTable[theory::THEORY_LAST];
 
   /**
-   * Check that the theory assertions are satisfied in the model.
-   * This function is called from the smt engine's checkModel routine.
+   * A collection of theories that are "active" for the current run.
+   * This set is provided by the user (as a logic string, say, in SMT-LIBv2
+   * format input), or else by default it's all-inclusive.  This is important
+   * because we can optimize for single-theory runs (no sharing), can reduce
+   * the cost of walking the DAG on registration, etc.
    */
-  void checkTheoryAssertionsWithModel(bool hardFailure);
-};/* class TheoryEngine */
+  const LogicInfo& d_logicInfo;
+
+  /** The separation logic location and data types */
+  TypeNode d_sepLocType;
+  TypeNode d_sepDataType;
+
+  //--------------------------------- new proofs
+  /** Proof node manager used by this theory engine, if proofs are enabled */
+  ProofNodeManager* d_pnm;
+  /** The lazy proof object
+   *
+   * This stores instructions for how to construct proofs for all theory lemmas.
+   */
+  std::shared_ptr<LazyCDProof> d_lazyProof;
+  /** The proof generator */
+  std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
+  //--------------------------------- end new proofs
+  /** The combination manager we are using */
+  std::unique_ptr<theory::CombinationEngine> d_tc;
+  /** The shared solver of the above combination engine. */
+  theory::SharedSolver* d_sharedSolver;
+  /** The quantifiers engine, which is owned by the quantifiers theory */
+  theory::QuantifiersEngine* d_quantEngine;
+  /**
+   * The decision manager
+   */
+  std::unique_ptr<theory::DecisionManager> d_decManager;
+  /** The relevance manager */
+  std::unique_ptr<theory::RelevanceManager> d_relManager;
+  /**
+   * An empty set of relevant assertions, which is returned as a dummy value for
+   * getRelevantAssertions when relevance is disabled.
+   */
+  std::unordered_set<TNode> d_emptyRelevantSet;
+
+  /** are we in eager model building mode? (see setEagerModelBuilding). */
+  bool d_eager_model_building;
+
+  /**
+   * Output channels for individual theories.
+   */
+  theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST];
+
+  /**
+   * Are we in conflict.
+   */
+  context::CDO<bool> d_inConflict;
+
+  /**
+   * Are we in "SAT mode"? In this state, the user can query for the model.
+   * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB
+   * standard, version 2.6.
+   */
+  bool d_inSatMode;
+
+  /**
+   * Debugging flag to ensure that shutdown() is called before the
+   * destructor.
+   */
+  bool d_hasShutDown;
+
+  /**
+   * True if a theory has notified us of incompleteness (at this
+   * context level or below).
+   */
+  context::CDO<bool> d_incomplete;
+  /** The theory and identifier that (most recently) set incomplete */
+  context::CDO<theory::TheoryId> d_incompleteTheory;
+  context::CDO<theory::IncompleteId> d_incompleteId;
+
+  /**
+   * Mapping of propagations from recievers to senders.
+   */
+  PropagationMap d_propagationMap;
+
+  /**
+   * Timestamp of propagations
+   */
+  context::CDO<size_t> d_propagationMapTimestamp;
+
+  /**
+   * Literals that are propagated by the theory. Note that these are TNodes.
+   * The theory can only propagate nodes that have an assigned literal in the
+   * SAT solver and are hence referenced in the SAT solver.
+   */
+  context::CDList<TNode> d_propagatedLiterals;
+
+  /**
+   * The index of the next literal to be propagated by a theory.
+   */
+  context::CDO<unsigned> d_propagatedLiteralsIndex;
+
+  /**
+   * A variable to mark if we added any lemmas.
+   */
+  bool d_lemmasAdded;
+
+  /**
+   * A variable to mark if the OutputChannel was "used" by any theory
+   * since the start of the last check.  If it has been, we require
+   * a FULL_EFFORT check before exiting and reporting SAT.
+   *
+   * See the documentation for the needCheck() function, below.
+   */
+  bool d_outputChannelUsed;
+
+  /** Atom requests from lemmas */
+  AtomRequests d_atomRequests;
+
+  /** sort inference module */
+  std::unique_ptr<theory::SortInference> d_sortInfer;
+
+  /** Time spent in theory combination */
+  TimerStat d_combineTheoriesTime;
+
+  Node d_true;
+  Node d_false;
+
+  /** Whether we were just interrupted (or not) */
+  bool d_interrupted;
+
+  /**
+   * Queue of nodes for pre-registration.
+   */
+  std::queue<TNode> d_preregisterQueue;
+
+  /**
+   * Boolean flag denoting we are in pre-registration.
+   */
+  bool d_inPreregister;
+
+  /**
+   * Did the theories get any new facts since the last time we called
+   * check()
+   */
+  context::CDO<bool> d_factsAsserted;
+
+}; /* class TheoryEngine */
 
 }  // namespace cvc5