From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Tue, 24 Nov 2009 21:30:50 +0000 (+0000)
Subject: Parser for boolean exprs (no commands)
X-Git-Tag: cvc5-1.0.0~9413
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f4f69b4f85b8906002f8002527f4486cb1ea1ce;p=cvc5.git

Parser for boolean exprs (no commands)
---

diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index 71809b049..b0946b41b 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -328,19 +328,20 @@ Expr:
       delete $1;
       delete $3;
     } 
-		// |	Expr IMPLIES_TOK Expr 
-                //         {
-		// 	  $$ = new CVC3::Expr(VC->listExpr("_IMPLIES", *$1, *$3));
-		// 	  delete $1;
-		// 	  delete $3;
-		// 	}
-		// |	Expr IFF_TOK Expr 
-                //         {
-		// 	  $$ = new CVC3::Expr(VC->listExpr("_IFF", *$1, *$3));
-		// 	  delete $1;
-		// 	  delete $3;
-		// 	} 
-;
+  | Expr IMPLIES_TOK Expr {
+      $$ = new Expr(EM->mkExpr(IMPLIES, *$1, *$3));
+      delete $1;
+      delete $3;
+    }
+  | Expr IFF_TOK Expr {
+      $$ = new Expr(EM->mkExpr(IFF, *$1, *$3));
+      delete $1;
+      delete $3;
+    } 
+  | NOT_TOK Expr {
+      $$ = new Expr(EM->mkExpr(NOT, *$2));
+      delete $2;
+    } ;
 
 
 // Identifier: