From 8559fb26aa4f930501405c6e062235a24f0270ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 25 Apr 2012 22:57:03 +0200
Subject: [PATCH] clean up the code
---
src/main/scala/leon/FairZ3Solver.scala | 16 +++-------------
1 file changed, 3 insertions(+), 13 deletions(-)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 2e10af6c5..c29e06bac 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -780,19 +780,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private def validateAndDeleteModel(model: Z3Model, formula: Expr, variables: Set[Identifier], evaluator: Option[(Map[Identifier,Expr])=>Boolean]) : (Boolean, Map[Identifier,Expr]) = {
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))
-//
-
if(!forceStop) {
+
+ val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
val functionsAsMap: Map[Identifier, Expr] = functionsModel.flatMap(p => {
if(isKnownDecl(p._1)) {
val fd = functionDeclToDef(p._1)
@@ -816,7 +806,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
} 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")
--
GitLab