From 202ff9676e0a72924d8eb2480616ca8e4f98b0b7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 15 Nov 2012 19:04:00 +0100
Subject: [PATCH] Implement solveSATWithCores
---
src/main/scala/leon/solvers/Solver.scala | 9 +++++++++
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 5 +++++
2 files changed, 14 insertions(+)
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index f42d6ed34..d6c15b269 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -33,6 +33,15 @@ abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
}
}
+ def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
+ solveSAT(And(expression +: assumptions.toSeq)) match {
+ case (Some(false), _) =>
+ (Some(false), Map(), assumptions)
+ case (r, m) =>
+ (r, m, Set())
+ }
+ }
+
def superseeds : Seq[String] = Nil
private var _forceStop = false
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index e35dc8815..95d89c73d 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -161,6 +161,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
+ override def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
+ restartZ3
+ decideWithModel(expression, false, None, Some(assumptions))
+ }
+
private[this] def decideWithModel(vc: Expr, forValidity: Boolean, evaluator: Option[(Map[Identifier,Expr]) => Boolean] = None, assumptions: Option[Set[Expr]] = None): (Option[Boolean], Map[Identifier,Expr], Set[Expr]) = {
val initializationStopwatch = new Stopwatch("init", false)
val blocking2Z3Stopwatch = new Stopwatch("blocking-set-to-z3", false)
--
GitLab