Oh, here's another cute compatibility fix for libantlr3c 3.4-beta4. They #define...

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1f817350c1d52f45113b025525c9d957eec6eb85..955f3a1f47cc7ebcfe16bcfae61bb8915049dac3 100644 (file)
--- 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 da20c68a2b2ac47621638eb53613c5ad7ed75eac..083bdf3b5a649a4c17fc1ac425e3db288d8ecd5f 100644 (file)
--- 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 5ae04adea5a199c155364a89ae685806e4aae7c7..f9a2cccf248bd08795748a4a33acf698f2d28fc1 100644 (file)
--- 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; }