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/proof | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/arith_proof.cpp | 51 | ||||
-rw-r--r-- | src/proof/array_proof.cpp | 36 | ||||
-rw-r--r-- | src/proof/bitvector_proof.cpp | 26 | ||||
-rw-r--r-- | src/proof/clausal_bitvector_proof.cpp | 34 | ||||
-rw-r--r-- | src/proof/cnf_proof.cpp | 33 | ||||
-rw-r--r-- | src/proof/dimacs.cpp | 2 | ||||
-rw-r--r-- | src/proof/drat/drat_proof.cpp | 8 | ||||
-rw-r--r-- | src/proof/er/er_proof.cpp | 16 | ||||
-rw-r--r-- | src/proof/lemma_proof.cpp | 3 | ||||
-rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 11 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 62 | ||||
-rw-r--r-- | src/proof/proof_output_channel.cpp | 6 | ||||
-rw-r--r-- | src/proof/proof_utils.h | 7 | ||||
-rw-r--r-- | src/proof/resolution_bitvector_proof.cpp | 6 | ||||
-rw-r--r-- | src/proof/skolemization_manager.cpp | 5 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 53 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 26 | ||||
-rw-r--r-- | src/proof/unsat_core.cpp | 2 |
18 files changed, 213 insertions, 174 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 8b55c29db..77f4b1630 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -236,7 +236,8 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, out << ss.str(); out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; } else { - Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); + Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) + || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); if(n1[1] == n2[0][0]) { out << "(symm _ _ _ " << ss.str() << ")"; } else { @@ -256,12 +257,17 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0].get()) { Assert(!pf2->d_node.isNull()); - Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE); + Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF + || pf2->d_node.getKind() == kind::BUILTIN + || pf2->d_node.getKind() == kind::APPLY_UF + || pf2->d_node.getKind() == kind::SELECT + || pf2->d_node.getKind() == kind::STORE); Assert(pf2->d_children.size() == 2); out << "(cong _ _ _ _ _ _ "; stk.push(pf2); } - Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); + Assert(stk.top()->d_children[0]->d_id + != theory::eq::MERGED_THROUGH_CONGRUENCE); NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); const theory::eq::EqProof* pf2 = stk.top(); stk.pop(); @@ -322,7 +328,12 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, b2 << n2[1-side]; out << ss.str(); } else { - Assert(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]); + Assert(pf2->d_node[b1.getNumChildren() + - (pf2->d_node.getMetaKind() + == kind::metakind::PARAMETERIZED + ? 0 + : 1)] + == n2[1 - side]); b1 << n2[1-side]; b2 << n2[side]; out << "(symm _ _ _ " << ss.str() << ")"; @@ -349,7 +360,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, b2 << n2[1-side]; out << ss.str(); } else { - Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]); + Assert(pf2->d_node[b1.getNumChildren()] == n2[1 - side]); b1 << n2[1-side]; b2 << n2[side]; out << "(symm _ _ _ " << ss.str() << ")"; @@ -677,7 +688,7 @@ void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM // !d_realMode <--> term.getType().isInteger() - Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH); + Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARITH); switch (term.getKind()) { case kind::CONST_RATIONAL: @@ -899,9 +910,8 @@ void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o, } default: #ifdef CVC4_ASSERTIONS - std::ostringstream msg; - msg << "Invalid operation " << n.getKind() << " in linear polynomial"; - Unreachable(msg.str().c_str()); + Unreachable() << "Invalid operation " << n.getKind() + << " in linear polynomial"; #endif // CVC4_ASSERTIONS break; } @@ -914,13 +924,11 @@ void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o, { case kind::MULT: { #ifdef CVC4_ASSERTIONS - std::ostringstream s; - s << "node " << n << " is not a linear monomial"; - s << " " << n[0].getKind() << " " << n[1].getKind(); Assert((n[0].getKind() == kind::CONST_RATIONAL && (n[1].getKind() == kind::VARIABLE - || n[1].getKind() == kind::SKOLEM)), - s.str().c_str()); + || n[1].getKind() == kind::SKOLEM))) + << "node " << n << " is not a linear monomial" + << " " << n[0].getKind() << " " << n[1].getKind(); #endif // CVC4_ASSERTIONS o << "\n (pn_mul_c_L _ _ _ "; @@ -946,9 +954,8 @@ void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o, } default: #ifdef CVC4_ASSERTIONS - std::ostringstream msg; - msg << "Invalid operation " << n.getKind() << " in linear monomial"; - Unreachable(msg.str().c_str()); + Unreachable() << "Invalid operation " << n.getKind() + << " in linear monomial"; #endif // CVC4_ASSERTIONS break; } @@ -963,18 +970,16 @@ void LFSCArithProof::printConstRational(std::ostream& o, const Node& n) void LFSCArithProof::printVariableNormalizer(std::ostream& o, const Node& n) { - std::ostringstream msg; - msg << "Invalid variable kind " << n.getKind() << " in linear monomial"; - Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM, - msg.str().c_str()); + Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM) + << "Invalid variable kind " << n.getKind() << " in linear monomial"; o << "(pn_var " << n << ")"; } void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o, const Node& n) { - Assert(n.getKind() == kind::GEQ, - "can only print normalization witnesses for (>=) nodes"); + Assert(n.getKind() == kind::GEQ) + << "can only print normalization witnesses for (>=) nodes"; Assert(n[1].getKind() == kind::CONST_RATIONAL); o << "(poly_formula_norm_>= _ _ _ "; o << "\n (pn_- _ _ _ _ _ "; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 131fcd3b6..ec2f85829 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -152,7 +152,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, out << ss.str(); out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; } else { - Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); + Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) + || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); if(n1[1] == n2[0][0]) { out << "(symm _ _ _ " << ss.str() << ")"; } else { @@ -166,7 +167,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } else { Node n2 = pf.d_node; Assert(n2.getKind() == kind::EQUAL); - Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); + Assert((n1[0] == n2[0] && n1[1] == n2[1]) + || (n1[1] == n2[0] && n1[0] == n2[1])); out << ss.str(); out << " "; @@ -323,10 +325,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b2 << n2[1-side]; out << ss.str(); } else { - Assert(pf2->d_node[b1.getNumChildren() + - (n1[side].getKind() == kind::PARTIAL_SELECT_0 ? 1 : 0) + - (n1[side].getKind() == kind::PARTIAL_SELECT_1 ? 1 : 0) - - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]); + Assert( + pf2->d_node[b1.getNumChildren() + + (n1[side].getKind() == kind::PARTIAL_SELECT_0 ? 1 : 0) + + (n1[side].getKind() == kind::PARTIAL_SELECT_1 ? 1 : 0) + - (pf2->d_node.getMetaKind() + == kind::metakind::PARAMETERIZED + ? 0 + : 1)] + == n2[1 - side]); b1 << n2[1-side]; b2 << n2[side]; out << "(symm _ _ _ " << ss.str() << ")"; @@ -359,7 +366,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, b2 << n2[1-side]; out << ss.str(); } else { - Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]); + Assert(pf2->d_node[b1.getNumChildren()] == n2[1 - side]); b1 << n2[1-side]; b2 << n2[side]; out << "(symm _ _ _ " << ss.str() << ")"; @@ -383,7 +390,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "n1.getNumChildren() + 1 = " << n1.getNumChildren() + 1 << std::endl; - Assert(!((n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 2))); + Assert(!( + (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 2))); if (n1.getKind() == kind::PARTIAL_SELECT_1 && n1.getNumChildren() == 2) { Debug("mgd") << "Finished a SELECT. Updating.." << std::endl; b1.clear(kind::SELECT); @@ -410,7 +418,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "n2.getNumChildren() + 1 = " << n2.getNumChildren() + 1 << std::endl; - Assert(!((n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 2))); + Assert(!( + (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 2))); if (n2.getKind() == kind::PARTIAL_SELECT_1 && n2.getNumChildren() == 2) { Debug("mgd") << "Finished a SELECT. Updating.." << std::endl; b2.clear(kind::SELECT); @@ -1115,7 +1124,7 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) { } void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { - Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS); + Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS); if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAYS) { // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term @@ -1129,7 +1138,10 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM return; } - Assert ((term.getKind() == kind::SELECT) || (term.getKind() == kind::PARTIAL_SELECT_0) || (term.getKind() == kind::PARTIAL_SELECT_1) || (term.getKind() == kind::STORE)); + Assert((term.getKind() == kind::SELECT) + || (term.getKind() == kind::PARTIAL_SELECT_0) + || (term.getKind() == kind::PARTIAL_SELECT_1) + || (term.getKind() == kind::STORE)); switch (term.getKind()) { case kind::SELECT: { @@ -1196,7 +1208,7 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) { Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl; - Assert (type.isArray() || type.isSort()); + Assert(type.isArray() || type.isSort()); if (type.isArray()){ ArrayType array_type(type); diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 18e46a292..98f57e25f 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -224,16 +224,16 @@ void BitVectorProof::printOwnedTerm(Expr term, 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"); + 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) { - Assert (term.getKind() == kind::BITVECTOR_BITOF); + Assert(term.getKind() == kind::BITVECTOR_BITOF); unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex; Expr var = term[0]; @@ -247,7 +247,7 @@ void BitVectorProof::printBitOf(Expr term, void BitVectorProof::printConstant(Expr term, std::ostream& os) { - Assert (term.isConst()); + Assert(term.isConst()); os << "(a_bv " << utils::getSize(term) << " "; if (d_useConstantLetification) { @@ -336,7 +336,7 @@ void BitVectorProof::printOperatorParametric(Expr term, os << high <<" " << low << " " << utils::getSize(term[0]); } os <<" "; - Assert (term.getNumChildren() == 1); + Assert(term.getNumChildren() == 1); d_proofEngine->printBoundTerm(term[0], os, map); os <<")"; } @@ -346,7 +346,7 @@ void BitVectorProof::printOwnedSort(Type type, std::ostream& os) Debug("pf::bv") << std::endl << "(pf::bv) BitVectorProof::printOwnedSort( " << type << " )" << std::endl; - Assert (type.isBitVector()); + Assert(type.isBitVector()); unsigned width = utils::getSize(type); os << "(BitVec " << width << ")"; } @@ -433,7 +433,7 @@ void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { // TODO: once we have the operator elimination rules remove those that we // eliminated - Assert (term.getType().isBitVector()); + Assert(term.getType().isBitVector()); Kind kind = term.getKind(); if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) @@ -568,7 +568,7 @@ void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os) return; } - default: Unreachable("BitVectorProof Unknown operator"); + default: Unreachable() << "BitVectorProof Unknown operator"; } } @@ -601,7 +601,7 @@ void BitVectorProof::printAtomBitblasting(Expr atom, return; } - default: Unreachable("BitVectorProof Unknown atom kind"); + default: Unreachable() << "BitVectorProof Unknown atom kind"; } } @@ -739,9 +739,9 @@ bool BitVectorProof::hasAlias(Expr expr) void BitVectorProof::printConstantDisequalityProof( std::ostream& os, Expr c1, Expr c2, const ProofLetMap& globalLetMap) { - Assert (c1.isConst()); - Assert (c2.isConst()); - Assert (utils::getSize(c1) == utils::getSize(c2)); + Assert(c1.isConst()); + Assert(c2.isConst()); + Assert(utils::getSize(c1) == utils::getSize(c2)); os << "(bv_disequal_constants " << utils::getSize(c1) << " "; diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index 4e700a832..bb9213b4b 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -175,13 +175,13 @@ void ClausalBitVectorProof::optimizeDratProof() optFormulaFilename, optDratFilename, drat2er::options::QUIET); - AlwaysAssert( - dratTrimExitCode == 0, "drat-trim exited with %d", dratTrimExitCode); + AlwaysAssert(dratTrimExitCode == 0) + << "drat-trim exited with " << dratTrimExitCode; } #else - Unimplemented( - "Proof production when using CryptoMiniSat requires drat2er.\n" - "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); + Unimplemented() + << "Proof production when using CryptoMiniSat requires drat2er.\n" + << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"; #endif { @@ -314,9 +314,9 @@ void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& paren, const ProofLetMap& map) { - Unreachable( - "Clausal bit-vector proofs should only be used in combination with eager " - "bitblasting, which **does not use theory lemmas**"); + Unreachable() << "Clausal bit-vector proofs should only be used in " + "combination with eager " + "bitblasting, which **does not use theory lemmas**"; } void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, @@ -339,9 +339,9 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, void LfscDratBitVectorProof::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"); + 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 "; @@ -366,9 +366,9 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os, 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"); + 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 "; @@ -396,9 +396,9 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os, 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"); + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + << "the BV theory should only be proving bottom directly in the eager " + "bitblasting mode"; d_dratTranslationStatistics.d_totalTime.start(); er::ErProof pf = diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 9c263e08f..c8284762c 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -57,7 +57,7 @@ bool CnfProof::isDefinition(Node node) { } ProofRule CnfProof::getProofRule(Node node) { - Assert (isAssertion(node)); + Assert(isAssertion(node)); NodeToProofRule::iterator it = d_assertionToProofRule.find(node); return (*it).second; } @@ -69,27 +69,26 @@ ProofRule CnfProof::getProofRule(ClauseId clause) { Node CnfProof::getAssertionForClause(ClauseId clause) { ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause); - Assert (it != d_clauseToAssertion.end()); + Assert(it != d_clauseToAssertion.end()); return (*it).second; } Node CnfProof::getDefinitionForClause(ClauseId clause) { ClauseIdToNode::const_iterator it = d_clauseToDefinition.find(clause); - Assert (it != d_clauseToDefinition.end()); + Assert(it != d_clauseToDefinition.end()); return (*it).second; } void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { - Assert (clause != ClauseIdUndef && - clause != ClauseIdError && - clause != ClauseIdEmpty); + Assert(clause != ClauseIdUndef && clause != ClauseIdError + && clause != ClauseIdEmpty); // Explanations do not need a CNF conversion proof since they are in CNF // (they will only need a theory proof as they are theory valid) if (explanation) { Debug("proof:cnf") << "CnfProof::registerConvertedClause " << clause << " explanation? " << explanation << std::endl; - Assert (d_explanations.find(clause) == d_explanations.end()); + Assert(d_explanations.find(clause) == d_explanations.end()); d_explanations.insert(clause); return; } @@ -180,7 +179,7 @@ void CnfProof::setCnfDependence(Node from, Node to) { << "from " << from << std::endl << " to " << to << std::endl; - Assert (from != to); + Assert(from != to); d_cnfDeps.insert(std::make_pair(from, to)); } @@ -196,7 +195,7 @@ void CnfProof::pushCurrentAssertion(Node assertion) { } void CnfProof::popCurrentAssertion() { - Assert (d_currentAssertionStack.size()); + Assert(d_currentAssertionStack.size()); Debug("proof:cnf") << "CnfProof::popCurrentAssertion " << d_currentAssertionStack.back() << std::endl; @@ -209,7 +208,7 @@ void CnfProof::popCurrentAssertion() { } Node CnfProof::getCurrentAssertion() { - Assert (d_currentAssertionStack.size()); + Assert(d_currentAssertionStack.size()); return d_currentAssertionStack.back(); } @@ -227,7 +226,7 @@ void CnfProof::pushCurrentDefinition(Node definition) { } void CnfProof::popCurrentDefinition() { - Assert (d_currentDefinitionStack.size()); + Assert(d_currentDefinitionStack.size()); Debug("proof:cnf") << "CnfProof::popCurrentDefinition " << d_currentDefinitionStack.back() << std::endl; @@ -236,7 +235,7 @@ void CnfProof::popCurrentDefinition() { } Node CnfProof::getCurrentDefinition() { - Assert (d_currentDefinitionStack.size()); + Assert(d_currentDefinitionStack.size()); return d_currentDefinitionStack.back(); } @@ -295,7 +294,7 @@ void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClause Node node = getAtom(lit.getSatVariable()); Expr atom = node.toExpr(); if (atom.isConst()) { - Assert (atom == utils::mkTrue()); + Assert(atom == utils::mkTrue()); continue; } clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node); @@ -462,7 +461,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, // return; - Assert( clause->size()>0 ); + Assert(clause->size() > 0); // If the clause contains x v ~x, it's easy! // @@ -639,10 +638,10 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, Node iatom; if (is_in_clause) { - Assert( assertion.getNumChildren()==2 ); + Assert(assertion.getNumChildren() == 2); iatom = assertion[ base_index==0 ? 1 : 0]; } else { - Assert( assertion.getNumChildren()==1 ); + Assert(assertion.getNumChildren() == 1); iatom = assertion[0]; } @@ -753,7 +752,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl; os_base_n << ProofManager::getLitName(lit1, d_name) << " "; } - Assert( elimNum!=0 ); + Assert(elimNum != 0); os_base_n << "(" << ( k==kind::EQUAL ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; if( !base_pol ){ os_base_n << "(not_" << ( base_assertion.getKind()==kind::EQUAL ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; diff --git a/src/proof/dimacs.cpp b/src/proof/dimacs.cpp index cced98660..fd5b79383 100644 --- a/src/proof/dimacs.cpp +++ b/src/proof/dimacs.cpp @@ -16,7 +16,7 @@ #include "proof/dimacs.h" -#include "base/cvc4_assert.h" +#include "base/check.h" #include <iostream> diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp index 5a01ffdfd..162efc3e5 100644 --- a/src/proof/drat/drat_proof.cpp +++ b/src/proof/drat/drat_proof.cpp @@ -158,7 +158,9 @@ void DratInstruction::outputAsText(std::ostream& os) const os << '0' << std::endl; break; } - default: { Unreachable("Unknown DRAT instruction kind"); + default: + { + Unreachable() << "Unknown DRAT instruction kind"; } } } @@ -267,7 +269,9 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const os << "DRATProofd "; break; } - default: { Unreachable("Unrecognized DRAT instruction kind"); + default: + { + Unreachable() << "Unrecognized DRAT instruction kind"; } } for (const SatLiteral& l : i.d_clause) diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp index 9f22e236b..19c838e2d 100644 --- a/src/proof/er/er_proof.cpp +++ b/src/proof/er/er_proof.cpp @@ -29,7 +29,7 @@ #include <iterator> #include <unordered_set> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/map_util.h" #include "proof/dimacs.h" #include "proof/lfsc_proof_printer.h" @@ -114,9 +114,9 @@ ErProof ErProof::fromBinaryDratProof( drat2er::options::QUIET, false); #else - Unimplemented( - "ER proof production requires drat2er.\n" - "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); + Unimplemented() + << "ER proof production requires drat2er.\n" + << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"; #endif } @@ -184,8 +184,8 @@ ErProof::ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses, size_t nLinesForThisDef = 2 + otherLiterals.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"); + AlwaysAssert(d_tracecheck.d_lines.size() > i + 1) + << "Malformed definition in TRACECHECK proof from drat2er"; d_definitions.emplace_back(newVar, ~d_tracecheck.d_lines[i + 1].d_clause[1], std::move(otherLiterals)); @@ -299,8 +299,8 @@ void ErProof::outputAsLfsc(std::ostream& os) const } // Write proof of bottom - Assert(d_tracecheck.d_lines.back().d_clause.size() == 0, - "The TRACECHECK proof from drat2er did not prove bottom."); + Assert(d_tracecheck.d_lines.back().d_clause.size() == 0) + << "The TRACECHECK proof from drat2er did not prove bottom."; os << "\n er.c" << d_tracecheck.d_lines.back().d_idx << " ; (holds cln)\n"; diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp index 6bb2c2854..f4249f3d5 100644 --- a/src/proof/lemma_proof.cpp +++ b/src/proof/lemma_proof.cpp @@ -147,7 +147,8 @@ bool LemmaProofRecipe::wasRewritten(Node assertion) const { } Node LemmaProofRecipe::getExplanation(Node assertion) const { - Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()); + Assert(d_assertionToExplanation.find(assertion) + != d_assertionToExplanation.end()); return d_assertionToExplanation.find(assertion)->second; } diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index 1685ad1c3..4a19f07be 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -24,7 +24,7 @@ #include <sstream> #include <unordered_map> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/output.h" #include "proof/dimacs.h" #include "proof/lfsc_proof_printer.h" @@ -151,9 +151,9 @@ LratProof LratProof::fromDratProof( drat2er::drat_trim::CheckAndConvertToLRAT( formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET); #else - Unimplemented( - "LRAT proof production requires drat2er.\n" - "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); + Unimplemented() + << "LRAT proof production requires drat2er.\n" + << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"; #endif } @@ -221,7 +221,8 @@ LratProof::LratProof(std::istream& textualProof) SatLiteral lit; firstS >> lit; Trace("pf::lrat") << "First lit: " << lit << std::endl; - Assert(!firstS.fail(), "Couldn't parse first literal from addition line"); + Assert(!firstS.fail()) + << "Couldn't parse first literal from addition line"; SatClause clause; for (; lit != 0; textualProof >> lit) diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index f68d5937c..fa4c1ecb5 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -17,7 +17,7 @@ #include "proof/proof_manager.h" -#include "base/cvc4_assert.h" +#include "base/check.h" #include "context/context.h" #include "options/bv_options.h" #include "options/proof_options.h" @@ -97,52 +97,52 @@ const Proof& ProofManager::getProof(SmtEngine* smt) } CoreSatProof* ProofManager::getSatProof() { - Assert (currentPM()->d_satProof); + Assert(currentPM()->d_satProof); return currentPM()->d_satProof; } CnfProof* ProofManager::getCnfProof() { - Assert (currentPM()->d_cnfProof); + Assert(currentPM()->d_cnfProof); return currentPM()->d_cnfProof; } TheoryProofEngine* ProofManager::getTheoryProofEngine() { - Assert (currentPM()->d_theoryProof != NULL); + Assert(currentPM()->d_theoryProof != NULL); return currentPM()->d_theoryProof; } UFProof* ProofManager::getUfProof() { - Assert (options::proof()); + Assert(options::proof()); TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF); return (UFProof*)pf; } proof::ResolutionBitVectorProof* ProofManager::getBitVectorProof() { - Assert (options::proof()); + Assert(options::proof()); TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV); return static_cast<proof::ResolutionBitVectorProof*>(pf); } ArrayProof* ProofManager::getArrayProof() { - Assert (options::proof()); + Assert(options::proof()); TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS); return (ArrayProof*)pf; } ArithProof* ProofManager::getArithProof() { - Assert (options::proof()); + Assert(options::proof()); TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARITH); return (ArithProof*)pf; } SkolemizationManager* ProofManager::getSkolemizationManager() { - Assert (options::proof() || options::unsatCores()); + Assert(options::proof() || options::unsatCores()); return &(currentPM()->d_skolemizationManager); } void ProofManager::initSatProof(Minisat::Solver* solver) { - Assert (currentPM()->d_satProof == NULL); + Assert(currentPM()->d_satProof == NULL); Assert(currentPM()->d_format == LFSC); currentPM()->d_satProof = new CoreSatProof(solver, d_context, ""); } @@ -151,8 +151,8 @@ void ProofManager::initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx) { ProofManager* pm = currentPM(); Assert(pm->d_satProof != NULL); - Assert (pm->d_cnfProof == NULL); - Assert (pm->d_format == LFSC); + Assert(pm->d_cnfProof == NULL); + Assert(pm->d_format == LFSC); CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, ""); pm->d_cnfProof = cnf; @@ -175,8 +175,8 @@ void ProofManager::initCnfProof(prop::CnfStream* cnfStream, } void ProofManager::initTheoryProofEngine() { - Assert (currentPM()->d_theoryProof == NULL); - Assert (currentPM()->d_format == LFSC); + Assert(currentPM()->d_theoryProof == NULL); + Assert(currentPM()->d_format == LFSC); currentPM()->d_theoryProof = new LFSCTheoryProofEngine(); } @@ -250,7 +250,7 @@ bool ProofManager::hasLitName(TNode lit) { } std::string ProofManager::sanitize(TNode node) { - Assert (node.isVar() || node.isConst()); + Assert(node.isVar() || node.isConst()); std::string name = node.toString(); if (node.isVar()) { @@ -282,7 +282,9 @@ void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) { Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl; return; } - InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str()); + InternalError() + << "Cannot trace dependence information back to input assertion:\n`" + << n << "'"; } Assert(d_deps.find(n) != d_deps.end()); std::vector<Node> deps = (*d_deps.find(n)).second; @@ -312,7 +314,9 @@ void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) { Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl; return; } - InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str()); + InternalError() + << "Cannot trace dependence information back to input assertion:\n`" + << n << "'"; } Assert(d_deps.find(n) != d_deps.end()); std::vector<Node> deps = (*d_deps.find(n)).second; @@ -327,7 +331,7 @@ void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) { } void ProofManager::traceUnsatCore() { - Assert (options::unsatCores()); + Assert(options::unsatCores()); d_satProof->refreshProof(); IdToSatClause used_lemmas; IdToSatClause used_inputs; @@ -375,8 +379,9 @@ void ProofManager::constructSatProof() { } void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) { - Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off"); - Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" ); + Assert(PROOF_ON()) << "Cannot compute unsat core when proofs are off"; + Assert(unsatCoreAvailable()) + << "Cannot get unsat core at this time. Mabye the input is SAT?"; constructSatProof(); @@ -425,8 +430,9 @@ std::set<Node> ProofManager::satClauseToNodeSet(prop::SatClause* clause) { } Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { - Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off"); - Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" ); + Assert(PROOF_ON()) << "Cannot compute unsat core when proofs are off"; + Assert(unsatCoreAvailable()) + << "Cannot get unsat core at this time. Mabye the input is SAT?"; // If we're doing aggressive minimization, work on all lemmas, not just conjunctions. if (!options::aggressiveCoreMin() && (lemma.getKind() != kind::AND)) @@ -531,7 +537,7 @@ void ProofManager::addDependence(TNode n, TNode dep) { } void ProofManager::addUnsatCore(Expr formula) { - Assert (d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end()); + Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end()); d_outputCoreFormulas.insert(formula); } @@ -912,7 +918,8 @@ void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) const for (rewrite = rewrites.begin(); rewrite != rewrites.end(); ++rewrite) { Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite << std::endl; if (ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())) { - Assert(ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())); + Assert( + ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())); Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl << "\tAdding filter: " << ProofManager::getPreprocessedAssertionName(*rewrite, "") @@ -947,7 +954,8 @@ Node ProofManager::mkOp(TNode n) { Node& op = d_ops[n]; if(op.isNull()) { - Assert((n.getConst<Kind>() == kind::SELECT) || (n.getConst<Kind>() == kind::STORE)); + Assert((n.getConst<Kind>() == kind::SELECT) + || (n.getConst<Kind>() == kind::STORE)); Debug("mgd-pm-mkop") << "making an op for " << n << "\n"; @@ -1036,12 +1044,12 @@ std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) { } void ProofManager::registerRewrite(unsigned ruleId, Node original, Node result){ - Assert (currentPM()->d_theoryProof != NULL); + Assert(currentPM()->d_theoryProof != NULL); currentPM()->d_rewriteLog.push_back(RewriteLogEntry(ruleId, original, result)); } void ProofManager::clearRewriteLog() { - Assert (currentPM()->d_theoryProof != NULL); + Assert(currentPM()->d_theoryProof != NULL); currentPM()->d_rewriteLog.clear(); } diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp index 449e12225..aa2175e66 100644 --- a/src/proof/proof_output_channel.cpp +++ b/src/proof/proof_output_channel.cpp @@ -17,7 +17,7 @@ #include "proof/proof_output_channel.h" -#include "base/cvc4_assert.h" +#include "base/check.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" @@ -55,8 +55,8 @@ theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, // following assertion cannot be enabled due to // "test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt". // Assert( - // d_lemma.isNull(), - // "Multiple calls to ProofOutputChannel::lemma() are not supported."); + // d_lemma.isNull()) << + // "Multiple calls to ProofOutputChannel::lemma() are not supported."; d_lemma = n; return theory::LemmaStatus(TNode::null(), 0); } diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index cb509063d..66e20069d 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -107,7 +107,7 @@ inline unsigned getSize(Type type) { inline unsigned getSize(Expr node) { - Assert (node.getType().isBitVector()); + Assert(node.getType().isBitVector()); return getSize(node.getType()); } @@ -147,7 +147,7 @@ inline Expr mkConst(const BitVector& value) { inline Expr mkOr(const std::vector<Expr>& nodes) { std::set<Expr> all; all.insert(nodes.begin(), nodes.end()); - Assert(all.size() != 0 ); + Assert(all.size() != 0); if (all.size() == 1) { // All the same, or just one @@ -220,8 +220,7 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) { }/* mkSortedNode() */ inline const bool getBit(Expr expr, unsigned i) { - Assert (i < utils::getSize(expr) && - expr.isConst()); + Assert(i < utils::getSize(expr) && expr.isConst()); Integer bit = expr.getConst<BitVector>().extract(i, i).getValue(); return (bit == 1u); } diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp index 505500d5e..f4ced1748 100644 --- a/src/proof/resolution_bitvector_proof.cpp +++ b/src/proof/resolution_bitvector_proof.cpp @@ -513,9 +513,9 @@ void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, void LfscResolutionBitVectorProof::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"); + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + << "the BV theory should only be proving bottom directly in the eager " + "bitblasting mode"; proof::LFSCProofPrinter::printResolutionEmptyClause( d_resolutionProof.get(), os, paren); } diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp index b0397d08c..44ca08fa6 100644 --- a/src/proof/skolemization_manager.cpp +++ b/src/proof/skolemization_manager.cpp @@ -37,13 +37,14 @@ bool SkolemizationManager::hasSkolem(Node disequality) { Node SkolemizationManager::getSkolem(Node disequality) { Debug("pf::pm") << "SkolemizationManager: getSkolem( "; - Assert (d_disequalityToSkolem.find(disequality) != d_disequalityToSkolem.end()); + Assert(d_disequalityToSkolem.find(disequality) + != d_disequalityToSkolem.end()); Debug("pf::pm") << disequality << " ) = " << d_disequalityToSkolem[disequality] << std::endl; return d_disequalityToSkolem[disequality]; } Node SkolemizationManager::getDisequality(Node skolem) { - Assert (d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end()); + Assert(d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end()); return d_skolemToDisequality[skolem]; } diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index c66aa59e4..1f3e6abf1 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -16,7 +16,7 @@ **/ #include "proof/theory_proof.h" -#include "base/cvc4_assert.h" +#include "base/check.h" #include "context/context.h" #include "options/bv_options.h" #include "options/proof_options.h" @@ -103,7 +103,9 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { bvp = new proof::LfscErBitVectorProof(thBv, this); break; } - default: { Unreachable("Invalid BvProofFormat"); + default: + { + Unreachable() << "Invalid BvProofFormat"; } }; d_theoryProofTable[id] = bvp; @@ -154,9 +156,9 @@ TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) { } if (d_theoryProofTable.find(id) == d_theoryProofTable.end()) { - std::stringstream ss; - ss << "Error! Proofs not yet supported for the following theory: " << id << std::endl; - InternalError(ss.str().c_str()); + InternalError() + << "Error! Proofs not yet supported for the following theory: " << id + << std::endl; } return d_theoryProofTable[id]; @@ -221,7 +223,7 @@ theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* cla Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); Expr atom = node.toExpr(); if (atom.isConst()) { - Assert (atom == utils::mkTrue()); + Assert(atom == utils::mkTrue()); continue; } @@ -229,7 +231,7 @@ theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* cla } // Ensure that the lemma is in the database. - Assert (pm->getCnfProof()->haveProofRecipe(nodes)); + Assert(pm->getCnfProof()->haveProofRecipe(nodes)); return pm->getCnfProof()->getProofRecipe(nodes).getTheory(); } @@ -257,7 +259,7 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { Expr current_expr = let_order[i].expr; unsigned let_id = let_order[i].id; ProofLetMap::const_iterator it = map.find(current_expr); - Assert (it != map.end()); + Assert(it != map.end()); unsigned let_count = it->second.count; Assert(let_count); // skip terms that only appear once @@ -387,8 +389,8 @@ void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, Node n1 = it->first; Node n2 = it->second; - Assert(n1.toExpr() == utils::mkFalse() || - theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); + Assert(n1.toExpr() == utils::mkFalse() + || theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); std::ostringstream rewriteRule; rewriteRule << ".lrr" << d_assertionToRewrite.size(); @@ -462,7 +464,7 @@ void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) { prop::SatLiteral lit = (*clause)[i]; Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); if (node.isConst()) { - Assert (node.toExpr() == utils::mkTrue()); + Assert(node.toExpr() == utils::mkTrue()); continue; } nodes.insert(lit.isNegated() ? node.notNode() : node); @@ -493,8 +495,8 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std // The literals (true) and (not false) are omitted from conflicts if (atom.isConst()) { - Assert (atom == utils::mkTrue() || - (atom == utils::mkFalse() && lit.isNegated())); + Assert(atom == utils::mkTrue() + || (atom == utils::mkFalse() && lit.isNegated())); continue; } @@ -584,7 +586,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, ProofManager::getBitVectorProof()->printBBDeclarationAndCnf(os, paren, map); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - Assert (lemmas.size() == 1); + Assert(lemmas.size() == 1); // nothing more to do (no combination with eager so far) return; } @@ -606,7 +608,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); Expr atom = node.toExpr(); if (atom.isConst()) { - Assert (atom == utils::mkTrue()); + Assert(atom == utils::mkTrue()); continue; } Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom; @@ -922,7 +924,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro case kind::DISTINCT: // Distinct nodes can have any number of chidlren. - Assert (term.getNumChildren() >= 2); + Assert(term.getNumChildren() >= 2); if (term.getNumChildren() == 2) { os << "(not (= "; @@ -999,8 +1001,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro return; } - default: - Unhandled(k); + default: Unhandled() << k; } } @@ -1010,7 +1011,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& paren, const ProofLetMap& map) { // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory - Assert(d_theory!=NULL); + Assert(d_theory != NULL); context::UserContext fakeContext; ProofOutputChannel oc; @@ -1032,7 +1033,8 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, os << " (clausify_false trust)"; return; } else { - InternalError(std::string("can't generate theory-proof for ") + ProofManager::currentPM()->getLogic()); + InternalError() << "can't generate theory-proof for " + << ProofManager::currentPM()->getLogic(); } Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->ProduceProofs()" << std::endl; @@ -1122,7 +1124,7 @@ BooleanProof::BooleanProof(TheoryProofEngine* proofEngine) {} void BooleanProof::registerTerm(Expr term) { - Assert (term.getType().isBoolean()); + Assert(term.getType().isBoolean()); if (term.isVariable() && d_declarations.find(term) == d_declarations.end()) { d_declarations.insert(term); @@ -1149,7 +1151,7 @@ void LFSCBooleanProof::printConstantDisequalityProof(std::ostream& os, Expr c1, } void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { - Assert (term.getType().isBoolean()); + Assert(term.getType().isBoolean()); if (term.isVariable()) { os << ProofManager::sanitize(term); return; @@ -1224,14 +1226,13 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe os << (term.getConst<bool>() ? "true" : "false"); return; - default: - Unhandled(k); + default: Unhandled() << k; } } void LFSCBooleanProof::printOwnedSort(Type type, std::ostream& os) { - Assert (type.isBoolean()); + Assert(type.isBoolean()); os << "Bool"; } @@ -1262,7 +1263,7 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) { - Unreachable("No boolean lemmas yet!"); + Unreachable() << "No boolean lemmas yet!"; } bool LFSCBooleanProof::printsAsBool(const Node &n) diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 10823693d..b88f7dc33 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -119,7 +119,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, } else if (n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE) { out << ss.str() << " " << ProofManager::getLitName(n2[0]) << "))"; } else { - Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); + Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) + || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); if(n1[1] == n2[0][0]) { out << "(symm _ _ _ " << ss.str() << ")"; } else { @@ -130,7 +131,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, } else { Node n2 = pf.d_node; Assert(n2.getKind() == kind::EQUAL); - Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1])); + Assert((n1[0] == n2[0] && n1[1] == n2[1]) + || (n1[1] == n2[0] && n1[0] == n2[1])); out << ss.str(); out << " "; @@ -160,7 +162,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, out << "(cong _ _ _ _ _ _ "; stk.push(pf2); } - Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE); + Assert(stk.top()->d_children[0]->d_id + != theory::eq::MERGED_THROUGH_CONGRUENCE); NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); const theory::eq::EqProof* pf2 = stk.top(); stk.pop(); @@ -231,7 +234,12 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, b2 << n2[1-side]; out << ss.str(); } else { - Assert(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]); + Assert(pf2->d_node[b1.getNumChildren() + - (pf2->d_node.getMetaKind() + == kind::metakind::PARAMETERIZED + ? 0 + : 1)] + == n2[1 - side]); b1 << n2[1-side]; b2 << n2[side]; out << "(symm _ _ _ " << ss.str() << ")"; @@ -258,7 +266,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, b2 << n2[1-side]; out << ss.str(); } else { - Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]); + Assert(pf2->d_node[b1.getNumChildren()] == n2[1 - side]); b1 << n2[1-side]; b2 << n2[side]; out << "(symm _ _ _ " << ss.str() << ")"; @@ -618,7 +626,7 @@ void UFProof::registerTerm(Expr term) { void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl; - Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF); + Assert(theory::Theory::theoryOf(term) == theory::THEORY_UF); if (term.getKind() == kind::VARIABLE || term.getKind() == kind::SKOLEM || @@ -627,7 +635,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& return; } - Assert (term.getKind() == kind::APPLY_UF); + Assert(term.getKind() == kind::APPLY_UF); if(term.getType().isBoolean()) { os << "(p_app "; @@ -653,7 +661,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) { Debug("pf::uf") << std::endl << "(pf::uf) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl; - Assert (type.isSort()); + Assert(type.isSort()); os << type; } @@ -705,7 +713,7 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { } os << fparen.str() << "))\n"; } else { - Assert (term.isVariable()); + Assert(term.isVariable()); os << type << ")\n"; } paren << ")"; diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index 4212331af..0776197cb 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -16,7 +16,7 @@ #include "proof/unsat_core.h" -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/expr_iomanip.h" #include "options/base_options.h" #include "printer/printer.h" |