summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/array_proof.cpp8
-rw-r--r--src/proof/clausal_bitvector_proof.cpp8
-rw-r--r--src/proof/drat/drat_proof.cpp12
-rw-r--r--src/proof/proof_manager.cpp6
-rw-r--r--src/proof/resolution_bitvector_proof.cpp10
-rw-r--r--src/proof/sat_proof_implementation.h4
-rw-r--r--src/proof/theory_proof.cpp2
-rw-r--r--src/proof/uf_proof.cpp8
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]))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback