From 7583e034bbd991877b634d50249bbccfd9e3c763 Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Fri, 31 Jan 2020 23:44:24 -0800
Subject: Handle `expectedType` in TheoryProofEngine (#3691)

`TheoryProofEngine` now uses the `expectedType` optional argument.
  * When printing terms, it sets this for theories that it dispatches too
  * It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
  * It is mindful of `expectedType` when using the let map.

I also moved to hpp function implementations into the cpp.
---
 src/proof/theory_proof.h | 32 +++++++++++++++++++++++---------
 1 file changed, 23 insertions(+), 9 deletions(-)

(limited to 'src/proof/theory_proof.h')

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index e8569d636..85c8e5fee 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -198,14 +198,15 @@ public:
   void printTheoryTerm(Expr term,
                        std::ostream& os,
                        const ProofLetMap& map,
-                       TypeNode expectedType = TypeNode())
-  {
-    this->printTheoryTermAsType(term, os, map, expectedType);
-  }
+                       TypeNode expectedType = TypeNode());
   virtual void printTheoryTermAsType(Expr term,
                                      std::ostream& os,
                                      const ProofLetMap& map,
                                      TypeNode expectedType) = 0;
+  /**
+   * Calls `TheoryProof::equalityType` on the appropriate theory.
+   */
+  TypeNode equalityType(const Expr& left, const Expr& right);
 
   bool printsAsBool(const Node &n);
 };
@@ -227,7 +228,7 @@ public:
   void printCoreTerm(Expr term,
                      std::ostream& os,
                      const ProofLetMap& map,
-                     Type expectedType = Type());
+                     TypeNode expectedType = TypeNode());
   void printLetTerm(Expr term, std::ostream& os) override;
   void printBoundTermAsType(Expr term,
                             std::ostream& os,
@@ -306,15 +307,28 @@ protected:
   void printOwnedTerm(Expr term,
                       std::ostream& os,
                       const ProofLetMap& map,
-                      TypeNode expectedType = TypeNode())
-  {
-    this->printOwnedTermAsType(term, os, map, expectedType);
-  }
+                      TypeNode expectedType = TypeNode());
+
   virtual void printOwnedTermAsType(Expr term,
                                     std::ostream& os,
                                     const ProofLetMap& map,
                                     TypeNode expectedType) = 0;
 
+  /**
+   * Return the type (at the SMT level, the sort) of an equality or disequality
+   * between `left` and `right`.
+   *
+   * The default implementation asserts that the two have the same type, and
+   * returns it.
+   *
+   * A theory may want to do something else.
+   *
+   * For example, the theory of arithmetic allows equalities between Reals and
+   * Integers. In this case the integer is upcast to a real, and the equality
+   * is over reals.
+   */
+  virtual TypeNode equalityType(const Expr& left, const Expr& right);
+
   /**
    * Print the proof representation of the given type that belongs to some theory.
    *
-- 
cgit v1.2.3