diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-01-31 23:44:24 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-31 23:44:24 -0800 |
commit | 7583e034bbd991877b634d50249bbccfd9e3c763 (patch) | |
tree | 9c4034b7eaa5a10663347f945dfb3362bcd913e9 /src/proof/theory_proof.h | |
parent | c099abeb9c3a45019b18daac19c4b4cd43b4c6f0 (diff) |
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.
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 32 |
1 files changed, 23 insertions, 9 deletions
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,16 +307,29 @@ 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. * * @param type |