Skip to content
Snippets Groups Projects
Commit 3623ccd1 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Define Printable for non-leon-trees

parent 113a7aea
No related branches found
No related tags found
No related merge requests found
...@@ -11,7 +11,7 @@ import Definitions.Program ...@@ -11,7 +11,7 @@ import Definitions.Program
object Common { object Common {
abstract class Tree extends Positioned with Serializable { abstract class Tree extends Positioned with Serializable with Printable {
def copiedFrom(o: Tree): this.type = { def copiedFrom(o: Tree): this.type = {
setPos(o) setPos(o)
this this
......
package leon
package purescala
trait Printable {
def asString(implicit ctx: LeonContext): String
}
...@@ -12,11 +12,9 @@ import TypeOps._ ...@@ -12,11 +12,9 @@ import TypeOps._
object Types { object Types {
trait Typed { trait Typed extends Printable {
val getType: TypeTree val getType: TypeTree
def isTyped : Boolean = getType != Untyped def isTyped : Boolean = getType != Untyped
def asString(implicit ctx: LeonContext): String
} }
class TypeErrorException(msg: String) extends Exception(msg) class TypeErrorException(msg: String) extends Exception(msg)
......
...@@ -494,6 +494,7 @@ abstract class SMTLIBSolver(val context: LeonContext, ...@@ -494,6 +494,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case BVUMinus(u) => FixedSizeBitVectors.Neg(toSMT(u)) case BVUMinus(u) => FixedSizeBitVectors.Neg(toSMT(u))
case BVNot(u) => FixedSizeBitVectors.Not(toSMT(u)) case BVNot(u) => FixedSizeBitVectors.Not(toSMT(u))
case Assert(a,_, b) => toSMT(IfExpr(a, b, Error(b.getType, "assertion failed"))) case Assert(a,_, b) => toSMT(IfExpr(a, b, Error(b.getType, "assertion failed")))
case Equals(a,b) => Core.Equals(toSMT(a), toSMT(b)) case Equals(a,b) => Core.Equals(toSMT(a), toSMT(b))
case Implies(a,b) => Core.Implies(toSMT(a), toSMT(b)) case Implies(a,b) => Core.Implies(toSMT(a), toSMT(b))
case Plus(a,b) => Ints.Add(toSMT(a), toSMT(b)) case Plus(a,b) => Ints.Add(toSMT(a), toSMT(b))
......
...@@ -4,12 +4,13 @@ package leon ...@@ -4,12 +4,13 @@ package leon
package solvers package solvers
package templates package templates
import purescala.Printable
import purescala.Common._ import purescala.Common._
import purescala.Expressions._ import purescala.Expressions._
import purescala.Types._ import purescala.Types._
import utils._ 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 debugSection = utils.DebugSectionSolver
implicit val ctx0 = ctx implicit val ctx0 = ctx
val reporter = ctx.reporter val reporter = ctx.reporter
...@@ -194,7 +195,7 @@ class UnrollingBank[T](ctx: LeonContext, templateGenerator: TemplateGenerator[T] ...@@ -194,7 +195,7 @@ class UnrollingBank[T](ctx: LeonContext, templateGenerator: TemplateGenerator[T]
reporter.debug("Generating clauses for: " + expr.asString) reporter.debug("Generating clauses for: " + expr.asString)
for (cls <- clauses) { for (cls <- clauses) {
reporter.debug(" . " + cls) reporter.debug(" . " + cls.asString(ctx))
} }
clauses clauses
......
...@@ -7,6 +7,7 @@ package z3 ...@@ -7,6 +7,7 @@ package z3
import utils._ import utils._
import _root_.z3.scala._ import _root_.z3.scala._
import purescala.Printable
import purescala.Common._ import purescala.Common._
import purescala.Definitions._ import purescala.Definitions._
import purescala.Expressions._ import purescala.Expressions._
...@@ -122,6 +123,10 @@ class FairZ3Solver(val context: LeonContext, val program: Program) ...@@ -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] { val templateGenerator = new TemplateGenerator(new TemplateEncoder[Z3AST] {
def encodeId(id: Identifier): Z3AST = { def encodeId(id: Identifier): Z3AST = {
idToFreshZ3Id(id) idToFreshZ3Id(id)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment