set(core_signature_files
sat.plf
+ er.plf
smt.plf
th_base.plf
+ lrat.plf
+ drat.plf
th_arrays.plf
th_bv.plf
th_bv_bitblast.plf
return IS_CRYPTOMINISAT_BUILD;
}
+bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; }
+
bool Configuration::isBuiltWithReadline() {
return IS_READLINE_BUILD;
}
static bool isBuiltWithCryptominisat();
+ static bool isBuiltWithDrat2Er();
+
static bool isBuiltWithReadline();
static bool isBuiltWithLfsc();
category = "expert"
long = "bv-proof-format=MODE"
type = "CVC4::theory::bv::BvProofFormat"
- default = "CVC4::theory::bv::BITVECTOR_PROOF_LRAT"
+ default = "CVC4::theory::bv::BITVECTOR_PROOF_ER"
handler = "stringToBvProofFormat"
predicates = ["satSolverEnabledBuild"]
includes = ["options/bv_bitblast_mode.h"]
{
#ifdef CVC4_PROOF
if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
- && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT)
+ && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT
+ && options::bvSatSolver() != theory::bv::SAT_SOLVER_CRYPTOMINISAT)
{
throw OptionException(
- "Eager BV proofs only supported when minisat is used");
+ "Eager BV proofs only supported when MiniSat or CryptoMiniSat is used");
}
#else
if(value) {
print_config_cond("glpk", Configuration::isBuiltWithGlpk());
print_config_cond("cadical", Configuration::isBuiltWithCadical());
print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
+ print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er());
print_config_cond("gmp", Configuration::isBuiltWithGmp());
print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
print_config_cond("readline", Configuration::isBuiltWithReadline());
}
}
+void BitVectorProof::printEmptyClauseProof(std::ostream& os,
+ std::ostream& paren)
+{
+ Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+ "the BV theory should only be proving bottom directly in the eager "
+ "bitblasting mode");
+}
+
void BitVectorProof::printBitOf(Expr term,
std::ostream& os,
const ProofLetMap& map)
* @param os the stream to print to
* @param paren any parentheses to add to the end of the global proof
*/
- virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren) = 0;
+ virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren);
/**
* Read the d_atomsInBitblastingProof member.
#include <algorithm>
#include <iterator>
#include <set>
+
#include "options/bv_options.h"
#include "proof/clausal_bitvector_proof.h"
#include "proof/drat/drat_proof.h"
+#include "proof/er/er_proof.h"
#include "proof/lfsc_proof_printer.h"
+#include "proof/lrat/lrat_proof.h"
#include "theory/bv/theory_bv.h"
namespace CVC4 {
void ClausalBitVectorProof::registerUsedClause(ClauseId id,
prop::SatClause& clause)
{
- d_usedClauses.emplace_back(
- id, std::unique_ptr<prop::SatClause>(new prop::SatClause(clause)));
+ d_usedClauses.emplace_back(id, clause);
};
void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
{
+ // Debug dump of DRAT Proof
if (Debug.isOn("bv::clausal"))
{
std::string serializedDratProof = d_binaryDratProof.str();
Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
dratProof.outputAsText(Debug("bv::clausal"));
}
- Unimplemented();
+
+ // Empty any old record of which atoms were used
+ d_atomsInBitblastingProof.clear();
+
+ // For each used clause, ask the CNF proof which atoms are used in it
+ for (const auto& usedIndexAndClause : d_usedClauses)
+ {
+ d_cnfProof->collectAtoms(&usedIndexAndClause.second,
+ d_atomsInBitblastingProof);
+ }
}
void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
std::ostream& paren,
ProofLetMap& letMap)
{
- Unimplemented();
+ os << "\n;; Bitblasting mappings\n";
+ printBitblasting(os, paren);
+
+ os << "\n;; BB-CNF mappings\n";
+ d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
+
+ os << "\n;; BB-CNF proofs\n";
+ for (const auto& idAndClause : d_usedClauses)
+ {
+ d_cnfProof->printCnfProofForClause(
+ idAndClause.first, &idAndClause.second, os, paren);
+ }
}
-void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os,
- std::ostream& paren)
+void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
+ std::ostream& paren)
{
- Unimplemented();
+ Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+ "the BV theory should only be proving bottom directly in the eager "
+ "bitblasting mode");
+
+ os << "\n;; Proof of input to SAT solver\n";
+ os << "(@ proofOfSatInput ";
+ paren << ")";
+ std::vector<ClauseId> usedIds;
+ usedIds.reserve(d_usedClauses.size());
+ for (const auto& idAnd : d_usedClauses)
+ {
+ usedIds.push_back(idAnd.first);
+ };
+ LFSCProofPrinter::printSatInputProof(usedIds, os, "bb");
+
+ os << "\n;; DRAT Proof Value\n";
+ os << "(@ dratProof ";
+ paren << ")";
+ drat::DratProof::fromBinary(d_binaryDratProof.str()).outputAsLfsc(os, 2);
+ os << "\n";
+
+ os << "\n;; Verification of DRAT Proof\n";
+ os << "(drat_proof_of_bottom _ proofOfSatInput dratProof "
+ << "\n)";
+}
+
+void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
+ std::ostream& paren)
+{
+ Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+ "the BV theory should only be proving bottom directly in the eager "
+ "bitblasting mode");
+
+ os << "\n;; Proof of input to SAT solver\n";
+ os << "(@ proofOfCMap ";
+ paren << ")";
+ std::vector<ClauseId> usedIds;
+ usedIds.reserve(d_usedClauses.size());
+ for (const auto& idAnd : d_usedClauses)
+ {
+ usedIds.push_back(idAnd.first);
+ };
+ LFSCProofPrinter::printCMapProof(usedIds, os, "bb");
+
+ os << "\n;; DRAT Proof Value\n";
+ os << "(@ lratProof ";
+ paren << ")";
+ lrat::LratProof pf =
+ lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str());
+ pf.outputAsLfsc(os);
+ os << "\n";
+
+ os << "\n;; Verification of DRAT Proof\n";
+ os << "(lrat_proof_of_bottom _ proofOfCMap lratProof "
+ << "\n)";
+}
+
+void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
+ std::ostream& paren)
+{
+ Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+ "the BV theory should only be proving bottom directly in the eager "
+ "bitblasting mode");
+
+ er::ErProof pf =
+ er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str());
+
+ pf.outputAsLfsc(os);
}
} // namespace proof
protected:
// A list of all clauses and their ids which are passed into the SAT solver
- std::vector<std::pair<ClauseId, std::unique_ptr<prop::SatClause>>>
- d_usedClauses;
+ std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
// Stores the proof recieved from the SAT solver.
std::ostringstream d_binaryDratProof;
};
TheoryProofEngine* proofEngine)
: ClausalBitVectorProof(bv, proofEngine)
{
- // That's all!
}
void printTheoryLemmaProof(std::vector<Expr>& lemma,
void printBBDeclarationAndCnf(std::ostream& os,
std::ostream& paren,
ProofLetMap& letMap) override;
+};
+
+/**
+ * A DRAT proof for a bit-vector problem
+ */
+class LfscDratBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+ LfscDratBitVectorProof(theory::bv::TheoryBV* bv,
+ TheoryProofEngine* proofEngine)
+ : LfscClausalBitVectorProof(bv, proofEngine)
+ {
+ }
+
+ void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+/**
+ * An LRAT proof for a bit-vector problem
+ */
+class LfscLratBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+ LfscLratBitVectorProof(theory::bv::TheoryBV* bv,
+ TheoryProofEngine* proofEngine)
+ : LfscClausalBitVectorProof(bv, proofEngine)
+ {
+ }
+
+ void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+/**
+ * An Extended Resolution proof for a bit-vector problem
+ */
+class LfscErBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+ LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+ : LfscClausalBitVectorProof(bv, proofEngine)
+ {
+ }
+
void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
};
}
}
+// Detects whether a clause has x v ~x for some x
+// If so, returns the positive occurence's idx first, then the negative's
+Maybe<std::pair<size_t, size_t>> CnfProof::detectTrivialTautology(
+ const prop::SatClause& clause)
+{
+ // a map from a SatVariable to its previous occurence's polarity and location
+ std::map<prop::SatVariable, std::pair<bool, size_t>> varsToPolsAndIndices;
+ for (size_t i = 0; i < clause.size(); ++i)
+ {
+ prop::SatLiteral lit = clause[i];
+ prop::SatVariable var = lit.getSatVariable();
+ bool polarity = !lit.isNegated();
+
+ // Check if this var has already occured w/ opposite polarity
+ auto iter = varsToPolsAndIndices.find(var);
+ if (iter != varsToPolsAndIndices.end() && iter->second.first != polarity)
+ {
+ if (iter->second.first)
+ {
+ return Maybe<std::pair<size_t, size_t>>{
+ std::make_pair(iter->second.second, i)};
+ }
+ else
+ {
+ return Maybe<std::pair<size_t, size_t>>{
+ std::make_pair(i, iter->second.second)};
+ }
+ }
+ varsToPolsAndIndices[var] = std::make_pair(polarity, i);
+ }
+ return Maybe<std::pair<size_t, size_t>>{};
+}
+
void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren) {
Assert( clause->size()>0 );
- Node base_assertion = getDefinitionForClause(id);
-
- //get the assertion for the clause id
- std::map<Node, unsigned > childIndex;
- std::map<Node, bool > childPol;
- Node assertion = clauseToNode( *clause, childIndex, childPol );
- //if there is no reason, construct assertion directly. This can happen for unit clauses.
- if( base_assertion.isNull() ){
- base_assertion = assertion;
+ // If the clause contains x v ~x, it's easy!
+ //
+ // It's important to check for this case, because our other logic for
+ // recording the location of variables in the clause assumes the clause is
+ // not tautological
+ Maybe<std::pair<size_t, size_t>> isTrivialTaut =
+ detectTrivialTautology(*clause);
+ if (isTrivialTaut.just())
+ {
+ size_t posIndexInClause = isTrivialTaut.value().first;
+ size_t negIndexInClause = isTrivialTaut.value().second;
+ Trace("cnf-pf") << "; Indices " << posIndexInClause << " (+) and "
+ << negIndexInClause << " (-) make this clause a tautology"
+ << std::endl;
+
+ std::string proofOfPos =
+ ProofManager::getLitName((*clause)[negIndexInClause], d_name);
+ std::string proofOfNeg =
+ ProofManager::getLitName((*clause)[posIndexInClause], d_name);
+ os << "(contra _ " << proofOfPos << " " << proofOfNeg << ")";
}
- //os_base is proof of base_assertion
- std::stringstream os_base;
-
- // checks if tautological definitional clause or top-level clause
- // and prints the proof of the top-level formula
- bool is_input = printProofTopLevel(base_assertion, os_base);
+ else
+ {
+ Node base_assertion = getDefinitionForClause(id);
+
+ // get the assertion for the clause id
+ std::map<Node, unsigned> childIndex;
+ std::map<Node, bool> childPol;
+ Node assertion = clauseToNode(*clause, childIndex, childPol);
+ // if there is no reason, construct assertion directly. This can happen
+ // for unit clauses.
+ if (base_assertion.isNull())
+ {
+ base_assertion = assertion;
+ }
+ // os_base is proof of base_assertion
+ std::stringstream os_base;
+
+ // checks if tautological definitional clause or top-level clause
+ // and prints the proof of the top-level formula
+ bool is_input = printProofTopLevel(base_assertion, os_base);
+
+ if (is_input)
+ {
+ Debug("cnf-pf") << std::endl
+ << "; base assertion is input. proof: " << os_base.str()
+ << std::endl;
+ }
- if (is_input) {
- Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl;
- }
+ // get base assertion with polarity
+ bool base_pol = base_assertion.getKind() != kind::NOT;
+ base_assertion = base_assertion.getKind() == kind::NOT ? base_assertion[0]
+ : base_assertion;
- //get base assertion with polarity
- bool base_pol = base_assertion.getKind()!=kind::NOT;
- base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion;
-
- std::map< Node, unsigned >::iterator itci = childIndex.find( base_assertion );
- bool is_in_clause = itci!=childIndex.end();
- unsigned base_index = is_in_clause ? itci->second : 0;
- Trace("cnf-pf") << std::endl;
- Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl;
- if (!is_input){
- Assert(is_in_clause);
- prop::SatLiteral blit = (*clause)[ base_index ];
- os_base << ProofManager::getLitName(blit, d_name);
- base_pol = !childPol[base_assertion]; // WHY? if the case is =>
- }
- Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl;
- Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl;
-
- bool success = false;
- if( is_input &&
- is_in_clause &&
- childPol[base_assertion]==base_pol ){
- //if both in input and in clause, the proof is trivial. this is the case for unit clauses.
- Trace("cnf-pf") << "; trivial" << std::endl;
- os << "(contra _ ";
- success = true;
- prop::SatLiteral lit = (*clause)[itci->second];
- if( base_pol ){
- os << os_base.str() << " " << ProofManager::getLitName(lit, d_name);
- }else{
- os << ProofManager::getLitName(lit, d_name) << " " << os_base.str();
+ std::map<Node, unsigned>::iterator itci = childIndex.find(base_assertion);
+ bool is_in_clause = itci != childIndex.end();
+ unsigned base_index = is_in_clause ? itci->second : 0;
+ Trace("cnf-pf") << std::endl;
+ Trace("cnf-pf") << "; input = " << is_input
+ << ", is_in_clause = " << is_in_clause << ", id = " << id
+ << ", assertion = " << assertion
+ << ", base assertion = " << base_assertion << std::endl;
+ if (!is_input)
+ {
+ Assert(is_in_clause);
+ prop::SatLiteral blit = (*clause)[base_index];
+ os_base << ProofManager::getLitName(blit, d_name);
+ base_pol = !childPol[base_assertion]; // WHY? if the case is =>
}
- os << ")";
- } else if ((base_assertion.getKind()==kind::AND && !base_pol) ||
+ Trace("cnf-pf") << "; polarity of base assertion = " << base_pol
+ << std::endl;
+ Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl;
+
+ bool success = false;
+ if (is_input && is_in_clause && childPol[base_assertion] == base_pol)
+ {
+ // if both in input and in clause, the proof is trivial. this is the case
+ // for unit clauses.
+ Trace("cnf-pf") << "; trivial" << std::endl;
+ os << "(contra _ ";
+ success = true;
+ prop::SatLiteral lit = (*clause)[itci->second];
+ if (base_pol)
+ {
+ os << os_base.str() << " " << ProofManager::getLitName(lit, d_name);
+ }
+ else
+ {
+ os << ProofManager::getLitName(lit, d_name) << " " << os_base.str();
+ }
+ os << ")";
+ } else if ((base_assertion.getKind()==kind::AND && !base_pol) ||
((base_assertion.getKind()==kind::OR ||
base_assertion.getKind()==kind::IMPLIES) && base_pol)) {
Trace("cnf-pf") << "; and/or case 1" << std::endl;
Trace("cnf-pf") << std::endl;
os << "trust-bad";
}
+ }
os << ")" << clause_paren.str()
<< " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
#include "proof/clause_id.h"
#include "proof/lemma_proof.h"
#include "proof/sat_proof.h"
+#include "util/maybe.h"
#include "util/proof.h"
namespace CVC4 {
std::ostream& paren,
ProofLetMap &letMap) = 0;
+ // Detects whether a clause has x v ~x for some x
+ // If so, returns the positive occurence's idx first, then the negative's
+ static Maybe<std::pair<size_t, size_t>> detectTrivialTautology(
+ const prop::SatClause& clause);
virtual void printClause(const prop::SatClause& clause,
std::ostream& os,
std::ostream& paren) = 0;
{
case ADDITION:
{
- os << "DRATProofa";
+ os << "DRATProofa ";
break;
}
case DELETION:
{
- os << "DRATProofd";
+ os << "DRATProofd ";
break;
}
default: { Unreachable("Unrecognized DRAT instruction kind");
for (const SatLiteral& l : i.d_clause)
{
os << "(clc (" << (l.isNegated() ? "neg " : "pos ")
- << ProofManager::getVarName(l.getSatVariable()) << ") ";
+ << ProofManager::getVarName(l.getSatVariable(), "bb") << ") ";
}
os << "cln";
std::fill_n(std::ostream_iterator<char>(os), i.d_clause.size(), ')');
// Write the formula
std::ofstream formStream(formulaFilename);
printDimacs(formStream, usedClauses);
- unlink(formulaFilename);
+ formStream.close();
// Write the (binary) DRAT proof
std::ofstream dratStream(dratFilename);
dratStream << dratBinary;
- unlink(dratFilename);
+ dratStream.close();
// Invoke drat2er
#if CVC4_USE_DRAT2ER
dratFilename,
tracecheckFilename,
false,
- drat2er::options::QUIET);
+ drat2er::options::QUIET,
+ false);
#else
Unimplemented(
// Parse the resulting TRACECHECK proof into an ER proof.
std::ifstream tracecheckStream(tracecheckFilename);
ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream));
- unlink(tracecheckFilename);
-
- formStream.close();
- dratStream.close();
tracecheckStream.close();
-
+ remove(formulaFilename);
+ remove(dratFilename);
+ remove(tracecheckFilename);
return proof;
}
{
for (size_t i = 0, n = usedClauses.size(); i < n; ++i)
{
+ Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
+ Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
+ std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+ traceCheckClause{d_tracecheck.d_lines[i].d_clause.begin(),
+ d_tracecheck.d_lines[i].d_clause.end()};
+ std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+ originalClause{usedClauses[i].second.begin(),
+ usedClauses[i].second.end()};
+ Assert(traceCheckClause == originalClause);
Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
Assert(d_tracecheck.d_lines[i].d_clause.size()
// Look at the negation of the second literal in the second clause to get
// the old literal
AlwaysAssert(d_tracecheck.d_lines.size() > i + 1,
- "Malformed definition in TRACECHECK proof from drat2er");
+ "Malformed definition in TRACECHECK proof from drat2er");
d_definitions.emplace_back(newVar,
~d_tracecheck.d_lines[i + 1].d_clause[1],
std::move(otherLiterals));
out << ";; Printing final unsat proof \n";
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
- proof::LFSCProofPrinter::printResolutionEmptyClause(
- ProofManager::getBitVectorProof()->getSatProof(), out, paren);
+ ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
} else {
// print actual resolution proof
proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&& options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT)
{
- proof::BitVectorProof* bvp =
- new proof::LfscClausalBitVectorProof(thBv, this);
+ proof::BitVectorProof* bvp = nullptr;
+ switch (options::bvProofFormat())
+ {
+ case theory::bv::BvProofFormat::BITVECTOR_PROOF_DRAT:
+ {
+ bvp = new proof::LfscDratBitVectorProof(thBv, this);
+ break;
+ }
+ case theory::bv::BvProofFormat::BITVECTOR_PROOF_LRAT:
+ {
+ bvp = new proof::LfscLratBitVectorProof(thBv, this);
+ break;
+ }
+ case theory::bv::BvProofFormat::BITVECTOR_PROOF_ER:
+ {
+ bvp = new proof::LfscErBitVectorProof(thBv, this);
+ break;
+ }
+ default: { Unreachable("Invalid BvProofFormat");
+ }
+ };
d_theoryProofTable[id] = bvp;
}
else
; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
+; REQUIRES: cryptominisat
+; REQUIRES: drat2er
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --check-proofs --no-check-unsat-cores
; EXPECT: unsat
(set-logic QF_UFBV)
(set-info :smt-lib-version 2.0)
+; REQUIRES: cryptominisat
+; REQUIRES: drat2er
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --check-proofs --no-check-unsat-cores
+; EXPECT: unsat
(benchmark slice
:status unsat
:logic QF_BV
}
}
std::string expectedLfsc =
- "(DRATProofd (clc (neg .v62) (clc (neg .v8192) cln))"
- "(DRATProofa (clc (pos .v128) (clc (neg .v8190) cln))"
+ "(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)
" RATHintsn)) "
"LRATProofn)))";
- TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(expectedLfsc));
+ TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()),
+ filterWhitespace(expectedLfsc));
}
projects / cvc5.git / commitdiff