From e345b6289b334ab978e084fde2fde3bb440d7ab2 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 23 Jul 2009 11:12:04 +0000
Subject: [PATCH] * When parsing SMTLIB format. Consider :formula and
 :assumption to be the same. Previously we took just the final :formula,
 discarding the prior ones. There shouldn't be multiple :formula elements, but
 there sometimes are. * 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
---
 parser/smtlib.y | 28 ++++++++--------------------
 1 file changed, 8 insertions(+), 20 deletions(-)

diff --git a/parser/smtlib.y b/parser/smtlib.y
index 8a5dd65..d9309f4 100644
--- 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
-- 
2.47.3