changed some files to fit into 80 characters terminal

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@310 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index 3eb9dbffa9ab13263c3e5035f3a17ace093981de..b48b96b4a2f63bfd0ac123e0dbc9cd4a3d1018a5 100644 (file)
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -152,9 +152,9 @@ namespace BEEV
   }
 
   // I don't think this is even called, since it called
-  // CreateSimpAndOr instead of CreateSimpXor until 1/9/07 with no
-  // ill effects.  Calls seem to go to the version that takes a vector
-  // of children.
+  // CreateSimpAndOr instead of CreateSimpXor until 1/9/07 with no ill
+  // effects.  Calls seem to go to the version that takes a vector of
+  // children.
   ASTNode STPMgr::CreateSimpXor(const ASTNode& form1, const ASTNode& form2)
   {
     ASTVec children;

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 667479bf0bf050c06aef852158bf0c6c8a2258ae..c0d84152ca4cf06303a505eaf9b58b40d849e476 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -401,7 +401,8 @@ namespace BEEV
     return psi;
   } //End of SINGLETON()
 
-  ClauseList* CNFMgr::UNION(const ClauseList& varphi1, const ClauseList& varphi2)
+  ClauseList* CNFMgr::UNION(const ClauseList& varphi1, 
+                           const ClauseList& varphi2)
   {    
     ClauseList* psi1 = COPY(varphi1);
     ClauseList* psi2 = COPY(varphi2);
@@ -411,20 +412,23 @@ namespace BEEV
     return psi1;    
   } //End of UNION()
 
-  void CNFMgr::INPLACE_UNION(ClauseList* varphi1, const ClauseList& varphi2)
+  void CNFMgr::INPLACE_UNION(ClauseList* varphi1, 
+                            const ClauseList& varphi2)
   {    
     ClauseList* psi2 = COPY(varphi2);
     varphi1->insert(varphi1->end(), psi2->begin(), psi2->end());
     delete psi2;
   } //End of INPLACE_UNION()
 
-  void CNFMgr::NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2)
+  void CNFMgr::NOCOPY_INPLACE_UNION(ClauseList* varphi1, 
+                                   ClauseList* varphi2)
   {    
     varphi1->insert(varphi1->end(), varphi2->begin(), varphi2->end());
     delete varphi2;
   } //End of NOCOPY_INPLACE_UNION
 
-  ClauseList* CNFMgr::PRODUCT(const ClauseList& varphi1, const ClauseList& varphi2)
+  ClauseList* CNFMgr::PRODUCT(const ClauseList& varphi1, 
+                             const ClauseList& varphi2)
   {    
     ClauseList* psi = new ClauseList();
     psi->reserve(varphi1.size() * varphi2.size());
@@ -807,7 +811,8 @@ namespace BEEV
   //########################################
   //main switch for individual cnf conversion cases
 
-  void CNFMgr::convertFormulaToCNFPosCases(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosCases(const ASTNode& varphi, 
+                                          ClauseList* defs)
   {
     if (isPred(varphi))
       {
@@ -880,13 +885,15 @@ namespace BEEV
         }
       default:
         {
-          fprintf(stderr, "convertFormulaToCNFPosCases: doesn't handle kind %d\n", k);
+          fprintf(stderr, "convertFormulaToCNFPosCases: "\
+                 "doesn't handle kind %d\n", k);
           FatalError("");
         }
       }
   } //End of convertFormulaToCNFPosCases()
 
-  void CNFMgr::convertFormulaToCNFNegCases(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegCases(const ASTNode& varphi, 
+                                          ClauseList* defs)
   {
 
     if (isPred(varphi))
@@ -960,7 +967,8 @@ namespace BEEV
         }
       default:
         {
-          fprintf(stderr, "convertFormulaToCNFNegCases: doesn't handle kind %d\n", k);
+          fprintf(stderr, "convertFormulaToCNFNegCases: "\
+                 "doesn't handle kind %d\n", k);
           FatalError("");
         }
       }
@@ -970,7 +978,8 @@ namespace BEEV
   //########################################
   // individual cnf conversion cases
 
-  void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi,
+                                         ClauseList* defs)
   {
     ASTVec psis;
 
@@ -981,39 +990,47 @@ namespace BEEV
         psis.push_back(*(info[*it]->termforcnf));
       }
 
