fixing #25

src/parsing/SMTLIBv2.g4

@@ -791,7 +791,8 @@ match_case
 
 term
     : spec_constant
-    |qual_identifier
+    | ParOpen GRW_Underscore symbol numeral ParClose
+    | qual_identifier
     | ParOpen qual_identifier term+ ParClose
     | ParOpen ParOpen GRW_Underscore qual_identifier term+ ParClose ParClose
     | ParOpen GRW_Let ParOpen var_binding+ ParClose term ParClose
@@ -855,7 +856,6 @@ logic
     : ParOpen PS_Logic symbol logic_attribue+ ParClose
     ;
 
-
 // Scripts
 
 sort_dec

src/parsing/ast.py

@@ -42,7 +42,7 @@ def _get_free_var_occs(self,e, global_vars):
                         global_vars.pop(var)
             for let_term in e.let_terms:
                 self._get_free_var_occs(let_term, global_vars)
-            
+
 
         if e.is_var:
             if e.name in global_vars:
@@ -75,7 +75,7 @@ def _prefix_free_vars(self, prefix, e):
         if e.var_binders:
             for i,var in enumerate(e.var_binders):
                 self._prefix_free_vars(prefix,e.let_terms[i])
-        
+
         for s in e.subterms:
             self._prefix_free_vars(prefix,s)
 
@@ -375,6 +375,7 @@ def Var(name,type, is_indexed_id=False):
 def Const(name, is_indexed_id=False,type="Unknown"):
     return Term(name=name,type=type, is_const=True,is_indexed_id=is_indexed_id)
 
+
 def Expr(op,subterms, is_indexed_id=False):
     return Term(op=op,subterms=subterms)
 

src/parsing/ast_visitor.py

@@ -53,14 +53,12 @@ def handleCommand(self, ctx:SMTLIBv2Parser.CommandContext):
             decl = DeclareConst(self.visitSymbol(ctx.symbol()[0]), self.visitSort(ctx.sort()[0]))
             return decl
         if ctx.cmd_declareFun():
-            print("Debug 1",flush=True)
             input_sorts = []
             for sort in ctx.sort()[:-1]:
                 input_sorts.append(self.visitSort(sort))
             output_sort = self.visitSort(ctx.sort()[-1])
             input_sorts = " ".join(input_sorts)
             identifier = self.visitSymbol(ctx.symbol()[0])
-            print("Debug 2 id=", identifier, flush=True)
             self.add_to_globals(identifier, input_sorts, output_sort)
             return DeclareFun(identifier, input_sorts, output_sort)
 
@@ -200,7 +198,6 @@ def handle_quantifier(self,ctx:SMTLIBv2Parser.TermContext, quant, local_vars):
     | binary
     | string
     | b_value
-    | ParOpen GRW_Underscore ' bv' numeral numeral  ParClose
     ;
     """
     def visitSpec_constant(self, ctx:SMTLIBv2Parser.Spec_constantContext):
@@ -211,26 +208,33 @@ def visitSpec_constant(self, ctx:SMTLIBv2Parser.Spec_constantContext):
 
     """
         term
-            : spec_constant
-            | qual_identifier
-            | ParOpen qual_identifier term+ ParClose
-            | ParOpen GRW_Let ParOpen var_binding+ ParClose term ParClose
-            | ParOpen GRW_Forall ParOpen sorted_var+ ParClose term ParClose
-            | ParOpen GRW_Exists ParOpen sorted_var+ ParClose term ParClose
-            | ParOpen GRW_Match term ParOpen match_case+ ParClose ParClose
-            | ParOpen GRW_Exclamation term attribute+ ParClose
-            ;
-        """
+        : spec_constant
+        | qual_identifier
+        | ParOpen qual_identifier term+ ParClose
+        | ParOpen GRW_Underscore ' bv' numeral numeral ParClose
+        | ParOpen ParOpen GRW_Underscore qual_identifier term+ ParClose ParClose
+        | ParOpen GRW_Let ParOpen var_binding+ ParClose term ParClose
+        | ParOpen GRW_Forall ParOpen sorted_var+ ParClose term ParClose
+        | ParOpen GRW_Exists ParOpen sorted_var+ ParClose term ParClose
+        | ParOpen GRW_Match term ParOpen match_case+ ParClose ParClose
+        | ParOpen GRW_Exclamation term attribute+ ParClose
+        ;
+
+    """
     def visitTerm(self, ctx:SMTLIBv2Parser.TermContext, local_vars):
         if ctx.ParOpen() and ctx.GRW_Exclamation() and ctx.term()\
            and len(ctx.attribute()) >= 1 and ctx.ParClose():
             term,label = self.visitTerm(ctx.term()[0]),self.visitAttribute(ctx.attribute()[0])
             return LabeledTerm(label, [term])
 
-        if len(ctx.ParOpen()) == 2 and ctx.GRW_Match() and ctx.term() and len(ctx.match_case()) >= 1 and\
-            len(ctx.ParClose()) == 2:
+        if len(ctx.ParOpen()) == 2 and ctx.GRW_Match() and ctx.term() and len(ctx.match_case()) >= 1:
             raise ASTException("ParOpen GRW_Match term ParOpen match_case+ ParClose ParClose")
 
+        if len(ctx.ParOpen()) == 1 and ctx.GRW_Underscore() and ctx.numeral():
+            bitwidth = ctx.symbol().getText().strip("bv")
+            value = ctx.numeral().getText()
+            return Const(name="(_ bv"+bitwidth+" "+ value+")")
+
         if len(ctx.ParOpen()) == 2 and ctx.GRW_Exists() and len(ctx.sorted_var()) >= 1 and\
             len(ctx.ParClose()) == 2 and ctx.term():
             return self.handle_quantifier(ctx,"exists",local_vars)
@@ -299,13 +303,11 @@ def visitQuotedSymbol(self, ctx:SMTLIBv2Parser.QuotedSymbolContext):
     ;
     """
     def visitSymbol(self, ctx:SMTLIBv2Parser.SymbolContext):
-        print("DEBUG 4",ctx.getText())
         if ctx.simpleSymbol():
             return self.visitSimpleSymbol(ctx.simpleSymbol())
 
         if ctx.quotedSymbol():
             return self.visitQuotedSymbol(ctx.quotedSymbol())
-        print("no case applies", flush=True)
 
     """
     identifier

tests/unittests/test_parsing.py

@@ -3,14 +3,16 @@
 import sys
 sys.path.append("../../")
 
-from src.parsing.parse import *                                                    
+from src.parsing.parse import *
 
+# Dominik: These are all regression. If these become more, it would make sense
+# to put them their own folder.
 class ParsingTestCase(unittest.TestCase):
-    def test_issue9(self): 
+    def test_issue9(self):
         formula = parse_file("tests/unittests/issue7.smt2")
         self.assertTrue('\x0a' in formula.__str__() and '\n' in formula.__str__())
-  
-    def test_issue18(self): 
+
+    def test_issue18(self):
         formula = parse_file("tests/unittests/issue18.smt2",silent=False)
         oracle="""\
 (declare-fun a () String)
@@ -20,9 +22,24 @@ def test_issue18(self):
 (assert (= a b))
 (check-sat)"""
         self.assertEqual(oracle, formula.__str__())
-
 
-
+    def test_issue25(self):
+    script="""\
+(declare-fun a () Bool)
+(assert (= ((_ extract 5 3) (_ bv96 8))))
+(check-sat)"""
+    script = parse_str(script, silent=False)
+    self.assertTrue("Term" in str(type(script.commands[1].term.subterms[0].subterms[0])))
+
+    script="""\
+(declare-fun bv () (_ BitVec 10))
+(declare-fun a () Bool)
+(assert (not (and (= ((_ extract 5 3) (_ bv96 8)) ((_ extract 4 2) (concat (_ bv121 7)
+((_ extract 0 0) bv)))) (= (concat (_ bv1 1) (ite a (_ bv0 1) (_ bv1 1))) ((_ extract 1 0)
+(ite a (_ bv6 3) (_ bv3 3)))))))
+(check-sat)"""
+    script = parse_str(script, silent=False)
+    self.assertTrue(script != None)
 
 if __name__ == '__main__':
     unittest.main()