Refactor quantified solvers. smt-z3-q is now sound

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)
   }
 
 }

src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala

+/* 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)
+  }
+
+}

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)
-  }
 
+  }
 
 }

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
+    )
 
   }
 }