Skip to content
Snippets Groups Projects
Commit 284bdf34 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Solver should instantiate reporter before registering with InterruptManager

parent f6b9d08c
No related branches found
No related tags found
No related merge requests found
...@@ -4,7 +4,6 @@ package leon ...@@ -4,7 +4,6 @@ package leon
package solvers package solvers
package smtlib package smtlib
import verification.VC
import purescala.Common._ import purescala.Common._
import purescala.Expressions._ import purescala.Expressions._
import purescala.ExprOps._ import purescala.ExprOps._
...@@ -21,9 +20,6 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program) ...@@ -21,9 +20,6 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
def targetName: String def targetName: String
override def name: String = "smt-"+targetName override def name: String = "smt-"+targetName
/* Reporter */
protected val reporter = context.reporter
override def dbg(msg: => Any) = { override def dbg(msg: => Any) = {
debugOut foreach { o => debugOut foreach { o =>
o.write(msg.toString) o.write(msg.toString)
......
...@@ -16,10 +16,15 @@ import purescala.Definitions._ ...@@ -16,10 +16,15 @@ import purescala.Definitions._
import _root_.smtlib.common._ import _root_.smtlib.common._
import _root_.smtlib.printer.{ RecursivePrinter => SMTPrinter } 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.{ import _root_.smtlib.parser.Terms.{
Forall => SMTForall, Forall => SMTForall,
Exists => SMTExists, Exists => _,
Identifier => SMTIdentifier, Identifier => SMTIdentifier,
Let => SMTLet, Let => SMTLet,
_ _
...@@ -31,7 +36,7 @@ import _root_.smtlib.interpreters.ProcessInterpreter ...@@ -31,7 +36,7 @@ import _root_.smtlib.interpreters.ProcessInterpreter
trait SMTLIBTarget extends Interruptible { trait SMTLIBTarget extends Interruptible {
val context: LeonContext val context: LeonContext
val program: Program val program: Program
protected val reporter: Reporter protected def reporter = context.reporter
def targetName: String def targetName: String
......
...@@ -4,24 +4,16 @@ package leon ...@@ -4,24 +4,16 @@ package leon
package solvers package solvers
package sygus package sygus
import utils._
import grammars._
import purescala.Common._ import purescala.Common._
import purescala.Definitions._ import purescala.Definitions._
import purescala.Types._
import purescala.ExprOps._ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Constructors._ import purescala.Constructors._
import purescala.Expressions._ import purescala.Expressions._
import scala.collection.mutable.ArrayBuffer
import synthesis.Problem import synthesis.Problem
import leon.solvers.smtlib._ import leon.solvers.smtlib._
import _root_.smtlib.common._
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _} import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _} import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.parser.CommandsResponses.{Error => _, _} import _root_.smtlib.parser.CommandsResponses.{Error => _, _}
...@@ -31,8 +23,6 @@ abstract class SygusSolver(val context: LeonContext, val program: Program, val p ...@@ -31,8 +23,6 @@ abstract class SygusSolver(val context: LeonContext, val program: Program, val p
implicit val ctx = context implicit val ctx = context
implicit val debugSection = leon.utils.DebugSectionSynthesis implicit val debugSection = leon.utils.DebugSectionSynthesis
val reporter = context.reporter
protected def unsupported(t: Tree, str: String): Nothing = { protected def unsupported(t: Tree, str: String): Nothing = {
throw new Unsupported(t, str) throw new Unsupported(t, str)
} }
......
...@@ -4,11 +4,9 @@ package leon ...@@ -4,11 +4,9 @@ package leon
package synthesis package synthesis
package rules package rules
import purescala.Types._
import solvers.sygus._ import solvers.sygus._
import grammars._ import grammars._
import utils._
case object SygusCVC4 extends Rule("SygusCVC4") { case object SygusCVC4 extends Rule("SygusCVC4") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = { def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment