From 6ac88da4b9af7a5c2c004cca31b07219208eec94 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 13 Oct 2015 17:29:26 +0200
Subject: [PATCH] Implement a bad version of printing vc position in SMT file
---
src/main/scala/leon/solvers/Solver.scala | 5 ++++-
.../leon/solvers/combinators/PortfolioSolver.scala | 3 ++-
.../solvers/combinators/PortfolioSolverFactory.scala | 2 --
.../leon/solvers/combinators/RewritingSolver.scala | 1 -
.../leon/solvers/combinators/UnrollingSolver.scala | 3 ++-
.../leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala | 1 +
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 10 +++++++++-
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 11 ++++-------
8 files changed, 22 insertions(+), 14 deletions(-)
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 1e20b15fd..841a28e50 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -3,7 +3,7 @@
package leon
package solvers
-import utils.{DebugSectionSolver, Interruptible}
+import leon.utils.{Position, DebugSectionSolver, Interruptible}
import purescala.Expressions._
import purescala.Common.{Tree, Identifier}
import purescala.ExprOps._
@@ -87,8 +87,11 @@ trait Solver extends Interruptible {
implicit lazy val leonContext = context
+ def dbg(msg: => Any) = context.reporter.debug(msg)
+
def assertCnstr(expression: Expr): Unit
def assertVC(vc: VC) = {
+ dbg(s"; Solving $vc @ ${vc.getPos}\n")
assertCnstr(Not(vc.condition))
}
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 21580d6c2..b2003d101 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -4,7 +4,6 @@ package leon
package solvers
package combinators
-import purescala.Common._
import purescala.Expressions._
import verification.VC
@@ -32,6 +31,8 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
solvers.foreach(_.assertVC(vc))
}
+ override def dbg(msg: => Any) = solvers foreach (_.dbg(msg))
+
def check: Option[Boolean] = {
model = Model.empty
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
index 855911455..7c29a16d0 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
@@ -4,8 +4,6 @@ package leon
package solvers
package combinators
-import utils.Interruptible
-import scala.collection.mutable.Queue
import scala.reflect.runtime.universe._
class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFactory[S]])(implicit tag: TypeTag[S]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
diff --git a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
index 2c414f2c0..0419d7d6e 100644
--- a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
@@ -4,7 +4,6 @@ package leon
package solvers
package combinators
-import purescala.Common._
import purescala.Expressions._
abstract class RewritingSolver[+S <: Solver, T](underlying: S) {
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 6e75a33a9..0c7afeb65 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -15,7 +15,6 @@ import utils._
import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre}
import templates._
-import utils.Interruptible
import evaluators._
class UnrollingSolver(val context: LeonContext, val program: Program, underlying: Solver)
@@ -85,6 +84,8 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
}
}
+ override def dbg(msg: => Any) = underlying.dbg(msg)
+
def push() {
unrollingBank.push()
solver.push()
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
index bfcb70668..f98b4f7e4 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
@@ -14,6 +14,7 @@ trait SMTLIBQuantifiedSolver {
// The reason is we do not want to assume postconditions of functions referring to
// the current function, as this may make the proof unsound
override def assertVC(vc: VC) = {
+ dbg(s"; Solving $vc")
currentFunDef = Some(vc.fd)
assertCnstr(withInductiveHyp(vc.condition))
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 05476ac11..99b4d9d17 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -4,6 +4,7 @@ package leon
package solvers
package smtlib
+import verification.VC
import purescala.Common._
import purescala.Expressions._
import purescala.ExprOps._
@@ -23,8 +24,15 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
/* Reporter */
protected val reporter = context.reporter
+ override def dbg(msg: => Any) = {
+ debugOut foreach { o =>
+ o.write(msg.toString)
+ o.flush()
+ }
+ }
+
/* Public solver interface */
- override def assertCnstr(expr: Expr): Unit = if(!hasError) {
+ def assertCnstr(expr: Expr): Unit = if(!hasError) {
try {
variablesOf(expr).foreach(declareVariable)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 9035700a0..01b35d9de 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -24,21 +24,18 @@ import _root_.smtlib.parser.Terms.{
Let => SMTLet,
_
}
-import _root_.smtlib.theories.Core.{
- Equals => SMTEquals
-}
import _root_.smtlib.parser.CommandsResponses.{ Error => ErrorResponse, _ }
import _root_.smtlib.theories._
import _root_.smtlib.interpreters.ProcessInterpreter
trait SMTLIBTarget extends Interruptible {
- val context: LeonContext;
- val program: Program;
- protected val reporter: Reporter;
+ val context: LeonContext
+ val program: Program
+ protected val reporter: Reporter
def targetName: String
- implicit val debugSection: DebugSection;
+ implicit val debugSection: DebugSection
protected def interpreterOps(ctx: LeonContext): Seq[String]
--
GitLab