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

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index ba38a314c51d93ec1464dba3ecec1ca93abb6d50..9ee5f2143f1e1ff8a5b0955e9f271c7407d41935 100644 (file)
--- 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 c70754a1f18e5c154b95ae91ba6cb36c988af03e..ac96ad1f337d5e6afb54fef754bc6679e5f70f5f 100644 (file)
--- 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 ec2f85829ecc3cc94db93f9372d6b874e8f56225..75b7b7f1b15786a5cef75a8b662198af83d4f970 100644 (file)
--- 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 372ad1f67e4d0c1a4d37039f046496cef0f7c92d..55cda0aba061366cffc0eae68c19713efead4333 100644 (file)
--- 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 c60cc8274d64142ee889ad41ec9a5d240b367fbc..e75b94c8e097a1ec271a6173be101b63307d6d58 100644 (file)
--- 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 f0a0717fa145c78e5e85e7f78a229f1fe02977bf..8264d3bc401f7e2146c561d8a0000f9634f8d89d 100644 (file)
--- 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 eee75e6126fbf8b0413e160935c22d602882b7c0..b74d4a4d22967ff1b011a2735c6a65b819750c22 100644 (file)
--- 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 577f0c03226935bf17af65184fd914c9878f61eb..e8569d636aadde070fde31f33781c6a107ef760d 100644 (file)
--- 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 b88f7dc33680e31b51777500a792ce140b422b59..3c4c7d381b99d7a719495bc69a4a5a0fd798bbfe 100644 (file)
--- 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 ca8b3f90e5833d2051d7cd959d154a0d0d584c54..834f6ef9ea7c98fefc752e730f6cd069610a1a88 100644 (file)
--- 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,