fixed the flex-related bug

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index ed0887a6578b8c875d31ba9c708dd6d5a1898a0d..a57a5216da0893455199db72b89cdab46f264a73 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -94,7 +94,12 @@ namespace BEEV
     int,
     ClauseList *,
     ltint> ClauseBuckets;
-  
+
+  typedef MAP<
+    int,
+    ASTVec,
+    ltint> UserGuided_AbsRefine_Asserts;
+
   // Function to dump contents of ASTNodeMap
   ostream &operator<<(ostream &os, const ASTNodeMap &nmap);
 }; // end namespace BEEV

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 3bafce16bfb2fc14043655f45a29e202c97afebb..ee69d1089a8f07ac42db8d565a13a27360807cf0 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -37,20 +37,20 @@ namespace BEEV {
             bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
             simplified_solved_InputToSAT = 
               arrayTransformer->
-             CreateSubstitutionMap(simplified_solved_InputToSAT);
+              CreateSubstitutionMap(simplified_solved_InputToSAT);
 
             bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
             //printf("##################################################\n");
             bm->ASTNodeStats("after pure substitution: ", 
-                            simplified_solved_InputToSAT);
+                             simplified_solved_InputToSAT);
 
 
             simplified_solved_InputToSAT = 
               simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, 
-                                            false);
+                                             false);
 
             bm->ASTNodeStats("after simplification: ", 
-                            simplified_solved_InputToSAT);
+                             simplified_solved_InputToSAT);
           }
 
         if(bm->UserFlags.wordlevel_solve_flag)
@@ -79,16 +79,16 @@ namespace BEEV {
             bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
             simplified_solved_InputToSAT = 
               arrayTransformer->
-             CreateSubstitutionMap(simplified_solved_InputToSAT);
+              CreateSubstitutionMap(simplified_solved_InputToSAT);
             bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
             bm->ASTNodeStats("after pure substitution: ",
-                            simplified_solved_InputToSAT);
+                             simplified_solved_InputToSAT);
 
             simplified_solved_InputToSAT = 
               simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, 
-                                            false);
+                                             false);
             bm->ASTNodeStats("after simplification: ", 
-                            simplified_solved_InputToSAT);
+                             simplified_solved_InputToSAT);
           }
         
         if(bm->UserFlags.wordlevel_solve_flag)

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 9389bfa94a0b67711518dcf68cb401a06d4dea9e..c2c8708460546165bfd1eef9aba3ec9bf5afc4d1 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -382,7 +382,7 @@ namespace BEEV
 
     ~STPMgr()
     {
-       ClearAllTables();
+      ClearAllTables();
 
       vector<ASTVec*>::iterator it    = _asserts.begin();
       vector<ASTVec*>::iterator itend = _asserts.end();
@@ -396,7 +396,7 @@ namespace BEEV
 
       delete letmgr;
       delete runTimes;
-         
+          
       _interior_unique_table.clear();
       _bvconst_unique_table.clear();
       _symbol_unique_table.clear();

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 3b7c77dc14cf6b62a2f3555dbd9dd170eae0674b..46c657f67650091481b9f5ba29175a93e773d39a 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -393,8 +393,8 @@ void vc_printQuery(VC vc){
 
 nodestar persistNode(node n)
 {
-       persist.push_back(new node(n));
-       return  persist.back();
+  persist.push_back(new node(n));
+  return  persist.back();
 }
 
 
@@ -421,7 +421,7 @@ Type vc_arrayType(VC vc, Type typeIndex, Type typeData) {
     }
   node output = b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0]);
 
- return persistNode(output);
+  return persistNode(output);
 }
 
 //! Create an expression for the value of array at the given index
