From b614a55c948716d16b626ceae3fffc69e135779d Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 19 Jan 2011 05:28:27 +0000
Subject: [PATCH] Fix. sat, unsat, unknown aren't reserved words so they can be
 used as variable names in the SMTLIB2 format. Treat them instead as strings.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1080 e59a4935-1847-0410-ae03-e826735625c1
---
 src/parser/smtlib2.lex |  4 ----
 src/parser/smtlib2.y   | 30 ++++++++++++++----------------
 2 files changed, 14 insertions(+), 20 deletions(-)

diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex
index 5f82b7d..411e9e7 100644
--- 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 9763e71..cd75e60 100644
--- 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; 
 }
 ;
-- 
2.47.3