diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/prop | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 2 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 2 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 18 | ||||
-rw-r--r-- | src/prop/cadical.cpp | 4 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 78 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 9 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 13 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 2 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 13 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 2 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 4 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 2 |
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 */ |