Skip to content
Snippets Groups Projects
Commit 7e2c8371 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Stuff for web

parent d450b289
No related branches found
No related tags found
No related merge requests found
......@@ -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!"))
......
......@@ -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)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment