From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 11 Oct 2021 14:28:51 +0000 (-0500)
Subject: Connect the LFSC printer (#7323)
X-Git-Tag: cvc5-1.0.0~1094
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c9c909d8815c8026b6aaa1da259672aa96d193e;p=cvc5.git

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 0ba3ae413..36891fd51 100644
--- 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 7f024c289..2e08ab2df 100644
--- 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 190903327..907dc22d1 100644
--- 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
index 000000000..d82ff30fd
--- /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)