* When parsing SMTLIB format. Consider :formula and :assumption to be the same. Previ...

* Remove some old/odd array accesses synatax.

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

diff --git a/parser/smtlib.y b/parser/smtlib.y
index 8a5dd658f18a7713ef9a8d9d3ef939e8c765141f..d9309f4c8862a630e9a6ba4ce430be5fd3099f23 100644 (file)
--- a/parser/smtlib.y
+++ b/parser/smtlib.y
@@ -274,13 +274,14 @@ bench_attribute:
     }
   | COLON_TOK FORMULA_TOK an_formula
     {
-      //the query
-      query = BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT,*$3);
-      BEEV::globalBeevMgr_for_parser->AddQuery(query);
-      //dummy true
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE));
-      
-      
+               // Previously this would call AddQuery() on the negation.
+               // But if multiple formula were (eroneously) present
+               // it discarded all but the last formula. Allowing multiple 
+               // formula and taking the conjunction of them along with all
+               // the assumptions is what the other solvers do.  
+
+      //assumptions are like asserts
+      $$ = $3;
     }
   | COLON_TOK STATUS_TOK status
     {
@@ -701,19 +702,6 @@ an_nonbvconst_term:
       //$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(*$2));
       //delete $2;
     }
-  | LPAREN_TOK TERMID_TOK an_term RPAREN_TOK
-    {
-      //ARRAY READ
-      // valuewidth is same as array, indexwidth is 0.
-      BEEV::ASTNode in = *$2;
-      BEEV::ASTNode m = *$3;
-      unsigned int width = in.GetValueWidth();
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, in, m));
-      BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-      $$ = n;
-      delete $2;
-      delete $3;
-    }
   | SELECT_TOK an_term an_term
     {
       //ARRAY READ