diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-12-06 07:51:54 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-06 07:51:54 -0800 |
commit | 499aa5641e2b830f60159c2ce1c791bf4d45aac1 (patch) | |
tree | 600ada9e557b8c22f15c37440b109bd5470c95f1 /src | |
parent | 008d6b51baec353f45324e1d9407d898866cf688 (diff) |
[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 <yoni206@users.noreply.github.com>
* 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
Diffstat (limited to 'src')
-rw-r--r-- | src/proof/er/er_proof.cpp | 34 |
1 files changed, 24 insertions, 10 deletions
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 <fstream> #include <iostream> #include <iterator> +#include <sstream> #include <unordered_set> #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(); } |