diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-13 13:21:24 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-13 13:21:24 -0800 |
commit | 300560dda47178cae18f5f4ad2edb381eabddb30 (patch) | |
tree | 17105907162c56850f0122e0b56a8ab7574b06f6 /test | |
parent | c652449ac9f4a54fc8f37796f0bff3960434cf40 (diff) |
LFSC LRAT Output (#2787)
* LFSC ouput & unit test
* Renamed lrat unit test file
* s/DRAT/LRAT/
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
1. Extracted a filter whitespace function.
2. Added @param annotations.
* Addressing Yoni's comments
Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/proof/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/proof/lrat_proof_black.h | 113 |
2 files changed, 114 insertions, 0 deletions
diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt index 8d76644dc..00c893bdb 100644 --- a/test/unit/proof/CMakeLists.txt +++ b/test/unit/proof/CMakeLists.txt @@ -2,4 +2,5 @@ # Add unit tests cvc4_add_unit_test_black(drat_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/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h new file mode 100644 index 000000000..49d18ac53 --- /dev/null +++ b/test/unit/proof/lrat_proof_black.h @@ -0,0 +1,113 @@ +/********************* */ +/*! \file lrat_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 LRAT proof class + ** + ** In particular, tests LRAT LFSC output. + **/ + +#include <cxxtest/TestSuite.h> + +#include <algorithm> +#include <cctype> +#include <iostream> +#include <iterator> + +#include "proof/lrat/lrat_proof.h" +#include "prop/sat_solver_types.h" + +using namespace CVC4::proof::lrat; +using namespace CVC4::prop; + +class LfscProofBlack : public CxxTest::TestSuite +{ + public: + void setUp() override {} + void tearDown() override {} + + 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; + + // 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)); +} |