[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

5 files changed, 114 insertions, 130 deletions

diff --git a/proofs/signatures/er.plf b/proofs/signatures/er.plf
index 8b559671e..9fcc9d4e8 100644
--- a/proofs/signatures/er.plf
+++ b/proofs/signatures/er.plf
@@ -64,13 +64,17 @@
                                            (holds cln)))
                   (holds cln)))))
 
-; Takes a `list` of literals and a clause, `suffix`, adds the suffix to each
-; literal and returns a list of clauses as a `cnf`.
-(program clause_add_suffix_all ((list clause) (suffix clause)) cnf
-         (match list
-                (cln cnfn)
-                ((clc l rest) (cnfc (clc l suffix)
-                                    (clause_add_suffix_all rest suffix)))))
+; Represents multiple conjoined clauses.
+; There is a list, `heads` of literals, each of which is suffixed by the
+; same `tail`.
+(declare common_tail_cnf_t type)
+(declare common_tail_cnf
+         (! heads clause
+         (! tail  clause common_tail_cnf_t)))
+
+; A member of this type is a proof of a common_tail_cnf.
+(declare common_tail_cnf_holds
+         (! cnf common_tail_cnf_t type))
 
 ; This translates a definition witness value for the def:
 ;
@@ -89,10 +93,6 @@
          (! def (definition new old others)
          (! negOld lit
          (! mkNegOld (^ (lit_flip old) negOld)
-         (! provenCnf cnf
-         (! mkProvenCnf (^ (clause_add_suffix_all
-                             others
-                             (clc (neg new) (clc old cln))) provenCnf)
          ; If you can prove bottom from its clausal representation
          (! pf_continuation
             ; new v l_1 v l_2 v ... v l_n
@@ -100,26 +100,31 @@
                ; new v ~old
                (! pf_c2 (holds (clc (pos new) (clc negOld cln)))
                   ; for each i <= n: l_i v ~new v old
-                  (! pf_cs (cnf_holds provenCnf)
+                  (! pf_cs (common_tail_cnf_holds
+                             (common_tail_cnf
+                               others
+                               (clc (neg new) (clc old cln))))
                      (holds cln))))
          ; Then you've proven bottom
-         (holds cln)))))))))))
+         (holds cln)))))))))
 
-; This axiom is useful for converting a proof of some CNF formula (a value of
-; type (cnf_holds ...)) into proofs of the constituent clauses (many values of
-; type (holds ...)).
+; These axioms are useful for converting a proof of some CNF formula represented
+; using the `common_tail_cnf` type (a value of type `common_tail_cnf_holds`),
+; into proofs of its constituent clauses (many values of type `holds`).
 ; Given
-;    1. a proof of some cnf, first ^ rest, and
-;    2. a proof continuation that
-;       a. takes in proofs of
-;          i. first and
-;          ii. rest and
-;       b. proceeds to prove bottom,
-; proves bottom.
-(declare cnfc_unroll_towards_bottom
-         (! first clause
-            (! rest cnf
-               (! pf (cnf_holds (cnfc first rest))
-                  (! pf_continuation (! r1 (holds first) (! r2 (cnf_holds rest) (holds cln)))
-                    (holds cln))))))
-
+;    1. a proof of some `common_tail_cnf`
+; Then
+;    1. the first axiom gives you a proof of the first `clause` therein and
+;    2. the second gives you a proof of the rest of the `common_tail_cnf`.
+(declare common_tail_cnf_prove_head
+         (! first lit
+         (! rest clause
+         (! tail clause
+         (! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail))
+            (holds (clc first tail)))))))
+(declare common_tail_cnf_prove_tail
+         (! first lit
+         (! rest clause
+         (! tail clause
+         (! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail))
+            (common_tail_cnf_holds (common_tail_cnf rest tail)))))))
diff --git a/proofs/signatures/er_test.plf b/proofs/signatures/er_test.plf
index 27c61de1f..1b5117a70 100644
--- a/proofs/signatures/er_test.plf
+++ b/proofs/signatures/er_test.plf
@@ -1,30 +1,5 @@
 ; Depends on er.plf
 
