Connect the LFSC printer (#7323)

This adds the option --proof-format=lfsc.

It adds an initial regression to test the LFSC printer. This will be followed up with a more comprehensive plan for regression tests.

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 0ba3ae4137a64dc6d0ba3d53bef82c592ef7d86c..36891fd517764a2926c9db792e4ed28a0d82326f 100644 (file)
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -15,6 +15,9 @@ name   = "Proof"
 [[option.mode.DOT]]
   name       = "dot"
   help       = "Output DOT proof"
+[[option.mode.LFSC]]
+  name       = "lfsc"
+  help       = "Output LFSC proof"
 [[option.mode.ALETHE]]
   name       = "alethe"
   help       = "Output Alethe proof"

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 7f024c28908b15a40ae3a2633401aaa4a1f9d4b0..2e08ab2dfba528284419673a302d2c1ba0ee74eb 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -22,6 +22,8 @@
 #include "proof/alethe/alethe_node_converter.h"
 #include "proof/alethe/alethe_post_processor.h"
 #include "proof/dot/dot_printer.h"
+#include "proof/lfsc/lfsc_post_processor.h"
+#include "proof/lfsc/lfsc_printer.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
@@ -166,8 +168,6 @@ void PfManager::printProof(std::ostream& out,
   {
     fp = d_pnm->clone(fp);
   }
-  // TODO (proj #37) according to the proof format, post process the proof node
-  // TODO (proj #37) according to the proof format, print the proof node
 
   // according to the proof format, post process and print the proof node
   if (options().proof.proofFormatMode == options::ProofFormatMode::DOT)
@@ -181,6 +181,16 @@ void PfManager::printProof(std::ostream& out,
     proof::AletheProofPostprocess vpfpp(d_pnm.get(), anc);
     vpfpp.process(fp);
   }
+  else if (options().proof.proofFormatMode == options::ProofFormatMode::LFSC)
+  {
+    std::vector<Node> assertions;
+    getAssertions(as, assertions);
+    proof::LfscNodeConverter ltp;
+    proof::LfscProofPostprocess lpp(ltp, d_pnm.get());
+    lpp.process(fp);
+    proof::LfscPrinter lp(ltp);
+    lp.print(out, assertions, fp.get());
+  }
   else if (options().proof.proofFormatMode == options::ProofFormatMode::TPTP)
   {
     out << "% SZS output start Proof for " << options().driver.filename

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 190903327482dbdf11811bb61ed4000af13e6a2d..907dc22d162fbbdae4b3f88313a72bff704b74d5 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -840,6 +840,7 @@ set(regress_0_tests
   regress0/printer/tuples_and_records.cvc.smt2
   regress0/proofs/cyclic-ucp.smt2
   regress0/proofs/issue277-circuit-propagator.smt2
+  regress0/proofs/lfsc-test-1.smt2
   regress0/proofs/open-pf-datatypes.smt2
   regress0/proofs/open-pf-if-unordered-iff.smt2
   regress0/proofs/open-pf-rederivation.smt2

diff --git a/test/regress/regress0/proofs/lfsc-test-1.smt2 b/test/regress/regress0/proofs/lfsc-test-1.smt2
new file mode 100644 (file)
index 0000000..d82ff30
--- /dev/null
+++ b/test/regress/regress0/proofs/lfsc-test-1.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --dump-proofs --proof-format-mode=lfsc 
+; EXIT: 0
+; SCRUBBER: grep -v -E '.*' 
+(set-logic QF_UF)
+(set-info :category "crafted")
+
+(declare-sort U 0)
+(declare-fun f1 () U)
+(declare-fun f2 () U)
+(declare-fun f3 () U)
+(declare-fun f4 () U)
+(declare-fun p (U) Bool)
+(assert (not (= f1 f2)))
+(assert (and (p f1) (or (= f1 f2) (distinct f3 f4 f2)) (p f3)))
+(assert (= f3 f4))
+(check-sat)
+(exit)