diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 93730b3c4f0c28c0e4c7623b9a999be33d0c4537..fd9085a95c2a20bfaacbd5ea180162bff5244410 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -3,40 +3,30 @@
package leon
package solvers.smtlib
-import leon.purescala.Common.Identifier
import purescala._
import Expressions._
-import ExprOps._
import Definitions._
import Constructors._
import DefOps.typedTransitiveCallees
-import leon.verification.VC
import smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
import smtlib.parser.Terms.{Exists => SMTExists, ForAll => SMTForall, _ }
import smtlib.theories.Core.Equals
// This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
// It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
-abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBCVC4Solver(context, program) {
+abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program)
+ extends SMTLIBCVC4Solver(context, program)
+ with SMTLIBQuantifiedSolver
+{
override def targetName = "cvc4-quantified"
- private var currentFunDef: Option[FunDef] = None
- def refersToCurrent(fd: FunDef) = {
- (currentFunDef contains fd) || (currentFunDef exists {
- program.callGraph.transitivelyCalls(fd, _)
- })
- }
-
- private val typedFunDefExplorationLimit = 10000
-
- protected val allowQuantifiedAssersions: Boolean
-
override def declareFunction(tfd: TypedFunDef): SSymbol = {
val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
if (!exploredAll) {
reporter.warning(
- s"Did not manage to explore the space of typed functions trasitively called from ${tfd.id}. The solver may fail"
+ "Did not manage to explore the space of typed functions " +
+ s"transitively called from ${tfd.id}. The solver may fail"
)
}
@@ -44,6 +34,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
// we declare-fun each one and assert it is equal to its body
val (withParams, withoutParams) = funs.toSeq filterNot functions.containsA partition(_.params.nonEmpty)
+ // FIXME this may introduce dependency errors
val parameterlessAssertions = withoutParams flatMap { tfd =>
val s = super.declareFunction(tfd)
@@ -119,42 +110,6 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
parameterlessAssertions foreach sendCommand
functions.toB(tfd)
-
- }
-
- private def withInductiveHyp(cond: Expr): Expr = {
-
- val inductiveHyps = for {
- fi@FunctionInvocation(tfd, args) <- functionCallsOf(cond).toSeq
- } yield {
- val formalToRealArgs = tfd.params.map{ _.id}.zip(args).toMap
- val post = tfd.postcondition map { post =>
- application(
- replaceFromIDs(formalToRealArgs, post),
- Seq(fi)
- )
- } getOrElse BooleanLiteral(true)
- val pre = tfd.precondition getOrElse BooleanLiteral(true)
- and(pre, post)
- }
-
- // We want to check if the negation of the vc is sat under inductive hyp.
- // So we need to see if (indHyp /\ !vc) is satisfiable
- liftLets(matchToIfThenElse(andJoin(inductiveHyps :+ not(cond))))
-
- }
-
- // We need to know the function context.
- // The reason is we do not want to assume postconditions of functions referring to
- // the current function, as this may make the proof unsound
- override def assertVC(vc: VC) = {
- currentFunDef = Some(vc.fd)
- assertCnstr(withInductiveHyp(vc.condition))
- }
-
- override def getModel: Map[Identifier, Expr] = {
- val filter = currentFunDef.map{ _.params.map{_.id}.toSet }.getOrElse( (_:Identifier) => true )
- getModel(filter)
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
new file mode 100644
index 0000000000000000000000000000000000000000..47a6bed091305e1f9ef1f9a93c2c6154874d9599
--- /dev/null
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
@@ -0,0 +1,62 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.solvers.smtlib
+
+import leon.purescala.Common.Identifier
+import leon.purescala.Constructors._
+import leon.purescala.Definitions.FunDef
+import leon.purescala.ExprOps._
+import leon.purescala.Expressions.{BooleanLiteral, FunctionInvocation, Expr}
+import leon.verification.VC
+
+trait SMTLIBQuantifiedSolver extends SMTLIBSolver {
+
+ private var currentFunDef: Option[FunDef] = None
+ protected def refersToCurrent(fd: FunDef) = {
+ (currentFunDef contains fd) || (currentFunDef exists {
+ program.callGraph.transitivelyCalls(fd, _)
+ })
+ }
+
+ protected val allowQuantifiedAssersions: Boolean
+
+ protected val typedFunDefExplorationLimit = 10000
+
+ protected def withInductiveHyp(cond: Expr): Expr = {
+
+ val inductiveHyps = for {
+ fi@FunctionInvocation(tfd, args) <- functionCallsOf(cond).toSeq
+ } yield {
+ val formalToRealArgs = tfd.params.map{ _.id}.zip(args).toMap
+ val post = tfd.postcondition map { post =>
+ application(
+ replaceFromIDs(formalToRealArgs, post),
+ Seq(fi)
+ )
+ } getOrElse BooleanLiteral(true)
+ val pre = tfd.precondition getOrElse BooleanLiteral(true)
+ and(pre, post)
+ }
+
+ // We want to check if the negation of the vc is sat under inductive hyp.
+ // So we need to see if (indHyp /\ !vc) is satisfiable
+ liftLets(matchToIfThenElse(andJoin(inductiveHyps :+ not(cond))))
+
+ }
+
+ // We need to know the function context.
+ // The reason is we do not want to assume postconditions of functions referring to
+ // the current function, as this may make the proof unsound
+ override def assertVC(vc: VC) = {
+ currentFunDef = Some(vc.fd)
+ assertCnstr(withInductiveHyp(vc.condition))
+ }
+
+ // Normally, UnrollingSolver tracks the input variable, but this one
+ // is invoked alone so we have to filter them here
+ override def getModel: Map[Identifier, Expr] = {
+ val filter = currentFunDef.map{ _.params.map{_.id}.toSet }.getOrElse( (_:Identifier) => true )
+ getModel(filter)
+ }
+
+}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index 7e8dd06733c2846871f8cacfafa9bd10a70ff9a8..bd2f3e05497a3ca3f087c714a5439686d143ee35 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -13,11 +13,14 @@ import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol}
* This solver models function definitions as universally quantified formulas.
* It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
*/
-class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBZ3Solver(context, program) {
+class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program)
+ extends SMTLIBZ3Solver(context, program)
+ with SMTLIBQuantifiedSolver
+{
- private val typedFunDefExplorationLimit = 10000
+ protected val allowQuantifiedAssersions: Boolean = true
- override def targetName = "z3-quantified"
+ override def targetName = "z3-q"
override def declareFunction(tfd: TypedFunDef): SSymbol = {
@@ -28,10 +31,10 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program) extends S
)
}
- val smtFunDecls = funs.toSeq.collect {
- case tfd if !functions.containsA(tfd) =>
- super.declareFunction(tfd)
- }
+ val notSeen = funs.toSeq filterNot functions.containsA
+
+ val smtFunDecls = notSeen map super.declareFunction
+
smtFunDecls foreach { sym =>
val tfd = functions.toA(sym)
val term = quantifiedTerm(
@@ -43,21 +46,28 @@ class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program) extends S
)
)
sendCommand(SMTAssert(term))
+ }
- tfd.postcondition foreach { post =>
- val axiom = implies(
- tfd.precondition getOrElse BooleanLiteral(true),
- application(
- post,
- Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable }))
- )
- )
- sendCommand(SMTAssert(quantifiedTerm(SMTForall, axiom)))
+ // If we encounter a function that does not refer to the current function,
+ // it is sound to assume its contracts for all inputs
+ if (allowQuantifiedAssersions) for {
+ tfd <- notSeen if !refersToCurrent(tfd.fd)
+ post <- tfd.postcondition
+ } {
+ val term = implies(
+ tfd.precondition getOrElse BooleanLiteral(true),
+ application(post, Seq(tfd.applied))
+ )
+ try {
+ sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)))
+ } catch {
+ case _ : IllegalArgumentException =>
+ addError()
}
}
functions.toB(tfd)
- }
+ }
}
diff --git a/src/test/scala/leon/test/verification/NewSolversSuite.scala b/src/test/scala/leon/test/verification/NewSolversSuite.scala
index 4a83e80cfb7dcbbeda1e5b7bd9fa150ba928a70d..93b51d436600bc22f68ab3d0215e2ca6a991e652 100644
--- a/src/test/scala/leon/test/verification/NewSolversSuite.scala
+++ b/src/test/scala/leon/test/verification/NewSolversSuite.scala
@@ -25,9 +25,23 @@ class NewSolversSuite extends VerificationSuite {
false
}
- if (isCVC4Available)
- List(List("--solvers=smt-cvc4-cex,smt-cvc4-proof,ground", "--timeout=5"))
- else Nil
+ val isZ3Available = try {
+ Z3Interpreter.buildDefault.free()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ (
+ if (isCVC4Available)
+ List(List("--solvers=smt-cvc4-cex,smt-cvc4-proof,ground", "--timeout=5"))
+ else Nil
+ ) ++ (
+ if (isZ3Available)
+ List(List("--solvers=smt-z3-q,ground", "--timeout=10"))
+ else Nil
+ )
}
}