ErProof class with LFSC output (#2812)

* ErProof class with LFSC output

* Created a TraceCheckProof class
   * parsable from text
* Created an ErProof class
   * constructible from a TraceCheckProof
   * writable as LFSC
* A bunch of unit tests

* Reponded to Mathias's first set of comments.

Credits to Mathias for many of the fixes!

* Responed to Andres's first set, fixed tests

I accidentally deleted a "!" last time, causing stuff to fail.

* Use Configuration::isAssertionBuild

* Clarified comment

* Responded to Andres's 2nd review

* Gaurding against a memory error.
* Renaming a file.
* Aggressively unlinking temporary files.

4 files changed, 442 insertions, 19 deletions

diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt
index 00c893bdb..315c78d6f 100644
--- a/test/unit/proof/CMakeLists.txt
+++ b/test/unit/proof/CMakeLists.txt
@@ -2,5 +2,6 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(drat_proof_black proof)
+cvc4_add_unit_test_black(er_proof_black proof)
 cvc4_add_unit_test_black(lrat_proof_black proof)
 cvc4_add_unit_test_black(lfsc_proof_printer_black proof)
diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h
new file mode 100644
index 000000000..1620bb113
--- /dev/null
+++ b/test/unit/proof/er_proof_black.h
@@ -0,0 +1,406 @@
+/*********************                                                        */
+/*! \file er_proof_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the ER proof class
+ **
+ ** In particular, tests TRACECHECK parsing and ER LFSC output.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <algorithm>
+#include <cctype>
+#include <iostream>
+#include <iterator>
+#include <vector>
+
+#include "proof/clause_id.h"
+#include "proof/er/er_proof.h"
+#include "prop/sat_solver_types.h"
+#include "utils.h"
+
+using namespace CVC4;
+using namespace CVC4::proof::er;
+using namespace CVC4::prop;
+
+class ErProofBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override {}
+  void tearDown() override {}
+
+  void testTraceCheckParse1Line();
+  void testTraceCheckParse5Lines();
+  void testErTraceCheckParse();
+  void testErTraceCheckOutput();
+  void testErTraceCheckOutputMedium();
+};
+
+void ErProofBlack::testTraceCheckParse1Line()
+{
+  std::string tracecheckText = "1 -2 3 0 4 2 0\n";
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof pf = TraceCheckProof::fromText(stream);
+  TS_ASSERT_EQUALS(pf.d_lines.size(), 1);
+
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_idx, 1);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause.size(), 2);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[0], SatLiteral(1, true));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[1], SatLiteral(2, false));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain.size(), 2);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain[0], 4);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain[1], 2);
+}
+
+void ErProofBlack::testTraceCheckParse5Lines()
+{
+  std::string tracecheckText =
+      "1 1 -2 3 0 0\n"
+      "2 -1 0 0\n"
+      "3 2 0 0\n"
+      "4 -3 0 0\n"
+      "5 0 1 2 4 3 0\n";
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof pf = TraceCheckProof::fromText(stream);
+  TS_ASSERT_EQUALS(pf.d_lines.size(), 5);
+
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_idx, 1);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_idx, 5);
+
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause.size(), 3);
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[0], SatLiteral(0, false));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[1], SatLiteral(1, true));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[2], SatLiteral(2, false));
+  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain.size(), 0);
+
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain.size(), 4);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[0], 1);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[1], 2);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[2], 4);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[3], 3);
+  TS_ASSERT_EQUALS(pf.d_lines[4].d_clause.size(), 0);
+}
+
+void ErProofBlack::testErTraceCheckParse()
+{
+  std::string tracecheckText =
+      "1  1  2 -3 0 0\n"
+      "2 -1 -2  3 0 0\n"
+      "3  2  3 -4 0 0\n"
+      "4 -2 -3  4 0 0\n"
+      "5 -1 -3 -4 0 0\n"
+      "6  1  3  4 0 0\n"
+      "7 -1  2  4 0 0\n"
+      "8  1 -2 -4 0 0\n"
+      "9 5 0 0\n"
+      "10 5 1 0 0\n"
+      "11 4 5 2 0 10 7 0\n"
+      "12 -4 5 -3 0 10 5 0\n"
+      "13 3 5 -2 0 10 2 0\n"
+      "14 -2 -4 0 2 5 8 0\n"
+      "15 4 3 0 7 2 6 0\n"
+      "16 2 -3 0 7 5 1 0\n"
+      "17 2 0 3 15 16 0\n"
+      "18 0 4 15 14 17 0\n";
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof tc = TraceCheckProof::fromText(stream);
+
+  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
+  usedClauses.emplace_back(
+      1,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
+  usedClauses.emplace_back(
+      2,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
+  usedClauses.emplace_back(
+      3,
+      std::vector<SatLiteral>{
+          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      4,
+      std::vector<SatLiteral>{
+          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      5,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      6,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      7,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      8,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
+  ErProof pf(usedClauses, std::move(tc));
+
+  TS_ASSERT_EQUALS(pf.getInputClauseIds()[0], 1);
+  TS_ASSERT_EQUALS(pf.getInputClauseIds()[7], 8);
+
+  TS_ASSERT_EQUALS(pf.getDefinitions().size(), 1)
+  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_newVariable, SatVariable(4));
+  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_oldLiteral, SatLiteral(0, true));
+  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_otherLiterals.size(), 0);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines.size(), 18);
+
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_idx, 1);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_idx, 17);
+
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause.size(), 3);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[0], SatLiteral(0, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[1], SatLiteral(1, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[2], SatLiteral(2, true));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_chain.size(), 0);
+
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause.size(), 1);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause[0], SatLiteral(1, false));
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain.size(), 3);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[0], 3);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[1], 15);
+  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[2], 16);
+}
+
+void ErProofBlack::testErTraceCheckOutput()
+{
+  std::string tracecheckText =
+      "1  1  2 -3 0 0\n"
+      "2 -1 -2  3 0 0\n"
+      "3  2  3 -4 0 0\n"
+      "4 -2 -3  4 0 0\n"
+      "5 -1 -3 -4 0 0\n"
+      "6  1  3  4 0 0\n"
+      "7 -1  2  4 0 0\n"
+      "8  1 -2 -4 0 0\n"
+      "9 5 0 0\n"
+      "10 5 1 0 0\n"
+      "11 4 5 2 0 10 7 0\n"
+      "12 -4 5 -3 0 10 5 0\n"
+      "13 3 5 -2 0 10 2 0\n"
+      "14 -2 -4 0 2 5 8 0\n"
+      "15 4 3 0 7 2 6 0\n"
+      "16 2 -3 0 7 5 1 0\n"
+      "17 2 0 3 15 16 0\n"
+      "18 0 4 15 14 17 0\n";
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof tc = TraceCheckProof::fromText(stream);
+
+  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
+  usedClauses.emplace_back(
+      1,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
+  usedClauses.emplace_back(
+      2,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
+  usedClauses.emplace_back(
+      3,
+      std::vector<SatLiteral>{
+          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      4,
+      std::vector<SatLiteral>{
+          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      5,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      6,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      7,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      8,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
+  ErProof pf(usedClauses, std::move(tc));
+
+  std::ostringstream lfsc;
+  pf.outputAsLfsc(lfsc);
+
+  std::string out = R"EOF(
+    (decl_rat_elimination_def
+      (neg bb.v0)
+      cln
+      (\ er.v4
+      (\ er.def4
+        (clausify_rat_elimination_def _ _ _ er.def4 _ _
+          (\ er.c9
+          (\ er.c10
+          (\ er.cnf4
+            (satlem_simplify _ _ _
+              (R _ _ er.c10 bb.pb7 bb.v0) (\ er.c11
+            (satlem_simplify _ _ _
+              (R _ _ er.c10 bb.pb5 bb.v0) (\ er.c12
+            (satlem_simplify _ _ _
+              (R _ _ er.c10 bb.pb2 bb.v0) (\ er.c13
+            (satlem_simplify _ _ _
+              (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c14
+            (satlem_simplify _ _ _
+              (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c15
+            (satlem_simplify _ _ _
+              (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c16
+            (satlem_simplify _ _ _
+              (R _ _ (Q _ _ bb.pb3 er.c15 bb.v3) er.c16 bb.v2) (\ er.c17
+            (satlem_simplify _ _ _
+              (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c15 bb.v2) er.c14 bb.v3)
+                  er.c17 bb.v1) (\ er.c18
+              er.c18 ; (holds cln)
+            ))))))))))))))))
+          )))
+        )
+      ))
+    )
+    )EOF";
+
+  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out));
+}
+
+/**
+ * This proof has been specially constructed to stress-test the proof
+ * machinery, while still being short. It's a bit meandering...
+ */
+void ErProofBlack::testErTraceCheckOutputMedium()
+{
+  std::string tracecheckText =
+      "1  1  2 -3 0 0\n"
+      "2 -1 -2  3 0 0\n"
+      "3  2  3 -4 0 0\n"
+      "4 -2 -3  4 0 0\n"
+      "5 -1 -3 -4 0 0\n"
+      "6  1  3  4 0 0\n"
+      "7 -1  2  4 0 0\n"
+      "8  1 -2 -4 0 0\n"
+
+      "9  5  2  4 0 0\n"    // Definition with 2 other variables
+      "10 5  1  0 0\n"
+      "11 2 -5 -1 0 0\n"
+      "12 4 -5 -1 0 0\n"
+
+      "13 6  0 0\n"       // Definition with no other variables
+      "14 6  -3  0 0\n"
+
+      "15 -3 4 0 11 1 10 7 4 0\n" // Chain w/ both def. and input clauses
+
+      "16 -2 -4 0 2 5 8 0\n" // The useful bit of the proof
+      "17 4 3 0 7 2 6 0\n"
+      "18 2 -3 0 7 5 1 0\n"
+      "19 2 0 3 17 18 0\n"
+      "20 0 4 17 16 19 0\n";
+
+  std::istringstream stream(tracecheckText);
+  TraceCheckProof tc = TraceCheckProof::fromText(stream);
+
+  std::vector<std::pair<ClauseId, SatClause>> usedClauses;
+  usedClauses.emplace_back(
+      1,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
+  usedClauses.emplace_back(
+      2,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
+  usedClauses.emplace_back(
+      3,
+      std::vector<SatLiteral>{
+          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      4,
+      std::vector<SatLiteral>{
+          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      5,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+  usedClauses.emplace_back(
+      6,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      7,
+      std::vector<SatLiteral>{
+          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
+  usedClauses.emplace_back(
+      8,
+      std::vector<SatLiteral>{
+          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
+  ErProof pf(usedClauses, std::move(tc));
+
+  std::ostringstream lfsc;
+  pf.outputAsLfsc(lfsc);
+
+  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)
+              ))))))))))))
+            )))
+            )))
+          )))
+        )
+          )))
+        )
+      ))
+    )
+      ))
+    )
+    )EOF";
+
+  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out));
+}
diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h
index 49d18ac53..48f571841 100644
--- a/test/unit/proof/lrat_proof_black.h
+++ b/test/unit/proof/lrat_proof_black.h
@@ -16,13 +16,11 @@
 
 #include <cxxtest/TestSuite.h>
 