-    info[varphi]->clausespos = SINGLETON(bm->CreateNode(varphi.GetKind(), psis));
+    info[varphi]->clausespos = 
+      SINGLETON(bm->CreateNode(varphi.GetKind(), psis));
   } //End of convertFormulaToCNFPosPred()
 
-  void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi,
+                                          ClauseList* defs)
   {
-    ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
+    ASTNode dummy_false_var = 
+      bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
     info[varphi]->clausespos = SINGLETON(dummy_false_var);
   } //End of convertFormulaToCNFPosFALSE()
 
-  void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, 
+                                         ClauseList* defs)
   {
     ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
     info[varphi]->clausespos = SINGLETON(dummy_true_var);
   } //End of convertFormulaToCNFPosTRUE
 
-  void CNFMgr::convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, 
+                                             ClauseList* defs)
   {
     info[varphi]->clausespos = SINGLETON(varphi);
   }//End of convertFormulaToCNFPosBVGETBIT()
 
-  void CNFMgr::convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, 
+                                           ClauseList* defs)
   {
     info[varphi]->clausespos = SINGLETON(varphi);
   } //End of convertFormulaToCNFPosSYMBOL()
 
-  void CNFMgr::convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosNOT(const ASTNode& varphi, 
+                                        ClauseList* defs)
   {
     convertFormulaToCNF(varphi[0], defs);
     info[varphi]->clausespos = COPY(*(info[varphi[0]]->clausesneg));
     reduceMemoryFootprintNeg(varphi[0]);
   } //End of convertFormulaToCNFPosNOT()
 
-  void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, 
+                                        ClauseList* defs)
   {
     //****************************************
     // (pos) AND ~> UNION
@@ -1031,7 +1048,8 @@ namespace BEEV
     info[varphi]->clausespos = psi;
   } //End of convertFormulaToCNFPosAND()
 
-  void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, 
+                                         ClauseList* defs)
   {
     bool renamesibs = false;
     ClauseList* clauses;
@@ -1073,7 +1091,8 @@ namespace BEEV
     info[varphi]->clausespos = psi;
   } //End of convertFormulaToCNFPosNAND()
 
-  void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi, 
+                                       ClauseList* defs)
   {
     bool renamesibs = false;
     ClauseList* clauses;
@@ -1114,7 +1133,8 @@ namespace BEEV
     info[varphi]->clausespos = psi;
   } //End of convertFormulaToCNFPosOR()
 
-  void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi, 
+                                        ClauseList* defs)
   {
     //****************************************
     // (pos) NOR ~> UNION NOT
@@ -1133,7 +1153,8 @@ namespace BEEV
     info[varphi]->clausespos = psi;
   } //End of convertFormulaToCNFPosNOR()
 
-  void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, 
+                                            ClauseList* defs)
   {
     //****************************************
     // (pos) IMPLIES ~> PRODUCT NOT [0] ; [1]
@@ -1152,7 +1173,8 @@ namespace BEEV
     info[varphi]->clausespos = psi;
   } //End of convertFormulaToCNFPosIMPLIES()
 
-  void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi, 
+                                        ClauseList* defs)
   {
     //****************************************
     // (pos) ITE ~> UNION (PRODUCT NOT [0] ; [1])
@@ -1183,7 +1205,8 @@ namespace BEEV
     info[varphi]->clausespos = psi1;
   } //End of convertFormulaToCNFPosITE()
 
-  void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, 
+                                        ClauseList* defs)
   {
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     for (; it != varphi.GetChildren().end(); it++)
@@ -1199,7 +1222,9 @@ namespace BEEV
     }
   } //End of convertFormulaToCNFPosXOR()
 
