From 3df2a8d7e6cc7da168ccf4c1aa2a054ecbde1061 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 25 Apr 2012 22:52:10 +0200
Subject: [PATCH] special treatment of function that take a constant value
---
mytest/Epsilon1.scala | 6 +++++-
src/main/scala/leon/FairZ3Solver.scala | 11 ++++++++++-
2 files changed, 15 insertions(+), 2 deletions(-)
diff --git a/mytest/Epsilon1.scala b/mytest/Epsilon1.scala
index 1d83db59a..827c1e6e5 100644
--- a/mytest/Epsilon1.scala
+++ b/mytest/Epsilon1.scala
@@ -2,7 +2,11 @@ import leon.Utils._
object Epsilon1 {
- def foo(x: Int): Int = {
+ def greater(x: Int): Int = {
+ epsilon((y: Int) => y > x)
+ } ensuring(_ >= x)
+
+ def greaterWrong(x: Int): Int = {
epsilon((y: Int) => y >= x)
} ensuring(_ > x)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 20e1f1dac..2e10af6c5 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -808,7 +808,16 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
} else Seq()
} else Seq()
}).toMap
- val asMap = modelToMap(model, variables) ++ functionsAsMap
+ val constantFunctionsAsMap: Map[Identifier, Expr] = model.getModelConstantInterpretations.flatMap(p => {
+ if(isKnownDecl(p._1)) {
+ val fd = functionDeclToDef(p._1)
+ if(!fd.hasImplementation) {
+ Seq((fd.id, fromZ3Formula(model, p._2, Some(fd.returnType))))
+ } else Seq()
+ } else Seq()
+ }).toMap
+ //val undefinedFunctionIds = functionMap.keys.filterNot(fd => fd.hasImplementation || !fd.args.isEmpty).map(_.id)
+ val asMap = modelToMap(model, variables) ++ functionsAsMap ++ constantFunctionsAsMap
model.delete
lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
val evalResult = eval(asMap, formula, evaluator)
--
GitLab