@@ -1856,8 +1856,8 @@ void vc_Destroy(VC vc) {
   //   }
 
   for (vector<nodestar>::iterator it = persist.begin(); it!= persist.end();it++)
-         delete *it;
- persist.clear();
+    delete *it;
+  persist.clear();
 
   delete decls;
   delete (stpstar)vc;

diff --git a/src/parser/Makefile b/src/parser/Makefile
index 1c088dc2f9d0da29b35a36b2bac02fcdd8acd223..18e8724396ba578dbd8c98e9dfefffd45fc57033 100644 (file)
--- a/src/parser/Makefile
+++ b/src/parser/Makefile
@@ -15,15 +15,17 @@ libparser.a: $(OBJS)
 lexCVC.cpp:    CVC.lex parseCVC_defs.h ../AST/AST.h
                $(LEX)  -olexCVC.cpp -Pcvc CVC.lex
 
-#For rules with multiple targets. Make runs the rule once for each target. 
-#These rules are "pattern rules" which only run once (rather than twice).
+#For rules with multiple targets. Make runs the rule once for each
+#target.  These rules are "pattern rules" which only run once (rather
+#than twice).
+
 parseCV%_defs.h parseCV%.cpp:  CVC.y
                $(YACC) -o cvc.tab.c -p cvc CVC.y
                @cp  cvc.tab.c parseCVC.cpp
                @cp  cvc.tab.h parseCVC_defs.h
 
 lexSMT.cpp:    parseSMT_defs.h smtlib.lex ../AST/AST.h
-               $(LEX) -o lexSMT.cpp --prefix smt smtlib.lex 
+               $(LEX) -olexSMT.cpp -Psmt smtlib.lex 
 
 parseSM%_defs.h parseSM%.cpp:smtlib.y
                $(YACC) -o smt.tab.c -p smt smtlib.y

diff --git a/src/parser/let-funcs.h b/src/parser/let-funcs.h
index 9b33e21f654e712dd887fe937ba2d793d9600930..b7ac39dabbafcf618c286a6d034932ea091021ed 100644 (file)
--- a/src/parser/let-funcs.h
+++ b/src/parser/let-funcs.h
@@ -33,9 +33,9 @@ namespace BEEV
     }
 
     ~LETMgr()
-       {
-         delete _letid_expr_map;
-       }
+    {
+      delete _letid_expr_map;
+    }
 
     ASTNode ResolveID(const ASTNode& var);
       

diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index 674409f3a14f82b1b55fe307361b527fec3b7cf7..7d32058cc321df5f32d913c6971717a967ff6b73 100644 (file)
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -23,10 +23,10 @@ namespace printer
 
   static string tolower(const char * name)
   {
-       string s(name);
-       for (size_t i = 0; i < s.size(); ++i)
-         s[i] = ::tolower(s[i]);
-       return s;
+    string s(name);
+    for (size_t i = 0; i < s.size(); ++i)
+      s[i] = ::tolower(s[i]);
+    return s;
   }
   
   string functionToSMTLIBName(const BEEV::Kind k);

diff --git a/src/sat/sat.h b/src/sat/sat.h
index 1c40435b1fbb2b8f5da85648a8b18d613c192447..4d3bdd9b1784e1c5c494f56a94c441259611d1cf 100644 (file)
--- a/src/sat/sat.h
+++ b/src/sat/sat.h
@@ -2,23 +2,23 @@
 #define SAT_H_
 
 #ifdef CRYPTOMINISAT
-  #include "cryptominisat/Solver.h"
-  #include "cryptominisat/SolverTypes.h"
+#include "cryptominisat/Solver.h"
+#include "cryptominisat/SolverTypes.h"
 #endif
 
 #ifdef CORE
-  #include "core/Solver.h"
-  #include "core/SolverTypes.h"
+#include "core/Solver.h"
+#include "core/SolverTypes.h"
 #endif
 
 #ifdef SIMP
-  #include "simp/SimpSolver.h"
-  #include "core/SolverTypes.h"
+#include "simp/SimpSolver.h"
+#include "core/SolverTypes.h"
 #endif
 
 #ifdef UNSOUND
