Producing SMTLIB that's accepted by Alt-Ergo (TermToSMT2 still needs …

…to be adapted for other Seq, Set, ... operations)

src/main/resources/field_value_functions_axioms.smt2

@@ -14,19 +14,17 @@
 (assert (forall ((vs $FVF<$FLD$>) (ws $FVF<$FLD$>)) (!
     (=>
       (and
-        (Set_equal ($FVF.domain_$FLD$ vs) ($FVF.domain_$FLD$ ws))
+        (Set_equal<Ref> ($FVF.domain_$FLD$ vs) ($FVF.domain_$FLD$ ws))
         (forall ((x $Ref)) (!
           (=>
-            (Set_in x ($FVF.domain_$FLD$ vs))
+            (Set_in<Ref> x ($FVF.domain_$FLD$ vs))
             (= ($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x)))
           :pattern (($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x))
-          :qid |qp.$FVF<$FLD$>-eq-inner|
           )))
       (= vs ws))
     :pattern (($SortWrappers.$FVF<$FLD$>To$Snap vs)
               ($SortWrappers.$FVF<$FLD$>To$Snap ws)
               )
-    :qid |qp.$FVF<$FLD$>-eq-outer|
     )))
 
 (assert (forall ((r $Ref) (pm $FPM)) (!

src/main/resources/field_value_functions_axioms_no_triggers.smt2

@@ -19,10 +19,8 @@
           (=>
             (Set_in x ($FVF.domain_$FLD$ vs))
             (= ($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x)))
-          :qid |qp.$FVF<$T$>-eq-inner|
           )))
       (= vs ws))
-    :qid |qp.$FVF<$T$>-eq-outer|
     )))
 
 (assert (forall ((r $Ref) (pm $FPM)) (!

src/main/resources/preamble.smt2

@@ -25,8 +25,8 @@
 (declare-sort $PPM 0)
 (define-sort $Perm () Real)
 
-(define-const $Perm.Write $Perm 1.0)
-(define-const $Perm.No $Perm 0.0)
+(define-fun $Perm.Write () $Perm 1.0)
+(define-fun $Perm.No () $Perm 0.0)
 
 (define-fun $Perm.isValidVar ((p $Perm)) Bool
 	(<= $Perm.No p))

src/main/resources/predicate_snap_functions_axioms.smt2

@@ -20,14 +20,12 @@
             (= ($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x)))
           ; :pattern ((Set_in x ($PSF.domain_$PRD$ vs)))
           :pattern (($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x))
-          :qid |qp.$PSF<$PRD$>-eq-inner|
           )))
       (= vs ws))
     :pattern (($SortWrappers.$PSF<$PRD$>To$Snap vs)
               ($SortWrappers.$PSF<$PRD$>To$Snap ws)
 ;              ($PSF.after_$PRD$ vs ws)
               )
-    :qid |qp.$PSF<$PRD$>-eq-outer|
     )))
 
 (assert (forall ((s $Snap) (pm $PPM)) (!

src/main/resources/predicate_snap_functions_axioms_no_triggers.smt2

@@ -18,10 +18,8 @@
           (=>
             (Set_in x ($PSF.domain_$FRD$ vs))
             (= ($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x)))
-          :qid |qp.$PSF<$S$>-eq-inner|
           )))
       (= vs ws))
-    :qid |qp.$PSF<$S$>-eq-outer|
     )))
 
 (assert (forall ((s $Snap) (f $S$)) (!

src/main/resources/sortwrappers.smt2

@@ -10,12 +10,10 @@
 (assert (forall ((x $T$)) (!
     (= x ($SortWrappers.$SnapTo$S$($SortWrappers.$S$To$Snap x)))
     :pattern (($SortWrappers.$S$To$Snap x))
-    :qid |$Snap.$SnapTo$S$To$Snap|
     )))
 (assert (forall ((x $Snap)) (!
     (= x ($SortWrappers.$S$To$Snap($SortWrappers.$SnapTo$S$ x)))
     :pattern (($SortWrappers.$SnapTo$S$ x))
-    :qid |$Snap.$S$To$SnapTo$S$|
     )))
 
 ; On several examples, e.g., AVLTree.iterative.sil, Z3 instantiates the sort

src/main/resources/z3config.smt2

@@ -11,20 +11,8 @@
 ; Currently, print-success MUST come first, because it guarantees that every query to Z3, including
 ; setting options, is answered by a success (or error) reply from Z3. Silicon currently relies on
 ; these replies when it interacts with Z3 via stdio.
-(set-option :print-success true) ; Boogie: false
-(set-option :global-decls true) ; Necessary for push pop mode
 
 ; These options are taken from Dafny 4.0.0 and proven to work decently well with up-to-date Z3 (currently 4.12.1),
 ; unlike the options used previously.
-(set-option :auto_config false)
-(set-option :smt.case_split 3)
-(set-option :smt.delay_units true)
-(set-option :type_check true)
-(set-option :smt.mbqi false)
-(set-option :pp.bv_literals false)
-(set-option :smt.qi.eager_threshold 100)
-(set-option :smt.arith.solver 2)
-(set-option :model.v2 true)
 
 ; We want unlimited multipatterns
-(set-option :smt.qi.max_multi_patterns 1000)

src/main/scala/Config.scala

@@ -236,7 +236,7 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
              +  s"Note that for the ${Cvc5ProverStdIO.name} prover, state saturation calls can "
              +  "either be disabled (weights or base timeout of 0) or forced with no timeout "
              + "(positive weight and base timeout)."),
-    default = Some(100),
+    default = Some(0),
     noshort = true
   )
 

src/main/scala/decider/Decider.scala

@@ -132,28 +132,14 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
       _prover.start() /* Cannot query prover version otherwise */
 
-      val proverVersion = _prover.version()
+      //val proverVersion = _prover.version()
       // One can pass some options. This allows to check whether they have been received.
 
       val path = prover match {
         case pio: ProverStdIO => pio.proverPath
         case _ => "No Path"
       }
-      val msg = s"Using ${_prover.name} $proverVersion located at ${path}"
-      reporter report ConfigurationConfirmation(msg)
-      logger debug msg
 
-      if (proverVersion < _prover.minVersion) {
-        val msg1 = s"Expected at least ${_prover.name} version ${_prover.minVersion.version}, but found $proverVersion"
-        reporter report InternalWarningMessage(msg1)
-        logger warn msg1
-      }
-
-      if (_prover.maxVersion.fold(false)(_ < proverVersion)) {
-        val msg1 = s"Silicon might not work with ${_prover.name} version $proverVersion, consider using ${_prover.maxVersion.get}"
-        reporter report InternalWarningMessage(msg1)
-        logger warn msg1
-      }
 
       None
     }

src/main/scala/decider/ProverStdIO.scala

@@ -178,13 +178,13 @@ abstract class ProverStdIO(uniqueId: String,
   def push(n: Int = 1, timeout: Option[Int] = None): Unit = {
     setTimeout(timeout)
     pushPopScopeDepth += n
-    val cmd = (if (n == 1) "(push)" else "(push " + n + ")") + " ; " + pushPopScopeDepth
+    val cmd = (if (n == 1) "(push 1)" else "(push " + n + ")") + " ; " + pushPopScopeDepth
     writeLine(cmd)
     readSuccess()
   }
 
   def pop(n: Int = 1): Unit = {
-    val cmd = (if (n == 1) "(pop)" else "(pop " + n + ")") + " ; " + pushPopScopeDepth
+    val cmd = (if (n == 1) "(pop 1)" else "(pop " + n + ")") + " ; " + pushPopScopeDepth
     pushPopScopeDepth -= n
     writeLine(cmd)
     readSuccess()
@@ -261,6 +261,10 @@ abstract class ProverStdIO(uniqueId: String,
     (result, endTime - startTime)
   }
 
+  def writeCheckSat(): Unit = {
+    writeLine("check-sat")
+  }
+
   def saturate(data: Option[Config.ProverStateSaturationTimeout]): Unit = {
     data match {
       case Some(Config.ProverStateSaturationTimeout(timeout, comment)) => saturate(timeout, comment)
@@ -400,10 +404,10 @@ abstract class ProverStdIO(uniqueId: String,
   /* TODO: Handle multi-line output, e.g. multiple error messages. */
 
   protected def readSuccess(): Unit = {
-    val answer = readLine()
+    //val answer = readLine()
 
-    if (answer != "success")
-      throw ProverInteractionFailed(uniqueId, s"Unexpected output of prover. Expected 'success' but found: $answer")
+    //if (answer != "success")
+    //  throw ProverInteractionFailed(uniqueId, s"Unexpected output of prover. Expected 'success' but found: $answer")
   }
 
   protected def readUnsat(): Boolean = readLine() match {

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -101,6 +101,16 @@ class TermToSMTLib2Converter
     super.pretty(defaultWidth, render(t))
   }
 
+  def getTypeArg(s: Sort) : String = {
+    val srt = s match {
+      case sorts.Seq(e) => Seq(e)
+      case sorts.Set(e) => Seq(e)
+      case sorts.Multiset(e) => Seq(e)
+      case sorts.Map(k, v) => Seq(k, v)
+    }
+    srt.mkString("<",",",">")
+  }
+
   protected def render(term: Term): Cont = term match {
     case lit: Literal => render(lit)
 
@@ -138,8 +148,7 @@ class TermToSMTLib2Converter
             ssep(renderedTriggerTerms.map(d => text(":pattern") <+> parens(d)).to(collection.immutable.Seq), line)
 
         val docQid: Cont =
-          if (name.isEmpty) nil
-          else s":qid |$name|"
+          nil
 
         val docWeight = weight match {
           case Some(value) => line <> text(":weight") <+> value.toString
@@ -218,11 +227,11 @@ class TermToSMTLib2Converter
     case SeqRanged(t0, t1) => renderBinaryOp("Seq_range", render(t0), render(t1))
     case SeqSingleton(t0) => parens(text("Seq_singleton") <+> render(t0))
     case bop: SeqAppend => renderBinaryOp("Seq_append", bop)
-    case uop: SeqLength => renderUnaryOp("Seq_length", uop)
-    case bop: SeqAt => renderBinaryOp("Seq_index", bop)
+    case uop: SeqLength => renderUnaryOp(s"Seq_length${getTypeArg(uop.p.sort)}", uop)
+    case bop: SeqAt => renderBinaryOp(s"Seq_index${getTypeArg(bop.p0.sort)}", bop)
     case bop: SeqTake => renderBinaryOp("Seq_take", bop)
     case bop: SeqDrop => renderBinaryOp("Seq_drop", bop)
-    case bop: SeqIn => renderBinaryOp("Seq_contains", bop)
+    case bop: SeqIn => renderBinaryOp(s"Seq_contains${getTypeArg(bop.p0.sort)}", bop)
     case SeqUpdate(t0, t1, t2) => renderNAryOp("Seq_update", t0, t1, t2)
 
     /* Sets */
@@ -233,7 +242,7 @@ class TermToSMTLib2Converter
     case bop: SetDifference => renderApp("Set_difference", Seq(bop.p0, bop.p1), bop.sort)
     case bop: SetIntersection => renderApp("Set_intersection", Seq(bop.p0, bop.p1), bop.sort)
     case bop: SetUnion => renderApp("Set_union", Seq(bop.p0, bop.p1), bop.sort)
-    case bop: SetIn => renderApp("Set_in", Seq(bop.p0, bop.p1), bop.sort)
+    case bop: SetIn => renderApp(s"Set_in${getTypeArg(bop.p1.sort)}", Seq(bop.p0, bop.p1), bop.sort)
     case bop: SetSubset => renderApp("Set_subset", Seq(bop.p0, bop.p1), bop.sort)
     case bop: SetDisjoint => renderApp("Set_disjoint", Seq(bop.p0, bop.p1), bop.sort)
 

src/main/scala/decider/Z3ProverStdIO.scala

@@ -22,7 +22,7 @@ object Z3ProverStdIO {
   val exeEnvironmentalVariable = "Z3_EXE"
   val dependencies = Seq(SilDefaultDependency("Z3", minVersion.version, "https://github.com/Z3Prover/z3"))
   val staticPreamble = "/z3config.smt2"
-  val startUpArgs = Seq("-smt2", "-in")
+  val startUpArgs = Seq("-smt2", "-in") // Seq("-i", "smtlib2")
   val randomizeSeedsOptions = Seq("sat.random_seed", "nlsat.seed", "fp.spacer.random_seed", "smt.random_seed", "sls.random_seed")
 }
 
@@ -55,9 +55,9 @@ class Z3ProverStdIO(uniqueId: String,
       if(Verifier.config.proverEnableResourceBounds) {
         writeLine(s"(set-option :rlimit ${effectiveTimeout * Verifier.config.proverResourcesPerMillisecond})")
       } else {
-        writeLine(s"(set-option :timeout $effectiveTimeout)")
+        //writeLine(s"(set-option :timeout $effectiveTimeout)")
       }
-      readSuccess()
+      //readSuccess()
     }
   }
 

src/main/scala/state/SymbolConverter.scala

@@ -60,6 +60,16 @@ class DefaultSymbolConverter extends SymbolConverter {
       terms.SMTFun(Identifier(function.interpretation.get), inSorts, outSort)
   }
 
+  def toBuiltinFunction(function: ast.DomainFunc, program: ast.Program, sorts: Seq[Sort]): terms.Applicable = {
+    val inSorts = function.formalArgs map (_.typ) map toSort
+    val outSort = toSort(function.typ)
+
+    val domainFunc = program.findDomainFunctionOptionally(function.name)
+    val id = Identifier(function.name + sorts.mkString("[",",","]"))
+
+    terms.DomainFun(id, inSorts, outSort)
+  }
+
   def toFunction(function: ast.DomainFunc, sorts: Seq[Sort], program: ast.Program): terms.DomainFun = {
     assert(sorts.nonEmpty, "Expected at least one sort, but found none")
 

src/main/scala/supporters/BuiltinDomainsContributor.scala

@@ -8,7 +8,6 @@ package viper.silicon.supporters
 
 import java.io.File
 import java.net.URL
-
 import scala.annotation.unused
 import scala.reflect.ClassTag
 import viper.silver.ast
@@ -17,7 +16,7 @@ import viper.silicon.interfaces.PreambleContributor
 import viper.silicon.interfaces.decider.ProverLike
 import viper.silicon.state.DefaultSymbolConverter
 import viper.silicon.state.terms._
-import viper.silver.ast.LineCol
+import viper.silver.ast.{LineCol, SeqType}
 
 abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, DomainFun, Term] {
   type BuiltinDomainType <: ast.GenericType
@@ -112,10 +111,24 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai
   }
 
   protected def collectFunctions(domains: Set[ast.Domain], program: ast.Program): Unit = {
-    domains foreach (
-      _.functions foreach (df =>
+    domains foreach (d =>
+      d.functions foreach (df =>
         if (df.interpretation.isEmpty)
-          collectedFunctions += symbolConverter.toFunction(df, program).asInstanceOf[DomainFun]))
+          collectedFunctions += symbolConverter.toBuiltinFunction(df, program, getTypeArgs(df).map(t => symbolConverter.toSort(t))).asInstanceOf[DomainFun]))
+  }
+
+  def getTypeArgs(df: ast.DomainFunc): Seq[ast.Type] = {
+    for (t <- df.formalArgs.map(v => v.typ) ++ Seq(df.typ)) {
+      t match {
+        case ast.DomainType(_, tvs) => return tvs.values.toSeq
+        case ast.SeqType(e) => return Seq(e)
+        case ast.SetType(e) => return Seq(e)
+        case ast.MultisetType(e) => return Seq(e)
+        case ast.MapType(k, v) => return Seq(k, v)
+        case _ =>
+      }
+    }
+    ??? // unreachable
   }
 
   protected def collectAxioms(domains: Set[(ast.DomainType, ast.Domain)]): Unit = {
@@ -130,7 +143,7 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai
      * are preserved.
      */
     val domainName = f"${d.domainName}[${d.typVarsMap.values.map(t => symbolConverter.toSort(t)).mkString(",")}]"
-    domainTranslator.translateAxiom(ax, symbolConverter.toSort, true).transform {
+    domainTranslator.translateAxiom(ax, symbolConverter.toSort, Some(d.typVarsMap.values.map(t => symbolConverter.toSort(t)).toSeq)).transform {
       case q@Quantification(_,_,_,_,name,_,_) if name != "" =>
         q.copy(name = f"${domainName}_${name}")
       case Equals(t1, t2) => BuiltinEquals(t1, t2)

src/main/scala/supporters/Domains.scala

@@ -135,14 +135,14 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter,
 }
 
 trait DomainsTranslator[R] {
-  def translateAxiom(ax: ast.DomainAxiom, toSort: ast.Type => Sort, builtin: Boolean = false): R
+  def translateAxiom(ax: ast.DomainAxiom, toSort: ast.Type => Sort, builtin: Option[Seq[Sort]] = None): R
 }
 
 class DefaultDomainsTranslator()
     extends DomainsTranslator[Term]
        with ExpressionTranslator {
 
-  def translateAxiom(ax: ast.DomainAxiom, toSort: ast.Type => Sort, builtin: Boolean = false): Term = {
+  def translateAxiom(ax: ast.DomainAxiom, toSort: ast.Type => Sort, builtin: Option[Seq[Sort]] = None): Term = {
     isBuiltin = builtin
     val res = translate(toSort)(ax.exp) match {
       case terms.Quantification(q, vars, body, triggers, "", _, weight) =>
@@ -155,7 +155,7 @@ class DefaultDomainsTranslator()
 
       case other => other
     }
-    isBuiltin = false
+    isBuiltin = None
     res
   }
 }

src/main/scala/supporters/ExpressionTranslator.scala

@@ -19,7 +19,7 @@ trait ExpressionTranslator {
    *       was done before - but that is less efficient and creates lots of additional noise output
    *       in the prover log.
    */
-  protected var isBuiltin: Boolean = false
+  protected var isBuiltin: Option[Seq[Sort]] = None
 
   protected def translate(toSort: ast.Type => Sort)
                          (exp: ast.Exp)
@@ -158,7 +158,7 @@ trait ExpressionTranslator {
         val tArgs = args map f
         val inSorts = tArgs map (_.sort)
         val outSort = toSort(exp.typ)
-        val id = if (isBuiltin) Identifier(funcName) else Identifier(funcName + Seq(outSort).mkString("[",",","]"))
+        val id = if (isBuiltin.isDefined) Identifier(funcName + isBuiltin.get.mkString("[",",","]")) else Identifier(funcName + Seq(outSort).mkString("[",",","]"))
         val df = Fun(id, inSorts, outSort)
         App(df, tArgs)