Remove the code for the not-working FOR construct.

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

diff --git a/src/AST/ASTKind.kinds b/src/AST/ASTKind.kinds
index 687181617badec5b3d1cc2baa53e297ea5772122..c10d916eeb6fcace60271f165b1d02a0437140b2 100644 (file)
--- a/src/AST/ASTKind.kinds
+++ b/src/AST/ASTKind.kinds
@@ -59,7 +59,6 @@ NOR           1       -       Form
 XOR            1       -       Form
 IFF            1       -       Form
 IMPLIES                2       2       Form
-FOR            5       5       Form
 PARAMBOOL       2       2       Form
 
 # array operations

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 15079099c7a16d1aa1c7326728e3740d99ecc1a2..bac06bccf531e5c4b41cf5ddae38100c09ce2722 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -409,9 +409,6 @@ bool containsArrayOps(const ASTNode&n)
             if (3 != n.Degree())
               FatalError("BVTypeCheck:ITE must have exactly 3 ChildNodes", n);
             break;
-          case FOR:
-            //FIXME: Todo
-            break;
           default:
             FatalError("BVTypeCheck: Unrecognized kind: ");
             break;

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index acd080e472e317d341bc86b2dd7f38cb35a77702..5f996de7346304486c81d21c1db2fde40fc81d37 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -377,13 +377,6 @@ namespace BEEV
           result = nf->CreateNode(k, vec);
           break;
         }
-      case FOR:
-        {
-          //Insert in a global list of FOR constructs. Return TRUE now
-          //GlobalList_Of_FiniteLoops.push_back(simpleForm);
-          return ASTTrue;
-          break;
-        }
       case PARAMBOOL:
         {
           //If the parameteric boolean variable is of the form

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index bf8a30bdade982f66635f684611856943ba67a7b..2fe332a4bc3aa6ce909e7f9f5b379fa6b978a248 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -69,16 +69,8 @@ namespace BEEV {
       }
     
        SOLVER_RETURN_TYPE result;
-    if(bm->UserFlags.num_absrefine_flag)
-      {
-     result =  UserGuided_AbsRefine(NewSolver,
-                                   original_input);
-      }
-    else 
-      {
-       result = TopLevelSTPAux(NewSolver,
+    result = TopLevelSTPAux(NewSolver,
                              original_input, original_input);
-      }
 
     delete newS;
 
@@ -531,19 +523,21 @@ namespace BEEV {
         return res;
       }
 
-    if (!bm->UserFlags.num_absrefine_flag)
+//    if (!bm->UserFlags.num_absrefine_flag)
       {
         FatalError("TopLevelSTPAux: reached the end without proper conclusion:"
           "either a divide by zero in the input or a bug in STP");
         //bogus return to make the compiler shut up
         return SOLVER_ERROR;
       }
-    else
+  //  else
       {
-        return res;
+       // return res;
       }
   } //End of TopLevelSTPAux
 
+#if 0
+
   //UserGuided abstraction refinement
   SOLVER_RETURN_TYPE
   STP::
@@ -620,4 +614,6 @@ namespace BEEV {
               "either a divide by zero in the input or a bug in STP");    
     return SOLVER_ERROR;
   } //End of UserGuided_AbsRefine()
+#endif
+
 }; //end of namespace

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index e13a72ae622fb929ea3555839e36f9cd85a55759..e9c8601ce830ea68afae5ef11582b41cf1d777a3 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -202,7 +202,6 @@ namespace BEEV
       ASTUndefined = CreateNode(UNDEFINED);
       runTimes     = new RunTimes();
       _current_query = ASTUndefined;
-      UserFlags.num_absrefine = 2;
       CreateBVConstVal = NULL;
     }    
     

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 650b5757616b9b0eab12f9baa2a4592af5e4fbcf..e01533ee8addd4cb63967302a07e88f6473addc5 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -57,14 +57,6 @@ namespace BEEV
     bool print_counterexample_flag;
     bool print_binary_flag;
     
-    //Expands out the finite for-construct completely
-    bool expand_finitefor_flag;
-    
-    //Determines the number of abstraction-refinement loop count for the
-    //for-construct
-    bool num_absrefine_flag;
-    int num_absrefine;
-    
     //if this option is true then print the way dawson wants using a
     //different printer. do not use this printer.
     bool print_arrayval_declaredorder_flag;
@@ -213,14 +205,6 @@ namespace BEEV
       output_CNF_flag = false;
       output_bench_flag = false;
 
