summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp2
-rw-r--r--src/prop/bvminisat/bvminisat.h2
-rw-r--r--src/prop/bvminisat/core/Solver.cc18
-rw-r--r--src/prop/cadical.cpp4
-rw-r--r--src/prop/cnf_stream.cpp78
-rw-r--r--src/prop/cryptominisat.cpp9
-rw-r--r--src/prop/minisat/core/Solver.cc13
-rw-r--r--src/prop/minisat/minisat.cpp2
-rw-r--r--src/prop/minisat/minisat.h2
-rw-r--r--src/prop/prop_engine.cpp13
-rw-r--r--src/prop/sat_solver.h2
-rw-r--r--src/prop/sat_solver_factory.cpp4
-rw-r--r--src/prop/theory_proxy.cpp2
13 files changed, 77 insertions, 74 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 76d473395..f1e2955da 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -66,7 +66,7 @@ ClauseId BVMinisatSatSolver::addClause(SatClause& clause,
// }
ClauseId clause_id = ClauseIdError;
d_minisat->addClause(minisat_clause, clause_id);
- THEORY_PROOF(Assert (clause_id != ClauseIdError););
+ THEORY_PROOF(Assert(clause_id != ClauseIdError););
return clause_id;
}
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index ca9c553d9..70e0b9157 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -74,7 +74,7 @@ public:
ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
{
- Unreachable("Minisat does not support native XOR reasoning");
+ Unreachable() << "Minisat does not support native XOR reasoning";
}
SatValue propagate() override;
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index a877f20c3..04658fc38 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -235,10 +235,10 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
clause_added = true;
Assert(falseLiteralsCount == 0 || THEORY_PROOF_ON());
-
+
if(falseLiteralsCount == 0) {
if (ps.size() == 0) {
- Assert (!THEORY_PROOF_ON());
+ Assert(!THEORY_PROOF_ON());
return ok = false;
}
else if (ps.size() == 1){
@@ -282,10 +282,10 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
// Check if it propagates
if (ps.size() == falseLiteralsCount + 1) {
Clause& cl = ca[cr];
-
- Assert (value(cl[0]) == l_Undef);
+
+ Assert(value(cl[0]) == l_Undef);
uncheckedEnqueue(cl[0], cr);
- Assert (cl.size() > 1);
+ Assert(cl.size() > 1);
CRef confl = propagate();
ok = (confl == CRef_Undef);
if(!ok) {
@@ -658,7 +658,7 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
if(d_bvp){
if (level(var(p)) == 0 && d_bvp->isAssumptionConflict()) {
- Assert ( marker[var(p)] == 2);
+ Assert(marker[var(p)] == 2);
if (reason(var(p)) == CRef_Undef) {
d_bvp->startBVConflict(p);
}
@@ -775,8 +775,8 @@ lbool Solver::assertAssumption(Lit p, bool propagate) {
}
void Solver::addMarkerLiteral(Var var) {
- // make sure it wasn't already marked
- Assert(marker[var] == 0);
+ // make sure it wasn't already marked
+ Assert(marker[var] == 0);
marker[var] = 1;
if(d_bvp){d_bvp->getSatProof()->registerAssumption(var);}
}
@@ -1284,7 +1284,7 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
assert(level(x) > 0);
explanation.push_back(trail[i]);
} else {
- Assert (level(x) == 0);
+ Assert(level(x) == 0);
if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); }
}
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 479ec2414..f35c343bd 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -90,7 +90,7 @@ ClauseId CadicalSolver::addXorClause(SatClause& clause,
bool rhs,
bool removable)
{
- Unreachable("CaDiCaL does not support adding XOR clauses.");
+ Unreachable() << "CaDiCaL does not support adding XOR clauses.";
}
SatVariable CadicalSolver::newVar(bool isTheoryAtom,
@@ -148,7 +148,7 @@ SatValue CadicalSolver::modelValue(SatLiteral l)
unsigned CadicalSolver::getAssertionLevel() const
{
- Unreachable("CaDiCal does not support assertion levels.");
+ Unreachable() << "CaDiCaL does not support assertion levels.";
}
bool CadicalSolver::ok() const { return d_okay; }
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index dc4722fa1..7df5fb492 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -19,7 +19,7 @@
#include <queue>
-#include "base/cvc4_assert.h"
+#include "base/check.h"
#include "base/output.h"
#include "expr/expr.h"
#include "expr/node.h"
@@ -138,12 +138,14 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
return;
}
- AlwaysAssertArgument(n.getType().isBoolean(), n,
- "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
- "got node: %s\n"
- "its type: %s\n",
- n.toString().c_str(),
- n.getType().toString().c_str());
+ AlwaysAssertArgument(
+ n.getType().isBoolean(),
+ n,
+ "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
+ "got node: %s\n"
+ "its type: %s\n",
+ n.toString().c_str(),
+ n.getType().toString().c_str());
bool negated CVC4_UNUSED = false;
SatLiteral lit;
@@ -231,14 +233,14 @@ void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
}
void CnfStream::setProof(CnfProof* proof) {
- Assert (d_cnfProof == NULL);
+ Assert(d_cnfProof == NULL);
d_cnfProof = proof;
}
SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
Debug("cnf") << "convertAtom(" << node << ")" << endl;
- Assert(!hasLiteral(node), "atom already mapped!");
+ Assert(!hasLiteral(node)) << "atom already mapped!";
bool theoryLiteral = false;
bool canEliminate = true;
@@ -260,11 +262,10 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
}
SatLiteral CnfStream::getLiteral(TNode node) {
- Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
+ Assert(!node.isNull()) << "CnfStream: can't getLiteral() of null node";
- Assert(d_nodeToLiteralMap.contains(node),
- "Literal not in the CNF Cache: %s\n",
- node.toString().c_str());
+ Assert(d_nodeToLiteralMap.contains(node))
+ << "Literal not in the CNF Cache: " << node << "\n";
SatLiteral literal = d_nodeToLiteralMap[node];
Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
@@ -272,10 +273,10 @@ SatLiteral CnfStream::getLiteral(TNode node) {
}
SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
- Assert(!hasLiteral(xorNode), "Atom already mapped!");
- Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
- Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
- Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+ Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
+ Assert(xorNode.getKind() == XOR) << "Expecting an XOR expression!";
+ Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
+ Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
SatLiteral a = toCNF(xorNode[0]);
SatLiteral b = toCNF(xorNode[1]);
@@ -291,10 +292,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
}
SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
- Assert(!hasLiteral(orNode), "Atom already mapped!");
- Assert(orNode.getKind() == OR, "Expecting an OR expression!");
- Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
- Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+ Assert(!hasLiteral(orNode)) << "Atom already mapped!";
+ Assert(orNode.getKind() == OR) << "Expecting an OR expression!";
+ Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!";
+ Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
// Number of children
unsigned n_children = orNode.getNumChildren();
@@ -328,10 +329,10 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
}
SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
- Assert(!hasLiteral(andNode), "Atom already mapped!");
- Assert(andNode.getKind() == AND, "Expecting an AND expression!");
- Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
- Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+ Assert(!hasLiteral(andNode)) << "Atom already mapped!";
+ Assert(andNode.getKind() == AND) << "Expecting an AND expression!";
+ Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!";
+ Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
// Number of children
unsigned n_children = andNode.getNumChildren();
@@ -365,10 +366,11 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
}
SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
- Assert(!hasLiteral(impliesNode), "Atom already mapped!");
- Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
- Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
- Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+ Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
+ Assert(impliesNode.getKind() == IMPLIES)
+ << "Expecting an IMPLIES expression!";
+ Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
+ Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
// Convert the children to cnf
SatLiteral a = toCNF(impliesNode[0]);
@@ -391,9 +393,9 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
- Assert(!hasLiteral(iffNode), "Atom already mapped!");
- Assert(iffNode.getKind() == EQUAL, "Expecting an EQUAL expression!");
- Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
+ Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
+ Assert(iffNode.getKind() == EQUAL) << "Expecting an EQUAL expression!";
+ Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
@@ -423,9 +425,9 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
- Assert(!hasLiteral(notNode), "Atom already mapped!");
- Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
- Assert(notNode.getNumChildren() == 1, "Expecting exactly 1 child!");
+ Assert(!hasLiteral(notNode)) << "Atom already mapped!";
+ Assert(notNode.getKind() == NOT) << "Expecting a NOT expression!";
+ Assert(notNode.getNumChildren() == 1) << "Expecting exactly 1 child!";
SatLiteral notLit = ~toCNF(notNode[0]);
@@ -435,7 +437,7 @@ SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
Assert(iteNode.getKind() == ITE);
Assert(iteNode.getNumChildren() == 3);
- Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+ Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
@@ -539,7 +541,7 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
SatClause clause(nChildren);
TNode::const_iterator disjunct = node.begin();
for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
- Assert( disjunct != node.end() );
+ Assert(disjunct != node.end());
clause[i] = toCNF(*disjunct, true);
}
Assert(disjunct == node.end());
@@ -555,7 +557,7 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
SatClause clause(nChildren);
TNode::const_iterator disjunct = node.begin();
for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
- Assert( disjunct != node.end() );
+ Assert(disjunct != node.end());
clause[i] = toCNF(*disjunct, false);
}
Assert(disjunct == node.end());
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 62e2c5a43..8a70bedce 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -149,7 +149,7 @@ bool CryptoMinisatSolver::ok() const {
SatVariable CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
d_solver->new_var();
++d_numVariables;
- Assert (d_numVariables == d_solver->nVars());
+ Assert(d_numVariables == d_solver->nVars());
return d_numVariables - 1;
}
@@ -179,7 +179,8 @@ SatValue CryptoMinisatSolver::solve(){
SatValue CryptoMinisatSolver::solve(long unsigned int& resource) {
// CMSat::SalverConf conf = d_solver->getConf();
- Unreachable("Not sure how to set different limits for calls to solve in Cryptominisat");
+ Unreachable() << "Not sure how to set different limits for calls to solve in "
+ "Cryptominisat";
return solve();
}
@@ -198,7 +199,7 @@ SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
SatValue CryptoMinisatSolver::value(SatLiteral l){
const std::vector<CMSat::lbool> model = d_solver->get_model();
CMSatVar var = l.getSatVariable();
- Assert (var < model.size());
+ Assert(var < model.size());
CMSat::lbool value = model[var];
return toSatLiteralValue(value);
}
@@ -208,7 +209,7 @@ SatValue CryptoMinisatSolver::modelValue(SatLiteral l){
}
unsigned CryptoMinisatSolver::getAssertionLevel() const {
- Unreachable("No interface to get assertion level in Cryptominisat");
+ Unreachable() << "No interface to get assertion level in Cryptominisat";
return -1;
}
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index c8a2e16c2..5b097dc39 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -210,7 +210,7 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo
void Solver::resizeVars(int newSize) {
assert(enable_incremental);
assert(decisionLevel() == 0);
- Assert(newSize >= 2, "always keep true/false");
+ Assert(newSize >= 2) << "always keep true/false";
if (newSize < nVars()) {
int shrinkSize = nVars() - newSize;
@@ -626,7 +626,8 @@ Lit Solver::pickBranchLit()
return lit_Undef;
}
if(nextLit != lit_Undef) {
- Assert(value(var(nextLit)) == l_Undef, "literal to decide already has value");
+ Assert(value(var(nextLit)) == l_Undef)
+ << "literal to decide already has value";
decisions++;
Var next = var(nextLit);
if(polarity[next] & 0x2) {
@@ -1736,7 +1737,7 @@ CRef Solver::updateLemmas() {
// If it's an empty lemma, we have a conflict at zero level
if (lemma.size() == 0) {
- Assert (! PROOF_ON());
+ Assert(!PROOF_ON());
conflict = CRef_Lazy;
backtrackLevel = 0;
Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -1766,7 +1767,7 @@ CRef Solver::updateLemmas() {
// Last index in the trail
int backtrack_index = trail.size();
- PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size()););
+ PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
// Attach all the clauses and enqueue all the propagations
for (int i = 0; i < lemmas.size(); ++ i)
@@ -1839,7 +1840,7 @@ CRef Solver::updateLemmas() {
}
}
- PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size()););
+ PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
// Clear the lemmas
lemmas.clear();
lemmas_cnf_assertion.clear();
@@ -1881,7 +1882,7 @@ void ClauseAllocator::reloc(CRef& cr,
inline bool Solver::withinBudget(uint64_t amount) const
{
- Assert (proxy);
+ Assert(proxy);
// spendResource sets async_interrupt or throws UnsafeInterruptException
// depending on whether hard-limit is enabled
proxy->spendResource(amount);
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 4995a60dd..3cdd6b654 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -151,7 +151,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
return ClauseIdUndef;
}
d_minisat->addClause(minisat_clause, removable, clause_id);
- PROOF( Assert (clause_id != ClauseIdError););
+ PROOF(Assert(clause_id != ClauseIdError););
return clause_id;
}
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index d4720def5..3cc0ed120 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -44,7 +44,7 @@ public:
ClauseId addClause(SatClause& clause, bool removable) override;
ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
{
- Unreachable("Minisat does not support native XOR reasoning");
+ Unreachable() << "Minisat does not support native XOR reasoning";
}
SatVariable newVar(bool isTheoryAtom,
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 55d8f7222..8a0cc9f15 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -20,7 +20,7 @@
#include <map>
#include <utility>
-#include "base/cvc4_assert.h"
+#include "base/check.h"
#include "base/output.h"
#include "decision/decision_engine.h"
#include "expr/expr.h"
@@ -30,13 +30,12 @@
#include "options/options.h"
#include "options/smt_options.h"
#include "proof/proof_manager.h"
-#include "proof/proof_manager.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
#include "prop/theory_proxy.h"
-#include "smt/smt_statistics_registry.h"
#include "smt/command.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
#include "util/resource_manager.h"
@@ -119,7 +118,7 @@ PropEngine::~PropEngine() {
}
void PropEngine::assertFormula(TNode node) {
- Assert(!d_inCheckSat, "Sat solver in solve()!");
+ Assert(!d_inCheckSat) << "Sat solver in solve()!";
Debug("prop") << "assertFormula(" << node << ")" << endl;
// Assert as non-removable
d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN);
@@ -170,7 +169,7 @@ void PropEngine::printSatisfyingAssignment(){
}
Result PropEngine::checkSat() {
- Assert(!d_inCheckSat, "Sat solver in solve()!");
+ Assert(!d_inCheckSat) << "Sat solver in solve()!";
Debug("prop") << "PropEngine::checkSat()" << endl;
// Mark that we are in the checkSat
@@ -261,13 +260,13 @@ void PropEngine::ensureLiteral(TNode n) {
}
void PropEngine::push() {
- Assert(!d_inCheckSat, "Sat solver in solve()!");
+ Assert(!d_inCheckSat) << "Sat solver in solve()!";
d_satSolver->push();
Debug("prop") << "push()" << endl;
}
void PropEngine::pop() {
- Assert(!d_inCheckSat, "Sat solver in solve()!");
+ Assert(!d_inCheckSat) << "Sat solver in solve()!";
d_satSolver->pop();
Debug("prop") << "pop()" << endl;
}
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 45bfca4d6..9898f3f87 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -83,7 +83,7 @@ public:
/** Check satisfiability under assumptions */
virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
{
- Unimplemented("Solving under assumptions not implemented");
+ Unimplemented() << "Solving under assumptions not implemented";
};
/** Interrupt the solver */
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index cfab5703c..460ab3ece 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -44,7 +44,7 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
#ifdef CVC4_USE_CRYPTOMINISAT
return new CryptoMinisatSolver(registry, name);
#else
- Unreachable("CVC4 was not compiled with Cryptominisat support.");
+ Unreachable() << "CVC4 was not compiled with Cryptominisat support.";
#endif
}
@@ -54,7 +54,7 @@ SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
#ifdef CVC4_USE_CADICAL
return new CadicalSolver(registry, name);
#else
- Unreachable("CVC4 was not compiled with CaDiCaL support.");
+ Unreachable() << "CVC4 was not compiled with CaDiCaL support.";
#endif
}
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index f6cd42eff..1258d2ee2 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -232,7 +232,7 @@ SatLiteral TheoryProxy::getNextReplayDecision() {
void TheoryProxy::logDecision(SatLiteral lit) {
#ifdef CVC4_REPLAY
if(d_replayLog != NULL) {
- Assert(lit != undefSatLiteral, "logging an `undef' decision ?!");
+ Assert(lit != undefSatLiteral) << "logging an `undef' decision ?!";
(*d_replayLog) << d_cnfStream->getNode(lit) << std::endl;
}
#endif /* CVC4_REPLAY */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback