expectedType in proof-printing code (#3665)

* expectedType in proof-printing code

To print lemma proofs in theories that use multiple sorts that have a
subtype relationship, we need to increase communication between the
TheoryProofEngine and the theory proofs themselves.

This commit add an (optional) argument `expectedType` to many
term-printing functions in TheoryProofEngine and TheoryProof.

Right now it is unused, so always takes on the default value of "null"
(meaning no type expectation), but in the future the TheoryProofEngine
will use it to signal TheoryProof about what type is expected to be
printed.

* TypeNode, Don't mix default args & virtual

* Use TypeNode instead of Type (The former are lighter)
* Don't add default arguments to virtual functions, because these cannot
  be dynamically overriden during a dynamic dispatch.
  * Since we don't want them to be overidable anyway, we use two
    functions: one that is non-virtual and has a default, the other that
    is virtual but has no default. The former just calls the latter.

* clang-format after signature changes

1 files changed, 94 insertions, 14 deletions

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 577f0c032..e8569d636 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -25,6 +25,7 @@
 #include <unordered_set>
 
 #include "expr/expr.h"
+#include "expr/type_node.h"
 #include "proof/clause_id.h"
 #include "proof/proof_utils.h"
 #include "prop/sat_solver_types.h"
@@ -69,8 +70,34 @@ public:
    * @param os
    */
   virtual void printLetTerm(Expr term, std::ostream& os) = 0;
-  virtual void printBoundTerm(Expr term, std::ostream& os,
-                              const ProofLetMap& map) = 0;
+
+  /**
+   * Print a term in some (core or non-core) theory
+   *
+   * @param term expression representing term
+   * @param os output stream
+   * @param expectedType The type that this is expected to have in a parent
+   * node. Null if there are no such requirements. This is useful for requesting
+   * type conversions from the theory. e.g. in (5.5 == 4) the right-hand-side
+   * should be converted to a real.
+   *
+   * The first version of this function has a default value for expectedType
+   * (null) The second version is virtual.
+   *
+   * They are split to avoid mixing virtual function and default argument
+   * values, which behave weirdly when combined.
+   */
+  void printBoundTerm(Expr term,
+                      std::ostream& os,
+                      const ProofLetMap& map,
+                      TypeNode expectedType = TypeNode())
+  {
+    this->printBoundTermAsType(term, os, map, expectedType);
+  }
+  virtual void printBoundTermAsType(Expr term,
+                                    std::ostream& os,
+                                    const ProofLetMap& map,
+                                    TypeNode expectedType) = 0;
 
   /**
    * Print the proof representation of the given sort.
@@ -152,7 +179,33 @@ public:
 
   void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
 
-  virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
+  /**
+   * Print a term in some non-core theory
+   *
+   * @param term expression representing term
+   * @param os output stream
+   * @param expectedType The type that this is expected to have in a parent
+   * node. Null if there are no such requirements. This is useful for requesting
+   * type conversions from the theory. e.g. in (5.5 == 4) the right-hand-side
+   * should be converted to a real.
+   *
+   * The first version of this function has a default value for expectedType
+   * (null) The second version is virtual.
+   *
+   * They are split to avoid mixing virtual function and default argument
+   * values, which behave weirdly when combined.
+   */
+  void printTheoryTerm(Expr term,
+                       std::ostream& os,
+                       const ProofLetMap& map,
+                       TypeNode expectedType = TypeNode())
+  {
+    this->printTheoryTermAsType(term, os, map, expectedType);
+  }
+  virtual void printTheoryTermAsType(Expr term,
+                                     std::ostream& os,
+                                     const ProofLetMap& map,
+                                     TypeNode expectedType) = 0;
 
   bool printsAsBool(const Node &n);
 };
@@ -163,18 +216,23 @@ public:
   LFSCTheoryProofEngine()
     : TheoryProofEngine() {}
 
-  void printTheoryTerm(Expr term,
-                       std::ostream& os,
-                       const ProofLetMap& map) override;
+  void printTheoryTermAsType(Expr term,
+                             std::ostream& os,
+                             const ProofLetMap& map,
+                             TypeNode expectedType) override;
 
   void registerTermsFromAssertions() override;
   void printSortDeclarations(std::ostream& os, std::ostream& paren);
   void printTermDeclarations(std::ostream& os, std::ostream& paren);
-  void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map);
+  void printCoreTerm(Expr term,
+                     std::ostream& os,
+                     const ProofLetMap& map,
+                     Type expectedType = Type());
   void printLetTerm(Expr term, std::ostream& os) override;
-  void printBoundTerm(Expr term,
-                      std::ostream& os,
-                      const ProofLetMap& map) override;
+  void printBoundTermAsType(Expr term,
+                            std::ostream& os,
+                            const ProofLetMap& map,
+                            TypeNode expectedType) override;
   void printAssertions(std::ostream& os, std::ostream& paren) override;
   void printLemmaRewrites(NodePairSet& rewrites,
                           std::ostream& os,
@@ -234,8 +292,29 @@ protected:
    *
    * @param term expression representing term
    * @param os output stream
+   * @param expectedType The type that this is expected to have in a parent
+   * node. Null if there are no such requirements. This is useful for requesting
+   * type conversions from the theory. e.g. in (5.5 == 4) the right-hand-side
+   * should be converted to a real.
+   *
+   * The first version of this function has a default value for expectedType
+   * (null) The second version is virtual.
+   *
+   * They are split to avoid mixing virtual function and default argument
+   * values, which behave weirdly when combined.
    */
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
+  void printOwnedTerm(Expr term,
+                      std::ostream& os,
+                      const ProofLetMap& map,
+                      TypeNode expectedType = TypeNode())
+  {
+    this->printOwnedTermAsType(term, os, map, expectedType);
+  }
+  virtual void printOwnedTermAsType(Expr term,
+                                    std::ostream& os,
+                                    const ProofLetMap& map,
+                                    TypeNode expectedType) = 0;
+
   /**
    * Print the proof representation of the given type that belongs to some theory.
    *
@@ -388,9 +467,10 @@ public:
   LFSCBooleanProof(TheoryProofEngine* proofEngine)
     : BooleanProof(proofEngine)
   {}
-  void printOwnedTerm(Expr term,
-                      std::ostream& os,
-                      const ProofLetMap& map) override;
+  void printOwnedTermAsType(Expr term,
+                            std::ostream& os,
+                            const ProofLetMap& map,
+                            TypeNode ty) override;
   void printOwnedSort(Type type, std::ostream& os) override;
   void printTheoryLemmaProof(std::vector<Expr>& lemma,
                              std::ostream& os,