From 2f287a59e9c775d9087cddd8c72be5169c2706e1 Mon Sep 17 00:00:00 2001 From: guykatzz Date: Thu, 9 Mar 2017 12:13:12 -0800 Subject: [PATCH] better proof support for bools and formulas --- proofs/signatures/smt.plf | 34 ++++++----- src/proof/array_proof.cpp | 18 +++++- src/proof/array_proof.h | 2 + src/proof/cnf_proof.cpp | 3 +- src/proof/proof_manager.cpp | 3 + src/proof/theory_proof.cpp | 84 ++++++++++++++++++++------- src/proof/theory_proof.h | 20 +++---- src/proof/uf_proof.cpp | 21 ++++--- src/proof/uf_proof.h | 2 + test/regress/regress0/bt-test-00.smt2 | 1 - test/regress/regress0/bt-test-01.smt2 | 1 - test/regress/regress0/bug217.smt2 | 1 - 12 files changed, 128 insertions(+), 62 deletions(-) diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index fa89a457f..6d04c3004 100644 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -20,13 +20,13 @@ (! f1 formula (! f2 formula formula))) - + (define formula_op3 (! f1 formula (! f2 formula (! f3 formula formula)))) - + (declare not formula_op1) (declare and formula_op2) (declare or formula_op2) @@ -76,6 +76,10 @@ (! u (th_holds (not (p_app x))) (th_holds (= Bool x t_false))))) +(declare f_to_b + (! f formula + (term Bool))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; ; CNF Clausification @@ -107,8 +111,8 @@ (! vbv (bvatom v bv_v) (holds cln)))))) (holds cln)))) - - + + ; clausify a formula directly (declare clausify_form (! f formula @@ -116,14 +120,14 @@ (! a (atom v f) (! u (th_holds f) (holds (clc (pos v) cln))))))) - + (declare clausify_form_not (! f formula (! v var (! a (atom v f) (! u (th_holds (not f)) (holds (clc (neg v) cln))))))) - + (declare clausify_false (! u (th_holds false) (holds cln))) @@ -134,7 +138,7 @@ (! u2 (! v (th_holds f) (holds cln)) (holds cln))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; ; Natural deduction rules : used for CNF @@ -191,7 +195,7 @@ (! f2 formula (! u2 (th_holds (not (or f1 f2))) (th_holds (and (not f1) (not f2))))))) - + ;; and elimination (declare and_elim_1 @@ -211,7 +215,7 @@ (! f2 formula (! u2 (th_holds (not (and f1 f2))) (th_holds (or (not f1) (not f2))))))) - + ;; impl elimination (declare impl_intro (! f1 formula @@ -231,7 +235,7 @@ (! f2 formula (! u (th_holds (not (impl f1 f2))) (th_holds (and f1 (not f2))))))) - + ;; iff elimination (declare iff_elim_1 @@ -358,10 +362,10 @@ (! u (! o (holds (clc (neg bv_v) cln)) ;; l binding to be used in proof (holds C)) (holds (clc (pos v) C)))))))))) - + (declare bv_ast (! v var - (! bv_v var + (! bv_v var (! f formula (! C clause (! r (atom v f) ; this is specified @@ -397,7 +401,7 @@ ;; ... ;; (or_elim_1 _ _ l2 ;; (or_elim_1 _ _ l1 A))))) ln) -;; +;; ;;))))))) (\ C ;; ;; We now have the free variable C, which should be the clause (v1 V ... V vn). @@ -415,9 +419,7 @@ ;; (contra _ l3 ;; (or_elim_1 _ _ l2 ;; (or_elim_1 _ _ (not_not_intro l1) A)))) -;; +;; ;;))))))) (\ C ;; ;; C should be the clause (~v1 V v2 V ~v3 ) - - diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index cc60d8c07..af158f37b 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -1197,8 +1197,11 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM Assert ((term.getKind() == kind::SELECT) || (term.getKind() == kind::PARTIAL_SELECT_0) || (term.getKind() == kind::PARTIAL_SELECT_1) || (term.getKind() == kind::STORE)); switch (term.getKind()) { - case kind::SELECT: + case kind::SELECT: { Assert(term.getNumChildren() == 2); + + bool convertToBool = (term[1].getType().isBoolean() && !d_proofEngine->printsAsBool(term[1])); + os << "(apply _ _ (apply _ _ (read "; printSort(ArrayType(term[0].getType()).getIndexType(), os); os << " "; @@ -1206,9 +1209,12 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM os << ") "; printTerm(term[0], os, map); os << ") "; + if (convertToBool) os << "(f_to_b "; printTerm(term[1], os, map); + if (convertToBool) os << ")"; os << ") "; return; + } case kind::PARTIAL_SELECT_0: Assert(term.getNumChildren() == 1); @@ -1381,7 +1387,15 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p } void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { - // Nothing to do here at this point. + // Nothing to do here at this point. +} + +bool LFSCArrayProof::printsAsBool(const Node &n) +{ + if (n.getKind() == kind::SELECT) + return true; + + return false; } } /* CVC4 namespace */ diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 61f168a16..eaf2f47fb 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -125,6 +125,8 @@ public: virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap); + + bool printsAsBool(const Node &n); }; diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 69b613f28..d1a228ecb 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -350,8 +350,9 @@ void LFSCCnfProof::printAtomMapping(const std::set& atoms, prop::SatVariable var = getLiteral(atom).getSatVariable(); //FIXME hideous LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); - // pe->printLetTerm(atom.toExpr(), os); + if (pe->printsAsBool(atom.toExpr())) os << "(p_app "; pe->printBoundTerm(atom.toExpr(), os, letMap); + if (pe->printsAsBool(atom.toExpr())) os << ")"; os << " (\\ " << ProofManager::getVarName(var, d_name); os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 5ce615366..ddd2029fb 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -565,6 +565,7 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; std::set atoms; + NodePairSet rewrites; // collects the atoms in the clauses d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites); @@ -779,7 +780,9 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, //TODO os << "(trust_f "; + if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << "(p_app "; ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); + if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << ")"; os << ") "; os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 156c90e47..65f66ce29 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -299,14 +299,6 @@ void LFSCTheoryProofEngine::performExtraRegistrations() { } } -void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) { - TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); - TheoryProofTable::const_iterator end = d_theoryProofTable.end(); - for (; it != end; ++it) { - it->second->treatBoolsAsFormulas(value); - } -} - void LFSCTheoryProofEngine::registerTermsFromAssertions() { ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); @@ -330,7 +322,11 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare // Assertions appear before the global let map, so we use a dummpMap to avoid letification here. ProofLetMap dummyMap; + + bool convertFromBool = (it->getType().isBoolean() && printsAsBool(*it)); + if (convertFromBool) os << "(p_app "; printBoundTerm(*it, os, dummyMap); + if (convertFromBool) os << ")"; os << ")\n"; paren << ")"; @@ -843,31 +839,47 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro Kind k = term.getKind(); switch(k) { - case kind::ITE: + 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 << ")"; + os << " "; printBoundTerm(term[1], os, map); os << " "; printBoundTerm(term[2], os, map); os << ")"; return; + } + + case kind::EQUAL: { + bool booleanCase = term[0].getType().isBoolean(); - case kind::EQUAL: os << "("; - if( term[0].getType().isBoolean() ){ + if (booleanCase) { os << "iff "; - }else{ + } else { os << "= "; printSort(term[0].getType(), os); os << " "; } + + if (booleanCase && printsAsBool(term[0])) os << "(p_app "; printBoundTerm(term[0], os, map); + if (booleanCase && printsAsBool(term[0])) os << ")"; + os << " "; + + if (booleanCase && printsAsBool(term[1])) os << "(p_app "; printBoundTerm(term[1], os, map); + if (booleanCase && printsAsBool(term[1])) os << ") "; os << ")"; + return; + } case kind::DISTINCT: // Distinct nodes can have any number of chidlren. @@ -917,9 +929,11 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro // arguments, so we have to flatten chained operators, like =. Kind op = term.getOperator().getConst().getOperator(); std::string op_str; - if( op==kind::EQUAL && term[0].getType().isBoolean() ){ + bool booleanCase; + if (op==kind::EQUAL && term[0].getType().isBoolean()) { + booleanCase = term[0].getType().isBoolean(); op_str = "iff"; - }else{ + } else { op_str = utils::toLFSCKind(op); } size_t n = term.getNumChildren(); @@ -930,9 +944,13 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro paren << ")"; } os << "(" << op_str << " "; + if (booleanCase && printsAsBool(term[i - 1])) os << "(p_app "; printBoundTerm(term[i - 1], os, map); + if (booleanCase && printsAsBool(term[i - 1])) os << ")"; os << " "; + if (booleanCase && printsAsBool(term[i])) os << "(p_app "; printBoundTerm(term[i], os, map); + if (booleanCase && printsAsBool(term[i])) os << ")"; os << ")"; if(i + 1 < n) { os << " "; @@ -1049,6 +1067,15 @@ bool TheoryProofEngine::supportedTheory(theory::TheoryId id) { id == theory::THEORY_BOOL); } +bool TheoryProofEngine::printsAsBool(const Node &n) { + if (!n.getType().isBoolean()) { + return false; + } + + theory::TheoryId theory_id = theory::Theory::theoryOf(n); + return getTheoryProof(theory_id)->printsAsBool(n); +} + BooleanProof::BooleanProof(TheoryProofEngine* proofEngine) : TheoryProof(NULL, proofEngine) {} @@ -1068,10 +1095,7 @@ void BooleanProof::registerTerm(Expr term) { void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Assert (term.getType().isBoolean()); if (term.isVariable()) { - if (d_treatBoolsAsFormulas) - os << "(p_app " << ProofManager::sanitize(term) <<")"; - else - os << ProofManager::sanitize(term); + os << ProofManager::sanitize(term); return; } @@ -1116,7 +1140,11 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe std::ostringstream paren; os << " "; for (unsigned i = 0; i < term.getNumChildren(); ++i) { + + if (printsAsBool(term[i])) os << "(p_app "; d_proofEngine->printBoundTerm(term[i], os, map); + if (printsAsBool(term[i])) os << ")"; + os << " "; if(i < term.getNumChildren() - 2) { os << "(" << utils::toLFSCKind(k) << " "; @@ -1128,17 +1156,16 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe // this is for binary and unary operators for (unsigned i = 0; i < term.getNumChildren(); ++i) { os << " "; + if (printsAsBool(term[i])) os << "(p_app "; d_proofEngine->printBoundTerm(term[i], os, map); + if (printsAsBool(term[i])) os << ")"; } os << ")"; } return; case kind::CONST_BOOLEAN: - if (d_treatBoolsAsFormulas) - os << (term.getConst() ? "true" : "false"); - else - os << (term.getConst() ? "t_true" : "t_false"); + os << (term.getConst() ? "true" : "false"); return; default: @@ -1182,6 +1209,19 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector& lemma, Unreachable("No boolean lemmas yet!"); } +bool LFSCBooleanProof::printsAsBool(const Node &n) +{ + Kind k = n.getKind(); + switch (k) { + case kind::BOOLEAN_TERM_VARIABLE: + case kind::VARIABLE: + return true; + + default: + return false; + } +} + void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { // By default, we just print a trust statement. Specific theories can implement // better proofs. diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 34248f7eb..bbdb7d6d7 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -151,9 +151,9 @@ public: void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); - virtual void treatBoolsAsFormulas(bool value) {}; - virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; + + bool printsAsBool(const Node &n); }; class LFSCTheoryProofEngine : public TheoryProofEngine { @@ -182,7 +182,6 @@ public: void performExtraRegistrations(); - void treatBoolsAsFormulas(bool value); void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os); private: @@ -294,7 +293,11 @@ public: */ virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2); - virtual void treatBoolsAsFormulas(bool value) {} + // Return true if node prints as bool, false if it prints as a formula. + virtual bool printsAsBool(const Node &n) { + // Most nodes print as formulas, so this is the default. + return false; + } }; class BooleanProof : public TheoryProof { @@ -318,7 +321,7 @@ public: class LFSCBooleanProof : public BooleanProof { public: LFSCBooleanProof(TheoryProofEngine* proofEngine) - : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true) + : BooleanProof(proofEngine) {} virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); @@ -328,12 +331,7 @@ public: virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap); - void treatBoolsAsFormulas(bool value) { - d_treatBoolsAsFormulas = value; - } - -private: - bool d_treatBoolsAsFormulas; + bool printsAsBool(const Node &n); }; } /* CVC4 namespace */ diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 41262051c..d3da2bcdb 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -701,17 +701,13 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF); if (term.getKind() == kind::VARIABLE || - term.getKind() == kind::SKOLEM) { + term.getKind() == kind::SKOLEM || + term.getKind() == kind::BOOLEAN_TERM_VARIABLE) { os << term; return; } - if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) { - os << "(p_app " << term << ")"; - return; - } Assert (term.getKind() == kind::APPLY_UF); - d_proofEngine->treatBoolsAsFormulas(false); if(term.getType().isBoolean()) { os << "(p_app "; @@ -722,13 +718,15 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& } os << func << " "; for (unsigned i = 0; i < term.getNumChildren(); ++i) { + bool convertToBool = (term[i].getType().isBoolean() && !d_proofEngine->printsAsBool(term[i])); + if (convertToBool) os << "(f_to_b "; d_proofEngine->printBoundTerm(term[i], os, map); + if (convertToBool) os << ")"; os << ")"; } if(term.getType().isBoolean()) { os << ")"; } - d_proofEngine->treatBoolsAsFormulas(true); } void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) { @@ -803,4 +801,13 @@ void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& pare // Nothing to do here at this point. } +bool LFSCUFProof::printsAsBool(const Node &n) +{ + Debug("gk::temp") << "\nUF printsAsBool: " << n << std::endl; + if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE) + return true; + + return false; +} + } /* namespace CVC4 */ diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index ff0f9a879..221a50f43 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -71,6 +71,8 @@ public: virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap); + + bool printsAsBool(const Node &n); }; diff --git a/test/regress/regress0/bt-test-00.smt2 b/test/regress/regress0/bt-test-00.smt2 index cd3e1137e..517806542 100644 --- a/test/regress/regress0/bt-test-00.smt2 +++ b/test/regress/regress0/bt-test-00.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-proofs ; EXPECT: unsat (set-logic QF_UF) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/bt-test-01.smt2 b/test/regress/regress0/bt-test-01.smt2 index 918dcf9ec..e17bd2d7a 100644 --- a/test/regress/regress0/bt-test-01.smt2 +++ b/test/regress/regress0/bt-test-01.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-proofs ; EXPECT: unsat (set-logic QF_UF) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2 index 34cfcad33..4d2e828b5 100644 --- a/test/regress/regress0/bug217.smt2 +++ b/test/regress/regress0/bug217.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-proofs ; EXPECT: unsat (set-logic QF_UF) (set-info :status unsat) -- 2.30.2