From 609c8fad23bd052785d5194f6eab0876f3d2417e Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 22 Oct 2012 16:04:06 +0200
Subject: [PATCH] Extending the interface of Solver to support counter-example
generation.
---
src/main/scala/leon/Extensions.scala | 3 +++
src/main/scala/leon/FairZ3Solver.scala | 5 +++++
src/main/scala/leon/TrivialSolver.scala | 1 -
3 files changed, 8 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index e9fdde89c..53bd6f37e 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -1,5 +1,6 @@
package leon
+import purescala.Common._
import purescala.Trees._
import purescala.Definitions._
@@ -20,6 +21,8 @@ object Extensions {
// 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 isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
def superseeds : Seq[String] = Nil
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 2c429bab3..b54f5db1d 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -478,6 +478,11 @@ 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]) = {
+ restartZ3
+ decideWithModel(vc, true)
+ }
+
def solveWithBounds(vc: Expr, fv: Boolean) : (Option[Boolean], Map[Identifier,Expr]) = {
restartZ3
boundValues
diff --git a/src/main/scala/leon/TrivialSolver.scala b/src/main/scala/leon/TrivialSolver.scala
index 7e08c4832..0b05bbb59 100644
--- a/src/main/scala/leon/TrivialSolver.scala
+++ b/src/main/scala/leon/TrivialSolver.scala
@@ -18,5 +18,4 @@ class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
case And(exs) if exs.contains(BooleanLiteral(false)) => Some(false)
case _ => None
}
-
}
--
GitLab