From a454d391ef27051df6aa835479103bd174a3b47b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 28 Apr 2015 09:53:43 +0200
Subject: [PATCH] Fix some bugs in new z3 solver
---
.../smtlib/SMTLIBZ3QuantifiedTarget.scala | 98 +++++++++----------
1 file changed, 49 insertions(+), 49 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index ab38c5203..3087d1183 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -3,9 +3,10 @@ package leon.solvers.smtlib
import leon.purescala.DefOps._
import leon.purescala.Definitions.TypedFunDef
import leon.purescala.ExprOps._
-import leon.purescala.Expressions.{Equals, FunctionInvocation}
+import leon.purescala.Expressions._
+import leon.purescala.Constructors._
import smtlib.parser.Commands.{DeclareFun, Assert}
-import smtlib.parser.Terms.{Term, SortedVar, SSymbol, ForAll}
+import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol}
/**
* This solver models function definitions as universally quantified formulas.
@@ -20,57 +21,56 @@ trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target {
override def targetName = "z3-quantified"
override def declareFunction(tfd: TypedFunDef): SSymbol = {
- if (tfd.params.isEmpty) {
- super[SMTLIBZ3Target].declareFunction(tfd)
- } else {
- val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
- if (!exploredAll) {
- reporter.warning(
- s"Did not manage to explore the space of typed functions called from ${tfd.id}. The solver may fail"
- )
- }
- val smtFunDecls = funs.toSeq.collect {
- case tfd if !functions.containsA(tfd) && tfd.params.nonEmpty =>
- val id = if (tfd.tps.isEmpty) {
- tfd.id
- } else {
- tfd.id.freshen
- }
- val sym = id2sym(id)
- functions +=(tfd, sym)
- sendCommand(DeclareFun(
- sym,
- tfd.params map { p => declareSort(p.getType) },
- declareSort(tfd.returnType)
- ))
- sym
- }
- smtFunDecls foreach { sym =>
- val tfd = functions.toA(sym)
- val sortedVars = tfd.params.map { p =>
- SortedVar(id2sym(p.id), declareSort(p.getType))
- }
- val term =
- if (sortedVars.isEmpty) {
- toSMT(Equals(FunctionInvocation(tfd, Seq()), tfd.body.get))(Map())
- } else {
- ForAll(
- sortedVars.head,
- sortedVars.tail,
- toSMT(Equals(
- FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
- matchToIfThenElse(tfd.body.get)
- ))(
- tfd.params.map { p => (p.id, id2sym(p.id): Term) }.toMap
- )
- )
+ val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
+ if (!exploredAll) {
+ reporter.warning(
+ s"Did not manage to explore the space of typed functions called from ${tfd.id}. The solver may fail"
+ )
+ }
+
+ val smtFunDecls = funs.toSeq.collect {
+ case tfd if !functions.containsA(tfd) =>
+ val id = if (tfd.tps.isEmpty) {
+ tfd.id
+ } else {
+ tfd.id.freshen
}
- sendCommand(Assert(term))
- }
+ val sym = id2sym(id)
+ functions +=(tfd, sym)
+ sendCommand(DeclareFun(
+ sym,
+ tfd.params map { p => declareSort(p.getType) },
+ declareSort(tfd.returnType)
+ ))
+ sym
+ }
+ smtFunDecls foreach { sym =>
+ val tfd = functions.toA(sym)
+ val term = quantifiedTerm(
+ SMTForall,
+ tfd.params map { _.id },
+ matchToIfThenElse(Equals(
+ FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
+ matchToIfThenElse(tfd.body.get)
+ ))
+ )
+ sendCommand(Assert(term))
- functions.toB(tfd)
+ tfd.postcondition foreach { post =>
+ val axiom = matchToIfThenElse(implies(
+ tfd.precondition getOrElse BooleanLiteral(true),
+ application(
+ post,
+ Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable }))
+ )
+ ))
+ sendCommand(Assert(quantifiedTerm(SMTForall, axiom)))
+ }
}
+
+ functions.toB(tfd)
}
+
}
--
GitLab