diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-01-29 16:07:09 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-29 16:07:09 -0800 |
| commit | 7849f09ece473f9822f91572115e50af7eae9564 (patch) | |
| tree | 5282b3bc4cb2ab247189edfc0a5df63558cea852 /src/proof/uf_proof.h | |
| parent | f4a10a74ee45018836aa7d7c07910f294c32b2cc (diff) | |
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
Diffstat (limited to 'src/proof/uf_proof.h')
| -rw-r--r-- | src/proof/uf_proof.h | 7 |
1 files changed, 4 insertions, 3 deletions
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, |