-#include <algorithm>
-#include <cctype>
 #include <iostream>
-#include <iterator>
 
 #include "proof/lrat/lrat_proof.h"
 #include "prop/sat_solver_types.h"
+#include "utils.h"
 
 using namespace CVC4::proof::lrat;
 using namespace CVC4::prop;
@@ -36,22 +34,6 @@ class LfscProofBlack : public CxxTest::TestSuite
   void testOutputAsLfsc();
 };
 
-/**
- * Creates a new stream with whitespace removed.
- *
- * @param s the source string
- *
- * @return a string without whitespace
- */
-std::string filterWhitespace(const std::string& s)
-{
-  std::string out;
-  std::copy_if(s.cbegin(), s.cend(), std::inserter(out, out.end()), [](char c) {
-    return !std::isspace(c);
-  });
-  return out;
-}
-
 void LfscProofBlack::testOutputAsLfsc()
 {
   std::vector<std::unique_ptr<LratInstruction>> instructions;
diff --git a/test/unit/proof/utils.h b/test/unit/proof/utils.h
new file mode 100644
index 000000000..19b24f4c3
--- /dev/null
+++ b/test/unit/proof/utils.h
@@ -0,0 +1,34 @@
+/*********************                                                        */
+/*! \file utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utilities for proof testing
+ **/
+
+#include <algorithm>
+#include <string>
+#include <cctype>
+#include <iterator>
+
+/**
+ * Creates a new stream with whitespace removed.
+ *
+ * @param s the source string
+ *
+ * @return a string without whitespace
+ */
+std::string filterWhitespace(const std::string& s)
+{
+  std::string out;
+  std::copy_if(s.cbegin(), s.cend(), std::inserter(out, out.end()), [](char c) {
+    return !std::isspace(c);
+  });
+  return out;
+}