From c467321952d248f362344e9f53075d3e95774a35 Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Thu, 15 Nov 2012 19:15:28 +0100 Subject: [PATCH] Simplify Solver API --- src/main/scala/leon/solvers/Solver.scala | 12 +++++------- src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 4 ++-- .../leon/solvers/z3/UninterpretedZ3Solver.scala | 12 ++++++------ 3 files changed, 13 insertions(+), 15 deletions(-) diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala index d6c15b269..947f4ce28 100644 --- a/src/main/scala/leon/solvers/Solver.scala +++ b/src/main/scala/leon/solvers/Solver.scala @@ -20,15 +20,13 @@ abstract class Solver(val reporter: Reporter) extends Extension(reporter) { // should halt as soon as possible with any result (Unknown is ok) as soon as forceStop is true def solve(expression: Expr) : Option[Boolean] - def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = (solve(expression), Map.empty) - def solveSAT(expression: Expr): (Option[Boolean], Map[Identifier, Expr]) = { - solveOrGetCounterexample(Not(expression)) match { - case (Some(true), _) => + solve(Not(expression)) match { + case Some(true) => (Some(false), Map()) - case (Some(false), model) => - (Some(true), model) - case (None, _) => + case Some(false) => + (Some(true), Map()) + case None => (None, Map()) } } diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala index 95d89c73d..c2b236bce 100644 --- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala @@ -141,9 +141,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S def solve(vc: Expr) = decide(vc, true) - override def solveOrGetCounterexample(vc : Expr) : (Option[Boolean],Map[Identifier,Expr]) = { + override def solveSAT(vc : Expr) : (Option[Boolean],Map[Identifier,Expr]) = { restartZ3 - val (res, model, core) = decideWithModel(vc, true) + val (res, model, core) = decideWithModel(vc, false) (res, model) } diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala index 0100286d6..2e2a7cf6f 100644 --- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala @@ -51,26 +51,26 @@ class UninterpretedZ3Solver(reporter : Reporter) extends Solver(reporter) with A protected[leon] def functionDeclToDef(decl: Z3FuncDecl) : FunDef = reverseFunctionMap(decl) protected[leon] def isKnownDecl(decl: Z3FuncDecl) : Boolean = reverseFunctionMap.isDefinedAt(decl) - override def solve(expression: Expr) : Option[Boolean] = solveOrGetCounterexample(expression)._1 + override def solve(expression: Expr) : Option[Boolean] = solveSAT(Not(expression))._1.map(!_) // Where the solving occurs - override def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = { + override def solveSAT(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = { restartZ3 val emptyModel = Map.empty[Identifier,Expr] val unknownResult = (None, emptyModel) - val validResult = (Some(true), emptyModel) + val unsatResult = (Some(false), emptyModel) val result = toZ3Formula(expression).map { asZ3 => - z3.assertCnstr(z3.mkNot(asZ3)) + z3.assertCnstr(asZ3) z3.checkAndGetModel() match { - case (Some(false), _) => validResult + case (Some(false), _) => unsatResult case (Some(true), model) => { if(containsFunctionCalls(expression)) { unknownResult } else { val variables = variablesOf(expression) - val r = (Some(false), modelToMap(model, variables)) + val r = (Some(true), modelToMap(model, variables)) model.delete r } -- GitLab