Use a different Sort for Sets used in the QP encoding

src/main/resources/dafny_axioms/sets_ref.vpr

@@ -0,0 +1,179 @@
+domain $Set[E] {
+  function Set_in(e: Ref, s: $Set[E]): Bool
+  function Set_card(s: $Set[E]): Int
+  function Set_empty(): $Set[E]
+  function Set_singleton(e: Ref): $Set[E]
+  function Set_unionone(s: $Set[E], e: Ref): $Set[E]
+  function Set_union(s1: $Set[E], s2: $Set[E]): $Set[E]
+  function Set_disjoint(s1: $Set[E], s2: $Set[E]): Bool
+  function Set_difference(s1: $Set[E], s2: $Set[E]): $Set[E]
+  function Set_intersection(s1: $Set[E], s2: $Set[E]): $Set[E]
+  function Set_subset(s1: $Set[E], s2: $Set[E]): Bool
+  function Set_equal(s1: $Set[E], s2: $Set[E]): Bool
+
+  axiom card_non_negative {
+    forall s: $Set[E] :: {Set_card(s)}
+      0 <= Set_card(s)
+  }
+
+  axiom in_empty_set {
+    forall e: Ref :: {Set_in(e, (Set_empty(): $Set[E]))}
+      !Set_in(e, (Set_empty(): $Set[E]))
+  }
+
+  axiom empty_set_cardinality {
+    forall s: $Set[E] :: {Set_card(s)}
+         (Set_card(s) == 0 <==> s == Set_empty())
+      && (Set_card(s) != 0 ==> exists e: Ref :: {Set_in(e, s)} Set_in(e, s))
+  }  
+
+  axiom in_singleton_set {
+    forall e: Ref :: {Set_singleton(e)}
+      Set_in(e, Set_singleton(e))
+  } 
+
+  axiom in_singleton_set_equality {
+    forall e1: Ref, e2: Ref :: {Set_in(e1, Set_singleton(e2))}
+      Set_in(e1, Set_singleton(e2)) <==> e1 == e2
+  } 
+
+  axiom singleton_set_cardinality {
+    forall e: Ref :: {Set_card(Set_singleton(e))}
+      Set_card(Set_singleton(e)) == 1
+  } 
+
+  axiom in_unionone_same {
+    forall s: $Set[E], e: Ref :: {Set_unionone(s, e)}
+      Set_in(e, Set_unionone(s, e))
+  } 
+
+  axiom in_unionone_other {
+    forall s: $Set[E], e1: Ref, e2: Ref :: {Set_in(e1, Set_unionone(s, e2))}
+           Set_in(e1, Set_unionone(s, e2))
+      <==> (e1 == e2 || Set_in(e1, s))
+  } 
+
+  axiom invariance_in_unionone {
+    forall s: $Set[E], e1: Ref, e2: Ref :: {Set_in(e1, s), Set_unionone(s, e2)}
+      Set_in(e1, s) ==> Set_in(e1, Set_unionone(s, e2))
+  } 
+
+  axiom unionone_cardinality_invariant {
+    forall s: $Set[E], e: Ref :: {Set_card(Set_unionone(s, e))}
+      Set_in(e, s) ==> Set_card(Set_unionone(s, e)) == Set_card(s)
+  } 
+
+  axiom unionone_cardinality_changed {
+    forall s: $Set[E], e: Ref :: {Set_card(Set_unionone(s, e)) }
+      !Set_in(e, s) ==> Set_card(Set_unionone(s, e)) == Set_card(s) + 1
+  } 
+
+  axiom in_union_in_one {
+    forall s1: $Set[E], s2: $Set[E], e: Ref :: {Set_in(e, Set_union(s1, s2))}
+           Set_in(e, Set_union(s1, s2))
+      <==> (Set_in(e, s1) || Set_in(e, s2))
+  } 
+
+  axiom in_left_in_union {
+    forall s1: $Set[E], s2: $Set[E], e: Ref :: {Set_in(e, s1), Set_union(s1, s2)}
+      Set_in(e, s1) ==> Set_in(e, Set_union(s1, s2))
+  } 
+
+  axiom in_right_in_union {
+    forall s1: $Set[E], s2: $Set[E], e: Ref :: {Set_in(e, s2), Set_union(s1, s2)}
+      Set_in(e, s2) ==> Set_in(e, Set_union(s1, s2))
+  }
+
+  /* Commented because the trigger looks very weak */
+  // axiom disjoint_sets_difference_union {
+    // forall s1: $Set[E], s2: $Set[E] :: {Set_union(s1, s2)}
+          // Set_disjoint(s1, s2)
+      // ==>    Set_difference(Set_union(s1, s2), a) == b
+          // && Set_difference(Set_union(s1, s2), b) == a
+  // }   
+
+  axiom in_intersection_in_both {
+    forall s1: $Set[E], s2: $Set[E], e: Ref :: {Set_in(e, Set_intersection(s1, s2))} {Set_intersection(s1, s2), Set_in(e, s1)} {Set_intersection(s1, s2), Set_in(e, s2)}
+           Set_in(e, Set_intersection(s1, s2))
+      <==> Set_in(e, s1) && Set_in(e, s2)
+  } 
+
+  axiom union_left_idempotency {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_union(s1, Set_union(s1, s2)) }
+      Set_union(s1, Set_union(s1, s2)) == Set_union(s1, s2)
+  }    
+
+  axiom union_right_idempotency {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_union(Set_union(s1, s2), s2)}
+      Set_union(Set_union(s1, s2), s2) == Set_union(s1, s2)
+  }
+
+  axiom intersection_left_idempotency {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_intersection(s1, Set_intersection(s1, s2))}
+      Set_intersection(s1, Set_intersection(s1, s2)) == Set_intersection(s1, s2)
+  } 
+
+  axiom intersection_right_idempotency {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_intersection(Set_intersection(s1, s2), s2)}
+      Set_intersection(Set_intersection(s1, s2), s2) == Set_intersection(s1, s2)
+  }  
+
+  axiom cardinality_sums {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_card(Set_union(s1, s2))}
+                                       {Set_card(Set_intersection(s1, s2))}
+         Set_card(Set_union(s1, s2)) + Set_card(Set_intersection(s1, s2))
+      == Set_card(s1) + Set_card(s2)
+  }   
+
+  axiom in_difference {
+    forall s1: $Set[E], s2: $Set[E], e: Ref :: {Set_in(e, Set_difference(s1, s2))}
+           Set_in(e, Set_difference(s1, s2))
+      <==> Set_in(e, s1) && !Set_in(e, s2)
+  }
+
+  axiom not_in_difference {
+    forall s1: $Set[E], s2: $Set[E], e: Ref :: {Set_difference(s1, s2), Set_in(e, s2)}
+           Set_in(e, s2)
+      ==> !Set_in(e, Set_difference(s1, s2))
+  } 
+
+  axiom subset_definition {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_subset(s1, s2)}
+           Set_subset(s1, s2)
+      <==> forall e: Ref :: {Set_in(e, s1)}
+                          {Set_in(e, s2)}
+              Set_in(e, s1) ==> Set_in(e, s2)
+  } 
+
+  axiom equality_definition {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_equal(s1, s2)}
+           Set_equal(s1, s2)
+      <==> forall e: Ref :: {Set_in(e, s1)}
+                          {Set_in(e, s2)}
+              Set_in(e, s1) <==> Set_in(e, s2)
+  }   
+
+  axiom native_equality {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_equal(s1, s2)}
+      Set_equal(s1, s2) ==> s1 == s2
+  } 
+
+  axiom disjointness_definition {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_disjoint(s1, s2)}
+           Set_disjoint(s1, s2)
+      <==> forall e: Ref :: {Set_in(e, s1)}
+                          {Set_in(e, s2)}
+              !Set_in(e, s1) || !Set_in(e, s2)
+  }
+
+  axiom cardinality_difference {
+    forall s1: $Set[E], s2: $Set[E] :: {Set_card(Set_difference(s1, s2))}
+              Set_card(Set_difference(s1, s2))
+            + Set_card(Set_difference(s2, s1))
+            + Set_card(Set_intersection(s1, s2))
+         == Set_card(Set_union(s1, s2))
+      &&
+            Set_card(Set_difference(s1, s2))
+         == Set_card(s1) - Set_card(Set_intersection(s1, s2))
+  }
+}