-; Type for representing success when testing a side-condition
-(declare TestSuccess type)
-
-; Test for clause_add_suffix_all
-(declare test_clause_add_suffix_all
-         (! list clause
-            (! suffix clause
-               (! result cnf
-                  (! (^ (clause_add_suffix_all list suffix) result)
-                     TestSuccess)))))
-
-(check
-  (% a lit
-  (% b lit
-  (% c lit
-     (test_clause_add_suffix_all
-       (clc a (clc b cln))
-       (clc c cln)
-       (cnfc (clc a (clc c cln))
-        (cnfc (clc b (clc c cln))
-        cnfn))
-     )
-  )))
-)
-
 ; This is a circuitous proof that uses the definition introduction and
 ; unrolling rules
 (check
@@ -40,13 +15,11 @@
             (clc (neg v2) cln)
             (\ v3
             (\ def3
-              (clausify_definition _ _ _ def3 _ _
+              (clausify_definition _ _ _ def3 _
                 (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln)))
                 (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln)))
-                (\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn))
-                  (cnfc_unroll_towards_bottom _ _ pf_cnf3
-                    (\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln)))
-                    (\ pf_cnfn
+                (\ pf_cnf ; type: (common_tail_cnf (clc (neg v2) cln) (clc (neg v3) (clc (neg v1) cln)))
+                  (@ pf_c7 (common_tail_cnf_prove_head _ _ _ pf_cnf)
                                                                           ; Clauses
                   (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1)  (\ pf_c8 ; v2
                   (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2)  (\ pf_c9 ; v3
@@ -61,7 +34,7 @@
                   ))
                   ))
                   ))
-                  )))
+                  )
                 )))
               )
             ))
