From: Lachnitt Date: Thu, 23 Sep 2021 21:46:05 +0000 (-0700) Subject: [proofs] Alethe: Add Alethe Files to be Compiled (#7241) X-Git-Tag: cvc5-1.0.0~1172 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6c67ed5a2521012d523eb3f11ff344bf7062ee6e;p=cvc5.git [proofs] Alethe: Add Alethe Files to be Compiled (#7241) Adds Alethe proof rule and option. Adds alethe_post_processor and alethe_proof_rule files to list of files to be compiled. During incorporating these changes errors occurred in the SCOPE rule that are also fixed in this PR. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3113f03ab..8f574dc82 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -221,6 +221,10 @@ libcvc5_add_sources( proof/unsat_core.h proof/alethe/alethe_node_converter.cpp proof/alethe/alethe_node_converter.h + proof/alethe/alethe_post_processor.cpp + proof/alethe/alethe_post_processor.h + proof/alethe/alethe_proof_rule.cpp + proof/alethe/alethe_proof_rule.h prop/bv_sat_solver_notify.h prop/bvminisat/bvminisat.cpp prop/bvminisat/bvminisat.h diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index 0225cf24c..0ba3ae413 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -15,9 +15,9 @@ name = "Proof" [[option.mode.DOT]] name = "dot" help = "Output DOT proof" -[[option.mode.VERIT]] - name = "verit" - help = "Output veriT proof" +[[option.mode.ALETHE]] + name = "alethe" + help = "Output Alethe proof" [[option.mode.TPTP]] name = "tptp" help = "Output TPTP proof (work in progress)" diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 312921db4..9b94175fa 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -150,12 +150,16 @@ bool AletheProofPostprocessCallback::update(Node res, sanitized_args, *cdp); - Node vp3 = vp1; - - if (args.size() != 1) + Node andNode, vp3; + if (args.size() == 1) + { + vp3 = vp1; + andNode = args[0]; // F1 + } + else { // Build vp2i - Node andNode = nm->mkNode(kind::AND, args); // (and F1 ... Fn) + andNode = nm->mkNode(kind::AND, args); // (and F1 ... Fn) std::vector premisesVP2 = {vp1}; std::vector notAnd = {d_cl, children[0]}; // cl F Node vp2_i; @@ -178,8 +182,7 @@ bool AletheProofPostprocessCallback::update(Node res, success &= addAletheStep(AletheRule::REORDER, vp2b, vp2b, {vp2a}, {}, *cdp); - Node vp3 = - nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), children[0]); + vp3 = nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), children[0]); success &= addAletheStep( AletheRule::DUPLICATED_LITERALS, vp3, vp3, {vp2b}, {}, *cdp); } @@ -288,6 +291,43 @@ bool AletheProofPostprocessCallback::addAletheStepFromOr( return addAletheStep(rule, res, conclusion, children, args, cdp); } +AletheProofPostprocessFinalCallback::AletheProofPostprocessFinalCallback( + ProofNodeManager* pnm, AletheNodeConverter& anc) + : d_pnm(pnm), d_anc(anc) +{ + NodeManager* nm = NodeManager::currentNM(); + d_cl = nm->mkBoundVar("cl", nm->sExprType()); +} + +bool AletheProofPostprocessFinalCallback::shouldUpdate( + std::shared_ptr pn, + const std::vector& fa, + bool& continueUpdate) +{ + return false; +} + +bool AletheProofPostprocessFinalCallback::update( + Node res, + PfRule id, + const std::vector& children, + const std::vector& args, + CDProof* cdp, + bool& continueUpdate) +{ + return true; +} + +AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm, + AletheNodeConverter& anc) + : d_pnm(pnm), d_cb(d_pnm, anc), d_fcb(d_pnm, anc) +{ +} + +AletheProofPostprocess::~AletheProofPostprocess() {} + +void AletheProofPostprocess::process(std::shared_ptr pf) {} + } // namespace proof } // namespace cvc5 diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index d8fae8a55..4a7d8cf61 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -16,9 +16,9 @@ #ifndef CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H #define CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H -#include "proof/proof_node_updater.h" #include "proof/alethe/alethe_node_converter.h" #include "proof/alethe/alethe_proof_rule.h" +#include "proof/proof_node_updater.h" namespace cvc5 { @@ -118,8 +118,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback { public: - AletheProofPostprocessFinalCallback(ProofNodeManager* pnm, - AletheNodeConverter& anc); + AletheProofPostprocessFinalCallback(ProofNodeManager* pnm, + AletheNodeConverter& anc); ~AletheProofPostprocessFinalCallback() {} /** Should proof pn be updated? It should, if the last step is printed as (cl * false) or if it is an assumption (in that case it is printed as false). @@ -159,7 +159,7 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback class AletheProofPostprocess { public: - AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc); + AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc); ~AletheProofPostprocess(); /** post-process */ void process(std::shared_ptr pf); diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 5cf5dc0f8..d4e763fe6 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -202,6 +202,7 @@ const char* toString(PfRule id) case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; //================================================= External rules case PfRule::LFSC_RULE: return "LFSC_RULE"; + case PfRule::ALETHE_RULE: return "ALETHE_RULE"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index bb677bdb9..25bbf3d34 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -1406,6 +1406,15 @@ enum class PfRule : uint32_t // --------------------- // Conclusion: (Q) LFSC_RULE, + //================================================ Place holder for Alethe + // rules + // ======== Alethe rule + // Children: (P1 ... Pn) + // Arguments: (id, Q, Q', A1, ..., Am) + // --------------------- + // Conclusion: (Q) + // where Q' is the representation of Q to be printed by the Alethe printer. + ALETHE_RULE, //================================================= Unknown rule UNKNOWN, diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 4d6e2b495..d5e07991a 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -19,6 +19,8 @@ #include "options/main_options.h" #include "options/proof_options.h" #include "options/smt_options.h" +#include "proof/alethe/alethe_node_converter.h" +#include "proof/alethe/alethe_post_processor.h" #include "proof/dot/dot_printer.h" #include "proof/proof_checker.h" #include "proof/proof_node_algorithm.h" @@ -60,13 +62,13 @@ PfManager::PfManager(Env& env) // where A is an available assumption from outside the scope (note // that B1 was an assumption of this SCOPE subproof but since it could // be inferred from A, it was updated). This shape is problematic for - // the veriT reconstruction, so we disable the update of scoped + // the Alethe reconstruction, so we disable the update of scoped // assumptions (which would disable the update of B1 in this case). d_pfpp.reset(new ProofPostproccess( env, d_pppg.get(), nullptr, - options::proofFormatMode() != options::ProofFormatMode::VERIT)); + options::proofFormatMode() != options::ProofFormatMode::ALETHE)); // add rules to eliminate here if (options::proofGranularityMode() != options::ProofGranularityMode::OFF) @@ -171,6 +173,12 @@ void PfManager::printProof(std::ostream& out, proof::DotPrinter dotPrinter; dotPrinter.print(out, fp.get()); } + else if (options::proofFormatMode() == options::ProofFormatMode::ALETHE) + { + proof::AletheNodeConverter anc; + proof::AletheProofPostprocess vpfpp(d_pnm.get(), anc); + vpfpp.process(fp); + } else if (options::proofFormatMode() == options::ProofFormatMode::TPTP) { out << "% SZS output start Proof for " << options().driver.filename