Fix parsing issue for empty records

Fixes #5

Author: florianschanda

pyvcg/driver/cvc5_smtlib.py

@@ -338,7 +338,7 @@ def parse_enum(self):
 
     def parse_record(self, typ):
         assert isinstance(typ, smt.Record)
-        if self.peek("BRA") or not typ.is_recursive:
+        if self.peek("BRA"):
             self.match("BRA")
             self.match("IDENTIFIER")
             if typ.name + "__cons" != self.ct.value:  # pragma: no cover
@@ -351,11 +351,13 @@ def parse_record(self, typ):
             self.match("KET")
         else:
             self.match("IDENTIFIER")
-            if typ.name + "__null" != self.ct.value:  # pragma: no cover
-                self.error("unexpected constructor %s (expected %s)" %
-                           (self.ct.value,
-                            typ.name + "__null"))
-            rv = None
+            if self.ct.value == typ.name + "__null" and typ.is_recursive:
+                rv = None
+            elif self.ct.value == typ.name + "__cons":
+                rv = {}
+            else:  # pragma: no cover
+                self.error("unexpected constructor %s" %
+                           self.ct.value)
         return rv
 
 

tests/testSmt.py

@@ -1038,6 +1038,31 @@ def test_Recursive_Record(self):
             """
         )
 
+    def test_Void_Records(self):
+        s_sort = smt.Record("Foo")
+        self.script.add_statement(smt.Record_Declaration(s_sort))
+
+        sym_a = smt.Constant(s_sort, "a")
+        self.script.add_statement(
+            smt.Constant_Declaration(sym_a,
+                                     relevant=True))
+
+        self.assertResult(
+            "sat",
+            """
+            (set-logic QF_DT)
+            (set-option :produce-models true)
+
+            (declare-datatype Foo (
+              (Foo__cons)))
+            (declare-const a Foo)
+            (check-sat)
+            (get-value (a))
+            (exit)
+            """
+        )
+        self.assertValue("a", {})
+
     def test_UF_No_Body(self):
         s_par = smt.Bound_Variable(smt.BUILTIN_INTEGER, "x")
         s_fun = smt.Function("potato", smt.BUILTIN_INTEGER, s_par)