diff --git a/src/main/scala/inox/solvers/cvc4/CVC4Solver.scala b/src/main/scala/inox/solvers/cvc4/CVC4Solver.scala
deleted file mode 100644
index ff112d7921fdf9f1c74bf7c7187f1e312c58d713..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/cvc4/CVC4Solver.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package cvc4
-
-trait CVC4Solver extends Solver
diff --git a/src/main/scala/inox/solvers/cvc4/CVC4UnrollingSolver.scala b/src/main/scala/inox/solvers/cvc4/CVC4UnrollingSolver.scala
deleted file mode 100644
index b293abbe209269ef1373ed4937be52a43850bc1c..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/cvc4/CVC4UnrollingSolver.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package solvers
-package cvc4
-
-import purescala.Definitions._
-
-import unrolling._
-import theories._
-
-class CVC4UnrollingSolver(context: SolverContext, program: Program, underlying: CVC4Solver)
- extends UnrollingSolver(context, program, underlying,
- theories = new BagEncoder(context.context, program))
- with CVC4Solver
diff --git a/src/main/scala/inox/solvers/isabelle/AdaptationPhase.scala b/src/main/scala/inox/solvers/isabelle/AdaptationPhase.scala
deleted file mode 100644
index d3743903d176b6ebe47220afbf5daed6753e5b41..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/AdaptationPhase.scala
+++ /dev/null
@@ -1,70 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import leon._
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.DefOps._
-import leon.purescala.Expressions._
-import leon.purescala.TypeOps
-import leon.purescala.Types._
-import leon.utils._
-
-object AdaptationPhase extends TransformationPhase {
-
- val name = "adaptation"
- val description = "Function parameter adaptation"
-
- implicit val debugSection = DebugSectionIsabelle
-
- def apply(context: LeonContext, program: Program): Program = {
- val dummy = program.library.Dummy match {
- case Some(dummy) => dummy
- case None => context.reporter.internalError("Definition of dummy type not found")
- }
-
- def mkDummyTyp(tp: TypeParameter) =
- CaseClassType(dummy, List(tp))
-
- def mkDummyParameter(tp: TypeParameter) =
- ValDef(FreshIdentifier("dummy", mkDummyTyp(tp)))
-
- def mkDummyArgument(tree: TypeTree) =
- CaseClass(CaseClassType(dummy, List(tree)), Nil)
-
- val enabled =
- context.findOptionOrDefault(GlobalOptions.optSelectedSolvers).contains("isabelle") ||
- context.findOptionOrDefault(Main.MainComponent.optIsabelle)
-
- if (!enabled) program
- else {
- context.reporter.debug("Running adaptation phase, because Isabelle is selected ...")
-
- val map = program.definedFunctions.flatMap { fd =>
- val expected = fd.tparams.map(_.tp).toSet
- val actual = fd.params.map(_.getType).flatMap(TypeOps.typeParamsOf).toSet ++ TypeOps.typeParamsOf(fd.returnType)
- if (expected == actual)
- None
- else {
- val diff: List[TypeParameter] = (expected -- actual).toList
- context.reporter.debug(s"Rewriting function definition ${fd.qualifiedName(program)}: adding dummies for hidden type parameter(s) ${diff.map(_.id).mkString(" and ")}")
- val nid = FreshIdentifier(fd.id.name, FunctionType(fd.params.map(_.getType) ++ diff.map(mkDummyTyp), fd.returnType))
- val nfd = fd.duplicate(id = nid, params = fd.params ++ diff.map(mkDummyParameter))
- Some(fd -> ((nfd, diff)))
- }
- }.toMap
-
- def mapFunDef(fd: FunDef): Option[FunDef] = map.get(fd).map(_._1)
-
- def mapFunInvocation(fi: FunctionInvocation, nfd: FunDef): Option[Expr] = map.get(fi.tfd.fd).map { case (_, diff) =>
- val inst = (nfd.tparams.map(_.tp) zip fi.tfd.tps).toMap
- val args = diff.map(t => mkDummyArgument(inst(t)))
- FunctionInvocation(nfd.typed(fi.tfd.tps), fi.args ++ args)
- }
-
- transformProgram(funDefReplacer(mapFunDef, mapFunInvocation), program)
- }
- }
-
-}
diff --git a/src/main/scala/inox/solvers/isabelle/Component.scala b/src/main/scala/inox/solvers/isabelle/Component.scala
deleted file mode 100644
index 463ed8478b62fb3753cf5522e14b485e7baccc58..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/Component.scala
+++ /dev/null
@@ -1,45 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import java.nio.file.Paths
-
-import scala.concurrent._
-import scala.concurrent.duration._
-import scala.concurrent.ExecutionContext.Implicits.global
-
-import leon._
-
-import edu.tum.cs.isabelle.setup._
-
-object Component extends LeonComponent {
-
- val name = "Isabelle"
- val description = "Isabelle solver"
-
- def platform =
- Platform.guess.getOrElse(sys.error("Unknown platform; can't run Isabelle here"))
-
- val optMapping = LeonFlagOptionDef(
- name = "isabelle:mapping",
- description = "Enable processing of type and function mapping annotations",
- default = true
- )
-
- val optDump = LeonStringOptionDef(
- name = "isabelle:dump",
- description = "Dump theory source files into the specified directory",
- default = "",
- usageRhs = "path"
- )
-
- val optStrict = LeonFlagOptionDef(
- name = "isabelle:strict",
- description = "Require proofs for indirectly referenced functions",
- default = true
- )
-
- override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optMapping, optDump, optStrict)
-
-}
diff --git a/src/main/scala/inox/solvers/isabelle/Functions.scala b/src/main/scala/inox/solvers/isabelle/Functions.scala
deleted file mode 100644
index a258fd1cd83813a05c0303af2d067f1e1f181f21..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/Functions.scala
+++ /dev/null
@@ -1,155 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import scala.concurrent._
-import scala.math.BigInt
-
-import leon.LeonContext
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.ExprOps
-import leon.purescala.Types._
-import leon.utils._
-
-import edu.tum.cs.isabelle._
-import edu.tum.cs.isabelle.pure.{Expr => _, _}
-
-final class Functions(context: LeonContext, program: Program, types: Types, funs: List[FunDef], system: System)(implicit ec: ExecutionContext) {
-
- private implicit val debugSection = DebugSectionIsabelle
- private val strict = context.findOptionOrDefault(Component.optStrict)
-
- private val translator = new Translator(context, program, types, system)
-
- private val allLemmas = program.definedFunctions.flatMap(_.checkLemma(program, context)).toMap
-
- private def closure(funs: Set[FunDef]): Set[FunDef] = {
- val referenced = funs.flatMap(program.callGraph.transitiveCallees)
- val lemmas = allLemmas.filter(_._2.exists(referenced.contains)).keySet
- if (lemmas.subsetOf(funs) && referenced.subsetOf(funs))
- funs
- else {
- context.reporter.debug(s"Discovered relevant lemma(s): ${lemmas.map(_.qualifiedName(program)).mkString(", ")}")
- closure(funs ++ referenced ++ lemmas)
- }
- }
-
- private val relevant = closure(funs.toSet).toList
-
- private val preGroups = program.callGraph.stronglyConnectedComponents.map(_.filter(relevant.contains)).filterNot(_.isEmpty).toSet
- private val callGraph = preGroups.map { group => group ->
- preGroups.filter(cand => cand.exists(to => group.exists(from => program.callGraph.calls(from, to))) && cand != group)
- }.toMap
-
- private val groups = GraphOps.topologicalSorting(callGraph) match {
- case Right(seq) => seq.toList
- case Left(_) => context.reporter.internalError("unexpected cycle in call graph")
- }
-
- context.reporter.debug(s"Functions to be defined: ${groups.map(_.map(_.qualifiedName(program)).mkString("{", ", ", "}")).mkString(", ")}")
-
- private def globalLookup(data: List[FunDef])(fun: FunDef, typ: Typ) =
- if (data.contains(fun))
- Const(s"${theory}.${fun.id.mangledName}", typ)
- else
- context.reporter.internalError(s"Unknown function ${fun.qualifiedName(program)}")
-
- private def processGroup(group: Set[FunDef], data: List[FunDef]): Future[List[FunDef]] = {
- def lookup(fun: FunDef, typ: Typ): Term =
- if (group.contains(fun))
- Free(fun.id.mangledName, typ)
- else if (data.contains(fun))
- Const(s"${theory}.${fun.id.mangledName}", typ)
- else
- context.reporter.internalError(s"Unknown function ${fun.qualifiedName(program)} while defining functions")
-
- val defs = group.toList
-
- context.reporter.debug(s"Defining function(s) ${defs.map(_.qualifiedName(program)).mkString(", ")} ...")
-
- val pairs = defs.flatMap { fun =>
- val name = fun.qualifiedName(program)
- fun.extAnnotations.get("isabelle.function") match {
- case Some(List(Some(name: String))) => Some(fun -> (fun.id.mangledName -> name))
- case Some(List(_)) =>
- context.reporter.fatalError(s"In function mapping for function definition $name: expected a string literal as name")
- case Some(_) =>
- context.reporter.internalError(s"Function mapping for function definition $name")
- case None =>
- None
- }
- }
-
- system.invoke(Declare)(defs.map(_.id.mangledName)).assertSuccess(context).flatMap { case () => Future.traverse(defs) { fun =>
- val name = fun.id.mangledName
- val params = Future.traverse(fun.params.toList) { param =>
- types.typ(param.getType, strict = true).map(param.id.mangledName -> _)
- }
-
- val full = fun.annotations.contains("isabelle.fullBody")
- val none = fun.annotations.contains("isabelle.noBody")
-
- val body = (full, none) match {
- case (true, false) => translator.term(fun.fullBody, Nil, lookup)
- case (false, true) => translator.mkFreshError(None)
- case (false, false) => translator.term(fun.body.get, Nil, lookup)
- case (true, true) => context.reporter.fatalError(s"Conflicting body annotations for function definition ${fun.qualifiedName(program)}")
- }
-
- for {
- params <- params
- body <- body
- typ <- types.typ(fun.returnType, strict = true)
- }
- yield
- (name, params, (body, typ))
- }}.flatMap(system.invoke(Functions)).assertSuccess(context).flatMap {
- case Some(msg) => context.reporter.fatalError(s"In function definition: $msg")
- case None =>
- def requireProof(fun: FunDef) = funs.contains(fun) || strict
-
- val (checked, unchecked) = pairs.partition { case (fun, _) => requireProof(fun) }
-
- val equivalences =
- for {
- failed <- system.invoke(Equivalences)(checked.map(_._2)).assertSuccess(context)
- () <- system.invoke(AssumeEquivalences)(unchecked.map(_._2)).assertSuccess(context)
- }
- yield failed
-
- equivalences.foreach {
- case Nil => ()
- case failed => context.reporter.warning(s"Equivalence check(s) for ${failed.mkString(" and ")} failed")
- }
- equivalences.map(_ => data ++ defs)
- }.flatMap { data =>
- def generateStatement(fun: FunDef): Option[Future[(String, Term)]] =
- fun.statement.map(expr => translator.term(expr, Nil, globalLookup(data)).map(fun.id.mangledName -> _))
-
- val lemmas =
- Future.sequence(defs.filterNot(funs.contains).flatMap(generateStatement)).flatMap { statements =>
- if (strict)
- system.invoke(Lemmas)(statements).assertSuccess(context)
- else
- system.invoke(AssumeLemmas)(statements).assertSuccess(context).map(_ => Nil)
- }
-
- lemmas.foreach {
- case Nil => ()
- case failed => context.reporter.warning(s"Proof(s) of lemma(s) for ${failed.mkString(" and ")} failed")
- }
-
- lemmas.map(_ => data)
- }
- }
-
- val data: Future[List[FunDef]] =
- groups.foldLeft(Future.successful(List.empty[FunDef])) { (acc, group) =>
- acc.flatMap(processGroup(group, _))
- }
-
- def term(expr: Expr): Future[Term] = data.flatMap(data => translator.term(expr, Nil, globalLookup(data)))
-
-}
diff --git a/src/main/scala/inox/solvers/isabelle/IsabelleEnvironment.scala b/src/main/scala/inox/solvers/isabelle/IsabelleEnvironment.scala
deleted file mode 100644
index 6b3346152ef0bfc0e4e16dd20291190154b5387d..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/IsabelleEnvironment.scala
+++ /dev/null
@@ -1,156 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import java.io.FileWriter
-import java.nio.file.{Files, Paths}
-
-import scala.concurrent._
-import scala.concurrent.duration._
-import scala.concurrent.ExecutionContext.Implicits.global
-
-import leon.LeonContext
-import leon.OptionsHelpers._
-import leon.GlobalOptions
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Common._
-import leon.solvers._
-import leon.utils._
-
-import edu.tum.cs.isabelle._
-import edu.tum.cs.isabelle.api._
-import edu.tum.cs.isabelle.setup._
-
-object IsabelleEnvironment {
-
- private implicit val debugSection = DebugSectionIsabelle
-
- def apply(context: LeonContext, program: Program): Future[IsabelleEnvironment] = {
- LeonLoggerFactory.reporter = context.reporter
-
- val version = Version(isabelleVersion)
- val dump = context.findOptionOrDefault(Component.optDump)
- val strict = context.findOptionOrDefault(Component.optStrict)
-
- val funFilter =
- // FIXME duplicated from AnalysisPhase
- filterInclusive[FunDef](context.findOption(GlobalOptions.optFunctions).map(fdMatcher(program)), Some(_.annotations contains "library"))
-
- val funs = program.definedFunctions.filter(funFilter)
-
- val scripts = funs.flatMap { fun =>
- val name = fun.qualifiedName(program)
- fun.extAnnotations.get("isabelle.script") match {
- case Some(List(Some(name: String), Some(source: String))) => Some(name -> source)
- case Some(List(_, _)) =>
- context.reporter.fatalError(s"In script for function definition $name: expected a string literal as name and a string literal as source")
- case Some(_) =>
- context.reporter.internalError(s"Script for function definition $name")
- case None =>
- None
- }
- }.toList
-
- context.reporter.info(s"Preparing Isabelle setup (this might take a while) ...")
- val setup = Setup.defaultSetup(version)
-
- val system = setup.flatMap { setup =>
- val resources = Resources.dumpIsabelleResources()
- val config = resources.makeConfiguration(Nil, "Leon")
-
- setup.makeEnvironment.flatMap { env =>
- context.reporter.info(s"Building session ...")
- if (!System.build(env, config))
- context.reporter.internalError("Build failed")
-
- context.reporter.info(s"Starting $version instance ...")
- System.create(env, config)
- }
- }
-
- val thy = system.flatMap { system =>
- context.reporter.debug(s"Loading theory as $theory ...")
-
- system.invoke(Load)(("Leon", theory, scripts)).assertSuccess(context).map {
- case Nil =>
- ()
- case bad =>
- context.reporter.fatalError(s"Could not process the following scripts: ${bad.mkString(", ")}")
- }
- }
-
- val oracle =
- if (strict) {
- context.reporter.debug("Strict mode enabled; background proofs will be replayed in Isabelle")
- Future.successful { () }
- }
- else {
- context.reporter.warning("Strict mode disabled; proofs may be unsound")
- thy.flatMap(_ => system.flatMap(_.invoke(Oracle)(()))).assertSuccess(context)
- }
-
- val types =
- for {
- s <- system
- () <- thy
- _ = context.reporter.debug(s"Defining types ...")
- }
- yield
- new Types(context, program, s)
-
- val functions =
- for {
- s <- system
- t <- types
- () <- oracle
- _ <- t.data
- }
- yield
- new Functions(context, program, t, funs, s)
-
- functions.flatMap(_.data).foreach { _ =>
- if (dump.isEmpty)
- system.foreach { sys =>
- sys.invoke(Report)(()).assertSuccess(context).foreach { report =>
- context.reporter.debug(s"Report for $theory ...")
- report.foreach { case (key, value) =>
- context.reporter.debug(s"$key: ${canonicalizeOutput(sys, value)}")
- }
- }
- }
- else
- system.flatMap(_.invoke(Dump)(())).assertSuccess(context).foreach { output =>
- context.reporter.debug(s"Dumping theory sources to $dump ...")
- val path = Files.createDirectories(Paths.get(dump))
- output.foreach { case (name, content) =>
- val writer = new FileWriter(path.resolve(s"$name.thy").toFile())
- writer.write(content)
- writer.close()
- }
- }
- }
-
- for {
- s <- system
- t <- types
- f <- functions
- _ <- t.data
- _ <- f.data
- }
- yield new IsabelleEnvironment(context, program, t, f, s, funs)
- }
-
-}
-
-final class IsabelleEnvironment private(
- val context: LeonContext,
- val program: Program,
- val types: Types,
- val functions: Functions,
- val system: System,
- val selectedFunDefs: List[FunDef]
-) {
- def solver: IsabelleSolver with TimeoutSolver =
- new IsabelleSolver(context.toSctx, program, types, functions, system) with TimeoutSolver
-}
diff --git a/src/main/scala/inox/solvers/isabelle/IsabellePhase.scala b/src/main/scala/inox/solvers/isabelle/IsabellePhase.scala
deleted file mode 100644
index 3cfe02990a70c14abf3a0df83536b21e6c18cd22..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/IsabellePhase.scala
+++ /dev/null
@@ -1,45 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import scala.concurrent._
-import scala.concurrent.duration._
-import scala.concurrent.ExecutionContext.Implicits.global
-
-import leon._
-import leon.purescala.Definitions._
-import leon.utils._
-import leon.verification._
-
-object IsabellePhase extends SimpleLeonPhase[Program, VerificationReport] {
-
- object IsabelleVC extends VCKind("Isabelle", "isa")
-
- val name = "isabelle"
- val description = "Isabelle verification"
-
- implicit val debugSection = DebugSectionIsabelle
-
- def apply(context: LeonContext, program: Program): VerificationReport = {
- val env = IsabelleEnvironment(context, program)
-
- val report = env.map { env =>
- def prove(fd: FunDef) = fd.statement.map { expr =>
- context.reporter.debug(s"Proving postcondition of ${fd.qualifiedName(program)} ...")
- val vc = VC(expr, fd, IsabelleVC).setPos(fd.getPos)
- val term = env.functions.term(expr)
- val input = term.map(t => (List(t), fd.proofMethod(vc, context)))
- val result = Await.result(input.flatMap(env.system.invoke(Prove)).assertSuccess(context), Duration.Inf) match {
- case Some(thm) => VCResult(VCStatus.Valid, None, None)
- case None => VCResult(VCStatus.Unknown, None, None)
- }
- vc -> Some(result)
- }
-
- VerificationReport(program, env.selectedFunDefs.flatMap(prove).toMap)
- }
-
- Await.result(report, Duration.Inf)
- }
-
-}
diff --git a/src/main/scala/inox/solvers/isabelle/IsabelleSolver.scala b/src/main/scala/inox/solvers/isabelle/IsabelleSolver.scala
deleted file mode 100644
index b1895380c94483c4646950d68b676aacf3cdb986..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/IsabelleSolver.scala
+++ /dev/null
@@ -1,98 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import scala.concurrent._
-import scala.concurrent.duration._
-
-import scala.math.BigInt
-
-import leon.LeonContext
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.solvers._
-import leon.utils.Interruptible
-import leon.verification.VC
-
-import edu.tum.cs.isabelle._
-import edu.tum.cs.isabelle.pure.{Expr => _, _}
-
-class IsabelleSolver(val sctx: SolverContext, program: Program, types: Types, functions: Functions, system: System) extends Solver with Interruptible { self: TimeoutSolver =>
-
- context.interruptManager.registerForInterrupts(this)
-
- import system.executionContext
-
- private def timeout = optTimeout.map(_.millis).getOrElse(Duration.Inf)
-
- val name = "isabelle"
-
- private var pending: List[Future[Term]] = Nil
- private var method: Option[String] = None
- private var running: Option[CancellableFuture[_]] = None
-
- def reset() = { pending = Nil; method = None; running = None }
- private def addPending(future: Future[Term]) = { pending ::= future }
- private def sequencePending() = { Future.sequence(pending) }
-
- override def assertVC(vc: VC): Unit = {
- val name = vc.fd.qualifiedName(program)
- addPending(functions.term(vc.condition))
- (vc.fd.proofMethod(vc, context), method) match {
- case (None, _) =>
- case (Some(m1), Some(m2)) if m1 == m2 =>
- case (Some(m1), Some(m2)) => context.reporter.error(s"In proof hint for function definition $name: can't override existing method $m2 with method $m1")
- case (Some(m1), None) => method = Some(m1)
- }
- }
-
- def check: Option[Boolean] = {
- val verdict = sequencePending().flatMapC { ts =>
- Future.traverse(ts)(system.invoke(Pretty)(_).assertSuccess(context)).foreach { strs =>
- context.reporter.debug(s"Attempting to prove disjunction of ${canonicalizeOutput(system, strs.mkString(", "))}")
- }
-
- system.cancellableInvoke(Prove)((ts, method))
- }
- running = Some(verdict)
-
- try {
- Await.result(verdict.future.assertSuccess(context), timeout) match {
- case Some(thm) =>
- context.reporter.debug(s"Proved theorem: ${canonicalizeOutput(system, thm)}")
- Some(false)
- case None =>
- None
- }
- }
- catch {
- case _: TimeoutException =>
- context.reporter.info("Isabelle timed out")
- verdict.cancel()
- None
- case _: CancellationException =>
- None
- }
- }
-
- def free(): Unit = {}
- def interrupt(): Unit = { running.foreach(_.cancel()) }
- def recoverInterrupt(): Unit = {}
-
- def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = None
-
- // 'check' never returns 'Some(true)'
- def getModel = sys.error("impossible")
-
- // 'checkAssumptions' never returns 'Some'
- def getUnsatCore = sys.error("impossible")
-
- // custom 'assertVC'
- def assertCnstr(expression: Expr): Unit = sys.error("impossible")
-
- // unimplemented
- def pop(): Unit = ???
- def push(): Unit = ???
-
-}
diff --git a/src/main/scala/inox/solvers/isabelle/IsabelleSolverFactory.scala b/src/main/scala/inox/solvers/isabelle/IsabelleSolverFactory.scala
deleted file mode 100644
index 11dfe40d392d1b0bb88fee7e1d7f9f1a2166450b..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/IsabelleSolverFactory.scala
+++ /dev/null
@@ -1,25 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import scala.concurrent._
-import scala.concurrent.duration._
-import scala.concurrent.ExecutionContext.Implicits.global
-
-import leon.LeonContext
-import leon.purescala.Definitions._
-import leon.solvers._
-
-final class IsabelleSolverFactory(context: LeonContext, program: Program) extends SolverFactory[TimeoutSolver] {
-
- val name = "isabelle"
-
- private val env = IsabelleEnvironment(context, program)
-
- override def shutdown() =
- Await.result(env.flatMap(_.system.dispose), Duration.Inf)
-
- def getNewSolver() =
- Await.result(env.map(_.solver), Duration.Inf)
-
-}
diff --git a/src/main/scala/inox/solvers/isabelle/LeonLoggerFactory.scala b/src/main/scala/inox/solvers/isabelle/LeonLoggerFactory.scala
deleted file mode 100644
index 078659c9c138fce536196c7642d5496dd85d9311..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/LeonLoggerFactory.scala
+++ /dev/null
@@ -1,48 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import org.slf4j.{Logger, ILoggerFactory}
-import org.slf4j.helpers.NOPLogger
-
-import info.hupel.slf4j.DefaultLogger
-
-import leon.Reporter
-import leon.utils._
-
-object LeonLoggerFactory {
-
- private implicit val debugSection = DebugSectionIsabelle
-
- private var _reporter: Option[Reporter] = None
-
- private[isabelle] def reporter_=(r: Reporter): Unit = _reporter = Some(r)
-
- private[isabelle] def reporter: Reporter = _reporter.getOrElse(sys.error("No reporter set"))
-
- private class LeonLogger extends DefaultLogger {
- import DefaultLogger._
- protected def writeLogMessage(level: LogLevel, message: Option[String], t: Option[Throwable] = None) {
- message.foreach { m =>
- level match {
- case TRACE => reporter.debug(m)
- case DEBUG => reporter.debug(m)
- case INFO => reporter.info(m)
- case WARN => reporter.warning(m)
- case ERROR => reporter.error(m)
- }
- }
- t.foreach(t => reporter.debug(t))
- }
-
- }
-
-}
-
-class LeonLoggerFactory extends ILoggerFactory {
- override def getLogger(name: String): Logger =
- if (name startsWith "edu.tum.cs.isabelle")
- new LeonLoggerFactory.LeonLogger
- else
- NOPLogger.NOP_LOGGER
-}
diff --git a/src/main/scala/inox/solvers/isabelle/Translator.scala b/src/main/scala/inox/solvers/isabelle/Translator.scala
deleted file mode 100644
index 3a0734726f0a2118bf3621fd1b9da35aa31b8f2e..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/Translator.scala
+++ /dev/null
@@ -1,329 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import scala.concurrent._
-import scala.math.BigInt
-
-import leon.LeonContext
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.ExprOps
-import leon.purescala.Types._
-import leon.utils._
-
-import edu.tum.cs.isabelle._
-import edu.tum.cs.isabelle.pure.{Expr => _, _}
-
-final class Translator(context: LeonContext, program: Program, types: Types, system: System)(implicit ec: ExecutionContext) {
-
- private implicit val debugSection = DebugSectionIsabelle
-
- private def mkApp(f: Term, args: Term*): Term =
- args.foldLeft(f) { (acc, arg) => App(acc, arg) }
-
- private def lookupConstructor(typ: CaseClassType): Future[Constructor] =
- types.data.map(_.get(Types.findRoot(typ).classDef).flatMap(_.constructors.get(typ.classDef)) match {
- case Some(constr) => constr
- case None => context.reporter.internalError(s"$typ not found in program")
- })
-
- private def mkFresh(typ: Option[TypeTree]) =
- system.invoke(Fresh)("fresh''").assertSuccess(context).flatMap { name =>
- types.optTyp(typ).map(Free(name, _))
- }
-
- def mkFreshError(typ: Option[TypeTree]): Future[Term] =
- system.invoke(SerialNat)(()).assertSuccess(context).flatMap { nat =>
- types.optTyp(typ).map { typ =>
- App(Const("Leon_Library.error", Type("fun", List(Typ.dummyT, typ))), nat)
- }
- }
-
- private def arity(typ: TypeTree): Int = typ match {
- case t: TupleType => t.dimension
- case _ => context.reporter.internalError(s"Expected tuple type, got $typ")
- }
-
- def term(expr: Expr, bounds: List[Identifier], consts: (FunDef, Typ) => Term): Future[Term] = {
- def mkAbs(params: List[Identifier], body: Expr, bounds: List[Identifier], wrap: Term => Term = identity): Future[Term] = params match {
- case Nil => term(body, bounds, consts)
- case p :: ps =>
- for {
- rec <- mkAbs(ps, body, p :: bounds, wrap)
- typ <- types.typ(p.getType)
- }
- yield
- wrap(Abs(p.mangledName /* name hint, no logical content */, typ, rec))
- }
-
- def nary(const: Term, xs: Expr*) =
- Future.traverse(xs.toList)(term(_, bounds, consts)).map(ts => mkApp(const, ts: _*))
-
- def flexary1(const: Term, xs: Seq[Expr]) =
- Future.traverse(xs.toList)(term(_, bounds, consts)).map(_.reduceRight { (t, acc) => mkApp(const, t, acc) })
-
- def flexary(const: Term, init: Term, xs: Seq[Expr]) =
- Future.traverse(xs.toList)(term(_, bounds, consts)).map(_.foldRight(init) { (t, acc) => mkApp(const, t, acc) })
-
- def inSet(set: Term, elem: Expr) =
- term(elem, bounds, consts).map(mkApp(Const("Set.member", Typ.dummyT), _, set))
-
- def lets(bindings: List[(Identifier, Term)], body: Expr) = {
- val referenced = ExprOps.variablesOf(body)
- val filtered = bindings.filter { case (id, _) => referenced contains id }
-
- val (names, rhss) = filtered.unzip
- rhss.foldLeft(mkAbs(names, body, bounds)) { (term, rhs) =>
- term.map(mkApp(Const("HOL.Let", Typ.dummyT), rhs, _))
- }
- }
-
- def let(name: Identifier, rhs: Term, body: Expr) =
- lets(List(name -> rhs), body)
-
- def precondition(pred: Expr, body: Expr) =
- for {
- p <- term(pred, bounds, consts)
- b <- term(body, bounds, consts)
- e <- mkFreshError(Some(body.getType))
- }
- yield
- mkApp(Const("HOL.If", Typ.dummyT), p, b, e)
-
- def postcondition(pred: Expr, body: Expr) =
- for {
- p <- term(pred, bounds, consts)
- b <- term(body, bounds, consts)
- e <- mkFreshError(Some(body.getType))
- }
- yield
- mkApp(Const("HOL.If", Typ.dummyT), App(p, b), b, e)
-
- def pattern(pat: Pattern): Future[Option[(Term, List[(Identifier, Term)])]] = {
- val res = pat match {
- case CaseClassPattern(_, typ, pats) =>
- Future.traverse(pats.toList)(pattern).flatMap { _.sequence match {
- case Some(args) =>
- val (pats, bindings) = args.unzip
-
- lookupConstructor(typ).map(_.term).map { head =>
- Some((mkApp(head, pats: _*), bindings.flatten))
- }
- case None =>
- Future.successful(None)
- }}
-
- case InstanceOfPattern(_, typ: CaseClassType) =>
- lookupConstructor(typ).flatMap { case Constructor(term, _, sels) =>
- val length = sels.size
- Future.traverse(1 to length) { _ => mkFresh(None) }.map { vars =>
- Some((mkApp(term, vars: _*), Nil))
- }
- }
-
- case TuplePattern(_, pats) =>
- Future.traverse(pats.toList)(pattern).map { _.sequence match {
- case Some(args) =>
- val (pats, bindings) = args.unzip
- val pat = pats.reduceRight { (p, acc) => mkApp(Const("Product_Type.Pair", Typ.dummyT), p, acc) }
- Some(pat, bindings.flatten)
- case None =>
- None
- }}
-
- case WildcardPattern(None) =>
- mkFresh(pat.binder.map(_.getType)).map { term => Some((term, Nil)) }
-
- case WildcardPattern(Some(id)) =>
- types.typ(id.getType).map { typ => Some((Free(id.mangledName, typ), Nil)) }
-
- case _ =>
- Future.successful(None)
- }
-
- val bind = pat match {
- case WildcardPattern(_) => false
- case _ => true
- }
-
- pat.binder match {
- case Some(id) if bind => res.map(_.map { case (term, bindings) =>
- (term, (id -> term) :: bindings)
- })
- case _ => res
- }
- }
-
- def clause(clause: MatchCase) = clause.optGuard match {
- case Some(_) =>
- Future.successful(None)
- case None =>
- pattern(clause.pattern).flatMap {
- case Some((pat, bindings)) =>
- lets(bindings, clause.rhs).map { term => Some(pat -> term) }
- case None =>
- Future.successful(None)
- }
- }
-
- expr match {
- case Variable(id) =>
- types.typ(id.getType) map { typ =>
- bounds.indexOf(id) match {
- case -1 => Free(id.mangledName, typ)
- case n => Bound(n)
- }
- }
-
- case Let(x, t, y) =>
- term(t, bounds, consts).flatMap { let(x, _, y) }
-
- case Lambda(args, expr) =>
- mkAbs(args.map(_.id).toList, expr, bounds)
-
- case Forall(args, expr) =>
- mkAbs(args.map(_.id).toList, expr, bounds, wrap = mkApp(Const("HOL.All", Typ.dummyT), _))
-
- case CaseClass(typ, exprs) =>
- lookupConstructor(typ).map(_.term).flatMap { nary(_, exprs: _*) }
-
- case CaseClassSelector(typ, expr, sel) =>
- lookupConstructor(typ).map(_.sels.collectFirst {
- case (field, term) if field.id == sel => term
- }).flatMap {
- case Some(term) => nary(term, expr)
- case None => context.reporter.internalError(s"$typ or $sel not found in program")
- }
-
- case IsInstanceOf(expr, typ: CaseClassType) =>
- lookupConstructor(typ).map(_.disc).flatMap { nary(_, expr) }
-
- case AsInstanceOf(expr, _) =>
- term(expr, bounds, consts)
-
- case Tuple(exprs) =>
- flexary1(Const("Product_Type.Pair", Typ.dummyT), exprs)
-
- case TupleSelect(expr, i) =>
- def sel(i: Int, len: Int, term: Term): Term = (i, len) match {
- case (1, _) => App(Const("Product_Type.prod.fst", Typ.dummyT), term)
- case (2, 2) => App(Const("Product_Type.prod.snd", Typ.dummyT), term)
- case _ => App(Const("Product_Type.prod.snd", Typ.dummyT), sel(i - 1, len - 1, term))
- }
-
- term(expr, bounds, consts).map(sel(i, arity(expr.getType), _))
-
- case MatchExpr(scrutinee, clauses) =>
- term(scrutinee, bounds, consts).flatMap { scrutinee =>
- Future.traverse(clauses.toList)(clause).flatMap { _.sequence match {
- case Some(clauses) =>
- val catchall =
- for {
- pat <- mkFresh(None)
- rhs <- mkFreshError(Some(expr.getType))
- }
- yield (pat, rhs)
-
- types.typ(expr.getType).flatMap { typ =>
- catchall.flatMap { catchall =>
- Future.traverse(bounds) { id =>
- types.typ(id.getType).map(id.mangledName -> _)
- }.flatMap { bounds =>
- system.invoke(Cases)(((scrutinee, bounds), (typ, clauses :+ catchall))).assertSuccess(context)
- }
- }
- }
- case None =>
- context.reporter.warning("Match uses unsupported features; translating to if-then-else")
- term(ExprOps.matchToIfThenElse(expr), bounds, consts)
- }}
- }
-
- case FunctionInvocation(fun, args) =>
- types.functionTyp(args.map(_.getType), expr.getType).flatMap { typ =>
- nary(consts(fun.fd, typ), args: _*)
- }
-
- case Application(fun, args) =>
- term(fun, bounds, consts).flatMap(nary(_, args: _*))
-
- case Error(tpe, _) =>
- mkFreshError(Some(tpe))
-
- case UnitLiteral() => Future.successful { Const("Product_Type.Unity", Typ.dummyT) }
- case BooleanLiteral(true) => Future.successful { Const("HOL.True", Typ.dummyT) }
- case BooleanLiteral(false) => Future.successful { Const("HOL.False", Typ.dummyT) }
-
- case InfiniteIntegerLiteral(n) =>
- system.invoke(NumeralLiteral)((n, Type("Int.int", Nil))).assertSuccess(context)
-
- case CharLiteral(c) =>
- types.char.flatMap(typ => system.invoke(NumeralLiteral)((c.toLong, typ))).assertSuccess(context)
-
- case IntLiteral(n) =>
- types.typ(expr.getType).flatMap(typ => system.invoke(NumeralLiteral)((n, typ))).assertSuccess(context)
-
- case Assert(pred, _, body) => precondition(pred, body)
- case Require(pred, body) => precondition(pred, body)
- case Ensuring(body, pred) => postcondition(pred, body)
-
- case IfExpr(x, y, z) => nary(Const("HOL.If", Typ.dummyT), x, y, z)
- case Not(x) => nary(Const("HOL.Not", Typ.dummyT), x)
- case Implies(x, y) => nary(Const("HOL.implies", Typ.dummyT), x, y)
- case And(xs) => flexary1(Const("HOL.conj", Typ.dummyT), xs)
- case Or(xs) => flexary1(Const("HOL.disj", Typ.dummyT), xs)
-
- // Isabelle doesn't have > or >=, need to swap operands in these cases
- case Equals(x, y) => nary(Const("HOL.eq", Typ.dummyT), x, y)
- case LessThan(x, y) => nary(Const("Orderings.ord_class.less", Typ.dummyT), x, y)
- case LessEquals(x, y) => nary(Const("Orderings.ord_class.less_eq", Typ.dummyT), x, y)
- case GreaterThan(x, y) => nary(Const("Orderings.ord_class.less", Typ.dummyT), y, x)
- case GreaterEquals(x, y) => nary(Const("Orderings.ord_class.less_eq", Typ.dummyT), y, x)
-
- case Plus(x, y) => nary(Const("Groups.plus_class.plus", Typ.dummyT), x, y)
- case Minus(x, y) => nary(Const("Groups.minus_class.minus", Typ.dummyT), x, y)
- case UMinus(x) => nary(Const("Groups.uminus_class.uminus", Typ.dummyT), x)
- case Times(x, y) => nary(Const("Groups.times_class.times", Typ.dummyT), x, y)
-
- case RealPlus(x, y) => nary(Const("Groups.plus_class.plus", Typ.dummyT), x, y)
- case RealMinus(x, y) => nary(Const("Groups.minus_class.minus", Typ.dummyT), x, y)
- case RealUMinus(x) => nary(Const("Groups.uminus_class.uminus", Typ.dummyT), x)
- case RealTimes(x, y) => nary(Const("Groups.times_class.times", Typ.dummyT), x, y)
-
- case FiniteSet(elems, _) => flexary(Const("Set.insert", Typ.dummyT), Const("Set.empty", Typ.dummyT), elems.toList)
- case SetUnion(x, y) => nary(Const("Lattices.sup_class.sup", Typ.dummyT), x, y)
- case SetIntersection(x, y) => nary(Const("Lattices.inf_class.inf", Typ.dummyT), x, y)
- case SetDifference(x, y) => nary(Const("Groups.minus_class.minus", Typ.dummyT), x, y)
- case SubsetOf(x, y) => nary(Const("Orderings.ord_class.less_eq", Typ.dummyT), x, y)
- case ElementOfSet(elem, set) => term(set, bounds, consts).flatMap(inSet(_, elem))
-
- case FiniteMap(elems, from, to) =>
- val es = Future.traverse(elems.toList) { case (k, v) => term(k, bounds, consts) zip term(v, bounds, consts) }
- for {
- f <- types.typ(from)
- t <- types.typ(to)
- es <- es
- res <- system.invoke(MapLiteral)((es, (f, t))).assertSuccess(context)
- }
- yield res
-
- case MapApply(map, key) =>
- term(map, bounds, consts).flatMap(nary(_, key)).map(App(Const("Option.option.the", Typ.dummyT), _))
- case MapIsDefinedAt(map, key) =>
- term(map, bounds, consts).flatMap { map =>
- inSet(App(Const("Map.dom", Typ.dummyT), map), key)
- }
- case MapUnion(x, y) => nary(Const("Map.map_add", Typ.dummyT), x, y)
-
- case Choose(pred) =>
- nary(Const("Hilbert_Choice.Eps", Typ.dummyT), pred)
-
- case _ =>
- context.reporter.warning(s"Unknown expression $expr, translating to unspecified term")
- mkFreshError(Some(expr.getType))
- }
- }
-
-}
diff --git a/src/main/scala/inox/solvers/isabelle/Types.scala b/src/main/scala/inox/solvers/isabelle/Types.scala
deleted file mode 100644
index 3847d80c5831fd84c1fc342c8fe8e9d61429c6bd..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/Types.scala
+++ /dev/null
@@ -1,196 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.isabelle
-
-import scala.concurrent._
-import scala.math.BigInt
-
-import leon.LeonContext
-import leon.purescala.Common._
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.Types._
-
-import edu.tum.cs.isabelle._
-import edu.tum.cs.isabelle.pure._
-
-case class Constructor(term: Term, disc: Term, sels: Map[ValDef, Term])
-case class Datatype(typ: String, constructors: Map[CaseClassDef, Constructor])
-
-object Types {
-
- def findRoot(typ: ClassType): ClassType =
- typ.parent.map(findRoot).getOrElse(typ)
-
-}
-
-final class Types(context: LeonContext, program: Program, system: System)(implicit ec: ExecutionContext) {
-
- lazy val char = system.invoke(WordLiteral)(32).assertSuccess(context)
-
- private val enableMapping = context.findOptionOrDefault(Component.optMapping)
-
- private val (mapped, unmapped) =
- program.classHierarchyRoots.map { root =>
- val descendants = root match {
- case ccd: CaseClassDef => List(ccd)
- case _ => root.knownDescendants.collect { case ccd: CaseClassDef => ccd }
- }
-
- root -> descendants
- }.toMap.partition { case (root, descendants) =>
- root.annotations.contains("isabelle.typ") && {
- if (!enableMapping)
- context.reporter.warning(s"Class definition ${root.id} is mapped, but mapping is disabled")
- enableMapping
- }
- }
-
- private val mappedData: Future[Map[ClassDef, Datatype]] = Future.traverse(mapped) { case (root, descendants) =>
- val name = root.extAnnotations("isabelle.typ") match {
- case List(Some(name: String)) => name
- case List(_) => context.reporter.fatalError(s"In type mapping for class definition ${root.id}: expected a string literal as name")
- case _ => context.reporter.internalError(s"Type mapping for class definition ${root.id}")
- }
-
- val constructors = descendants.map { desc =>
- val name = desc.extAnnotations.get("isabelle.constructor") match {
- case Some(List(Some(name: String))) => name
- case Some(List(_)) =>
- context.reporter.fatalError(s"In constructor mapping for class definition ${desc.id}: expected a string literal as name")
- case None =>
- context.reporter.fatalError(s"Expected constructor mapping for class definition ${desc.id}, because it inherits from ${root.id} which has a type mapping")
- case Some(_) =>
- context.reporter.internalError(s"Constructor mapping for class definition ${desc.id}")
- }
-
- (desc.id.mangledName, name)
- }.toList
-
- system.invoke(LookupDatatype)(name -> constructors).assertSuccess(context).map {
- case Left(err) =>
- context.reporter.fatalError(s"In mapping for class definition ${root.id}: $err")
- case Right(constructors) => root ->
- Datatype(
- typ = name,
- constructors =
- constructors.map { case (name, (term, disc, sels)) =>
- val desc = descendants.find(_.id.mangledName == name).get
- if (desc.fields.length != sels.length)
- context.reporter.fatalError(s"Invalid constructor mapping for ${desc.id}: Isabelle constructor $name has different number of arguments")
- desc -> Constructor(term, disc, (desc.fields, sels).zipped.toMap)
- }.toMap
- )
- }
- }.map(_.toMap)
-
- def optTyp(tree: Option[TypeTree]): Future[Typ] = tree match {
- case Some(tree) => typ(tree)
- case None => Future.successful(Typ.dummyT)
- }
-
- def typ(tree: TypeTree, subst: Map[Identifier, Identifier] = Map.empty, strict: Boolean = false): Future[Typ] = {
- def flexary1(constructor: String, ts: Seq[TypeTree]): Future[Typ] =
- Future.traverse(ts.toList)(typ(_, subst, strict)).map(_.reduceRight { (t, acc) => Type(constructor, List(t, acc)) })
-
- tree match {
- case BooleanType => Future.successful { Type("HOL.bool", Nil) }
- case IntegerType => Future.successful { Type("Int.int", Nil) }
- case UnitType => Future.successful { Type("Product_Type.unit", Nil) }
- case RealType => Future.successful { Type("Real.real", Nil) }
- case CharType => char
- case TypeParameter(id) =>
- val id0 = subst.getOrElse(id, id)
- Future.successful { TFree(s"'${id0.mangledName}", List("HOL.type")) }
- case SetType(base) =>
- typ(base, subst, strict).map { typ => Type("Set.set", List(typ)) }
- case TupleType(bases) =>
- flexary1("Product_Type.prod", bases)
- case FunctionType(args, res) =>
- for {
- r <- typ(res, subst, strict)
- as <- Future.traverse(args)(typ(_, subst, strict))
- }
- yield
- as.foldRight(r) { (t, acc) => Type("fun", List(t, acc)) }
- case bvt: BitVectorType =>
- system.invoke(WordLiteral)(bvt.size).assertSuccess(context)
- case MapType(from, to) =>
- for {
- f <- typ(from, subst, strict)
- t <- typ(to, subst, strict)
- }
- yield
- Type("fun", List(f, Type("Option.option", List(t))))
- case ct: ClassType =>
- val root = Types.findRoot(ct)
- Future.traverse(root.tps.toList) { typ(_, subst, strict) }.flatMap { args =>
- mappedData.map { _.get(root.classDef) match {
- case None => s"$theory.${root.id.mangledName}"
- case Some(datatype) => datatype.typ
- }}.map { Type(_, args) }
- }
- case StringType =>
- context.reporter.warning("Strings are not yet supported, translating to unspecified type")
- Future.successful { Type("Leon_Library.string", Nil) }
- case _ if strict =>
- context.reporter.fatalError(s"Unsupported type $tree, can't be inferred")
- case _ =>
- context.reporter.warning(s"Unknown type $tree, translating to dummy (to be inferred)")
- Future.successful { Typ.dummyT }
- }
- }
-
- def functionTyp(args: Seq[TypeTree], res: TypeTree): Future[Typ] =
- typ(res).flatMap { res =>
- Future.traverse(args.toList)(typ(_)).map(_.foldRight(res) { (t, acc) => Type("fun", List(t, acc)) })
- }
-
- private val unmappedData: Future[Map[ClassDef, Datatype]] = {
- val entries = unmapped.map { case (root, descendants) =>
- val name = s"$theory.${root.id.mangledName}"
-
- if (!enableMapping)
- descendants.foreach { desc =>
- if (desc.annotations.contains("isabelle.constructor"))
- context.reporter.warning(s"Ignoring constructor mapping of class definition ${desc.id}, because its root ${root.id} has no type mapping")
- }
-
- val constructors = descendants.map { desc => desc ->
- Constructor(
- term = Const(s"$name.c${desc.id.mangledName}", Typ.dummyT),
- disc = Const(s"$name.d${desc.id.mangledName}", Typ.dummyT),
- sels = desc.fields.map { field => field ->
- Const(s"$name.s${field.id.mangledName}", Typ.dummyT)
- }.toMap
- )
- }.toMap
-
- root -> Datatype(name, constructors)
- }
-
- val translation = Future.traverse(entries.toList) { case (cls, Datatype(_, constructors)) =>
- val tparams = cls.tparams.map(_.id)
- Future.traverse(constructors.toList) { case (subcls, Constructor(_, _, sels)) =>
- val subst = (subcls.tparams.map(_.id), tparams).zipped.toMap
- Future.traverse(subcls.fields.toList) { field =>
- typ(field.getType, subst, true).map { typ =>
- field.id.mangledName -> typ
- }
- }.map {
- subcls.id.mangledName -> _
- }
- }.map {
- (cls.id.mangledName, tparams.toList.map(_.mangledName), _)
- }
- }
-
- translation.flatMap(system.invoke(Datatypes)).assertSuccess(context).map {
- case None => entries
- case Some(msg) => context.reporter.fatalError(s"In datatype definition: $msg")
- }
- }
-
- val data = for { d1 <- mappedData; d2 <- unmappedData } yield d1 ++ d2
-
-}
diff --git a/src/main/scala/inox/solvers/isabelle/package.scala b/src/main/scala/inox/solvers/isabelle/package.scala
deleted file mode 100644
index 2e5341013311cd469c4fb9f1a8d3dabc10ac738d..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/isabelle/package.scala
+++ /dev/null
@@ -1,142 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers.isabelle
-
-import scala.concurrent._
-import scala.math.BigInt
-import scala.reflect.NameTransformer
-
-import leon.LeonContext
-import leon.purescala.Common.Identifier
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.verification.VC
-
-import edu.tum.cs.isabelle._
-import edu.tum.cs.isabelle.api.Environment
-import edu.tum.cs.isabelle.pure.{Expr => _, _}
-
-import shapeless.tag
-
-object `package` {
-
- val theory = "Leon_Runtime"
- val isabelleVersion = "2016"
-
-
- implicit class FutureResultOps[A](val future: Future[ProverResult[A]]) extends AnyVal {
- def assertSuccess(context: LeonContext)(implicit ec: ExecutionContext): Future[A] = future map {
- case ProverResult.Success(a) => a
- case ProverResult.Failure(err: Operation.ProverException) => context.reporter.internalError(err.fullMessage)
- case ProverResult.Failure(err) => context.reporter.internalError(err.getMessage)
- }
- }
-
- implicit class ListOptionOps[A](val list: List[Option[A]]) extends AnyVal {
- def sequence: Option[List[A]] = list match {
- case Nil => Some(Nil)
- case None :: _ => None
- case Some(x) :: xs => xs.sequence.map(x :: _)
- }
- }
-
- implicit class IdentifierOps(val id: Identifier) extends AnyVal {
- def mangledName: String =
- NameTransformer.encode(id.name)
- .replace("_", "'u'")
- .replace("$", "'d'")
- .replaceAll("^_*", "")
- .replaceAll("_*$", "")
- .replaceAll("^'*", "") + "'" + id.globalId
- }
-
- implicit class FunDefOps(val fd: FunDef) extends AnyVal {
- private def name = fd.id.name
-
- def statement: Option[Expr] = fd.postcondition match {
- case Some(post) =>
- val args = fd.params.map(_.id.toVariable)
- val appliedPost = Application(post, List(FunctionInvocation(fd.typed, args)))
- Some(fd.precondition match {
- case None => appliedPost
- case Some(pre) => Implies(pre, appliedPost)
- })
- case None => None
- }
-
- def proofMethod(vc: VC, context: LeonContext): Option[String] =
- fd.extAnnotations.get("isabelle.proof") match {
- case Some(List(Some(method: String), Some(kind: String))) =>
- val kinds = kind.split(',')
- if (kinds.contains(vc.kind.name) || kind == "")
- Some(method)
- else {
- context.reporter.warning(s"Ignoring proof hint for function definition $name: only applicable for VC kinds ${kinds.mkString(", ")}")
- None
- }
- case Some(List(Some(method: String), None)) =>
- Some(method)
- case Some(List(_, _)) =>
- context.reporter.fatalError(s"In proof hint for function definition $name: expected a string literal as method and (optionally) a string literal as kind")
- case Some(_) =>
- context.reporter.internalError(s"Proof hint for function definition $name")
- case None =>
- None
- }
-
- def isLemma: Boolean =
- fd.annotations.contains("isabelle.lemma")
-
- def checkLemma(program: Program, context: LeonContext): Option[(FunDef, List[FunDef])] = {
- val name = fd.qualifiedName(program)
-
- def error(msg: String) =
- context.reporter.fatalError(s"In lemma declaration for function definition $name: $msg")
-
- fd.extAnnotations.get("isabelle.lemma") match {
- case Some(List(Some(abouts: String))) =>
- val refs = abouts.split(',').toList.map { about =>
- program.lookupAll(about) match {
- case List(fd: FunDef) if !fd.isLemma => fd
- case List(_: FunDef) => error(s"lemmas can only be about plain functions, but $about is itself a lemma")
- case Nil | List(_) => error(s"$about is not a function definition")
- case _ => error(s"$about is ambiguous")
- }
- }
- Some(fd -> refs)
- case Some(List(_)) => error("expected a string literal for about")
- case Some(_) => context.reporter.internalError(s"Lemma declaration for function definition $name")
- case None => None
- }
- }
- }
-
- def canonicalizeOutput(system: System, str: String) = {
- // FIXME use this everywhere
- val raw = """\s+""".r.replaceAllIn(str, " ")
- system.env.decode(tag[Environment.Raw].apply(raw))
- }
-
- val Prove = Operation.implicitly[(List[Term], Option[String]), Option[String]]("prove")
- val Pretty = Operation.implicitly[Term, String]("pretty")
- val Load = Operation.implicitly[(String, String, List[(String, String)]), List[String]]("load")
- val Report = Operation.implicitly[Unit, List[(String, String)]]("report")
- val Dump = Operation.implicitly[Unit, List[(String, String)]]("dump")
- val Oracle = Operation.implicitly[Unit, Unit]("oracle")
- val Fresh = Operation.implicitly[String, String]("fresh")
- val NumeralLiteral = Operation.implicitly[(BigInt, Typ), Term]("numeral_literal")
- val Cases = Operation.implicitly[((Term, List[(String, Typ)]), (Typ, List[(Term, Term)])), Term]("cases")
- val SerialNat = Operation.implicitly[Unit, Term]("serial_nat")
- val MapLiteral = Operation.implicitly[(List[(Term, Term)], (Typ, Typ)), Term]("map_literal")
- val Functions = Operation.implicitly[(List[(String, List[(String, Typ)], (Term, Typ))]), Option[String]]("functions")
- val Declare = Operation.implicitly[List[String], Unit]("declare")
- val Equivalences = Operation.implicitly[List[(String, String)], List[String]]("equivalences")
- val AssumeEquivalences = Operation.implicitly[List[(String, String)], Unit]("assume_equivalences")
- val Lemmas = Operation.implicitly[List[(String, Term)], List[String]]("lemmas")
- val AssumeLemmas = Operation.implicitly[List[(String, Term)], Unit]("assume_lemmas")
- val WordLiteral = Operation.implicitly[BigInt, Typ]("word_literal")
- val Datatypes = Operation.implicitly[List[(String, List[String], List[(String, List[(String, Typ)])])], Option[String]]("datatypes")
- val LookupDatatype = Operation.implicitly[(String, List[(String, String)]), Either[String, List[(String, (Term, Term, List[Term]))]]]("lookup_datatype")
-
-}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
deleted file mode 100644
index ff27a312f858992f5fdd890181f9d86ac5f8aac3..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
+++ /dev/null
@@ -1,25 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package smtlib
-
-import purescala.Definitions.Program
-
-class SMTLIBCVC4CounterExampleSolver(context: SolverContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
-
- override def targetName = "cvc4-cex"
-
- override def interpreterOps(ctx: LeonContext) = {
- Seq(
- "-q",
- "--rewrite-divk",
- "--produce-models",
- "--print-success",
- "--lang", "smt2.5",
- "--fmf-fun"
- ) ++ userDefinedOps(ctx)
- }
-
- protected val allowQuantifiedAssertions: Boolean = false
-}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
deleted file mode 100644
index ce6b963ba88fe7e5280f6e30291d56a17d431b4b..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ /dev/null
@@ -1,47 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package smtlib
-
-import purescala.Definitions.Program
-import purescala.Expressions.Expr
-
-import _root_.smtlib.parser.Commands.{Assert => SMTAssert}
-import _root_.smtlib.parser.Terms.{Exists => SMTExists}
-
-class SMTLIBCVC4ProofSolver(context: SolverContext, program: Program)
- extends SMTLIBCVC4QuantifiedSolver(context, program) {
-
- override def targetName = "cvc4-proof"
-
- override def interpreterOps(ctx: LeonContext) = {
- Seq(
- "-q",
- "--print-success",
- "--lang", "smt2.5",
- "--quant-ind",
- "--rewrite-divk",
- "--conjecture-gen",
- "--conjecture-gen-per-round=3",
- "--conjecture-gen-gt-enum=40",
- "--full-saturate-quant"
- ) ++ userDefinedOps(ctx)
- }
-
- // For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free
- override def assertCnstr(e: Expr) = try {
- emit(SMTAssert(quantifiedTerm(SMTExists, e)(Map())))
- } catch {
- case _ : SMTLIBUnsupportedError =>
- addError()
- }
-
- // This solver does not support model extraction
- override def getModel: solvers.Model = {
- // We don't send the error through reporter because it may be caught by PortfolioSolver
- throw LeonFatalError(Some(s"Solver $name does not support model extraction."))
- }
-
- protected val allowQuantifiedAssertions: Boolean = true
-}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
deleted file mode 100644
index 86768670465a89ea498e5bf30d29fc19d578c48a..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ /dev/null
@@ -1,14 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package smtlib
-
-import purescala.Definitions.Program
-
-// This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
-// It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
-abstract class SMTLIBCVC4QuantifiedSolver(context: SolverContext, program: Program)
- extends SMTLIBCVC4Solver(context, program)
- with SMTLIBQuantifiedSolver
- with SMTLIBCVC4QuantifiedTarget
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
deleted file mode 100644
index 8b5fd705b6aa6fe37ff55a0c902599f957f2011b..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ /dev/null
@@ -1,114 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package smtlib
-
-import purescala.Expressions._
-import purescala.Constructors._
-import purescala.Definitions._
-import purescala.DefOps.typedTransitiveCallees
-
-import _root_.smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
-import _root_.smtlib.parser.Terms.{Exists => SMTExists, Forall => SMTForall, _ }
-import _root_.smtlib.theories.Core.Equals
-import _root_.smtlib.parser.Commands._
-
-trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target with SMTLIBQuantifiedTarget {
-
- override def targetName = "cvc4-quantified"
-
- override def declareFunction(tfd: TypedFunDef): SSymbol = {
- val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
-
- if (!exploredAll) {
- context.reporter.warning(
- "Did not manage to explore the space of typed functions " +
- s"transitively called from ${tfd.id}. The solver may fail"
- )
- }
-
- // define-funs-rec does not accept parameterless functions, so we have to treat them differently:
- // we declare-fun each one and assert it is equal to its body
- val (withParams, withoutParams) = funs.toSeq filterNot functions.containsA partition(_.params.nonEmpty)
-
- // FIXME this may introduce dependency errors
- val parameterlessAssertions = withoutParams flatMap { tfd =>
- val s = super.declareFunction(tfd)
-
- try {
- val bodyAssert = tfd.body.map { body =>
- SMTAssert(Equals(s: Term, toSMT(body)(Map())))
- }
-
- val specAssert = tfd.postcondition map { post =>
- val term = implies(
- tfd.precOrTrue,
- application(post, Seq(FunctionInvocation(tfd, Seq())))
- )
- SMTAssert(toSMT(term)(Map()))
- }
-
- bodyAssert ++ specAssert
- } catch {
- case _ : SMTLIBUnsupportedError =>
- addError()
- Seq()
- }
- }
-
- val smtFunDecls = withParams map { tfd =>
- val id = if (tfd.tps.isEmpty) {
- tfd.id
- } else {
- tfd.id.freshen
- }
- val sym = id2sym(id)
- functions +=(tfd, sym)
- FunDec(
- sym,
- tfd.params map { p => SortedVar(id2sym(p.id), declareSort(p.getType)) },
- declareSort(tfd.returnType)
- )
- }
-
- val smtBodies = smtFunDecls map { case f =>
- val tfd = functions.toA(f.name)
- try {
- toSMT(tfd.body.get)(tfd.params.map { p =>
- (p.id, id2sym(p.id): Term)
- }.toMap)
- } catch {
- case _: SMTLIBUnsupportedError =>
- addError()
- toSMT(Error(tfd.body.get.getType, ""))(Map())
- }
- }
-
- if (smtFunDecls.nonEmpty) {
- emit(DefineFunsRec(smtFunDecls, smtBodies))
- // Assert contracts for defined functions
- if (allowQuantifiedAssertions) for {
- // If we encounter a function that does not refer to the current function,
- // it is sound to assume its contracts for all inputs
- tfd <- withParams if !refersToCurrent(tfd.fd)
- post <- tfd.postcondition
- } {
- val term = implies(
- tfd.precOrTrue,
- application(post, Seq(tfd.applied))
- )
- try {
- emit(SMTAssert(quantifiedTerm(SMTForall, term)(Map())))
- } catch {
- case _ : SMTLIBUnsupportedError =>
- addError()
- }
- }
- }
-
- parameterlessAssertions.foreach(a => emit(a))
-
- functions.toB(tfd)
- }
-}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBQuantifiedSolver.scala
deleted file mode 100644
index d4819cfbae997d729e064926b98cc879f0effeb0..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBQuantifiedSolver.scala
+++ /dev/null
@@ -1,29 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package smtlib
-
-import purescala.Common.Identifier
-import verification.VC
-
-trait SMTLIBQuantifiedSolver {
- this: SMTLIBSolver with SMTLIBQuantifiedTarget =>
-
- // We need to know the function context.
- // The reason is we do not want to assume postconditions of functions referring to
- // the current function, as this may make the proof unsound
- override def assertVC(vc: VC) = {
- dbg(s"; Solving $vc")
- currentFunDef = Some(vc.fd)
- assertCnstr(withInductiveHyp(vc.condition))
- }
-
- // Normally, UnrollingSolver tracks the input variable, but this one
- // is invoked alone so we have to filter them here
- override def getModel: Model = {
- val filter = currentFunDef.map{ _.paramIds.toSet }.getOrElse( (_:Identifier) => true )
- getModel(filter)
- }
-
-}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBQuantifiedTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBQuantifiedTarget.scala
deleted file mode 100644
index 76037a9451a27011a7ff47609073fcc07e99a92b..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBQuantifiedTarget.scala
+++ /dev/null
@@ -1,42 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package smtlib
-
-import purescala.Expressions._
-import purescala.Definitions._
-import purescala.Constructors._
-import purescala.ExprOps._
-
-trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
-
- protected var currentFunDef: Option[FunDef] = None
-
- protected def refersToCurrent(fd: FunDef) = {
- (currentFunDef contains fd) || (currentFunDef exists {
- program.callGraph.transitivelyCalls(fd, _)
- })
- }
-
- protected val allowQuantifiedAssertions: Boolean
-
- protected val typedFunDefExplorationLimit = 10000
-
- protected def withInductiveHyp(cond: Expr): Expr = {
-
- val inductiveHyps = for {
- fi @ FunctionInvocation(tfd, args) <- functionCallsOf(cond).toSeq
- } yield {
- val post = application(
- tfd.withParamSubst(args, tfd.postOrTrue),
- Seq(fi)
- )
- and(tfd.precOrTrue, post)
- }
-
- // We want to check if the negation of the vc is sat under inductive hyp.
- // So we need to see if (indHyp /\ !vc) is satisfiable
- liftLets(matchToIfThenElse(andJoin(inductiveHyps :+ not(cond))))
- }
-}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
deleted file mode 100644
index 7dd3e4be718ce0e2d39de37086ccc637cc90d202..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ /dev/null
@@ -1,18 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package smtlib
-
-import purescala.Definitions.Program
-
-import theories._
-
-/**
- * This solver models function definitions as universally quantified formulas.
- * It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
- */
-class SMTLIBZ3QuantifiedSolver(context: SolverContext, program: Program)
- extends SMTLIBZ3Solver(context, program)
- with SMTLIBQuantifiedSolver
- with SMTLIBZ3QuantifiedTarget
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
deleted file mode 100644
index 9b696cea0b496014d402ac4b9f9491d4b9494272..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ /dev/null
@@ -1,69 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package smtlib
-
-import purescala.Expressions._
-import purescala.Constructors._
-import purescala.Definitions._
-import purescala.DefOps.typedTransitiveCallees
-
-import _root_.smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
-import _root_.smtlib.parser.Terms.{Exists => SMTExists, Forall => SMTForall, _ }
-
-trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target with SMTLIBQuantifiedTarget {
-
- protected val allowQuantifiedAssertions: Boolean = true
-
- override def targetName = "z3-q"
-
- override def declareFunction(tfd: TypedFunDef): SSymbol = {
-
- val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
-
- if (!exploredAll) {
- context.reporter.warning(
- "Did not manage to explore the space of typed functions " +
- s"transitively called from ${tfd.id}. The solver may fail"
- )
- }
-
- val notSeen = funs.toSeq filterNot functions.containsA
-
- val smtFunDecls = notSeen map super.declareFunction
-
- smtFunDecls foreach { sym =>
- val tfd = functions.toA(sym)
- val term = quantifiedTerm(
- SMTForall,
- tfd.paramIds,
- Equals(
- FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
- tfd.body.get
- )
- )(Map())
- emit(SMTAssert(term))
- }
-
- // If we encounter a function that does not refer to the current function,
- // it is sound to assume its contracts for all inputs
- if (allowQuantifiedAssertions) for {
- tfd <- notSeen if !refersToCurrent(tfd.fd)
- post <- tfd.postcondition
- } {
- val term = implies(
- tfd.precOrTrue,
- application(post, Seq(tfd.applied))
- )
- try {
- emit(SMTAssert(quantifiedTerm(SMTForall, term)(Map())))
- } catch {
- case _ : SMTLIBUnsupportedError =>
- addError()
- }
- }
-
- functions.toB(tfd)
- }
-}
diff --git a/src/main/scala/inox/solvers/string/StringSolver.scala b/src/main/scala/inox/solvers/string/StringSolver.scala
deleted file mode 100644
index c39dc9043500498f1a0e4fbde866a0a2259aa77f..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/string/StringSolver.scala
+++ /dev/null
@@ -1,705 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.solvers.string
-
-import leon.purescala.Common._
-import scala.collection.mutable.ListBuffer
-import scala.annotation.tailrec
-
-/**
- * @author Mikael
- */
-object StringSolver {
- type Assignment = Map[Identifier, String]
-
- type StringFormToken = Either[String, Identifier]
-
- type StringForm = List[StringFormToken]
-
- type Equation = (StringForm, String)
-
- /** Sequences of equalities such as xyz"1"uv"2" = "1, 2" */
- type Problem = List[Equation]
-
- def renderStringForm(sf: StringForm): String = sf match {
- case Left(const)::Nil => "\""+const+"\""
- case Right(id)::Nil => id.toString
- case Left(const)::q => "\""+const+"\"+" + renderStringForm(q)
- case Right(id)::q => id.toString + "+" + renderStringForm(q)
- case Nil => ""
- }
-
- def renderProblem(p: Problem): String = {
- def renderEquation(e: Equation): String = {
- renderStringForm(e._1) + "==\""+e._2+"\""
- }
- p match {case Nil => ""
- case e::q => renderEquation(e) + ", " + renderProblem(q)}
- }
-
- /** Evaluates a String form. Requires the solution to have an assignment to all identifiers. */
- @tailrec def evaluate(s: Assignment, acc: StringBuffer = new StringBuffer(""))(sf: StringForm): String = sf match {
- case Nil => acc.toString
- case Left(constant)::q => evaluate(s, acc append constant)(q)
- case Right(identifier)::q => evaluate(s, acc append s(identifier))(q)
- }
-
- /** Assigns the new values to the equations and simplify them at the same time. */
- @tailrec def reduceStringForm(s: Assignment, acc: ListBuffer[StringFormToken] = ListBuffer())(sf: StringForm): StringForm = sf match {
- case Nil => acc.toList
- case (l@Left(constant))::(l2@Left(constant2))::q => reduceStringForm(s, acc)(Left(constant + constant2)::q)
- case (l@Left(constant))::(r2@Right(id))::q =>
- s.get(id) match {
- case Some(sid) =>
- reduceStringForm(s, acc)(Left(constant + sid)::q)
- case None =>
- reduceStringForm(s, (acc += l) += r2)(q)
- }
- case (l@Left(constant))::q => reduceStringForm(s, acc += l)(q)
- case (r@Right(id))::q =>
- s.get(id) match {
- case Some(sid) =>
- reduceStringForm(s, acc)(Left(sid)::q)
- case None =>
- reduceStringForm(s, acc += r)(q)
- }
- }
-
- /** Assignes the variable to their values in all equations and simplifies them. */
- def reduceProblem(s: Assignment, acc: ListBuffer[Equation] = ListBuffer())(p: Problem): Problem = p match {
- case Nil => acc.toList
- case ((sf, rhs)::q) => reduceProblem(s, acc += ((reduceStringForm(s)(sf): StringForm, rhs)))(q)
- }
-
- /** Computes a foldable property on the problem */
- def fold[T](init: T, s: StringFormToken => T, f: (T, T) => T)(p: Problem) = {
- p.view.foldLeft(init) {
- case (t, (lhs, rhs)) =>
- lhs.view.foldLeft(t) {
- case (t, sft) => f(t, s(sft))
- }
- }
- }
-
- /** Returns true if there is a StringFormToken which satisfies the given property */
- def exists(s: StringFormToken => Boolean)(p: Problem) = fold[Boolean](false, s, _ || _)(p)
- /** Counts the number of StringFormToken which satisfy the given property */
- def count(s: StringFormToken => Boolean)(p: Problem) = fold[Int](0, s andThen (if(_) 1 else 0), _ + _)(p)
-
- /** Maps every StringFormToken of the problem to create a new one */
- def map(s: StringFormToken => StringFormToken)(p: Problem): Problem = {
- p.map { case (lhs, rhs) => (lhs map s, rhs) }
- }
-
- /** Returns true if the assignment is a solution to the problem */
- def errorcheck(p: Problem, s: Assignment): Option[String] = {
- val res = p flatMap {eq =>
- val resultNotCorrect = reduceStringForm(s)(eq._1) match {
- case Left(a)::Nil if a == eq._2 => None
- case Nil if eq._2 == "" => None
- case res => Some(res)
- }
- if(resultNotCorrect.nonEmpty) Some(renderStringForm(eq._1) + " == "+ renderStringForm(resultNotCorrect.get) + ", but expected " + eq._2) else None
- }
- if(res == Nil) None else Some(res.mkString("\n") + "\nAssignment: " + s)
- }
-
- /** Concatenates constants together */
- def reduceStringForm(s: StringForm): StringForm = {
- @tailrec def rec(s: StringForm, acc: ListBuffer[StringFormToken] = ListBuffer()): StringForm = s match {
- case Nil => acc.toList
- case Left("")::q => rec(q, acc)
- case Left(c)::Left(d)::q => rec(Left(c+d)::q, acc)
- case a::q => rec(q, acc += a)
- }
- rec(s)
- }
-
- /** Split the stringFrom at the last constant.
- * @param s The concatenation of constants and variables
- * @return (a, b, c) such that a ++ Seq(b) ++ c == s and b is the last constant of s */
- def splitAtLastConstant(s: StringForm): (StringForm, StringFormToken, StringForm) = {
- val i = s.lastIndexWhere(x => x.isInstanceOf[Left[_, _]])
- (s.take(i), s(i), s.drop(i+1))
- }
-
- /** Use `val ConsReverse(init, last) = list` to retrieve the n-1 elements and the last element directly. */
- object ConsReverse {
- def unapply[A](l: List[A]): Option[(List[A], A)] = {
- if(l.nonEmpty) Some((l.init, l.last)) else None
- }
- def apply[A](q: List[A], a: A): List[A] = q :+ a
- }
-
-
- /** Returns all start positions of the string s in text.*/
- def occurrences(s: String, text: String): List[Int] = {
- ("(?="+java.util.regex.Pattern.quote(s)+")").r.findAllMatchIn(text).map(m => m.start).toList
- }
-
- /** Returns a list of all possible positions of the constants inside the string */
- def repartitions(constants: List[String], text: String): List[List[Int]] = constants match {
- case Nil => List(List())
- case c::q =>
- occurrences(c, text).flatMap(startPos =>
- repartitions(q, text.substring(startPos + c.length))
- .map(startPos :: _.map(_ + (startPos + c.length))))
- }
-
- /** Computes the Combinatorial coefficient c(n, k)*/
- def cnk(n: BigInt, k: BigInt): BigInt = {
- var res = BigInt(1)
- var i = 0
- while(i < k) {
- res *= n - i
- i+=1
- }
- i = 2
- while(i <= k) {
- res /= i
- i+=1
- }
- res
- }
-
- /** Returns a stream of prioritary positions and another of remaining positions */
- def prioritizedPositions(s: String): (Stream[Int], Stream[Int])= {
- val separations = "\\b".r.findAllMatchIn(s).map(m => m.start).toStream
- val done = separations.toSet
- val remaining = for( i <- (0 to s.length).toStream if !done(i)) yield i
- (separations, remaining)
- }
-
-
- /** A single pass simplification process. Converts as much as equations to assignments if possible. */
- trait ProblemSimplicationPhase { self =>
- def apply(p: Problem, s: Assignment) = run(p, s)
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)]
- def andThen(other: ProblemSimplicationPhase): ProblemSimplicationPhase = new ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment) = {
- ProblemSimplicationPhase.this.run(p, s) match {
- case Some((p, s)) =>
- //println("Problem before " + other.getClass.getName.substring(33) + ":" + (renderProblem(p), s))
- other.run(p, s)
- case None =>
- None
- }
- }
- }
- /** Applies a phase until the output does not change anymore */
- def loopUntilConvergence = new ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- leon.utils.fixpoint[Option[(Problem, Assignment)]]{
- case None => None
- case Some((problem: Problem, assignment: Assignment)) => self.run(problem, assignment)
- }(Option((p, s)))
- }
- }
- }
- def loopUntilConvergence(psp: ProblemSimplicationPhase) = psp.loopUntilConvergence
-
- /** Removes duplicate equations from the problem */
- object DistinctEquation extends ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- Some((p.distinct, s))
- }
- }
-
- /** Merge constant in string forms */
- object MergeConstants extends ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- @tailrec def mergeConstants(p: Problem, acc: ListBuffer[Equation] = ListBuffer()): Option[Problem] = p match {
- case Nil => Some(acc.toList)
- case (sf, rhs)::q => mergeConstants(q, acc += ((reduceStringForm(sf), rhs)))
- }
- mergeConstants(p).map((_, s))
- }
- }
-
- /** Unsat if Const1 = Const2 but constants are different.
- * if Const1 = Const2 and constants are same, remove equality. */
- object SimplifyConstants extends ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- @tailrec def simplifyConstants(p: Problem, acc: ListBuffer[Equation] = ListBuffer()): Option[Problem] = p match {
- case Nil => Some(acc.toList)
- case (Nil, rhs)::q => if("" != rhs) None else simplifyConstants(q, acc)
- case (List(Left(c)), rhs)::q => if(c != rhs) None else simplifyConstants(q, acc)
- case sentence::q => simplifyConstants(q, acc += sentence)
- }
- simplifyConstants(p).map((_, s))
- }
- }
-
- /** . Get new assignments from equations such as id = Const, and propagate them */
- object PropagateAssignments extends ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- @tailrec def obtainAssignments(p: Problem, assignments: Assignment = Map()): Option[Assignment] = p match {
- case Nil => Some(assignments)
- case (List(Right(id)), rhs)::q =>
- assignments.get(id) match { // It was assigned already.
- case Some(v) =>
- if(rhs != v) None else obtainAssignments(q, assignments)
- case None =>
- obtainAssignments(q, assignments + (id -> rhs))
- }
- case sentence::q => obtainAssignments(q, assignments)
- }
- obtainAssignments(p, s).map(newAssignments => {
- //println("Obtained new assignments: " + newAssignments)
- val newProblem = if(newAssignments.nonEmpty) reduceProblem(newAssignments)(p) else p
- (newProblem, s ++ newAssignments)
- })
- }
- }
-
- /** Removes all constants from the left of the equations (i.e. "ab" x ... = "abcd" ==> x ... = "cd" ) */
- object RemoveLeftConstants extends ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- @tailrec def removeLeftconstants(p: Problem, acc: ListBuffer[Equation] = ListBuffer()): Option[Problem] = p match {
- case Nil => Some(acc.toList)
- case ((Left(constant)::q, rhs))::ps =>
- if(rhs.startsWith(constant)) {
- removeLeftconstants(ps, acc += ((q, rhs.substring(constant.length))))
- } else None
- case (t@(q, rhs))::ps =>
- removeLeftconstants(ps, acc += t)
- }
- removeLeftconstants(p).map((_, s))
- }
- }
-
- /** Removes all constants from the right of the equations (i.e. ... x "cd" = "abcd" ==> ... x = "ab" ) */
- object RemoveRightConstants extends ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- @tailrec def removeRightConstants(p: Problem, acc: ListBuffer[Equation] = ListBuffer()): Option[Problem] = p match {
- case Nil => Some(acc.toList)
- case (ConsReverse(q, Left(constant)), rhs)::ps =>
- if(rhs.endsWith(constant)) {
- removeRightConstants(ps, acc += ((q, rhs.substring(0, rhs.length - constant.length))))
- } else None
- case (t@(q, rhs))::ps =>
- removeRightConstants(ps, acc += t)
- }
- removeRightConstants(p).map((_, s))
- }
- }
-
- /** If constants can have only one position in an equation, splits the equation.
- * If an equation is empty, treats all left-hand-side identifiers as empty.
- * Requires MergeConstants so that empty constants have been removed. */
- object PropagateMiddleConstants extends ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- @tailrec def constantPropagate(p: Problem, assignments: Assignment = Map(), newProblem: ListBuffer[Equation] = ListBuffer()): Option[(Problem, Assignment)] = {
- p match {
- case Nil =>
- Some((newProblem.toList, assignments))
- case (ids, "")::q => // All identifiers should be empty.
- val constants = ids.find {
- case Left(s) if s != "" => true
- case Right(_) => false
- }
- (constants match {
- case Some(_) => None
- case None => // Ok now let's assign all variables to empty string.
- val newMap = ids.collect { case Right(id) => id -> "" }
- val newAssignments = (Option(assignments) /: newMap) {
- case (None, (id, rhs)) => None
- case (Some(a), (id, rhs)) =>
- a.get(id) match { // It was assigned already.
- case Some(v) =>
- if(rhs != v) None else Some(a)
- case None =>
- Some(a + (id -> rhs))
- }
- }
- newAssignments
- }) match {
- case None => None
- case Some(a) =>
- constantPropagate(q, a, newProblem)
- }
- case (sentence@(ids, rhs))::q => // If the constants have an unique position, we should split the equation.
- val constants = ids.collect {
- case l@Left(s) => s
- }
- // Check if constants form a partition in the string, i.e. getting the .indexOf() the first time is the only way to split the string.
-
- if(constants.nonEmpty) {
-
- var pos = -2
- var lastPos = -2
- var lastConst = ""
- var invalid = false
-
- for(c <- constants) {
- val i = rhs.indexOfSlice(c, pos)
- lastPos = i
- lastConst = c
- if(i == -1) invalid = true
- pos = i + c.length
- }
- if(invalid) None else {
- val i = rhs.indexOfSlice(lastConst, lastPos + 1)
- if(i == -1) { // OK it's the smallest position possible, hence we can split at the last position.
- val (before, _, after) = splitAtLastConstant(ids)
- val firstConst = rhs.substring(0, lastPos)
- val secondConst = rhs.substring(lastPos + lastConst.length)
- constantPropagate((before, firstConst)::(after, secondConst)::q, assignments, newProblem)
- } else {
- // Other splitting strategy: independent constants ?
-
- val constantsSplit = constants.flatMap{ c => {
- val i = rhs.indexOfSlice(c, -1)
- val j = rhs.indexOfSlice(c, i + 1)
- if(j == -1 && i != -1) {
- List((c, i))
- } else Nil
- }}
-
- constantsSplit match {
- case Nil =>
- constantPropagate(q, assignments, newProblem += sentence)
- case ((c, i)::_) =>
- val (before, after) = ids.splitAt(ids.indexOf(Left(c)))
- val firstconst = rhs.substring(0, i)
- val secondConst = rhs.substring(i+c.length)
- constantPropagate((before, firstconst)::(after.tail, secondConst)::q, assignments, newProblem)
- }
-
- }
- }
- } else {
- constantPropagate(q, assignments, newProblem += sentence)
- }
- case sentence::q => constantPropagate(q, assignments, newProblem += sentence)
- }
- }
- constantPropagate(p).map(ps => {
- val newP = if(ps._2.nonEmpty) reduceProblem(ps._2)(p) else p
- (newP, s ++ ps._2)
- })
- }
- }
-
- /** If a left-hand side of the equation appears somewhere else, replace it by the right-hand-side of this equation */
- object PropagateEquations extends ProblemSimplicationPhase {
- def run(p: Problem, s: Assignment): Option[(Problem, Assignment)] = {
- var newP = p.distinct
- for((lhs, rhs) <- newP if lhs.length >= 2) { // Original distinct p.
- var indexInP = 0
- for(eq@(lhs2, rhs2) <- newP) {
- if((!(lhs2 eq lhs) || !(rhs2 eq rhs))) {
- val i = lhs2.indexOfSlice(lhs)
- if(i != -1) {
- val res = (lhs2.take(i) ++ Seq(Left(rhs)) ++ lhs2.drop(i + lhs.size), rhs2)
- newP = newP.updated(indexInP, res)
- }
- }
- indexInP += 1
- }
- }
- Some((newP, s))
- }
- }
-
- /** returns a simplified version of the problem. If it is not satisfiable, returns None. */
- val simplifyProblem: ProblemSimplicationPhase = {
- loopUntilConvergence(MergeConstants andThen
- SimplifyConstants andThen
- PropagateAssignments)
- }
-
- /** Removes all constants from the left and right of the equations */
- val noLeftRightConstants: ProblemSimplicationPhase = {
- RemoveLeftConstants andThen RemoveRightConstants
- }
-
- /** Composition of simplifyProblem and noLeftRightConstants */
- val forwardStrategy =
- loopUntilConvergence(
- simplifyProblem andThen
- noLeftRightConstants andThen
- PropagateMiddleConstants andThen
- DistinctEquation andThen
- PropagateEquations
- )
-
-
- /** Solves the equation x1x2x3...xn = CONSTANT
- * Prioritizes split positions in the CONSTANT that are word boundaries
- * Prioritizes variables which have a higher frequency */
- def simpleSplit(ids: List[Identifier], rhs: String)(implicit statistics: Map[Identifier, Int]): Stream[Assignment] = {
- ids match {
- case Nil => if(rhs == "") Stream(Map()) else Stream.empty
- case List(x) =>
- Stream(Map(x -> rhs))
- case x :: ys =>
- val (bestVar, bestScore, worstScore) = ((None: Option[(Identifier, Int, Int)]) /: ids) {
- case (None, x) => val sx = statistics(x)
- Some((x, sx, sx))
- case (s@Some((x, i, ws)), y) => val yi = statistics(y)
- if (i >= yi) Some((x, i, Math.min(yi, ws))) else Some((y, yi, ws))
- }.get
- val (prioritaryPos, remainingPos) = prioritizedPositions(rhs)
- val numBestVars = ids.count { x => x == bestVar }
-
- if(worstScore == bestScore) {
- for{
- i <- (prioritaryPos append remainingPos) // Prioritization on positions which are separators.
- xvalue = rhs.substring(0, i)
- rvalue = rhs.substring(i)
- remaining_split <- simpleSplit(ys, rvalue)
- if !remaining_split.contains(x) || remaining_split(x) == xvalue
- } yield (remaining_split + (x -> xvalue))
- } else { // A variable appears more than others in the same equation, so its changes are going to propagate more.
- val indexBestVar = ids.indexOf(bestVar)
- val strings = if(indexBestVar == 0) { // Test only string prefixes or empty string
- ((for{j <- (rhs.length to 1 by -1).toStream
- if prioritaryPos contains j} yield rhs.substring(0, j)) append
- Stream("") append
- (for{j <- (rhs.length to 1 by -1).toStream
- if remainingPos contains j} yield rhs.substring(0, j)))
- } else {
- val lastIndexBestVar = ids.lastIndexOf(bestVar)
- if(lastIndexBestVar == ids.length - 1) {
- val pos = prioritaryPos append remainingPos
- (for{ i <- pos.toStream // Try to maximize the size of the string from the start
- if i != rhs.length
- } yield rhs.substring(i)) #:::
- Stream("")
- } else { // Inside, can be anything.
- def substrings(startPos: Stream[Int], endPos: Stream[Int]): Stream[String] = {
- for{ i <- startPos.toStream
- if i != rhs.length
- j <- rhs.length to (i+1) by -1
- if endPos contains j} yield rhs.substring(i, j)
- }
- (substrings(prioritaryPos, prioritaryPos) append
- Stream("") append
- substrings(prioritaryPos, remainingPos) append
- substrings(remainingPos, prioritaryPos) append
- substrings(remainingPos, remainingPos))
- }
- }
- for {str <- strings.distinct
- if java.util.regex.Pattern.quote(str).r.findAllMatchIn(rhs).length >= numBestVars
- } yield {
- Map(bestVar -> str)
- }
- }
- }
- }
-
- @tailrec def statsStringForm(e: StringForm, acc: Map[Identifier, Int] = Map()): Map[Identifier, Int] = e match {
- case Nil => acc
- case Right(id)::q => statsStringForm(q, acc + (id -> (acc.getOrElse(id, 0) + 1)))
- case (_::q) => statsStringForm(q, acc)
- }
-
- @tailrec def stats(p: Problem, acc: Map[Identifier, Int] = Map()): Map[Identifier, Int] = p match {
- case Nil => acc
- case (sf, rhs)::q =>
- stats(q, (statsStringForm(sf) /: acc) { case (m, (k, v)) => m + (k -> (m.getOrElse(k, 0) + v)) })
- }
-
- /** Deduces possible new assignments from the problem. */
- def splitStrategy(p: Problem): Stream[Assignment] = {
- // Look for the equation with the least degree of freedom.
- if(p.isEmpty) return Stream(Map())
-
- var minStatement = p.head
- var minweight = BigInt(-1)
- var minConstants = List[String]()
- var minIdentifiersGrouped = List[List[Identifier]]()
- // Counts the number of possible enumerations, take the least.
- for((lhs, rhs) <- p) {
- val constants = lhs.collect{ case Left(constant) => constant }
- val identifiers_grouped = ListBuffer[List[Identifier]]()
- val current_buffer = ListBuffer[Identifier]()
- for(e <- lhs) e match {
- case Left(constant) => // At this point, there is only one constant here.
- identifiers_grouped.append(current_buffer.toList)
- current_buffer.clear()
- case Right(identifier) =>
- current_buffer.append(identifier)
- }
- identifiers_grouped.append(current_buffer.toList)
- var weight = BigInt(9)
- for(positions <- repartitions(constants, rhs)) {
- var tmp_weight = BigInt(1)
- var prev_position = 0
- for(((p, c), ids) <- positions.zip(constants).zip(identifiers_grouped.init)) {
- tmp_weight *= cnk(p - prev_position, ids.length - 1) // number of positions
- prev_position = p + c.length
- }
- tmp_weight *= cnk(rhs.length - prev_position, identifiers_grouped.last.length - 1)
- weight += tmp_weight
- }
- if(minweight == -1 || weight < minweight) {
- minweight = weight
- minStatement = (lhs, rhs)
- minConstants = constants
- minIdentifiersGrouped = identifiers_grouped.toList
- }
- }
- val (_, rhs) = minStatement
- val constants = minConstants
- val identifiers_grouped = minIdentifiersGrouped
- val statistics = stats(p)
- if(identifiers_grouped.length > 1) {
- // There might be different repartitions of the first boundary constant. We need to investigate all of them.
- repartitions(constants, rhs).map(_.head).distinct.toStream.flatMap(p => {
- val firstString = rhs.substring(0, p) // We only split on the first string.
- simpleSplit(identifiers_grouped.head, firstString)(statistics)
- })
- } else if(identifiers_grouped.length == 1) {
- simpleSplit(identifiers_grouped.head, rhs)(statistics) // All new assignments
- } else {
- if(rhs == "") Stream(Map()) else Stream.Empty
- }
- }
-
- /** Solves the problem and returns all possible satisfying assignment */
- def solve(p: Problem): Stream[Assignment] = {
- val realProblem = forwardStrategy.run(p, Map())
- /*println("Problem:\n"+renderProblem(p))
- if(realProblem.nonEmpty && realProblem.get._1.nonEmpty) {
- println("Solutions:\n"+realProblem.get._2)
- println("Real problem:\n"+renderProblem(realProblem.get._1))
- }*/
-
- realProblem match {
- case None =>
- Stream.Empty
- case Some((Nil, solution)) =>
- Stream(solution)
- case Some((problem, partialSolution)) =>
- // 1) No double constants ("a" + "b" have been replaced by "ab")
- // 2) No just an identifier on the LHS (x = "a" has been replaced by an assignment
- // 3) No leading or trailing constants in equation ("a" + ... + "b" = "axyzb" has been replaced by ... = "xyz")
-
- /* Equation of the type
- variables "constant" variables "constant".... variables = "constant".
- For each constant we check its possible positions in the output, which determines possible assignments.
-
- Then since variables = constant, we can just iterate on them.
- Heuristic: We need to resolve smaller equations first.
- */
- for{assignment <- splitStrategy(problem)
- newProblem = reduceProblem(assignment)(problem)
- remainingSolution <- solve(newProblem)
- } yield {
- partialSolution ++ assignment ++ remainingSolution
- }
- }
- }
-
- ////////////////////////////////////////////////
- //// Transitively Bounded problem extension ////
- ////////////////////////////////////////////////
-
- /** More general types of equations */
- type GeneralEquation = (StringForm, StringForm)
-
- /** Supposes that all variables are transitively bounded by length*/
- type GeneralProblem = List[GeneralEquation]
-
- def variablesStringForm(sf: StringForm): Set[Identifier] = sf.collect { case Right(id) => id }.toSet
- def variables(gf: GeneralEquation): Set[Identifier] = variablesStringForm(gf._1) ++ variablesStringForm(gf._2)
-
- /** Returns true if the problem is transitively bounded */
- def isTransitivelyBounded(b: GeneralProblem, transitivelyBounded: Set[Identifier] = Set()): Boolean = {
- def isBounded(sf: GeneralEquation) = {
- variablesStringForm(sf._1).forall(transitivelyBounded) || variablesStringForm(sf._2).forall(transitivelyBounded)
- }
- val (bounded, notbounded) = b.partition(isBounded)
-
- if(notbounded == Nil) true
- else if(notbounded == b) false
- else {
- isTransitivelyBounded(notbounded, transitivelyBounded ++ bounded.flatMap { x => variables(x) })
- }
- }
-
- /** Propagates an assignment into a general equation */
- def reduceGeneralEquation(a: Assignment)(g: GeneralEquation): GeneralEquation = g match {
- case (sf1, sf2) => (reduceStringForm(a)(sf1), reduceStringForm(a)(sf2))
- }
-
- /** Solves the bounded problem version.
- * Requires all the variables to be transitively bounded by size. */
- def solveGeneralProblem(b: GeneralProblem): Stream[Assignment] = {
- val realProblem = b map { case (lhs, rhs) => (reduceStringForm(lhs), reduceStringForm(rhs)) }
-
- def partition(b: GeneralProblem, bounded: ListBuffer[Equation] = ListBuffer(), unbounded: ListBuffer[GeneralEquation] = ListBuffer()): (Problem, GeneralProblem) = b match {
- case Nil => (bounded.toList, unbounded.toList)
- case (sf1, List(Left(a)))::q => partition(q, bounded += ((sf1, a)), unbounded)
- case (sf1, Nil)::q => partition(q, bounded += ((sf1, "")), unbounded)
- case (List(Left(a)), sf1)::q => partition(q, bounded += ((sf1, a)), unbounded)
- case (Nil, sf1)::q => partition(q, bounded += ((sf1, "")), unbounded)
- case a::q => partition(q, bounded, unbounded += a)
- }
-
- val (bounded, unbounded) = partition(realProblem)
-
- if(unbounded == Nil) solve(bounded) else
- solve(bounded).flatMap(assignment => {
- solveGeneralProblem(unbounded.map(reduceGeneralEquation(assignment)(_))).map(assignment ++ _)
- })
- }
-
-
- ////////////////////////////////////////////////
- //// Incremental problem extension ////
- ////////////////////////////////////////////////
-
- /** Returns all subsets of i elements of a sequence. */
- def take[A](i: Int, of: Seq[A]): Stream[Seq[A]] = {
- if(i > of.size || i < 0) Stream.empty
- else if(i == of.size) Stream(of)
- else if(i == 0) Stream(Seq.empty)
- else {
- take(i - 1, of.tail).map(of.head +: _) #::: take(i, of.tail)
- }
- }
-
- /** Keeps only partial assignments which completely differ from the initial mapping. */
- def removeRedundancies(s: Stream[Assignment], initialMapping: Assignment): Stream[Assignment] = {
- s.filter(m =>
- m.keys forall (key => initialMapping(key) != m(key)))
- }
-
- /** If the stream is not empty and there are more than two variables,
- * it will try to assign values to variables which minimize changes.
- * It will try deletions from the end and from the start of one variable.
- * */
- def minimizeChanges(s: Stream[Assignment], p: Problem, ifVariable: Set[Identifier], initialMapping: Assignment): Stream[Assignment] = {
- if(s.isEmpty || ifVariable.size <= 1) s else {
- ((for{v <- ifVariable.toStream
- originalValue = initialMapping(v)
- i <- originalValue.length to 0 by -1
- prefix <- (if(i == 0 || i == originalValue.length) List(true) else List(true, false))
- possibleValue = (if(prefix) originalValue.substring(0, i) else originalValue.substring(originalValue.length - i))
- s <- solve(reduceProblem(Map(v -> possibleValue))(p))
- } yield s + (v -> possibleValue)) ++ s).distinct
- }
- }
-
- /** Solves the problem while supposing that a minimal number of variables have been changed.
- * Will try to replace variables from the left first.
- * If a variable occurs multiple times, will try to replace each of its occurrence first.
- * */
- def solveMinChange(p: Problem, initialMapping: Assignment): Stream[Assignment] = {
- // First try to see if the problem is solved. If yes, returns the initial mapping
- val initKeys = initialMapping.keys.toSeq
- for{
- i <- (0 to initialMapping.size).toStream
- toReplace <- take(i, initKeys)
- ifVariable = toReplace.toSet
- newProblem = reduceProblem(initialMapping filterKeys (x => !ifVariable(x)))(p)
- newSolutions = solve(newProblem)
- newSolutions_nonredundant = removeRedundancies(newSolutions, initialMapping)
- solution <- minimizeChanges(newSolutions_nonredundant, newProblem, ifVariable, initialMapping: Assignment)
- } yield solution
- }
-}
diff --git a/src/main/scala/inox/solvers/sygus/CVC4SygusSolver.scala b/src/main/scala/inox/solvers/sygus/CVC4SygusSolver.scala
deleted file mode 100644
index 564dc67fe75fe016bcbba38a62dfbb6ba0544efc..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/sygus/CVC4SygusSolver.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package sygus
-
-import purescala._
-import Definitions.Program
-
-import synthesis.Problem
-
-import leon.solvers.smtlib._
-
-import _root_.smtlib.interpreters.CVC4Interpreter
-
-class CVC4SygusSolver(ctx: LeonContext, pgm: Program, p: Problem) extends SygusSolver(ctx, pgm, p) with SMTLIBCVC4QuantifiedTarget {
- override def targetName = "cvc4-sygus";
-
- def interpreterOps(ctx: LeonContext) = {
- Seq(
- "-q",
- "--cegqi-si",
- "--cbqi-sym-lia",
- "--macros-quant",
- "--lang", "sygus",
- "--print-success"
- )
- }
-
- protected val allowQuantifiedAssertions: Boolean = true
-}
diff --git a/src/main/scala/inox/solvers/sygus/SygusSolver.scala b/src/main/scala/inox/solvers/sygus/SygusSolver.scala
deleted file mode 100644
index 9cfefb228f95ac9adaa39023aa1671fb98fa4509..0000000000000000000000000000000000000000
--- a/src/main/scala/inox/solvers/sygus/SygusSolver.scala
+++ /dev/null
@@ -1,140 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-package sygus
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.ExprOps._
-import purescala.Constructors._
-import purescala.Expressions._
-
-import synthesis.Problem
-
-import leon.solvers.smtlib._
-
-import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
-import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
-import _root_.smtlib.parser.CommandsResponses.{Error => _, _}
-import _root_.smtlib.parser.Parser.UnexpectedEOFException
-
-abstract class SygusSolver(val context: LeonContext, val program: Program, val p: Problem) extends SMTLIBTarget {
- implicit val ctx = context
- implicit val debugSection = leon.utils.DebugSectionSynthesis
-
- protected def unsupported(t: Tree, str: String): Nothing = {
- throw new Unsupported(t, str)
- }
-
- def checkSynth(): Option[Expr] = {
-
- emit(SList(SSymbol("set-logic"), SSymbol("ALL_SUPPORTED")))
-
- val constraintId = QualifiedIdentifier(SMTIdentifier(SSymbol("constraint")))
-
- val bindings = p.as.map(a => a -> (symbolToQualifiedId(id2sym(a)): Term)).toMap
-
- // declare inputs
- for (a <- p.as) {
- emit(SList(SSymbol("declare-var"), id2sym(a), toSMT(a.getType)))
- variables += a -> id2sym(a)
- }
-
- // declare outputs
- val xToFd = for (x <- p.xs) yield {
- val fd = new FunDef(x.freshen, Seq(), p.as.map(a => ValDef(a)), x.getType)
-
- val fsym = id2sym(fd.id)
-
- functions += fd.typed -> fsym
-
- // declare function to synthesize
- emit(SList(SSymbol("synth-fun"), id2sym(fd.id), SList(fd.params.map(vd => SList(id2sym(vd.id), toSMT(vd.getType))) :_*), toSMT(fd.returnType)))
-
- x -> fd
- }
-
- val xToFdCall = xToFd.toMap.mapValues(fd => FunctionInvocation(fd.typed, p.as.map(_.toVariable)))
-
- val synthPhi = replaceFromIDs(xToFdCall, p.phi)
-
- val constraint = p.pc implies synthPhi
-
- emit(FunctionApplication(constraintId, Seq(toSMT(constraint)(bindings))))
-
- emit(SList(SSymbol("check-synth"))) // check-synth emits: success; unsat; fdef*
-
- // We currently cannot predict the amount of success we will get, so we read as many as possible
- try {
- var lastRes = interpreter.parser.parseSExpr
- while(lastRes == SSymbol("success")) {
- lastRes = interpreter.parser.parseSExpr
- }
-
- lastRes match {
- case SSymbol("unsat") =>
-
- val solutions = (for (x <- p.xs) yield {
- interpreter.parser.parseCommand match {
- case DefineFun(SMTFunDef(name, params, retSort, body)) =>
- val res = fromSMT(body, sorts.toA(retSort))(Map(), Map())
- Some(res)
- case r =>
- context.reporter.warning("Unnexpected result from cvc4-sygus: "+r)
- None
- }
- }).flatten
-
- if (solutions.size == p.xs.size) {
- Some(tupleWrap(solutions))
- } else {
- None
- }
-
- case SSymbol("unknown") =>
- None
-
- case r =>
- context.reporter.warning("Unnexpected result from cvc4-sygus: "+r+" expected unsat")
- None
- }
- } catch {
- case _: UnexpectedEOFException =>
- None
- }
- }
-}
-
- //val g = BaseGrammar || OneOf(p.as.map(_.toVariable))
-
- //type Label = TypeTree
-
- //var defined = Map[Label, Identifier]()
- //var definitions = new ArrayBuffer[(Identifier, Seq[Expr])]()
-
- //def getLabel(l: Label): Identifier = defined.getOrElse(l, {
- // val id = FreshIdentifier(l.getType.toString, l.getType)
- // defined += l -> id
-
- // val defs = g.getProductions(l).map { g =>
- // g.builder(g.subTrees.map(getLabel(_).toVariable))
- // }
-
- // definitions += (id -> defs)
-
- // id
- //})
-
- //// discover grammar
- //getLabel(out.getType)
-
- //val grammarBindings: Map[Identifier, Term] = defined.map{ case (_, id) =>
- // id -> QualifiedIdentifier(SMTIdentifier(idToSymbol(id)))
- //}
-
- //// define grammar
- //val grammar = SList((for ((id, ds) <- definitions) yield {
- // SList(idToSymbol(id), typeToSort(id.getType), SList(ds.map(d => smt.toSMT(d)(bindings++grammarBindings)): _*))
- //}).toList)
-