Fix. sat, unsat, unknown aren't reserved words so they can be used as variable names...

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

diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex
index 5f82b7dbdfdc3bbabda73362a4a1557d6bd0af4f..411e9e7efb155b97253ec3d7b80b1c060f64f5d8 100644 (file)
--- a/src/parser/smtlib2.lex
+++ b/src/parser/smtlib2.lex
@@ -147,10 +147,6 @@ bv{DIGIT}+ { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_
 <STRING_LITERAL>.      { _string_lit.insert(_string_lit.end(),*smt2text); }                           
 <STRING_LITERAL>"\n"   { _string_lit.insert(_string_lit.end(),*smt2text); }
 
-"sat"           { return SAT_TOK; }
-"unsat"         { return UNSAT_TOK; }
-"unknown"       { return UNKNOWN_TOK; }
-
  /* Valid character are: ~ ! @ # $ % ^ & * _ - + = | \ : ; " < > . ? / ( )     */
 "("             { return LPAREN_TOK; }
 ")"             { return RPAREN_TOK; }

diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y
index 9763e715f7cdfe852c9f538da3aeb126a556f6f3..cd75e6074245e6f930a795bcc0162a28c643fdb7 100644 (file)
--- a/src/parser/smtlib2.y
+++ b/src/parser/smtlib2.y
@@ -115,11 +115,7 @@
 %token LPAREN_TOK
 %token RPAREN_TOK
 
- /* Status */
-%token SAT_TOK
-%token UNSAT_TOK
-%token UNKNOWN_TOK
-  
+ 
  /*BV SPECIFIC TOKENS*/
 %token BVLEFTSHIFT_1_TOK
 %token BVRIGHTSHIFT_1_TOK 
@@ -253,17 +249,19 @@ cmdi:
 ;
 
 status:
-SAT_TOK { 
-  input_status = TO_BE_SATISFIABLE; 
-  $$ = NULL; 
-}
-| UNSAT_TOK { 
-  input_status = TO_BE_UNSATISFIABLE; 
-  $$ = NULL; 
-  }
-| UNKNOWN_TOK 
-{ 
-  input_status = TO_BE_UNKNOWN; 
+STRING_TOK { 
+ 
+ std::transform($1->begin(), $1->end(), $1->begin(), ::tolower);
+  
+  if (0 == strcmp($1->c_str(), "sat"))
+       input_status = TO_BE_SATISFIABLE;
+  else if (0 == strcmp($1->c_str(), "unsat"))
+    input_status = TO_BE_UNSATISFIABLE;
+  else if (0 == strcmp($1->c_str(), "unknown"))
+       input_status = TO_BE_UNKNOWN; 
+  else 
+       yyerror($1->c_str());
+  delete $1;
   $$ = NULL; 
 }
 ;