Marking HasDomain terms as global to fix issue #954 (#955)

Author: marcoeilers

silver

@@ -679,6 +679,8 @@ object PathConditions {
     assumption match {
       case quantification: Quantification => quantification.isGlobal
       case _: IsReadPermVar => true
+      case hd: HasDomain => hd.isGlobal
+      case hd: HasPredicateDomain => hd.isGlobal
       case _ => false
     }
   }

src/main/scala/decider/PathConditions.scala

@@ -263,7 +263,7 @@ 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 HasDomain(id, fvf, _) => parens(text("$FVF.has_domain_") <> id <+> render(fvf))
 
     case Lookup(field, fvf, at) => //fvf.sort match {
 //      case _: sorts.PartialFieldValueFunction =>
@@ -284,7 +284,7 @@ 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 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/TermToSMTLib2Converter.scala

@@ -406,7 +406,7 @@ 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 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)
@@ -420,7 +420,7 @@ 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 HasPredicateDomain(id, psf, _) => createApp("$PSF.has_domain_" + id, Seq(psf), term.sort)
 
       case PredicateLookup(id, psf, args) =>
         val snap: Term = toSnapTree(args)

src/main/scala/decider/TermToZ3APIConverter.scala

@@ -526,12 +526,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     val (domainTerm, hasDomain) = resource match {
       case field: ast.Field =>
-        (Domain(field.name, sm), HasDomain(field.name, sm))
+        (Domain(field.name, sm), HasDomain(field.name, sm, relevantQvars.isEmpty))
       case predicate: ast.Predicate =>
-        (PredicateDomain(predicate.name, sm), HasPredicateDomain(predicate.name, sm))
+        (PredicateDomain(predicate.name, sm), HasPredicateDomain(predicate.name, sm, relevantQvars.isEmpty))
       case wand: ast.MagicWand =>
         val mwi = MagicWandIdentifier(wand, s.program).toString
-        (PredicateDomain(mwi, sm), HasPredicateDomain(mwi, sm))
+        (PredicateDomain(mwi, sm), HasPredicateDomain(mwi, sm, relevantQvars.isEmpty))
     }
 
     val qvarInDomainOfSummarisingSm = SetIn(qvar, domainTerm)

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -2200,15 +2200,15 @@ object Domain extends CondFlyweightTermFactory[(String, Term), Domain] {
 
 /** Marks FVFs that have a defined domain (i.e. for which some information is available about Domain(field, fvf)).
   * Only for these FVFs is it useful to trigger the extensionality axiom.  */
-class HasDomain(val field: String, val fvf: Term) extends Term with ConditionalFlyweight[(String, Term), HasDomain] {
+class HasDomain(val field: String, val fvf: Term, val isGlobal: Boolean) extends Term with ConditionalFlyweight[(String, Term, Boolean), HasDomain] {
   utils.assertSort(fvf, "field value function", "FieldValueFunction", _.isInstanceOf[sorts.FieldValueFunction])
 
   val sort = sorts.Bool
-  override val equalityDefiningMembers: (String, Term) = (field, fvf)
+  override val equalityDefiningMembers: (String, Term, Boolean) = (field, fvf, isGlobal)
 }
 
-object HasDomain extends CondFlyweightTermFactory[(String, Term), HasDomain] {
-  override def actualCreate(args: (String, Term)): HasDomain = new HasDomain(args._1, args._2)
+object HasDomain extends CondFlyweightTermFactory[(String, Term, Boolean), HasDomain] {
+  override def actualCreate(args: (String, Term, Boolean)): HasDomain = new HasDomain(args._1, args._2, args._3)
 }
 
 class FieldTrigger(val field: String, val fvf: Term, val at: Term) extends Term with ConditionalFlyweight[(String, Term, Term), FieldTrigger] {
@@ -2259,14 +2259,14 @@ object PredicateDomain extends CondFlyweightTermFactory[(String, Term), Predicat
 }
 
 /** Like HasDomain, but for predicate snap functions; see comment above. */
-class HasPredicateDomain(val predname: String, val psf: Term) extends Term with ConditionalFlyweight[(String, Term), HasPredicateDomain] {
+class HasPredicateDomain(val predname: String, val psf: Term, val isGlobal: Boolean) extends Term with ConditionalFlyweight[(String, Term, Boolean), HasPredicateDomain] {
   utils.assertSort(psf, "predicate snap function", "PredicateSnapFunction", _.isInstanceOf[sorts.PredicateSnapFunction])
   val sort = sorts.Bool
-  override val equalityDefiningMembers: (String, Term) = (predname, psf)
+  override val equalityDefiningMembers: (String, Term, Boolean) = (predname, psf, isGlobal)
 }
 
-object HasPredicateDomain extends CondFlyweightTermFactory[(String, Term), HasPredicateDomain] {
-  override def actualCreate(args: (String, Term)): HasPredicateDomain = new HasPredicateDomain(args._1, args._2)
+object HasPredicateDomain extends CondFlyweightTermFactory[(String, Term, Boolean), HasPredicateDomain] {
+  override def actualCreate(args: (String, Term, Boolean)): HasPredicateDomain = new HasPredicateDomain(args._1, args._2, args._3)
 }
 
 class PredicateTrigger(val predname: String, val psf: Term, val args: Seq[Term]) extends Term with ConditionalFlyweight[(String, Term, Seq[Term]), PredicateTrigger] {

src/main/scala/state/Terms.scala

@@ -124,11 +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 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 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
@@ -247,13 +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 HasDomain(f, fvf, g) => HasDomain(f, go(fvf), g)
       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 HasPredicateDomain(p, psf, g) => HasPredicateDomain(p, go(psf), g)
       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)