Parser for boolean exprs (no commands)

diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index 71809b04976dffc207b961d3b346181d6c75f85b..b0946b41ba5a9046b777be90f975ea8007c9f217 100644 (file)
--- 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: