diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
commit | dc3f45d6e41bdd4e52e39b0c6fecae3148a2944c (patch) | |
tree | 7516d3d5d43f0dadb943bb186615e0903cbd9f7f /src/proof/sat_proof_implementation.h | |
parent | 74bf9ff63f5566fbe1b5db9124f9dc1fde65cb82 (diff) | |
parent | 6b355496aaf27d46d6a33402814753589b755842 (diff) |
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
-rw-r--r-- | src/proof/sat_proof_implementation.h | 29 |
1 files changed, 21 insertions, 8 deletions
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 1e01e4dce..603559da1 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -224,6 +224,7 @@ TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name, d_seenLearnt(), d_seenInputs(), d_seenLemmas(), + d_satProofConstructed(false), d_statistics(name) { d_proxy = new ProofProxy<Solver>(this); } @@ -957,10 +958,16 @@ void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) { template <class Solver> void TSatProof<Solver>::constructProof(ClauseId conflict) { + d_satProofConstructed = true; collectClauses(conflict); } template <class Solver> +bool TSatProof<Solver>::proofConstructed() const { + return d_satProofConstructed; +} + +template <class Solver> std::string TSatProof<Solver>::clauseName(ClauseId id) { std::ostringstream os; if (isInputClause(id)) { @@ -998,6 +1005,11 @@ prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) { } template <class Solver> +bool TSatProof<Solver>::derivedEmptyClause() const { + return hasResolutionChain(d_emptyClauseId); +} + +template <class Solver> void TSatProof<Solver>::collectClauses(ClauseId id) { if (d_seenInputs.find(id) != d_seenInputs.end() || d_seenLemmas.find(id) != d_seenLemmas.end() || @@ -1080,33 +1092,34 @@ TSatProof<Solver>::Statistics::~Statistics() { template <class Solver> void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { - out << "(satlem_simplify _ _ _ "; + out << "(satlem_simplify _ _ _"; + paren << ")"; const ResChain<Solver>& res = this->getResolutionChain(id); const typename ResChain<Solver>::ResSteps& steps = res.getSteps(); for (int i = steps.size() - 1; i >= 0; i--) { - out << "("; - out << (steps[i].sign ? "R" : "Q") << " _ _ "; + out << " ("; + out << (steps[i].sign ? "R" : "Q") << " _ _"; } ClauseId start_id = res.getStart(); - out << this->clauseName(start_id) << " "; + out << " " << this->clauseName(start_id); for (unsigned i = 0; i < steps.size(); i++) { prop::SatVariable v = prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); - out << this->clauseName(steps[i].id) << " " + out << " " << this->clauseName(steps[i].id) << " " << ProofManager::getVarName(v, this->d_name) << ")"; } if (id == this->d_emptyClauseId) { - out <<"(\\ empty empty)"; + out <<" (\\ empty empty)"; return; } - out << "(\\ " << this->clauseName(id) << "\n"; // bind to lemma name - paren << "))"; // closing parethesis for lemma binding and satlem + out << " (\\ " << this->clauseName(id) << "\n"; // bind to lemma name + paren << ")"; } /// LFSCSatProof class |