From 2f5199f4ec5528b458e38a428cbc15dfb039cf60 Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Tue, 27 Nov 2012 19:08:17 +0100 Subject: [PATCH] Remove unused cleanups when restarting, fix reporter to solver --- .../leon/solvers/z3/AbstractZ3Solver.scala | 26 +++---------------- .../scala/leon/solvers/z3/FairZ3Solver.scala | 4 --- .../solvers/z3/UninterpretedZ3Solver.scala | 14 +++++----- .../scala/leon/synthesis/ParallelSearch.scala | 2 +- 4 files changed, 11 insertions(+), 35 deletions(-) diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala index aae1dcc84..993496484 100644 --- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala @@ -122,36 +122,16 @@ trait AbstractZ3Solver { neverInitialized = false z3 = new Z3Context(z3cfg) solver = z3.mkSolver + prepareSorts + prepareFunctions } else { solver = z3.mkSolver } exprToZ3Id = Map.empty z3IdToExpr = Map.empty - - fallbackSorts = Map.empty - - mapSorts = Map.empty - arraySorts = Map.empty - funSorts = Map.empty - funDomainConstructors = Map.empty - funDomainSelectors = Map.empty - - tupleSorts = Map.empty - tupleConstructors = Map.empty - tupleSelectors = Map.empty - - mapRangeSorts.clear - mapRangeSomeConstructors.clear - mapRangeNoneConstructors.clear - mapRangeSomeTesters.clear - mapRangeNoneTesters.clear - mapRangeValueSelectors.clear - - prepareSorts - - prepareFunctions } + protected[leon] def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match { case Some(z3sort) => z3sort case None => { diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala index 4001d5345..93c0e8e73 100644 --- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala @@ -306,7 +306,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ // reporter.warning("Z3 doesn't know because: " + z3.getSearchFailure.message) reporter.warning("Z3 doesn't know because ??") foundAnswer(None) - m.delete } case (Some(true), m) => { // SAT validatingStopwatch.start @@ -336,8 +335,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ // This branch is both for with and without unsat cores. The // distinction is made inside. case (Some(false), m) => { - //m.delete - if(!Settings.useCores) solver.pop(1) @@ -540,7 +537,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ }).toMap val asMap = modelToMap(model, variables) ++ functionsAsMap ++ constantFunctionsAsMap - model.delete lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n") val evalResult = eval(asMap, formula, evaluator) diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala index 08b27c9ed..9215e6c40 100644 --- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala @@ -61,17 +61,17 @@ class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with val unsatResult = (Some(false), emptyModel) val result = toZ3Formula(expression).map { asZ3 => - z3.assertCnstr(asZ3) - z3.checkAndGetModel() match { - case (Some(false), _) => unsatResult - case (Some(true), model) => { + solver.assertCnstr(asZ3) + solver.check match { + case Some(false) => unsatResult + case Some(true) => { + val model = solver.getModel + if(containsFunctionCalls(expression)) { unknownResult } else { val variables = variablesOf(expression) - val r = (Some(true), modelToMap(model, variables)) - model.delete - r + (Some(true), modelToMap(model, variables)) } } case _ => unknownResult diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala index 184714e7b..9d24d1d27 100644 --- a/src/main/scala/leon/synthesis/ParallelSearch.scala +++ b/src/main/scala/leon/synthesis/ParallelSearch.scala @@ -14,7 +14,7 @@ class ParallelSearch(synth: Synthesizer, def initWorkerContext(wr: ActorRef) = { val reporter = new SilentReporter - val solver = new FairZ3Solver(synth.context) + val solver = new FairZ3Solver(synth.context.copy(reporter = reporter)) solver.setProgram(synth.program) SynthesisContext(solver = solver, reporter = synth.reporter) -- GitLab