From 395244dc3a02201cddc93ece9ea3a821a2d87cef Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 22 Feb 2016 15:07:34 +0100
Subject: [PATCH] Finishing up ADT invariants
---
.../leon/solvers/templates/DatatypeManager.scala | 5 +++++
.../leon/solvers/templates/LambdaManager.scala | 7 +------
.../leon/solvers/templates/TemplateManager.scala | 13 +++++++------
.../scala/leon/solvers/z3/AbstractZ3Solver.scala | 2 +-
4 files changed, 14 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/solvers/templates/DatatypeManager.scala b/src/main/scala/leon/solvers/templates/DatatypeManager.scala
index 8f9c2202a..365fe85ff 100644
--- a/src/main/scala/leon/solvers/templates/DatatypeManager.scala
+++ b/src/main/scala/leon/solvers/templates/DatatypeManager.scala
@@ -20,6 +20,11 @@ import Template._
import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
+case class FreshFunction(expr: Expr) extends Expr with Extractable {
+ val getType = BooleanType
+ val extract = Some(Seq(expr), (exprs: Seq[Expr]) => FreshFunction(exprs.head))
+}
+
object DatatypeTemplate {
def apply[T](
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index edb096ef2..647c75a69 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -24,11 +24,6 @@ case class App[T](caller: T, tpe: FunctionType, args: Seq[Arg[T]], encoded: T) {
override def toString = "(" + caller + " : " + tpe + ")" + args.map(_.encoded).mkString("(", ",", ")")
}
-case class FreshFunction(expr: Expr) extends Expr with Extractable {
- val getType = BooleanType
- val extract = Some(Seq(expr), (exprs: Seq[Expr]) => FreshFunction(exprs.head))
-}
-
object LambdaTemplate {
def apply[T](
@@ -238,7 +233,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends DatatypeManager(enco
neqClauses ++ extClauses
}
- def assumptions: Seq[T] = freeBlockers.flatMap(_._2.map(p => encoder.mkNot(p._2))).toSeq
+ def assumptions: Seq[T] = freeBlockers.toSeq.flatMap(_._2.map(p => encoder.mkNot(p._1)))
private val typeBlockers = new IncrementalMap[T, T]()
private val typeEnablers: MutableSet[T] = MutableSet.empty
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index 62a3f0c76..56c8e6211 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -159,18 +159,19 @@ object Template {
var clauses: Seq[T] = Seq.empty
val cleanGuarded = guardedExprs.map { case (b, es) => b -> es.map { e =>
+ def clean(expr: Expr): Expr = postMap {
+ case FreshFunction(f) => Some(BooleanLiteral(true))
+ case _ => None
+ } (expr)
+
val withPaths = CollectorWithPaths { case FreshFunction(f) => f }.traverse(e)
functions ++= withPaths.map { case (f, TopLevelAnds(paths)) =>
val tpe = bestRealType(f.getType).asInstanceOf[FunctionType]
- val path = andJoin(paths.filterNot(_.isInstanceOf[FreshFunction]))
+ val path = andJoin(paths.map(clean))
(encodeExpr(and(Variable(b), path)), tpe, encodeExpr(f))
}
- val cleanExpr = postMap {
- case FreshFunction(f) => Some(BooleanLiteral(true))
- case _ => None
- } (e)
-
+ val cleanExpr = clean(e)
clauses :+= encodeExpr(Implies(Variable(b), cleanExpr))
cleanExpr
}}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 3cadf39a6..7ae02d83e 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -257,7 +257,7 @@ trait AbstractZ3Solver extends Solver {
}
case other =>
- throw SolverUnsupportedError(other, this)
+ unsupported(other)
}
protected[leon] def toZ3Formula(expr: Expr, initialMap: Map[Identifier, Z3AST] = Map.empty): Z3AST = {
--
GitLab