diff options
author | Guy <katz911@gmail.com> | 2016-07-25 17:20:14 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-25 17:20:14 -0700 |
commit | d1cdf6f1719c3d56590ef6305f70f376f4d80b57 (patch) | |
tree | a9316bf4e3275248f65c2a9037f7d8e92f84d2ca /src/proof/theory_proof.h | |
parent | df8c922b3d212bc5fadcd5cd26ebe868a9fe0f47 (diff) |
Propagate the usage of proof let maps into constant disequality proofs
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 968d46e68..c622fabee 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -149,7 +149,7 @@ public: void markTermForFutureRegistration(Expr term, theory::TheoryId id); - void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); virtual void treatBoolsAsFormulas(bool value) {}; @@ -286,7 +286,7 @@ public: * * @param term */ - virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); /** * Print a proof for the equivalence of n1 and n2. * |