From: Andres Notzli <andres.noetzli@gmail.com>
Date: Tue, 9 Aug 2016 03:33:24 +0000 (-0700)
Subject: Fix missing/redundant spaces in proofs
X-Git-Tag: cvc5-1.0.0~6040^2~10^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0610224d0eeab12fd4f779e01b5fdd36c57b304;p=cvc5.git

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 100f60600..4e813d646 100644
--- 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 514d81184..32a7c247d 100644
--- 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 49e0e8e2f..cbe54ff4b 100644
--- 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 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 << ")";
 }
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 8aefaae45..d29fc8615 100644
--- 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 17faf0f7d..27f351102 100644
--- 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) {