From d2b25e384f76bcb05c37bb7f9cf871c7e9f70e08 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 14 Jan 2013 20:05:54 +0100
Subject: [PATCH] Fix timeouts for sub solvers
---
.../scala/leon/solvers/z3/FairZ3Solver.scala | 10 +++++++++-
.../scala/leon/synthesis/rules/Cegis.scala | 18 ++++++++----------
2 files changed, 17 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index bce3e3bb1..448f42c25 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -391,8 +391,15 @@ class FairZ3Solver(context : LeonContext)
frameExpressions = Nil :: frameExpressions
}
+ override def init() {
+ FairZ3Solver.super.init
+ }
+
def halt() {
- z3.interrupt
+ FairZ3Solver.super.halt
+ if(z3 ne null) {
+ z3.interrupt
+ }
}
def pop(lvl: Int = 1) {
@@ -590,6 +597,7 @@ class FairZ3Solver(context : LeonContext)
}
case None =>
+ foundAnswer(None)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 1bdf8d1cf..296d4ef40 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -557,8 +557,12 @@ case object CEGIS extends Rule("CEGIS") {
// the assumptions are.
solver1.getUnsatCore
- case _ =>
+ case Some(true) =>
+ // Can't be!
bssAssumptions
+
+ case None =>
+ return RuleApplicationImpossible
}
solver1.pop()
@@ -602,10 +606,7 @@ case object CEGIS extends Rule("CEGIS") {
result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr)))
case _ =>
- if (!sctx.shouldStop.get) {
- sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
- }
- needMoreUnrolling = true
+ return RuleApplicationImpossible
}
}
@@ -617,7 +618,7 @@ case object CEGIS extends Rule("CEGIS") {
solver1.check match {
case Some(false) =>
// Unsat even without blockers (under which fcalls are then uninterpreted)
- result = Some(RuleApplicationImpossible)
+ return RuleApplicationImpossible
case _ =>
}
@@ -626,11 +627,8 @@ case object CEGIS extends Rule("CEGIS") {
needMoreUnrolling = true
case _ =>
- if (!sctx.shouldStop.get) {
- sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
- }
//println("%%%% WOOPS")
- needMoreUnrolling = true
+ return RuleApplicationImpossible
}
}
--
GitLab