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

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 b6ab66accd465eec9a6fb3c03e5e5bf3b136cf93..8c0e2c292d0e2344977fa63153da0437a111d1ea 100644 (file)
--- 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 5765d2b80df962130a8d893466d15d2de785d726..d5daf71ef995beace59e71382a74bc7cdc5e8763 100644 (file)
--- 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 cabc1f2c6cee97057d6868f7df87a00390b3e798..b71c6035d2d2b23dc5a17fb7936104f435f96a6b 100644 (file)
--- 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: