From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 4 Oct 2011 01:25:35 +0000 (+0000)
Subject: Oh, here's another cute compatibility fix for libantlr3c 3.4-beta4.  They #define... 
X-Git-Tag: cvc5-1.0.0~8435
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87ea8ded0593debfda9d649bcce086286247c9fd;p=cvc5.git

Oh, here's another cute compatibility fix for libantlr3c 3.4-beta4.  They #define true and false to their own ANTLR3_TRUE and ANTLR3_FALSE, wreaking havoc on our parsers.  I'm really fed up with this package.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1f817350c..955f3a1f4 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -587,7 +587,7 @@ mainCommand[CVC4::Command*& cmd]
 
   | QUERY_TOK formula[f] { cmd = new QueryCommand(f); }
   | CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); }
-  | CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(true)); }
+  | CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
 
     /* options */
   | OPTION_TOK
@@ -1655,8 +1655,8 @@ simpleTerm[CVC4::Expr& f]
     }
 
     /* boolean literals */
-  | TRUE_TOK  { f = MK_CONST(true); }
-  | FALSE_TOK { f = MK_CONST(false); }
+  | TRUE_TOK  { f = MK_CONST(bool(true)); }
+  | FALSE_TOK { f = MK_CONST(bool(false)); }
     /* arithmetic literals */
     /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot!
      * This is a rational constant!  Otherwise the parser interprets it as a tuple
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index da20c68a2..083bdf3b5 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -278,8 +278,8 @@ annotatedFormula[CVC4::Expr& expr]
     { PARSER_STATE->popScope(); }
 
     /* constants */
-  | TRUE_TOK          { expr = MK_CONST(true); }
-  | FALSE_TOK         { expr = MK_CONST(false); }
+  | TRUE_TOK          { expr = MK_CONST(bool(true)); }
+  | FALSE_TOK         { expr = MK_CONST(bool(false)); }
   | NUMERAL_TOK
     { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
   | RATIONAL_TOK
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5ae04adea..f9a2cccf2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -290,7 +290,7 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new AssertCommand(expr); }
   | /* checksat */
     CHECKSAT_TOK
-    { cmd = new CheckSatCommand(MK_CONST(true)); }
+    { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
   | /* get-assertions */
     GET_ASSERTIONS_TOK
     { cmd = new GetAssertionsCommand; }