Invariant Solver (#214)

.gitignore

@@ -70,3 +70,5 @@ out-classes
 project/.bloop/
 project/metals.sbt
 project/project/
+
+*.semanticdb

build.sbt

@@ -33,13 +33,21 @@ Compile / unmanagedJars += {
 resolvers ++= Seq(
   "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots",
   "Sonatype OSS Releases" at "https://oss.sonatype.org/content/repositories/releases",
-  ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven").withAllowInsecureProtocol(true)
+  "uuverifiers" at "https://eldarica.org/maven"
 )
 
 libraryDependencies ++= Seq(
   "org.scalatest" %% "scalatest" % "3.2.9" % "test;it",
   "org.apache.commons" % "commons-lang3" % "3.4",
-  ("org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.2").cross(CrossVersion.for3Use2_13)
+  ("uuverifiers" %% "eldarica" % "nightly-SNAPSHOT").cross(CrossVersion.for3Use2_13),
+  ("uuverifiers" %% "princess" % "nightly-SNAPSHOT").cross(CrossVersion.for3Use2_13),
+  "org.scala-lang.modules" %% "scala-parser-combinators" % "2.3.0"
+)
+
+excludeDependencies ++= Seq(
+  "org.scala-lang.modules" % "scala-parser-combinators_2.13",
+  "org.scala-lang.modules" % "scala-xml_2.13",
+  "org.scalactic" % "scalactic_2.13",
 )
 
 lazy val nTestParallelism = {
@@ -60,9 +68,6 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi
 // lazy val smtlib = RootProject(file("../scala-smtlib")) // If you have a local copy of Scala-SMTLIB and would like to do some changes
 lazy val smtlib = ghProject("https://github.com/epfl-lara/scala-smtlib.git", "51a44878858b427f1a4e5a5eb01d8f796898d812")
 
-// lazy val princess = RootProject(file("../princess")) // If you have a local copy of Princess and would like to do some changes
-lazy val princess = ghProject("https://github.com/uuverifiers/princess.git", "93cbff11d7b02903e532c7b64207bc12f19b79c7")
-
 lazy val scriptName = settingKey[String]("Name of the generated 'inox' script")
 
 scriptName := "inox"
@@ -153,7 +158,7 @@ lazy val root = (project in file("."))
   )) : _*)
   .settings(compile := ((Compile / compile) dependsOn script).value)
   .settings(Compile / packageDoc / mappings := Seq())
-  .dependsOn(smtlib, princess)
+  .dependsOn(smtlib)
 
 Global / concurrentRestrictions := Seq(
   Tags.limit(Tags.Test, nTestParallelism)

src/main/scala/inox/ast/TypeOps.scala

@@ -42,7 +42,8 @@ trait TypeOps {
   def greatestLowerBound(tps: Seq[Type]): Type =
     if (tps.isEmpty) Untyped else tps.reduceLeft(greatestLowerBound)
 
-  def isSubtypeOf(t1: Type, t2: Type): Boolean = t1.getType == t2.getType
+  def isSubtypeOf(t1: Type, t2: Type): Boolean = 
+    t1.getType == Untyped || t2.getType == Untyped || t1.getType == t2.getType
 
   private type Instantiation = Map[TypeParameter, Type]
   def instantiation(from: Type, to: Type): Option[Instantiation] = {

src/main/scala/inox/solvers/SolverFactory.scala

@@ -5,6 +5,8 @@ package solvers
 
 import transformers._
 import inox.solvers.evaluating.EvaluatingSolver
+import inox.solvers.invariant.AbstractInvariantSolver
+import inox.solvers.invariant.InvariantSolver
 
 trait SolverFactory {
   val program: Program
@@ -80,17 +82,21 @@ object SolverFactory {
     "smt-z3-opt"    -> "Z3 optimizer through SMT-LIB",
     "smt-z3:<exec>" -> "Z3 through SMT-LIB with custom executable name",
     "princess"      -> "Princess with inox unrolling",
-    "eval"          -> "Internal evaluator to discharge ground assertions"
+    "eval"          -> "Internal evaluator to discharge ground assertions",
+    "inv-z3"        -> "Horn solver using Z3 / Spacer",
+    "inv-eld"       -> "Horn solver using Eldarica"
   )
 
   private val fallbacks = Map(
     "nativez3"     -> (() => hasNativeZ3, Seq("smt-z3", "smt-cvc4", "smt-cvc5", "princess"),   "Z3 native interface"),
     "nativez3-opt" -> (() => hasNativeZ3, Seq("smt-z3-opt"),                                   "Z3 native interface"),
     "unrollz3"     -> (() => hasNativeZ3, Seq("smt-z3", "smt-cvc4", "smt-cvc5", "princess"),   "Z3 native interface"),
+    "inv-z3"       -> (() => hasZ3,       Seq("smt-z3", "smt-cvc4", "smt-cvc5", "princess"),   "Z3 native interface"),
     "smt-cvc4"     -> (() => hasCVC4,     Seq("nativez3", "smt-z3", "princess"),               "'cvc4' binary"),
     "smt-cvc5"     -> (() => hasCVC5,     Seq("nativez3", "smt-z3", "princess"),               "'cvc5' binary"),
     "smt-z3"       -> (() => hasZ3,       Seq("nativez3", "smt-cvc4", "smt-cvc5", "princess"), "'z3' binary"),
     "smt-z3-opt"   -> (() => hasZ3,       Seq("nativez3-opt"),                                 "'z3' binary"),
+    "inv-eld"      -> (() => true,        Seq(),                                               "Eldarica solver"),
     "princess"     -> (() => true,        Seq(),                                               "Princess solver"),
     "eval"         -> (() => true,        Seq(),                                               "Internal evaluator")
   )
@@ -257,6 +263,100 @@ object SolverFactory {
         () => new SMTZ3OptImpl(p)
       })
 
+      case "inv-z3" => create(p)(finalName, {
+        val emptyEnc = ProgramEncoder.empty(enc.targetProgram)
+        val chooses = ChooseEncoder(enc.targetProgram)(emptyEnc)
+        class SMTZ3Impl(override val program: enc.targetProgram.type)
+          extends AbstractInvariantSolver (program, ctx)(program)(emptyEnc)(emptyEnc)(using program.getSemantics, emptyEnc.targetProgram.getSemantics)
+            with InvariantSolver
+            with TimeoutSolver
+            with tip.TipDebugger {
+
+          override val name = "inv-z3" 
+
+          class Underlying(override val program: targetProgram.type)
+            extends smtlib.SMTLIBSolver(program, context)
+              with smtlib.Z3Solver {
+            override def targetName = "z3"
+            import _root_.smtlib.trees.Terms
+            import _root_.smtlib.trees.CommandsResponses._
+            import _root_.smtlib.trees.Commands._
+            import _root_.smtlib.Interpreter
+            import _root_.smtlib.printer.Printer
+            import _root_.smtlib.printer.RecursivePrinter
+            import java.io.BufferedReader
+            import _root_.smtlib.interpreters.ProcessInterpreter
+            import _root_.smtlib.parser.Parser
+            import _root_.smtlib.extensions.tip.Lexer
+
+            class  HornZ3Interpreter(executable: String,
+                              args: Array[String],
+                              printer: Printer = RecursivePrinter,
+                              parserCtor: BufferedReader => Parser = out => new Parser(new Lexer(out)))
+            extends ProcessInterpreter (executable, args, printer, parserCtor):
+              printer.printCommand(SetOption(PrintSuccess(true)), in)
+              in.write("\n")
+              in.flush()
+              parser.parseGenResponse
+              in.write("(set-logic HORN)\n")
+              in.flush()
+              parser.parseGenResponse
+
+              override def eval(cmd: Terms.SExpr): Terms.SExpr = 
+                super.eval(cmd)
+
+            override protected val interpreter = {
+              val opts = interpreterOpts
+              // reporter.debug("Invoking solver "+targetName+" with "+opts.mkString(" "))
+              new HornZ3Interpreter(targetName, opts.toArray, parserCtor = out => new Z3Parser(new Lexer(out)))
+            }
+          }
+
+          override protected val underlyingHorn = Underlying(targetProgram)
+
+          // encoder is from TipDebugger and enc from AbstractUnrollingSolver
+          override protected val encoder = emptyEnc
+        }
+
+        class EncodedImpl(program: p.type, enc: transformers.ProgramTransformer {
+                         val sourceProgram: program.type
+                         val targetProgram: Program { val trees: inox.trees.type }
+                       }, underlying: Solver {val program: enc.targetProgram.type}) 
+              extends EncodingSolver(program, enc, underlying) with TimeoutSolver
+
+        () => new EncodedImpl(p, enc, SMTZ3Impl(enc.targetProgram))
+      })
+
+      case "inv-eld" => create(p)(finalName, {
+        val emptyEnc = ProgramEncoder.empty(enc.targetProgram)
+        val chooses = ChooseEncoder(enc.targetProgram)(emptyEnc)
+        class SMTEldaricaImpl(override val program: enc.targetProgram.type)
+          extends AbstractInvariantSolver (program, ctx)(program)(emptyEnc)(emptyEnc)(using program.getSemantics, emptyEnc.targetProgram.getSemantics)
+            with InvariantSolver
+            with TimeoutSolver
+            with tip.TipDebugger {
+
+          override val name = "inv-eld" 
+
+          class Underlying(override val program: targetProgram.type)
+            extends smtlib.SMTLIBSolver(program, context)
+              with smtlib.EldaricaSolver
+
+          override protected val underlyingHorn = Underlying(targetProgram)
+
+          // encoder is from TipDebugger and enc from AbstractUnrollingSolver
+          override protected val encoder = emptyEnc
+        }
+
+        class EncodedImpl(program: p.type, enc: transformers.ProgramTransformer {
+                         val sourceProgram: program.type
+                         val targetProgram: Program { val trees: inox.trees.type }
+                       }, underlying: Solver {val program: enc.targetProgram.type}) 
+              extends EncodingSolver(program, enc, underlying) with TimeoutSolver
+
+        () => new EncodedImpl(p, enc, SMTEldaricaImpl(enc.targetProgram))
+      })
+
       case _ if finalName == "smt-z3" || finalName.startsWith("smt-z3:") => create(p)(finalName, {
         class SMTZ3Impl(override val program: p.type)
                        (override val enc: transformers.ProgramTransformer {