From f448b5d8fed7934c3491e094340a9c5e076f7055 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 25 Aug 2015 11:35:11 +0200
Subject: [PATCH] Reverted evaluation of quantifiers
---
.../scala/leon/codegen/CodeGeneration.scala | 1 -
.../codegen/runtime/ChooseEntryPoint.scala | 6 +-
.../codegen/runtime/SolverEntryPoint.scala | 149 ------------------
.../leon/evaluators/RecursiveEvaluator.scala | 7 +
4 files changed, 10 insertions(+), 153 deletions(-)
delete mode 100644 src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 1e37626f0..985c5970e 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -843,7 +843,6 @@ trait CodeGeneration {
val id = runtime.ChooseEntryPoint.register(prob, this)
ch << Ldc(id)
-
ch << Ldc(prob.as.size)
ch << NewArray(ObjectClass)
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 8eb9d1565..4328a7e92 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -76,8 +76,8 @@ object ChooseEntryPoint {
} else {
val tStart = System.currentTimeMillis
- val solverf = SolverFactory.default(ctx, program)
- val solver = solverf.getNewSolver().setTimeout(10.seconds)
+ val solverf = SolverFactory.default(ctx, program).withTimeout(10.second)
+ val solver = solverf.getNewSolver()
val inputsMap = (p.as zip inputs).map {
case (id, v) =>
@@ -110,7 +110,7 @@ object ChooseEntryPoint {
throw new LeonCodeGenRuntimeException("Timeout exceeded")
}
} finally {
- solverf.reclaim(solver)
+ solver.free()
solverf.shutdown()
}
}
diff --git a/src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala b/src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala
deleted file mode 100644
index e36f8aef0..000000000
--- a/src/main/scala/leon/codegen/runtime/SolverEntryPoint.scala
+++ /dev/null
@@ -1,149 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package codegen.runtime
-
-import utils._
-import purescala.Common._
-import purescala.Expressions._
-import purescala.ExprOps.valuateWithModel
-import purescala.Constructors._
-import solvers.SolverFactory
-
-import java.util.WeakHashMap
-import java.lang.ref.WeakReference
-import scala.collection.mutable.{HashMap => MutableMap}
-import scala.concurrent.duration._
-
-import codegen.CompilationUnit
-
-import synthesis._
-
-object SolverEntryPoint {
- implicit val debugSection = DebugSectionSolver
-
- private case class ExprId(id: Int)
- private case class SolverProblem(args: Seq[Identifier], problem: Expr)
-
- private[this] val context = new WeakHashMap[ExprId, (WeakReference[CompilationUnit], SolverProblem)]()
- private[this] val cache = new WeakHashMap[ExprId, MutableMap[Seq[AnyRef], Option[java.lang.Object]]]()
-
- private[this] val ids = new WeakHashMap[CompilationUnit, MutableMap[SolverProblem, ExprId]]()
-
- private[this] var _next = 0
- private[this] def nextInt(): Int = {
- _next += 1
- _next
- }
-
- private def getUniqueId(unit: CompilationUnit, p: SolverProblem): ExprId = {
- if (!ids.containsKey(unit)) {
- ids.put(unit, new MutableMap())
- }
-
- if (ids.get(unit) contains p) {
- ids.get(unit)(p)
- } else {
- val cid = new ExprId(nextInt())
- ids.get(unit) += p -> cid
- cid
- }
- }
-
- def register(args: Seq[Identifier], expr: Expr, unit: CompilationUnit): Int = {
- val p = SolverProblem(args, expr)
- val cid = getUniqueId(unit, p)
-
- context.put(cid, new WeakReference(unit) -> p)
-
- cid.id
- }
-
- def check(i: Int, inputs: Array[AnyRef]): Boolean = {
- val id = ExprId(i)
- val (ur, p) = context.get(id)
- val unit = ur.get
-
- val program = unit.program
- val ctx = unit.ctx
-
- ctx.reporter.debug("Executing SAT problem (codegen)!")
- val is = inputs.toSeq
-
- if (!cache.containsKey(id)) {
- cache.put(id, new MutableMap())
- }
-
- val resultCache = cache.get(id)
-
- if (resultCache contains is) {
- resultCache(is).isDefined
- } else {
- val tStart = System.currentTimeMillis
-
- val solverf = SolverFactory.default(ctx, program).withTimeout(10.second)
- val solver = solverf.getNewSolver()
-
- val bindingCnstrs = (p.args zip inputs).flatMap { case (id, jvmExpr) =>
- val v = Variable(id)
- val expr = unit.jvmToExpr(jvmExpr, id.getType)
-
- val inputCnstr = expr match {
- case purescala.Extractors.FiniteLambda(default, mapping) =>
- Some(ElementOfSet(v, FiniteSet(mapping.map(_._1).toSet, id.getType)))
- case _ => None
- }
-
- Seq(Equals(v, expr)) ++ inputCnstr
- }
-
- solver.assertCnstr(andJoin(p.problem +: bindingCnstrs))
-
- try {
- solver.check match {
- case Some(true) =>
- val model = solver.getModel
- val valModel = valuateWithModel(model) _
- val res = p.args.map(valModel)
- val leonRes = tupleWrap(res)
-
- val total = System.currentTimeMillis-tStart
-
- ctx.reporter.debug("Constraint \"execution\" took "+total+"ms")
- ctx.reporter.debug("SAT with model "+leonRes.asString(ctx))
-
- val obj = unit.exprToJVM(leonRes)(new LeonCodeGenRuntimeMonitor(unit.params.maxFunctionInvocations))
- resultCache += is -> Some(obj)
- true
-
- case Some(false) =>
- resultCache += is -> None
- false
-
- case _ =>
- throw new LeonCodeGenRuntimeException("Timeout exceeded")
- }
- } finally {
- solver.free()
- solverf.shutdown()
- }
- }
- }
-
- def getModel(i: Int, inputs: Array[AnyRef]): java.lang.Object = {
- val id = ExprId(i)
- if (!cache.containsKey(id)) {
- throw new LeonCodeGenRuntimeException("Problem was not checked before model query")
- }
-
- cache.get(id).get(inputs.toSeq) match {
- case Some(Some(obj)) =>
- obj
- case Some(None) =>
- throw new LeonCodeGenRuntimeException("Problem was UNSAT")
- case None =>
- throw new LeonCodeGenRuntimeException("Problem was not checked before model query")
- }
- }
-}
-
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 38710837f..f67f03e19 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -551,7 +551,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case p : Passes =>
e(p.asConstraint)
+<<<<<<< HEAD
case choose: Choose =>
+=======
+ case choose @ Choose(_, Some(impl)) =>
+ e(impl)
+
+ case choose @ Choose(_, None) =>
+>>>>>>> Reverted evaluation of quantifiers
implicit val debugSection = utils.DebugSectionSynthesis
--
GitLab