From 82e00daa7c4c54fc4c205be9fd6918c882daa16d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 25 Apr 2012 18:36:03 +0200
Subject: [PATCH] model evaluation can handle function model for epsilon
---
src/main/scala/leon/Evaluator.scala | 5 ++--
src/main/scala/leon/FairZ3Solver.scala | 33 +++++++++++++++++---------
2 files changed, 25 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index 72c62ef15..0f3204e70 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -85,10 +85,11 @@ object Evaluator {
}
}
- if(!fd.hasBody) {
+ if(!fd.hasBody && !context.isDefinedAt(fd.id)) {
throw RuntimeErrorEx("Evaluation of function with unknown implementation.")
}
- val callResult = rec(frame, matchToIfThenElse(fd.body.get))
+ val body = fd.body.getOrElse(context(fd.id))
+ val callResult = rec(frame, matchToIfThenElse(body))
if(fd.hasPostcondition) {
val freshResID = FreshIdentifier("result").setType(fd.returnType)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 7745edc76..5dc1f673e 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -781,19 +781,30 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
import Evaluator._
val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
- println(functionsModel.toList.map(p => p._1 + " -> " + {
- val (cses, default) = p._2
- val ite = cses.foldLeft(fromZ3Formula(model, default))((expr, q) => IfExpr(
- And(
- q._1.zip(functionDeclToDef(p._1).args).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id)))
- ),
- fromZ3Formula(model, q._2),
- expr))
- ite.toString
- }).mkString("\n"))
+
+// println(functionsModel.toList.map(p => p._1 + " -> " + {
+// val (cses, default) = p._2
+// val ite = cses.foldLeft(fromZ3Formula(model, default))((expr, q) => IfExpr(
+// And(
+// q._1.zip(functionDeclToDef(p._1).args).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id)))
+// ),
+// fromZ3Formula(model, q._2),
+// expr))
+//
if(!forceStop) {
- val asMap = modelToMap(model, variables)
+ val functionsAsMap = functionsModel.map(p => {
+ val fd = functionDeclToDef(p._1)
+ val (cses, default) = p._2
+ val ite = cses.foldLeft(fromZ3Formula(model, default))((expr, q) => IfExpr(
+ And(
+ q._1.zip(fd.args).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id)))
+ ),
+ fromZ3Formula(model, q._2),
+ expr))
+ (fd.id, ite)
+ })
+ val asMap = modelToMap(model, variables) ++ functionsAsMap
model.delete
lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
val evalResult = eval(asMap, formula, evaluator)
--
GitLab