-  ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs)
+  ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, 
+                                                  unsigned int idx, 
+                                                  ClauseList* defs)
   {
 
     bool renamesibs;
@@ -1214,19 +1239,25 @@ namespace BEEV
         //    (PRODUCT       [idx]   ;     [idx+1])
         //  ; (PRODUCT NOT   [idx]   ; NOT [idx+1])
         //****************************************
-        renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
+        renamesibs = 
+         (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
         if (renamesibs)
           {
             setDoSibRenamingPos(*info[varphi[idx + 1]]);
           }
-        renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false;
+        renamesibs = 
+         (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false;
         if (renamesibs)
           {
             setDoSibRenamingNeg(*info[varphi[idx + 1]]);
           }
 
-        psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausespos));
-        psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausesneg));
+        psi1 = 
+         PRODUCT(*(info[varphi[idx]]->clausespos), 
+                 *(info[varphi[idx + 1]]->clausespos));
+        psi2 = 
+         PRODUCT(*(info[varphi[idx]]->clausesneg), 
+                 *(info[varphi[idx + 1]]->clausesneg));
         NOCOPY_INPLACE_UNION(psi1, psi2);
 
         psi = psi1;
@@ -1265,7 +1296,8 @@ namespace BEEV
     return psi;
   } //End of convertFormulaToCNFPosXORAux()
 
-  void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, 
+                                         ClauseList* defs)
   {
 
     ASTVec psis;
@@ -1277,40 +1309,49 @@ namespace BEEV
         psis.push_back(*(info[*it]->termforcnf));
       }
 
-    info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, bm->CreateNode(varphi.GetKind(), psis)));
+    info[varphi]->clausesneg = 
+      SINGLETON(bm->CreateNode(NOT,
+                              bm->CreateNode(varphi.GetKind(), psis)));
   } //End of convertFormulaToCNFNegPred()
 
-  void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, 
+                                          ClauseList* defs)
   {
     ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
     info[varphi]->clausesneg = SINGLETON(dummy_true_var);
   } //End of convertFormulaToCNFNegFALSE()
 
-  void CNFMgr::convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegTRUE(const ASTNode& varphi, 
+                                         ClauseList* defs)
   {
-    ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
+    ASTNode dummy_false_var = 
+      bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
     info[varphi]->clausesneg = SINGLETON(dummy_false_var);
   } //End of convertFormulaToCNFNegTRUE()
 
-  void CNFMgr::convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, 
+                                             ClauseList* defs)
   {
     ClauseList* psi = SINGLETON(bm->CreateNode(NOT, varphi));
     info[varphi]->clausesneg = psi;
   } //End of convertFormulaToCNFNegBVGETBIT()
 
-  void CNFMgr::convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegSYMBOL(const ASTNode& varphi,
+                                           ClauseList* defs)
   {
     info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, varphi));
   } //End of convertFormulaToCNFNegSYMBOL()
 
-  void CNFMgr::convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegNOT(const ASTNode& varphi,
+                                        ClauseList* defs)
   {
     convertFormulaToCNF(varphi[0], defs);
     info[varphi]->clausesneg = COPY(*(info[varphi[0]]->clausespos));
     reduceMemoryFootprintPos(varphi[0]);
   } //End of convertFormulaToCNFNegNOT()
 
-  void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi,
+                                        ClauseList* defs)
   {
     bool renamesibs = false;
     ClauseList* clauses;
@@ -1352,7 +1393,8 @@ namespace BEEV
     info[varphi]->clausesneg = psi;
   } //End of convertFormulaToCNFNegAND()
 
-  void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi,
+                                         ClauseList* defs)
   {
     //****************************************
     // (neg) NAND ~> UNION
@@ -1371,7 +1413,8 @@ namespace BEEV
     info[varphi]->clausespos = psi;
   } //End of convertFormulaToCNFNegNAND()
 
-  void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi,
+                                       ClauseList* defs)
   {
     //****************************************
     // (neg) OR ~> UNION NOT
@@ -1390,7 +1433,8 @@ namespace BEEV
     info[varphi]->clausesneg = psi;
   } //End of convertFormulaToCNFNegOR()
 
-  void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi,
+                                        ClauseList* defs)
   {
     bool renamesibs = false;
     ClauseList* clauses;
@@ -1431,7 +1475,8 @@ namespace BEEV
     info[varphi]->clausesneg = psi;
   } //End of convertFormulaToCNFNegNOR()
 
-  void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi,
+                                            ClauseList* defs)
   {
     //****************************************
     // (neg) IMPLIES ~> UNION [0] ; NOT [1]
@@ -1446,7 +1491,8 @@ namespace BEEV
     reduceMemoryFootprintNeg(varphi[1]);
   } //End of convertFormulaToCNFNegIMPLIES()
 
