diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala index 0c32db911..fb48ba198 100644 --- a/src/main/scala/inox/solvers/SolverFactory.scala +++ b/src/main/scala/inox/solvers/SolverFactory.scala @@ -45,13 +45,6 @@ object SolverFactory { case _: java.io.IOException => false } - lazy val hasEld = try { - new CVC5Interpreter("eld", Array("-hsmt")).interrupt() - true - } catch { - case _: java.io.IOException => false - } - lazy val hasCVC4 = try { new CVC4Interpreter("cvc4", Array("-q", "--lang", "smt2.6")).interrupt() true @@ -90,20 +83,20 @@ object SolverFactory { "smt-z3:" -> "Z3 through SMT-LIB with custom executable name", "princess" -> "Princess with inox unrolling", "eval" -> "Internal evaluator to discharge ground assertions", - "horn-z3" -> "Horn solver using Z3 / Spacer", - "horn-eld" -> "Horn solver using Eldarica", + "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"), - "horn-z3" -> (() => hasNativeZ3, Seq("smt-z3", "smt-cvc4", "smt-cvc5", "princess"), "Z3 native interface"), - "horn-eld" -> (() => hasEld, Seq("smt-z3", "smt-cvc4", "smt-cvc5", "princess"), "Eldarica binary"), + "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") ) @@ -347,41 +340,7 @@ object SolverFactory { class Underlying(override val program: targetProgram.type) extends smtlib.SMTLIBSolver(program, context) - with smtlib.CVC5Solver { - override def targetName = "unmanaged/inter" - 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 HornEldInterpreter(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 HornEldInterpreter(targetName, opts.toArray, parserCtor = out => new Parser(new Lexer(out))) - } - } + with smtlib.EldaricaSolver override protected val underlyingHorn = Underlying(targetProgram) diff --git a/src/main/scala/inox/solvers/smtlib/EldaricaInterpreter.scala b/src/main/scala/inox/solvers/smtlib/EldaricaInterpreter.scala new file mode 100644 index 000000000..2d26d0895 --- /dev/null +++ b/src/main/scala/inox/solvers/smtlib/EldaricaInterpreter.scala @@ -0,0 +1,177 @@ +package inox.solvers.smtlib + +import _root_.smtlib.trees.Terms.* +import _root_.smtlib.printer.Printer +import _root_.smtlib.parser.Parser +import _root_.smtlib.Interpreter +import _root_.smtlib.theories.* +import java.io.BufferedReader +import _root_.smtlib.trees.CommandsResponses.* +import _root_.smtlib.trees.Commands.* +import java.io.StringReader +import java.util.concurrent.Future + +/** + * + * + * @param printer + * @param parser + */ +class EldaricaInterpreter(val printer: Printer, val parserCtor: BufferedReader => Parser) extends Interpreter { + + import collection.mutable.{Stack => MStack, Seq => MSeq} + + private val commands = MStack(MSeq.empty[SExpr]) + + private var lastModelResponse: Option[GetModelResponse] = None + + val parser = parserCtor(new BufferedReader(new StringReader(""))) // dummy parser + + private class InterruptibleExecutor[T]: + private var task: Option[Future[T]] = None + + private val executor = scala.concurrent.ExecutionContext.fromExecutorService(null) + + private def asCallable[A](block: => A): java.util.concurrent.Callable[A] = + new java.util.concurrent.Callable[A] { def call(): A = block } + + def execute(block: => T): Option[T] = + this.synchronized: // run only one task at a time + task = Some(executor.submit(asCallable(block))) + + val res = + try + Some(task.get.get()) // block for result or interrupt + catch + case e: java.util.concurrent.CancellationException => None // externally interrupted + case e: Exception => throw e + + task = None + res + + def interrupt(): Unit = + task.foreach(_.cancel(true)) + + private val executor = new InterruptibleExecutor[SExpr] + + /** + * args to run Eldarica calls under + */ + private val eldArgs = Array( + "-in", // read input from (simulated) stdin + "-hsmt", // use SMT-LIB2 input format + "-disj" // use disjunctive interpolation + ) + + def eval(cmd: SExpr): SExpr = + cmd match + case CheckSat() => + checkSat + case CheckSatAssuming(assumptions) => + def toAssertion(lit: PropLiteral): SExpr = + val PropLiteral(sym, polarity) = lit + val id = QualifiedIdentifier(SimpleIdentifier(sym), Some(Core.BoolSort())) + val term = if polarity then id else Core.Not(id) + Assert(term) + + commands.push(assumptions.map(toAssertion).to(MSeq)) + val res = checkSat + commands.pop() + res + case Echo(value) => + EchoResponseSuccess(value.toString) + case Exit() => + // equivalent to reset + commands.clear() + trySuccess + case GetInfo(flag) => + flag match + case VersionInfoFlag() => + GetInfoResponseSuccess(VersionInfoResponse("0.1"), Seq.empty) + case _ => Unsupported + case GetModel() => + getModel + case Pop(n) => + (1 to n).foreach(_ => commands.pop()) + trySuccess + case Push(n) => + (1 to n).foreach(_ => commands.push(MSeq())) + trySuccess + case Reset() => + commands.clear() + trySuccess + case SetOption(option) => + // slightly haphazard + // but we always expect that PrintSuccess(true) has been passed as the first command + trySuccess + case _ => + commands.push(commands.pop() :+ cmd) + trySuccess + + //A free method is kind of justified by the need for the IO streams to be closed, and + //there seems to be a decent case in general to have such a method for things like solvers + //note that free can be used even if the solver is currently solving, and act as a sort of interrupt + def free(): Unit = + commands.clear() + + def interrupt(): Unit = + executor.interrupt() + + private def trySuccess: SExpr = Success + + private def collapsedCommands = commands.toSeq.flatten + + private def checkSat: SExpr = + this.synchronized { + // reset last model + setLastModelResponse(None) + executor + .execute(seqCheckSat) + .getOrElse(CheckSatStatus(UnknownStatus)) + } + + private def seqCheckSat: SExpr = + val commands = collapsedCommands :+ CheckSat() + val script = commands.map(printer.toString).mkString("\n") + + val inputStream = new java.io.StringReader(script) + + val buffer = new java.io.ByteArrayOutputStream + val printStream = new java.io.PrintStream(buffer) + + // actually check sat, requesting a model if possible + Console.withIn(inputStream): + Console.withOut(printStream): + lazabs.Main.doMain(eldArgs, false) + + val eldRes = new java.io.BufferedReader(new java.io.StringReader(buffer.toString)) + + val parser = parserCtor(eldRes) + + val result = parser.parseCheckSatResponse + + result match + case CheckSatStatus(SatStatus) => + // FIXME: @sg: disabled due to non-SMTLIB compliant model printing from eldarica + // there will be a parser exception if we attemp this + // // if Sat, parse and store model + // val model = parser.parseGetModelResponse + // // could be a model or an error, in either case, this is the response for (get-model) + // setLastModelResponse(Some(model)) + setLastModelResponse(Some(GetModelResponseSuccess(Nil))) // empty model + result + case _ => + // if unsat or unknown, reset the model + setLastModelResponse(None) + result + + private def setLastModelResponse(model: Option[GetModelResponse]): Unit = + lastModelResponse = model + + private def getModel: SExpr = + lastModelResponse match + case Some(modelResponse) => + modelResponse + case None => + Error("No model available") +} diff --git a/src/main/scala/inox/solvers/smtlib/EldaricaSolver.scala b/src/main/scala/inox/solvers/smtlib/EldaricaSolver.scala new file mode 100644 index 000000000..760e1b534 --- /dev/null +++ b/src/main/scala/inox/solvers/smtlib/EldaricaSolver.scala @@ -0,0 +1,19 @@ +/* Copyright 2009-2018 EPFL, Lausanne */ + +package inox +package solvers +package smtlib + +import _root_.{smtlib => sl} +import _root_.smtlib.trees.Terms.{Identifier => _, _} +import _root_.smtlib.trees.CommandsResponses._ + +trait EldaricaSolver extends SMTLIBSolver with EldaricaTarget { + + protected val interpreter: sl.Interpreter = + new EldaricaInterpreter(sl.printer.RecursivePrinter, out => sl.parser.Parser(sl.extensions.tip.Lexer(out))) + + def targetName = "eldarica" + + protected def interpreterOpts: Seq[String] = Seq.empty +} diff --git a/src/main/scala/inox/solvers/smtlib/EldaricaTarget.scala b/src/main/scala/inox/solvers/smtlib/EldaricaTarget.scala new file mode 100644 index 000000000..0da970233 --- /dev/null +++ b/src/main/scala/inox/solvers/smtlib/EldaricaTarget.scala @@ -0,0 +1,19 @@ +/* Copyright 2009-2018 EPFL, Lausanne */ + +package inox +package solvers +package smtlib + +import _root_.smtlib.trees.Terms.{Identifier => SMTIdentifier, _} +import _root_.smtlib.trees.Commands._ +import _root_.smtlib.theories._ +import _root_.smtlib.theories.cvc._ + +trait EldaricaTarget extends SMTLIBTarget with SMTLIBDebugger { + import context.{given, _} + import program._ + import program.trees._ + import program.symbols.{given, _} + + override protected def toSMT(e: Expr)(using bindings: Map[Identifier, Term]) = super.toSMT(e) +}