-      //Expands out the finite for-construct completely
-      expand_finitefor_flag = false;
-      
-      //Determines the number of abstraction-refinement loop count for the
-      //for-construct
-      num_absrefine_flag = false;
-      num_absrefine = 0;
-            
       //if this option is true then print the way dawson wants using a
       //different printer. do not use this printer.
       print_arrayval_declaredorder_flag = false;

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 661e4be2b00bdfc8483708cc709fd9ada424efed..8d5476bd879591ff799341473894d984f68e182d 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -541,10 +541,6 @@ namespace BEEV
         output = bm->NewParameterized_BooleanVar(form[0],form[1]);
         output = ComputeFormulaUsingModel(output);
         break;
-      case FOR:
-        //output = Check_FiniteLoop_UsingModel(form);
-        output = ASTTrue;
-        break;
       default:
           cerr << _kind_names[k];
       FatalError(" ComputeFormulaUsingModel: "

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 5738611fe24ee1c7ca14246ac4f5df3ac73f6a64..8c961098c2f54297af322ee3cc5b2663036469c1 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -50,8 +50,6 @@ void vc_setFlags(VC vc, char c, int param_value) {
     "-c  : construct counterexample\n";
   helpstring +=  
     "-d  : check counterexample\n";
-  helpstring +=  
-    "-e  : expand finite-for construct\n";
   helpstring +=  
     "-f  : number of abstraction-refinement loops\n";
   helpstring +=  
@@ -84,13 +82,6 @@ void vc_setFlags(VC vc, char c, int param_value) {
     b->UserFlags.construct_counterexample_flag = true;
     b->UserFlags.check_counterexample_flag = true;
     break;
-  case 'e':
-    b->UserFlags.expand_finitefor_flag = true;
-    break;
-  case 'f':
-    b->UserFlags.num_absrefine_flag = true;
-    b->UserFlags.num_absrefine = param_value;
-    break;
   case 'h':
     fprintf(stderr,BEEV::usage,BEEV::prog);
     cout << helpstring;

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 275bd92039884b9f6a1274bb8b763593b537059b..263294ab16797295f40f54dd0fe552939d4ec3a1 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -396,7 +396,6 @@ extern "C" {
       XOR,
       IFF,
       IMPLIES,
-      FOR,
       PARAMBOOL,
       READ,
       WRITE,

diff --git a/src/main/main.cpp b/src/main/main.cpp
index b0cb1246496e9dd787cc1e1620a30e24c51a3093..6c95ed3614aeff39f91808129a9392d8d24b7105 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -338,13 +338,6 @@ int main(int argc, char ** argv) {
               bm->UserFlags.construct_counterexample_flag = true;
               bm->UserFlags.check_counterexample_flag = true;
               break;
-            case 'e':
-              bm->UserFlags.expand_finitefor_flag = true;
-              break;
-            case 'f':
-              bm->UserFlags.num_absrefine_flag = true;
-              bm->UserFlags.num_absrefine = atoi(argv[++i]);
-              break;            
             case 'g':
               signal(SIGVTALRM, handle_time_out);
               timeout.it_interval.tv_usec = 0;

diff --git a/src/parser/cvc.lex b/src/parser/cvc.lex
index bfdbbcdcf9d31fc404b27c6c636ecb16993db102..cd08ab46097558c6ca653fbc2727eb34ee59d90c 100644 (file)
--- a/src/parser/cvc.lex
+++ b/src/parser/cvc.lex
@@ -58,7 +58,6 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 "NAND"          { return NAND_TOK;}
 "NOR"           { return NOR_TOK;}
 "NOT"           { return NOT_TOK; }
-"FOR"           { return FOR_TOK; }
 "EXCEPT"        { return EXCEPT_TOK; }
 "OR"            { return OR_TOK; }
 "/="            { return NEQ_TOK; }

diff --git a/src/parser/cvc.y b/src/parser/cvc.y
index 050a41fe83a655869e2439c41969b7d2d2d8d82a..c1d24e6a48bf65606ca20d69a7edd516f00b0c26 100644 (file)
--- a/src/parser/cvc.y
+++ b/src/parser/cvc.y
@@ -63,7 +63,6 @@
 %token  AND_TOK                 "AND"
 %token  OR_TOK                  "OR"
 %token  NOT_TOK                 "NOT"
-%token  FOR_TOK                 "FOR"
 %token  EXCEPT_TOK              "EXCEPT"
 %token  XOR_TOK                 "XOR"
 %token  NAND_TOK                "NAND"
@@ -487,69 +486,6 @@ Formula         :     '(' Formula ')'
   delete $1;
   delete $3;
 }
-|      FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' EXCEPT_TOK Formula ')' '{' Formula '}'
-{
-  //Allows a compact representation of
-  //parameterized set of formulas (bounded
-  //universal quantification)
-  //
-  //parameter name (a variable)
-  //
-  //initial value (BVCONST)
-  //
-  //limit value (BVCONST)
-  //
-  //increment value (BVCONST)
-  //
-  //formula (it can be a nested forloop)                         
-                           
-  ASTVec vec;
-  vec.push_back(*$3);
-  vec.push_back(*$5);
-  vec.push_back(*$7);
-  vec.push_back(*$9);
-  vec.push_back(*$12);
-  vec.push_back(*$15);
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(FOR,vec));
-  $$ = n;
-  delete $3;
-  delete $5;
-  delete $7;
-  delete $9;
-  delete $12;                  
-  delete $15;
-}
-|      FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}'
-{
-  //Allows a compact representation of
-  //parameterized set of formulas (bounded
-  //universal quantification)
-  //
-  //parameter name (a variable)
-  //
-  //initial value (BVCONST)
-  //
-  //limit value (BVCONST)
-  //
-  //increment value (BVCONST)
-  //
-  //formula (it can be a nested forloop)                         
-                           
-  ASTVec vec;
-  vec.push_back(*$3);
-  vec.push_back(*$5);
-  vec.push_back(*$7);
-  vec.push_back(*$9);
-  vec.push_back(parserInterface->CreateNode(FALSE));
-  vec.push_back(*$12);
-  ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(FOR,vec));
-  $$ = n;
-  delete $3;
-  delete $5;
-  delete $7;
-  delete $9;
-  delete $12;
-}
 |      NOT_TOK Formula 
 {
   $$ = new ASTNode(parserInterface->nf->CreateNode(NOT, *$2));

diff --git a/src/printer/PLPrinter.cpp b/src/printer/PLPrinter.cpp
index 499ac62507c73b54ced04e7e721efbaae739fe0e..45afe483eeaa4c2d496e6839f9a359a82dc7afb9 100644 (file)
--- a/src/printer/PLPrinter.cpp
+++ b/src/printer/PLPrinter.cpp
@@ -216,30 +216,6 @@ string functionToCVCName(const Kind k) {
         PL_Print1(os, c[1], indentation, letize);
         os << ")";
         break;
-      case FOR:
-        // if(expand_finitefor_flag) 
-        //        {
-        //          ASTNode expandedfor = bm->Expand_FiniteLoop_TopLevel(n);
-        //          PL_Print1(os, expandedfor, indentation, letize);
-        //        }
-        //      else 
-        {
-          os << "FOR(";
-          PL_Print1(os, c[0], indentation, letize);
-          os << ";";
-          PL_Print1(os, c[1], indentation, letize);
-          os << ";";
-          PL_Print1(os, c[2], indentation, letize);
-          os << ";";
-          PL_Print1(os, c[3], indentation, letize);
-          os << ";";
-          os << "EXCEPT ";
-          PL_Print1(os, c[4], indentation, letize);
-          os << "){ \n";
-          PL_Print1(os, c[5], indentation, letize);
-          os << "} \n";
-        }
-        break;
 
       case BVLT: // two arity, prefixed function name.
       case BVLE:

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 0a648dfad0770a2e4c15bed501425876080a5e7e..3e507b7bed6454e0de799a0151ca70f839e448c1 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -315,7 +315,6 @@ namespace BEEV
     ASTVec ca = a.GetChildren();
     if (!(IMPLIES == kind || 
           ITE == kind     || 
-          FOR == kind     ||
           PARAMBOOL==kind ||
           isAtomic(kind)))
       {
@@ -383,9 +382,6 @@ namespace BEEV
       case ITE:
         output = SimplifyIteFormula(a, pushNeg, VarConstMap);
         break;
-      case FOR:
-        output = SimplifyForFormula(a, pushNeg, VarConstMap);
-        break;
       default:
         //kind can be EQ,NEQ,BVLT,BVLE,... or a propositional variable
         output = SimplifyAtomicFormula(a, pushNeg, VarConstMap);