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

10 files changed, 149 insertions, 38 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index ba38a314c..9ee5f2143 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -681,7 +681,11 @@ void ArithProof::registerTerm(Expr term) {
   }
 }
 
-void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
+void LFSCArithProof::printOwnedTermAsType(Expr term,
+                                          std::ostream& os,
+                                          const ProofLetMap& map,
+                                          TypeNode expectedType)
+{
   Debug("pf::arith") << "Arith print term: " << term << ". Kind: " << term.getKind()
                      << ". Type: " << term.getType()
                      << ". Number of children: " << term.getNumChildren() << std::endl;
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index c70754a1f..ac96ad1f3 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -82,9 +82,10 @@ public:
   LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine)
     : ArithProof(arith, proofEngine)
   {}
-  void printOwnedTerm(Expr term,
-                      std::ostream& os,
-                      const ProofLetMap& map) override;
+  void printOwnedTermAsType(Expr term,
+                            std::ostream& os,
+                            const ProofLetMap& map,
+                            TypeNode expectedType) override;
   void printOwnedSort(Type type, std::ostream& os) override;
 
   /**
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index ec2f85829..75b7b7f1b 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -1123,7 +1123,11 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) {
   return d_skolemToLiteral[skolem];
 }
 
-void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
+void LFSCArrayProof::printOwnedTermAsType(Expr term,
+                                          std::ostream& os,
+                                          const ProofLetMap& map,
+                                          TypeNode expectedType)
+{
   Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS);
 
   if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAYS) {
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 372ad1f67..55cda0aba 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -95,9 +95,10 @@ public:
     : ArrayProof(arrays, proofEngine)
   {}
 
-  void printOwnedTerm(Expr term,
-                      std::ostream& os,
-                      const ProofLetMap& map) override;
+  void printOwnedTermAsType(Expr term,
+                            std::ostream& os,
+                            const ProofLetMap& map,
+                            TypeNode expectedType) override;
   void printOwnedSort(Type type, std::ostream& os) override;
   void printTheoryLemmaProof(std::vector<Expr>& lemma,
                              std::ostream& os,
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index c60cc8274..e75b94c8e 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -121,9 +121,10 @@ std::string BitVectorProof::getBBTermName(Expr expr)
   return os.str();
 }
 
-void BitVectorProof::printOwnedTerm(Expr term,
-                                    std::ostream& os,
-                                    const ProofLetMap& map)
+void BitVectorProof::printOwnedTermAsType(Expr term,
+                                          std::ostream& os,
+                                          const ProofLetMap& map,
+                                          TypeNode expectedType)
 {
   Debug("pf::bv") << std::endl
                   << "(pf::bv) BitVectorProof::printOwnedTerm( " << term
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index f0a0717fa..8264d3bc4 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -135,9 +135,10 @@ class BitVectorProof : public TheoryProof
   theory::TheoryId getTheoryId() override;
 
  public:
-  void printOwnedTerm(Expr term,
-                      std::ostream& os,
-                      const ProofLetMap& map) override;
+  void printOwnedTermAsType(Expr term,
+                            std::ostream& os,
+                            const ProofLetMap& map,
+                            TypeNode expectedType) override;
 
   void printOwnedSort(Type type, std::ostream& os) override;
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index eee75e612..b74d4a4d2 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -283,7 +283,11 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
   os << paren.str();
 }
 
-void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
+void LFSCTheoryProofEngine::printTheoryTermAsType(Expr term,
+                                                  std::ostream& os,
+                                                  const ProofLetMap& map,
+                                                  TypeNode expectedType)
+{
   theory::TheoryId theory_id = theory::Theory::theoryOf(term);
 
   // boolean terms and ITEs are special because they
@@ -855,7 +859,11 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
   }
 }
 
-void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
+void LFSCTheoryProofEngine::printBoundTermAsType(Expr term,
+                                                 std::ostream& os,
+                                                 const ProofLetMap& map,
+                                                 TypeNode expectedType)
+{
   Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
 
   ProofLetMap::const_iterator it = map.find(term);
@@ -889,7 +897,11 @@ void LFSCTheoryProofEngine::printBoundFormula(Expr term,
   }
 }
 
-void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
+void LFSCTheoryProofEngine::printCoreTerm(Expr term,
+                                          std::ostream& os,
+                                          const ProofLetMap& map,
+                                          Type expectedType)
+{
   if (term.isVariable()) {
     os << ProofManager::sanitize(term);
     return;
@@ -1034,7 +1046,6 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
 
   default: Unhandled() << k;
   }
-
 }
 
 void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
@@ -1181,7 +1192,11 @@ void LFSCBooleanProof::printConstantDisequalityProof(std::ostream& os, Expr c1,
     os << "(negsymm _ _ _ t_t_neq_f)";
 }
 
-void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
+void LFSCBooleanProof::printOwnedTermAsType(Expr term,
+                                            std::ostream& os,
+                                            const ProofLetMap& map,
+                                            TypeNode expectedType)
+{
   Assert(term.getType().isBoolean());
   if (term.isVariable()) {
     os << ProofManager::sanitize(term);
@@ -1259,7 +1274,6 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
 
   default: Unhandled() << k;
   }
-
 }
 
 void LFSCBooleanProof::printOwnedSort(Type type, std::ostream& os) {
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,
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index b88f7dc33..3c4c7d381 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -623,7 +623,11 @@ void UFProof::registerTerm(Expr term) {
   }
 }
 
-void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
+void LFSCUFProof::printOwnedTermAsType(Expr term,
+                                       std::ostream& os,
+                                       const ProofLetMap& map,
+                                       TypeNode expectedType)
+{
   Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl;
 
   Assert(theory::Theory::theoryOf(term) == theory::THEORY_UF);
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index ca8b3f90e..834f6ef9e 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -75,9 +75,10 @@ public:
   LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine)
     : UFProof(uf, proofEngine)
   {}
-  void printOwnedTerm(Expr term,
-                      std::ostream& os,
-                      const ProofLetMap& map) override;
+  void printOwnedTermAsType(Expr term,
+                            std::ostream& os,
+                            const ProofLetMap& map,
+                            TypeNode expectedType) override;
   void printOwnedSort(Type type, std::ostream& os) override;
   void printTheoryLemmaProof(std::vector<Expr>& lemma,
                              std::ostream& os,