Add program to TransformerWithPC. Implement SimplifierWithPC. Make some methods final.

src/main/scala/inox/transformers/Collector.scala

@@ -10,7 +10,7 @@ package transformers
 trait Collector extends Transformer {
   /** The type of collected objects */
   type R
-  type Result = (R, Env)
+  final type Result = (R, Env)
   import trees.Expr
   private var results: List[Result] = Nil
 
@@ -23,7 +23,7 @@ trait Collector extends Transformer {
   }
 
   /** Traverses the expression and collects */
-  def collect(e: Expr) = {
+  final def collect(e: Expr) = {
     results = Nil
     transform(e)
     results

src/main/scala/inox/transformers/CollectorWithPC.scala

@@ -11,10 +11,10 @@ object CollectorWithPC {
     new CollectorWithPC {
 
       type R = T
-      val trees: p.trees.type = p.trees
-      val symbols: p.symbols.type = p.symbols
-      import trees.Expr
-      import symbols.Path
+      val program: p.type = p
+      import program._
+      import symbols._
+      import trees._
       val initEnv: Path = Path.empty
 
       protected def step(e: Expr, env: Path): List[(T, Path)] = {

src/main/scala/inox/transformers/SimplifierWithPC.scala

@@ -3,19 +3,30 @@
 package inox
 package transformers
 
+import inox.solvers.{SimpleSolverAPI, SolverFactory}
+
 /** Uses solvers to perform PC-aware simplifications */
-trait SimplifierWithPC extends TransformerWithPC {
+trait SimplifierWithPC extends TransformerWithPC { self =>
 
+  import program._
   import trees._
-  import symbols.Path
-
-  implicit protected val s = symbols
+  import symbols._
+
+  protected val sf: SolverFactory{ val program: self.program.type }
+  protected lazy val s = SimpleSolverAPI(sf)
+
+  private def querie(e: Expr, path: Path, implied: Boolean) = {
+    val underTest = if (implied) e else Not(e)
+    try {
+      s.solveVALID(path implies underTest).contains(true)
+    } catch {
+      case _: Throwable =>
+        false
+    }
+  }
 
-  // FIXME: This needs to be changed when SolverAPI's are available
-  protected def impliedBy(e: Expr, path: Path) : Boolean
-  protected def contradictedBy(e: Expr, path: Path) : Boolean
-  protected def valid(e: Expr) : Boolean
-  protected def sat(e: Expr) : Boolean
+  protected final def impliedBy(e: Expr, path: Path) = querie(e, path, true)
+  protected final def contradictedBy(e: Expr, path: Path) = querie(e, path, false)
 
   protected override def rec(e: Expr, path: Path) = e match {
     case IfExpr(cond, thenn, _) if impliedBy(cond, path) =>
@@ -44,10 +55,10 @@ trait SimplifierWithPC extends TransformerWithPC {
     case Implies(lhs, rhs) if contradictedBy(lhs, path) =>
       BooleanLiteral(true).copiedFrom(e)
 
-    case a @ Assume(pred, body) if impliedBy(pred, path) =>
+    case Assume(pred, body) if impliedBy(pred, path) =>
       rec(body, path)
 
-    case a @ Assume(pred, body) if contradictedBy(pred, path) =>
+    case Assume(pred, body) if contradictedBy(pred, path) =>
       Assume(BooleanLiteral(false), rec(body, path))
 
     case b if b.getType == BooleanType && impliedBy(b, path) =>

src/main/scala/inox/transformers/Transformer.scala

@@ -25,10 +25,10 @@ trait Transformer {
   protected def rec(e: Expr, env: Env): Expr
 
   /** Transform an [[Expr]] with the specified environment */
-  def transform(e: Expr, init: Env): Expr = rec(e, init)
+  final def transform(e: Expr, init: Env): Expr = rec(e, init)
   /** Transform an [[Expr]] with the initial environment */
-  def transform(e: Expr): Expr            = transform(e, initEnv)
+  final def transform(e: Expr): Expr            = transform(e, initEnv)
   /** Transform the body of a [[FunDef]] */
-  def transform(fd: FunDef): Option[Expr] = fd.body.map(transform)
+  final def transform(fd: FunDef): Option[Expr] = fd.body.map(transform)
 }
 

src/main/scala/inox/transformers/TransformerWithPC.scala

@@ -5,11 +5,12 @@ package transformers
 
 /** A [[Transformer]] which uses path conditions as environment */
 trait TransformerWithPC extends Transformer {
+  val program: Program
+  import program._
+  final val trees: program.trees.type = program.trees
   import trees._
-  val symbols: Symbols
   import symbols._
   type Env = Path
-  import exprOps.replaceFromSymbols
 
   protected def rec(e: Expr, path: Path): Expr = e match {
     case Let(i, v, b) =>