-  void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi,
+                                        ClauseList* defs)
   {
     //****************************************
     // (neg) ITE ~> UNION (PRODUCT NOT [0] ; NOT [1])
@@ -1477,7 +1523,8 @@ namespace BEEV
     info[varphi]->clausesneg = psi1;
   } //End of convertFormulaToCNFNegITE()
 
-  void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs)
+  void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi,
+                                        ClauseList* defs)
   {
     ASTVec::const_iterator it = varphi.GetChildren().begin();
     for (; it != varphi.GetChildren().end(); it++)
@@ -1493,7 +1540,9 @@ namespace BEEV
     }
   } //End of convertFormulaToCNFNegXOR()
 
-  ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs)
+  ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi,
+                                                  unsigned int idx, 
+                                                  ClauseList* defs)
   {
     bool renamesibs;
     ClauseList* psi;
@@ -1509,21 +1558,27 @@ namespace BEEV
         //  ; (PRODUCT       [idx]   ; NOT [idx+1])
         //****************************************
         convertFormulaToCNF(varphi[idx], defs);
-        renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false;
+        renamesibs = 
+         (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false;
         if (renamesibs)
           {
             setDoSibRenamingPos(*info[varphi[idx + 1]]);
           }
 
         convertFormulaToCNF(varphi[idx], defs);
-        renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
+        renamesibs =
+         (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
         if (renamesibs)
           {
             setDoSibRenamingNeg(*info[varphi[idx + 1]]);
           }
 
-        psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausespos));
-        psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausesneg));
+        psi1 = 
+         PRODUCT(*(info[varphi[idx]]->clausesneg),
+                 *(info[varphi[idx + 1]]->clausespos));
+        psi2 = 
+         PRODUCT(*(info[varphi[idx]]->clausespos),
+                 *(info[varphi[idx + 1]]->clausesneg));
         NOCOPY_INPLACE_UNION(psi1, psi2);
 
         psi = psi1;
@@ -1625,7 +1680,7 @@ namespace BEEV
   {
     delete info[varphi]->clausespos;
     CNFInfo* toDelete = info[varphi]; // get the thing to delete.
-    info.erase(varphi);                                 // remove it from the hashtable
+    info.erase(varphi);               // remove it from the hashtable
     delete toDelete;
 
 
@@ -1712,12 +1767,17 @@ namespace BEEV
   void CNFMgr::PrintClauseList(ostream& os, ClauseList& cll)
   {
     int num_clauses = cll.size();
-    os << "Clauses: " << endl << "=========================================" << endl;
+    os << "Clauses: " 
+       << endl 
+       << "=========================================" << endl;
     for (int i = 0; i < num_clauses; i++)
       {
-       os << "Clause " << i << endl << "-------------------------------------------" << endl;
+       os << "Clause " 
+          << i << endl 
+          << "-------------------------------------------" << endl;
        LispPrintVecSpecial(os, *cll[i], 0);
-       os << endl << "-------------------------------------------" << endl;
+       os << endl 
+          << "-------------------------------------------" << endl;
       }
   } //end of PrintClauseList()  
 } // end namespace BEEV

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index 843dc4bec433b952e1024243d80134e2a2efe9c2..abfde5de893025a257626288caaa6d43b1666164 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -135,7 +135,8 @@ namespace BEEV
 
     void NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2);   
 
-    ClauseList* PRODUCT(const ClauseList& varphi1, const ClauseList& varphi2);    
+    ClauseList* PRODUCT(const ClauseList& varphi1, 
+                       const ClauseList& varphi2);    
 
     //########################################
     //########################################
@@ -167,77 +168,53 @@ namespace BEEV
     //########################################
     //main switch for individual cnf conversion cases
 
-    void convertFormulaToCNFPosCases(const ASTNode& varphi, ClauseList* defs);    
-
+    void convertFormulaToCNFPosCases(const ASTNode& varphi, ClauseList* defs);
     void convertFormulaToCNFNegCases(const ASTNode& varphi, ClauseList* defs);
 
     //########################################
     //########################################
     // individual cnf conversion cases
 
