From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 22 Apr 2013 13:49:46 +0000 (-0400)
Subject: add bit0 and bit1 constants to smt-lib v1 parser
X-Git-Tag: cvc5-1.0.0~7315
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a006e7b92327668b76a1ab993007f42fe91052c3;p=cvc5.git

add bit0 and bit1 constants to smt-lib v1 parser
---

diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index ee4e19689..bfcd8cd4d 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -313,6 +313,10 @@ annotatedFormula[CVC4::Expr& expr]
       expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
   | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']'
     { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); }
+  | n = BITVECTOR1_BV_CONST
+    { unsigned int bit = AntlrInput::tokenText($n)[3] - '0';
+      expr = MK_CONST( BitVector(1, bit) );
+    }
     // NOTE: Theory constants go here
     /* TODO: quantifiers, arithmetic constants */
 
@@ -745,6 +749,13 @@ BITVECTOR_BV_CONST
   : 'bv' DIGIT+
   ;
 
+/**
+ * Matches a bit-vector constant of the form bit(0|1)
+ */
+BITVECTOR1_BV_CONST
+  : 'bit0' | 'bit1'
+  ;
+
 
 /**
  * Matches an identifier from the input. An identifier is a sequence of letters,