From d76c561a4e213a6ea5766beaf886be1777c4ed83 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 20 Jun 2011 05:17:02 +0000 Subject: [PATCH] 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 --- src/AST/ASTKind.kinds | 1 - src/AST/ASTmisc.cpp | 3 - src/AST/ArrayTransformer.cpp | 7 -- src/STPManager/STP.cpp | 20 +++--- src/STPManager/STPManager.h | 1 - src/STPManager/UserDefinedFlags.h | 16 ----- .../CounterExample.cpp | 4 -- src/c_interface/c_interface.cpp | 9 --- src/c_interface/c_interface.h | 1 - src/main/main.cpp | 7 -- src/parser/cvc.lex | 1 - src/parser/cvc.y | 64 ------------------- src/printer/PLPrinter.cpp | 24 ------- src/simplifier/simplifier.cpp | 4 -- 14 files changed, 8 insertions(+), 154 deletions(-) diff --git a/src/AST/ASTKind.kinds b/src/AST/ASTKind.kinds index 6871816..c10d916 100644 --- 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 1507909..bac06bc 100644 --- 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 acd080e..5f996de 100644 --- 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 bf8a30b..2fe332a 100644 --- 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 e13a72a..e9c8601 100644 --- 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 650b575..e01533e 100644 --- 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 661e4be..8d5476b 100644 --- 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 5738611..8c96109 100644 --- 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 275bd92..263294a 100644 --- 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 b0cb124..6c95ed3 100644 --- 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 bfdbbcd..cd08ab4 100644 --- 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 050a41f..c1d24e6 100644 --- 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 499ac62..45afe48 100644 --- 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 0a648df..3e507b7 100644 --- 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); -- 2.47.3