diff options
| -rw-r--r-- | src/proof/arith_proof.cpp | 7 | ||||
| -rw-r--r-- | src/proof/arith_proof.h | 5 | ||||
| -rw-r--r-- | src/proof/theory_proof.cpp | 46 | ||||
| -rw-r--r-- | src/proof/theory_proof.h | 14 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/ite-lift.smt2 | 15 |
6 files changed, 79 insertions, 9 deletions
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<Node, std::string> 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; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c85065ef9..e27cff94d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -28,6 +28,7 @@ set(regress_0_tests regress0/arith/issue1399.smt2 regress0/arith/issue3412.smt2 regress0/arith/issue3413.smt2 + regress0/arith/ite-lift.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc regress0/arith/miplib2.cvc diff --git a/test/regress/regress0/arith/ite-lift.smt2 b/test/regress/regress0/arith/ite-lift.smt2 new file mode 100644 index 000000000..bd2df3def --- /dev/null +++ b/test/regress/regress0/arith/ite-lift.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --check-proofs +(set-option :incremental false) +(set-info :status unsat) +(set-info :category "crafted") +(set-info :difficulty "0") +(set-logic QF_LRA) + +(declare-fun x_0 () Real) +(declare-fun x_1 () Real) +(declare-fun b_f () Bool) +(assert (<= x_0 0)) +(assert (<= x_1 0)) +(assert (not b_f)) +(assert (ite b_f b_f (>= (+ x_0 x_1) 1))) +(check-sat) |