Move first order model for full model check to own file (#5918)

[cvc5.git] / src / theory / theory.h

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 9519624b771603d54d187162b08afcf7a7a2596e..fa26ab65e9ccb9b7d49d570e6386d94b8002486f 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -140,12 +140,6 @@ class Theory {
   /** The care graph the theory will use during combination. */
   CareGraph* d_careGraph;
 
-  /**
-   * Pointer to the quantifiers engine (or NULL, if quantifiers are not
-   * supported or not enabled). Not owned by the theory.
-   */
-  QuantifiersEngine* d_quantEngine;
-
   /** Pointer to the decision manager. */
   DecisionManager* d_decManager;
 
@@ -234,9 +228,22 @@ class Theory {
    */
   TheoryInferenceManager* d_inferManager;
 
+  /**
+   * Pointer to the quantifiers engine (or NULL, if quantifiers are not
+   * supported or not enabled). Not owned by the theory.
+   */
+  QuantifiersEngine* d_quantEngine;
+
   /** Pointer to proof node manager */
   ProofNodeManager* d_pnm;
 
+  /**
+   * Are proofs enabled?
+   *
+   * They are considered enabled if the ProofNodeManager is non-null.
+   */
+  bool proofsEnabled() const;
+
   /**
    * Returns the next assertion in the assertFact() queue.
    *
@@ -248,6 +255,15 @@ class Theory {
     return d_logicInfo;
   }
 
+  /**
+   * Set separation logic heap. This is called when the location and data
+   * types for separation logic are determined. This should be called at
+   * most once, before solving.
+   *
+   * This currently should be overridden by the separation logic theory only.
+   */
+  virtual void declareSepHeap(TypeNode locT, TypeNode dataT) {}
+
   /**
    * The theory that owns the uninterpreted sort.
    */
@@ -712,15 +728,20 @@ class Theory {
                                   TrustSubstitutionMap& outSubstitutions);
 
   /**
-   * Given an atom of the theory coming from the input formula, this
-   * method can be overridden in a theory implementation to rewrite
-   * the atom into an equivalent form.  This is only called just
-   * before an input atom to the engine. This method returns a TrustNode of
-   * kind TrustNodeKind::REWRITE, which carries information about the proof
-   * generator for the rewrite. Similarly to expandDefinition, this method may
-   * return the null TrustNode if atom is unchanged.
+   * Given a term of the theory coming from the input formula or
+   * from a lemma generated during solving, this method can be overridden in a
+   * theory implementation to rewrite the term into an equivalent form.
+   *
+   * This method returns a TrustNode of kind TrustNodeKind::REWRITE, which
+   * carries information about the proof generator for the rewrite, which can
+   * be the null TrustNode if n is unchanged.
+   *
+   * Notice this method is used both in the "theory rewrite equalities"
+   * preprocessing pass, where n is an equality from the input formula,
+   * and in theory preprocessing, where n is a (non-equality) term occurring
+   * in the input or generated in a lemma.
    */
-  virtual TrustNode ppRewrite(TNode atom) { return TrustNode::null(); }
+  virtual TrustNode ppRewrite(TNode n) { return TrustNode::null(); }
 
   /**
    * Notify preprocessed assertions. Called on new assertions after