From 8265a97e72c628c5915f9c4fabb5a00ac5aa9f76 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 20 Oct 2016 18:47:39 +0200
Subject: [PATCH] Nicer transformers
---
src/main/scala/inox/Program.scala | 4 +-
src/main/scala/inox/ast/Definitions.scala | 4 +-
src/main/scala/inox/ast/Identifier.scala | 2 +-
src/main/scala/inox/ast/ProgramEncoder.scala | 60 +++++--
src/main/scala/inox/ast/TreeOps.scala | 153 +++++-------------
src/main/scala/inox/ast/TypeOps.scala | 13 ++
.../inox/solvers/theories/BagEncoder.scala | 8 +-
.../inox/solvers/theories/StringEncoder.scala | 8 +-
.../inox/solvers/theories/TheoryEncoder.scala | 38 +----
.../solvers/unrolling/UnrollingSolver.scala | 10 +-
.../inox/solvers/z3/NativeZ3Solver.scala | 10 +-
11 files changed, 127 insertions(+), 183 deletions(-)
diff --git a/src/main/scala/inox/Program.scala b/src/main/scala/inox/Program.scala
index 374464d05..69ce5b2e5 100644
--- a/src/main/scala/inox/Program.scala
+++ b/src/main/scala/inox/Program.scala
@@ -30,9 +30,7 @@ trait Program {
val ctx = Program.this.ctx
}
- def transform(t: SymbolTransformer {
- val transformer: TreeTransformer { val s: trees.type }
- }): Program { val trees: t.t.type } = new Program {
+ def transform(t: SymbolTransformer { val s: trees.type }): Program { val trees: t.t.type } = new Program {
val trees: t.t.type = t.t
val symbols = t.transform(Program.this.symbols)
val ctx = Program.this.ctx
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index f010ad44f..a9491af7c 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -136,9 +136,7 @@ trait Definitions { self: Trees =>
functions.map(p => prettyPrint(p._2, opts)).mkString("\n\n")
}
- def transform(trans: SelfTransformer): Symbols = new SymbolTransformer {
- val transformer: trans.type = trans
- }.transform(this)
+ def transform(trans: SelfTransformer): Symbols = SymbolTransformer(trans).transform(this)
override def equals(that: Any): Boolean = that match {
case sym: AbstractSymbols => functions == sym.functions && adts == sym.adts
diff --git a/src/main/scala/inox/ast/Identifier.scala b/src/main/scala/inox/ast/Identifier.scala
index 557de837f..5ca58353d 100644
--- a/src/main/scala/inox/ast/Identifier.scala
+++ b/src/main/scala/inox/ast/Identifier.scala
@@ -10,7 +10,7 @@ import inox.utils.{UniqueCounter, Positioned}
class Identifier (
val name: String,
val globalId: Int,
- private val id: Int,
+ val id: Int,
private val alwaysShowUniqueID: Boolean = false
) extends Ordered[Identifier] with Positioned {
diff --git a/src/main/scala/inox/ast/ProgramEncoder.scala b/src/main/scala/inox/ast/ProgramEncoder.scala
index e7cae628d..0f8edaf9d 100644
--- a/src/main/scala/inox/ast/ProgramEncoder.scala
+++ b/src/main/scala/inox/ast/ProgramEncoder.scala
@@ -3,22 +3,58 @@
package inox
package ast
-trait ProgramEncoder extends TreeBijection {
+trait ProgramEncoder { self =>
val sourceProgram: Program
- lazy val s: sourceProgram.trees.type = sourceProgram.trees
- lazy val targetProgram: Program { val trees: t.type } = sourceProgram.transform(encoder)
+ val t: Trees
- /* @nv XXX: ideally, we would want to replace `>>` by `override def andThen`, however this
- * seems to break the scala compiler for some weird reason... */
- def >>(that: TreeBijection { val s: ProgramEncoder.this.t.type }): ProgramEncoder {
- val sourceProgram: ProgramEncoder.this.sourceProgram.type
+ protected val extraFunctions: Seq[t.FunDef] = Seq.empty
+ protected val extraADTs: Seq[t.ADTDefinition] = Seq.empty
+
+ /** Override point for more complex program transformations */
+ protected def encodedProgram: Program { val trees: t.type } = {
+ sourceProgram.transform(SymbolTransformer(encoder))
+ }
+
+ lazy final val s: sourceProgram.trees.type = sourceProgram.trees
+ lazy final val targetProgram: Program { val trees: t.type } = {
+ encodedProgram.withFunctions(extraFunctions).withADTs(extraADTs)
+ }
+
+ protected val encoder: TreeTransformer { val s: self.s.type; val t: self.t.type }
+ protected val decoder: TreeTransformer { val s: self.t.type; val t: self.s.type }
+
+ def encode(vd: s.ValDef): t.ValDef = encoder.transform(vd)
+ def decode(vd: t.ValDef): s.ValDef = decoder.transform(vd)
+
+ def encode(v: s.Variable): t.Variable = encoder.transform(v).asInstanceOf[t.Variable]
+ def decode(v: t.Variable): s.Variable = decoder.transform(v).asInstanceOf[s.Variable]
+
+ def encode(e: s.Expr): t.Expr = encoder.transform(e)
+ def decode(e: t.Expr): s.Expr = decoder.transform(e)
+
+ def encode(tpe: s.Type): t.Type = encoder.transform(tpe)
+ def decode(tpe: t.Type): s.Type = decoder.transform(tpe)
+
+ def compose(that: ProgramEncoder { val t: self.s.type }): ProgramEncoder {
+ val sourceProgram: that.sourceProgram.type
+ val t: self.t.type
+ } = new ProgramEncoder {
+ val sourceProgram: that.sourceProgram.type = that.sourceProgram
+ val t: self.t.type = self.t
+
+ val encoder = self.encoder compose that.encoder
+ val decoder = that.decoder compose self.decoder
+ }
+
+ def andThen(that: ProgramEncoder { val sourceProgram: self.targetProgram.type }): ProgramEncoder {
+ val sourceProgram: self.sourceProgram.type
val t: that.t.type
} = new ProgramEncoder {
- val sourceProgram: ProgramEncoder.this.sourceProgram.type = ProgramEncoder.this.sourceProgram
+ val sourceProgram: self.sourceProgram.type = self.sourceProgram
val t: that.t.type = that.t
- val encoder = ProgramEncoder.this.encoder andThen that.encoder
- val decoder = that.decoder andThen ProgramEncoder.this.decoder
+ val encoder = self.encoder andThen that.encoder
+ val decoder = that.decoder andThen self.decoder
}
}
@@ -30,8 +66,8 @@ object ProgramEncoder {
val sourceProgram: p.type = p
val t: p.trees.type = p.trees
- object encoder extends p.trees.IdentitySymbolTransformer
- object decoder extends p.trees.IdentitySymbolTransformer
+ protected object encoder extends p.trees.IdentityTreeTransformer
+ protected object decoder extends p.trees.IdentityTreeTransformer
}
}
diff --git a/src/main/scala/inox/ast/TreeOps.scala b/src/main/scala/inox/ast/TreeOps.scala
index 67de1df34..5aeeef5aa 100644
--- a/src/main/scala/inox/ast/TreeOps.scala
+++ b/src/main/scala/inox/ast/TreeOps.scala
@@ -21,7 +21,6 @@ trait TreeOps { self: Trees =>
trait IdentityTreeTransformer extends SelfTreeTransformer {
override def transform(id: Identifier, tpe: s.Type): (Identifier, t.Type) = (id, tpe)
- override def transform(v: s.Variable): t.Variable = v
override def transform(vd: s.ValDef): t.ValDef = vd
override def transform(e: s.Expr): t.Expr = e
override def transform(tpe: s.Type): t.Type = tpe
@@ -29,13 +28,9 @@ trait TreeOps { self: Trees =>
}
trait IdentitySymbolTransformer extends SymbolTransformer {
- /* For some reason, the scala compiler doesn't accept {{{
- * object transformer extends IdentityTreeTransformer
- * }}} which would be nicer. */
- val transformer = new IdentityTreeTransformer {}
+ val s: self.type = self
+ val t: self.type = self
- override protected final def transformFunction(fd: s.FunDef): t.FunDef = sys.error("unexpected")
- override protected final def transformADT(adt: s.ADTDefinition): t.ADTDefinition = sys.error("unexpected")
override def transform(syms: s.Symbols): t.Symbols = syms
}
@@ -69,15 +64,6 @@ trait TreeTransformer {
def transform(id: Identifier, tpe: s.Type): (Identifier, t.Type) = (id, transform(tpe))
- def transform(v: s.Variable): t.Variable = {
- val (id, tpe) = transform(v.id, v.tpe)
- if ((id ne v.id) || (tpe ne v.tpe) || (s ne t)) {
- t.Variable(id, tpe).copiedFrom(v)
- } else {
- v.asInstanceOf[t.Variable]
- }
- }
-
def transform(vd: s.ValDef): t.ValDef = {
val (id, es, Seq(tpe), builder) = deconstructor.deconstruct(vd)
val (newId, newTpe) = transform(id, tpe)
@@ -101,7 +87,7 @@ trait TreeTransformer {
var changed = false
val newVs = for (v <- vs) yield {
- val newV = transform(v)
+ val newV = transformVariable(v)
if (v ne newV) changed = true
newV
}
@@ -168,11 +154,18 @@ trait TreeTransformer {
/* Type parameters can't be modified by transformed but they need to be
* translated into the new tree definitions given by `t`. */
@inline
- protected[ast] final def transformTypeParams(tparams: Seq[s.TypeParameterDef]): Seq[t.TypeParameterDef] = {
+ final def transformTypeParams(tparams: Seq[s.TypeParameterDef]): Seq[t.TypeParameterDef] = {
if (s eq t) tparams.asInstanceOf[Seq[t.TypeParameterDef]]
else tparams.map(tdef => t.TypeParameterDef(t.TypeParameter(tdef.id)))
}
+ @inline
+ final def transformVariable(v: s.Variable): t.Variable = {
+ val (nid, ntpe) = transform(v.id, v.tpe)
+ if ((v.id ne nid) || (v.tpe ne ntpe) || (s ne t)) t.Variable(nid, ntpe).copiedFrom(v)
+ else v.asInstanceOf[t.Variable]
+ }
+
final def transform(fd: s.FunDef): t.FunDef = {
new t.FunDef(
fd.id,
@@ -215,7 +208,6 @@ trait TreeTransformer {
t2.transform(id1, tp1)
}
- override def transform(v: s.Variable): t.Variable = t2.transform(t1.transform(v))
override def transform(vd: s.ValDef): t.ValDef = t2.transform(t1.transform(vd))
override def transform(e: s.Expr): t.Expr = t2.transform(t1.transform(e))
override def transform(tpe: s.Type): t.Type = t2.transform(t1.transform(tpe))
@@ -250,115 +242,56 @@ trait TreeTransformer {
}
}
-/** Symbol table transformer */
-trait SymbolTransformer {
- val transformer: TreeTransformer
- lazy val s: transformer.s.type = transformer.s
- lazy val t: transformer.t.type = transformer.t
-
- def transform(id: Identifier, tpe: s.Type): (Identifier, t.Type) = transformer.transform(id, tpe)
- def transform(v: s.Variable): t.Variable = transformer.transform(v)
- def transform(vd: s.ValDef): t.ValDef = transformer.transform(vd)
- def transform(e: s.Expr): t.Expr = transformer.transform(e)
- def transform(tpe: s.Type): t.Type = transformer.transform(tpe)
- def transform(flag: s.Flag): t.Flag = transformer.transform(flag)
-
- @inline
- protected def transformTypeParams(tparams: Seq[s.TypeParameterDef]) = transformer.transformTypeParams(tparams)
+/** Symbol table transformer base type */
+trait SymbolTransformer { self =>
+ val s: Trees
+ val t: Trees
- protected def transformFunction(fd: s.FunDef): t.FunDef = transformer.transform(fd)
- protected def transformADT(adt: s.ADTDefinition): t.ADTDefinition = transformer.transform(adt)
-
- def transform(syms: s.Symbols): t.Symbols = t.NoSymbols
- .withFunctions(syms.functions.values.toSeq.map(transformFunction))
- .withADTs(syms.adts.values.toSeq.map(transformADT))
+ def transform(syms: s.Symbols): t.Symbols
def compose(that: SymbolTransformer {
- val transformer: TreeTransformer { val t: SymbolTransformer.this.s.type }
+ val t: self.s.type
}): SymbolTransformer {
- val transformer: TreeTransformer {
- val s: that.s.type
- val t: SymbolTransformer.this.t.type
- }
+ val s: that.s.type
+ val t: self.t.type
} = new SymbolTransformer {
- val transformer = SymbolTransformer.this.transformer compose that.transformer
- override def transform(syms: s.Symbols): t.Symbols = SymbolTransformer.this.transform(that.transform(syms))
+ val s: that.s.type = that.s
+ val t: self.t.type = self.t
+ override def transform(syms: s.Symbols): t.Symbols = self.transform(that.transform(syms))
}
def andThen(that: SymbolTransformer {
- val transformer: TreeTransformer { val s: SymbolTransformer.this.t.type }
+ val s: self.t.type
}): SymbolTransformer {
- val transformer: TreeTransformer {
- val s: SymbolTransformer.this.s.type
- val t: that.t.type
- }
+ val s: self.s.type
+ val t: that.t.type
} = {
// the scala compiler doesn't realize that this relation must hold here
that compose this.asInstanceOf[SymbolTransformer {
- val transformer: TreeTransformer {
- val s: SymbolTransformer.this.s.type
- val t: that.s.type
- }
+ val s: self.s.type
+ val t: that.s.type
}]
}
}
-trait TreeBijection {
- val s: Trees
- val t: Trees
-
- val encoder: SymbolTransformer { val transformer: TreeTransformer {
- val s: TreeBijection.this.s.type
- val t: TreeBijection.this.t.type
- }}
-
- val decoder: SymbolTransformer { val transformer: TreeTransformer {
- val s: TreeBijection.this.t.type
- val t: TreeBijection.this.s.type
- }}
-
- def encode(vd: s.ValDef): t.ValDef = encoder.transform(vd)
- def decode(vd: t.ValDef): s.ValDef = decoder.transform(vd)
-
- def encode(v: s.Variable): t.Variable = encoder.transform(v)
- def decode(v: t.Variable): s.Variable = decoder.transform(v)
-
- def encode(e: s.Expr): t.Expr = encoder.transform(e)
- def decode(e: t.Expr): s.Expr = decoder.transform(e)
-
- def encode(tpe: s.Type): t.Type = encoder.transform(tpe)
- def decode(tpe: t.Type): s.Type = decoder.transform(tpe)
-
- def inverse: TreeBijection {
- val s: TreeBijection.this.t.type
- val t: TreeBijection.this.s.type
- } = new TreeBijection {
- val s: TreeBijection.this.t.type = TreeBijection.this.t
- val t: TreeBijection.this.s.type = TreeBijection.this.s
+trait SimpleSymbolTransformer extends SymbolTransformer { self =>
+ protected def transformFunction(fd: s.FunDef): t.FunDef
+ protected def transformADT(adt: s.ADTDefinition): t.ADTDefinition
- val encoder = TreeBijection.this.decoder
- val decoder = TreeBijection.this.encoder
- }
-
- def compose(that: TreeBijection { val t: TreeBijection.this.s.type }): TreeBijection {
- val s: that.s.type
- val t: TreeBijection.this.t.type
- } = new TreeBijection {
- val s: that.s.type = that.s
- val t: TreeBijection.this.t.type = TreeBijection.this.t
-
- val encoder = TreeBijection.this.encoder compose that.encoder
- val decoder = that.decoder compose TreeBijection.this.decoder
- }
+ def transform(syms: s.Symbols): t.Symbols = t.NoSymbols
+ .withFunctions(syms.functions.values.toSeq.map(transformFunction))
+ .withADTs(syms.adts.values.toSeq.map(transformADT))
+}
- def andThen(that: TreeBijection { val s: TreeBijection.this.t.type }): TreeBijection {
- val s: TreeBijection.this.s.type
- val t: that.t.type
- } = new TreeBijection {
- val s: TreeBijection.this.s.type = TreeBijection.this.s
- val t: that.t.type = that.t
+object SymbolTransformer {
+ def apply(trans: TreeTransformer): SymbolTransformer {
+ val s: trans.s.type
+ val t: trans.t.type
+ } = new SimpleSymbolTransformer {
+ val s: trans.s.type = trans.s
+ val t: trans.t.type = trans.t
- val encoder = TreeBijection.this.encoder andThen that.encoder
- val decoder = that.decoder andThen TreeBijection.this.decoder
+ protected def transformFunction(fd: s.FunDef): t.FunDef = trans.transform(fd)
+ protected def transformADT(adt: s.ADTDefinition): t.ADTDefinition = trans.transform(adt)
}
}
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index d4006f908..1bc145426 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -187,6 +187,19 @@ trait TypeOps {
}
}
+ def greatestLowerBound(ts: Seq[Type]): Option[Type] = {
+ def oglb(ot1: Option[Type], t2: Option[Type]): Option[Type] = ot1 match {
+ case Some(t1) => greatestLowerBound(t1, t2.get)
+ case None => None
+ }
+
+ if (ts.isEmpty) {
+ None
+ } else {
+ ts.map(Some(_)).reduceLeft(oglb)
+ }
+ }
+
def isSubtypeOf(t1: Type, t2: Type): Boolean = {
leastUpperBound(t1, t2) == Some(t2)
}
diff --git a/src/main/scala/inox/solvers/theories/BagEncoder.scala b/src/main/scala/inox/solvers/theories/BagEncoder.scala
index b91f3e52d..c7badaee2 100644
--- a/src/main/scala/inox/solvers/theories/BagEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/BagEncoder.scala
@@ -71,10 +71,10 @@ trait BagEncoder extends TheoryEncoder {
})
}
- override val newFunctions = Seq(Get, Add, Union, Difference, Intersect, BagEquals)
- override val newADTs = Seq(bagADT)
+ override val extraFunctions = Seq(Get, Add, Union, Difference, Intersect, BagEquals)
+ override val extraADTs = Seq(bagADT)
- val treeEncoder = new SelfTreeTransformer {
+ protected object encoder extends SelfTreeTransformer {
import sourceProgram._
override def transform(e: Expr): Expr = e match {
@@ -117,7 +117,7 @@ trait BagEncoder extends TheoryEncoder {
}
}
- val treeDecoder = new SelfTreeTransformer {
+ protected object decoder extends SelfTreeTransformer {
import targetProgram._
override def transform(e: Expr): Expr = e match {
diff --git a/src/main/scala/inox/solvers/theories/StringEncoder.scala b/src/main/scala/inox/solvers/theories/StringEncoder.scala
index b37b9aaef..dac9759b9 100644
--- a/src/main/scala/inox/solvers/theories/StringEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/StringEncoder.scala
@@ -81,8 +81,8 @@ trait StringEncoder extends TheoryEncoder {
}
}))
- override val newFunctions = Seq(Size, Take, Drop, Slice, Concat)
- override val newADTs = Seq(stringADT, stringNilADT, stringConsADT)
+ override val extraFunctions = Seq(Size, Take, Drop, Slice, Concat)
+ override val extraADTs = Seq(stringADT, stringNilADT, stringConsADT)
private val stringBijection = new Bijection[String, Expr]()
@@ -95,7 +95,7 @@ trait StringEncoder extends TheoryEncoder {
v.toList.foldRight(StringNil()){ case (char, l) => StringCons(E(char), l) }
}
- val treeEncoder = new SelfTreeTransformer {
+ protected object encoder extends SelfTreeTransformer {
override def transform(e: Expr): Expr = e match {
case StringLiteral(v) => convertFromString(v)
case StringLength(a) => Size(transform(a)).copiedFrom(e)
@@ -113,7 +113,7 @@ trait StringEncoder extends TheoryEncoder {
}
}
- val treeDecoder = new SelfTreeTransformer {
+ protected object decoder extends SelfTreeTransformer {
override def transform(e: Expr): Expr = e match {
case cc @ ADT(adt, args) if adt == StringNil || adt == StringCons =>
StringLiteral(convertToString(cc)).copiedFrom(cc)
diff --git a/src/main/scala/inox/solvers/theories/TheoryEncoder.scala b/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
index 225aa13a4..b5d07dbcd 100644
--- a/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
+++ b/src/main/scala/inox/solvers/theories/TheoryEncoder.scala
@@ -6,47 +6,15 @@ package theories
import utils._
-trait TheoryEncoder extends ast.TreeBijection {
- val sourceProgram: Program
+trait TheoryEncoder extends ast.ProgramEncoder { self =>
lazy val trees: sourceProgram.trees.type = sourceProgram.trees
-
- lazy val s: trees.type = trees
lazy val t: trees.type = trees
-
- lazy val targetProgram: Program { val trees: TheoryEncoder.this.trees.type } = {
- sourceProgram.transform(encoder).withFunctions(newFunctions).withADTs(newADTs)
- }
-
- import trees._
-
- protected val treeEncoder: SelfTransformer
- protected val treeDecoder: SelfTransformer
-
- lazy val encoder = new ast.SymbolTransformer {
- val transformer: treeEncoder.type = treeEncoder
- }
-
- lazy val decoder = new ast.SymbolTransformer {
- val transformer: treeEncoder.type = treeEncoder
- }
-
- val newFunctions: Seq[FunDef] = Seq.empty
- val newADTs: Seq[ADTDefinition] = Seq.empty
-
- def >>(that: TheoryEncoder { val sourceProgram: TheoryEncoder.this.targetProgram.type }): TheoryEncoder {
- val sourceProgram: TheoryEncoder.this.sourceProgram.type
- } = new TheoryEncoder {
- val sourceProgram: TheoryEncoder.this.sourceProgram.type = TheoryEncoder.this.sourceProgram
-
- protected val treeEncoder: SelfTransformer = TheoryEncoder.this.treeEncoder andThen that.treeEncoder
- protected val treeDecoder: SelfTransformer = that.treeDecoder andThen TheoryEncoder.this.treeDecoder
- }
}
trait NoEncoder extends TheoryEncoder {
import trees._
- protected object treeEncoder extends IdentityTreeTransformer
- protected object treeDecoder extends IdentityTreeTransformer
+ protected object encoder extends IdentityTreeTransformer
+ protected object decoder extends IdentityTreeTransformer
}
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 4aaa154b5..9929f0e05 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -21,7 +21,7 @@ object optFeelingLucky extends FlagOptionDef(
object optUnrollAssumptions extends FlagOptionDef(
"unrollassumptions", "Use unsat-assumptions to drive unfolding while remaining fair", false)
-trait AbstractUnrollingSolver extends Solver {
+trait AbstractUnrollingSolver extends Solver { self =>
import program._
import program.trees._
@@ -32,9 +32,9 @@ trait AbstractUnrollingSolver extends Solver {
protected val encoder: ast.ProgramEncoder { val sourceProgram: program.type }
- protected val theories: TheoryEncoder { val sourceProgram: AbstractUnrollingSolver.this.encoder.targetProgram.type }
+ protected val theories: TheoryEncoder { val sourceProgram: self.encoder.targetProgram.type }
- protected lazy val programEncoder = encoder >> theories
+ protected lazy val programEncoder = encoder andThen theories
protected lazy val s: programEncoder.s.type = programEncoder.s
protected lazy val t: programEncoder.t.type = programEncoder.t
@@ -56,11 +56,11 @@ trait AbstractUnrollingSolver extends Solver {
protected val templates: Templates {
val program: targetProgram.type
- type Encoded = AbstractUnrollingSolver.this.Encoded
+ type Encoded = self.Encoded
}
protected val evaluator: DeterministicEvaluator with SolvingEvaluator {
- val program: AbstractUnrollingSolver.this.program.type
+ val program: self.program.type
}
protected val underlying: AbstractSolver {
diff --git a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
index 2b62d3683..87f3f2183 100644
--- a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
+++ b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala
@@ -9,8 +9,7 @@ import theories._
import z3.scala._
-trait NativeZ3Solver
- extends AbstractUnrollingSolver {
+trait NativeZ3Solver extends AbstractUnrollingSolver { self =>
import program._
import program.trees._
@@ -21,13 +20,12 @@ trait NativeZ3Solver
type Encoded = Z3AST
object theories extends {
- val sourceProgram: NativeZ3Solver.this.encoder.targetProgram.type =
- NativeZ3Solver.this.encoder.targetProgram
+ val sourceProgram: self.encoder.targetProgram.type = self.encoder.targetProgram
} with StringEncoder
protected object underlying extends {
val program: targetProgram.type = targetProgram
- val options = NativeZ3Solver.this.options
+ val options = self.options
} with AbstractZ3Solver
private lazy val z3 = underlying.z3
@@ -37,7 +35,7 @@ trait NativeZ3Solver
} with Templates {
import program.trees._
- type Encoded = NativeZ3Solver.this.Encoded
+ type Encoded = self.Encoded
def asString(ast: Z3AST): String = ast.toString
--
GitLab