src/main/resources/field_value_functions_declarations.smt2

@@ -7,7 +7,7 @@
 ;   - $S$ is the sort corresponding to the type of the field
 ;   - $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.domain_$FLD$ ($FVF<$FLD$>) Set<$QPRef>)
 (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/scala/decider/TermToSMTLib2Converter.scala

@@ -43,6 +43,7 @@ class TermToSMTLib2Converter
     case sorts.Perm => "$Perm"
     case sorts.Snap => "$Snap"
     case sorts.Ref => "$Ref"
+    case sorts.QPRef => "$QPRef"
     case sorts.Map(keySort, valueSort) => text("Map") <> "<" <> doRender(keySort, true) <> "~_" <> doRender(valueSort, true) <> ">"
     case sorts.Seq(elementSort) => text("Seq<") <> doRender(elementSort, true) <> ">"
     case sorts.Set(elementSort) => text("Set<") <> doRender(elementSort, true) <> ">"

src/main/scala/state/Terms.scala

@@ -48,6 +48,8 @@ object sorts {
     override lazy val toString = id.toString
   }
 
+  object QPRef extends Sort { val id = Identifier("$QPRef");   override lazy val toString = id.toString }
+
   case class Multiset(elementsSort: Sort) extends Sort {
     val id = Identifier(s"Multiset[$elementsSort]")
     override lazy val toString = id.toString

src/main/scala/supporters/DefaultSetsContributor.scala

@@ -41,7 +41,7 @@ class DefaultSetsContributor(val domainTranslator: DomainsTranslator[Term], conf
     }) {
       program.fields foreach {f => setTypeInstances += ast.SetType(f.typ)}
 
-      setTypeInstances += ast.SetType(ast.Ref) /* $FVF.domain_f is of type Set[Ref] */
+      //setTypeInstances += ast.SetType(ast.Ref) /* $FVF.domain_f is of type Set[Ref] */
 
       /* $PSF.domain_p is of type Set[Snap], and a corresponding instantiation of the set axioms
        * is thus needed. Currently, such an instantiation is supported only for Viper types.

src/main/scala/supporters/DefaultSetsContributor2.scala

@@ -0,0 +1,37 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2019 ETH Zurich.
+
+package viper.silicon.supporters
+
+import scala.reflect.{ClassTag, classTag}
+import viper.silicon.Config
+import viper.silver.ast
+import viper.silicon.common.collections.immutable.InsertionOrderedSet
+import viper.silicon.state.terms.{Sort, Term, sorts}
+
+import scala.reflect.{ClassTag, classTag}
+
+class DefaultSetsContributor2(val domainTranslator: DomainsTranslator[Term], config: Config)
+    extends BuiltinDomainsContributor {
+
+  type BuiltinDomainType = ast.SetType
+  val builtinDomainTypeTag: ClassTag[BuiltinDomainType] = classTag[ast.SetType]
+
+  val defaultSourceResource: String = "/dafny_axioms/sets_ref.vpr"
+  val userProvidedSourceFilepath: Option[String] = config.setAxiomatizationFile.toOption
+  val sourceDomainName: String = "$Set"
+
+  override def computeGroundTypeInstances(program: ast.Program): InsertionOrderedSet[ast.SetType] = {
+    val setTypeInstances: InsertionOrderedSet[ast.SetType] = InsertionOrderedSet(ast.SetType(viper.silicon.utils.ast.ViperEmbedding(sorts.QPRef))) /* $FVF.domain_f is of type Set[Ref] */
+
+    setTypeInstances
+  }
+
+  def targetSortFactory(argumentSorts: Iterable[Sort]): Sort = {
+    assert(argumentSorts.size == 1)
+    sorts.Set(argumentSorts.head)
+  }
+}

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -67,6 +67,7 @@ class DefaultMainVerifier(config: Config,
 
   protected val sequencesContributor = new DefaultSequencesContributor(domainTranslator, config)
   protected val setsContributor = new DefaultSetsContributor(domainTranslator, config)
+  protected val setsContributor2 = new DefaultSetsContributor2(domainTranslator, config)
   protected val multisetsContributor = new DefaultMultisetsContributor(domainTranslator, config)
   protected val mapsContributor = new DefaultMapsContributor(domainTranslator, config)
   protected val domainsContributor = new DefaultDomainsContributor(symbolConverter, domainTranslator)
@@ -79,7 +80,7 @@ class DefaultMainVerifier(config: Config,
 
   private val statefulSubcomponents = List[StatefulComponent](
     uniqueIdCounter,
-    sequencesContributor, setsContributor, multisetsContributor, mapsContributor, domainsContributor,
+    sequencesContributor, setsContributor, setsContributor2, multisetsContributor, mapsContributor, domainsContributor,
     fieldValueFunctionsContributor,
     predSnapGenerator, predicateAndWandSnapFunctionsContributor,
     functionsSupporter, predicateSupporter,
@@ -374,7 +375,7 @@ class DefaultMainVerifier(config: Config,
 
   private val analysisOrder: Seq[PreambleContributor[_, _, _]] = Seq(
     sequencesContributor,
-    setsContributor,
+    setsContributor, setsContributor2,
     multisetsContributor,
     mapsContributor,
     domainsContributor,
@@ -386,7 +387,7 @@ class DefaultMainVerifier(config: Config,
 
   private val sortDeclarationOrder: Seq[PreambleContributor[_, _, _]] = Seq(
     sequencesContributor,
-    setsContributor,
+    setsContributor, setsContributor2,
     multisetsContributor,
     mapsContributor,
     domainsContributor,
@@ -398,7 +399,7 @@ class DefaultMainVerifier(config: Config,
 
   private val sortWrapperDeclarationOrder: Seq[PreambleContributor[Sort, _, _]] = Seq(
     sequencesContributor,
-    setsContributor,
+    setsContributor, setsContributor2,
     multisetsContributor,
     mapsContributor,
     domainsContributor,
@@ -414,7 +415,7 @@ class DefaultMainVerifier(config: Config,
      * Multisets depend on sets ($Multiset.fromSet).
      * Maps depend on sets (Map_domain, Map_range, Map_cardinality).
      */
-    setsContributor,
+    setsContributor, setsContributor2,
     multisetsContributor,
     sequencesContributor,
     mapsContributor,
@@ -427,7 +428,7 @@ class DefaultMainVerifier(config: Config,
 
   private val axiomDeclarationOrder: Seq[PreambleContributor[Sort, _, _]] = Seq(
     sequencesContributor,
-    setsContributor,
+    setsContributor, setsContributor2,
     multisetsContributor,
     mapsContributor,
     domainsContributor,