diff options
| -rw-r--r-- | src/proof/array_proof.cpp | 4 | ||||
| -rw-r--r-- | src/proof/proof_manager.cpp | 13 | ||||
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 3 |
3 files changed, 9 insertions, 11 deletions
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index ccc072eca..514d81184 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -1324,6 +1324,7 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren printSort(array_type.getConstituentType(), os); os << "))\n"; + paren << ")"; } else { Assert(term.isVariable()); if (ProofManager::getSkolemizationManager()->isSkolem(*it)) { @@ -1333,10 +1334,9 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren os << "(% " << ProofManager::sanitize(term) << " "; os << "(term "; os << term.getType() << ")\n"; + paren << ")"; } } - - paren << ")"; } Debug("pf::array") << "Declaring terms done!" << std::endl; diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 42319153f..e987f1c6f 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -596,6 +596,7 @@ void LFSCProof::toStream(std::ostream& out) { smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; + paren << ")"; out << " ;; Declarations\n"; // declare the theory atoms @@ -618,6 +619,7 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << std::endl << "LFSCProof::toStream: print assertions DONE" << std::endl; out << "(: (holds cln)\n\n"; + paren << ")"; // Have the theory proofs print deferred declarations, e.g. for skolem variables. out << " ;; Printing deferred declarations \n\n"; @@ -659,20 +661,15 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { - // print actual resolution proof - // d_satProof->printResolutions(out, paren); ProofManager::getBitVectorProof()->getSatProof()->printResolutionEmptyClause(out, paren); - paren <<")))\n;;"; - out << paren.str(); - out << "\n"; } else { // print actual resolution proof d_satProof->printResolutions(out, paren); d_satProof->printResolutionEmptyClause(out, paren); - paren <<")))\n;;"; - out << paren.str(); - out << "\n"; } + + out << paren.str(); + out << "\n;;\n"; } void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index fc2bae19b..76b5efbe6 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -1093,6 +1093,7 @@ template <class Solver> void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { out << "(satlem_simplify _ _ _ "; + paren << ")"; const ResChain<Solver>& res = this->getResolutionChain(id); const typename ResChain<Solver>::ResSteps& steps = res.getSteps(); @@ -1118,7 +1119,7 @@ void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, } out << "(\\ " << this->clauseName(id) << "\n"; // bind to lemma name - paren << "))"; // closing parethesis for lemma binding and satlem + paren << ")"; } /// LFSCSatProof class |