diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala index 2e10af6c538aad94f4414c8e936b50caf90b219c..c29e06bac2a14d19695db2cd8507a120aa3f4224 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")