-  #include "unsound/UnsoundSimpSolver.h"
-  #include "core/SolverTypes.h"
+#include "unsound/UnsoundSimpSolver.h"
+#include "core/SolverTypes.h"
 #endif
 
 #endif

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index 8ecf2a097327f0ea5d3a230f45ca7daa254219d6..c93cf89e3346902b0624cfbb7f2e697d98b8a7ac 100644 (file)
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -19,35 +19,35 @@ namespace BEEV
     
     //Sort the clauses, and bucketize by the size of the clauses
     for(ClauseList::iterator it = cl->begin(), itend = cl->end(); 
-       it!=itend; it++)
+        it!=itend; it++)
       {
-       ClausePtr cptr = *it;
-       int cl_size = cptr->size();
-       if(cl_size >= MAX_BUCKET_LIMIT)
-         {
-           cl_size = MAX_BUCKET_LIMIT;
-         }
-
-       //If no clauses of size cl_size have been seen, then create a
-       //bucket for that size
-       if(cb->find(cl_size) == cb->end())
-         {
-           ClauseList * cllist = new ClauseList();
-           cllist->push_back(cptr);
-           (*cb)[cl_size] = cllist;
-         }
-       else
-         {
-           ClauseList * cllist = (*cb)[cl_size];
-           cllist->push_back(cptr);
-         }
+        ClausePtr cptr = *it;
+        int cl_size = cptr->size();
+        if(cl_size >= MAX_BUCKET_LIMIT)
+          {
+            cl_size = MAX_BUCKET_LIMIT;
+          }
+
+        //If no clauses of size cl_size have been seen, then create a
+        //bucket for that size
+        if(cb->find(cl_size) == cb->end())
+          {
+            ClauseList * cllist = new ClauseList();
+            cllist->push_back(cptr);
+            (*cb)[cl_size] = cllist;
+          }
+        else
+          {
+            ClauseList * cllist = (*cb)[cl_size];
+            cllist->push_back(cptr);
+          }
       }
     
     return cb;
   } //End of SortClauseList_IntoBuckets()
 
   bool ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver,
-                                      ClauseBuckets * cb)
+                                       ClauseBuckets * cb)
   {
     ClauseBuckets::iterator it = cb->begin();
     ClauseBuckets::iterator itend = cb->end();
@@ -55,12 +55,12 @@ namespace BEEV
     bool sat = false;
     for(;it!=itend;it++)
       {
-       ClauseList *cl = (*it).second;
-       sat = toSATandSolve(SatSolver,*cl);
-       if(!sat)
-         {
-           return sat;
-         }
+        ClauseList *cl = (*it).second;
+        sat = toSATandSolve(SatSolver,*cl);
+        if(!sat)
+          {
+            return sat;
+          }
       }
     return sat;
   }
@@ -94,13 +94,13 @@ namespace BEEV
 
     if(!sat)
       {
-       return sat;
+        return sat;
       }
 
 #ifdef CRYPTOMINISAT
     if(!xorcl->empty())
-      {        
-       sat = toSATandSolve(SatSolver, *xorcl, true);
+      { 
+        sat = toSATandSolve(SatSolver, *xorcl, true);
       }
     cm->DELETE(xorcl);
 #endif 

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 48ce34eb89e6e9e11f2188d85a168cd5087add04..f9f70ae0a31bafb29ad4fb969854ed55ab1f1cba 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -638,12 +638,12 @@ namespace BEEV
     
 #ifdef CRYPTOMINISAT
     if ((x->clausespos != NULL 
-        && x->clausespos->size() > 1) 
-       || (doRenamePos(*x) && !wasVisited(*x)))
+         && x->clausespos->size() > 1) 
+        || (doRenamePos(*x) && !wasVisited(*x)))
       {
         if (doSibRenamingPos(*x) 
-           || sharesPos(*x) > 1 
-           || doRenamePos(*x))
+            || sharesPos(*x) > 1 
+            || doRenamePos(*x))
           {
             doRenamingPos(varphi, defs);
           }
@@ -654,7 +654,7 @@ namespace BEEV
     if (x->clausespos != NULL && x->clausespos->size() > 1)
       {
         if (doSibRenamingPos(*x) 
-           || sharesPos(*x) > 1)
+            || sharesPos(*x) > 1)
           {
             doRenamingPos(varphi, defs);
           }
@@ -1293,13 +1293,13 @@ namespace BEEV
       {
         convertFormulaToCNF(*it, defs); // make pos and neg clause set
 
-       //Creating a new variable name for each of the children of the
-       //XOR node
-       //doRenamingPos(*it, defs);
-       doRenamingNeg(*it, defs);
-       xor_clause->insert(xor_clause->end(), 
-                          ((*(info[*it]->clausespos))[0])->begin(),
-                          ((*(info[*it]->clausespos))[0])->end());
+        //Creating a new variable name for each of the children of the
+        //XOR node
+        //doRenamingPos(*it, defs);
+        doRenamingNeg(*it, defs);
+        xor_clause->insert(xor_clause->end(), 
+                           ((*(info[*it]->clausespos))[0])->begin(),
+                           ((*(info[*it]->clausespos))[0])->end());
       }
     doRenamingPosXor(varphi);
     //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
@@ -1655,7 +1655,7 @@ namespace BEEV
     //        && sharesPos(*xx) > 0
     //        && sharesNeg(*xx) > 0)
     //       {
-    //         return;
+    //  return;
     //       }
 
     ASTVec::const_iterator it = varphi.GetChildren().begin();
@@ -1665,12 +1665,12 @@ namespace BEEV
       {
         convertFormulaToCNF(*it, defs); // make pos and neg clause set
 
-       //Creating a new variable name for each of the children of the
-       //XOR node doRenamingPos(*it, defs);
-       doRenamingNeg(*it, defs);
-       xor_clause->insert(xor_clause->end(), 
-                          ((*(info[*it]->clausespos))[0])->begin(),
-                          ((*(info[*it]->clausespos))[0])->end());
+        //Creating a new variable name for each of the children of the
+        //XOR node doRenamingPos(*it, defs);
+        doRenamingNeg(*it, defs);
+        xor_clause->insert(xor_clause->end(), 
+                           ((*(info[*it]->clausespos))[0])->begin(),
+                           ((*(info[*it]->clausespos))[0])->end());
       }
     doRenamingPosXor(varphi);
     //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
@@ -1909,8 +1909,8 @@ namespace BEEV
       {
         cerr << "Number of clauses:" << defs->size() << endl;
         PrintClauseList(cout, *defs);
-       cerr << "Number of xor-clauses:" << clausesxor->size() << endl;
-       PrintClauseList(cout, *clausesxor);
+        cerr << "Number of xor-clauses:" << clausesxor->size() << endl;
+        PrintClauseList(cout, *clausesxor);
       }
 
     return defs;

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 8f62a516bbbe0ab480c7bc646cc8187d627c58e7..aa0d65f00f98e6c18c7c774e7451b6a091d74208 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -11,23 +11,23 @@
 namespace BEEV
 {
 
-bool isTseitinVariable(const ASTNode& n) {
-       if (n.GetKind() == SYMBOL && n.GetType() == BOOLEAN_TYPE) {
-               const char * zz = n.GetName();
-               //if the variables ARE cnf variables then dont make them
-               // decision variables.
-               if (0 == strncmp("cnf", zz, 3))
-               {
-                       return true;
-               }
-       }
-       return false;
-}
+  bool isTseitinVariable(const ASTNode& n) {
+    if (n.GetKind() == SYMBOL && n.GetType() == BOOLEAN_TYPE) {
+      const char * zz = n.GetName();
+      //if the variables ARE cnf variables then dont make them
+      // decision variables.
+      if (0 == strncmp("cnf", zz, 3))
+        {
+          return true;
+        }
+    }
+    return false;
+  }
 
-       /* FUNCTION: lookup or create a new MINISAT literal
-          * lookup or create new MINISAT Vars from the global MAP
-          * _ASTNode_to_SATVar.
-          */
+  /* FUNCTION: lookup or create a new MINISAT literal
+   * lookup or create new MINISAT Vars from the global MAP
+   * _ASTNode_to_SATVar.
+   */
 
   MINISAT::Var 
   ToSAT::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n)
@@ -49,11 +49,11 @@ bool isTseitinVariable(const ASTNode& n) {
 
         // experimental. Don't add Tseitin variables as decision variables.
         if (!bm->UserFlags.tseitin_are_decision_variables_flag && isTseitinVariable(n))
-        {
-               newS.setDecisionVar(v,false);
-        }
+          {
+            newS.setDecisionVar(v,false);
+          }
 
-       }
+      }
     else
       v = it->second;
     return v;
@@ -66,7 +66,7 @@ bool isTseitinVariable(const ASTNode& n) {
    * unsat. else continue.
    */
   bool ToSAT::toSATandSolve(MINISAT::Solver& newS,
-                           ClauseList& cll, bool add_xor_clauses)
+                            ClauseList& cll, bool add_xor_clauses)
   {
     CountersAndStats("SAT Solver", bm);
     bm->GetRunTimes()->start(RunTimes::SendingToSAT);
@@ -110,31 +110,31 @@ bool isTseitinVariable(const ASTNode& n) {
         //          continue;
         //        }
 #ifdef CRYPTOMINISAT
-       if(add_xor_clauses)
-         {         
-           //cout << "addXorClause:\n";
-           newS.addXorClause(satSolverClause, false, 0, "z");
-         }
-       else 
-         {
-           newS.addClause(satSolverClause,0,"z");
-         }
+        if(add_xor_clauses)
+          {         
+            //cout << "addXorClause:\n";
+            newS.addXorClause(satSolverClause, false, 0, "z");
+          }
+        else 
+          {
+            newS.addClause(satSolverClause,0,"z");
+          }
 #else
         newS.addClause(satSolverClause);
 #endif
         float percentage=CLAUSAL_ABSTRACTION_CUTOFF;
         if(count++ >= input_clauselist_size*percentage)
           {
-               //Arbitrary adding only 60% of the clauses in the hopes of
+            //Arbitrary adding only 60% of the clauses in the hopes of
             //terminating early 
             //      cout << "Percentage clauses added: " 
             //           << percentage << endl;
             bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
             bm->GetRunTimes()->start(RunTimes::Solving);
 #ifdef CRYPTOMINISAT
-           if (newS.simplify() == MINISAT::l_Undef)
+            if (newS.simplify() == MINISAT::l_Undef)
 #endif
-             newS.solve();
+              newS.solve();
             bm->GetRunTimes()->stop(RunTimes::Solving);
             if(!newS.okay())
               {

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 4654ae6427b1e9d2bd9f9fcfd082b3e26338da6d..25ccbe002eeb04bca0576603e73a3e5760c13759 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -23,7 +23,7 @@
 
 namespace BEEV
 {
-  #define CLAUSAL_ABSTRACTION_CUTOFF 0.5
+#define CLAUSAL_ABSTRACTION_CUTOFF 0.5
 
   class ToSAT {
   private:
@@ -108,11 +108,11 @@ namespace BEEV
     //Iteratively goes through the Clause Buckets, and calls
     //toSATandSolve()
     bool CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver,
-                                 ClauseBuckets * cb);
+                                  ClauseBuckets * cb);
     
     // Converts the clause to SAT and calls SAT solver
     bool toSATandSolve(MINISAT::Solver& S,
-                      ClauseList& cll, bool add_xor_clauses=false);
+                       ClauseList& cll, bool add_xor_clauses=false);
     
     //print the STP solver output
     void PrintOutput(SOLVER_RETURN_TYPE ret);