From bcb2b0cd8fb437d1e6dacb8941804a34f63cf991 Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Wed, 10 Feb 2016 19:34:54 +0100
Subject: [PATCH] In the midst of updating Orb to use unflatenned exprs while
solving
---
.../templateSolvers/NLTemplateSolver.scala | 6 +-
.../templateSolvers/TemplateSolver.scala | 2 +
.../util/ExpressionTransformer.scala | 6 +-
.../invariant/util/FlatToUnflatExpr.scala | 60 +++++++++++++++++++
4 files changed, 69 insertions(+), 5 deletions(-)
create mode 100644 src/main/scala/leon/invariant/util/FlatToUnflatExpr.scala
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 31f9e8b47..82255bbfa 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -42,7 +42,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val debugAxioms = false
val verifyInvariant = false
val debugReducedFormula = false
- val trackUnpackedVCCTime = true
+ val trackUnpackedVCCTime = false
//print flags
val verbose = true
@@ -445,9 +445,9 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
//for debugging
if (this.trackUnpackedVCCTime) {
- val upVCinst = simplifyArithmetic(TemplateInstantiator.instantiate(ctrTracker.getVC(fd).unpackedExpr, tempVarMap))
+ val upVCinst = unFlatten(simplifyArithmetic(
+ TemplateInstantiator.instantiate(ctrTracker.getVC(fd).unpackedExpr, tempVarMap)))
Stats.updateCounterStats(atomNum(upVCinst), "UP-VC-size", "disjuncts")
-
t1 = System.currentTimeMillis()
val (res2, _) = SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())).solveSAT(upVCinst)
val unpackedTime = System.currentTimeMillis() - t1
diff --git a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
index a85a7d4f5..c9876ffd1 100644
--- a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
@@ -1,6 +1,7 @@
package leon
package invariant.templateSolvers
+import scala.collection.mutable.{Map => MutableMap}
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
@@ -13,6 +14,7 @@ import invariant.structure._
import invariant.structure.FunctionUtils._
import leon.solvers.Model
import PredicateUtil._
+import ExpressionTransformer._
abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
ctrTracker: ConstraintTracker) {
diff --git a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
index 83ed0a86b..8f72e12ec 100644
--- a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
+++ b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
@@ -471,7 +471,7 @@ object ExpressionTransformer {
* This is used to produce a readable formula or more efficiently
* solvable formulas.
*/
- def unFlatten(ine: Expr): Expr = {
+ def unFlattenWithMap(ine: Expr): (Expr, Map[Identifier,Expr]) = {
var idMap = Map[Identifier, Expr]()
val newe = simplePostTransform {
case e @ Equals(Variable(id), rhs @ _) if isTemp(id, flatContext) =>
@@ -483,9 +483,11 @@ object ExpressionTransformer {
case e => e
}(ine)
val closure = (e: Expr) => replaceFromIDs(idMap, e)
- fix(closure)(newe)
+ (fix(closure)(newe), idMap)
}
+ def unFlatten(ine: Expr) = unFlattenWithMap(ine)._1
+
/**
* convert all integer constants to real constants
*/
diff --git a/src/main/scala/leon/invariant/util/FlatToUnflatExpr.scala b/src/main/scala/leon/invariant/util/FlatToUnflatExpr.scala
new file mode 100644
index 000000000..563a7feb5
--- /dev/null
+++ b/src/main/scala/leon/invariant/util/FlatToUnflatExpr.scala
@@ -0,0 +1,60 @@
+package leon
+package invariant.util
+
+import purescala.Common._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
+import invariant.factories._
+import solvers._
+import scala.collection.immutable._
+import scala.collection.mutable.{Set => MutableSet, Map => MutableMap}
+import ExpressionTransformer._
+import leon.evaluators._
+import EvaluationResults._
+
+/**
+ *A class that can used to compress a flattened expression
+ * and also expand the compressed models to the flat forms
+ */
+class FlatToUnflatExpr(ine: Expr, eval: DeterministicEvaluator) {
+
+ val (unflate, flatIdMap) = unFlattenWithMap(ine)
+ def getModel(m: Model) = new FlatModel(m)
+
+ /**
+ * Expands the model into a model with mappings for identifiers.
+ * Note: this class cannot be accessed in parallel.
+ */
+ class FlatModel(initModel: Model) {
+ var idModel = initModel.toMap
+
+ def apply(iden: Identifier) = {
+ var seen = Set[Identifier]()
+ def recBind(id: Identifier): Expr = {
+ val idv = idModel.get(id)
+ if (idv.isDefined) idv.get
+ else {
+ if (seen(id)) {
+ //we are in a cycle here
+ throw new IllegalStateException(s"$id depends on itself $id, input expression: $ine")
+ } else if (flatIdMap.contains(id)) {
+ val rhs = flatIdMap(id)
+ // recursively bind all freevars to values (we can ignore the return values)
+ seen += id
+ variablesOf(rhs).map(recBind)
+ eval.eval(rhs, idModel) match {
+ case Successful(v) =>
+ idModel += (id -> v)
+ v
+ case _ =>
+ throw new IllegalStateException(s"Evaluation Falied for $rhs")
+ }
+ } else
+ throw new IllegalStateException(s"Cannot extract model $id as it is not a part of the input expression: $ine")
+ }
+ }
+ recBind(iden)
+ }
+ }
+}
\ No newline at end of file
--
GitLab