summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress0/bug217.smt21
-rw-r--r--test/regress/regress0/options/invalid_option_inc_proofs.smt26
-rw-r--r--test/regress/regress1/bv/bench_38.delta.smt22
-rw-r--r--test/regress/regress1/non-fatal-errors.smt24
-rw-r--r--test/regress/regress1/quantifiers/dump-inst-proof.smt28
-rw-r--r--test/unit/CMakeLists.txt1
-rw-r--r--test/unit/proof/CMakeLists.txt7
-rw-r--r--test/unit/proof/drat_proof_black.h187
-rw-r--r--test/unit/proof/er_proof_black.h464
-rw-r--r--test/unit/proof/lfsc_proof_printer_black.h118
-rw-r--r--test/unit/proof/lrat_proof_black.h97
-rw-r--r--test/unit/proof/utils.h34
-rw-r--r--test/unit/prop/cnf_stream_white.h60
-rw-r--r--test/unit/theory/theory_engine_white.h7
-rw-r--r--test/unit/theory/theory_white.h9
16 files changed, 32 insertions, 976 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4de32a426..1a33ee3a5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -622,7 +622,6 @@ set(regress_0_tests
regress0/nl/very-easy-sat.smt2
regress0/nl/very-simple-unsat.smt2
regress0/options/invalid_dump.smt2
- regress0/options/invalid_option_inc_proofs.smt2
regress0/opt-abd-no-use.smt2
regress0/parallel-let.smt2
regress0/parser/as.smt2
@@ -872,7 +871,7 @@ set(regress_0_tests
regress0/seq/seq-nth.smt2
regress0/seq/seq-nth-uf.smt2
regress0/seq/seq-nth-uf-z.smt2
- regress0/seq/seq-nth-undef.smt2
+ regress0/seq/seq-nth-undef.smt2
regress0/seq/seq-rewrites.smt2
regress0/sets/abt-min.smt2
regress0/sets/abt-te-exh.smt2
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 30c87333e..4d2e828b5 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --fewer-preprocessing-holes
; EXPECT: unsat
(set-logic QF_UF)
(set-info :status unsat)
diff --git a/test/regress/regress0/options/invalid_option_inc_proofs.smt2 b/test/regress/regress0/options/invalid_option_inc_proofs.smt2
deleted file mode 100644
index f63dbd27f..000000000
--- a/test/regress/regress0/options/invalid_option_inc_proofs.smt2
+++ /dev/null
@@ -1,6 +0,0 @@
-; REQUIRES: proof
-; COMMAND-LINE: --incremental --proof
-; EXPECT: (error "Error in option parsing: --incremental is not supported with proofs")
-; EXIT: 1
-(set-logic QF_BV)
-(check-sat)
diff --git a/test/regress/regress1/bv/bench_38.delta.smt2 b/test/regress/regress1/bv/bench_38.delta.smt2
index 760614348..3f809716a 100644
--- a/test/regress/regress1/bv/bench_38.delta.smt2
+++ b/test/regress/regress1/bv/bench_38.delta.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fewer-preprocessing-holes --check-proof --quiet
+; COMMAND-LINE: --quiet
; EXPECT: unsat
(set-logic QF_BV)
(declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress1/non-fatal-errors.smt2 b/test/regress/regress1/non-fatal-errors.smt2
index 1e1865883..ec3d02927 100644
--- a/test/regress/regress1/non-fatal-errors.smt2
+++ b/test/regress/regress1/non-fatal-errors.smt2
@@ -2,11 +2,10 @@
; EXPECT: success
; EXPECT: success
; EXPECT: success
+; EXPECT: unsupported
; EXPECT: success
; EXPECT: success
; EXPECT: success
-; EXPECT: success
-; EXPECT: (error "")
; EXPECT: (error "")
; EXPECT: (error "")
; EXPECT: (error "")
@@ -22,7 +21,6 @@
(declare-fun p () Bool)
(get-unsat-core)
(get-value (p))
-(get-proof)
(get-model)
(get-assignment)
(assert true)
diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index 9edc4df2b..f900e78a9 100644
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,5 +1,5 @@
; REQUIRES: proof
-; COMMAND-LINE: --dump-instantiations --proof --print-inst-full
+; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full
; EXPECT: unsat
; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) )
; EXPECT: ( 2 )
@@ -21,7 +21,7 @@
(assert (forall ((x Int)) (or (not (S x)) (not (Q x)))))
(assert (and (not (R 0)) (not (R 10)) (not (S 1)) (not (P 2))))
(assert (S 2))
-; This tests that --proof minimizes the instantiations printed out.
-; This regression should require only the 2 instantiations above, but
-; may try more.
+; This tests that --produce-unsat-cores minimizes the instantiations
+; printed out. This regression should require only the 2
+; instantiations above, but may try more.
(check-sat)
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index bd7c1ea22..bd7029c54 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -107,7 +107,6 @@ add_subdirectory(expr)
add_subdirectory(main)
add_subdirectory(parser)
add_subdirectory(prop)
-add_subdirectory(proof)
add_subdirectory(theory)
add_subdirectory(preprocessing)
add_subdirectory(util)
diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt
deleted file mode 100644
index 315c78d6f..000000000
--- a/test/unit/proof/CMakeLists.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-#-----------------------------------------------------------------------------#
-# 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/drat_proof_black.h b/test/unit/proof/drat_proof_black.h
deleted file mode 100644
index 4b593a588..000000000
--- a/test/unit/proof/drat_proof_black.h
+++ /dev/null
@@ -1,187 +0,0 @@
-/********************* */
-/*! \file drat_proof_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Alex Ozdemir, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 DRAT proof class
- **
- ** In particular, tests DRAT binary parsing.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <cctype>
-
-#include "proof/drat/drat_proof.h"
-
-using namespace CVC4::proof::drat;
-
-class DratProofBlack : public CxxTest::TestSuite
-{
- public:
- void setUp() override {}
- void tearDown() override {}
-
- void testParseOneAdd();
- void testParseOneMediumAdd();
- void testParseOneBigAdd();
- void testParseLiteralIsTooBig();
- void testParseLiteralOverflow();
- void testParseClauseOverflow();
-
- void testParseTwo();
-
- void testOutputTwoAsText();
- void testOutputTwoAsLfsc();
-};
-
-void DratProofBlack::testParseOneAdd()
-{
- // a 1;
- std::string input("a\x02\x00", 3);
- DratProof proof = DratProof::fromBinary(input);
-
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
- SatLiteral(0, false));
-}
-
-void DratProofBlack::testParseOneMediumAdd()
-{
- // a -255;
- std::string input("a\xff\x01\x00", 4);
- DratProof proof = DratProof::fromBinary(input);
-
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
- SatLiteral(126, true));
-}
-
-void DratProofBlack::testParseOneBigAdd()
-{
- // a -2199023255551;
- std::string input("a\xff\xff\xff\xff\xff\x7f\x00", 8);
- DratProof proof = DratProof::fromBinary(input);
-
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
- SatLiteral(2199023255550, true));
-}
-
-void DratProofBlack::testParseLiteralIsTooBig()
-{
- std::string input("a\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7f\x00",
- 14);
- TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
-}
-
-void DratProofBlack::testParseLiteralOverflow()
-{
- std::string input("a\x80", 2);
- TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
-}
-
-void DratProofBlack::testParseClauseOverflow()
-{
- std::string input("a\x80\x01", 3);
- TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
-}
-
-void DratProofBlack::testParseTwo()
-{
- // d -63 -8193
- // 129 -8191
- std::string input("\x64\x7f\x83\x80\x01\x00\x61\x82\x02\xff\x7f\x00", 12);
- DratProof proof = DratProof::fromBinary(input);
-
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, DELETION);
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 2);
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
- SatLiteral(62, true));
- TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[1],
- SatLiteral(8192, true));
-
- TS_ASSERT_EQUALS(proof.getInstructions()[1].d_kind, ADDITION);
- TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause.size(), 2);
- TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause[0],
- SatLiteral(128, false));
- TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause[1],
- SatLiteral(8190, true));
-}
-
-void DratProofBlack::testOutputTwoAsText()
-{
- // d -63 -8193
- // 129 -8191
- std::string input("\x64\x7f\x83\x80\x01\x00\x61\x82\x02\xff\x7f\x00", 12);
- DratProof proof = DratProof::fromBinary(input);
-
- std::ostringstream output;
- proof.outputAsText(output);
-
- std::istringstream tokens(output.str());
- std::string token;
-
- tokens >> token;
- TS_ASSERT_EQUALS(token, "d");
-
- tokens >> token;
- TS_ASSERT_EQUALS(token, "-63");
-
- tokens >> token;
- TS_ASSERT_EQUALS(token, "-8193");
-
- tokens >> token;
- TS_ASSERT_EQUALS(token, "0");
-
- tokens >> token;
- TS_ASSERT_EQUALS(token, "129");
-
- tokens >> token;
- TS_ASSERT_EQUALS(token, "-8191");
-
- tokens >> token;
- TS_ASSERT_EQUALS(token, "0");
-}
-
-void DratProofBlack::testOutputTwoAsLfsc()
-{
- // d -63 -8193
- // 129 -8191
- std::string input("\x64\x7f\x83\x80\x01\x00\x61\x82\x02\xff\x7f\x00", 12);
- DratProof proof = DratProof::fromBinary(input);
- std::ostringstream lfsc;
- proof.outputAsLfsc(lfsc, 2);
- std::ostringstream lfscWithoutWhitespace;
- for (char c : lfsc.str())
- {
- if (!std::isspace(c))
- {
- lfscWithoutWhitespace << c;
- }
- }
- std::string expectedLfsc =
- "(DRATProofd (clc (neg bb.v62) (clc (neg bb.v8192) cln))"
- "(DRATProofa (clc (pos bb.v128) (clc (neg bb.v8190) cln))"
- "DRATProofn))";
- std::ostringstream expectedLfscWithoutWhitespace;
- for (char c : expectedLfsc)
- {
- if (!std::isspace(c))
- {
- expectedLfscWithoutWhitespace << c;
- }
- }
-
- TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
- expectedLfscWithoutWhitespace.str());
-}
diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h
deleted file mode 100644
index d9178e34e..000000000
--- a/test/unit/proof/er_proof_black.h
+++ /dev/null
@@ -1,464 +0,0 @@
-/********************* */
-/*! \file er_proof_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Alex Ozdemir
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 <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;
-
-class ErProofBlack : public CxxTest::TestSuite
-{
- public:
- void setUp() override {}
- void tearDown() override {}
-
- void testTraceCheckParse1Line();
- void testTraceCheckParse5Lines();
- void testErTraceCheckParse();
- void testErTraceCheckOutput();
- void testErTraceCheckOutputMedium();
-};
-
-/**
- * @brief Add a new clause to the clause store and list of used clauses
- *
- * @param clauses the clause store
- * @param usedIds the used clauses
- * @param id the id of the new clause
- * @param clause the clause itself
- */
-void addClause(std::unordered_map<ClauseId, SatClause>& clauses,
- std::vector<ClauseId>& usedIds,
- ClauseId id,
- SatClause&& clause)
-{
- clauses.emplace(id, std::move(clause));
- usedIds.push_back(id);
-}
-
-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::unordered_map<ClauseId, SatClause> clauses;
- std::vector<ClauseId> usedIds;
- addClause(
- clauses,
- usedIds,
- 1,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
- addClause(
- clauses,
- usedIds,
- 2,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
- addClause(
- clauses,
- usedIds,
- 3,
- std::vector<SatLiteral>{
- SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
- addClause(
- clauses,
- usedIds,
- 4,
- std::vector<SatLiteral>{
- SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
- addClause(clauses,
- usedIds,
- 5,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
- addClause(
- clauses,
- usedIds,
- 6,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
- addClause(
- clauses,
- usedIds,
- 7,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
- addClause(
- clauses,
- usedIds,
- 8,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
- ErProof pf(clauses, usedIds, 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::unordered_map<ClauseId, SatClause> clauses;
- std::vector<ClauseId> usedIds;
- addClause(
- clauses,
- usedIds,
- 1,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
- addClause(
- clauses,
- usedIds,
- 2,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
- addClause(
- clauses,
- usedIds,
- 3,
- std::vector<SatLiteral>{
- SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
- addClause(
- clauses,
- usedIds,
- 4,
- std::vector<SatLiteral>{
- SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
- addClause(clauses,
- usedIds,
- 5,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
- addClause(
- clauses,
- usedIds,
- 6,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
- addClause(
- clauses,
- usedIds,
- 7,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
- addClause(
- clauses,
- usedIds,
- 8,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
- ErProof pf(clauses, usedIds, std::move(tc));
-
- std::ostringstream lfsc;
- pf.outputAsLfsc(lfsc);
-
- std::string out = R"EOF(
- (decl_definition
- (neg bb.v0)
- cln
- (\ er.v4
- (\ er.def4
- (clausify_definition _ _ _ 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::unordered_map<ClauseId, SatClause> clauses;
- std::vector<ClauseId> usedIds;
- addClause(
- clauses,
- usedIds,
- 1,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
- addClause(
- clauses,
- usedIds,
- 2,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
- addClause(
- clauses,
- usedIds,
- 3,
- std::vector<SatLiteral>{
- SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
- addClause(
- clauses,
- usedIds,
- 4,
- std::vector<SatLiteral>{
- SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
- addClause(clauses,
- usedIds,
- 5,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
- addClause(
- clauses,
- usedIds,
- 6,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
- addClause(
- clauses,
- usedIds,
- 7,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
- addClause(
- clauses,
- usedIds,
- 8,
- std::vector<SatLiteral>{
- SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
- ErProof pf(clauses, usedIds, std::move(tc));
-
- 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 pf_footer = R"EOF(
- )
- ))))))))
- ))))
- )
- )EOF";
-
- 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
-}
diff --git a/test/unit/proof/lfsc_proof_printer_black.h b/test/unit/proof/lfsc_proof_printer_black.h
deleted file mode 100644
index 74fda4996..000000000
--- a/test/unit/proof/lfsc_proof_printer_black.h
+++ /dev/null
@@ -1,118 +0,0 @@
-/********************* */
-/*! \file lfsc_proof_printer_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Alex Ozdemir
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 LFSC proof printing
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "proof/lfsc_proof_printer.h"
-#include "prop/sat_solver_types.h"
-#include "proof/clause_id.h"
-
-using namespace CVC4::proof;
-using namespace CVC4::prop;
-
-class LfscProofPrinterBlack : public CxxTest::TestSuite
-{
- public:
- void setUp() override {}
- void tearDown() override {}
-
- void testPrintClause();
- void testPrintSatInputProof();
- void testPrintCMapProof();
-};
-
-void LfscProofPrinterBlack::testPrintClause()
-{
- SatClause clause{
- SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, false)};
- std::ostringstream lfsc;
-
- LFSCProofPrinter::printSatClause(clause, lfsc, "");
-
- std::string expectedLfsc =
- "(clc (pos .v0) "
- "(clc (neg .v1) "
- "(clc (pos .v3) "
- "cln)))";
-
- TS_ASSERT_EQUALS(lfsc.str(), expectedLfsc);
-}
-
-void LfscProofPrinterBlack::testPrintSatInputProof()
-{
- std::vector<CVC4::ClauseId> ids{2, 40, 3};
- std::ostringstream lfsc;
-
- LFSCProofPrinter::printSatInputProof(ids, lfsc, "");
-
- std::string expectedLfsc =
- "(cnfc_proof _ _ _ .pb2 "
- "(cnfc_proof _ _ _ .pb40 "
- "(cnfc_proof _ _ _ .pb3 "
- "cnfn_proof)))";
-
- std::ostringstream lfscWithoutWhitespace;
- for (char c : lfsc.str())
- {
- if (!std::isspace(c))
- {
- lfscWithoutWhitespace << c;
- }
- }
- std::ostringstream expectedLfscWithoutWhitespace;
- for (char c : expectedLfsc)
- {
- if (!std::isspace(c))
- {
- expectedLfscWithoutWhitespace << c;
- }
- }
-
- TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
- expectedLfscWithoutWhitespace.str());
-}
-
-void LfscProofPrinterBlack::testPrintCMapProof()
-{
- std::vector<CVC4::ClauseId> ids{2, 40, 3};
- std::ostringstream lfsc;
-
- LFSCProofPrinter::printCMapProof(ids, lfsc, "");
-
- std::string expectedLfsc =
- "(CMapc_proof 1 _ _ _ .pb2 "
- "(CMapc_proof 2 _ _ _ .pb40 "
- "(CMapc_proof 3 _ _ _ .pb3 "
- "CMapn_proof)))";
-
- std::ostringstream lfscWithoutWhitespace;
- for (char c : lfsc.str())
- {
- if (!std::isspace(c))
- {
- lfscWithoutWhitespace << c;
- }
- }
- std::ostringstream expectedLfscWithoutWhitespace;
- for (char c : expectedLfsc)
- {
- if (!std::isspace(c))
- {
- expectedLfscWithoutWhitespace << c;
- }
- }
-
- TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
- expectedLfscWithoutWhitespace.str());
-}
diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h
deleted file mode 100644
index 8d91fee33..000000000
--- a/test/unit/proof/lrat_proof_black.h
+++ /dev/null
@@ -1,97 +0,0 @@
-/********************* */
-/*! \file lrat_proof_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Alex Ozdemir, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 LRAT proof class
- **
- ** In particular, tests LRAT LFSC output.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-
-#include "proof/lrat/lrat_proof.h"
-#include "prop/sat_solver_types.h"
-#include "utils.h"
-
-using namespace CVC4;
-using namespace CVC4::proof::lrat;
-using namespace CVC4::prop;
-
-class LratProofBlack : public CxxTest::TestSuite
-{
- public:
- void setUp() override {}
- void tearDown() override {}
-
- void testOutputAsLfsc();
-};
-
-void LratProofBlack::testOutputAsLfsc()
-{
- std::vector<std::unique_ptr<LratInstruction>> instructions;
-
- // 6 d 1 2
- std::vector<ClauseIdx> clausesToDelete{1, 2};
- std::unique_ptr<LratDeletion> deletion = std::unique_ptr<LratDeletion>(
- new LratDeletion(6, std::move(clausesToDelete)));
- instructions.push_back(std::move(deletion));
-
- // 7 1 2 0 5 2 0
- std::vector<SatLiteral> firstAddedClause{SatLiteral(1, false),
- SatLiteral(2, false)};
- LratUPTrace firstTrace{5, 2};
- std::vector<std::pair<ClauseIdx, LratUPTrace>> firstHints;
- std::unique_ptr<LratAddition> add1 =
- std::unique_ptr<LratAddition>(new LratAddition(
- 7, std::move(firstAddedClause), std::move(firstTrace), firstHints));
- instructions.push_back(std::move(add1));
-
- // 8 2 0 -1 3 -5 2 0
- std::vector<SatLiteral> secondAddedClause{SatLiteral(2, false)};
- LratUPTrace secondTrace;
- std::vector<std::pair<ClauseIdx, LratUPTrace>> secondHints;
- LratUPTrace secondHints0Trace{3};
- secondHints.emplace_back(1, secondHints0Trace);
- LratUPTrace secondHints1Trace{2};
- secondHints.emplace_back(5, secondHints1Trace);
- std::unique_ptr<LratAddition> add2 = std::unique_ptr<LratAddition>(
- new LratAddition(8,
- std::move(secondAddedClause),
- std::move(secondTrace),
- secondHints));
- instructions.push_back(std::move(add2));
-
- LratProof proof(std::move(instructions));
-
- std::ostringstream lfsc;
- proof.outputAsLfsc(lfsc);
-
- // 6 d 1 2
- // 7 1 2 0 5 2 0
- // 8 2 0 -1 3 -5 2 0
- std::string expectedLfsc =
- "(LRATProofd (CIListc 1 (CIListc 2 CIListn)) "
- "(LRATProofa 7 "
- " (clc (pos bb.v1) (clc (pos bb.v2) cln))"
- " (Tracec 5 (Tracec 2 Tracen))"
- " RATHintsn "
- "(LRATProofa 8 "
- " (clc (pos bb.v2) cln)"
- " Tracen "
- " (RATHintsc 1 (Tracec 3 Tracen)"
- " (RATHintsc 5 (Tracec 2 Tracen)"
- " RATHintsn)) "
- "LRATProofn)))";
-
- TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()),
- filterWhitespace(expectedLfsc));
-}
diff --git a/test/unit/proof/utils.h b/test/unit/proof/utils.h
deleted file mode 100644
index 3db6e2171..000000000
--- a/test/unit/proof/utils.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/********************* */
-/*! \file utils.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Alex Ozdemir
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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;
-}
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index f0253fdbf..33fc15674 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -174,8 +174,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c),
- false, false, RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
@@ -189,26 +189,27 @@ class CnfStreamWhite : public CxxTest::TestSuite {
Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
d_cnfStream->convertAndAssert(
d_nodeManager->mkNode(
- kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b),
+ kind::IMPLIES,
+ d_nodeManager->mkNode(kind::AND, a, b),
d_nodeManager->mkNode(
- kind::EQUAL, d_nodeManager->mkNode(kind::OR, c, d),
+ kind::EQUAL,
+ d_nodeManager->mkNode(kind::OR, c, d),
d_nodeManager->mkNode(kind::NOT,
d_nodeManager->mkNode(kind::XOR, e, f)))),
- false, false, RULE_INVALID, Node::null());
+ false,
+ false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
void testTrue() {
NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false,
- RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
void testFalse() {
NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false,
- RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
@@ -216,8 +217,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::EQUAL, a, b), false,
- false, RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::EQUAL, a, b), false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
@@ -225,33 +226,16 @@ class CnfStreamWhite : public CxxTest::TestSuite {
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES, a, b),
- false, false, RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
- // ITEs should be removed before going to CNF
- // void testIte() {
- // NodeManagerScope nms(d_nodeManager);
- // d_cnfStream->convertAndAssert(
- // d_nodeManager->mkNode(
- // kind::EQUAL,
- // d_nodeManager->mkNode(
- // kind::ITE,
- // d_nodeManager->mkVar(d_nodeManager->booleanType()),
- // d_nodeManager->mkVar(d_nodeManager->integerType()),
- // d_nodeManager->mkVar(d_nodeManager->integerType())
- // ),
- // d_nodeManager->mkVar(d_nodeManager->integerType())
- // ), false, false, RULE_INVALID, Node::null());
- //
- //}
-
void testNot() {
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::NOT, a), false,
- false, RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::NOT, a), false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
@@ -260,8 +244,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::OR, a, b, c),
- false, false, RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::OR, a, b, c), false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
@@ -269,10 +253,10 @@ class CnfStreamWhite : public CxxTest::TestSuite {
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(a, false, false, RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(a, false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
d_satSolver->reset();
- d_cnfStream->convertAndAssert(b, false, false, RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(b, false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
@@ -280,8 +264,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
NodeManagerScope nms(d_nodeManager);
Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::XOR, a, b), false,
- false, RULE_INVALID, Node::null());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::XOR, a, b), false, false);
TS_ASSERT(d_satSolver->addClauseCalled());
}
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index a67d0aeb2..ae4264aa2 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -41,7 +41,6 @@
#include "theory/theory_rewriter.h"
#include "theory/valuation.h"
#include "util/integer.h"
-#include "util/proof.h"
#include "util/rational.h"
using namespace CVC4;
@@ -55,13 +54,9 @@ using namespace CVC4::theory::bv;
using namespace std;
class FakeOutputChannel : public OutputChannel {
- void conflict(TNode n, std::unique_ptr<Proof> pf) override
- {
- Unimplemented();
- }
+ void conflict(TNode n) override { Unimplemented(); }
bool propagate(TNode n) override { Unimplemented(); }
LemmaStatus lemma(TNode n,
- ProofRule rule,
LemmaProperty p = LemmaProperty::NONE) override
{
Unimplemented();
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 9693000a3..e90bd56a2 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -26,7 +26,6 @@
#include "smt/smt_engine_scope.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
-#include "util/proof.h"
#include "util/resource_manager.h"
using namespace CVC4;
@@ -48,10 +47,7 @@ class TestOutputChannel : public OutputChannel {
~TestOutputChannel() override {}
void safePoint(ResourceManager::Resource r) override {}
- void conflict(TNode n, std::unique_ptr<Proof> pf) override
- {
- push(CONFLICT, n);
- }
+ void conflict(TNode n) override { push(CONFLICT, n); }
bool propagate(TNode n) override {
push(PROPAGATE, n);
@@ -59,7 +55,6 @@ class TestOutputChannel : public OutputChannel {
}
LemmaStatus lemma(TNode n,
- ProofRule rule,
LemmaProperty p = LemmaProperty::NONE) override
{
push(LEMMA, n);
@@ -298,7 +293,7 @@ class TheoryBlack : public CxxTest::TestSuite {
void testOutputChannel() {
Node n = atom0.orNode(atom1);
- d_outputChannel.lemma(n, RULE_INVALID);
+ d_outputChannel.lemma(n);
d_outputChannel.split(atom0);
Node s = atom0.orNode(atom0.notNode());
TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback