From 9e1cc021f2f480daa7f82bcdc4c813319f1852a4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 5 May 2015 11:42:24 +0200
Subject: [PATCH] Last-minute matchToIfThenElse, when not done by templates.
---
.../smtlib/SMTLIBCVC4QuantifiedTarget.scala | 15 +++++++--------
.../scala/leon/solvers/smtlib/SMTLIBTarget.scala | 8 +++++++-
.../solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala | 10 +++++-----
3 files changed, 19 insertions(+), 14 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index b9de2bd61..c6385d426 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -6,9 +6,8 @@ package solvers.smtlib
import purescala.Common.FreshIdentifier
import purescala.Expressions.{FunctionInvocation, BooleanLiteral, Expr, Implies}
import purescala.Definitions.TypedFunDef
-import purescala.Constructors.application
+import purescala.Constructors.{application, implies}
import purescala.DefOps.typedTransitiveCallees
-import leon.purescala.ExprOps.matchToIfThenElse
import smtlib.parser.Commands._
import smtlib.parser.Terms._
import smtlib.theories.Core.Equals
@@ -43,13 +42,13 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target {
functions +=(tfd, id2sym(id))
- val bodyAssert = Assert(Equals(id2sym(id): Term, toSMT(matchToIfThenElse(tfd.body.get))(Map())))
+ val bodyAssert = Assert(Equals(id2sym(id): Term, toSMT(tfd.body.get)(Map())))
val specAssert = tfd.postcondition map { post =>
- val term = matchToIfThenElse(Implies(
+ val term = implies(
tfd.precondition getOrElse BooleanLiteral(true),
application(post, Seq(FunctionInvocation(tfd, Seq())))
- ))
+ )
Assert(toSMT(term)(Map()))
}
@@ -75,7 +74,7 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target {
val smtBodies = smtFunDecls map { case FunDec(sym, _, _) =>
val tfd = functions.toA(sym)
- toSMT(matchToIfThenElse(tfd.body.get))(tfd.params.map { p =>
+ toSMT(tfd.body.get)(tfd.params.map { p =>
(p.id, id2sym(p.id): Term)
}.toMap)
}
@@ -87,10 +86,10 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target {
tfd <- seen
post <- tfd.postcondition
} {
- val term = matchToIfThenElse(Implies(
+ val term = implies(
tfd.precondition getOrElse BooleanLiteral(true),
application(post, Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable})))
- ))
+ )
sendCommand(Assert(quantifiedTerm(ForAll, term)))
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 9c21bc903..fcfe4c801 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -505,6 +505,13 @@ trait SMTLIBTarget {
someTester(vt),
Seq(ArraysEx.Select(toSMT(m), toSMT(k)))
)
+
+ case p : Passes =>
+ toSMT(matchToIfThenElse(p.asConstraint))
+
+ case m : MatchExpr =>
+ toSMT(matchToIfThenElse(m))
+
/**
* ===== Everything else =====
*/
@@ -575,7 +582,6 @@ trait SMTLIBTarget {
case _ => reporter.fatalError("Unhandled nary "+e)
}
-
case o => unsupported("Tree: " + o)
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index 3087d1183..4c40da893 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -50,21 +50,21 @@ trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target {
val term = quantifiedTerm(
SMTForall,
tfd.params map { _.id },
- matchToIfThenElse(Equals(
+ Equals(
FunctionInvocation(tfd, tfd.params.map {_.toVariable}),
- matchToIfThenElse(tfd.body.get)
- ))
+ tfd.body.get
+ )
)
sendCommand(Assert(term))
tfd.postcondition foreach { post =>
- val axiom = matchToIfThenElse(implies(
+ val axiom = implies(
tfd.precondition getOrElse BooleanLiteral(true),
application(
post,
Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable }))
)
- ))
+ )
sendCommand(Assert(quantifiedTerm(SMTForall, axiom)))
}
}
--
GitLab