From 9806d230f3286aa89496f13fa749e76c46748875 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 19 Jun 2015 17:39:29 +0200
Subject: [PATCH] No forall in cvc4-cex
---
.../leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala | 1 +
.../scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala | 2 ++
.../leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala | 4 +++-
3 files changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index 361806c2d..19bf27741 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
@@ -20,4 +20,5 @@ class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) ext
) ++ userDefinedOps(ctx)
}
+ val allowQuantifiedAssersions: Boolean = false
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index fc4d8a1eb..e02c0dfc9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -54,4 +54,6 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
other
}
}
+
+ protected val allowQuantifiedAssersions: Boolean = true
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 9a949a6d7..70903557b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -29,6 +29,8 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
private val typedFunDefExplorationLimit = 10000
+ protected val allowQuantifiedAssersions: Boolean
+
override def declareFunction(tfd: TypedFunDef): SSymbol = {
val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
if (!exploredAll) {
@@ -94,7 +96,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
if (smtFunDecls.nonEmpty) {
sendCommand(DefineFunsRec(smtFunDecls, smtBodies))
// Assert contracts for defined functions
- for {
+ if (allowQuantifiedAssersions) for {
// If we encounter a function that does not refer to the current function,
// it is sound to assume its contracts for all inputs
tfd <- withParams if !refersToCurrent(tfd.fd)
--
GitLab