From 57094716a81770c86366b905228de069b3027618 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 5 Aug 2016 18:35:40 +0200
Subject: [PATCH] Delete rewriting solver
---
.../solvers/combinators/RewritingSolver.scala | 32 -------------------
1 file changed, 32 deletions(-)
delete mode 100644 src/main/scala/inox/solvers/combinators/RewritingSolver.scala
diff --git a/src/main/scala/inox/solvers/combinators/RewritingSolver.scala b/src/main/scala/inox/solvers/combinators/RewritingSolver.scala
deleted file mode 100644
index ff0c8bf6f..000000000
--- a/src/main/scala/inox/solvers/combinators/RewritingSolver.scala
+++ /dev/null
@@ -1,32 +0,0 @@
-/* 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)
- }
- }
-}
--
GitLab