From e5649f3dfd6502c33a13a6a62517e7f58651f2b3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 2 Nov 2012 19:34:46 +0100
Subject: [PATCH] Reporter should be silent, as it fails on under-constrained
expressions using selectors, lift solveSat to the level of Solvers
---
src/main/scala/leon/solvers/Solver.scala | 11 +++++++++++
src/main/scala/leon/synthesis/Heuristics.scala | 4 ++--
src/main/scala/leon/synthesis/Rules.scala | 2 +-
src/main/scala/leon/synthesis/SynthesisPhase.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 14 +-------------
5 files changed, 16 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index d99801323..69551967c 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -22,6 +22,17 @@ abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
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), _) =>
+ (Some(false), Map())
+ case (Some(false), model) =>
+ (Some(true), model)
+ case (None, _) =>
+ (None, Map())
+ }
+ }
+
def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
def superseeds : Seq[String] = Nil
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 0e39e3f9c..7ad623ec0 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -33,13 +33,13 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
while (result.isEmpty && i < maxTries) {
val phi = And(p.phi +: predicates)
- synth.solveSAT(phi) match {
+ synth.solver.solveSAT(phi) match {
case (Some(true), satModel) =>
val satXsModel = satModel.filterKeys(xss)
val newPhi = valuateWithModelIn(phi, xss, satModel)
- synth.solveSAT(Not(newPhi)) match {
+ synth.solver.solveSAT(Not(newPhi)) match {
case (Some(true), invalidModel) =>
// Found as such as the xs break, refine predicates
predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 213793663..c6371a00e 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -88,7 +88,7 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 50, 0) {
val tpe = TupleType(p.xs.map(_.getType))
- synth.solveSAT(p.phi) match {
+ synth.solver.solveSAT(p.phi) match {
case (Some(true), model) =>
RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
case (Some(false), model) =>
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index f51749d82..2f8dc774e 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -22,7 +22,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
)
def run(ctx: LeonContext)(p: Program): Program = {
- val reporter = new QuietReporter
+ val reporter = new SilentReporter
val mainSolver = new FairZ3Solver(reporter)
mainSolver.setProgram(p)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 895ec71c4..936862fd4 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -13,7 +13,7 @@ import java.io.File
import collection.mutable.PriorityQueue
class Synthesizer(val r: Reporter,
- solver: Solver,
+ val solver: Solver,
generateDerivationTrees: Boolean,
filterFuns: Option[Set[String]],
firstOnly: Boolean,
@@ -70,18 +70,6 @@ class Synthesizer(val r: Reporter,
bestSolutionSoFar()
}
- def solveSAT(phi: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
- solver.solveOrGetCounterexample(Not(phi)) match {
- case (Some(true), _) =>
- (Some(false), Map())
- case (Some(false), model) =>
- (Some(true), model)
- case (None, _) =>
- println("WOOPS: failure on "+phi)
- (None, Map())
- }
- }
-
val rules = Rules.all(this) ++ Heuristics.all(this)
import purescala.Trees._
--
GitLab