From: Alex Ozdemir Date: Fri, 6 Dec 2019 15:51:54 +0000 (-0800) Subject: [proof] Eliminate side-condition from ER signature (#3230) X-Git-Tag: cvc5-1.0.0~3791 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=499aa5641e2b830f60159c2ce1c791bf4d45aac1;p=cvc5.git [proof] Eliminate side-condition from ER signature (#3230) * [proof] Eliminate the side condition in er.plf By tweaking the axioms a bit, I got rid of the lone SC in the Extended Resolution signature. * [proof] Changed er_proof.cpp in line with signature The new signature requires slightly different proof printing. * [proof] clang-format er_proof.cpp * Fix tests * [proof] Actually delete the SC * Apply suggestions from code review Co-Authored-By: yoni206 * Add LFSC-checking unit test for ER proof * Gate the lfsc invocation on the build system * Properly gate the lfsc check on the build system * gate the plf_signatures forward def on the build system --- diff --git a/proofs/signatures/er.plf b/proofs/signatures/er.plf index 8b559671e..9fcc9d4e8 100644 --- a/proofs/signatures/er.plf +++ b/proofs/signatures/er.plf @@ -64,13 +64,17 @@ (holds cln))) (holds cln))))) -; Takes a `list` of literals and a clause, `suffix`, adds the suffix to each -; literal and returns a list of clauses as a `cnf`. -(program clause_add_suffix_all ((list clause) (suffix clause)) cnf - (match list - (cln cnfn) - ((clc l rest) (cnfc (clc l suffix) - (clause_add_suffix_all rest suffix))))) +; Represents multiple conjoined clauses. +; There is a list, `heads` of literals, each of which is suffixed by the +; same `tail`. +(declare common_tail_cnf_t type) +(declare common_tail_cnf + (! heads clause + (! tail clause common_tail_cnf_t))) + +; A member of this type is a proof of a common_tail_cnf. +(declare common_tail_cnf_holds + (! cnf common_tail_cnf_t type)) ; This translates a definition witness value for the def: ; @@ -89,10 +93,6 @@ (! def (definition new old others) (! negOld lit (! mkNegOld (^ (lit_flip old) negOld) - (! provenCnf cnf - (! mkProvenCnf (^ (clause_add_suffix_all - others - (clc (neg new) (clc old cln))) provenCnf) ; If you can prove bottom from its clausal representation (! pf_continuation ; new v l_1 v l_2 v ... v l_n @@ -100,26 +100,31 @@ ; new v ~old (! pf_c2 (holds (clc (pos new) (clc negOld cln))) ; for each i <= n: l_i v ~new v old - (! pf_cs (cnf_holds provenCnf) + (! pf_cs (common_tail_cnf_holds + (common_tail_cnf + others + (clc (neg new) (clc old cln)))) (holds cln)))) ; Then you've proven bottom - (holds cln))))))))))) + (holds cln))))))))) -; This axiom is useful for converting a proof of some CNF formula (a value of -; type (cnf_holds ...)) into proofs of the constituent clauses (many values of -; type (holds ...)). +; These axioms are useful for converting a proof of some CNF formula represented +; using the `common_tail_cnf` type (a value of type `common_tail_cnf_holds`), +; into proofs of its constituent clauses (many values of type `holds`). ; Given -; 1. a proof of some cnf, first ^ rest, and -; 2. a proof continuation that -; a. takes in proofs of -; i. first and -; ii. rest and -; b. proceeds to prove bottom, -; proves bottom. -(declare cnfc_unroll_towards_bottom - (! first clause - (! rest cnf - (! pf (cnf_holds (cnfc first rest)) - (! pf_continuation (! r1 (holds first) (! r2 (cnf_holds rest) (holds cln))) - (holds cln)))))) - +; 1. a proof of some `common_tail_cnf` +; Then +; 1. the first axiom gives you a proof of the first `clause` therein and +; 2. the second gives you a proof of the rest of the `common_tail_cnf`. +(declare common_tail_cnf_prove_head + (! first lit + (! rest clause + (! tail clause + (! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail)) + (holds (clc first tail))))))) +(declare common_tail_cnf_prove_tail + (! first lit + (! rest clause + (! tail clause + (! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail)) + (common_tail_cnf_holds (common_tail_cnf rest tail))))))) diff --git a/proofs/signatures/er_test.plf b/proofs/signatures/er_test.plf index 27c61de1f..1b5117a70 100644 --- a/proofs/signatures/er_test.plf +++ b/proofs/signatures/er_test.plf @@ -1,30 +1,5 @@ ; Depends on er.plf -; Type for representing success when testing a side-condition -(declare TestSuccess type) - -; Test for clause_add_suffix_all -(declare test_clause_add_suffix_all - (! list clause - (! suffix clause - (! result cnf - (! (^ (clause_add_suffix_all list suffix) result) - TestSuccess))))) - -(check - (% a lit - (% b lit - (% c lit - (test_clause_add_suffix_all - (clc a (clc b cln)) - (clc c cln) - (cnfc (clc a (clc c cln)) - (cnfc (clc b (clc c cln)) - cnfn)) - ) - ))) -) - ; This is a circuitous proof that uses the definition introduction and ; unrolling rules (check @@ -40,13 +15,11 @@ (clc (neg v2) cln) (\ v3 (\ def3 - (clausify_definition _ _ _ def3 _ _ + (clausify_definition _ _ _ def3 _ (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln))) (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln))) - (\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn)) - (cnfc_unroll_towards_bottom _ _ pf_cnf3 - (\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) - (\ pf_cnfn + (\ pf_cnf ; type: (common_tail_cnf (clc (neg v2) cln) (clc (neg v3) (clc (neg v1) cln))) + (@ pf_c7 (common_tail_cnf_prove_head _ _ _ pf_cnf) ; Clauses (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2 (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3 @@ -61,7 +34,7 @@ )) )) )) - ))) + ) ))) ) )) @@ -92,10 +65,10 @@ cln (\ v5 (\ def1 - (clausify_definition _ _ _ def1 _ _ + (clausify_definition _ _ _ def1 _ (\ pf_c9 ; type: (holds (clc (pos def1v) cln)) (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln))) - (\ idc0 ; type: (cnf_holds cnfn) + (\ idc0 ; type: (common_tail_cnf cln _) (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11 (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12 (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13 diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp index 19c838e2d..9b036c3a6 100644 --- a/src/proof/er/er_proof.cpp +++ b/src/proof/er/er_proof.cpp @@ -27,6 +27,7 @@ #include #include #include +#include #include #include "base/check.h" @@ -204,7 +205,7 @@ void ErProof::outputAsLfsc(std::ostream& os) const // Print Definitions for (const ErDefinition& def : d_definitions) { - os << "\n (decl_rat_elimination_def (" + os << "\n (decl_definition (" << (def.d_oldLiteral.isNegated() ? "neg " : "pos ") << ProofManager::getVarName(def.d_oldLiteral.getSatVariable(), "bb") << ") "; @@ -219,8 +220,8 @@ void ErProof::outputAsLfsc(std::ostream& os) const TraceCheckIdx firstDefClause = d_inputClauseIds.size() + 1; for (const ErDefinition& def : d_definitions) { - os << "\n (clausify_rat_elimination_def _ _ _ " - << "er.def " << def.d_newVariable << " _ _ (\\ er.c" << firstDefClause + os << "\n (clausify_definition _ _ _ " + << "er.def" << def.d_newVariable << " _ (\\ er.c" << firstDefClause << " (\\ er.c" << (firstDefClause + 1) << " (\\ er.cnf" << def.d_newVariable; @@ -228,22 +229,35 @@ void ErProof::outputAsLfsc(std::ostream& os) const } parenCount += 4 * d_definitions.size(); - // Unroll proofs of CNFs to proofs of clauses + // Unroll proofs of CNF to proofs of clauses firstDefClause = d_inputClauseIds.size() + 1; for (const ErDefinition& def : d_definitions) { for (size_t i = 0, n = def.d_otherLiterals.size(); i < n; ++i) { - os << "\n (cnfc_unroll _ _ "; - os << "er.cnf" << def.d_newVariable; + // Compute the name of the CNF proof we're unrolling in this step + std::ostringstream previousCnfProof; + previousCnfProof << "er.cnf" << def.d_newVariable; if (i != 0) { - os << ".u" << i; + // For all but the first unrolling, the previous CNF has an unrolling + // number attached + previousCnfProof << ".u" << i; } - os << " (\\ er.c" << (firstDefClause + 2 + i); - os << " (\\ er.cnf" << def.d_newVariable << ".u" << (i + 1); + + // Prove the first clause in the CNF + os << "\n (@ "; + os << "er.c" << (firstDefClause + 2 + i); + os << " (common_tail_cnf_prove_head _ _ _ " << previousCnfProof.str() + << ")"; + + // Prove the rest of the CNF + os << "\n (@ "; + os << "er.cnf" << def.d_newVariable << ".u" << (i + 1); + os << " (common_tail_cnf_prove_tail _ _ _ " << previousCnfProof.str() + << ")"; } - parenCount += 3 * def.d_otherLiterals.size(); + parenCount += 2 * def.d_otherLiterals.size(); firstDefClause += 2 + def.d_otherLiterals.size(); } diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 0c82bcc1a..9b9a2a100 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -61,6 +61,10 @@ macro(cvc4_add_unit_test is_white name output_dir) target_link_libraries(${name} main-test) target_include_directories(${name} PRIVATE ${CxxTest_INCLUDE_DIR}) target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK}) + if(USE_LFSC) + # We don't link against LFSC, because CVC4 is already linked against it. + target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR}) + endif() if(${is_white}) target_compile_options(${name} PRIVATE -fno-access-control) endif() diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h index 9089cee5f..fa7721f97 100644 --- a/test/unit/proof/er_proof_black.h +++ b/test/unit/proof/er_proof_black.h @@ -20,14 +20,27 @@ #include #include #include +#include #include #include +#include "base/configuration_private.h" #include "proof/clause_id.h" #include "proof/er/er_proof.h" #include "prop/sat_solver_types.h" #include "utils.h" +#if IS_LFSC_BUILD +#include "lfscc.h" + +namespace CVC4 { +namespace proof { +extern const char* const plf_signatures; +} // namespace proof +} // namespace CVC4 +#endif + + using namespace CVC4; using namespace CVC4::proof::er; using namespace CVC4::prop; @@ -291,12 +304,12 @@ void ErProofBlack::testErTraceCheckOutput() pf.outputAsLfsc(lfsc); std::string out = R"EOF( - (decl_rat_elimination_def + (decl_definition (neg bb.v0) cln (\ er.v4 (\ er.def4 - (clausify_rat_elimination_def _ _ _ er.def4 _ _ + (clausify_definition _ _ _ er.def4 _ (\ er.c9 (\ er.c10 (\ er.cnf4 @@ -414,63 +427,38 @@ void ErProofBlack::testErTraceCheckOutputMedium() SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)}); ErProof pf(clauses, usedIds, std::move(tc)); - std::ostringstream lfsc; - pf.outputAsLfsc(lfsc); + std::ostringstream actual_pf_body; + pf.outputAsLfsc(actual_pf_body); + +#if IS_LFSC_BUILD + std::string pf_header = R"EOF( + (check + (% bb.v0 var + (% bb.v1 var + (% bb.v2 var + (% bb.v3 var + (% bb.pb1 (holds (clc (pos bb.v0) (clc (pos bb.v1) (clc (neg bb.v2) cln)))) + (% bb.pb2 (holds (clc (neg bb.v0) (clc (neg bb.v1) (clc (pos bb.v2) cln)))) + (% bb.pb3 (holds (clc (pos bb.v1) (clc (pos bb.v2) (clc (neg bb.v3) cln)))) + (% bb.pb4 (holds (clc (neg bb.v1) (clc (neg bb.v2) (clc (pos bb.v3) cln)))) + (% bb.pb5 (holds (clc (neg bb.v0) (clc (neg bb.v2) (clc (neg bb.v3) cln)))) + (% bb.pb6 (holds (clc (pos bb.v0) (clc (pos bb.v2) (clc (pos bb.v3) cln)))) + (% bb.pb7 (holds (clc (neg bb.v0) (clc (pos bb.v1) (clc (pos bb.v3) cln)))) + (% bb.pb8 (holds (clc (pos bb.v0) (clc (neg bb.v1) (clc (neg bb.v3) cln)))) + (: (holds cln) + )EOF"; - std::string out = R"EOF( - (decl_rat_elimination_def - (neg bb.v0) - (clc (pos bb.v1) (clc (pos bb.v3) cln)) - (\ er.v4 - (\ er.def4 - (decl_rat_elimination_def - (pos bb.v2) - cln - (\ er.v5 - (\ er.def5 - (clausify_rat_elimination_def _ _ _ er.def4 _ _ - (\ er.c9 - (\ er.c10 - (\ er.cnf4 - (clausify_rat_elimination_def _ _ _ er.def5 _ _ - (\ er.c13 - (\ er.c14 - (\ er.cnf5 - (cnfc_unroll _ _ er.cnf4 - (\ er.c11 - (\ er.cnf4.u1 - (cnfc_unroll _ _ er.cnf4.u1 - (\ er.c12 - (\ er.cnf4.u2 - (satlem_simplify _ _ _ - (R _ _ (R _ _ (Q _ _ (Q _ _ er.c11 bb.pb1 bb.v0) - er.c10 er.v4) - bb.pb7 bb.v0) - bb.pb4 bb.v1) (\ er.c15 - (satlem_simplify _ _ _ - (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c16 - (satlem_simplify _ _ _ - (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c17 - (satlem_simplify _ _ _ - (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c18 - (satlem_simplify _ _ _ - (R _ _ (Q _ _ bb.pb3 er.c17 bb.v3) er.c18 bb.v2) (\ er.c19 - (satlem_simplify _ _ _ - (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c17 bb.v2) er.c16 bb.v3) - er.c19 bb.v1) (\ er.c20 - er.c20 ; (holds cln) - )))))))))))) - ))) - ))) - ))) - ) - ))) - ) - )) - ) - )) + std::string pf_footer = R"EOF( + ) + )))))))) + )))) ) )EOF"; - TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out)); + std::stringstream actual_pf; + actual_pf << proof::plf_signatures << pf_header << actual_pf_body.str() << pf_footer; + + lfscc_init(); + lfscc_check_file(actual_pf, false, false, false, false, false, false, false); +#endif }