diff options
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
-rw-r--r-- | src/proof/sat_proof_implementation.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 76b5efbe6..603559da1 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -1092,33 +1092,33 @@ 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 + out << " (\\ " << this->clauseName(id) << "\n"; // bind to lemma name paren << ")"; } |