diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/array_proof.cpp | 8 | ||||
-rw-r--r-- | src/proof/clausal_bitvector_proof.cpp | 8 | ||||
-rw-r--r-- | src/proof/drat/drat_proof.cpp | 12 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 6 | ||||
-rw-r--r-- | src/proof/resolution_bitvector_proof.cpp | 10 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 4 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 2 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 8 |
8 files changed, 25 insertions, 33 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 75b7b7f1b..32dcaf5b2 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -475,7 +475,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node); Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); - Node n2; Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n"; @@ -489,7 +488,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, std::map<size_t, Node> childToStream; - std::stringstream ss1(ss.str()), ss2; std::pair<Node, Node> nodePair; for (size_t i = 1; i < pf.d_children.size(); ++i) { @@ -562,9 +560,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, while (j < pf.d_children.size() && !sequenceOver) { - std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC( - dontCare, tp, *(pf.d_children[j]), tb + 1, map); + std::stringstream ignore; + nodeAfterEqualitySequence = + toStreamRecLFSC(ignore, tp, *(pf.d_children[j]), tb + 1, map); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || ((nodeAfterEqualitySequence[0] == n1[1]) diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index 6b0a57725..6a5009b1f 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -196,11 +196,11 @@ void ClausalBitVectorProof::optimizeDratProof() if (options::bvOptimizeSatProof() == options::BvOptimizeSatProof::FORMULA) { - std::ifstream optFormulaStream{optFormulaFilename}; - const int64_t startPos = static_cast<int64_t>(optFormulaStream.tellg()); - std::vector<prop::SatClause> core = parseDimacs(optFormulaStream); + std::ifstream optFormulaInStream{optFormulaFilename}; + const int64_t startPos = static_cast<int64_t>(optFormulaInStream.tellg()); + std::vector<prop::SatClause> core = parseDimacs(optFormulaInStream); d_dratOptimizationStatistics.d_optimizedFormulaSize.setData( - static_cast<int64_t>(optFormulaStream.tellg()) - startPos); + static_cast<int64_t>(optFormulaInStream.tellg()) - startPos); CodeTimer clauseMatchingTimer{ d_dratOptimizationStatistics.d_clauseMatchingTime}; diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp index 162efc3e5..e35741cde 100644 --- a/src/proof/drat/drat_proof.cpp +++ b/src/proof/drat/drat_proof.cpp @@ -215,12 +215,12 @@ DratProof DratProof::fromBinary(const std::string& s) } default: { - std::ostringstream s; - s << "Invalid instruction in Drat proof. Instruction bits: " - << std::bitset<8>(*i) - << ". Expected 'a' (01100001) or 'd' " - "(01100100)."; - throw InvalidDratProofException(s.str()); + std::ostringstream errmsg; + errmsg << "Invalid instruction in Drat proof. Instruction bits: " + << std::bitset<8>(*i) + << ". Expected 'a' (01100001) or 'd' " + "(01100100)."; + throw InvalidDratProofException(errmsg.str()); } } } diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index fda3f7424..33f284bf8 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -682,11 +682,9 @@ void LFSCProof::toStream(std::ostream& out) const d_cnfProof->collectAtomsForClauses(used_lemmas, atoms); // collects the atoms in the assertions - for (NodeSet::const_iterator it = used_assertions.begin(); - it != used_assertions.end(); - ++it) + for (TNode used_assertion : used_assertions) { - utils::collectAtoms(*it, atoms); + utils::collectAtoms(used_assertion, atoms); } std::set<Node>::iterator atomIt; diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp index 8d4b56d54..120397d08 100644 --- a/src/proof/resolution_bitvector_proof.cpp +++ b/src/proof/resolution_bitvector_proof.cpp @@ -366,10 +366,8 @@ void LfscResolutionBitVectorProof::printTheoryLemmaProof( if (possibleMatch.getKind() == kind::OR) { - for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) + for (const Expr& lit : possibleMatch) { - Expr lit = possibleMatch[i]; - if (lit.getKind() == kind::NOT) { os << "(intro_assump_t _ _ _ "; @@ -434,13 +432,13 @@ void LfscResolutionBitVectorProof::printTheoryLemmaProof( // conflict has a FALSE assertion in it; this can happen in some corner // cases, where the FALSE is the result of a rewrite. - for (unsigned i = 0; i < lemma.size(); ++i) + for (const Expr& lit : lemma) { - if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) + if (lit.getKind() == kind::NOT && lit[0] == utils::mkFalse()) { Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl; os << "(clausify_false "; - os << ProofManager::getLitName(lemma[i]); + os << ProofManager::getLitName(lit); os << ")"; return; } diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index d9c959ae4..8c65d42e7 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -285,8 +285,8 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { typename Solver::TLit var = steps[i].lit; LitSet clause2; createLitSet(steps[i].id, clause2); - bool res = resolve<Solver>(var, clause1, clause2, steps[i].sign); - if (res == false) { + if (!resolve<Solver>(var, clause1, clause2, steps[i].sign)) + { validRes = false; break; } diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 7e2ed84b1..e746a6315 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1026,7 +1026,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, for (unsigned i = 0; i < term.getNumChildren(); ++i) { for (unsigned j = i + 1; j < term.getNumChildren(); ++j) { - TypeNode armType = equalityType(term[i], term[j]); + armType = equalityType(term[i], term[j]); if ((i != 0) || (j != 1)) { os << "(not (= "; printSort(term[0].getType(), os); diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 214198756..225cb6aa4 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -337,7 +337,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n"; - Node n2; if(tb == 1) { Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n"; } @@ -349,7 +348,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, toStreamRecLFSC(dontCare, tp, *(pf.d_children[0]), tb + 1, map); std::map<size_t, Node> childToStream; - std::stringstream ss1(ss.str()), ss2; std::pair<Node, Node> nodePair; for(size_t i = 1; i < pf.d_children.size(); ++i) { std::stringstream ss1(ss.str()), ss2; @@ -410,9 +408,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, while (j < pf.d_children.size() && !sequenceOver) { - std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC( - dontCare, tp, *(pf.d_children[j]), tb + 1, map); + std::stringstream ignore; + nodeAfterEqualitySequence = + toStreamRecLFSC(ignore, tp, *(pf.d_children[j]), tb + 1, map); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) |