minor edits. Lot more work remains in optimizing FOR construct

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

diff --git a/Makefile b/Makefile
index d4fa64a04dbfc4106ad881e1ac8d29a8476535a4..ad6a82ae708ae06016ca46a50fbae356d6266d23 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -68,12 +68,13 @@ clean:
        $(MAKE) clean -C $(SRC)/parser
        $(MAKE) clean -C $(SRC)/main
 
-# this is make way too difficult because of the recursive Make junk, it 
-# should be removed
-TAGS: FORCE
-       find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags -
 
-FORCE:
+.PHONY: regressall
+regressall:
+       $(MAKE) regresscvc
+       $(MAKE) regresssmt
+       $(MAKE) regresscapi
+       $(MAKE) regressbigarray
 
 # The higher the level, the more tests are run (3 = all)
 REGRESS_LEVEL=4

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 66b2cb077d65d58b59f3a7fdad5467138e2b1549..32774213d708b8df03d8b1431962681f372fa0a4 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -40,6 +40,7 @@ ifeq ($(shell uname -s), DarwinX)
 else
   LDFLAGS = $(LDFLAGS_BASE)
   CFLAGS = $(CFLAGS_BASE) -m32
+  CFLAGS = $(CFLAGS_BASE)
 endif
 
 #CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index d4fa64a04dbfc4106ad881e1ac8d29a8476535a4..ad6a82ae708ae06016ca46a50fbae356d6266d23 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -68,12 +68,13 @@ clean:
        $(MAKE) clean -C $(SRC)/parser
        $(MAKE) clean -C $(SRC)/main
 
-# this is make way too difficult because of the recursive Make junk, it 
-# should be removed
-TAGS: FORCE
-       find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags -
 
-FORCE:
+.PHONY: regressall
+regressall:
+       $(MAKE) regresscvc
+       $(MAKE) regresssmt
+       $(MAKE) regresscapi
+       $(MAKE) regressbigarray
 
 # The higher the level, the more tests are run (3 = all)
 REGRESS_LEVEL=4

diff --git a/src/AST/Makefile b/src/AST/Makefile
index 5416feb1bba4231869c95e5a7ed228f4eedfda86..22010428471b060fc9bafb7ef98d043d50b21171 100644 (file)
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -23,5 +23,5 @@ clean:
 depend: $(SRCS)
        @$(CXX) -MM -MG $(CXXFLAGS) $(SRCS) > $@
 
--include ./depend
+#-include ./depend
 

diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp
index 13f3c19600d31d74ca46db28e8e55734ab583d15..b8bdea9a1157f6d0967aac50489d4b06255e2e10 100644 (file)
--- a/src/abstraction-refinement/AbstractionRefinement.cpp
+++ b/src/abstraction-refinement/AbstractionRefinement.cpp
@@ -227,6 +227,21 @@ namespace BEEV
     return arraywrite_axiom;
   }//end of Create_ArrayWriteAxioms()
 
+
+  static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap, 
+                               const ASTNode& key, const ASTNode& value)
+  {
+    ASTNodeMap::iterator it = VarToConstMap->find(key);
+    if(it != VarToConstMap->end())
+      {
+       VarToConstMap->erase(it);       
+      }
+
+    (*VarToConstMap)[key] = value;
+    return;   
+  }
+
+
   /******************************************************************
    * FINITE FORLOOP ABSTRACTION REFINEMENT
    *
@@ -250,7 +265,7 @@ namespace BEEV
   BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, 
                                              const ASTNode& original_input)
   {
-    //cout << "The number of abs-refinement limit is " << num_absrefine << endl;
+    cout << "The number of abs-refinement limit is " << num_absrefine << endl;
     for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) 
       {
        ASTVec Allretvec0;
@@ -287,7 +302,7 @@ namespace BEEV
            return res;
          }     
       } //end of absrefine count
-        
+    
     ASTVec Allretvec1;
     Allretvec1.push_back(ASTTrue);
     SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; 
@@ -355,11 +370,13 @@ namespace BEEV
     ASTNode exceptFormula = finiteloop[4];
     ASTNode formulabody   = finiteloop[5];
     int paramCurrentValue = paramInit;
+    int width             = finiteloop[1].GetValueWidth();
 
     //Update ParamToCurrentValMap with parameter and its current
     //value. Here paramCurrentValue is the initial value    
-    (*ParamToCurrentValMap)[parameter] = 
-      CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
+    ASTNode value =       
+      CreateBVConst(width,paramCurrentValue);
+    ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
     
     //Go recursively thru' all the FOR-constructs.
     if(FOR == formulabody.GetKind()) 
@@ -383,11 +400,13 @@ namespace BEEV
              }
 
             //Update ParamToCurrentValMap with parameter and its
-            //current value. FIXME: Possible leak since I am not
-            //freeing the previous 'value' for the same 'key'
-            paramCurrentValue = paramCurrentValue + paramIncrement;
-            (*ParamToCurrentValMap)[parameter] = 
-             CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
+            //current value.
+            paramCurrentValue = paramCurrentValue + paramIncrement;        
+           value = CreateTerm(BVPLUS, 
+                              width, 
+                              (*ParamToCurrentValMap)[parameter],
+                              CreateOneConst(width));  
+           ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
           } //end of While
 
        return retvec;
@@ -416,8 +435,10 @@ namespace BEEV
 
         //Check the currentformula against the model, and add it to the
         //SAT solver if it is false against the model
-        if(absrefine_flag && 
-          ASTFalse == ComputeFormulaUsingModel(currentFormula)) 
+        if(absrefine_flag 
+          && 
+          ASTFalse == ComputeFormulaUsingModel(currentFormula)
+          ) 
          {
            ForloopVec.push_back(currentFormula);
           }
@@ -435,11 +456,13 @@ namespace BEEV
          }
         
         //Update ParamToCurrentValMap with parameter and its current
-        //value. FIXME: Possible leak since I am not freeing the
-        //previous 'value' for the same 'key'
+        //value.
        paramCurrentValue = paramCurrentValue + paramIncrement;
-        (*ParamToCurrentValMap)[parameter] = 
-         CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);       
+       value = CreateTerm(BVPLUS, 
+                          width, 
+                          (*ParamToCurrentValMap)[parameter],
+                          CreateOneConst(width));      
+       ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
       } //end of expanding the FOR loop
     
     return ForloopVec;
@@ -477,12 +500,14 @@ namespace BEEV
     ASTNode exceptFormula = finiteloop[4];
     ASTNode formulabody   = finiteloop[5];
     int paramCurrentValue = paramInit;
+    int width             = finiteloop[1].GetValueWidth();
 
     //Update ParamToCurrentValMap with parameter and its current
     //value. Here paramCurrentValue is the initial value
-    (*ParamToCurrentValMap)[parameter] = 
-      CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
-    
+    ASTNode value =       
+      CreateBVConst(width,paramCurrentValue);
+    ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
+
     ASTNode ret = ASTTrue;
     ASTVec returnVec;
     //Go recursively thru' all the FOR-constructs.
@@ -504,16 +529,21 @@ namespace BEEV
              }
 
             //Update ParamToCurrentValMap with parameter and its
-            //current value. FIXME: Possible leak since I am not
-            //freeing the previous 'value' for the same 'key'
+            //current value.
             paramCurrentValue = paramCurrentValue + paramIncrement;
-            (*ParamToCurrentValMap)[parameter] = 
-             CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
+           value = CreateTerm(BVPLUS, 
+                              width, 
+                              (*ParamToCurrentValMap)[parameter],
+                              CreateOneConst(width));
+           ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
           } //end of While
 
        ASTNode retFormula = 
-         (returnVec.size() != 1) ? 
-         CreateNode(AND, returnVec) : returnVec[0];
+         (returnVec.size() > 1) ? 
+         CreateNode(AND, returnVec) : 
+         (returnVec.size() == 1) ?
+         returnVec[0] :
+         ASTTrue;
         return retFormula;      
       }
 
@@ -560,12 +590,12 @@ namespace BEEV
         
         //Update ParamToCurrentValMap with parameter and its current
         //value         
-        //FIXME: Possible leak since I am not freeing the previous
-        //'value' for the same 'key'
        paramCurrentValue = paramCurrentValue + paramIncrement;
-       (*ParamToCurrentValMap)[parameter] = 
-         CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
-       //cout << (*ParamToCurrentValMap)[parameter];
+       value = CreateTerm(BVPLUS, 
+                          width, 
+                          (*ParamToCurrentValMap)[parameter],
+                          CreateOneConst(width));      
+       ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
       } //end of For
 
     if(checkusingmodel_flag) 
@@ -575,9 +605,11 @@ namespace BEEV
     else 
       {
         ASTNode retFormula = 
-          (forloopFormulaVector.size() != 1) ? 
-         CreateNode(AND, forloopFormulaVector) : 
-         forloopFormulaVector[0];
+          (forloopFormulaVector.size() > 1) ? 
+         CreateNode(AND, forloopFormulaVector) :
+         (forloopFormulaVector.size() == 1) ? 
+         forloopFormulaVector[0] :
+         ASTTrue;
         return retFormula;
       }
   } //end of the Check_FiniteLoop_UsingModel()
@@ -601,7 +633,6 @@ namespace BEEV
   } //end of Check_FiniteLoop_UsingModel
 
 
-
 //   /******************************************************************
 //    * FINITE FORLOOP ABSTRACTION REFINEMENT
 //    *

diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile
index 78906ac8566a1bf90f6d5bc592daf6fadb15bc04..15b5666d60d8fa65be17671c146d95874fe11867 100644 (file)
--- a/src/sat/core/Makefile
+++ b/src/sat/core/Makefile
@@ -2,6 +2,7 @@ MTL       = ../mtl
 CHDRS     = $(wildcard *.h) $(wildcard $(MTL)/*.h)
 EXEC      = minisat
 CFLAGS    = -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store -m32
+CFLAGS    = -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store
 LFLAGS    = -lz
 
 

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 2e4770e6523549de9b9bf42baf2a75cf214c5d93..e02340b1a3ebcee806723648949f8297ccc4df7c 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -854,7 +854,7 @@ namespace BEEV
        output = ComputeFormulaUsingModel(output);
        break;
       case FOR:
-       output = Check_FiniteLoop_UsingModel(form);
+       output = Check_FiniteLoop_UsingModel(form);     
        break;
       default:
         FatalError(" ComputeFormulaUsingModel: "\
@@ -1018,31 +1018,6 @@ namespace BEEV
       }
 
     TermsAlreadySeenMap.clear();
-    // do
-//       {
-//         inputToSAT = simplified_solved_InputToSAT;
-
-//     if(optimize_flag) 
-//       {
-//         //simplified_solved_InputToSAT =
-//         //CreateSubstitutionMap(simplified_solved_InputToSAT);
-//         //Begin_RemoveWrites = true; ASTNodeStats("after pure
-//         //substitution: ", simplified_solved_InputToSAT);
-//         simplified_solved_InputToSAT = 
-//           SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
-//         //ASTNodeStats("after simplification: ",
-//         //simplified_solved_InputToSAT); 
-//         //
-//       }
-
-//     if(wordlevel_solve_flag)
-//       {
-//         simplified_solved_InputToSAT
-//           = bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
-//         ASTNodeStats("after solving: ",
-//                      simplified_solved_InputToSAT);
-//       }
-//       } while (inputToSAT != simplified_solved_InputToSAT);
 
     if (start_abstracting)
       {
@@ -1068,7 +1043,6 @@ namespace BEEV
       }
 
     res = CallSAT_ResultCheck(newS, simplified_solved_InputToSAT, orig_input);
-
     if (SOLVER_UNDECIDED != res)
       {
         CountersAndStats("print_func_stats");

diff --git a/tests/for-tests/for-boolean2.cvc b/tests/for-tests/for-boolean2.cvc
new file mode 100644 (file)
index 0000000..cca2f54
--- /dev/null
+++ b/tests/for-tests/for-boolean2.cvc
@@ -0,0 +1,11 @@
+A,B : BOOLEAN;
+
+ASSERT A(0x00) <=> TRUE ; 
+ASSERT B(0x00) <=> FALSE;
+ASSERT (
+FOR(j:BITVECTOR(8);0x00;0xFF;0x01){
+  A(j) <=> B(j)
+}
+);
+
+QUERY FALSE;
\ No newline at end of file