From 4dd083500db56f4978a1709cab2bb7676a7dfbc3 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 1 Nov 2016 16:49:27 +0100
Subject: [PATCH] Some fixes for ADT invariants
---
.../inox/solvers/unrolling/DatatypeTemplates.scala | 11 ++++++++++-
1 file changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index 9a2f915e3..49114239e 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -138,7 +138,8 @@ trait DatatypeTemplates { self: Templates =>
guardedExprs += pathVar -> (expr +: prev)
}
- @inline protected def iff(e1: Expr, e2: Expr): Unit = storeGuarded(pathVar, Equals(e1, e2))
+ private var equations = Seq[Expr]()
+ @inline protected def iff(e1: Expr, e2: Expr): Unit = equations :+= Equals(e1, e2)
private var tpes = Map[Variable, Set[(TypedADTSort, Expr)]]()
@inline protected def storeType(pathVar: Variable, tsort: TypedADTSort, arg: Expr): Unit = {
@@ -179,6 +180,7 @@ trait DatatypeTemplates { self: Templates =>
}
val vars = tpes.keys.toSet ++ functions.keys ++
+ guardedExprs.keys ++
guardedExprs.flatMap(_._2.flatMap(exprOps.variablesOf))
if (vars(newBool)) {
@@ -223,6 +225,8 @@ trait DatatypeTemplates { self: Templates =>
if (callInfos.nonEmpty) calls += encoder(b) -> callInfos
}
+ clauses ++= equations.map(encoder)
+
val encodedTypes: Map[Encoded, Set[(TypedADTSort, Encoded)]] = tpes.map { case (b, tps) =>
encoder(b) -> tps.map { case (tadt, expr) => (tadt, encoder(expr)) }
}
@@ -487,6 +491,11 @@ trait DatatypeTemplates { self: Templates =>
newClauses ++= template.instantiate(blocker, container, arg)
}
+ ctx.reporter.debug("Unrolling datatypes (" + newClauses.size + ")")
+ for (cl <- newClauses) {
+ ctx.reporter.debug(" . " + cl)
+ }
+
newClauses.toSeq
}
}
--
GitLab