From f10f495cbb3784cfed51779836f49f7a06b4f289 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 30 Dec 2019 20:13:48 -0800 Subject: [proof] ITE translation fix (#3484) * Bugfix: convert ifte arms to formulas for printing We have two kinds of ITEs in our LFSC proofs: * ite: for sort-typed expressions * ifte: for formulas Say that we have a Bool-sorted ITE. We had machinery for emitting an `ifte` for it, but this machinery didn't actually convert the arms of the ITE into formulas... Facepalm. Fixed now. * Test the lifting of ITEs from arithmetic. This test verifies that booleans ITEs are correctly lifted to formula ITEs in LRA proofs. It used to fail, but now passes. * clang-format * Typos. * Add test to CMake * Set --check-proofs in test * Address Yoni * Expand printsAsBool documentation * Assert ITE typing soundness * Assert a subtype relation for ITEs, not equality * Update src/proof/arith_proof.h Thanks Yoni! Co-Authored-By: yoni206 Co-authored-by: yoni206 --- src/proof/arith_proof.cpp | 7 +++++++ src/proof/arith_proof.h | 5 +++++ src/proof/theory_proof.cpp | 46 ++++++++++++++++++++++++++++++++++++++-------- src/proof/theory_proof.h | 14 +++++++++++++- 4 files changed, 63 insertions(+), 9 deletions(-) (limited to 'src/proof') diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 77f4b1630..ba38a314c 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -1193,4 +1193,11 @@ void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& p // Nothing to do here at this point. } +bool LFSCArithProof::printsAsBool(const Node& n) +{ + // Our boolean variables and constants print as sort Bool. + // All complex booleans print as formulas. + return n.getType().isBoolean() and (n.isVar() or n.isConst()); +} + } /* CVC4 namespace */ diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index a1df24fac..c70754a1f 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -167,6 +167,11 @@ public: void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap& globalLetMap) override; + + /** + * Return whether this node, when serialized to LFSC, has sort `Bool`. Otherwise, the sort is `formula`. + */ + bool printsAsBool(const Node& n) override; }; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index d95572820..eee75e612 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -872,6 +872,23 @@ void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const Pr printTheoryTerm(term, os, map); } +void LFSCTheoryProofEngine::printBoundFormula(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ + Assert(term.getType().isBoolean() or term.getType().isPredicate()); + bool wrapWithBoolToPred = term.getType().isBoolean() and printsAsBool(term); + if (wrapWithBoolToPred) + { + os << "(p_app "; + } + printBoundTerm(term, os, map); + if (wrapWithBoolToPred) + { + os << ")"; + } +} + void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map) { if (term.isVariable()) { os << ProofManager::sanitize(term); @@ -882,17 +899,30 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro switch(k) { case kind::ITE: { - os << (term.getType().isBoolean() ? "(ifte ": "(ite _ "); - - bool booleanCase = term[0].getType().isBoolean(); - if (booleanCase && printsAsBool(term[0])) os << "(p_app "; - printBoundTerm(term[0], os, map); - if (booleanCase && printsAsBool(term[0])) os << ")"; + bool useFormulaType = term.getType().isBoolean(); + Assert(term[1].getType().isSubtypeOf(term.getType())); + Assert(term[2].getType().isSubtypeOf(term.getType())); + os << (useFormulaType ? "(ifte " : "(ite _ "); + printBoundFormula(term[0], os, map); os << " "; - printBoundTerm(term[1], os, map); + if (useFormulaType) + { + printBoundFormula(term[1], os, map); + } + else + { + printBoundTerm(term[1], os, map); + } os << " "; - printBoundTerm(term[2], os, map); + if (useFormulaType) + { + printBoundFormula(term[2], os, map); + } + else + { + printBoundTerm(term[2], os, map); + } os << ")"; return; } diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index b487b62a8..577f0c032 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -197,6 +197,11 @@ public: private: static void dumpTheoryLemmas(const IdToSatClause& lemmas); + // Prints this boolean term as a formula. + // If necessary, it prints a wrapper converting a `Bool`-sorted term to a + // formula. + void printBoundFormula(Expr term, std::ostream& os, const ProofLetMap& map); + // TODO: this function should be moved into the BV prover. std::map d_assertionToRewrite; @@ -353,7 +358,14 @@ protected: */ virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2); - // Return true if node prints as bool, false if it prints as a formula. + /** + * Return whether this node, when serialized as an LFSC proof, has sort `Bool`. + * + * This is virtual because it ultimately, theories control the serialization + * of their proofs, so a theory will need to override this appropriately. + * + * This should only be called on nodes of type `Bool`. + */ virtual bool printsAsBool(const Node &n) { // Most nodes print as formulas, so this is the default. return false; -- cgit v1.2.3