From 8581353bdd7266a5b4e92bc8a9149447cdf42647 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Wed, 10 Jun 2009 02:44:13 +0000
Subject: Changed expression nodes to be ExprHandle (instead of ExprHandle*),
 and added a quick hack to change Bison unions to structs.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73154 91177308-0d34-0410-b5e6-96231b3b80d8
---
 lib/SMT/smtlib.y | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'lib/SMT/smtlib.y')

diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index be1c5143..72185a93 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -23,8 +23,11 @@
    commands in SMT-LIB language.
 */
 
-//#include "vc.h"
 #include "parser_temp.h"
+#include "klee/Expr.h"
+
+using namespace klee;
+using namespace klee::expr;
 
 // Exported shared data
 namespace CVC3 {
@@ -75,9 +78,7 @@ int smtliberror(const char *s)
 
 %union {
   std::string *str;
-  std::vector<std::string> *strvec;
-  klee::expr::ExprHandle* node;
-  std::vector<void*> *vec;
+  klee::expr::ExprHandle node;
 };
 
 
@@ -176,13 +177,14 @@ benchmark:
       $$ = new CVC3::Expr(VC->listExpr("_SEQ",*$4));
       delete $4;
       */
-      $$ = NULL;
+      $$ = $4;
     }
   | EOF_TOK
     { 
       TMP->done = true;
       //$$ = new CVC3::Expr();
-      $$ = NULL;
+      //$$ = ConstantExpr::create(1, 1);
+      $$ = ExprHandle();
     }
 ;
 
@@ -761,12 +763,12 @@ prop_atom:
     TRUE_TOK
     {
       //$$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR"));
-      $$ = NULL;
+      $$ = ConstantExpr::create(1, 1);
     }
   | FALSE_TOK
     { 
       //$$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR"));
-      $$ = NULL;
+      $$ = ConstantExpr::create(0, 1);;
     }
 /*
   | fvar
-- 
cgit 1.4.1