From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 9 Jul 2011 06:56:51 +0000 (+0000)
Subject: Fix. The SMTLIB2 parser now outputs "success" in reply to commands if the option... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a59551ef4c90e2b76d52c84fc39710301e100c13;p=francis%2Fstp.git

Fix. The SMTLIB2 parser now outputs "success" in reply to commands if the option is enabled.

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

diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h
index b6ab66a..8c0e2c2 100644
--- a/src/parser/ParserInterface.h
+++ b/src/parser/ParserInterface.h
@@ -24,7 +24,7 @@ class ParserInterface
 	STPMgr& bm;
 	//boost::object_pool<ASTNode> node_pool;
 	bool alreadyWarned;
-
+	bool print_success;
 public:
 	LETMgr letMgr;
 	NodeFactory* nf;
@@ -38,7 +38,7 @@ public:
 		alreadyWarned = false;
 		cache.push_back(Entry(SOLVER_UNDECIDED));
 		symbols.push_back(ASTVec());
-
+		print_success=false;
 	}
 
 	const ASTVec GetAsserts(void)
@@ -126,6 +126,11 @@ public:
            return bm.LookupSymbol(name);
     }
 
+    void setPrintSuccess(bool ps)
+    {
+      print_success= ps;
+    }
+
 
     bool isSymbolAlreadyDeclared(string name)
 	{
@@ -188,6 +193,16 @@ public:
 	  letMgr._parser_symbol_table.insert(s);
 	}
 
+	void
+        success()
+        {
+          if (print_success)
+            {
+              cout << "success" << endl;
+              flush(cout);
+            }
+        }
+
         void
         pop()
         {
diff --git a/src/parser/smt2.lex b/src/parser/smt2.lex
index 5765d2b..d5daf71 100644
--- a/src/parser/smt2.lex
+++ b/src/parser/smt2.lex
@@ -158,20 +158,20 @@ bv{DIGIT}+	{ smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_
 ":difficulty"    { return DIFFICULTY_TOK; }
 ":smt-lib-version"  { return VERSION_TOK; }
 ":status"        { return STATUS_TOK; }
+":print-success"        { return PRINT_TOK; }
+
 
  /* COMMANDS */
 "set-logic"         { return LOGIC_TOK; }  
 "set-info"  		{ return NOTES_TOK;  }
+"set-option"  		{ return OPTION_TOK;  }
 "declare-fun"		{ return DECLARE_FUNCTION_TOK; }
 "push"				{ return PUSH_TOK;}
 "pop"				{ return POP_TOK;}
  
  /*
-	"set-option" 
 	"declare-sort" 
 	"define-sort"  
-	  
-	"pop"
 */ 
 "assert" 			{ return FORMULA_TOK; }
 "check-sat"			{ return CHECK_SAT_TOK; }
diff --git a/src/parser/smt2.y b/src/parser/smt2.y
index cabc1f2..b71c603 100644
--- a/src/parser/smt2.y
+++ b/src/parser/smt2.y
@@ -108,6 +108,7 @@
 %token DIFFICULTY_TOK
 %token VERSION_TOK
 %token STATUS_TOK
+%token PRINT_TOK
 
  /* ASCII Symbols */
  /* Semicolons (comments) are ignored by the lexer */
@@ -179,6 +180,7 @@
 %token CHECK_SAT_TOK
 %token LOGIC_TOK
 %token NOTES_TOK
+%token OPTION_TOK
 %token DECLARE_FUNCTION_TOK
 %token FORMULA_TOK
 %token PUSH_TOK
@@ -226,12 +228,16 @@ cmdi:
 	        0 == strcmp($3->c_str(),"QF_AUFBV"))) {
 	    yyerror("Wrong input logic:");
 	  }
+	  parserInterface->success();
 	  delete $3;
 	}
 |	LPAREN_TOK NOTES_TOK attribute STRING_TOK RPAREN_TOK
 	{
 	delete $4;
 	}
+|	LPAREN_TOK OPTION_TOK attribute RPAREN_TOK
+	{
+	}
 |	LPAREN_TOK NOTES_TOK attribute DECIMAL_TOK RPAREN_TOK
 	{}
 |	LPAREN_TOK NOTES_TOK attribute RPAREN_TOK
@@ -243,6 +249,7 @@ cmdi:
 			parserInterface->push();
 			assertionsSMT2.push_back(ASTVec());
 		}
+		parserInterface->success();
 	}
 |	LPAREN_TOK POP_TOK NUMERAL_TOK RPAREN_TOK
 	{
@@ -251,13 +258,17 @@ cmdi:
 			parserInterface->pop();
 			assertionsSMT2.erase(assertionsSMT2.end()-1);
 		}
+		parserInterface->success();
 	}
 |   LPAREN_TOK DECLARE_FUNCTION_TOK var_decl RPAREN_TOK
-    {}
+    {
+    parserInterface->success();
+    }
 |   LPAREN_TOK FORMULA_TOK an_formula RPAREN_TOK
 	{
 	assertionsSMT2.back().push_back(*$3);
 	parserInterface->deleteNode($3);
+	parserInterface->success();
 	}
 ;
 
@@ -290,6 +301,16 @@ SOURCE_TOK
 {}
 | STATUS_TOK status
 {} 
+| PRINT_TOK TRUE_TOK
+{
+	parserInterface->setPrintSuccess(true);
+	parserInterface->success();
+}
+| PRINT_TOK FALSE_TOK
+{
+	parserInterface->setPrintSuccess(false);
+}
+
 ;
 
 var_decl: