summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt4
-rw-r--r--src/options/proof_options.toml6
-rw-r--r--src/proof/alethe/alethe_post_processor.cpp52
-rw-r--r--src/proof/alethe/alethe_post_processor.h8
-rw-r--r--src/proof/proof_rule.cpp1
-rw-r--r--src/proof/proof_rule.h9
-rw-r--r--src/smt/proof_manager.cpp12
7 files changed, 77 insertions, 15 deletions
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<Node> premisesVP2 = {vp1};
std::vector<Node> 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<ProofNode> pn,
+ const std::vector<Node>& fa,
+ bool& continueUpdate)
+{
+ return false;
+}
+
+bool AletheProofPostprocessFinalCallback::update(
+ Node res,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& 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<ProofNode> 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<ProofNode> 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback