#5 Use better test for null

Update changelog to make it clear that record_access
needs to be guarded.

Author: florianschanda

CHANGELOG.md

@@ -23,7 +23,12 @@
 
   * A new expression `Record_Null_Check` can be used to check if a
     given term is equal to the null constructor. This can only be used
-    on recursive records.
+    on recursive records. Note that if you have a recursive record,
+    then this is a pre-condition that you need to check on any access;
+    otherwise you might get unexpected results (it is perfectly
+    possible to access a record null constructor, you just get an
+    uninterpreted function result). This checking has to happen inside
+    the program driving PyVCG, it cannot happen inside PyVCG.
 
 * Move to CVC 1.3.1.
 

pyvcg/driver/cvc5_api.py

@@ -506,10 +506,9 @@ def visit_record_null_check(self, node, tr_record):
         s_dt = s_record_sort.getDatatype()
         s_cons = s_dt.getConstructor(node.record.sort.name + "__null")
         return self.solver.mkTerm(
-            cvc5.Kind.EQUAL,
-            tr_record,
-            self.solver.mkTerm(cvc5.Kind.APPLY_CONSTRUCTOR,
-                               s_cons.getTerm()))
+            cvc5.Kind.APPLY_TESTER,
+            s_cons.getTesterTerm(),
+            tr_record)
 
     def visit_function_application(self, node, tr_function, tr_args):
         assert isinstance(node, smt.Function_Application)

pyvcg/driver/file_smtlib.py

@@ -332,9 +332,9 @@ def visit_record_access(self, node, tr_record):
 
     def visit_record_null_check(self, node, tr_record):
         assert isinstance(node, smt.Record_Null_Check)
-        return "(= %s %s)" % (
-            tr_record,
-            self.escape_name(node.record.sort.name + "__null"))
+        return "((_ is %s) %s)" % (
+            self.escape_name(node.record.sort.name + "__null"),
+            tr_record)
 
     def visit_function_application(self, node, tr_function, tr_args):
         assert isinstance(node, smt.Function_Application)

tests/testSmt.py

@@ -1030,14 +1030,90 @@ def test_Recursive_Record(self):
             (declare-const a List)
             (declare-const b List)
             (assert (= (value (next a)) 42))
-            (assert (not (= b List__null)))
+            (assert (not ((_ is List__null) b)))
             (check-sat)
             (get-value (a))
             (get-value (b))
             (exit)
             """
         )
 
+    def test_Recursive_Record_Loop(self):
+        s_sort = smt.Record("List")
+        s_sort.add_component("value", smt.BUILTIN_INTEGER)
+        s_sort.add_component("next", s_sort)
+        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))
+        sym_b = smt.Constant(s_sort, "b")
+        self.script.add_statement(
+            smt.Constant_Declaration(sym_b,
+                                     relevant=True))
+        sym_c = smt.Constant(s_sort, "c")
+        self.script.add_statement(
+            smt.Constant_Declaration(sym_c,
+                                     relevant=True))
+
+        self.script.add_statement(
+            smt.Assertion(
+                smt.Boolean_Negation(
+                    smt.Record_Null_Check(sym_a))))
+        self.script.add_statement(
+            smt.Assertion(
+                smt.Boolean_Negation(
+                    smt.Record_Null_Check(sym_b))))
+        self.script.add_statement(
+            smt.Assertion(
+                smt.Boolean_Negation(
+                    smt.Record_Null_Check(sym_c))))
+
+        self.script.add_statement(
+            smt.Assertion(
+                smt.Comparison("=",
+                               smt.Record_Access(sym_a, "next"),
+                               sym_b)))
+        self.script.add_statement(
+            smt.Assertion(
+                smt.Comparison("=",
+                               smt.Record_Access(sym_b, "next"),
+                               sym_c)))
+        self.script.add_statement(
+            smt.Assertion(
+                smt.Comparison("=",
+                               smt.Record_Access(sym_c, "next"),
+                               sym_a)))
+
+        self.assertResult(
+            "unsat",
+            """
+            (set-logic QF_DTLIA)
+            (set-option :produce-models true)
+
+            (declare-datatype List (
+              (List__null)
+              (List__cons
+                (value Int)
+                (next List))))
+            (declare-const a List)
+            (declare-const b List)
+            (declare-const c List)
+            (assert (not ((_ is List__null) a)))
+            (assert (not ((_ is List__null) b)))
+            (assert (not ((_ is List__null) c)))
+            (assert (= (next a) b))
+            (assert (= (next b) c))
+            (assert (= (next c) a))
+            (check-sat)
+            (get-value (a))
+            (get-value (b))
+            (get-value (c))
+            (exit)
+            """
+        )
+
     def test_Void_Records(self):
         s_sort = smt.Record("Foo")
         self.script.add_statement(smt.Record_Declaration(s_sort))