Stricter triggers on FVF snap extensionality axiom

src/main/resources/field_value_functions_axioms.smt2

@@ -23,8 +23,8 @@
           :qid |qp.$FVF<$FLD$>-eq-inner|
           )))
       (= vs ws))
-    :pattern (($SortWrappers.$FVF<$FLD$>To$Snap vs)
-              ($SortWrappers.$FVF<$FLD$>To$Snap ws)
+    :pattern (($SortWrappers.$FVF<$FLD$>To$Snap vs) ($FVF.has_domain_$FLD$ vs)
+              ($SortWrappers.$FVF<$FLD$>To$Snap ws) ($FVF.has_domain_$FLD$ ws)
               )
     :qid |qp.$FVF<$FLD$>-eq-outer|
     )))

src/main/resources/field_value_functions_declarations.smt2

@@ -8,6 +8,7 @@
 ;   - $T$ is the sanitized name of the sort corresponding to the type of the field
 
 (declare-fun $FVF.domain_$FLD$ ($FVF<$FLD$>) Set<$Ref>)
+(declare-fun $FVF.has_domain_$FLD$ ($FVF<$FLD$>) Bool)
 (declare-fun $FVF.lookup_$FLD$ ($FVF<$FLD$> $Ref) $S$)
 (declare-fun $FVF.after_$FLD$ ($FVF<$FLD$> $FVF<$FLD$>) Bool)
 (declare-fun $FVF.loc_$FLD$ ($S$ $Ref) Bool)

src/main/resources/predicate_snap_functions_axioms.smt2

@@ -23,8 +23,8 @@
           :qid |qp.$PSF<$PRD$>-eq-inner|
           )))
       (= vs ws))
-    :pattern (($SortWrappers.$PSF<$PRD$>To$Snap vs)
-              ($SortWrappers.$PSF<$PRD$>To$Snap ws)
+    :pattern (($SortWrappers.$PSF<$PRD$>To$Snap vs) ($PSF.has_domain_$PRD$ vs)
+              ($SortWrappers.$PSF<$PRD$>To$Snap ws) ($PSF.has_domain_$PRD$ ws)
 ;              ($PSF.after_$PRD$ vs ws)
               )
     :qid |qp.$PSF<$PRD$>-eq-outer|

src/main/resources/predicate_snap_functions_declarations.smt2

@@ -7,6 +7,7 @@
 ;   - $S$ is the sort corresponding to the type of the predicate arguments
 
 (declare-fun $PSF.domain_$PRD$ ($PSF<$PRD$>) Set<$Snap>)
+(declare-fun $PSF.has_domain_$PRD$ ($PSF<$PRD$>) Bool)
 (declare-fun $PSF.lookup_$PRD$ ($PSF<$PRD$> $Snap) $S$)
 (declare-fun $PSF.after_$PRD$ ($PSF<$PRD$> $PSF<$PRD$>) Bool)
 (declare-fun $PSF.loc_$PRD$ ($S$ $Snap) Bool)

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -263,6 +263,8 @@ class TermToSMTLib2Converter
 
     case Domain(id, fvf) => parens(text("$FVF.domain_") <> id <+> render(fvf))
 
+    case HasDomain(id, fvf) => parens(text("$FVF.has_domain_") <> id <+> render(fvf))
+
     case Lookup(field, fvf, at) => //fvf.sort match {
 //      case _: sorts.PartialFieldValueFunction =>
       parens(text("$FVF.lookup_") <> field <+> render(fvf) <+> render(at))
@@ -282,6 +284,8 @@ class TermToSMTLib2Converter
 
     case PredicateDomain(id, psf) => parens(text("$PSF.domain_") <> id <+> render(psf))
 
+    case HasPredicateDomain(id, psf) => parens(text("$PSF.has_domain_") <> id <+> render(psf))
+
     case PredicateLookup(id, psf, args) =>
       val snap: Term = toSnapTree(args)
 

src/main/scala/decider/TermToZ3APIConverter.scala

@@ -406,6 +406,8 @@ class TermToZ3APIConverter
 
       case Domain(id, fvf) => createApp("$FVF.domain_" + id, Seq(fvf), term.sort)
 
+      case HasDomain(id, fvf) => createApp("$FVF.has_domain_" + id, Seq(fvf), term.sort)
+
       case Lookup(field, fvf, at) =>
         createApp("$FVF.lookup_" + field, Seq(fvf, at), term.sort)
 
@@ -418,6 +420,8 @@ class TermToZ3APIConverter
 
       case PredicateDomain(id, psf) => createApp("$PSF.domain_" + id, Seq(psf), term.sort)
 
+      case HasPredicateDomain(id, psf) => createApp("$PSF.has_domain_" + id, Seq(psf), term.sort)
+
       case PredicateLookup(id, psf, args) =>
         val snap: Term = toSnapTree(args)
         createApp("$PSF.lookup_" + id, Seq(psf, snap), term.sort)

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -487,7 +487,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                         resource: ast.Resource,
                         optSmDomainDefinitionCondition: Option[Term], /* c(rs) */
                         v: Verifier)
-                       : (Term, Seq[Quantification], Option[Quantification]) = {
+                       : (Term, Seq[Quantification], Seq[Term]) = {
     // TODO: Consider if axioms can be simplified in case codomainQVars is empty
 
     val snapshotMaps = relevantChunks.map(_.snapshotMap)
@@ -514,15 +514,18 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         (qvar, transformedOptSmDomainDefinitionCondition, (ch: QuantifiedBasicChunk) => IsPositive(ch.perm).replace(snapToCodomainTermsSubstitution))
     }
 
-    val qvarInDomainOfSummarisingSm = resource match {
+    val (domainTerm, hasDomain) = resource match {
       case field: ast.Field =>
-        SetIn(qvar, Domain(field.name, sm))
+        (Domain(field.name, sm), HasDomain(field.name, sm))
       case predicate: ast.Predicate =>
-        SetIn(qvar, PredicateDomain(predicate.name, sm))
+        (PredicateDomain(predicate.name, sm), HasPredicateDomain(predicate.name, sm))
       case wand: ast.MagicWand =>
-        SetIn(qvar, PredicateDomain(MagicWandIdentifier(wand, s.program).toString, sm))
+        val mwi = MagicWandIdentifier(wand, s.program).toString
+        (PredicateDomain(mwi, sm), HasPredicateDomain(mwi, sm))
     }
 
+    val qvarInDomainOfSummarisingSm = SetIn(qvar, domainTerm)
+
     val valueDefinitions =
       relevantChunks map (chunk => {
         val lookupSummary = ResourceLookup(resource, sm, Seq(qvar), s.program)
@@ -569,15 +572,18 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     }
 
     val optDomainDefinition =
-      smDomainDefinitionCondition.map(condition =>
-        Forall(
-          qvar,
-          Iff(
-            qvarInDomainOfSummarisingSm,
-            condition),
-          if (Verifier.config.disableISCTriggers()) Nil else Seq(Trigger(qvarInDomainOfSummarisingSm)),
-          s"qp.psmDomDef${v.counter(this).next()}",
-          isGlobal = relevantQvars.isEmpty
+      smDomainDefinitionCondition.toSeq.flatMap(condition =>
+        Seq(
+          Forall(
+            qvar,
+            Iff(
+              qvarInDomainOfSummarisingSm,
+              condition),
+            if (Verifier.config.disableISCTriggers()) Nil else Seq(Trigger(qvarInDomainOfSummarisingSm)),
+            s"qp.psmDomDef${v.counter(this).next()}",
+            isGlobal = relevantQvars.isEmpty
+          ),
+          hasDomain
         ))
 
     (sm, resourceAndValueDefinitions, optDomainDefinition)

src/main/scala/state/Terms.scala

@@ -2198,6 +2198,17 @@ object Domain extends CondFlyweightTermFactory[(String, Term), Domain] {
   override def actualCreate(args: (String, Term)): Domain = new Domain(args._1, args._2)
 }
 
+class HasDomain(val field: String, val fvf: Term) extends Term with ConditionalFlyweight[(String, Term), HasDomain] {
+  utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction])
+
+  val sort = sorts.Bool
+  override val equalityDefiningMembers: (String, Term) = (field, fvf)
+}
+
+object HasDomain extends CondFlyweightTermFactory[(String, Term), HasDomain] {
+  override def actualCreate(args: (String, Term)): HasDomain = new HasDomain(args._1, args._2)
+}
+
 class FieldTrigger(val field: String, val fvf: Term, val at: Term) extends Term with ConditionalFlyweight[(String, Term, Term), FieldTrigger] {
   utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction])
   utils.assertSort(at, "receiver", sorts.Ref)
@@ -2245,6 +2256,16 @@ object PredicateDomain extends CondFlyweightTermFactory[(String, Term), Predicat
   override def actualCreate(args: (String, Term)): PredicateDomain = new PredicateDomain(args._1, args._2)
 }
 
+class HasPredicateDomain(val predname: String, val psf: Term) extends Term with ConditionalFlyweight[(String, Term), HasPredicateDomain] {
+  utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction])
+  val sort = sorts.Bool
+  override val equalityDefiningMembers: (String, Term) = (predname, psf)
+}
+
+object HasPredicateDomain extends CondFlyweightTermFactory[(String, Term), HasPredicateDomain] {
+  override def actualCreate(args: (String, Term)): HasPredicateDomain = new HasPredicateDomain(args._1, args._2)
+}
+
 class PredicateTrigger(val predname: String, val psf: Term, val args: Seq[Term]) extends Term with ConditionalFlyweight[(String, Term, Seq[Term]), PredicateTrigger] {
   utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction])
 

src/main/scala/state/Utils.scala

@@ -124,9 +124,11 @@ package object utils {
       val (vs, ts) = l.bindings.toSeq.unzip
       vs ++ ts :+ l.body
     case Domain(_, fvf) => fvf :: Nil
+    case HasDomain(_, fvf) => fvf :: Nil
     case Lookup(_, fvf, at) => fvf :: at :: Nil
     case PermLookup(_, pm, at) => pm :: at :: Nil
     case PredicateDomain(_, psf) => psf :: Nil
+    case HasPredicateDomain(_, psf) => psf :: Nil
     case PredicateLookup(_, psf, args) => Seq(psf) ++ args
     case PredicatePermLookup(_, pm, args) => Seq(pm) ++ args
     case FieldTrigger(_, fvf, at) => fvf :: at :: Nil
@@ -245,11 +247,13 @@ package object utils {
 //      case Distinct(ts) => Distinct(ts map go)
       case Let(bindings, body) => Let(bindings map (p => go(p._1) -> go(p._2)), go(body))
       case Domain(f, fvf) => Domain(f, go(fvf))
+      case HasDomain(f, fvf) => HasDomain(f, go(fvf))
       case Lookup(f, fvf, at) => Lookup(f, go(fvf), go(at))
       case PermLookup(field, pm, at) => PermLookup(field, go(pm), go(at))
       case FieldTrigger(f, fvf, at) => FieldTrigger(f, go(fvf), go(at))
 
       case PredicateDomain(p, psf) => PredicateDomain(p, go(psf))
+      case HasPredicateDomain(p, psf) => HasPredicateDomain(p, go(psf))
       case PredicateLookup(p, psf, args) => PredicateLookup(p, go(psf), args map go)
       case PredicatePermLookup(predname, pm, args) => PredicatePermLookup(predname, go(pm), args map go)
       case PredicateTrigger(p, psf, args) => PredicateTrigger(p, go(psf), args map go)