Skip to content
Snippets Groups Projects
Commit 57094716 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Delete rewriting solver

parent 379ac744
Branches
Tags
No related merge requests found
/* Copyright 2009-2016 EPFL, Lausanne */
package leon
package solvers
package combinators
import purescala.Expressions._
abstract class RewritingSolver[+S <: Solver, T](underlying: S) {
val context = underlying.context
/** The type T is used to encode any meta information useful, for instance, to reconstruct
* models. */
def rewriteCnstr(expression: Expr) : (Expr,T)
def reconstructModel(model: Model, meta: T) : Model
private var storedMeta : List[T] = Nil
def assertCnstr(expression: Expr) {
val (rewritten, meta) = rewriteCnstr(expression)
storedMeta = meta :: storedMeta
underlying.assertCnstr(rewritten)
}
def getModel: Model = {
storedMeta match {
case Nil => underlying.getModel
case m :: _ => reconstructModel(underlying.getModel, m)
}
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment