From 1a51b69168774bf2c41dc767e7536716ef05d4f5 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 2 Apr 2015 13:41:29 +0200
Subject: [PATCH] Function without args should not end up in a define-funs-rec
---
.../smtlib/SMTLIBUnrollingCVC4Target.scala | 24 +++++++++++++++----
.../verification/NewSolversRegression.scala | 12 +++++-----
2 files changed, 25 insertions(+), 11 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
index bfa9c4175..ea6f20d2b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
@@ -3,8 +3,9 @@
package leon
package solvers.smtlib
+import leon.purescala.Common.FreshIdentifier
import leon.purescala.Expressions.Expr
-import purescala.Definitions.TypedFunDef
+import leon.purescala.Definitions.{ValDef, TypedFunDef}
import purescala.DefOps.typedTransitiveCallees
import leon.purescala.ExprOps.{variablesOf, matchToIfThenElse}
import smtlib.parser.Commands._
@@ -23,11 +24,23 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
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"
+ s"Did not manage to explore the space of typed functions trasitively called from ${tfd.id}. The solver may fail"
)
}
- val smtFunDecls = funs.toSeq.collect {
+ val smtFunDecls = funs.toSeq.flatMap {
+ case tfd if tfd.params.isEmpty =>
+ // FIXME: Here we actually want to call super[SMTLIBCVC4Target].declareFunction(tfd),
+ // but we inline it to work around a freakish compiler bug
+ if (!functions.containsA(tfd)) {
+ val id = if (tfd.tps.isEmpty) {
+ tfd.id
+ } else {
+ FreshIdentifier(tfd.id.name)
+ }
+ sendCommand( DeclareFun(id2sym(id),Seq(),declareSort(tfd.returnType)) )
+ }
+ None
case tfd if !functions.containsA(tfd) && tfd.params.nonEmpty =>
val id = if (tfd.tps.isEmpty) {
tfd.id
@@ -36,11 +49,12 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
}
val sym = id2sym(id)
functions +=(tfd, sym)
- FunDec(
+ Some(FunDec(
sym,
tfd.params map { p => SortedVar(id2sym(p.id), declareSort(p.getType)) },
declareSort(tfd.returnType)
- )
+ ))
+ case _ => None
}
val smtBodies = smtFunDecls map { case FunDec(sym, _, _) =>
val tfd = functions.toA(sym)
diff --git a/src/test/scala/leon/test/verification/NewSolversRegression.scala b/src/test/scala/leon/test/verification/NewSolversRegression.scala
index 9013002f8..f73ab1a1a 100644
--- a/src/test/scala/leon/test/verification/NewSolversRegression.scala
+++ b/src/test/scala/leon/test/verification/NewSolversRegression.scala
@@ -30,15 +30,15 @@ class NewSolversRegression extends VerificationRegression {
false
}
- (
- if (isZ3Available)
- List(List("--solvers=smt-z3-quantified", "--feelinglucky", "--timeout=3"))
- else Nil
- ) ++ (
+ //(
+ // if (isZ3Available)
+ //List(List("--solvers=smt-z3-quantified", "--feelinglucky", "--timeout=3"))
+ //else Nil
+ //) ++ (
if (isCVC4Available)
List(List("--solvers=smt-2.5-cvc4", "--feelinglucky"))
else Nil
- )
+ //)
}
test()
--
GitLab