@@ -92,10 +65,10 @@
             cln
             (\ v5
             (\ def1
-              (clausify_definition _ _ _ def1 _ _
+              (clausify_definition _ _ _ def1 _
                 (\ pf_c9 ; type: (holds (clc (pos def1v) cln))
                 (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln)))
-                (\ idc0 ; type: (cnf_holds cnfn)
+                (\ idc0 ; type: (common_tail_cnf cln _)
                   (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11
                   (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12
                   (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13
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();
   }
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 0c82bcc1a..9b9a2a100 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -61,6 +61,10 @@ macro(cvc4_add_unit_test is_white name output_dir)
   target_link_libraries(${name} main-test)
   target_include_directories(${name} PRIVATE ${CxxTest_INCLUDE_DIR})
   target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
+  if(USE_LFSC)
+    # We don't link against LFSC, because CVC4 is already linked against it.
+    target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
+  endif()
   if(${is_white})
     target_compile_options(${name} PRIVATE -fno-access-control)
   endif()
diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h
index 9089cee5f..fa7721f97 100644
--- a/test/unit/proof/er_proof_black.h
+++ b/test/unit/proof/er_proof_black.h
@@ -20,14 +20,27 @@
 #include <cctype>
 #include <iostream>
 #include <iterator>
+#include <string>
 #include <unordered_map>
 #include <vector>
 
+#include "base/configuration_private.h"
 #include "proof/clause_id.h"
 #include "proof/er/er_proof.h"
 #include "prop/sat_solver_types.h"
 #include "utils.h"
 
+#if IS_LFSC_BUILD
+#include "lfscc.h"
+
+namespace CVC4 {
+namespace proof {
+extern const char* const plf_signatures;
+}  // namespace proof
+}  // namespace CVC4
+#endif
+
+
 using namespace CVC4;
 using namespace CVC4::proof::er;
 using namespace CVC4::prop;
@@ -291,12 +304,12 @@ void ErProofBlack::testErTraceCheckOutput()
   pf.outputAsLfsc(lfsc);
 
   std::string out = R"EOF(
-    (decl_rat_elimination_def
+    (decl_definition
       (neg bb.v0)
       cln
       (\ er.v4
       (\ er.def4
-        (clausify_rat_elimination_def _ _ _ er.def4 _ _
+        (clausify_definition _ _ _ er.def4 _
           (\ er.c9
           (\ er.c10
           (\ er.cnf4
@@ -414,63 +427,38 @@ void ErProofBlack::testErTraceCheckOutputMedium()
           SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
   ErProof pf(clauses, usedIds, std::move(tc));
 
-  std::ostringstream lfsc;
-  pf.outputAsLfsc(lfsc);
+  std::ostringstream actual_pf_body;
+  pf.outputAsLfsc(actual_pf_body);
+
+#if IS_LFSC_BUILD
+  std::string pf_header = R"EOF(
+    (check
+      (% bb.v0 var
+      (% bb.v1 var
+      (% bb.v2 var
+      (% bb.v3 var
+        (% bb.pb1 (holds (clc (pos bb.v0) (clc (pos bb.v1) (clc (neg bb.v2) cln))))
+        (% bb.pb2 (holds (clc (neg bb.v0) (clc (neg bb.v1) (clc (pos bb.v2) cln))))
+        (% bb.pb3 (holds (clc (pos bb.v1) (clc (pos bb.v2) (clc (neg bb.v3) cln))))
+        (% bb.pb4 (holds (clc (neg bb.v1) (clc (neg bb.v2) (clc (pos bb.v3) cln))))
+        (% bb.pb5 (holds (clc (neg bb.v0) (clc (neg bb.v2) (clc (neg bb.v3) cln))))
+        (% bb.pb6 (holds (clc (pos bb.v0) (clc (pos bb.v2) (clc (pos bb.v3) cln))))
+        (% bb.pb7 (holds (clc (neg bb.v0) (clc (pos bb.v1) (clc (pos bb.v3) cln))))
+        (% bb.pb8 (holds (clc (pos bb.v0) (clc (neg bb.v1) (clc (neg bb.v3) cln))))
+          (: (holds cln)
+    )EOF";
 
-  std::string out = R"EOF(
-    (decl_rat_elimination_def
-      (neg bb.v0)
-      (clc (pos bb.v1) (clc (pos bb.v3) cln))
-      (\ er.v4
-      (\ er.def4
-    (decl_rat_elimination_def
-      (pos bb.v2)
-      cln
-      (\ er.v5
-      (\ er.def5
-        (clausify_rat_elimination_def _ _ _ er.def4 _ _
-          (\ er.c9
-          (\ er.c10
-          (\ er.cnf4
-        (clausify_rat_elimination_def _ _ _ er.def5 _ _
-          (\ er.c13
-          (\ er.c14
-          (\ er.cnf5
-            (cnfc_unroll _ _ er.cnf4
-              (\ er.c11
-              (\ er.cnf4.u1
-            (cnfc_unroll _ _ er.cnf4.u1
-              (\ er.c12
-              (\ er.cnf4.u2
-                (satlem_simplify _ _ _
-                  (R _ _ (R _ _ (Q _ _ (Q _ _ er.c11 bb.pb1 bb.v0)
-                    er.c10 er.v4)
-                    bb.pb7 bb.v0)
-                    bb.pb4 bb.v1) (\ er.c15
-                (satlem_simplify _ _ _
-                  (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c16
-                (satlem_simplify _ _ _
-                  (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c17
-                (satlem_simplify _ _ _
-                  (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c18
-                (satlem_simplify _ _ _
-                  (R _ _ (Q _ _ bb.pb3 er.c17 bb.v3) er.c18 bb.v2) (\ er.c19
-                (satlem_simplify _ _ _
-                  (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c17 bb.v2) er.c16 bb.v3)
-                      er.c19 bb.v1) (\ er.c20
-                  er.c20 ; (holds cln)
-              ))))))))))))
-            )))
-            )))
-          )))
-        )
-          )))
-        )
-      ))
-    )
-      ))
+  std::string pf_footer = R"EOF(
+          )
+        ))))))))
+      ))))
     )
     )EOF";
 
-  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out));
+  std::stringstream actual_pf;
+  actual_pf << proof::plf_signatures << pf_header << actual_pf_body.str() << pf_footer;
+
+  lfscc_init();
+  lfscc_check_file(actual_pf, false, false, false, false, false, false, false);
+#endif
 }