Fix missing/redundant spaces in proofs

Before, in some cases, e.g. when printing sorts and in resolution
proofs, the proofs contained redundant and/or missing spaces. With this
commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10
let12)` instead of `(trust_f (= (Array Index  Element )let10 let12))`.

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 100f606009be372e9d2a695fdc32421a77ce20fb..4e813d6462680c6b6f1d0b774ea4f56582a406c7 100644 (file)
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -804,9 +804,9 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
 
   if (type.isInteger() && d_realMode) {
     // If in "real mode", don't use type Int for, e.g., equality.
-    os << "Real ";
+    os << "Real";
   } else {
-    os << type << " ";
+    os << type;
   }
 }
 

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 514d8118455b5f96085540ecda019cff16ecfb15..32a7c247d06064f9f811e6bc7a093b4c9dea0e42 100644 (file)
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -1271,7 +1271,7 @@ void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) {
     printSort(array_type.getConstituentType(), os);
     os << ")";
   } else {
-    os << type <<" ";
+    os << type;
   }
 }
 

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 49e0e8e2f16728d37c88375e3889076662cee3e2..cbe54ff4ba421990bc1efd830bd1095138840c82 100644 (file)
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -479,7 +479,7 @@ void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) {
   Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl;
   Assert (type.isBitVector());
   unsigned width = utils::getSize(type);
-  os << "(BitVec "<<width<<")";
+  os << "(BitVec " << width << ")";
 }
 
 void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {

diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 76b5efbe6723cccb65581e934fd83e16040af9b8..603559da108e5b72141b3be47eab1cb41537d449 100644 (file)
--- 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 << ")";
 }
 

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 8aefaae45f406367abfa0689acf8133c3586d1ad..d29fc86154551bb5165f6857262f04db303e8c93 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -861,6 +861,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
     os << "(";
     os << "= ";
     printSort(term[0].getType(), os);
+    os << " ";
     printBoundTerm(term[0], os, map);
     os << " ";
     printBoundTerm(term[1], os, map);
@@ -874,6 +875,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
     if (term.getNumChildren() == 2) {
       os << "(not (= ";
       printSort(term[0].getType(), os);
+      os << " ";
       printBoundTerm(term[0], os, map);
       os << " ";
       printBoundTerm(term[1], os, map);
@@ -889,6 +891,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
           if ((i != 0) || (j != 1)) {
             os << "(not (= ";
             printSort(term[0].getType(), os);
+            os << " ";
             printBoundTerm(term[i], os, map);
             os << " ";
             printBoundTerm(term[j], os, map);
@@ -896,6 +899,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
           } else {
             os << "(not (= ";
             printSort(term[0].getType(), os);
+            os << " ";
             printBoundTerm(term[0], os, map);
             os << " ";
             printBoundTerm(term[1], os, map);

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 17faf0f7dbb24159afff87cd628cb38f0429a998..27f35110208b999c161b6bb245e531e5cb23f5f2 100644 (file)
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -733,7 +733,7 @@ void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
   Debug("pf::uf") << std::endl << "(pf::uf) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
 
   Assert (type.isSort());
-  os << type <<" ";
+  os << type;
 }
 
 void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {