Trying out different mask axioms/triggers

viperproject · Jul 15, 2023 · c9a9f0a · c9a9f0a
1 parent 792aa3d
commit c9a9f0a
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git a/src/main/resources/mask_axioms.smt2 b/src/main/resources/mask_axioms.smt2
@@ -69,6 +69,7 @@
           ($Hp.get_$Perm ($Hp.maskAdd m r1 v) r2)
           (+ ($Hp.get_$Perm m r2) (ite (= r1 r2) v 0.0)))
       :pattern (($Hp.get_$Perm ($Hp.maskAdd m r1 v) r2))
+      ;:pattern (($Hp.get_$Perm m r2))
       :qid |qp.$Hp.maskAdd-def-inner|
       ))
     :pattern (($Hp.maskAdd m r1 v))
@@ -103,4 +104,17 @@
       )))
     :pattern (($Hp.maskGoodField m))
     :qid |qp.$Hp.maskGoodField-def|
+    )))
+
+
+(assert (forall ((m $Hp<$Perm>) (r $Ref) (v Real)) (!
+  (=> ($Hp.maskGoodField m)
+        (and (>=
+          ($Hp.get_$Perm ($Hp.maskAdd m r v) r)
+          0.0)
+          (<=
+                    ($Hp.get_$Perm ($Hp.maskAdd m r v) r)
+                    1.0)))
+    :pattern (($Hp.maskGoodField ($Hp.maskAdd m r v)))
+    :qid |qp.$Hp.maskGoodFieldAdd-def|
     )))
diff --git a/src/main/scala/decider/TermToSMTLib2Converter.scala b/src/main/scala/decider/TermToSMTLib2Converter.scala
@@ -304,7 +304,7 @@ class TermToSMTLib2Converter
     case GoodMask(mask) =>
       parens(text("$Hp.maskGood") <+> render(mask))
 
-    case GoodMask(mask) =>
+    case GoodFieldMask(mask) =>
       parens(text("$Hp.maskGoodField") <+> render(mask))
 
     case DummyHeap(sort) =>