summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/proof/arith_proof.cpp6
-rw-r--r--src/proof/arith_proof.h7
-rw-r--r--src/proof/array_proof.cpp6
-rw-r--r--src/proof/array_proof.h7
-rw-r--r--src/proof/bitvector_proof.cpp7
-rw-r--r--src/proof/bitvector_proof.h7
-rw-r--r--src/proof/theory_proof.cpp26
-rw-r--r--src/proof/theory_proof.h108
-rw-r--r--src/proof/uf_proof.cpp6
-rw-r--r--src/proof/uf_proof.h7
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback