From 15a2c73170e310db5b972e0370081de53ef76392 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 11 Mar 2016 16:00:45 +0100
Subject: [PATCH] Fix comparison bugs
---
.../scala/leon/solvers/combinators/UnrollingSolver.scala | 2 +-
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 9 +--------
src/main/scala/leon/synthesis/rules/StringRender.scala | 2 +-
3 files changed, 3 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 2e896736f..6594eb07e 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -663,7 +663,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
override def foundAnswer(res: Option[Boolean], model: Model = Model.empty, core: Set[Expr] = Set.empty) = {
super.foundAnswer(res, model, core)
- if (!interrupted && res == None && model == None) {
+ if (!interrupted && res.isEmpty && model.isEmpty) {
reporter.ifDebug { debug =>
debug("Unknown result!?")
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index d87559f93..fa3352b1e 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -10,18 +10,11 @@ import _root_.z3.scala._
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
-import purescala.Constructors._
-import purescala.Quantification._
import purescala.ExprOps._
import purescala.Types._
import solvers.templates._
import solvers.combinators._
-import Template._
-
-import evaluators._
-
-import termination._
class FairZ3Solver(val context: LeonContext, val program: Program)
extends AbstractZ3Solver
@@ -211,7 +204,7 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
override def foundAnswer(res: Option[Boolean], model: Model = Model.empty, core: Set[Expr] = Set.empty) = {
super.foundAnswer(res, model, core)
- if (!interrupted && res == None && model == None) {
+ if (!interrupted && res.isEmpty && model.isEmpty) {
reporter.ifDebug { debug =>
if (solver.getReasonUnknown != "canceled") {
debug("Z3 returned unknown: " + solver.getReasonUnknown)
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 7085ed7d9..ec681763e 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -419,7 +419,7 @@ case object StringRender extends Rule("StringRender") {
.excludeFunction(hctx.functionContext)
.prettyPrintersForType(input.getType)(hctx, hctx.program)
.map(l => (application(l, Seq(input)), List[Identifier]())) // Use already pre-defined pretty printers.
- val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(fd, _)), _) if fd == hctx.functionContext => 0 case _ => 1}
+ val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(tfd, _)), _) if tfd.fd == hctx.functionContext => 0 case _ => 1}
val exprs2 = ctx.abstractStringConverters.getOrElse(input.getType, Nil).map(f => (f(input), List[Identifier]()))
val defaultConverters: Stream[WithIds[Expr]] = exprs1.toStream #::: exprs2.toStream
val recursiveConverters: Stream[WithIds[Expr]] =
--
GitLab