-    void convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs);    
-
-    void convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs);    
-
-    void convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs);    
-
-    void convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, ClauseList* defs);    
-
-    void convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs);    
-
+    void convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs);
+    void convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs);  
+    void convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs);   
+    void convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, 
+                                       ClauseList* defs);    
+    void convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs);
     void convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs);    
-
     void convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs);    
-
-    void convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs);    
-
+    void convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs);   
     void convertFormulaToCNFPosOR(const ASTNode& varphi, ClauseList* defs);    
-
     void convertFormulaToCNFPosNOR(const ASTNode& varphi, ClauseList* defs);   
-
-    void convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs);    
-
+    void convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs);
     void convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs);    
-
     void convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs);    
-
-    ClauseList* convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs);    
-
-    void convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs);    
-
+    ClauseList* convertFormulaToCNFPosXORAux(const ASTNode& varphi, 
+                                            unsigned int idx, 
+                                            ClauseList* defs);    
+    void convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs);
     void convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs);
-    
-
-    void convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs);    
-
-    void convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, ClauseList* defs);    
-
-    void convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs);    
-
+    void convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs);   
+    void convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi,
+                                       ClauseList* defs);    
+    void convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs);
     void convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs);    
-
     void convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs);    
-
-    void convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs);    
-
+    void convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs);
     void convertFormulaToCNFNegOR(const ASTNode& varphi, ClauseList* defs);    
-
     void convertFormulaToCNFNegNOR(const ASTNode& varphi, ClauseList* defs);    
-
     void convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, ClauseList* defs);
-
     void convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs);    
-
     void convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs);    
-
-    ClauseList* convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs);    
+    ClauseList* convertFormulaToCNFNegXORAux(const ASTNode& varphi, 
+                                            unsigned int idx, 
+                                            ClauseList* defs);    
 
     //########################################
     //########################################
     // utilities for reclaiming memory.
 
     void reduceMemoryFootprintPos(const ASTNode& varphi);    
-
     void reduceMemoryFootprintNeg(const ASTNode& varphi);    
 
     //########################################

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 47eb0b53c320843d85937bf20df345876b29735b..fbcfb89e6c8546ae993957582e1923404c087fa6 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -202,8 +202,13 @@ namespace BEEV
 
           result = SymbolTruthValue(newS, form);
 
-          cout << "================" << endl << "Checking BB formula:" << form << endl;
-          cout << "----------------" << endl << "Result:" << result << endl;
+          cout << "================" 
+              << endl 
+              << "Checking BB formula:" 
+              << form << endl;
+          cout << "----------------" 
+              << endl 
+              << "Result:" << result << endl;
 
           break;
         }
@@ -219,8 +224,12 @@ namespace BEEV
             }
           result = bm->CreateSimpForm(k, eval_children);
 
-          cout << "================" << endl << "Checking BB formula:" << form << endl;
-          cout << "----------------" << endl << "Result:" << result << endl;
+          cout << "================" 
+              << endl 
+              << "Checking BB formula:" << form << endl;
+          cout << "----------------" 
+              << endl 
+              << "Result:" << result << endl;
 
           ASTNode replit_eval;
           // Compare with replit, if there is one.
@@ -236,16 +245,22 @@ namespace BEEV
               else
                 {
                   // It's (NOT sym).  Get value of sym and complement.
-                  replit_eval = bm->CreateSimpNot(SymbolTruthValue(newS, replit[0]));
+                  replit_eval = 
+                   bm->CreateSimpNot(SymbolTruthValue(newS, replit[0]));
                 }
 
-              cout << "----------------" << endl << "Rep lit: " << replit << endl;
-              cout << "----------------" << endl << "Rep lit value: " << replit_eval << endl;
+              cout << "----------------" 
+                  << endl 
+                  << "Rep lit: " << replit << endl;
+              cout << "----------------" 
+                  << endl 
+                  << "Rep lit value: " << replit_eval << endl;
 
               if (result != replit_eval)
                 {
                   // Hit the panic button.
-                  FatalError("Truth value of BitBlasted formula disagrees with representative literal in CNF.");
+                  FatalError("Truth value of BitBlasted formula "\
+                            "disagrees with representative literal in CNF.");
                 }
             }
           else