From 3623ccd18f897a4c59ad65b9d304bf78385a8e81 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 17 Aug 2015 15:10:19 +0200
Subject: [PATCH] Define Printable for non-leon-trees
---
src/main/scala/leon/purescala/Common.scala | 2 +-
src/main/scala/leon/purescala/Printable.scala | 7 +++++++
src/main/scala/leon/purescala/Types.scala | 4 +---
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 1 +
src/main/scala/leon/solvers/templates/UnrollingBank.scala | 5 +++--
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 5 +++++
6 files changed, 18 insertions(+), 6 deletions(-)
create mode 100644 src/main/scala/leon/purescala/Printable.scala
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index e10036a36..38206418d 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -11,7 +11,7 @@ import Definitions.Program
object Common {
- abstract class Tree extends Positioned with Serializable {
+ abstract class Tree extends Positioned with Serializable with Printable {
def copiedFrom(o: Tree): this.type = {
setPos(o)
this
diff --git a/src/main/scala/leon/purescala/Printable.scala b/src/main/scala/leon/purescala/Printable.scala
new file mode 100644
index 000000000..27be03538
--- /dev/null
+++ b/src/main/scala/leon/purescala/Printable.scala
@@ -0,0 +1,7 @@
+package leon
+package purescala
+
+
+trait Printable {
+ def asString(implicit ctx: LeonContext): String
+}
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index b780cfb69..d39fda333 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -12,11 +12,9 @@ import TypeOps._
object Types {
- trait Typed {
+ trait Typed extends Printable {
val getType: TypeTree
def isTyped : Boolean = getType != Untyped
-
- def asString(implicit ctx: LeonContext): String
}
class TypeErrorException(msg: String) extends Exception(msg)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index b3365ba28..26fb3d9a1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -494,6 +494,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case BVUMinus(u) => FixedSizeBitVectors.Neg(toSMT(u))
case BVNot(u) => FixedSizeBitVectors.Not(toSMT(u))
case Assert(a,_, b) => toSMT(IfExpr(a, b, Error(b.getType, "assertion failed")))
+
case Equals(a,b) => Core.Equals(toSMT(a), toSMT(b))
case Implies(a,b) => Core.Implies(toSMT(a), toSMT(b))
case Plus(a,b) => Ints.Add(toSMT(a), toSMT(b))
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 95a9e47ce..07bc7de6d 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -4,12 +4,13 @@ package leon
package solvers
package templates
+import purescala.Printable
import purescala.Common._
import purescala.Expressions._
import purescala.Types._
import utils._
-class UnrollingBank[T](ctx: LeonContext, templateGenerator: TemplateGenerator[T]) extends IncrementalState {
+class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: TemplateGenerator[T]) extends IncrementalState {
implicit val debugSection = utils.DebugSectionSolver
implicit val ctx0 = ctx
val reporter = ctx.reporter
@@ -194,7 +195,7 @@ class UnrollingBank[T](ctx: LeonContext, templateGenerator: TemplateGenerator[T]
reporter.debug("Generating clauses for: " + expr.asString)
for (cls <- clauses) {
- reporter.debug(" . " + cls)
+ reporter.debug(" . " + cls.asString(ctx))
}
clauses
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 5a42c60c4..eef9ffb90 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -7,6 +7,7 @@ package z3
import utils._
import _root_.z3.scala._
+import purescala.Printable
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
@@ -122,6 +123,10 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
}
}
+ implicit val z3Printable = (z3: Z3AST) => new Printable {
+ def asString(implicit ctx: LeonContext) = z3.toString
+ }
+
val templateGenerator = new TemplateGenerator(new TemplateEncoder[Z3AST] {
def encodeId(id: Identifier): Z3AST = {
idToFreshZ3Id(id)
--
GitLab