Skip to content
Snippets Groups Projects
Commit 982874fd authored by Régis Blanc's avatar Régis Blanc
Browse files

managed to generate a function body of a function model

parent d382964d
No related branches found
No related tags found
No related merge requests found
......@@ -581,7 +581,6 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
case (Some(true), m) => { // SAT
//println("MODEL IS: " + m)
validatingStopwatch.start
val (trueModel, model) = if(Settings.verifyModel)
validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
......@@ -781,6 +780,18 @@ 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))
ite.toString
}).mkString("\n"))
if(!forceStop) {
val asMap = modelToMap(model, variables)
model.delete
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment