From 7e2c837135aedf7ea85b5bfa3db3508e100a5800 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Tue, 3 Feb 2015 00:30:48 +0100
Subject: [PATCH] Stuff for web
---
src/main/scala/leon/synthesis/Solution.scala | 5 +++++
src/main/scala/leon/synthesis/Synthesizer.scala | 4 ++--
2 files changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 19f44bb33..f4d839536 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -84,6 +84,11 @@ object Solution {
new Solution(BooleanLiteral(true), Set(), simplestValue(t))
}
+ def failed(implicit p: Problem): Solution = {
+ val tpe = tupleTypeWrap(p.xs.map(_.getType))
+ Solution(BooleanLiteral(false), Set(), Error(tpe, "Rule failed!"))
+ }
+
def UNSAT(implicit p: Problem): Solution = {
val tpe = tupleTypeWrap(p.xs.map(_.getType))
Solution(BooleanLiteral(false), Set(), Error(tpe, p.phi+" is UNSAT!"))
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 6ba4adebf..46ecb4e33 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -27,6 +27,8 @@ class Synthesizer(val context : LeonContext,
val reporter = context.reporter
+ lazy val sctx = SynthesisContext.fromSynthesizer(this)
+
def getSearch(): Search = {
if (settings.manualSearch.isDefined) {
new ManualSearch(context, ci, problem, settings.costModel, settings.manualSearch)
@@ -41,8 +43,6 @@ class Synthesizer(val context : LeonContext,
def synthesize(): (Search, Stream[Solution]) = {
val s = getSearch();
- val sctx = SynthesisContext.fromSynthesizer(this)
-
val t = context.timers.synthesis.search.start()
val sols = s.search(sctx)
--
GitLab