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/uf_proof.cpp | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/proof/uf_proof.cpp')
-rw-r--r-- | src/proof/uf_proof.cpp | 26 |
1 files changed, 17 insertions, 9 deletions
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 << ")"; |