From b01601dfdd01b18c73dcd7473fe2faf3f2962416 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 25 Apr 2012 21:21:02 +0200
Subject: [PATCH] fix bug: only collect relevant function and pass expected
type to avoid asarray operator
---
src/main/scala/leon/FairZ3Solver.scala | 26 +++++++++++++++-----------
1 file changed, 15 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 5dc1f673e..20e1f1dac 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -793,17 +793,21 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
//
if(!forceStop) {
- 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 functionsAsMap: Map[Identifier, Expr] = functionsModel.flatMap(p => {
+ if(isKnownDecl(p._1)) {
+ val fd = functionDeclToDef(p._1)
+ if(!fd.hasImplementation) {
+ val (cses, default) = p._2
+ val ite = cses.foldLeft(fromZ3Formula(model, default, Some(fd.returnType)))((expr, q) => IfExpr(
+ And(
+ q._1.zip(fd.args).map(a12 => Equals(fromZ3Formula(model, a12._1, Some(a12._2.tpe)), Variable(a12._2.id)))
+ ),
+ fromZ3Formula(model, q._2, Some(fd.returnType)),
+ expr))
+ Seq((fd.id, ite))
+ } else Seq()
+ } else Seq()
+ }).toMap
val asMap = modelToMap(model, variables) ++ functionsAsMap
model.delete
lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
--
GitLab