From 284bdf34bdad542eafc8d495fba2897a292ae7ab Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 23 Oct 2015 16:56:12 +0200
Subject: [PATCH] Solver should instantiate reporter before registering with
InterruptManager
---
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 4 ----
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 11 ++++++++---
src/main/scala/leon/solvers/sygus/SygusSolver.scala | 10 ----------
src/main/scala/leon/synthesis/rules/SygusCVC4.scala | 2 --
4 files changed, 8 insertions(+), 19 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 99b4d9d17..f13ed21a2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -4,7 +4,6 @@ package leon
package solvers
package smtlib
-import verification.VC
import purescala.Common._
import purescala.Expressions._
import purescala.ExprOps._
@@ -21,9 +20,6 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
def targetName: String
override def name: String = "smt-"+targetName
- /* Reporter */
- protected val reporter = context.reporter
-
override def dbg(msg: => Any) = {
debugOut foreach { o =>
o.write(msg.toString)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 01b35d9de..33b3a26d8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -16,10 +16,15 @@ import purescala.Definitions._
import _root_.smtlib.common._
import _root_.smtlib.printer.{ RecursivePrinter => SMTPrinter }
-import _root_.smtlib.parser.Commands.{ Constructor => SMTConstructor, FunDef => _, Assert => SMTAssert, _ }
+import _root_.smtlib.parser.Commands.{
+ Constructor => SMTConstructor,
+ FunDef => _,
+ Assert => _,
+ _
+}
import _root_.smtlib.parser.Terms.{
Forall => SMTForall,
- Exists => SMTExists,
+ Exists => _,
Identifier => SMTIdentifier,
Let => SMTLet,
_
@@ -31,7 +36,7 @@ import _root_.smtlib.interpreters.ProcessInterpreter
trait SMTLIBTarget extends Interruptible {
val context: LeonContext
val program: Program
- protected val reporter: Reporter
+ protected def reporter = context.reporter
def targetName: String
diff --git a/src/main/scala/leon/solvers/sygus/SygusSolver.scala b/src/main/scala/leon/solvers/sygus/SygusSolver.scala
index b0a7f0aab..6d2c76789 100644
--- a/src/main/scala/leon/solvers/sygus/SygusSolver.scala
+++ b/src/main/scala/leon/solvers/sygus/SygusSolver.scala
@@ -4,24 +4,16 @@ package leon
package solvers
package sygus
-import utils._
-import grammars._
-
import purescala.Common._
import purescala.Definitions._
-import purescala.Types._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Constructors._
import purescala.Expressions._
-import scala.collection.mutable.ArrayBuffer
-
import synthesis.Problem
import leon.solvers.smtlib._
-import _root_.smtlib.common._
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.parser.CommandsResponses.{Error => _, _}
@@ -31,8 +23,6 @@ abstract class SygusSolver(val context: LeonContext, val program: Program, val p
implicit val ctx = context
implicit val debugSection = leon.utils.DebugSectionSynthesis
- val reporter = context.reporter
-
protected def unsupported(t: Tree, str: String): Nothing = {
throw new Unsupported(t, str)
}
diff --git a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala b/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
index 7a0e7edf4..7760b8c0d 100644
--- a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
+++ b/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
@@ -4,11 +4,9 @@ package leon
package synthesis
package rules
-import purescala.Types._
import solvers.sygus._
import grammars._
-import utils._
case object SygusCVC4 extends Rule("SygusCVC4") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
--
GitLab