diff --git a/.gitignore b/.gitignore
index 057efa0f356af5b6b7af02bd7b0e9e8dcbb7f2b3..4ef5b5eae48b78d3f7dd97318ed2794a9123564f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -54,3 +54,4 @@ out-classes
# Isabelle
contrib
+/bin/
diff --git a/build.sbt b/build.sbt
index d7a5a5e090f1d63706130c0554b4e514c470418a..9215fea007959ffb86d5226f3e5427c58697aa9e 100644
--- a/build.sbt
+++ b/build.sbt
@@ -143,7 +143,7 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi
lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
-lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "204018c3f413fc8191c99ae9ccc4806912e02a83")
+lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "3b6ef4992b6af15d08a7320fd12202f35e97b905")
lazy val root = (project in file(".")).
configs(RegressionTest, IsabelleTest, IntegrTest).
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3a8cb39df090fcb5ca3d3d902bedf6a52557026b..45c62bd0d3a5e82735b98237d2671f485915d13d 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -21,7 +21,7 @@ object Main {
purescala.FunctionClosure,
synthesis.SynthesisPhase,
termination.TerminationPhase,
- verification.AnalysisPhase,
+ verification.VerificationPhase,
repair.RepairPhase,
evaluators.EvaluationPhase,
solvers.isabelle.AdaptationPhase,
@@ -44,15 +44,15 @@ object Main {
val description = "Selection of Leon functionality. Default: verify"
val optEval = LeonStringOptionDef("eval", "Evaluate ground functions through code generation or evaluation (default: evaluation)", "default", "[code|default]")
- val optTermination = LeonFlagOptionDef("termination", "Check program termination. Can be used along --verify", false)
- val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
- val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
- val optIsabelle = LeonFlagOptionDef("isabelle", "Run Isabelle verification", false)
- val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
- val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", false)
- val optHelp = LeonFlagOptionDef("help", "Show help message", false)
- val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
- val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
+ val optTermination = LeonFlagOptionDef("termination", "Check program termination. Can be used along --verify", false)
+ val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
+ val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
+ val optIsabelle = LeonFlagOptionDef("isabelle", "Run Isabelle verification", false)
+ val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
+ val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", false)
+ val optHelp = LeonFlagOptionDef("help", "Show help message", false)
+ val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
+ val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv)
@@ -74,7 +74,7 @@ object Main {
}
reporter.info("")
- reporter.info("Additional options, by component:")
+ reporter.title("Additional options, by component:")
for (c <- (allComponents - MainComponent - SharedOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
reporter.info("")
@@ -147,7 +147,7 @@ object Main {
import synthesis.SynthesisPhase
import termination.TerminationPhase
import xlang.FixReportLabels
- import verification.AnalysisPhase
+ import verification.VerificationPhase
import repair.RepairPhase
import evaluators.EvaluationPhase
import solvers.isabelle.IsabellePhase
@@ -177,19 +177,19 @@ object Main {
ExtractionPhase andThen
new PreprocessingPhase(xlangF)
- val analysis = if (xlangF) AnalysisPhase andThen FixReportLabels else AnalysisPhase
+ val verification = if (xlangF) VerificationPhase andThen FixReportLabels else VerificationPhase
val pipeProcess: Pipeline[Program, Any] = {
if (noopF) RestoreMethods andThen FileOutputPhase
else if (synthesisF) SynthesisPhase
else if (repairF) RepairPhase
- else if (analysisF) Pipeline.both(analysis, TerminationPhase)
+ else if (analysisF) Pipeline.both(verification, TerminationPhase)
else if (terminationF) TerminationPhase
else if (isabelleF) IsabellePhase
else if (evalF) EvaluationPhase
else if (inferInvF) InferInvariantsPhase
else if (instrumentF) InstrumentationPhase andThen FileOutputPhase
- else analysis
+ else verification
}
pipeBegin andThen
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 9e97c6c7bfc097c811d86bc825e5082a9be7c7c1..80f71fd87be7f27e1793e13fe38eb09b78f78d62 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -14,8 +14,6 @@ import purescala.Extractors._
import purescala.Quantification._
import solvers.{Model, HenkinModel}
import solvers.SolverFactory
-import synthesis.ConvertHoles.convertHoles
-import leon.purescala.ExprOps
abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int) extends Evaluator(ctx, prog) {
val name = "evaluator"
@@ -123,11 +121,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case en@Ensuring(body, post) =>
if ( exists{
case Hole(_,_) => true
+ case WithOracle(_,_) => true
case _ => false
- }(en))
- e(convertHoles(en, ctx))
- else
+ }(en)) {
+ import synthesis.ConversionPhase.convert
+ e(convert(en, ctx))
+ } else {
e(en.toAssert)
+ }
case Error(tpe, desc) =>
throw RuntimeError("Error reached in evaluation: " + desc)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 299e8995a072084bba0adf0a98603e64b1611aac..0a75dfebc5ae78d8147d0f601d61d38e2e0c05e2 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -984,11 +984,14 @@ trait CodeExtraction extends ASTExtractors {
val b = extractTreeOrNoTree(body)
- val closure = post.getType match {
- case BooleanType =>
+ val closure = post match {
+ case IsTyped(_, BooleanType) =>
val resId = FreshIdentifier("res", b.getType).setPos(post)
Lambda(Seq(LeonValDef(resId)), post).setPos(post)
- case _ => post
+ case l: Lambda => l
+ case other =>
+ val resId = FreshIdentifier("res", b.getType).setPos(post)
+ Lambda(Seq(LeonValDef(resId)), application(other, Seq(Variable(resId)))).setPos(post)
}
Ensuring(b, closure)
diff --git a/src/main/scala/leon/invariant/datastructure/DisjointSet.scala b/src/main/scala/leon/invariant/datastructure/DisjointSet.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4cab7291bfa58dd3d79993233251d7dd589e0019
--- /dev/null
+++ b/src/main/scala/leon/invariant/datastructure/DisjointSet.scala
@@ -0,0 +1,61 @@
+package leon
+package invariant.datastructure
+
+import scala.collection.mutable.{ Map => MutableMap }
+import scala.annotation.migration
+import scala.collection.mutable.{Map => MutableMap}
+
+class DisjointSets[T] {
+ // A map from elements to their parent and rank
+ private var disjTree = MutableMap[T, (T, Int)]()
+
+ private def findInternal(x: T): (T, Int) = {
+ val (p, rank) = disjTree(x)
+ if (p == x)
+ (x, rank)
+ else {
+ val root = findInternal(p)
+ // compress path
+ disjTree(x) = root
+ root
+ }
+ }
+
+ private def findOrCreateInternal(x: T) =
+ if (!disjTree.contains(x)) {
+ disjTree += (x -> (x, 1))
+ (x, 1)
+ } else findInternal(x)
+
+ def findOrCreate(x: T) = findOrCreateInternal(x)._1
+
+ def find(x: T) = findInternal(x)._1
+
+ def union(x: T, y: T) {
+ val (rep1, rank1) = findOrCreateInternal(x)
+ val (rep2, rank2) = findOrCreateInternal(y)
+ if (rank1 < rank2) {
+ disjTree(rep1) = (rep2, rank2)
+ } else if (rank2 < rank1) {
+ disjTree(rep2) = (rep1, rank1)
+ } else
+ disjTree(rep1) = (rep2, rank2 + 1)
+ }
+
+ def toMap = {
+ val repToSet = disjTree.keys.foldLeft(MutableMap[T, Set[T]]()) {
+ case (acc, k) =>
+ val root = find(k)
+ if (acc.contains(root))
+ acc(root) = acc(root) + k
+ else
+ acc += (root -> Set(k))
+ acc
+ }
+ disjTree.keys.map {k => (k -> repToSet(find(k)))}.toMap
+ }
+
+ override def toString = {
+ disjTree.toString
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/util/Graph.scala b/src/main/scala/leon/invariant/datastructure/Graph.scala
similarity index 99%
rename from src/main/scala/leon/invariant/util/Graph.scala
rename to src/main/scala/leon/invariant/datastructure/Graph.scala
index 22f4e83d12bb96407f37cb548b71482c38376914..484f04668c08a6b02f8acfd2db12b343e4b4c303 100644
--- a/src/main/scala/leon/invariant/util/Graph.scala
+++ b/src/main/scala/leon/invariant/datastructure/Graph.scala
@@ -1,5 +1,5 @@
package leon
-package invariant.util
+package invariant.datastructure
class DirectedGraph[T] {
diff --git a/src/main/scala/leon/invariant/datastructure/Maps.scala b/src/main/scala/leon/invariant/datastructure/Maps.scala
new file mode 100644
index 0000000000000000000000000000000000000000..777a79375d874588f3be108d702aa6dc8118df79
--- /dev/null
+++ b/src/main/scala/leon/invariant/datastructure/Maps.scala
@@ -0,0 +1,117 @@
+package leon
+package invariant.util
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Extractors._
+import purescala.Types._
+import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
+import scala.annotation.tailrec
+
+class MultiMap[A, B] extends scala.collection.mutable.HashMap[A, scala.collection.mutable.Set[B]] with scala.collection.mutable.MultiMap[A, B] {
+ /**
+ * Creates a new map and does not change the existing map
+ */
+ def append(that: MultiMap[A, B]): MultiMap[A, B] = {
+ val newmap = new MultiMap[A, B]()
+ this.foreach { case (k, vset) => newmap += (k -> vset) }
+ that.foreach {
+ case (k, vset) => vset.foreach(v => newmap.addBinding(k, v))
+ }
+ newmap
+ }
+}
+
+/**
+ * A multimap that allows duplicate entries
+ */
+class OrderedMultiMap[A, B] extends scala.collection.mutable.HashMap[A, scala.collection.mutable.ListBuffer[B]] {
+
+ def addBinding(key: A, value: B): this.type = {
+ get(key) match {
+ case None =>
+ val list = new scala.collection.mutable.ListBuffer[B]()
+ list += value
+ this(key) = list
+ case Some(list) =>
+ list += value
+ }
+ this
+ }
+
+ /**
+ * Creates a new map and does not change the existing map
+ */
+ def append(that: OrderedMultiMap[A, B]): OrderedMultiMap[A, B] = {
+ val newmap = new OrderedMultiMap[A, B]()
+ this.foreach { case (k, vlist) => newmap += (k -> vlist) }
+ that.foreach {
+ case (k, vlist) => vlist.foreach(v => newmap.addBinding(k, v))
+ }
+ newmap
+ }
+
+ /**
+ * Make the value of every key distinct
+ */
+ def distinct: OrderedMultiMap[A, B] = {
+ val newmap = new OrderedMultiMap[A, B]()
+ this.foreach { case (k, vlist) => newmap += (k -> vlist.distinct) }
+ newmap
+ }
+}
+
+/**
+ * Implements a mapping from Seq[A] to B where Seq[A]
+ * is stored as a Trie
+ */
+final class TrieMap[A, B] {
+ var childrenMap = Map[A, TrieMap[A, B]]()
+ var dataMap = Map[A, B]()
+
+ @tailrec def addBinding(key: Seq[A], value: B) {
+ key match {
+ case Seq() =>
+ throw new IllegalStateException("Key is empty!!")
+ case Seq(x) =>
+ //add the value to the dataMap
+ if (dataMap.contains(x))
+ throw new IllegalStateException("A mapping for key already exists: " + x + " --> " + dataMap(x))
+ else
+ dataMap += (x -> value)
+ case head +: tail => //here, tail has at least one element
+ //check if we have an entry for seq(0) if yes go to the children, if not create one
+ val child = childrenMap.getOrElse(head, {
+ val ch = new TrieMap[A, B]()
+ childrenMap += (head -> ch)
+ ch
+ })
+ child.addBinding(tail, value)
+ }
+ }
+
+ @tailrec def lookup(key: Seq[A]): Option[B] = {
+ key match {
+ case Seq() =>
+ throw new IllegalStateException("Key is empty!!")
+ case Seq(x) =>
+ dataMap.get(x)
+ case head +: tail => //here, tail has at least one element
+ childrenMap.get(head) match {
+ case Some(child) =>
+ child.lookup(tail)
+ case _ => None
+ }
+ }
+ }
+}
+
+class CounterMap[T] extends scala.collection.mutable.HashMap[T, Int] {
+ def inc(v: T) = {
+ if (this.contains(v))
+ this(v) += 1
+ else this += (v -> 1)
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala b/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
index 4c443b3f6e08b7cf381b661a1725862156c1bba6..647616fce1bab0eb01182ad50d75c060ce4ff737 100644
--- a/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
@@ -8,20 +8,21 @@ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
import invariant.templateSolvers._
-import invariant.util.Util._
import transformations._
import invariant.structure.FunctionUtils._
import transformations.InstUtil._
import leon.invariant.structure.Formula
import leon.invariant.structure.Call
-import leon.invariant.util.RealToInt
-import leon.invariant.util.OrderedMultiMap
-import leon.invariant.util.ExpressionTransformer
+import leon.invariant.util._
import leon.invariant.factories.TemplateSolverFactory
import leon.invariant.util.Minimizer
import leon.solvers.Model
+import Util._
+import PredicateUtil._
+import ProgramUtil._
+import SolverUtil._
-class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
+class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd: FunDef)
extends FunctionTemplateSolver {
val printIntermediatePrograms = false
@@ -30,7 +31,7 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
val reporter = ctx.reporter
def inferTemplate(instProg: Program) = {
- (new UnfoldingTemplateSolver(ctx.copy(program = instProg), findRoot(instProg)))()
+ (new UnfoldingTemplateSolver(ctx, instProg, findRoot(instProg)))()
}
def findRoot(prog: Program) = {
@@ -45,7 +46,7 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
throw new IllegalStateException("Templates for tpr, rec, time as well as all other templates " +
" taken together should not have the any common template variables for compositional analysis")
- val origProg = ctx.program
+ val origProg = prog
// add only rec templates for all functions
val funToRecTmpl = origProg.definedFunctions.collect {
case fd if fd.hasTemplate && fd == rootFd =>
@@ -81,7 +82,7 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
}.toMap
val compProg = assignTemplateAndCojoinPost(funToTmpl, origProg)
val compFunDef = findRoot(compProg)
- val nctx = ctx.copy(program = compProg)
+ //val nctx = ctx.copy(program = compProg)
// construct the instantiated tpr bound and check if it monotonically decreases
val Operator(Seq(_, tprFun), _) = tprTmpl
@@ -118,13 +119,13 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
if (printIntermediatePrograms) reporter.info("Comp prog: " + compProg)
if (debugComposition) reporter.info("Compositional VC: " + vcExpr)
- val recTempSolver = new UnfoldingTemplateSolver(nctx, compFunDef) {
+ val recTempSolver = new UnfoldingTemplateSolver(ctx, compProg, compFunDef) {
val minFunc = {
- val mizer = new Minimizer(ctx)
+ val mizer = new Minimizer(ctx, compProg)
Some(mizer.minimizeBounds(mizer.computeCompositionLevel(timeTmpl)) _)
}
override lazy val templateSolver =
- TemplateSolverFactory.createTemplateSolver(ctx, constTracker, rootFd, minFunc)
+ TemplateSolverFactory.createTemplateSolver(ctx, compProg, constTracker, rootFd, minFunc)
override def instantiateModel(model: Model, funcs: Seq[FunDef]) = {
funcs.collect {
case `compFunDef` =>
@@ -148,12 +149,12 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
}
}
- def combineMapsUsingConjunction(maps: List[Map[FunDef, Expr]]) = {
+ /*def combineMapsUsingConjunction(maps: List[Map[FunDef, Expr]], prog: Program) = {
val combMap = new OrderedMultiMap[FunDef, Expr]
maps.foreach {
_.foreach {
case (k, v) =>
- val origFun = functionByName(k.id.name, ctx.program).get
+ val origFun = functionByName(k.id.name, prog).get
combMap.addBinding(origFun, v)
}
}
@@ -161,7 +162,7 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
case (acc, (k, vs)) if vs.size == 1 => acc + (k -> vs(0))
case (acc, (k, vs)) => acc + (k -> And(vs.toSeq))
}
- }
+ }*/
def extractSeparateTemplates(funDef: FunDef): (Option[Expr], Option[Expr], Option[Expr], Seq[Expr]) = {
if (!funDef.hasTemplate) (None, None, None, Seq[Expr]())
@@ -204,7 +205,7 @@ class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
}
def inferTPRTemplate(tprProg: Program) = {
- val tempSolver = new UnfoldingTemplateSolver(ctx.copy(program = tprProg), findRoot(tprProg)) {
+ val tempSolver = new UnfoldingTemplateSolver(ctx, tprProg, findRoot(tprProg)) {
override def constructVC(rootFd: FunDef): (Expr, Expr) = {
val body = Equals(getResId(rootFd).get.toVariable, matchToIfThenElse(rootFd.body.get))
val preExpr =
diff --git a/src/main/scala/leon/invariant/engine/ConstraintTracker.scala b/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
index e50b50bb8b84886bff46c54641f55050fc5f5e52..3058a267eceef7c5ec1aa537c4766bee15a93204 100644
--- a/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
+++ b/src/main/scala/leon/invariant/engine/ConstraintTracker.scala
@@ -16,13 +16,13 @@ import invariant.factories._
import invariant.util._
import invariant.structure._
-class ConstraintTracker(ctx : InferenceContext, rootFun : FunDef/*, temFactory: TemplateFactory*/) {
+class ConstraintTracker(ctx : InferenceContext, program: Program, rootFun : FunDef/*, temFactory: TemplateFactory*/) {
//a mapping from functions to its VCs represented as a CNF formula
protected var funcVCs = Map[FunDef,Formula]()
- val vcRefiner = new RefinementEngine(ctx, this/*, temFactory*/)
- val specInstantiator = new SpecInstantiator(ctx, this/*, temFactory*/)
+ val vcRefiner = new RefinementEngine(ctx, program, this)
+ val specInstantiator = new SpecInstantiator(ctx, program, this)
def getFuncs : Seq[FunDef] = funcVCs.keys.toSeq
def hasVC(fdef: FunDef) = funcVCs.contains(fdef)
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index ce69f2b6f755279d333471bacf9aa0579013defd..eca69f0c0f0246dae7840ae9b6511f841fcc90d2 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -14,21 +14,17 @@ import invariant.util._
import invariant.structure.FunctionUtils._
import invariant.structure._
import transformations._
-import verification._
-import verification.VCKinds
import leon.purescala.ScalaPrinter
import leon.purescala.PrettyPrinter
/**
* @author ravi
* This phase performs automatic invariant inference.
- * TODO: should time be implicitly made positive
*/
object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
val name = "InferInv"
val description = "Invariant Inference"
- val optWholeProgram = LeonFlagOptionDef("wholeprogram", "Perform an non-modular whole program analysis", false)
val optFunctionUnroll = LeonFlagOptionDef("fullunroll", "Unroll all calls in every unroll step", false)
val optWithMult = LeonFlagOptionDef("withmult", "Multiplication is not converted to a recursive function in VCs", false)
val optUseReals = LeonFlagOptionDef("usereals", "Interpret the input program as a real program", false)
@@ -36,121 +32,18 @@ object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
val optInferTemp = LeonFlagOptionDef("inferTemp", "Infer templates by enumeration", false)
val optCegis = LeonFlagOptionDef("cegis", "use cegis instead of farkas", false)
val optStatsSuffix = LeonStringOptionDef("stats-suffix", "the suffix of the statistics file", "", "s")
- val optTimeout = LeonLongOptionDef("timeout", "Timeout after T seconds when trying to prove a verification condition.", 20, "s")
+ val optVCTimeout = LeonLongOptionDef("vcTimeout", "Timeout after T seconds when trying to prove a verification condition", 20, "s")
val optDisableInfer = LeonFlagOptionDef("disableInfer", "Disable automatic inference of auxiliary invariants", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optWholeProgram, optFunctionUnroll, optWithMult, optUseReals,
- optMinBounds, optInferTemp, optCegis, optStatsSuffix, optTimeout,
+ Set(optFunctionUnroll, optWithMult, optUseReals,
+ optMinBounds, optInferTemp, optCegis, optStatsSuffix, optVCTimeout,
optDisableInfer)
- //TODO provide options for analyzing only selected functions
def apply(ctx: LeonContext, program: Program): InferenceReport = {
-
- //control printing of statistics
- val dumpStats = false
- var timeout: Int = 15
-
- //defualt true flags
- var modularlyAnalyze = true
- var targettedUnroll = true
-
- //default false flags
- var tightBounds = false
- var withmult = false
- var inferTemp = false
- var enumerationRelation: (Expr, Expr) => Expr = LessEquals
- var useCegis = false
- //var maxCegisBound = 200 //maximum bound for the constants in cegis
- var maxCegisBound = 1000000000
- var statsSuff = "-stats" + FileCountGUID.getID
- var usereals = false
- var autoInference = true
-
- for (opt <- ctx.options) (opt.optionDef.name, opt.value) match {
- case ("wholeprogram", true) =>
- modularlyAnalyze = false
- case ("fullunroll", true) =>
- targettedUnroll = false
- case ("minbounds", true) =>
- tightBounds = true
- case ("withmult", true) =>
- withmult = true
- case ("usereals", true) =>
- usereals = true
- case ("disableInfer", true) =>
- autoInference = false
- case ("inferTemp", true) =>
- inferTemp = true
- case ("cegis", true) =>
- useCegis = true
- case ("timeout", timeOut: Int) =>
- timeout = timeOut
- case ("stats-suffix", suffix: String) =>
- statsSuff = suffix
- case _ =>
- }
-
- // (a) first run instrumentation phase
- val instProg = InstrumentationPhase(ctx, program)
-
- // (b) convert qmarks to tmpl functions
- val funToTmpl = instProg.definedFunctions.collect {
- case fd if fd.hasTemplate =>
- fd -> fd.getTemplate
- }.toMap
- val qMarksRemovedProg = Util.assignTemplateAndCojoinPost(funToTmpl, instProg, Map())
-
- // convert nonlinearity to recursive functions
- val newprog = if (usereals) {
- (new IntToRealProgram())(qMarksRemovedProg)
- } else qMarksRemovedProg
- val nlelim = new NonlinearityEliminator(withmult, if (usereals) RealType else IntegerType)
- val finalprog = nlelim(newprog)
-
- val toVerifyPost = validateAndCollectNotValidated(qMarksRemovedProg, ctx, timeout)
-
- // collect strongest relation for enumeration if defined
- var foundStrongest = false
- //go over all post-conditions and pick the strongest relation
- instProg.definedFunctions.foreach((fd) => {
- if (!foundStrongest && fd.hasPostcondition) {
- val cond = fd.postcondition.get
- simplePostTransform((e) => e match {
- case Equals(_, _) => {
- enumerationRelation = Equals.apply _
- foundStrongest = true
- e
- }
- case _ => e
- })(cond)
- }
- })
-
- //populate the inference context and invoke inferenceEngine
- val inferctx = new InferenceContext(program, finalprog, toVerifyPost, ctx,
- //multiplication operation
- (e1, e2) => FunctionInvocation(TypedFunDef(nlelim.multFun, nlelim.multFun.tparams.map(_.tp)), Seq(e1, e2)),
- enumerationRelation = LessEquals, modularlyAnalyze, targettedUnroll, autoInference,
- dumpStats, tightBounds, withmult, usereals, inferTemp, useCegis, timeout, maxCegisBound, statsSuff)
- val report = (new InferenceEngine(inferctx)).run()
+ val inferctx = new InferenceContext(program, ctx)
+ val report = (new InferenceEngine(inferctx)).runWithTimeout()
//println("Final Program: \n" +PrettyPrinter.apply(report.finalProgramWoInstrumentation))
report
}
-
- def createLeonContext(ctx: LeonContext, opts: String*): LeonContext = {
- Main.processOptions(opts.toList).copy(reporter = ctx.reporter,
- interruptManager = ctx.interruptManager, files = ctx.files, timers = ctx.timers)
- }
-
- def validateAndCollectNotValidated(prog: Program, ctx: LeonContext, timeout: Int): Set[String] = {
- val verifyPipe = AnalysisPhase
- val ctxWithTO = createLeonContext(ctx, "--timeout=" + timeout)
- (verifyPipe.run(ctxWithTO, prog)._2).results.collect{
- case (VC(_, fd, VCKinds.Postcondition), Some(vcRes)) if vcRes.isInconclusive =>
- fd.id.name
- case (VC(_, fd, vcKind), Some(vcRes)) if vcRes.isInvalid =>
- throw new IllegalStateException("Invalid" + vcKind + " for function " + fd.id.name)
- }.toSet
- }
}
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index bf3d83845b3fcb9b2ecbd3fe108186655dbc26b2..b735cb8de7101f3bf109c6318cc7a05c571ba4b7 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -1,32 +1,116 @@
package leon
package invariant.engine
+import scala.collection.mutable.{ Map => MutableMap }
import purescala.Definitions._
import purescala.Expressions._
-import purescala._
+import purescala.Types._
+import purescala.ExprOps._
+import transformations._
+import invariant.structure.FunctionUtils._
+import invariant.util._
+import verification._
+import verification.VCKinds
+import InferInvariantsPhase._
+import Util._
+import ProgramUtil._
/**
* @author ravi
*/
-case class InferenceContext(
- val uninstrumentedProgram : Program,
- val program : Program,
- val toVerifyPostFor: Set[String],
- val leonContext : LeonContext,
- val multOp: (Expr,Expr) => Expr,
- val enumerationRelation : (Expr,Expr) => Expr,
- val modularlyAnalyze : Boolean,
- val targettedUnroll : Boolean,
- val autoInference : Boolean,
- val dumpStats : Boolean ,
- val tightBounds : Boolean,
- val withmult : Boolean,
- val usereals : Boolean,
- val inferTemp : Boolean,
- val useCegis : Boolean,
- val timeout: Int, //in secs
- val maxCegisBound : Int,
- val statsSuffix : String) {
+class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
+ var abort = false // a flag for aborting
+
+ // get options from ctx or initialize them to default values
+ // the following options are enabled by default
+ val targettedUnroll = !(leonContext.findOption(optFunctionUnroll).getOrElse(false))
+ val autoInference = leonContext.findOption(optDisableInfer).getOrElse(true)
+
+ // the following options are disabled by default
+ val tightBounds = leonContext.findOption(optMinBounds).getOrElse(false)
+ val inferTemp = leonContext.findOption(optInferTemp).getOrElse(false)
+ val withmult = leonContext.findOption(optWithMult).getOrElse(false)
+ val usereals = leonContext.findOption(optUseReals).getOrElse(false)
+ val useCegis: Boolean = leonContext.findOption(optCegis).getOrElse(false)
+ val dumpStats = false
+
+ // the following options have default values
+ val vcTimeout = leonContext.findOption(optVCTimeout).getOrElse(15L) // in secs
+ val totalTimeout = leonContext.findOption(SharedOptions.optTimeout) // in secs
+ val functionsToInfer = leonContext.findOption(SharedOptions.optFunctions)
val reporter = leonContext.reporter
+ val maxCegisBound = 1000
+ val statsSuffix = leonContext.findOption(optStatsSuffix).getOrElse("-stats" + FileCountGUID.getID)
+
+ val instrumentedProg = InstrumentationPhase(leonContext, initProgram)
+ // convets qmarks to templates
+ val qMarksRemovedProg = {
+ val funToTmpl = instrumentedProg.definedFunctions.collect {
+ case fd if fd.hasTemplate =>
+ fd -> fd.getTemplate
+ }.toMap
+ assignTemplateAndCojoinPost(funToTmpl, instrumentedProg, Map())
+ }
+
+ val nlelim = new NonlinearityEliminator(withmult, if (usereals) RealType else IntegerType)
+
+ val inferProgram = {
+ // convert nonlinearity to recursive functions
+ nlelim(if (usereals)
+ (new IntToRealProgram())(qMarksRemovedProg)
+ else qMarksRemovedProg)
+ }
+
+ // other utilities
+ lazy val enumerationRelation = {
+ // collect strongest relation for enumeration if defined
+ var foundStrongest = false
+ var rel: (Expr, Expr) => Expr = LessEquals.apply _
+ //go over all post-conditions and pick the strongest relation
+ instrumentedProg.definedFunctions.foreach((fd) => {
+ if (!foundStrongest && fd.hasPostcondition) {
+ val cond = fd.postcondition.get
+ postTraversal((e) => e match {
+ case Equals(_, _) => {
+ rel = Equals.apply _
+ foundStrongest = true
+ }
+ case _ => ;
+ })(cond)
+ }
+ })
+ rel
+ }
+
+ def multOp(e1: Expr, e2: Expr) = {
+ FunctionInvocation(TypedFunDef(nlelim.multFun, nlelim.multFun.tparams.map(_.tp)), Seq(e1, e2))
+ }
+
+ val validPosts = MutableMap[String, VCResult]()
+
+ /**
+ * There should be only one function with funName in the
+ * program
+ */
+ def isFunctionPostVerified(funName: String) = {
+ if (validPosts.contains(funName)) {
+ validPosts(funName).isValid
+ } else {
+ val verifyPipe = VerificationPhase
+ val ctxWithTO = createLeonContext(leonContext, s"--timeout=$vcTimeout", s"--functions=$funName")
+ (true /: verifyPipe.run(ctxWithTO, qMarksRemovedProg)._2.results) {
+ case (acc, (VC(_, _, vckind), Some(vcRes))) if vcRes.isInvalid =>
+ throw new IllegalStateException(s"$vckind invalid for function $funName") // TODO: remove the exception
+ case (acc, (VC(_, _, VCKinds.Postcondition), None)) =>
+ throw new IllegalStateException(s"Postcondition verification returned unknown for function $funName") // TODO: remove the exception
+ case (acc, (VC(_, _, VCKinds.Postcondition), _)) if validPosts.contains(funName) =>
+ throw new IllegalStateException(s"Multiple postcondition VCs for function $funName") // TODO: remove the exception
+ case (acc, (VC(_, _, VCKinds.Postcondition), Some(vcRes))) =>
+ validPosts(funName) = vcRes
+ vcRes.isValid
+ case (acc, _) => acc
+ }
+ }
+ }
}
diff --git a/src/main/scala/leon/invariant/engine/InferenceEngine.scala b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
index 03202f9dbb3a300a8eca4c2454b295e924dfd1b3..85491acf1924560e5fe020a38176b513da989690 100644
--- a/src/main/scala/leon/invariant/engine/InferenceEngine.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
@@ -20,17 +20,45 @@ import invariant.util.Util._
import invariant.structure._
import invariant.structure.FunctionUtils._
import leon.invariant.factories.TemplateFactory
+import transformations._
+import leon.utils._
+import Util._
+import PredicateUtil._
+import ProgramUtil._
+import SolverUtil._
/**
* @author ravi
* This phase performs automatic invariant inference.
* TODO: should time be implicitly made positive
*/
-class InferenceEngine(ctx: InferenceContext) {
+class InferenceEngine(ctx: InferenceContext) extends Interruptible {
- def run(): InferenceReport = {
+ val ti = new TimeoutFor(this)
+
+ def interrupt() = {
+ ctx.abort = true
+ ctx.leonContext.interruptManager.interrupt()
+ }
+
+ def recoverInterrupt() = {
+ ctx.abort = false
+ }
+
+ def runWithTimeout(progressCallback: Option[InferenceCondition => Unit] = None) = {
+ ctx.totalTimeout match {
+ case Some(t) => // timeout in secs
+ ti.interruptAfter(t * 1000) {
+ run(progressCallback)
+ }
+ case None =>
+ run(progressCallback)
+ }
+ }
+
+ private def run(progressCallback: Option[InferenceCondition => Unit] = None): InferenceReport = {
val reporter = ctx.reporter
- val program = ctx.program
+ val program = ctx.inferProgram
reporter.info("Running Inference Engine...")
//register a shutdownhook
@@ -40,15 +68,19 @@ class InferenceEngine(ctx: InferenceContext) {
val t1 = System.currentTimeMillis()
//compute functions to analyze by sorting based on topological order (this is an ascending topological order)
val callgraph = CallGraphUtil.constructCallGraph(program, withTemplates = true)
- val functionsToAnalyze = if (ctx.modularlyAnalyze) {
- callgraph.topologicalOrder
- } else {
- callgraph.topologicalOrder.reverse
+ val functionsToAnalyze = ctx.functionsToInfer match {
+ case Some(rootfuns) =>
+ val rootset = rootfuns.toSet
+ val rootfds = program.definedFunctions.filter(fd => rootset(InstUtil.userFunctionName(fd)))
+ val relfuns = rootfds.flatMap(callgraph.transitiveCallees _).toSet
+ callgraph.topologicalOrder.filter { fd => relfuns(fd) }
+ case _ =>
+ callgraph.topologicalOrder
}
//reporter.info("Analysis Order: " + functionsToAnalyze.map(_.id))
var results: Map[FunDef, InferenceCondition] = null
if (!ctx.useCegis) {
- results = analyseProgram(functionsToAnalyze)
+ results = analyseProgram(program, functionsToAnalyze, progressCallback)
//println("Inferrence did not succeeded for functions: "+functionsToAnalyze.filterNot(succeededFuncs.contains _).map(_.id))
} else {
var remFuncs = functionsToAnalyze
@@ -57,7 +89,7 @@ class InferenceEngine(ctx: InferenceContext) {
breakable {
while (b <= maxCegisBound) {
Stats.updateCumStats(1, "CegisBoundsTried")
- val succeededFuncs = analyseProgram(remFuncs)
+ val succeededFuncs = analyseProgram(program, remFuncs, progressCallback)
remFuncs = remFuncs.filterNot(succeededFuncs.contains _)
if (remFuncs.isEmpty) break;
b += 5 //increase bounds in steps of 5
@@ -75,12 +107,12 @@ class InferenceEngine(ctx: InferenceContext) {
new InferenceReport(results.map(pair => {
val (fd, ic) = pair
(fd -> List[VC](ic))
- }))(ctx)
+ }), program)(ctx)
}
def dumpStats(statsSuffix: String) = {
//pick the module id.
- val modid = ctx.program.modules.last.id
+ val modid = ctx.inferProgram.modules.last.id
val pw = new PrintWriter(modid + statsSuffix + ".txt")
Stats.dumpStats(pw)
SpecificStats.dumpOutputs(pw)
@@ -94,85 +126,111 @@ class InferenceEngine(ctx: InferenceContext) {
* TODO: use function names in inference conditions, so that
* we an get rid of dependence on origFd in many places.
*/
- def analyseProgram(functionsToAnalyze: Seq[FunDef]): Map[FunDef, InferenceCondition] = {
+ def analyseProgram(startProg: Program, functionsToAnalyze: Seq[FunDef],
+ progressCallback: Option[InferenceCondition => Unit]): Map[FunDef, InferenceCondition] = {
val reporter = ctx.reporter
val funToTmpl =
if (ctx.autoInference) {
//A template generator that generates templates for the functions (here we are generating templates by enumeration)
- val tempFactory = new TemplateFactory(Some(new TemplateEnumerator(ctx)), ctx.program, ctx.reporter)
- ctx.program.definedFunctions.map(fd => fd -> getOrCreateTemplateForFun(fd)).toMap
+ // not usef for now
+ /*val tempFactory = new TemplateFactory(Some(new TemplateEnumerator(ctx, startProg)),
+ startProg, ctx.reporter)*/
+ startProg.definedFunctions.map(fd => fd -> getOrCreateTemplateForFun(fd)).toMap
} else
- ctx.program.definedFunctions.collect { case fd if fd.hasTemplate => fd -> fd.getTemplate }.toMap
- val progWithTemplates = assignTemplateAndCojoinPost(funToTmpl, ctx.program)
+ startProg.definedFunctions.collect { case fd if fd.hasTemplate => fd -> fd.getTemplate }.toMap
+ val progWithTemplates = assignTemplateAndCojoinPost(funToTmpl, startProg)
var analyzedSet = Map[FunDef, InferenceCondition]()
+
functionsToAnalyze.filterNot((fd) => {
(fd.annotations contains "verified") ||
(fd.annotations contains "library") ||
(fd.annotations contains "theoryop")
}).foldLeft(progWithTemplates) { (prog, origFun) =>
- val funDef = functionByName(origFun.id.name, prog).get
- reporter.info("- considering function " + funDef.id.name + "...")
-
- //skip the function if it has been analyzed
- if (!analyzedSet.contains(origFun)) {
- if (funDef.hasBody && funDef.hasPostcondition) {
- val currCtx = ctx.copy(program = prog)
- // for stats
- Stats.updateCounter(1, "procs")
- val solver =
- if (funDef.annotations.contains("compose")) //compositional inference ?
- new CompositionalTimeBoundSolver(currCtx, funDef)
- else
- new UnfoldingTemplateSolver(currCtx, funDef)
- val t1 = System.currentTimeMillis()
- val infRes = solver()
- val funcTime = (System.currentTimeMillis() - t1) / 1000.0
- infRes match {
- case Some(InferResult(true, model, inferredFuns)) =>
- val funsWithTemplates = inferredFuns.filter { fd =>
- val origFd = Util.functionByName(fd.id.name, ctx.program).get
- !analyzedSet.contains(origFd) && origFd.hasTemplate
- }
- // create a inference condition for reporting
- var first = true
- funsWithTemplates.foreach { fd =>
- val origFd = Util.functionByName(fd.id.name, ctx.program).get
- val inv = TemplateInstantiator.getAllInvariants(model.get,
- Map(origFd -> origFd.getTemplate))
- // record the inferred invariants
- val ic = new InferenceCondition(Some(inv(origFd)), origFd)
- ic.time = if (first) Some(funcTime) else Some(0.0)
- // update analyzed set
- analyzedSet += (origFd -> ic)
- first = false
- }
- val invs = TemplateInstantiator.getAllInvariants(model.get,
- funsWithTemplates.collect {
- case fd if fd.hasTemplate => fd -> fd.getTemplate
- }.toMap)
- if (ctx.modularlyAnalyze) {
+ if (ctx.abort) {
+ reporter.info("- Aborting analysis of " + origFun.id.name)
+ val ic = new InferenceCondition(Seq(), origFun)
+ ic.time = Some(0)
+ prog
+ } else if (origFun.getPostWoTemplate == tru && !origFun.hasTemplate) {
+ reporter.info("- Nothing to solve for " + origFun.id.name)
+ prog
+ } else {
+ val funDef = functionByName(origFun.id.name, prog).get
+ reporter.info("- considering function " + funDef.id.name + "...")
+ //skip the function if it has been analyzed
+ if (!analyzedSet.contains(origFun)) {
+ if (funDef.hasBody && funDef.hasPostcondition) {
+ // for stats
+ Stats.updateCounter(1, "procs")
+ val solver =
+ if (funDef.annotations.contains("compose")) //compositional inference ?
+ new CompositionalTimeBoundSolver(ctx, prog, funDef)
+ else
+ new UnfoldingTemplateSolver(ctx, prog, funDef)
+ val t1 = System.currentTimeMillis()
+ val infRes = solver()
+ val funcTime = (System.currentTimeMillis() - t1) / 1000.0
+ infRes match {
+ case Some(InferResult(true, model, inferredFuns)) =>
+ // create a inference condition for reporting
+ var first = true
+ inferredFuns.foreach { fd =>
+ val origFd = functionByName(fd.id.name, startProg).get
+ val inv = if (origFd.hasTemplate) {
+ TemplateInstantiator.getAllInvariants(model.get,
+ Map(origFd -> origFd.getTemplate), prettyInv = true)(origFd)
+ } else {
+ val currentInv = TemplateInstantiator.getAllInvariants(model.get,
+ Map(fd -> fd.getTemplate), prettyInv = true)(fd)
+ // map result variable in currentInv
+ val repInv = replace(Map(getResId(fd).get.toVariable -> getResId(origFd).get.toVariable), currentInv)
+ translateExprToProgram(repInv, prog, startProg)
+ }
+ // record the inferred invariants
+ val inferCond = if (analyzedSet.contains(origFd)) {
+ val ic = analyzedSet(origFd)
+ ic.addInv(Seq(inv))
+ ic
+ } else {
+ val ic = new InferenceCondition(Seq(inv), origFd)
+ ic.time = if (first) Some(funcTime) else Some(0.0)
+ // update analyzed set
+ analyzedSet += (origFd -> ic)
+ first = false
+ ic
+ }
+ progressCallback.map(cb => cb(inferCond))
+ }
+ val funsWithTemplates = inferredFuns.filter { fd =>
+ val origFd = functionByName(fd.id.name, startProg).get
+ !analyzedSet.contains(origFd) && origFd.hasTemplate
+ }
+ val invs = TemplateInstantiator.getAllInvariants(model.get,
+ funsWithTemplates.collect {
+ case fd if fd.hasTemplate => fd -> fd.getTemplate
+ }.toMap)
// create a new program that has the inferred templates
val funToTmpl = prog.definedFunctions.collect {
case fd if !invs.contains(fd) && fd.hasTemplate =>
fd -> fd.getTemplate
}.toMap
assignTemplateAndCojoinPost(funToTmpl, prog, invs)
- } else
+
+ case _ =>
+ reporter.info("- Exhausted all templates, cannot infer invariants")
+ val ic = new InferenceCondition(Seq(), origFun)
+ ic.time = Some(funcTime)
+ analyzedSet += (origFun -> ic)
prog
- case _ =>
- reporter.info("- Exhausted all templates, cannot infer invariants")
- val ic = new InferenceCondition(None, origFun)
- ic.time = Some(funcTime)
- analyzedSet += (origFun -> ic)
- prog
+ }
+ } else {
+ //nothing needs to be done here
+ reporter.info("Function does not have a body or postcondition")
+ prog
}
- } else {
- //nothing needs to be done here
- reporter.info("Function does not have a body or postcondition")
- prog
- }
- } else prog
+ } else prog
+ }
}
analyzedSet
}
diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala
index 26337c6fff8111ba59f11dfd25213ee61610ac8b..39af145c31bd5a7253475a5cebe047fca4e932b3 100644
--- a/src/main/scala/leon/invariant/engine/InferenceReport.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala
@@ -15,13 +15,33 @@ import invariant.util._
import invariant.structure._
import leon.transformations.InstUtil
import leon.purescala.PrettyPrinter
+import Util._
+import PredicateUtil._
+import ProgramUtil._
+import SolverUtil._
+import FunctionUtils._
+import purescala._
-class InferenceCondition(val invariant: Option[Expr], funDef: FunDef)
- extends VC(BooleanLiteral(true), funDef, null) {
+class InferenceCondition(invs: Seq[Expr], funDef: FunDef)
+ extends VC(BooleanLiteral(true), funDef, null) {
var time: Option[Double] = None
- lazy val prettyInv = invariant.map(inv =>
- simplifyArithmetic(InstUtil.replaceInstruVars(Util.multToTimes(inv), fd)))
+ var invariants = invs
+
+ def addInv(invs: Seq[Expr]) {
+ invariants ++= invs
+ }
+
+ lazy val prettyInv = invariants.map(inv =>
+ simplifyArithmetic(InstUtil.replaceInstruVars(multToTimes(inv), fd))) match {
+ case Seq() => None
+ case invs =>
+ invs.map(ExpressionTransformer.simplify _).filter(_ != tru) match {
+ case Seq() => Some(tru)
+ case Seq(ninv) => Some(ninv)
+ case ninvs => Some(And(ninvs))
+ }
+ }
def status: String = prettyInv match {
case None => "unknown"
@@ -30,8 +50,8 @@ class InferenceCondition(val invariant: Option[Expr], funDef: FunDef)
}
}
-class InferenceReport(fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContext)
- extends VerificationReport(ctx.program, Map()) {
+class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ctx: InferenceContext)
+ extends VerificationReport(program, Map()) {
import scala.math.Ordering.Implicits._
val conditions: Seq[InferenceCondition] =
@@ -65,7 +85,7 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContex
})
val summaryStr = {
val totalTime = conditions.foldLeft(0.0)((a, ic) => a + ic.time.getOrElse(0.0))
- val inferredConds = conditions.count((ic) => ic.invariant.isDefined)
+ val inferredConds = conditions.count((ic) => ic.prettyInv.isDefined)
"total: %-4d inferred: %-4d unknown: %-4d time: %-3.3f".format(
conditions.size, inferredConds, conditions.size - inferredConds, totalTime)
}
@@ -83,29 +103,151 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContex
def finalProgram: Program = {
val funToTmpl = conditions.collect {
- case cd if cd.invariant.isDefined =>
- cd.fd -> cd.invariant.get
+ case cd if cd.prettyInv.isDefined =>
+ cd.fd -> cd.prettyInv.get
}.toMap
- Util.assignTemplateAndCojoinPost(funToTmpl, ctx.program)
+ assignTemplateAndCojoinPost(funToTmpl, program)
}
+}
- def finalProgramWoInstrumentation: Program = {
+object InferenceReportUtil {
- val funToUninstFun = ctx.program.definedFunctions.foldLeft(Map[FunDef, FunDef]()) {
+ /* def programWoInstrumentation(ctx: InferenceContext, p: Program, ics: Seq[InferenceCondition]) = {
+ val funToUninstFun = p.definedFunctions.foldLeft(Map[FunDef, FunDef]()) {
case (acc, fd) =>
val uninstFunName = InstUtil.userFunctionName(fd)
val uninstFdOpt =
if (uninstFunName.isEmpty) None
- else Util.functionByName(uninstFunName, ctx.uninstrumentedProgram)
+ else functionByName(uninstFunName, ctx.initProgram)
if (uninstFdOpt.isDefined) {
acc + (fd -> uninstFdOpt.get)
} else acc
}
- val funToPost = conditions.collect {
- case cd if cd.invariant.isDefined && funToUninstFun.contains(cd.fd) =>
+ val funToPost = ics.collect {
+ case cd if cd.prettyInv.isDefined && funToUninstFun.contains(cd.fd) =>
funToUninstFun(cd.fd) -> cd.prettyInv.get
}.toMap
//println("Function to template: " + funToTmpl.map { case (k, v) => s"${k.id.name} --> $v" }.mkString("\n"))
- Util.assignTemplateAndCojoinPost(Map(), ctx.uninstrumentedProgram, funToPost, uniqueIdDisplay = false)
+ assignTemplateAndCojoinPost(Map(), ctx.initProgram, funToPost, uniqueIdDisplay = false)
+ }*/
+
+ def pluginResultInInput(ctx: InferenceContext, ics: Seq[InferenceCondition], p: Program) = {
+
+ val solvedICs = ics.filter { _.prettyInv.isDefined }
+ // mapping from init to output
+ val outputFunMap =
+ functionsWOFields(ctx.initProgram.definedFunctions).map {
+ case fd if fd.isTheoryOperation => (fd -> fd)
+ case fd => {
+ val freshId = FreshIdentifier(fd.id.name, fd.returnType)
+ val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
+ fd -> newfd
+ }
+ }.toMap
+
+ def fullNameWoInst(fd: FunDef) = {
+ val splits = DefOps.fullName(fd)(p).split("-")
+ if (!splits.isEmpty) splits(0)
+ else ""
+ }
+
+ // mapping from p to output
+ val progFunMap = (Map[FunDef, FunDef]() /: functionsWOFields(p.definedFunctions)) {
+ case (acc, fd) =>
+ val inFun = functionByFullName(fullNameWoInst(fd), ctx.initProgram)
+ if (inFun.isDefined)
+ acc + (fd -> outputFunMap(inFun.get))
+ else acc
+ }.toMap
+
+ // mapping from init to ic
+ val initICmap = (Map[FunDef, InferenceCondition]() /: solvedICs) {
+ case (acc, ic) =>
+ val initfd = functionByFullName(fullNameWoInst(ic.fd), ctx.initProgram)
+ if (initfd.isDefined) {
+ acc + (initfd.get -> ic)
+ } else acc
+ }
+
+ def mapProgram(funMap: Map[FunDef, FunDef]) = {
+
+ def mapExpr(ine: Expr): Expr = {
+ val replaced = simplePostTransform((e: Expr) => e match {
+ case FunctionInvocation(tfd, args) if funMap.contains(tfd.fd) =>
+ FunctionInvocation(TypedFunDef(funMap(tfd.fd), tfd.tps), args)
+ case _ => e
+ })(ine)
+ replaced
+ }
+
+ for ((from, to) <- funMap) {
+ to.body = from.body.map(mapExpr)
+ to.precondition = from.precondition.map(mapExpr)
+ if (initICmap.contains(from)) {
+ val ic = initICmap(from)
+ val paramMap = (ic.fd.params zip from.params).map {
+ case (p1, p2) =>
+ (p1.id.toVariable -> p2.id.toVariable)
+ }.toMap
+ val icres = getResId(ic.fd).get
+ val npost =
+ if (from.hasPostcondition) {
+ val resid = getResId(from).get
+ val inv = replace(Map(icres.toVariable -> resid.toVariable) ++ paramMap, ic.prettyInv.get)
+ val postBody = from.postWoTemplate.map(post => createAnd(Seq(post, inv))).getOrElse(inv)
+ Lambda(Seq(ValDef(resid)), postBody)
+ } else {
+ val resid = FreshIdentifier(icres.name, icres.getType)
+ val inv = replace(Map(icres.toVariable -> resid.toVariable) ++ paramMap, ic.prettyInv.get)
+ Lambda(Seq(ValDef(resid)), inv)
+ }
+ to.postcondition = Some(mapExpr(npost))
+ } else
+ to.postcondition = from.postcondition.map(mapExpr)
+ //copy annotations
+ from.flags.foreach(to.addFlag(_))
+ }
+ }
+ mapProgram(outputFunMap ++ progFunMap)
+ copyProgram(ctx.initProgram, (defs: Seq[Definition]) => defs.map {
+ case fd: FunDef if outputFunMap.contains(fd) =>
+ outputFunMap(fd)
+ case d => d
+ })
+ /*if (debugSimplify)
+ println("After Simplifications: \n" + ScalaPrinter.apply(newprog))*/
+ // /newprog
+ /*if (ic.prettyInv.isDefined) {
+ val uninstFunName = InstUtil.userFunctionName(ic.fd)
+ val inputFdOpt =
+ if (uninstFunName.isEmpty) None
+ else functionByName(uninstFunName, ctx.initProgram)
+ inputFdOpt match {
+ case None => ctx.initProgram
+ case Some(inFd) =>
+ ProgramUtil.copyProgram(ctx.initProgram, defs => defs map {
+ case fd if fd.id == inFd.id =>
+ val newfd = new FunDef(FreshIdentifier(inFd.id.name), inFd.tparams, inFd.params, inFd.returnType)
+ newfd.body = inFd.body
+ newfd.precondition = inFd.precondition
+ val fdres = getResId(ic.fd).get
+ val npost =
+ if (inFd.hasPostcondition) {
+ val resid = getResId(inFd).get
+ val inv = replace(Map(fdres.toVariable -> resid.toVariable), ic.prettyInv.get)
+ // map also functions here.
+ val postBody = inFd.postWoTemplate.map(post => createAnd(Seq(post, inv))).getOrElse(inv)
+ Lambda(Seq(ValDef(resid)), postBody)
+ } else {
+ val resid = FreshIdentifier(fdres.name, fdres.getType)
+ val inv = replace(Map(fdres.toVariable -> resid.toVariable), ic.prettyInv.get)
+ Lambda(Seq(ValDef(resid)), inv)
+ }
+ newfd.postcondition = Some(npost)
+ newfd
+ case d => d
+ })
+ }
+ } else ctx.initProgram*/
}
}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/engine/RefinementEngine.scala b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
index cce8a3cb45a27693824944ed32c190921691cd2c..6cadb5b4f4563b95dbe6928f24237fb1f5b161c0 100644
--- a/src/main/scala/leon/invariant/engine/RefinementEngine.scala
+++ b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
@@ -15,14 +15,16 @@ import invariant.util._
import invariant.util.Util._
import invariant.structure._
import FunctionUtils._
+import Util._
+import PredicateUtil._
+import ProgramUtil._
//TODO: the parts of the code that collect the new head functions is ugly and has many side-effects. Fix this.
//TODO: there is a better way to compute heads, which is to consider all guards not previous seen
-class RefinementEngine(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
+class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: ConstraintTracker) {
val tru = BooleanLiteral(true)
val reporter = ctx.reporter
- val prog = ctx.program
val cg = CallGraphUtil.constructCallGraph(prog)
//this count indicates the number of times we unroll a recursive call
@@ -161,7 +163,7 @@ class RefinementEngine(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
} else plainBody
//note: here we are only adding the template as the postcondition
- val idmap = Util.formalToActual(Call(resvar, FunctionInvocation(recFunTyped, recFun.params.map(_.toVariable))))
+ val idmap = formalToActual(Call(resvar, FunctionInvocation(recFunTyped, recFun.params.map(_.toVariable))))
val postTemp = replace(idmap, recFun.getTemplate)
val vcExpr = ExpressionTransformer.normalizeExpr(And(bodyExpr, Not(postTemp)), ctx.multOp)
ctrTracker.addVC(recFun, vcExpr)
@@ -185,8 +187,8 @@ class RefinementEngine(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
//Important: make sure we use a fresh body expression here
val freshBody = freshenLocals(matchToIfThenElse(callee.body.get))
val calleeSummary =
- Equals(Util.getFunctionReturnVariable(callee), freshBody)
- val argmap1 = Util.formalToActual(call)
+ Equals(getFunctionReturnVariable(callee), freshBody)
+ val argmap1 = formalToActual(call)
val inlinedSummary = ExpressionTransformer.normalizeExpr(replace(argmap1, calleeSummary), ctx.multOp)
if (this.dumpInlinedSummary)
diff --git a/src/main/scala/leon/invariant/engine/SpecInstatiator.scala b/src/main/scala/leon/invariant/engine/SpecInstatiator.scala
index 9961df29357d1de52c98fe135f106993ab1e388a..e692cb6ab591cabe9732251e9edbc15f11c796cb 100644
--- a/src/main/scala/leon/invariant/engine/SpecInstatiator.scala
+++ b/src/main/scala/leon/invariant/engine/SpecInstatiator.scala
@@ -18,11 +18,14 @@ import scala.concurrent.duration._
import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
-import invariant.util.Util._
import invariant.structure._
import FunctionUtils._
+import Util._
+import PredicateUtil._
+import ProgramUtil._
+import SolverUtil._
-class SpecInstantiator(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
+class SpecInstantiator(ctx: InferenceContext, program: Program, ctrTracker: ConstraintTracker) {
val verbose = false
@@ -31,7 +34,6 @@ class SpecInstantiator(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
val tru = BooleanLiteral(true)
val axiomFactory = new AxiomFactory(ctx) //handles instantiation of axiomatic specification
- val program = ctx.program
//the guards of the set of calls that were already processed
protected var exploredGuards = Set[Variable]()
@@ -51,7 +53,7 @@ class SpecInstantiator(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
if (!disableAxioms) {
//remove all multiplication if "withmult" is specified
val relavantCalls = if (ctx.withmult) {
- newcalls.filter(call => !Util.isMultFunctions(call.fi.tfd.fd))
+ newcalls.filter(call => !isMultFunctions(call.fi.tfd.fd))
} else newcalls
instantiateAxioms(formula, relavantCalls)
}
@@ -107,7 +109,7 @@ class SpecInstantiator(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
}
def specForCall(call: Call): Option[Expr] = {
- val argmap = Util.formalToActual(call)
+ val argmap = formalToActual(call)
val callee = call.fi.tfd.fd
if (callee.hasPostcondition) {
//get the postcondition without templates
@@ -130,7 +132,7 @@ class SpecInstantiator(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
def templateForCall(call: Call): Option[Expr] = {
val callee = call.fi.tfd.fd
if (callee.hasTemplate) {
- val argmap = Util.formalToActual(call)
+ val argmap = formalToActual(call)
val tempExpr = replace(argmap, callee.getTemplate)
val template = if (callee.hasPrecondition) {
val freshPre = replace(argmap, freshenLocals(matchToIfThenElse(callee.precondition.get)))
@@ -158,7 +160,7 @@ class SpecInstantiator(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
val inst2 = instantiateBinaryAxioms(formula, calls)
val axiomInsts = inst1 ++ inst2
- Stats.updateCounterStats(Util.atomNum(Util.createAnd(axiomInsts)), "AxiomBlowup", "VC-refinement")
+ Stats.updateCounterStats(atomNum(createAnd(axiomInsts)), "AxiomBlowup", "VC-refinement")
if(verbose) ctx.reporter.info("Number of axiom instances: " + axiomInsts.size)
if (this.debugAxiomInstantiation) {
@@ -222,9 +224,9 @@ class SpecInstantiator(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
(call1.fi.tfd.id == call2.fi.tfd.id) && (call1 != call2)
}
- val product = Util.cross[Call, Call](newCallsWithAxioms, getBinaxCalls(formula.fd), Some(isInstantiable)).flatMap(
+ val product = cross[Call, Call](newCallsWithAxioms, getBinaxCalls(formula.fd), Some(isInstantiable)).flatMap(
p => Seq((p._1, p._2), (p._2, p._1))) ++
- Util.cross[Call, Call](newCallsWithAxioms, newCallsWithAxioms, Some(isInstantiable)).map(p => (p._1, p._2))
+ cross[Call, Call](newCallsWithAxioms, newCallsWithAxioms, Some(isInstantiable)).map(p => (p._1, p._2))
//ctx.reporter.info("# of pairs with axioms: "+product.size)
//Stats.updateCumStats(product.size, "Call-pairs-with-axioms")
diff --git a/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala b/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
index 17bfdee4b4d761f3d974abac06cc637166f46e98..c568910684e89d78862a516583eb0baf31174888 100644
--- a/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
+++ b/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
@@ -11,47 +11,49 @@ import purescala.Types._
import scala.collection.mutable.{ Set => MutableSet }
import java.io._
import scala.collection.mutable.{ Set => MutableSet }
-import scala.collection.mutable.{Set => MutableSet}
+import scala.collection.mutable.{ Set => MutableSet }
import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
import invariant.structure._
+import Util._
+import PredicateUtil._
+import ProgramUtil._
/**
- * An enumeration based template generator.
- * Enumerates all numerical terms in some order (this enumeration is incomplete for termination).
- * TODO: Feature:
- * (a) allow template functions and functions with template variables ?
- * (b) should we unroll algebraic data types ?
- *
- * The following function may potentially have complexity O(n^i) where 'n' is the number of functions
- * and 'i' is the increment step
- * TODO: optimize the running and also reduce the size of the input templates
- *
- * For now this is incomplete
- */
-class TemplateEnumerator(ctx: InferenceContext) extends TemplateGenerator {
- val prog = ctx.program
+ * An enumeration based template generator.
+ * Enumerates all numerical terms in some order (this enumeration is incomplete for termination).
+ * TODO: Feature:
+ * (a) allow template functions and functions with template variables ?
+ * (b) should we unroll algebraic data types ?
+ *
+ * The following function may potentially have complexity O(n^i) where 'n' is the number of functions
+ * and 'i' is the increment step
+ * TODO: optimize the running and also reduce the size of the input templates
+ *
+ * For now this is incomplete
+ */
+class TemplateEnumerator(ctx: InferenceContext, prog: Program) extends TemplateGenerator {
val reporter = ctx.reporter
- //create a call graph for the program
- //Caution: this call-graph could be modified later while call the 'getNextTemplate' method
- private val callGraph = {
- val cg = CallGraphUtil.constructCallGraph(prog)
- cg
- }
+ //create a call graph for the program
+ //Caution: this call-graph could be modified later while call the 'getNextTemplate' method
+ private val callGraph = {
+ val cg = CallGraphUtil.constructCallGraph(prog)
+ cg
+ }
- private var tempEnumMap = Map[FunDef, FunctionTemplateEnumerator]()
+ private var tempEnumMap = Map[FunDef, FunctionTemplateEnumerator]()
- def getNextTemplate(fd : FunDef) : Expr = {
- if(tempEnumMap.contains(fd)) tempEnumMap(fd).getNextTemplate()
- else {
- val enumerator = new FunctionTemplateEnumerator(fd, prog, ctx.enumerationRelation, callGraph, reporter)
- tempEnumMap += (fd -> enumerator)
- enumerator.getNextTemplate()
- }
- }
+ def getNextTemplate(fd: FunDef): Expr = {
+ if (tempEnumMap.contains(fd)) tempEnumMap(fd).getNextTemplate()
+ else {
+ val enumerator = new FunctionTemplateEnumerator(fd, prog, ctx.enumerationRelation, callGraph, reporter)
+ tempEnumMap += (fd -> enumerator)
+ enumerator.getNextTemplate()
+ }
+ }
}
/**
@@ -59,15 +61,15 @@ class TemplateEnumerator(ctx: InferenceContext) extends TemplateGenerator {
* 'op' is a side-effects parameter
* Caution: The methods of this class has side-effects on the 'callGraph' parameter
*/
-class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr,Expr) => Expr,
- callGraph : CallGraph, reporter: Reporter) {
+class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr, Expr) => Expr,
+ callGraph: CallGraph, reporter: Reporter) {
private val MAX_INCREMENTS = 2
private val zero = InfiniteIntegerLiteral(0)
//using default op as <= or == (manually adjusted)
//private val op = LessEquals
- //LessThan
- //LessEquals
- //Equals.apply _
+ //LessThan
+ //LessEquals
+ //Equals.apply _
private var currTemp: Expr = null
private var incrStep: Int = 0
private var typeTermMap = Map[TypeTree, MutableSet[Expr]]()
@@ -82,11 +84,10 @@ class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr,Expr)
def getNextTemplate(): Expr = {
//println("Getting next template for function: "+fd.id)
- if (incrStep == MAX_INCREMENTS){
+ if (incrStep == MAX_INCREMENTS) {
//exhausted the templates, so return
op(currTemp, zero)
- }
- else {
+ } else {
incrStep += 1
@@ -104,7 +105,7 @@ class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr,Expr)
}
})
- val resVar = Util.getFunctionReturnVariable(rootFun)
+ val resVar = getFunctionReturnVariable(rootFun)
if (newTerms.contains(rootFun.returnType)) {
newTerms(rootFun.returnType).add(resVar)
} else {
@@ -152,10 +153,10 @@ class FunctionTemplateEnumerator(rootFun: FunDef, prog: Program, op: (Expr,Expr)
//return all the integer valued terms of newTerms
//++ newTerms.getOrElse(Int32Type, Seq[Expr]()) (for now not handling int 32 terms)
val numericTerms = (newTerms.getOrElse(RealType, Seq[Expr]()) ++ newTerms.getOrElse(IntegerType, Seq[Expr]())).toSeq
- if(!numericTerms.isEmpty) {
+ if (!numericTerms.isEmpty) {
//create a linear combination of intTerms
val newTemp = numericTerms.foldLeft(null: Expr)((acc, t: Expr) => {
- val summand = Times(t, TemplateIdFactory.freshTemplateVar() : Expr)
+ val summand = Times(t, TemplateIdFactory.freshTemplateVar(): Expr)
if (acc == null) summand
else
Plus(summand, acc)
diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
index 5a806fa3cf3d0786637f7b80db4ab9b710c58eab..f54eeef6249651ee7d8ab1517a1982f9e69f6694 100644
--- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
@@ -8,6 +8,7 @@ import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
+import purescala.DefOps._
import solvers._
import solvers.z3.FairZ3Solver
import java.io._
@@ -17,11 +18,14 @@ import scala.reflect.runtime.universe
import invariant.templateSolvers._
import invariant.factories._
import invariant.util._
-import invariant.util.Util._
import invariant.structure._
import transformations._
import FunctionUtils._
import leon.invariant.templateSolvers.ExtendedUFSolver
+import Util._
+import PredicateUtil._
+import ProgramUtil._
+import SolverUtil._
/**
* @author ravi
@@ -35,14 +39,13 @@ trait FunctionTemplateSolver {
def apply(): Option[InferResult]
}
-class UnfoldingTemplateSolver(ctx: InferenceContext, rootFd: FunDef) extends FunctionTemplateSolver {
+class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: FunDef) extends FunctionTemplateSolver {
val reporter = ctx.reporter
- val program = ctx.program
val debugVCs = false
- lazy val constTracker = new ConstraintTracker(ctx, rootFd)
- lazy val templateSolver = TemplateSolverFactory.createTemplateSolver(ctx, constTracker, rootFd)
+ lazy val constTracker = new ConstraintTracker(ctx, program, rootFd)
+ lazy val templateSolver = TemplateSolverFactory.createTemplateSolver(ctx, program, constTracker, rootFd)
def constructVC(funDef: FunDef): (Expr, Expr) = {
val body = funDef.body.get
@@ -55,15 +58,18 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, rootFd: FunDef) extends Fun
And(matchToIfThenElse(funDef.precondition.get), plainBody)
} else plainBody
- val fullPost = matchToIfThenElse(if (funDef.hasTemplate)
- if (ctx.toVerifyPostFor.contains(funDef.id.name))
- And(funDef.getPostWoTemplate, funDef.getTemplate)
- else
- funDef.getTemplate
- else if (ctx.toVerifyPostFor.contains(funDef.id.name))
- funDef.getPostWoTemplate
- else
- BooleanLiteral(true))
+ val funName = fullName(funDef, useUniqueIds = false)(program)
+ val fullPost = matchToIfThenElse(
+ if (funDef.hasTemplate) {
+ // if the postcondition is verified do not include it in the sequent
+ if (ctx.isFunctionPostVerified(funName))
+ funDef.getTemplate
+ else
+ And(funDef.getPostWoTemplate, funDef.getTemplate)
+ } else if (!ctx.isFunctionPostVerified(funName))
+ funDef.getPostWoTemplate
+ else
+ BooleanLiteral(true))
(bodyExpr, fullPost)
}
@@ -80,41 +86,47 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, rootFd: FunDef) extends Fun
var toRefineCalls: Option[Set[Call]] = None
var infRes: Option[InferResult] = None
do {
- Stats.updateCounter(1, "VC-refinement")
- /* uncomment if we want to bound refinements
- * if (refinementStep >= 5)
- throw new IllegalStateException("Done 4 refinements")*/
- val refined =
- if (refinementStep >= 1) {
- reporter.info("- More unrollings for invariant inference")
-
- val toUnrollCalls = if (ctx.targettedUnroll) toRefineCalls else None
- val unrolledCalls = constTracker.refineVCs(toUnrollCalls)
- if (unrolledCalls.isEmpty) {
- reporter.info("- Cannot do more unrollings, reached unroll bound")
- false
- } else true
- } else {
- constTracker.initialize
- true
- }
- refinementStep += 1
infRes =
- if (!refined)
+ if(ctx.abort)
Some(InferResult(false, None, List()))
- else {
- //solve for the templates in this unroll step
- templateSolver.solveTemplates() match {
- case (Some(model), callsInPath) =>
- toRefineCalls = callsInPath
- //Validate the model here
- instantiateAndValidateModel(model, constTracker.getFuncs.toSeq)
- Some(InferResult(true, Some(model),
- constTracker.getFuncs.toList))
- case (None, callsInPath) =>
- toRefineCalls = callsInPath
- //here, we do not know if the template is solvable or not, we need to do more unrollings.
- None
+ else{
+ Stats.updateCounter(1, "VC-refinement")
+ /*
+ * uncomment if we want to bound refinements
+ * if (refinementStep >= 5)
+ * throw new IllegalStateException("Done 4 refinements")
+ */
+ val refined =
+ if (refinementStep >= 1) {
+ reporter.info("- More unrollings for invariant inference")
+
+ val toUnrollCalls = if (ctx.targettedUnroll) toRefineCalls else None
+ val unrolledCalls = constTracker.refineVCs(toUnrollCalls)
+ if (unrolledCalls.isEmpty) {
+ reporter.info("- Cannot do more unrollings, reached unroll bound")
+ false
+ } else true
+ } else {
+ constTracker.initialize
+ true
+ }
+ refinementStep += 1
+ if (!refined)
+ Some(InferResult(false, None, List()))
+ else {
+ //solve for the templates in this unroll step
+ templateSolver.solveTemplates() match {
+ case (Some(model), callsInPath) =>
+ toRefineCalls = callsInPath
+ //Validate the model here
+ instantiateAndValidateModel(model, constTracker.getFuncs.toSeq)
+ Some(InferResult(true, Some(model),
+ constTracker.getFuncs.toList))
+ case (None, callsInPath) =>
+ toRefineCalls = callsInPath
+ //here, we do not know if the template is solvable or not, we need to do more unrollings.
+ None
+ }
}
}
} while (!infRes.isDefined)
@@ -175,7 +187,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, rootFd: FunDef) extends Fun
//create a fundef for each function in the program
//note: mult functions are also copied
val newFundefs = program.definedFunctions.collect {
- case fd @ _ => { //if !Util.isMultFunctions(fd)
+ case fd @ _ => { //if !isMultFunctions(fd)
val newfd = new FunDef(FreshIdentifier(fd.id.name, Untyped, false), fd.tparams, fd.params, fd.returnType)
(fd, newfd)
}
@@ -226,7 +238,7 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, rootFd: FunDef) extends Fun
newfd.addFlags(fd.flags)
})
- val augmentedProg = Util.copyProgram(program, (defs: Seq[Definition]) => defs.collect {
+ val augmentedProg = copyProgram(program, (defs: Seq[Definition]) => defs.collect {
case fd: FunDef if (newFundefs.contains(fd)) => newFundefs(fd)
case d if (!d.isInstanceOf[FunDef]) => d
})
diff --git a/src/main/scala/leon/invariant/factories/AxiomFactory.scala b/src/main/scala/leon/invariant/factories/AxiomFactory.scala
index 27c7e44c708e2d3126166afc7417ddfab858bc1d..6fdf7fa633def45017de8df5fbab4250ce70928e 100644
--- a/src/main/scala/leon/invariant/factories/AxiomFactory.scala
+++ b/src/main/scala/leon/invariant/factories/AxiomFactory.scala
@@ -18,6 +18,8 @@ import invariant.engine._
import invariant.util._
import invariant.structure._
import FunctionUtils._
+import Util._
+import PredicateUtil._
class AxiomFactory(ctx : InferenceContext) {
@@ -78,7 +80,7 @@ class AxiomFactory(ctx : InferenceContext) {
lesse +: acc
})
val conseq = LessEquals(call1.retexpr, call2.retexpr)
- (Util.createAnd(ants), conseq)
+ (createAnd(ants), conseq)
}
//this is applicable only to binary operations
diff --git a/src/main/scala/leon/invariant/factories/TemplateFactory.scala b/src/main/scala/leon/invariant/factories/TemplateFactory.scala
index 68080a79e8106decdeb6c809d0601c10be637e68..ab1f51359151de13ef8cd506f4f1c9da9472c208 100644
--- a/src/main/scala/leon/invariant/factories/TemplateFactory.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateFactory.scala
@@ -17,6 +17,9 @@ import invariant.engine._
import invariant.util._
import invariant.structure._
import FunctionUtils._
+import Util._
+import PredicateUtil._
+import ProgramUtil._
object TemplateIdFactory {
//a set of template ids
@@ -70,7 +73,7 @@ class TemplateFactory(tempGen : Option[TemplateGenerator], prog: Program, report
private var templateMap = {
//initialize the template map with predefined user maps
var muMap = MutableMap[FunDef, Expr]()
- Util.functionsWOFields(prog.definedFunctions).foreach { fd =>
+ functionsWOFields(prog.definedFunctions).foreach { fd =>
val tmpl = fd.template
if (tmpl.isDefined) {
muMap.update(fd, tmpl.get)
@@ -90,8 +93,8 @@ class TemplateFactory(tempGen : Option[TemplateGenerator], prog: Program, report
def getDefaultTemplate(fd : FunDef): Expr = {
//just consider all the arguments, return values that are integers
- val baseTerms = fd.params.filter((vardecl) => Util.isNumericType(vardecl.getType)).map(_.toVariable) ++
- (if(Util.isNumericType(fd.returnType)) Seq(Util.getFunctionReturnVariable(fd))
+ val baseTerms = fd.params.filter((vardecl) => isNumericType(vardecl.getType)).map(_.toVariable) ++
+ (if(isNumericType(fd.returnType)) Seq(getFunctionReturnVariable(fd))
else Seq())
val lhs = baseTerms.foldLeft(TemplateIdFactory.freshTemplateVar() : Expr)((acc, t)=> {
@@ -101,7 +104,6 @@ class TemplateFactory(tempGen : Option[TemplateGenerator], prog: Program, report
tempExpr
}
-
/**
* Constructs a template using a mapping from the formals to actuals.
* Uses default template if a template does not exist for the function and no template generator is provided.
@@ -123,7 +125,6 @@ class TemplateFactory(tempGen : Option[TemplateGenerator], prog: Program, report
replace(argmap,templateMap(fd))
}
-
/**
* Refines the templates of the functions that were assigned templates using the template generator.
*/
diff --git a/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala b/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
index 5944f68bd9faa11ddfa5d26d8d057a086aea080c..ccaabc57aabecb9fa22fd94a5972c1a554196729 100644
--- a/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
@@ -15,26 +15,29 @@ import invariant.util._
import invariant.structure._
import leon.solvers.Model
import leon.invariant.util.RealValuedExprEvaluator
+import Util._
+import PredicateUtil._
+import ProgramUtil._
object TemplateInstantiator {
- /**
+ /**
* Computes the invariant for all the procedures given a mapping for the
* template variables.
* (Undone) If the mapping does not have a value for an id, then the id is bound to the simplest value
*/
- def getAllInvariants(model: Model, templates :Map[FunDef, Expr]): Map[FunDef, Expr] = {
+ def getAllInvariants(model: Model, templates: Map[FunDef, Expr], prettyInv: Boolean = false): Map[FunDef, Expr] = {
val invs = templates.map((pair) => {
val (fd, t) = pair
//flatten the template
val freevars = variablesOf(t)
val template = ExpressionTransformer.FlattenFunction(t)
- val tempvars = Util.getTemplateVars(template)
+ val tempvars = getTemplateVars(template)
val tempVarMap: Map[Expr, Expr] = tempvars.map((v) => {
(v, model(v.id))
}).toMap
- val instTemplate = instantiate(template, tempVarMap)
+ val instTemplate = instantiate(template, tempVarMap, prettyInv)
//now unflatten it
val comprTemp = ExpressionTransformer.unFlatten(instTemplate, freevars)
(fd, comprTemp)
@@ -46,40 +49,36 @@ object TemplateInstantiator {
* Instantiates templated subexpressions of the given expression (expr) using the given mapping for the template variables.
* The instantiation also takes care of converting the rational coefficients to integer coefficients.
*/
- def instantiate(expr: Expr, tempVarMap: Map[Expr, Expr]): Expr = {
+ def instantiate(expr: Expr, tempVarMap: Map[Expr, Expr], prettyInv: Boolean = false): Expr = {
//do a simple post transform and replace the template vars by their values
val inv = simplePostTransform((tempExpr: Expr) => tempExpr match {
case e @ Operator(Seq(lhs, rhs), op) if ((e.isInstanceOf[Equals] || e.isInstanceOf[LessThan]
|| e.isInstanceOf[LessEquals] || e.isInstanceOf[GreaterThan]
|| e.isInstanceOf[GreaterEquals])
&&
- !Util.getTemplateVars(tempExpr).isEmpty) => {
-
- //println("Template Expression: "+tempExpr)
+ !getTemplateVars(tempExpr).isEmpty) => {
val linearTemp = LinearConstraintUtil.exprToTemplate(tempExpr)
- // println("MODEL\n" + tempVarMap)
- instantiateTemplate(linearTemp, tempVarMap)
+ instantiateTemplate(linearTemp, tempVarMap, prettyInv)
}
case _ => tempExpr
})(expr)
inv
}
-
- def validateLiteral(e : Expr) = e match {
+ def validateLiteral(e: Expr) = e match {
case FractionalLiteral(num, denom) => {
if (denom == 0)
- throw new IllegalStateException("Denominator is zero !! " +e)
+ throw new IllegalStateException("Denominator is zero !! " + e)
if (denom < 0)
throw new IllegalStateException("Denominator is negative: " + denom)
true
}
- case IntLiteral(_) => true
+ case IntLiteral(_) => true
case InfiniteIntegerLiteral(_) => true
- case _ => throw new IllegalStateException("Not a real literal: " + e)
+ case _ => throw new IllegalStateException("Not a real literal: " + e)
}
- def instantiateTemplate(linearTemp: LinearTemplate, tempVarMap: Map[Expr, Expr]): Expr = {
+ def instantiateTemplate(linearTemp: LinearTemplate, tempVarMap: Map[Expr, Expr], prettyInv: Boolean = false): Expr = {
val bigone = BigInt(1)
val coeffMap = linearTemp.coeffTemplate.map((entry) => {
val (term, coeffTemp) = entry
@@ -90,20 +89,19 @@ object TemplateInstantiator {
(term -> coeff)
})
- val const = if (linearTemp.constTemplate.isDefined){
+ val const = if (linearTemp.constTemplate.isDefined) {
val constE = replace(tempVarMap, linearTemp.constTemplate.get)
val constV = RealValuedExprEvaluator.evaluate(constE)
validateLiteral(constV)
Some(constV)
- }
- else None
+ } else None
val realValues: Seq[Expr] = coeffMap.values.toSeq ++ { if (const.isDefined) Seq(const.get) else Seq() }
//the coefficients could be fractions ,so collect all the denominators
val getDenom = (t: Expr) => t match {
case FractionalLiteral(num, denum) => denum
- case _ => bigone
+ case _ => bigone
}
val denoms = realValues.foldLeft(Set[BigInt]())((acc, entry) => { acc + getDenom(entry) })
@@ -112,8 +110,8 @@ object TemplateInstantiator {
val gcd = denoms.foldLeft(bigone)((acc, d) => acc.gcd(d))
val lcm = denoms.foldLeft(BigInt(1))((acc, d) => {
val product = (acc * d)
- if(product % gcd == 0)
- product/ gcd
+ if (product % gcd == 0)
+ product / gcd
else product
})
@@ -129,6 +127,8 @@ object TemplateInstantiator {
val intConst = if (const.isDefined) Some(scaleNum(const.get)) else None
val linearCtr = new LinearConstraint(linearTemp.op, intCoeffMap, intConst)
- linearCtr.toExpr
+ if (prettyInv)
+ linearCtr.toPrettyExpr
+ else linearCtr.toExpr
}
}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala b/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
index 25abefa22e51479c6d56fffd2c9e8a91a8b0bfec..469317998a98f979a9a90770fd9c902544eee584 100644
--- a/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
@@ -17,27 +17,27 @@ import leon.solvers.Model
object TemplateSolverFactory {
- def createTemplateSolver(ctx: InferenceContext, ctrack: ConstraintTracker, rootFun: FunDef,
+ def createTemplateSolver(ctx: InferenceContext, prog: Program, ctrack: ConstraintTracker, rootFun: FunDef,
// options to solvers
minopt: Option[(Expr, Model) => Model] = None,
bound: Option[Int] = None): TemplateSolver = {
if (ctx.useCegis) {
// TODO: find a better way to specify CEGIS total time bound
- new CegisSolver(ctx, rootFun, ctrack, 10000, bound)
+ new CegisSolver(ctx, prog, rootFun, ctrack, 10000, bound)
} else {
val minimizer = if (ctx.tightBounds && rootFun.hasTemplate) {
if (minopt.isDefined)
minopt
else {
//TODO: need to assert that the templates are resource templates
- Some((new Minimizer(ctx)).tightenTimeBounds(rootFun.getTemplate) _)
+ Some((new Minimizer(ctx, prog)).tightenTimeBounds(rootFun.getTemplate) _)
}
} else
None
if (ctx.withmult) {
- new NLTemplateSolverWithMult(ctx, rootFun, ctrack, minimizer)
+ new NLTemplateSolverWithMult(ctx, prog, rootFun, ctrack, minimizer)
} else {
- new NLTemplateSolver(ctx, rootFun, ctrack, minimizer)
+ new NLTemplateSolver(ctx, prog, rootFun, ctrack, minimizer)
}
}
}
diff --git a/src/main/scala/leon/invariant/structure/Constraint.scala b/src/main/scala/leon/invariant/structure/Constraint.scala
index 2a6e32ce40f8882ec4e240578bd1a60b35eaee0e..9d2490fe5f8b61b6847636007c61d6ba3c0dba34 100644
--- a/src/main/scala/leon/invariant/structure/Constraint.scala
+++ b/src/main/scala/leon/invariant/structure/Constraint.scala
@@ -17,6 +17,8 @@ import evaluators._
import java.io._
import solvers.z3.UninterpretedZ3Solver
import invariant.util._
+import Util._
+import PredicateUtil._
trait Constraint {
def toExpr: Expr
@@ -41,19 +43,15 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
val coeffTemplate = {
//assert if the coefficients are templated expressions
assert(coeffTemp.values.foldLeft(true)((acc, e) => {
- acc && Util.isTemplateExpr(e)
+ acc && isTemplateExpr(e)
}))
-
- //print the template mapping
- /*println("Coeff Mapping: "+coeffTemp)
- println("Constant: "+constTemplate)*/
coeffTemp
}
val constTemplate = {
assert(constTemp match {
case None => true
- case Some(e) => Util.isTemplateExpr(e)
+ case Some(e) => isTemplateExpr(e)
})
constTemp
}
@@ -70,13 +68,11 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
else Plus(lhs, constTemp.get)
} else lhs
val expr = oper(Seq(lhs, zero))
- //assert(expr.isInstanceOf[Equals] || expr.isInstanceOf[LessThan] || expr.isInstanceOf[GreaterThan]
- // || expr.isInstanceOf[LessEquals] || expr.isInstanceOf[GreaterEquals])
expr
}
def templateVars: Set[Variable] = {
- Util.getTemplateVars(template)
+ getTemplateVars(template)
}
def coeffEntryToString(coeffEntry: (Expr, Expr)): String = {
@@ -94,6 +90,45 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
override def toExpr: Expr = template
+ /**
+ * Converts the template to a more human readable form
+ * by group positive (and negative) terms together
+ */
+ def toPrettyExpr = {
+ val (lhsCoeff, rhsCoeff) = coeffTemplate.partition {
+ case (term, InfiniteIntegerLiteral(v)) =>
+ v >= 0
+ case _ => true
+ }
+ var lhsExprs: Seq[Expr] = lhsCoeff.map(e => Times(e._2, e._1)).toSeq
+ var rhsExprs: Seq[Expr] = rhsCoeff.map {
+ case (term, InfiniteIntegerLiteral(v)) =>
+ Times(InfiniteIntegerLiteral(-v), term) // make the coeff +ve
+ }.toSeq
+ constTemplate match {
+ case Some(InfiniteIntegerLiteral(v)) if v < 0 =>
+ rhsExprs :+= InfiniteIntegerLiteral(-v)
+ case Some(c) =>
+ lhsExprs :+= c
+ case _ => Nil
+ }
+ val lhsExprOpt = ((None: Option[Expr]) /: lhsExprs) {
+ case (acc, minterm) =>
+ if (acc.isDefined)
+ Some(Plus(acc.get, minterm))
+ else Some(minterm)
+ }
+ val rhsExprOpt = ((None: Option[Expr]) /: rhsExprs) {
+ case (acc, minterm) =>
+ if (acc.isDefined)
+ Some(Plus(acc.get, minterm))
+ else Some(minterm)
+ }
+ val lhs = lhsExprOpt.getOrElse(InfiniteIntegerLiteral(0))
+ val rhs = rhsExprOpt.getOrElse(InfiniteIntegerLiteral(0))
+ oper(Seq(lhs, rhs))
+ }
+
override def toString(): String = {
val coeffStr = if (coeffTemplate.isEmpty) ""
@@ -143,7 +178,6 @@ class LinearConstraint(opr: Seq[Expr] => Expr, cMap: Map[Expr, Expr], constant:
assert(cMap.values.foldLeft(true)((acc, e) => {
acc && variablesOf(e).isEmpty
}))
-
//TODO: here we should try to simplify the constant expressions
cMap
}
diff --git a/src/main/scala/leon/invariant/structure/Formula.scala b/src/main/scala/leon/invariant/structure/Formula.scala
index 0fedbc7057b6172b43c405caa6a976a24541c81a..daed61ff679cba61666a6c227005c103a31d8d01 100644
--- a/src/main/scala/leon/invariant/structure/Formula.scala
+++ b/src/main/scala/leon/invariant/structure/Formula.scala
@@ -16,6 +16,8 @@ import solvers.z3._
import invariant.engine._
import invariant.util._
import leon.solvers.Model
+import Util._
+import PredicateUtil._
/**
* Data associated with a call
@@ -99,12 +101,12 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
})
//create a temporary for Or
val gor = TVarFactory.createTemp("b", BooleanType).toVariable
- val newor = Util.createOr(newargs)
+ val newor = createOr(newargs)
conjuncts += (gor -> newor)
gor
}
case And(args) => {
- val newargs = args.map(arg => if (Util.getTemplateVars(e).isEmpty) {
+ val newargs = args.map(arg => if (getTemplateVars(e).isEmpty) {
arg
} else {
//if the expression has template variables then we separate it using guards
@@ -114,7 +116,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
disjuncts += (g -> ctrs)
g
})
- Util.createAnd(newargs)
+ createAnd(newargs)
}
case _ => e
})(ExpressionTransformer.simplify(simplifyArithmetic(
@@ -209,24 +211,24 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
var rest = Seq[Expr]()
disjuncts.foreach(entry => {
val (g,ctrs) = entry
- val ctrExpr = combiningOp(g,Util.createAnd(ctrs.map(_.toExpr)))
- if(Util.getTemplateVars(ctrExpr).isEmpty)
+ val ctrExpr = combiningOp(g,createAnd(ctrs.map(_.toExpr)))
+ if(getTemplateVars(ctrExpr).isEmpty)
rest :+= ctrExpr
else
paramPart :+= ctrExpr
})
val conjs = conjuncts.map((entry) => combiningOp(entry._1, entry._2)).toSeq ++ roots
- (Util.createAnd(paramPart), Util.createAnd(rest ++ conjs ++ roots))
+ (createAnd(paramPart), createAnd(rest ++ conjs ++ roots))
}
def toExpr : Expr={
val disjs = disjuncts.map((entry) => {
val (g,ctrs) = entry
- combiningOp(g, Util.createAnd(ctrs.map(_.toExpr)))
+ combiningOp(g, createAnd(ctrs.map(_.toExpr)))
}).toSeq
val conjs = conjuncts.map((entry) => combiningOp(entry._1, entry._2)).toSeq
- Util.createAnd(disjs ++ conjs ++ roots)
+ createAnd(disjs ++ conjs ++ roots)
}
//unpack the disjunct and conjuncts by removing all guards
@@ -238,7 +240,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
case BoolConstraint(g@Variable(_)) if conjuncts.contains(g) => conjuncts(g)
case ctr@_ => ctr.toExpr
})
- (g, Util.createAnd(newctrs))
+ (g, createAnd(newctrs))
})
val rootexprs = roots.map(_ match {
case g@Variable(_) if conjuncts.contains(g) => conjuncts(g)
@@ -266,13 +268,13 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
unpackedDisjs = newDisjs
}
//replace all the 'guards' in root using 'unpackedDisjs'
- replace(unpackedDisjs, Util.createAnd(rootexprs))
+ replace(unpackedDisjs, createAnd(rootexprs))
}
override def toString : String = {
val disjStrs = disjuncts.map((entry) => {
val (g,ctrs) = entry
- simplifyArithmetic(combiningOp(g, Util.createAnd(ctrs.map(_.toExpr)))).toString
+ simplifyArithmetic(combiningOp(g, createAnd(ctrs.map(_.toExpr)))).toString
}).toSeq
val conjStrs = conjuncts.map((entry) => combiningOp(entry._1, entry._2).toString).toSeq
val rootStrs = roots.map(_.toString)
diff --git a/src/main/scala/leon/invariant/structure/FunctionUtils.scala b/src/main/scala/leon/invariant/structure/FunctionUtils.scala
index f676520cd6907114f3130316cb9e3c38955a02d8..a0acdcda7388ee4b6971106cf78cdb49c42768a4 100644
--- a/src/main/scala/leon/invariant/structure/FunctionUtils.scala
+++ b/src/main/scala/leon/invariant/structure/FunctionUtils.scala
@@ -10,6 +10,8 @@ import purescala.Types._
import invariant.factories._
import invariant.util._
import Util._
+import PredicateUtil._
+import ProgramUtil._
import scala.language.implicitConversions
/**
@@ -107,8 +109,8 @@ object FunctionUtils {
case a if exists(isQMark)(a) => true
case _ => false
}
- //println(s"Otherpreds: $otherPreds ${qmarksToTmplFunction(Util.createAnd(tempExprs))}")
- Util.createAnd(otherPreds :+ qmarksToTmplFunction(Util.createAnd(tempExprs)))
+ //println(s"Otherpreds: $otherPreds ${qmarksToTmplFunction(createAnd(tempExprs))}")
+ createAnd(otherPreds :+ qmarksToTmplFunction(createAnd(tempExprs)))
case pb if exists(isQMark)(pb) =>
qmarksToTmplFunction(pb)
case other => other
diff --git a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
index 102c2a088446102f6d0f9a1403cd106009fdfb11..7910df7230e82f7ac8b695bc8089fcd64c005e3a 100644
--- a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
+++ b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
@@ -14,6 +14,8 @@ import java.io._
import invariant.util._
import BigInt._
import Constructors._
+import Util._
+import PredicateUtil._
class NotImplementedException(message: String) extends RuntimeException(message) {
@@ -105,7 +107,7 @@ object LinearConstraintUtil {
//handle each minterm
minterms.foreach((minterm: Expr) => minterm match {
- case _ if (Util.isTemplateExpr(minterm)) => {
+ case _ if (isTemplateExpr(minterm)) => {
addConstant(minterm)
}
case Times(e1, e2) => {
@@ -117,7 +119,7 @@ object LinearConstraintUtil {
}
e1 match {
//case c @ InfiniteIntegerLiteral(_) => addCoefficient(e2, c)
- case _ if (Util.isTemplateExpr(e1)) => {
+ case _ if (isTemplateExpr(e1)) => {
addCoefficient(e2, e1)
}
case _ => throw new IllegalStateException("Coefficient not a constant or template expression: " + e1)
@@ -219,7 +221,7 @@ object LinearConstraintUtil {
|| e.isInstanceOf[GreaterEquals])) => {
//check if the expression has real valued sub-expressions
- val isReal = Util.hasReals(e1) || Util.hasReals(e2)
+ val isReal = hasReals(e1) || hasReals(e2)
//doing something else ... ?
// println("[DEBUG] Expr 1 " + e1 + " of type " + e1.getType + " and Expr 2 " + e2 + " of type" + e2.getType)
val (newe, newop) = e match {
@@ -256,9 +258,9 @@ object LinearConstraintUtil {
case Times(_, _) | RealTimes(_, _) => {
val Operator(Seq(e1, e2), op) = inExpr
val (r1, r2) = (mkLinearRecur(e1), mkLinearRecur(e2))
- if(Util.isTemplateExpr(r1)) {
+ if(isTemplateExpr(r1)) {
PushTimes(r1, r2)
- } else if(Util.isTemplateExpr(r2)){
+ } else if(isTemplateExpr(r2)){
PushTimes(r2, r1)
} else
throw new IllegalStateException("Expression not linear: " + Times(r1, r2))
@@ -486,4 +488,3 @@ object LinearConstraintUtil {
}
}
}
-
diff --git a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
index 305bd98e34383a572c20618c1e429722f0c91341..98f162fea4b2974702c4672274ed6d8f86075690 100644
--- a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
@@ -17,18 +17,19 @@ import invariant.util._
import invariant.structure._
import invariant.structure.FunctionUtils._
import leon.invariant.util.RealValuedExprEvaluator._
+import Util._
+import PredicateUtil._
+import SolverUtil._
-class CegisSolver(ctx: InferenceContext,
- rootFun: FunDef,
- ctrTracker: ConstraintTracker,
- timeout: Int,
- bound: Option[Int] = None) extends TemplateSolver(ctx, rootFun, ctrTracker) {
+class CegisSolver(ctx: InferenceContext, program: Program,
+ rootFun: FunDef, ctrTracker: ConstraintTracker,
+ timeout: Int, bound: Option[Int] = None) extends TemplateSolver(ctx, rootFun, ctrTracker) {
override def solve(tempIds: Set[Identifier], funcVCs: Map[FunDef, Expr]): (Option[Model], Option[Set[Call]]) = {
val initCtr = if (bound.isDefined) {
//use a predefined bound on the template variables
- Util.createAnd(tempIds.map((id) => {
+ createAnd(tempIds.map((id) => {
val idvar = id.toVariable
And(Implies(LessThan(idvar, realzero), GreaterEquals(idvar, InfiniteIntegerLiteral(-bound.get))),
Implies(GreaterEquals(idvar, realzero), LessEquals(idvar, InfiniteIntegerLiteral(bound.get))))
@@ -37,10 +38,10 @@ class CegisSolver(ctx: InferenceContext,
} else tru
val funcs = funcVCs.keys
- val formula = Util.createOr(funcs.map(funcVCs.apply _).toSeq)
+ val formula = createOr(funcs.map(funcVCs.apply _).toSeq)
//using reals with bounds does not converge and also results in overflow
- val (res, _, model) = (new CegisCore(ctx, timeout, this)).solve(tempIds, formula, initCtr, solveAsInt = true)
+ val (res, _, model) = (new CegisCore(ctx, program, timeout, this)).solve(tempIds, formula, initCtr, solveAsInt = true)
res match {
case Some(true) => (Some(model), None)
case Some(false) => (None, None) //no solution exists
@@ -51,7 +52,7 @@ class CegisSolver(ctx: InferenceContext,
}
class CegisCore(ctx: InferenceContext,
- timeout: Int,
+ program: Program, timeout: Int,
cegisSolver: TemplateSolver) {
val fls = BooleanLiteral(false)
@@ -60,7 +61,6 @@ class CegisCore(ctx: InferenceContext,
val timeoutMillis = timeout.toLong * 1000
val dumpCandidateInvs = true
val minimizeSum = false
- val program = ctx.program
val context = ctx.leonContext
val reporter = context.reporter
@@ -80,7 +80,7 @@ class CegisCore(ctx: InferenceContext,
//for some sanity checks
var oldModels = Set[Expr]()
def addModel(m: Model) = {
- val mexpr = Util.modelToExpr(m)
+ val mexpr = modelToExpr(m)
if (oldModels.contains(mexpr))
throw new IllegalStateException("repeating model !!:" + m)
else oldModels += mexpr
@@ -94,7 +94,7 @@ class CegisCore(ctx: InferenceContext,
val tempVarSum = if (minimizeSum) {
//compute the sum of the tempIds
- val rootTempIds = Util.getTemplateVars(cegisSolver.rootFun.getTemplate)
+ val rootTempIds = getTemplateVars(cegisSolver.rootFun.getTemplate)
if (rootTempIds.size >= 1) {
rootTempIds.tail.foldLeft(rootTempIds.head.asInstanceOf[Expr])((acc, tvar) => Plus(acc, tvar))
} else zero
@@ -102,7 +102,7 @@ class CegisCore(ctx: InferenceContext,
//convert initCtr to a real-constraint
val initRealCtr = ExpressionTransformer.IntLiteralToReal(initCtr)
- if (Util.hasInts(initRealCtr))
+ if (hasInts(initRealCtr))
throw new IllegalStateException("Initial constraints have integer terms: " + initRealCtr)
def cegisRec(model: Model, prevctr: Expr): (Option[Boolean], Expr, Model) = {
@@ -128,7 +128,7 @@ class CegisCore(ctx: InferenceContext,
val spuriousTempIds = variablesOf(instFormula).intersect(TemplateIdFactory.getTemplateIds)
if (!spuriousTempIds.isEmpty)
throw new IllegalStateException("Found a template variable in instFormula: " + spuriousTempIds)
- if (Util.hasReals(instFormula))
+ if (hasReals(instFormula))
throw new IllegalStateException("Reals in instFormula: " + instFormula)
//println("solving instantiated vcs...")
@@ -166,7 +166,7 @@ class CegisCore(ctx: InferenceContext,
//println("Newctr: " +newctr)
if (ctx.dumpStats) {
- Stats.updateCounterStats(Util.atomNum(newctr), "CegisTemplateCtrs", "CegisIters")
+ Stats.updateCounterStats(atomNum(newctr), "CegisTemplateCtrs", "CegisIters")
}
//println("solving template constraints...")
@@ -188,7 +188,7 @@ class CegisCore(ctx: InferenceContext,
(res1, rti.unmapModel(intModel))
} else {
- /*if(InvariantUtil.hasInts(tempctrs))
+ /*if(InvarianthasInts(tempctrs))
throw new IllegalStateException("Template constraints have integer terms: " + tempctrs)*/
if (minimizeSum) {
minimizeReals(And(newctr, initRealCtr), tempVarSum)
diff --git a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index 6e80c47496aa59f5b9b5c6a01085ff0ec877f298..26710b7111b301748340d738fd35a1465364c9da 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -14,8 +14,12 @@ import solvers.SimpleSolverAPI
import scala.collection.mutable.{ Map => MutableMap }
import invariant.engine._
import invariant.factories._
-import invariant.util.Util._
import invariant.util._
+import Util._
+import ProgramUtil._
+import SolverUtil._
+import PredicateUtil._
+import TimerUtil._
import invariant.structure._
import leon.solvers.TimeoutSolver
import leon.solvers.SolverFactory
@@ -24,7 +28,7 @@ import leon.solvers.Model
import leon.solvers.smtlib.SMTLIBZ3Solver
import leon.invariant.util.RealValuedExprEvaluator._
-class FarkasLemmaSolver(ctx: InferenceContext) {
+class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
//debug flags
val verbose = true
@@ -39,9 +43,9 @@ class FarkasLemmaSolver(ctx: InferenceContext) {
val useIncrementalSolvingForNLctrs = false //note: NLsat doesn't support incremental solving. It starts from sratch even in incremental solving.
val leonctx = ctx.leonContext
- val program = ctx.program
val reporter = ctx.reporter
- val timeout = ctx.timeout
+ val timeout = ctx.vcTimeout // Note: we are using vcTimeout here as well
+
/**
* This procedure produces a set of constraints that need to be satisfiable for the
* conjunction ants and conseqs to be false
@@ -54,11 +58,6 @@ class FarkasLemmaSolver(ctx: InferenceContext) {
*
*/
def constraintsForUnsat(linearCtrs: Seq[LinearConstraint], temps: Seq[LinearTemplate]): Expr = {
-
- //for debugging
- /*println("#" * 20)
- println(allAnts + " ^ " + allConseqs)
- println("#" * 20)*/
this.applyFarkasLemma(linearCtrs ++ temps, Seq(), true)
}
@@ -253,7 +252,7 @@ class FarkasLemmaSolver(ctx: InferenceContext) {
reduceNonlinearity)(nlctrs)
//for debugging nonlinear constraints
- if (this.debugNLCtrs && Util.hasInts(simpctrs)) {
+ if (this.debugNLCtrs && hasInts(simpctrs)) {
throw new IllegalStateException("Nonlinear constraints have integers: " + simpctrs)
}
if (verbose && LinearConstraintUtil.isLinear(simpctrs)) {
@@ -263,30 +262,31 @@ class FarkasLemmaSolver(ctx: InferenceContext) {
reporter.info("InputCtrs: " + nlctrs)
reporter.info("SimpCtrs: " + simpctrs)
if (this.dumpNLCtrsAsSMTLIB) {
- val filename = ctx.program.modules.last.id + "-nlctr" + FileCountGUID.getID + ".smt2"
- if (Util.atomNum(simpctrs) >= 5) {
+ val filename = program.modules.last.id + "-nlctr" + FileCountGUID.getID + ".smt2"
+ if (atomNum(simpctrs) >= 5) {
if (solveAsBitvectors)
- Util.toZ3SMTLIB(simpctrs, filename, "QF_BV", leonctx, program, useBitvectors = true, bitvecSize = bvsize)
+ toZ3SMTLIB(simpctrs, filename, "QF_BV", leonctx, program, useBitvectors = true, bitvecSize = bvsize)
else
- Util.toZ3SMTLIB(simpctrs, filename, "QF_NRA", leonctx, program)
+ toZ3SMTLIB(simpctrs, filename, "QF_NRA", leonctx, program)
reporter.info("NLctrs dumped to: " + filename)
}
}
}
// solve the resulting constraints using solver
- val innerSolver = if (solveAsBitvectors) {
+ val solver = if (solveAsBitvectors) {
throw new IllegalStateException("Not supported now. Will be in the future!")
//new ExtendedUFSolver(leonctx, program, useBitvectors = true, bitvecSize = bvsize) with TimeoutSolver
} else {
- // use SMTLIBSolver to solve the constraints so that it can be timed out effectively
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver
- //new ExtendedUFSolver(leonctx, program) with TimeoutSolver
+ //new AbortableSolver(() => new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver, ctx)
+ SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
+ new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), timeout * 1000))
}
- val solver = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => innerSolver), timeout * 1000))
+ //val solver = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => innerSolver), ))
if (verbose) reporter.info("solving...")
val t1 = System.currentTimeMillis()
- val (res, model) = solver.solveSAT(simpctrs)
+ //solver.solveSAT(simpctrs)
+ val (res, model) = solver.solveSAT(simpctrs) //solver.solveSAT(simpctrs, timeout * 1000)
val t2 = System.currentTimeMillis()
if (verbose) reporter.info((if (res.isDefined) "solved" else "timed out") + "... in " + (t2 - t1) / 1000.0 + "s")
Stats.updateCounterTime((t2 - t1), "NL-solving-time", "disjuncts")
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 47901d3b9ec6d41ccbfcab75e41db37ebd2aab85..0e0e4ef355e116d717a210cb2b587ad76c3b733b 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -25,10 +25,14 @@ import invariant.util._
import invariant.util.ExpressionTransformer._
import invariant.structure._
import invariant.structure.FunctionUtils._
-import leon.invariant.util.RealValuedExprEvaluator._
-
-class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: ConstraintTracker,
- minimizer: Option[(Expr, Model) => Model])
+import RealValuedExprEvaluator._
+import Util._
+import PredicateUtil._
+import SolverUtil._
+
+class NLTemplateSolver(ctx: InferenceContext, program: Program,
+ rootFun: FunDef, ctrTracker: ConstraintTracker,
+ minimizer: Option[(Expr, Model) => Model])
extends TemplateSolver(ctx, rootFun, ctrTracker) {
//flags controlling debugging
@@ -49,12 +53,11 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
val printCallConstriants = false
val dumpInstantiatedVC = false
- private val program = ctx.program
- private val timeout = ctx.timeout
+ private val timeout = ctx.vcTimeout
private val leonctx = ctx.leonContext
//flag controlling behavior
- private val farkasSolver = new FarkasLemmaSolver(ctx)
+ private val farkasSolver = new FarkasLemmaSolver(ctx, program)
private val startFromEarlierModel = true
private val disableCegis = true
private val useIncrementalSolvingForVCs = true
@@ -84,7 +87,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
} else
splitVC(fd)
- if (Util.hasReals(rest) && Util.hasInts(rest))
+ if (hasReals(rest) && hasInts(rest))
throw new IllegalStateException("Non-param Part has both integers and reals: " + rest)
val vcSolver =
@@ -95,7 +98,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
vcSolver.assertCnstr(rest)
if (debugIncrementalVC) {
- assert(Util.getTemplateVars(rest).isEmpty)
+ assert(getTemplateVars(rest).isEmpty)
println("For function: " + fd.id)
println("Param part: " + paramPart)
/*vcSolver.check match {
@@ -178,6 +181,8 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
val (res, newCtr, newModel, newdisjs, newcalls) = invalidateSATDisjunct(inputCtr, model)
res match {
+ case _ if ctx.abort =>
+ (None, None)
case None => {
//here, we cannot proceed and have to return unknown
//However, we can return the calls that need to be unrolled
@@ -219,7 +224,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
val tempIds = model.map(_._1)
val tempVarMap: Map[Expr, Expr] = model.map((elem) => (elem._1.toVariable, elem._2)).toMap
- val inputSize = Util.atomNum(inputCtr)
+ val inputSize = atomNum(inputCtr)
var disjsSolvedInIter = Seq[Expr]()
var callsInPaths = Set[Call]()
@@ -247,7 +252,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
case (Some(acc), fd) =>
val disableCounterExs = if (seenPaths.contains(fd)) {
blockedCEs = true
- Not(Util.createOr(seenPaths(fd)))
+ Not(createOr(seenPaths(fd)))
} else tru
getUNSATConstraints(fd, model, disableCounterExs) match {
case None =>
@@ -288,8 +293,8 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
}
} else {
//check that the new constraints does not have any reals
- val newPart = Util.createAnd(newctrs)
- val newSize = Util.atomNum(newPart)
+ val newPart = createAnd(newctrs)
+ val newSize = atomNum(newPart)
Stats.updateCounterStats((newSize + inputSize), "NLsize", "disjuncts")
if (verbose)
reporter.info("# of atomic predicates: " + newSize + " + " + inputSize)
@@ -297,6 +302,9 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
val combCtr = And(prevCtr, newPart)
val (res, newModel) = farkasSolver.solveFarkasConstraints(combCtr)
res match {
+ case _ if ctx.abort =>
+ // stop immediately
+ (None, tru, Model.empty)
case None => {
//here we have timed out while solving the non-linear constraints
if (verbose)
@@ -305,7 +313,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
else
reporter.info("NLsolver timed-out on the disjunct... blocking this disjunct...")
if (!this.disableCegis) {
- val (cres, cctr, cmodel) = solveWithCegis(tempIds.toSet, Util.createOr(confDisjuncts), inputCtr, Some(model))
+ val (cres, cctr, cmodel) = solveWithCegis(tempIds.toSet, createOr(confDisjuncts), inputCtr, Some(model))
cres match {
case Some(true) => {
disjsSolvedInIter ++= confDisjuncts
@@ -355,7 +363,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
def solveWithCegis(tempIds: Set[Identifier], expr: Expr, precond: Expr, initModel: Option[Model]): (Option[Boolean], Expr, Model) = {
- val cegisSolver = new CegisCore(ctx, timeout, this)
+ val cegisSolver = new CegisCore(ctx, program, timeout.toInt, this)
val (res, ctr, model) = cegisSolver.solve(tempIds, expr, precond, solveAsInt = false, initModel)
if (!res.isDefined)
reporter.info("cegis timed-out on the disjunct...")
@@ -374,7 +382,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
def getUNSATConstraints(fd: FunDef, inModel: Model, disableCounterExs: Expr): Option[((Expr, Set[Call]), Expr)] = {
val tempVarMap: Map[Expr, Expr] = inModel.map((elem) => (elem._1.toVariable, elem._2)).toMap
- val innerSolver =
+ val solver =
if (this.useIncrementalSolvingForVCs) vcSolvers(fd)
else new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver
val instExpr = if (this.useIncrementalSolvingForVCs) {
@@ -399,26 +407,28 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
wr.flush()
wr.close()
}
- if (Util.hasMixedIntReals(instExpr)) {
+ if (hasMixedIntReals(instExpr)) {
throw new IllegalStateException("Instantiated VC of " + fd.id + " contains mixed integer/reals: " + instExpr)
}
//reporter.info("checking VC inst ...")
var t1 = System.currentTimeMillis()
- innerSolver.setTimeout(timeout * 1000)
+ solver.setTimeout(timeout * 1000)
val (res, model) = if (this.useIncrementalSolvingForVCs) {
- innerSolver.push
- innerSolver.assertCnstr(instExpr)
- val solRes = innerSolver.check match {
+ solver.push
+ solver.assertCnstr(instExpr)
+ // new InterruptOnSignal(solver).interruptOnSignal(ctx.abort)(
+ val solRes = solver.check match {
+ case _ if ctx.abort =>
+ (None, Model.empty)
case r @ Some(true) =>
- (r, innerSolver.getModel)
+ (r, solver.getModel)
case r => (r, Model.empty)
}
- innerSolver.pop()
+ solver.pop()
solRes
} else {
- val solver = SimpleSolverAPI(SolverFactory(() => innerSolver))
- solver.solveSAT(instExpr)
+ SimpleSolverAPI(SolverFactory(() => solver)).solveSAT(instExpr)
}
val vccTime = (System.currentTimeMillis() - t1)
@@ -429,7 +439,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
//for debugging
if (this.trackUnpackedVCCTime) {
val upVCinst = simplifyArithmetic(TemplateInstantiator.instantiate(ctrTracker.getVC(fd).unpackedExpr, tempVarMap))
- Stats.updateCounterStats(Util.atomNum(upVCinst), "UP-VC-size", "disjuncts")
+ Stats.updateCounterStats(atomNum(upVCinst), "UP-VC-size", "disjuncts")
t1 = System.currentTimeMillis()
val (res2, _) = SimpleSolverAPI(SolverFactory(() => new SMTLIBZ3Solver(leonctx, program))).solveSAT(upVCinst)
@@ -471,7 +481,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
}
}
- val evaluator = new DefaultEvaluator(leonctx, program) //as of now used only for debugging
+ lazy val evaluator = new DefaultEvaluator(leonctx, program) //as of now used only for debugging
//a helper method
//TODO: this should also handle reals
protected def doesSatisfyModel(expr: Expr, model: Model): Boolean = {
@@ -537,7 +547,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
//for debugging
if (this.debugChooseDisjunct || this.printPathToConsole || this.dumpPathAsSMTLIB || this.verifyInvariant) {
val pathctrs = satCtrs.map(_.toExpr)
- val plainFormula = Util.createAnd(pathctrs)
+ val plainFormula = createAnd(pathctrs)
val pathcond = simplifyArithmetic(plainFormula)
if (this.debugChooseDisjunct) {
@@ -549,7 +559,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
if (this.verifyInvariant) {
println("checking invariant for path...")
- val sat = Util.checkInvariant(pathcond, leonctx, program)
+ val sat = checkInvariant(pathcond, leonctx, program)
}
if (this.printPathToConsole) {
@@ -566,7 +576,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
if (this.dumpPathAsSMTLIB) {
val filename = "pathcond" + FileCountGUID.getID + ".smt2"
- Util.toZ3SMTLIB(pathcond, filename, "QF_NIA", leonctx, program)
+ toZ3SMTLIB(pathcond, filename, "QF_NIA", leonctx, program)
println("Path dumped to: " + filename)
}
}
@@ -617,15 +627,15 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
}
if (this.debugTheoryReduction) {
- val simpPathCond = Util.createAnd((lnctrs ++ temps).map(_.template).toSeq)
+ val simpPathCond = createAnd((lnctrs ++ temps).map(_.template).toSeq)
if (this.verifyInvariant) {
println("checking invariant for simp-path...")
- Util.checkInvariant(simpPathCond, leonctx, program)
+ checkInvariant(simpPathCond, leonctx, program)
}
}
if (this.trackNumericalDisjuncts) {
- numericalDisjuncts :+= Util.createAnd((lnctrs ++ temps).map(_.template).toSeq)
+ numericalDisjuncts :+= createAnd((lnctrs ++ temps).map(_.template).toSeq)
}
val (data, nlctr) = processNumCtrs(lnctrs.toSeq, temps.toSeq)
@@ -639,14 +649,14 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
//here we are invalidating A^~(B)
if (temps.isEmpty) {
//here ants ^ conseq is sat (otherwise we wouldn't reach here) and there is no way to falsify this path
- (Util.createAnd(lnctrs.map(_.toExpr)), fls)
+ (createAnd(lnctrs.map(_.toExpr)), fls)
} else {
if (this.debugElimination) {
//println("Path Constraints (before elim): "+(lnctrs ++ temps))
if (this.verifyInvariant) {
println("checking invariant for disjunct before elimination...")
- Util.checkInvariant(Util.createAnd((lnctrs ++ temps).map(_.template)), leonctx, program)
+ checkInvariant(createAnd((lnctrs ++ temps).map(_.template)), leonctx, program)
}
}
//compute variables to be eliminated
@@ -659,7 +669,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
Some((ctrs: Seq[LinearConstraint]) => {
//println("checking disjunct before elimination...")
//println("ctrs: "+ctrs)
- val debugRes = Util.checkInvariant(Util.createAnd((ctrs ++ temps).map(_.template)), leonctx, program)
+ val debugRes = checkInvariant(createAnd((ctrs ++ temps).map(_.template)), leonctx, program)
})
} else None
val elimLnctrs = LinearConstraintUtil.apply1PRuleOnDisjunct(lnctrs, elimVars, debugger)
@@ -669,7 +679,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
println("Path constriants (after elimination): " + elimLnctrs)
if (this.verifyInvariant) {
println("checking invariant for disjunct after elimination...")
- Util.checkInvariant(Util.createAnd((elimLnctrs ++ temps).map(_.template)), leonctx, program)
+ checkInvariant(createAnd((elimLnctrs ++ temps).map(_.template)), leonctx, program)
}
}
//for stats
@@ -701,7 +711,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
//TODO: Use the dependence chains in the formulas to identify what to assertionize
// and what can never be implied by solving for the templates
- val disjunct = Util.createAnd((newLnctrs ++ temps).map(_.template))
+ val disjunct = createAnd((newLnctrs ++ temps).map(_.template))
val implCtrs = farkasSolver.constraintsForUnsat(newLnctrs, temps)
//for debugging
@@ -709,7 +719,7 @@ class NLTemplateSolver(ctx: InferenceContext, rootFun: FunDef, ctrTracker: Const
println("Final Path Constraints: " + disjunct)
if (this.verifyInvariant) {
println("checking invariant for final disjunct... ")
- Util.checkInvariant(disjunct, leonctx, program)
+ checkInvariant(disjunct, leonctx, program)
}
}
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
index 10a232e3fcb4730a4e2d3026ebd5f92db2f51ee5..a2a6524c6d6f52ffa232129b4adb2ff0f794ee42 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
@@ -16,22 +16,25 @@ import invariant.engine._
import invariant.factories._
import invariant.util._
import invariant.structure._
+import Util._
+import PredicateUtil._
+import SolverUtil._
-class NLTemplateSolverWithMult(ctx : InferenceContext, rootFun: FunDef,
+class NLTemplateSolverWithMult(ctx : InferenceContext, program: Program, rootFun: FunDef,
ctrTracker: ConstraintTracker, minimizer: Option[(Expr, Model) => Model])
- extends NLTemplateSolver(ctx, rootFun, ctrTracker, minimizer) {
+ extends NLTemplateSolver(ctx, program, rootFun, ctrTracker, minimizer) {
val axiomFactory = new AxiomFactory(ctx)
override def getVCForFun(fd: FunDef): Expr = {
val plainvc = ctrTracker.getVC(fd).toExpr
- val nlvc = Util.multToTimes(plainvc)
+ val nlvc = multToTimes(plainvc)
nlvc
}
override def splitVC(fd: FunDef) : (Expr,Expr) = {
val (paramPart, rest) = ctrTracker.getVC(fd).splitParamPart
- (Util.multToTimes(paramPart),Util.multToTimes(rest))
+ (multToTimes(paramPart),multToTimes(rest))
}
override def axiomsForTheory(formula : Formula, calls: Set[Call], model: Model) : Seq[Constraint] = {
@@ -61,7 +64,7 @@ class NLTemplateSolverWithMult(ctx : InferenceContext, rootFun: FunDef,
}
def isMultOp(call : Call) : Boolean = {
- Util.isMultFunctions(call.fi.tfd.fd)
+ isMultFunctions(call.fi.tfd.fd)
}
def unaryMultAxioms(formula: Formula, calls: Set[Call], predEval: (Expr => Boolean)) : Seq[Expr] = {
@@ -81,7 +84,7 @@ class NLTemplateSolverWithMult(ctx : InferenceContext, rootFun: FunDef,
def binaryMultAxioms(formula: Formula, calls: Set[Call], predEval: (Expr => Boolean)) : Seq[Expr] = {
val mults = calls.filter(call => isMultOp(call) && axiomFactory.hasBinaryAxiom(call))
- val product = Util.cross(mults,mults).collect{ case (c1,c2) if c1 != c2 => (c1,c2) }
+ val product = cross(mults,mults).collect{ case (c1,c2) if c1 != c2 => (c1,c2) }
ctx.reporter.info("Theory axioms: "+product.size)
Stats.updateCumStats(product.size, "-Total-theory-axioms")
diff --git a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
index 9b360c2db7d2f4442fb253e7fed58a0079b44c84..b373c5e7045aab99264c5403648c2ac968b48ef5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
@@ -19,6 +19,7 @@ import invariant.util._
import invariant.structure._
import invariant.structure.FunctionUtils._
import leon.solvers.Model
+import PredicateUtil._
abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
ctrTracker: ConstraintTracker) {
@@ -33,7 +34,6 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
private val dumpVCtoConsole = false
private val dumpVCasText = false
- private val dumpVCasSMTLIB = false
/**
* Completes a model by adding mapping to new template variables
@@ -73,7 +73,7 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
val vc = if (ctx.usereals)
ExpressionTransformer.IntLiteralToReal(getVCForFun(fd))
else getVCForFun(fd)
- if (dumpVCtoConsole || dumpVCasText || dumpVCasSMTLIB) {
+ if (dumpVCtoConsole || dumpVCasText) {
//val simpForm = simplifyArithmetic(vc)
val filename = "vc-" + FileCountGUID.getID
if (dumpVCtoConsole) {
@@ -87,15 +87,11 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
wr.flush()
wr.close()
}
- if (dumpVCasSMTLIB) {
- Util.toZ3SMTLIB(vc, filename + ".smt2", "QF_LIA", ctx.leonContext, ctx.program)
- println("Printed VC of " + fd.id + " to file: " + filename)
- }
}
if (ctx.dumpStats) {
- Stats.updateCounterStats(Util.atomNum(vc), "VC-size", "VC-refinement")
- Stats.updateCounterStats(Util.numUIFADT(vc), "UIF+ADT", "VC-refinement")
+ Stats.updateCounterStats(atomNum(vc), "VC-size", "VC-refinement")
+ Stats.updateCounterStats(numUIFADT(vc), "UIF+ADT", "VC-refinement")
}
(fd -> vc)
}).toMap
@@ -105,7 +101,7 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
//val tempOption = if (fd.hasTemplate) Some(fd.getTemplate) else None
//if (!tempOption.isDefined) acc
//else
- acc ++ Util.getTemplateIds(vc)
+ acc ++ getTemplateIds(vc)
}
Stats.updateCounterStats(tempIds.size, "TemplateIds", "VC-refinement")
diff --git a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
index fb7519850bcebaafab437f1d270f2f9d37417dc9..f41ec7e8963a45978fb4a9ac3fe091de48140d10 100644
--- a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
@@ -8,10 +8,13 @@ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
import java.io._
-import leon.invariant.util.UndirectedGraph
+import invariant.datastructure.UndirectedGraph
import scala.util.control.Breaks._
import invariant.util._
import leon.purescala.TypeOps
+import PredicateUtil._
+import SolverUtil._
+import Util._
class UFADTEliminator(ctx: LeonContext, program: Program) {
@@ -32,7 +35,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
val product = vec.foldLeft(Set[(Expr, Expr)]())((acc, call) => {
//an optimization: here we can exclude calls to maxFun from axiomatization, they will be inlined anyway
- /*val shouldConsider = if(InvariantUtil.isCallExpr(call)) {
+ /*val shouldConsider = if(InvariantisCallExpr(call)) {
val BinaryOperator(_,FunctionInvocation(calledFun,_), _) = call
if(calledFun == DepthInstPhase.maxFun) false
else true
@@ -88,7 +91,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
val Operator(Seq(r2 @ Variable(_), _), _) = call2
val resEquals = predEval(Equals(r1, r2))
if (resEquals) {
- if (Util.isCallExpr(call1)) {
+ if (isCallExpr(call1)) {
val (ants, _) = axiomatizeCalls(call1, call2)
val antsHold = ants.forall(ant => {
val Operator(Seq(lvar @ Variable(_), rvar @ Variable(_)), _) = ant
@@ -102,7 +105,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
def predForEquality(call1: Expr, call2: Expr): Seq[Expr] = {
- val eqs = if (Util.isCallExpr(call1)) {
+ val eqs = if (isCallExpr(call1)) {
val (_, rhs) = axiomatizeCalls(call1, call2)
Seq(rhs)
} else {
@@ -125,7 +128,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
def predForDisequality(call1: Expr, call2: Expr): Seq[Expr] = {
- val (ants, _) = if (Util.isCallExpr(call1)) {
+ val (ants, _) = if (isCallExpr(call1)) {
axiomatizeCalls(call1, call2)
} else {
axiomatizeADTCons(call1, call2)
diff --git a/src/main/scala/leon/invariant/util/CallGraph.scala b/src/main/scala/leon/invariant/util/CallGraph.scala
index 73ac3b099389eb33223d83302bc74b82d3b1547f..23f87d5bc0b62163ef40e852d7cc0af0cd658bc3 100644
--- a/src/main/scala/leon/invariant/util/CallGraph.scala
+++ b/src/main/scala/leon/invariant/util/CallGraph.scala
@@ -8,8 +8,10 @@ import purescala.Expressions._
import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
+import ProgramUtil._
import Util._
import invariant.structure.FunctionUtils._
+import invariant.datastructure._
/**
* This represents a call graph of the functions in the program
diff --git a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
index e38bdf3aa5cc3dd7d1f591bbee464e5dd19bd1a5..6750bd59c144fa656b2d820516d6691e3e169862 100644
--- a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
+++ b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
@@ -13,6 +13,8 @@ import purescala.ScalaPrinter
import invariant.structure.Call
import invariant.structure.FunctionUtils._
import leon.invariant.factories.TemplateIdFactory
+import PredicateUtil._
+import Util._
/**
* A collection of transformation on expressions and some utility methods.
@@ -40,17 +42,17 @@ object ExpressionTransformer {
case And(args) if !insideFunction => {
val newargs = args.map((arg) => {
val (nexp, ncjs) = transformer(arg, false)
- Util.createAnd(nexp +: ncjs.toSeq)
+ createAnd(nexp +: ncjs.toSeq)
})
- (Util.createAnd(newargs), Set())
+ (createAnd(newargs), Set())
}
case Or(args) if !insideFunction => {
val newargs = args.map((arg) => {
val (nexp, ncjs) = transformer(arg, false)
- Util.createAnd(nexp +: ncjs.toSeq)
+ createAnd(nexp +: ncjs.toSeq)
})
- (Util.createOr(newargs), Set())
+ (createOr(newargs), Set())
}
case t: Terminal => (t, Set())
@@ -117,7 +119,7 @@ object ExpressionTransformer {
val mult = multop(quo, rhs)
val divsem = Equals(lhs, Plus(mult, rem))
//TODO: here, we have to use |rhs|
- val newexpr = Util.createAnd(Seq(divsem, LessEquals(zero, rem), LessEquals(rem, Minus(rhs, one))))
+ val newexpr = createAnd(Seq(divsem, LessEquals(zero, rem), LessEquals(rem, Minus(rhs, one))))
val resset = transform(newexpr, true)
(quo, resset._2 + resset._1)
}
@@ -184,7 +186,7 @@ object ExpressionTransformer {
}
val (nexp, ncjs) = transform(inexpr, false)
val res = if (!ncjs.isEmpty) {
- Util.createAnd(nexp +: ncjs.toSeq)
+ createAnd(nexp +: ncjs.toSeq)
} else nexp
res
}
@@ -306,7 +308,7 @@ object ExpressionTransformer {
val (nexp, ncjs) = flattenFunc(inExpr, false)
if (!ncjs.isEmpty) {
- Util.createAnd(nexp +: ncjs.toSeq)
+ createAnd(nexp +: ncjs.toSeq)
} else nexp
}
@@ -327,8 +329,8 @@ object ExpressionTransformer {
case Not(Not(e1)) => nnf(e1)
case e @ Not(t: Terminal) => e
case e @ Not(FunctionInvocation(_, _)) => e
- case Not(And(args)) => Util.createOr(args.map(arg => nnf(Not(arg))))
- case Not(Or(args)) => Util.createAnd(args.map(arg => nnf(Not(arg))))
+ case Not(And(args)) => createOr(args.map(arg => nnf(Not(arg))))
+ case Not(Or(args)) => createAnd(args.map(arg => nnf(Not(arg))))
case Not(e @ Operator(Seq(e1, e2), op)) => {
//matches integer binary relation or a boolean equality
if (e1.getType == BooleanType || e1.getType == Int32Type || e1.getType == RealType || e1.getType == IntegerType) {
@@ -391,14 +393,14 @@ object ExpressionTransformer {
case Or(inArgs) => acc ++ inArgs
case _ => acc :+ arg
})
- Util.createOr(newArgs)
+ createOr(newArgs)
}
case And(args) => {
val newArgs = args.foldLeft(Seq[Expr]())((acc, arg) => arg match {
case And(inArgs) => acc ++ inArgs
case _ => acc :+ arg
})
- Util.createAnd(newArgs)
+ createAnd(newArgs)
}
case _ => e
})(expr)
@@ -474,7 +476,7 @@ object ExpressionTransformer {
case _ => e
})(ine)
val closure = (e: Expr) => replace(tempMap, e)
- Util.fix(closure)(newinst)
+ fix(closure)(newinst)
}
/**
@@ -626,7 +628,7 @@ object ExpressionTransformer {
def distribute(e: Expr): Expr = {
simplePreTransform(_ match {
- case e @ FunctionInvocation(TypedFunDef(fd, _), Seq(e1, e2)) if Util.isMultFunctions(fd) =>
+ case e @ FunctionInvocation(TypedFunDef(fd, _), Seq(e1, e2)) if isMultFunctions(fd) =>
val newe = (e1, e2) match {
case (Plus(sum1, sum2), _) =>
// distribute e2 over e1
diff --git a/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala b/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
index 966121756fd62e0ef2d517f8ad99153b161858fb..bd99992014bd94ab29c099b7a03eb7e452e154c0 100644
--- a/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
+++ b/src/main/scala/leon/invariant/util/LetTupleSimplifications.scala
@@ -11,6 +11,7 @@ import java.io._
import java.io._
import purescala.ScalaPrinter
import leon.utils._
+import PredicateUtil._
import invariant.structure.Call
import invariant.structure.FunctionUtils._
@@ -178,7 +179,7 @@ object LetTupleSimplification {
}
val newargs: Seq[Expr] = args.map(simplifyArithmetic)
val Seq(arg1: Expr, arg2: Expr) = newargs
- val simpval = if (!Util.hasCalls(arg1) && !Util.hasCalls(arg2)) {
+ val simpval = if (!hasCalls(arg1) && !hasCalls(arg2)) {
import invariant.structure.LinearConstraintUtil._
val lt = exprToTemplate(LessEquals(Minus(arg1, arg2), InfiniteIntegerLiteral(0)))
//now, check if all the variables in 'lt' have only positive coefficients
diff --git a/src/main/scala/leon/invariant/util/Minimizer.scala b/src/main/scala/leon/invariant/util/Minimizer.scala
index 78e82db2d233d1b980206c96a5bc86a7696611d2..f9ee65b007147b245330ede807e959a25411e3c0 100644
--- a/src/main/scala/leon/invariant/util/Minimizer.scala
+++ b/src/main/scala/leon/invariant/util/Minimizer.scala
@@ -16,8 +16,9 @@ import invariant.engine.InferenceContext
import invariant.factories._
import leon.invariant.templateSolvers.ExtendedUFSolver
import leon.invariant.util.RealValuedExprEvaluator._
+import invariant.util.TimerUtil._
-class Minimizer(ctx: InferenceContext) {
+class Minimizer(ctx: InferenceContext, program: Program) {
val verbose = false
val debugMinimization = false
@@ -26,14 +27,11 @@ class Minimizer(ctx: InferenceContext) {
* TODO: make sure that the template for rootFun is the time template
*/
val MaxIter = 16 //note we may not be able to represent anything beyond 2^16
- /*val MaxInt = Int.MaxValue
- val sqrtMaxInt = 45000 //this is a number that is close a sqrt of 2^31
-*/ val half = FractionalLiteral(1, 2)
+ val half = FractionalLiteral(1, 2)
val two = FractionalLiteral(2, 1)
val rzero = FractionalLiteral(0, 1)
val mone = FractionalLiteral(-1, 1)
- private val program = ctx.program
private val leonctx = ctx.leonContext
val reporter = leonctx.reporter
@@ -57,10 +55,8 @@ class Minimizer(ctx: InferenceContext) {
val orderedTempVars = nestMap.toSeq.sortWith((a, b) => a._2 >= b._2).map(_._1)
//do a binary search sequentially on each of these tempvars
// note: use smtlib solvers so that they can be timedout
- val solver = SimpleSolverAPI(
- new TimeoutSolverFactory(SolverFactory(() =>
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), ctx.timeout * 1000))
- //new ExtendedUFSolver(leonctx, program) with TimeoutSolver), ctx.timeout * 1000))
+ val solver = new SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
+ new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), ctx.vcTimeout * 1000))
reporter.info("minimizing...")
var currentModel = initModel
@@ -115,7 +111,7 @@ class Minimizer(ctx: InferenceContext) {
}
}
}
- } while (continue && iter < MaxIter)
+ } while (!ctx.abort && continue && iter < MaxIter)
//this is the last ditch effort to make the upper bound constant smaller.
//check if the floor of the upper-bound is a solution
val currval @ FractionalLiteral(n, d) =
@@ -124,7 +120,7 @@ class Minimizer(ctx: InferenceContext) {
} else {
initModel(tvar.id).asInstanceOf[FractionalLiteral]
}
- if (d != 1) {
+ if (d != 1 && !ctx.abort) {
val (res, newModel) = solver.solveSAT(And(acc, Equals(tvar, floor(currval))))
if (res == Some(true))
updateState(newModel)
@@ -151,7 +147,7 @@ class Minimizer(ctx: InferenceContext) {
val (res, newModel) = solver.solveSAT(And(nlctr, Equals(tvar, flval)))
res match {
case Some(true) => Some(newModel)
- case _ => None
+ case _ => None
}
} else None
}
@@ -191,10 +187,10 @@ class Minimizer(ctx: InferenceContext) {
0
}
case FunctionInvocation(_, args) => 1 + args.foldLeft(0)((acc, arg) => acc + functionNesting(arg))
- case t: Terminal => 0
+ case t: Terminal => 0
/*case UnaryOperator(arg, _) => functionNesting(arg)
case BinaryOperator(a1, a2, _) => functionNesting(a1) + functionNesting(a2)*/
- case Operator(args, _) => args.foldLeft(0)((acc, arg) => acc + functionNesting(arg))
+ case Operator(args, _) => args.foldLeft(0)((acc, arg) => acc + functionNesting(arg))
}
}
functionNesting(template)
diff --git a/src/main/scala/leon/invariant/util/RealToIntExpr.scala b/src/main/scala/leon/invariant/util/RealToIntExpr.scala
new file mode 100644
index 0000000000000000000000000000000000000000..54650b2c4111b32e127070cdc23889708a81b6fd
--- /dev/null
+++ b/src/main/scala/leon/invariant/util/RealToIntExpr.scala
@@ -0,0 +1,73 @@
+package leon
+package invariant.util
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Extractors._
+import purescala.Types._
+import leon.invariant._
+import invariant.factories._
+import solvers._
+
+/**
+ * maps all real valued variables and literals to new integer variables/literals and
+ * performs the reverse mapping
+ * Note: this should preserve the template identifier property
+ */
+class RealToInt {
+
+ val bone = BigInt(1)
+ var realToIntId = Map[Identifier, Identifier]()
+ var intToRealId = Map[Identifier, Identifier]()
+
+ def mapRealToInt(inexpr: Expr): Expr = {
+ val transformer = (e: Expr) => e match {
+ case FractionalLiteral(num, `bone`) => InfiniteIntegerLiteral(num)
+ case FractionalLiteral(_, _) => throw new IllegalStateException("Real literal with non-unit denominator")
+ case v @ Variable(realId) if (v.getType == RealType) => {
+ val newId = realToIntId.getOrElse(realId, {
+ //note: the fresh identifier has to be a template identifier if the original one is a template identifier
+ val freshId = if (TemplateIdFactory.IsTemplateIdentifier(realId))
+ TemplateIdFactory.freshIdentifier(realId.name, IntegerType)
+ else
+ FreshIdentifier(realId.name, IntegerType, true)
+
+ realToIntId += (realId -> freshId)
+ intToRealId += (freshId -> realId)
+ freshId
+ })
+ Variable(newId)
+ }
+ case _ => e
+ }
+ simplePostTransform(transformer)(inexpr)
+ }
+
+ def unmapModel(model: Model): Model = {
+ new Model(model.map(pair => {
+ val (key, value) = if (intToRealId.contains(pair._1)) {
+ (intToRealId(pair._1),
+ pair._2 match {
+ case InfiniteIntegerLiteral(v) => FractionalLiteral(v.toInt, 1)
+ case _ => pair._2
+ })
+ } else pair
+ (key -> value)
+ }).toMap)
+ }
+
+ def mapModel(model: Model): Model = {
+ new Model(model.collect {
+ case (k, FractionalLiteral(n, bone)) =>
+ (realToIntId(k), InfiniteIntegerLiteral(n))
+ case (k, v) =>
+ if (realToIntId.contains(k)) {
+ (realToIntId(k), v)
+ } else {
+ (k, v)
+ }
+ }.toMap)
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/util/SolverUtil.scala b/src/main/scala/leon/invariant/util/SolverUtil.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e67385c435ea94b24ef63ed8fe8bdbf41f602570
--- /dev/null
+++ b/src/main/scala/leon/invariant/util/SolverUtil.scala
@@ -0,0 +1,133 @@
+package leon
+package invariant.util
+
+import utils._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Extractors._
+import purescala.Types._
+import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
+import leon.invariant._
+import solvers.z3._
+import solvers._
+import invariant.engine._
+import invariant.factories._
+import invariant.structure._
+import FunctionUtils._
+import leon.invariant.templateSolvers.ExtendedUFSolver
+import java.io._
+import Util._
+import PredicateUtil._
+
+object SolverUtil {
+
+ def modelToExpr(model: Model): Expr = {
+ model.foldLeft(tru: Expr)((acc, elem) => {
+ val (k, v) = elem
+ val eq = Equals(k.toVariable, v)
+ if (acc == tru) eq
+ else And(acc, eq)
+ })
+ }
+
+ def toZ3SMTLIB(expr: Expr, filename: String,
+ theory: String, ctx: LeonContext, pgm: Program,
+ useBitvectors: Boolean = false,
+ bitvecSize: Int = 32) = {
+ //create new solver, assert constraints and print
+ val printSol = new ExtendedUFSolver(ctx, pgm)
+ printSol.assertCnstr(expr)
+ val writer = new PrintWriter(filename)
+ writer.println(printSol.ctrsToString(theory))
+ printSol.free()
+ writer.flush()
+ writer.close()
+ }
+
+ /**
+ * A helper function that can be used to hardcode an invariant and see if it unsatifies the paths
+ */
+ def checkInvariant(expr: Expr, ctx: LeonContext, prog: Program): Option[Boolean] = {
+ val idmap: Map[Expr, Expr] = variablesOf(expr).collect {
+ case id @ _ if (id.name.toString == "a?") => id.toVariable -> InfiniteIntegerLiteral(6)
+ case id @ _ if (id.name.toString == "c?") => id.toVariable -> InfiniteIntegerLiteral(2)
+ }.toMap
+ //println("found ids: " + idmap.keys)
+ if (!idmap.keys.isEmpty) {
+ val newpathcond = replace(idmap, expr)
+ //check if this is solvable
+ val solver = SimpleSolverAPI(SolverFactory(() => new ExtendedUFSolver(ctx, prog)))
+ solver.solveSAT(newpathcond)._1 match {
+ case Some(true) => {
+ println("Path satisfiable for a?,c? -->6,2 ")
+ Some(true)
+ }
+ case _ => {
+ println("Path unsat for a?,c? --> 6,2")
+ Some(false)
+ }
+ }
+ } else None
+ }
+
+ def collectUNSATCores(ine: Expr, ctx: LeonContext, prog: Program): Expr = {
+ var controlVars = Map[Variable, Expr]()
+ var newEqs = Map[Expr, Expr]()
+ val solver = new ExtendedUFSolver(ctx, prog)
+ val newe = simplePostTransform((e: Expr) => e match {
+ case And(_) | Or(_) => {
+ val v = TVarFactory.createTemp("a", BooleanType).toVariable
+ newEqs += (v -> e)
+ val newe = Equals(v, e)
+
+ //create new variable and add it in disjunction
+ val cvar = FreshIdentifier("ctrl", BooleanType, true).toVariable
+ controlVars += (cvar -> newe)
+ solver.assertCnstr(Or(newe, cvar))
+ v
+ }
+ case _ => e
+ })(ine)
+ //create new variable and add it in disjunction
+ val cvar = FreshIdentifier("ctrl", BooleanType, true).toVariable
+ controlVars += (cvar -> newe)
+ solver.assertCnstr(Or(newe, cvar))
+
+ val res = solver.checkAssumptions(controlVars.keySet.map(Not.apply _))
+ println("Result: " + res)
+ val coreExprs = solver.getUnsatCore
+ val simpcores = coreExprs.foldLeft(Seq[Expr]())((acc, coreExp) => {
+ val Not(cvar @ Variable(_)) = coreExp
+ val newexp = controlVars(cvar)
+ //println("newexp: "+newexp)
+ newexp match {
+ // case Iff(v@Variable(_),rhs) if(newEqs.contains(v)) => acc
+ case Equals(v @ Variable(_), rhs) if (v.getType == BooleanType && rhs.getType == BooleanType && newEqs.contains(v)) => acc
+ case _ => {
+ acc :+ newexp
+ }
+ }
+ })
+ val cores = Util.fix((e: Expr) => replace(newEqs, e))(createAnd(simpcores.toSeq))
+
+ solver.free
+ //cores
+ ExpressionTransformer.unFlatten(cores,
+ variablesOf(ine).filterNot(TVarFactory.isTemporary _))
+ }
+
+ //tests if the solver uses nlsat
+ def usesNLSat(solver: AbstractZ3Solver) = {
+ //check for nlsat
+ val x = FreshIdentifier("x", RealType).toVariable
+ val testExpr = Equals(Times(x, x), FractionalLiteral(2, 1))
+ solver.assertCnstr(testExpr)
+ solver.check match {
+ case Some(true) => true
+ case _ => false
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/util/TemporaryVarFactory.scala b/src/main/scala/leon/invariant/util/TemporaryVarFactory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c85c7837b1c4dbf35e2a90b87d93bccca929a6c9
--- /dev/null
+++ b/src/main/scala/leon/invariant/util/TemporaryVarFactory.scala
@@ -0,0 +1,31 @@
+package leon
+package invariant.util
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
+import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
+
+object TVarFactory {
+
+ val temporaries = MutableSet[Identifier]()
+ //these are dummy identifiers used in 'CaseClassSelector' conversion
+ val dummyIds = MutableSet[Identifier]()
+
+ def createTemp(name: String, tpe: TypeTree = Untyped): Identifier = {
+ val freshid = FreshIdentifier(name, tpe, true)
+ temporaries.add(freshid)
+ freshid
+ }
+
+ def createDummy(tpe: TypeTree): Identifier = {
+ val freshid = FreshIdentifier("dy", tpe, true)
+ dummyIds.add(freshid)
+ freshid
+ }
+
+ def isTemporary(id: Identifier): Boolean = temporaries.contains(id)
+ def isDummy(id: Identifier): Boolean = dummyIds.contains(id)
+}
diff --git a/src/main/scala/leon/invariant/util/TimerUtil.scala b/src/main/scala/leon/invariant/util/TimerUtil.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1284951709d4c374c56f1115b8b946f1a796855d
--- /dev/null
+++ b/src/main/scala/leon/invariant/util/TimerUtil.scala
@@ -0,0 +1,64 @@
+package leon
+package invariant.util
+
+import utils._
+import solvers._
+import invariant.engine._
+import purescala.Expressions._
+
+object TimerUtil {
+ /**
+ * Timeout in milliseconds
+ */
+ def scheduleTask(callBack: () => Unit, timeOut: Long): Option[java.util.Timer] = {
+ if (timeOut > 0) {
+ val timer = new java.util.Timer();
+ timer.schedule(new java.util.TimerTask() {
+ def run() {
+ callBack()
+ timer.cancel() //the timer will be cancelled after it runs
+ }
+ }, timeOut);
+ Some(timer)
+ } else None
+ }
+}
+
+class InterruptOnSignal(it: Interruptible) {
+
+ private class Poll(signal: => Boolean, onSignal: => Unit) extends Thread {
+ private var keepRunning = true
+
+ override def run(): Unit = {
+ val startTime: Long = System.currentTimeMillis
+ while (!signal && keepRunning) {
+ Thread.sleep(100) // a relatively infrequent poll
+ }
+ if (signal && keepRunning) {
+ onSignal
+ }
+ }
+
+ def finishedRunning(): Unit = {
+ keepRunning = false
+ }
+ }
+
+ def interruptOnSignal[T](signal: => Boolean)(body: => T): T = {
+ var recdSignal = false
+
+ val timer = new Poll(signal, {
+ it.interrupt()
+ recdSignal = true
+ })
+
+ timer.start()
+ val res = body
+ timer.finishedRunning()
+
+ if (recdSignal) {
+ it.recoverInterrupt()
+ }
+ res
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/util/TreeUtil.scala b/src/main/scala/leon/invariant/util/TreeUtil.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6e3e45f22a49bc3ef70d0d18e3d0371fedac2654
--- /dev/null
+++ b/src/main/scala/leon/invariant/util/TreeUtil.scala
@@ -0,0 +1,360 @@
+package leon
+package invariant.util
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Extractors._
+import purescala.Types._
+import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
+import leon.invariant._
+import invariant.engine._
+import invariant.factories._
+import invariant.structure._
+import FunctionUtils._
+import scala.annotation.tailrec
+import PredicateUtil._
+import ProgramUtil._
+import Util._
+import solvers._
+import purescala.DefOps._
+
+object ProgramUtil {
+
+ def createLeonContext(ctx: LeonContext, opts: String*): LeonContext = {
+ Main.processOptions(opts.toList).copy(reporter = ctx.reporter,
+ interruptManager = ctx.interruptManager, files = ctx.files, timers = ctx.timers)
+ }
+
+ /**
+ * Here, we exclude empty units that do not have any modules and empty
+ * modules that do not have any definitions
+ */
+ def copyProgram(prog: Program, mapdefs: (Seq[Definition] => Seq[Definition])): Program = {
+ prog.copy(units = prog.units.collect {
+ case unit if (!unit.defs.isEmpty) => unit.copy(defs = unit.defs.collect {
+ case module : ModuleDef if (!module.defs.isEmpty) =>
+ module.copy(defs = mapdefs(module.defs))
+ case other => other
+ })
+ })
+ }
+
+ def createTemplateFun(plainTemp: Expr): FunctionInvocation = {
+ val tmpl = Lambda(getTemplateIds(plainTemp).toSeq.map(id => ValDef(id)), plainTemp)
+ val tmplFd = new FunDef(FreshIdentifier("tmpl", FunctionType(Seq(tmpl.getType), BooleanType), false), Seq(), Seq(ValDef(FreshIdentifier("arg", tmpl.getType),
+ Some(tmpl.getType))), BooleanType)
+ tmplFd.body = Some(BooleanLiteral(true))
+ FunctionInvocation(TypedFunDef(tmplFd, Seq()), Seq(tmpl))
+ }
+
+ /**
+ * This is the default template generator.
+ * Note: we are not creating template for libraries.
+ */
+ def getOrCreateTemplateForFun(fd: FunDef): Expr = {
+ val plainTemp = if (fd.hasTemplate) fd.getTemplate
+ else if (fd.annotations.contains("library")) BooleanLiteral(true)
+ else {
+ //just consider all the arguments, return values that are integers
+ val baseTerms = fd.params.filter((vardecl) => isNumericType(vardecl.getType)).map(_.toVariable) ++
+ (if (isNumericType(fd.returnType)) Seq(getFunctionReturnVariable(fd))
+ else Seq())
+ val lhs = baseTerms.foldLeft(TemplateIdFactory.freshTemplateVar(): Expr)((acc, t) => {
+ Plus(Times(TemplateIdFactory.freshTemplateVar(), t), acc)
+ })
+ val tempExpr = LessEquals(lhs, InfiniteIntegerLiteral(0))
+ tempExpr
+ }
+ plainTemp
+ }
+
+ def mapFunctionsInExpr(funmap: Map[FunDef, FunDef])(ine: Expr): Expr = {
+ simplePostTransform((e: Expr) => e match {
+ case FunctionInvocation(tfd, args) if funmap.contains(tfd.fd) =>
+ FunctionInvocation(TypedFunDef(funmap(tfd.fd), tfd.tps), args)
+ case _ => e
+ })(ine)
+ }
+
+ /**
+ * For functions for which `funToTmpl` is not defined, their templates
+ * will be removed
+ */
+ def assignTemplateAndCojoinPost(funToTmpl: Map[FunDef, Expr], prog: Program,
+ funToPost: Map[FunDef, Expr] = Map(), uniqueIdDisplay : Boolean = true): Program = {
+
+ val funMap = functionsWOFields(prog.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
+ case (accMap, fd) if fd.isTheoryOperation =>
+ accMap + (fd -> fd)
+ case (accMap, fd) => {
+ val freshId = FreshIdentifier(fd.id.name, fd.returnType, uniqueIdDisplay)
+ val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
+ accMap.updated(fd, newfd)
+ }
+ }
+
+ // FIXME: This with createAnd (which performs simplifications) gives an error during composition.
+ val mapExpr = mapFunctionsInExpr(funMap) _
+ for ((from, to) <- funMap) {
+ to.fullBody = if (!funToTmpl.contains(from)) {
+ mapExpr {
+ from.fullBody match {
+ case Ensuring(b, post) =>
+ Ensuring(b,
+ Lambda(Seq(ValDef(getResId(from).get)),
+ createAnd(Seq(from.getPostWoTemplate, funToPost.getOrElse(from, tru)))))
+ case fb =>
+ fb
+ }
+ }
+ } else {
+ val newTmpl = createTemplateFun(funToTmpl(from))
+ mapExpr {
+ from.fullBody match {
+ case Require(pre, body) =>
+ val toPost =
+ Lambda(Seq(ValDef(FreshIdentifier("res", from.returnType))),
+ createAnd(Seq(newTmpl, funToPost.getOrElse(from, tru))))
+ Ensuring(Require(pre, body), toPost)
+
+ case Ensuring(Require(pre, body), post) =>
+ Ensuring(Require(pre, body),
+ Lambda(Seq(ValDef(getResId(from).get)),
+ createAnd(Seq(from.getPostWoTemplate, newTmpl, funToPost.getOrElse(from, tru)))))
+
+ case Ensuring(body, post) =>
+ Ensuring(body,
+ Lambda(Seq(ValDef(getResId(from).get)),
+ createAnd(Seq(from.getPostWoTemplate, newTmpl, funToPost.getOrElse(from, tru)))))
+
+ case body =>
+ val toPost =
+ Lambda(Seq(ValDef(FreshIdentifier("res", from.returnType))),
+ createAnd(Seq(newTmpl, funToPost.getOrElse(from, tru))))
+ Ensuring(body, toPost)
+ }
+ }
+ }
+ //copy annotations
+ from.flags.foreach(to.addFlag(_))
+ }
+ val newprog = copyProgram(prog, (defs: Seq[Definition]) => defs.map {
+ case fd: FunDef if funMap.contains(fd) =>
+ funMap(fd)
+ case d => d
+ })
+ newprog
+ }
+
+ def functionByName(nm: String, prog: Program) = {
+ prog.definedFunctions.find(fd => fd.id.name == nm)
+ }
+
+ def functionByFullName(nm: String, prog: Program) = {
+ prog.definedFunctions.find(fd => fullName(fd)(prog) == nm)
+ }
+
+ def functionsWOFields(fds: Seq[FunDef]): Seq[FunDef] = {
+ fds.filter(_.isRealFunction)
+ }
+
+ def translateExprToProgram(ine: Expr, currProg: Program, newProg: Program): Expr = {
+ simplePostTransform((e: Expr) => e match {
+ case FunctionInvocation(TypedFunDef(fd, tps), args) =>
+ functionByName(fullName(fd)(currProg), newProg) match {
+ case Some(nfd) =>
+ FunctionInvocation(TypedFunDef(nfd, tps), args)
+ case _ =>
+ throw new IllegalStateException(s"Cannot find translation for ${fd.id.name}")
+ }
+ case _ => e
+ })(ine)
+ }
+
+ def getFunctionReturnVariable(fd: FunDef) = {
+ if (fd.hasPostcondition) getResId(fd).get.toVariable
+ else ResultVariable(fd.returnType) /*FreshIdentifier("res", fd.returnType).toVariable*/
+ }
+
+ def getResId(funDef: FunDef): Option[Identifier] = {
+ funDef.fullBody match {
+ case Ensuring(_, post) => {
+ post match {
+ case Lambda(Seq(ValDef(fromRes, _)), _) => Some(fromRes)
+ }
+ }
+ case _ => None
+ }
+ }
+
+ //compute the formal to the actual argument mapping
+ def formalToActual(call: Call): Map[Expr, Expr] = {
+ val fd = call.fi.tfd.fd
+ val resvar = getFunctionReturnVariable(fd)
+ val argmap: Map[Expr, Expr] = Map(resvar -> call.retexpr) ++ fd.params.map(_.id.toVariable).zip(call.fi.args)
+ argmap
+ }
+}
+
+object PredicateUtil {
+
+ /**
+ * Checks if the input expression has only template variables as free variables
+ */
+ def isTemplateExpr(expr: Expr): Boolean = {
+ var foundVar = false
+ simplePostTransform((e: Expr) => e match {
+ case Variable(id) => {
+ if (!TemplateIdFactory.IsTemplateIdentifier(id))
+ foundVar = true
+ e
+ }
+ case ResultVariable(_) => {
+ foundVar = true
+ e
+ }
+ case _ => e
+ })(expr)
+
+ !foundVar
+ }
+
+ def getTemplateIds(expr: Expr) = {
+ variablesOf(expr).filter(TemplateIdFactory.IsTemplateIdentifier)
+ }
+
+ def getTemplateVars(expr: Expr): Set[Variable] = {
+ getTemplateIds(expr).map(_.toVariable)
+ }
+
+ /**
+ * Checks if the expression has real valued sub-expressions.
+ */
+ def hasReals(expr: Expr): Boolean = {
+ var foundReal = false
+ simplePostTransform((e: Expr) => e match {
+ case _ => {
+ if (e.getType == RealType)
+ foundReal = true;
+ e
+ }
+ })(expr)
+ foundReal
+ }
+
+ /**
+ * Checks if the expression has real valued sub-expressions.
+ * Note: important, <, <=, > etc have default int type.
+ * However, they can also be applied over real arguments
+ * So check only if all terminals are real
+ */
+ def hasInts(expr: Expr): Boolean = {
+ var foundInt = false
+ simplePostTransform((e: Expr) => e match {
+ case e: Terminal if (e.getType == Int32Type || e.getType == IntegerType) => {
+ foundInt = true;
+ e
+ }
+ case _ => e
+ })(expr)
+ foundInt
+ }
+
+ def hasMixedIntReals(expr: Expr): Boolean = {
+ hasInts(expr) && hasReals(expr)
+ }
+
+ def atomNum(e: Expr): Int = {
+ var count: Int = 0
+ simplePostTransform((e: Expr) => e match {
+ case And(args) => {
+ count += args.size
+ e
+ }
+ case Or(args) => {
+ count += args.size
+ e
+ }
+ case _ => e
+ })(e)
+ count
+ }
+
+ def numUIFADT(e: Expr): Int = {
+ var count: Int = 0
+ simplePostTransform((e: Expr) => e match {
+ case FunctionInvocation(_, _) | CaseClass(_, _) | Tuple(_) => {
+ count += 1
+ e
+ }
+ case _ => e
+ })(e)
+ count
+ }
+
+ def hasCalls(e: Expr) = numUIFADT(e) >= 1
+
+ def getCallExprs(ine: Expr): Set[Expr] = {
+ var calls = Set[Expr]()
+ simplePostTransform((e: Expr) => e match {
+ case call @ _ if isCallExpr(e) => {
+ calls += e
+ call
+ }
+ case _ => e
+ })(ine)
+ calls
+ }
+
+ def isCallExpr(e: Expr): Boolean = e match {
+ case Equals(Variable(_), FunctionInvocation(_, _)) => true
+ // case Iff(Variable(_),FunctionInvocation(_,_)) => true
+ case _ => false
+ }
+
+ def isADTConstructor(e: Expr): Boolean = e match {
+ case Equals(Variable(_), CaseClass(_, _)) => true
+ case Equals(Variable(_), Tuple(_)) => true
+ case _ => false
+ }
+
+ def isMultFunctions(fd: FunDef) = {
+ (fd.id.name == "mult" || fd.id.name == "pmult") &&
+ fd.isTheoryOperation
+ }
+
+ //replaces occurrences of mult by Times
+ def multToTimes(ine: Expr): Expr = {
+ simplePostTransform((e: Expr) => e match {
+ case FunctionInvocation(TypedFunDef(fd, _), args) if isMultFunctions(fd) => {
+ Times(args(0), args(1))
+ }
+ case _ => e
+ })(ine)
+ }
+
+ def createAnd(exprs: Seq[Expr]): Expr = {
+ val newExprs = exprs.filterNot(conj => conj == tru)
+ newExprs match {
+ case Seq() => tru
+ case Seq(e) => e
+ case _ => And(newExprs)
+ }
+ }
+
+ def createOr(exprs: Seq[Expr]): Expr = {
+ val newExprs = exprs.filterNot(disj => disj == fls)
+ newExprs match {
+ case Seq() => fls
+ case Seq(e) => e
+ case _ => Or(newExprs)
+ }
+ }
+
+ def isNumericType(t: TypeTree) = t match {
+ case IntegerType | RealType => true
+ case _ => false
+ }
+}
diff --git a/src/main/scala/leon/invariant/util/Util.scala b/src/main/scala/leon/invariant/util/Util.scala
index 5a101569e5832cfa1340508345cac38e74f1e2f1..f8358dec14f22f420a2b19b90dcf9dd9d308d80d 100644
--- a/src/main/scala/leon/invariant/util/Util.scala
+++ b/src/main/scala/leon/invariant/util/Util.scala
@@ -5,24 +5,10 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet, Map => MutableMap }
-import scala.collection.immutable.Stack
-import java.io._
-import leon.invariant._
-import java.io._
-import solvers.z3._
-import solvers._
-import invariant.engine._
-import invariant.factories._
-import invariant.structure._
import leon.purescala.PrettyPrintable
import leon.purescala.PrinterContext
import purescala.PrinterHelpers._
-import FunctionUtils._
-import leon.invariant.templateSolvers.ExtendedUFSolver
-import scala.annotation.tailrec
object FileCountGUID {
var fileCount = 0
@@ -51,46 +37,6 @@ case class ResultVariable(tpe: TypeTree) extends Expr with Terminal with PrettyP
}
}
-//this used to refer to the time steps of a procedure
-case class TimeVariable() extends Expr with Terminal with PrettyPrintable {
- val getType = IntegerType
- override def toString: String = "#time"
- def printWith(implicit pctx: PrinterContext) {
- p"#time"
- }
-}
-
-//this used to refer to the depth of a procedure
-case class DepthVariable() extends Expr with Terminal with PrettyPrintable {
- val getType = IntegerType
- override def toString: String = "#depth"
- def printWith(implicit pctx: PrinterContext) {
- p"#time"
- }
-}
-
-object TVarFactory {
-
- val temporaries = MutableSet[Identifier]()
- //these are dummy identifiers used in 'CaseClassSelector' conversion
- val dummyIds = MutableSet[Identifier]()
-
- def createTemp(name: String, tpe: TypeTree = Untyped): Identifier = {
- val freshid = FreshIdentifier(name, tpe, true)
- temporaries.add(freshid)
- freshid
- }
-
- def createDummy(tpe: TypeTree): Identifier = {
- val freshid = FreshIdentifier("dy", tpe, true)
- dummyIds.add(freshid)
- freshid
- }
-
- def isTemporary(id: Identifier): Boolean = temporaries.contains(id)
- def isDummy(id: Identifier): Boolean = dummyIds.contains(id)
-}
-
object Util {
val zero = InfiniteIntegerLiteral(0)
@@ -98,396 +44,16 @@ object Util {
val tru = BooleanLiteral(true)
val fls = BooleanLiteral(false)
- /**
- * Here, we exclude empty units that do not have any modules and empty
- * modules that do not have any definitions
- */
- def copyProgram(prog: Program, mapdefs: (Seq[Definition] => Seq[Definition])): Program = {
- prog.copy(units = prog.units.collect {
- case unit if (!unit.defs.isEmpty) => unit.copy(defs = unit.defs.collect {
- case module : ModuleDef if (!module.defs.isEmpty) =>
- module.copy(defs = mapdefs(module.defs))
- case other => other
- })
- })
- }
-
- def createTemplateFun(plainTemp: Expr): FunctionInvocation = {
- val tmpl = Lambda(getTemplateIds(plainTemp).toSeq.map(id => ValDef(id)), plainTemp)
- val tmplFd = new FunDef(FreshIdentifier("tmpl", FunctionType(Seq(tmpl.getType), BooleanType), false), Seq(), Seq(ValDef(FreshIdentifier("arg", tmpl.getType),
- Some(tmpl.getType))), BooleanType)
- tmplFd.body = Some(BooleanLiteral(true))
- FunctionInvocation(TypedFunDef(tmplFd, Seq()), Seq(tmpl))
- }
-
- /**
- * This is the default template generator.
- * Note: we are not creating template for libraries.
- */
- def getOrCreateTemplateForFun(fd: FunDef): Expr = {
- val plainTemp = if (fd.hasTemplate) fd.getTemplate
- else if (fd.annotations.contains("library")) BooleanLiteral(true)
- else {
- //just consider all the arguments, return values that are integers
- val baseTerms = fd.params.filter((vardecl) => isNumericType(vardecl.getType)).map(_.toVariable) ++
- (if (isNumericType(fd.returnType)) Seq(Util.getFunctionReturnVariable(fd))
- else Seq())
- val lhs = baseTerms.foldLeft(TemplateIdFactory.freshTemplateVar(): Expr)((acc, t) => {
- Plus(Times(TemplateIdFactory.freshTemplateVar(), t), acc)
- })
- val tempExpr = LessEquals(lhs, InfiniteIntegerLiteral(0))
- tempExpr
- }
- plainTemp
- }
-
- def mapFunctionsInExpr(funmap: Map[FunDef, FunDef])(ine: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(tfd, args) if funmap.contains(tfd.fd) =>
- FunctionInvocation(TypedFunDef(funmap(tfd.fd), tfd.tps), args)
- case _ => e
- })(ine)
- }
-
- def assignTemplateAndCojoinPost(funToTmpl: Map[FunDef, Expr], prog: Program,
- funToPost: Map[FunDef, Expr] = Map(), uniqueIdDisplay : Boolean = true): Program = {
-
- val funMap = Util.functionsWOFields(prog.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
- case (accMap, fd) if fd.isTheoryOperation =>
- accMap + (fd -> fd)
- case (accMap, fd) => {
- val freshId = FreshIdentifier(fd.id.name, fd.returnType, uniqueIdDisplay)
- val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
- accMap.updated(fd, newfd)
- }
- }
-
- // FIXME: This with createAnd (which performs simplifications) gives an error during composition.
- val mapExpr = mapFunctionsInExpr(funMap) _
- for ((from, to) <- funMap) {
- to.fullBody = if (!funToTmpl.contains(from)) {
- mapExpr {
- from.fullBody match {
- case Ensuring(b, post) =>
- Ensuring(b,
- Lambda(Seq(ValDef(Util.getResId(from).get)),
- createAnd(Seq(from.getPostWoTemplate, funToPost.getOrElse(from, tru)))))
- case fb =>
- fb
- }
- }
- } else {
- val newTmpl = createTemplateFun(funToTmpl(from))
- mapExpr {
- from.fullBody match {
- case Require(pre, body) =>
- val toPost =
- Lambda(Seq(ValDef(FreshIdentifier("res", from.returnType))),
- createAnd(Seq(newTmpl, funToPost.getOrElse(from, tru))))
- Ensuring(Require(pre, body), toPost)
-
- case Ensuring(Require(pre, body), post) =>
- Ensuring(Require(pre, body),
- Lambda(Seq(ValDef(Util.getResId(from).get)),
- createAnd(Seq(from.getPostWoTemplate, newTmpl, funToPost.getOrElse(from, tru)))))
-
- case Ensuring(body, post) =>
- Ensuring(body,
- Lambda(Seq(ValDef(Util.getResId(from).get)),
- createAnd(Seq(from.getPostWoTemplate, newTmpl, funToPost.getOrElse(from, tru)))))
-
- case body =>
- val toPost =
- Lambda(Seq(ValDef(FreshIdentifier("res", from.returnType))),
- createAnd(Seq(newTmpl, funToPost.getOrElse(from, tru))))
- Ensuring(body, toPost)
- }
- }
- }
- //copy annotations
- from.flags.foreach(to.addFlag(_))
- }
- val newprog = Util.copyProgram(prog, (defs: Seq[Definition]) => defs.map {
- case fd: FunDef if funMap.contains(fd) =>
- funMap(fd)
- case d => d
- })
- newprog
- }
-
- def functionByName(nm: String, prog: Program) = {
- prog.definedFunctions.find(fd => fd.id.name == nm)
- }
-
- def functionsWOFields(fds: Seq[FunDef]): Seq[FunDef] = {
- fds.filter(_.isRealFunction)
- }
-
- def isNumericExpr(expr: Expr): Boolean = {
- expr.getType == IntegerType ||
- expr.getType == RealType
- }
-
- def getFunctionReturnVariable(fd: FunDef) = {
- if (fd.hasPostcondition) getResId(fd).get.toVariable
- else ResultVariable(fd.returnType) /*FreshIdentifier("res", fd.returnType).toVariable*/
- }
-
- //compute the formal to the actual argument mapping
- def formalToActual(call: Call): Map[Expr, Expr] = {
- val fd = call.fi.tfd.fd
- val resvar = getFunctionReturnVariable(fd)
- val argmap: Map[Expr, Expr] = Map(resvar -> call.retexpr) ++ fd.params.map(_.id.toVariable).zip(call.fi.args)
- argmap
- }
-
- /**
- * Checks if the input expression has only template variables as free variables
- */
- def isTemplateExpr(expr: Expr): Boolean = {
- var foundVar = false
- simplePostTransform((e: Expr) => e match {
- case Variable(id) => {
- if (!TemplateIdFactory.IsTemplateIdentifier(id))
- foundVar = true
- e
- }
- case ResultVariable(_) => {
- foundVar = true
- e
- }
- case _ => e
- })(expr)
-
- !foundVar
- }
-
- def getTemplateIds(expr: Expr) = {
- variablesOf(expr).filter(TemplateIdFactory.IsTemplateIdentifier)
- }
-
- def getTemplateVars(expr: Expr): Set[Variable] = {
- /*var tempVars = Set[Variable]()
- postTraversal(e => e match {
- case t @ Variable(id) =>
- if (TemplateIdFactory.IsTemplateIdentifier(id))
- tempVars += t
- case _ =>
- })(expr)
- tempVars*/
- getTemplateIds(expr).map(_.toVariable)
- }
-
- /**
- * Checks if the expression has real valued sub-expressions.
- */
- def hasReals(expr: Expr): Boolean = {
- var foundReal = false
- simplePostTransform((e: Expr) => e match {
- case _ => {
- if (e.getType == RealType)
- foundReal = true;
- e
- }
- })(expr)
- foundReal
- }
-
- /**
- * Checks if the expression has real valued sub-expressions.
- * Note: important, <, <=, > etc have default int type.
- * However, they can also be applied over real arguments
- * So check only if all terminals are real
- */
- def hasInts(expr: Expr): Boolean = {
- var foundInt = false
- simplePostTransform((e: Expr) => e match {
- case e: Terminal if (e.getType == Int32Type || e.getType == IntegerType) => {
- foundInt = true;
- e
- }
- case _ => e
- })(expr)
- foundInt
- }
-
- def hasMixedIntReals(expr: Expr): Boolean = {
- hasInts(expr) && hasReals(expr)
- }
-
def fix[A](f: (A) => A)(a: A): A = {
val na = f(a)
if (a == na) a else fix(f)(na)
}
- def atomNum(e: Expr): Int = {
- var count: Int = 0
- simplePostTransform((e: Expr) => e match {
- case And(args) => {
- count += args.size
- e
- }
- case Or(args) => {
- count += args.size
- e
- }
- case _ => e
- })(e)
- count
- }
-
- def numUIFADT(e: Expr): Int = {
- var count: Int = 0
- simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(_, _) | CaseClass(_, _) | Tuple(_) => {
- count += 1
- e
- }
- case _ => e
- })(e)
- count
- }
-
- def hasCalls(e: Expr) = numUIFADT(e) >= 1
-
- def getCallExprs(ine: Expr): Set[Expr] = {
- var calls = Set[Expr]()
- simplePostTransform((e: Expr) => e match {
- case call @ _ if Util.isCallExpr(e) => {
- calls += e
- call
- }
- case _ => e
- })(ine)
- calls
- }
-
- def isCallExpr(e: Expr): Boolean = e match {
- case Equals(Variable(_), FunctionInvocation(_, _)) => true
- // case Iff(Variable(_),FunctionInvocation(_,_)) => true
- case _ => false
- }
-
- def isADTConstructor(e: Expr): Boolean = e match {
- case Equals(Variable(_), CaseClass(_, _)) => true
- case Equals(Variable(_), Tuple(_)) => true
- case _ => false
- }
-
- def modelToExpr(model: Model): Expr = {
- model.foldLeft(tru: Expr)((acc, elem) => {
- val (k, v) = elem
- val eq = Equals(k.toVariable, v)
- if (acc == tru) eq
- else And(acc, eq)
- })
- }
-
def gcd(x: Int, y: Int): Int = {
if (x == 0) y
else gcd(y % x, x)
}
- def toZ3SMTLIB(expr: Expr, filename: String,
- theory: String, ctx: LeonContext, pgm: Program,
- useBitvectors: Boolean = false,
- bitvecSize: Int = 32) = {
- //create new solver, assert constraints and print
- val printSol = new ExtendedUFSolver(ctx, pgm)
- printSol.assertCnstr(expr)
- val writer = new PrintWriter(filename)
- writer.println(printSol.ctrsToString(theory))
- printSol.free()
- writer.flush()
- writer.close()
- }
-
- /**
- * A helper function that can be used to hardcode an invariant and see if it unsatifies the paths
- */
- def checkInvariant(expr: Expr, ctx: LeonContext, prog: Program): Option[Boolean] = {
- val idmap: Map[Expr, Expr] = variablesOf(expr).collect {
- case id @ _ if (id.name.toString == "a?") => id.toVariable -> InfiniteIntegerLiteral(6)
- case id @ _ if (id.name.toString == "c?") => id.toVariable -> InfiniteIntegerLiteral(2)
- }.toMap
- //println("found ids: " + idmap.keys)
- if (!idmap.keys.isEmpty) {
- val newpathcond = replace(idmap, expr)
- //check if this is solvable
- val solver = SimpleSolverAPI(SolverFactory(() => new ExtendedUFSolver(ctx, prog)))
- solver.solveSAT(newpathcond)._1 match {
- case Some(true) => {
- println("Path satisfiable for a?,c? -->6,2 ")
- Some(true)
- }
- case _ => {
- println("Path unsat for a?,c? --> 6,2")
- Some(false)
- }
- }
- } else None
- }
-
- def collectUNSATCores(ine: Expr, ctx: LeonContext, prog: Program): Expr = {
- var controlVars = Map[Variable, Expr]()
- var newEqs = Map[Expr, Expr]()
- val solver = new ExtendedUFSolver(ctx, prog)
- val newe = simplePostTransform((e: Expr) => e match {
- case And(_) | Or(_) => {
- val v = TVarFactory.createTemp("a", BooleanType).toVariable
- newEqs += (v -> e)
- val newe = Equals(v, e)
-
- //create new variable and add it in disjunction
- val cvar = FreshIdentifier("ctrl", BooleanType, true).toVariable
- controlVars += (cvar -> newe)
- solver.assertCnstr(Or(newe, cvar))
- v
- }
- case _ => e
- })(ine)
- //create new variable and add it in disjunction
- val cvar = FreshIdentifier("ctrl", BooleanType, true).toVariable
- controlVars += (cvar -> newe)
- solver.assertCnstr(Or(newe, cvar))
-
- val res = solver.checkAssumptions(controlVars.keySet.map(Not.apply _))
- println("Result: " + res)
- val coreExprs = solver.getUnsatCore
- val simpcores = coreExprs.foldLeft(Seq[Expr]())((acc, coreExp) => {
- val Not(cvar @ Variable(_)) = coreExp
- val newexp = controlVars(cvar)
- //println("newexp: "+newexp)
- newexp match {
- // case Iff(v@Variable(_),rhs) if(newEqs.contains(v)) => acc
- case Equals(v @ Variable(_), rhs) if (v.getType == BooleanType && rhs.getType == BooleanType && newEqs.contains(v)) => acc
- case _ => {
- acc :+ newexp
- }
- }
- })
- val cores = Util.fix((e: Expr) => replace(newEqs, e))(Util.createAnd(simpcores.toSeq))
-
- solver.free
- //cores
- ExpressionTransformer.unFlatten(cores,
- variablesOf(ine).filterNot(TVarFactory.isTemporary _))
- }
-
- def isMultFunctions(fd: FunDef) = {
- (fd.id.name == "mult" || fd.id.name == "pmult") &&
- fd.isTheoryOperation
- }
- //replaces occurrences of mult by Times
- def multToTimes(ine: Expr): Expr = {
- simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(TypedFunDef(fd, _), args) if isMultFunctions(fd) => {
- Times(args(0), args(1))
- }
- case _ => e
- })(ine)
- }
-
/**
* A cross product with an optional filter
*/
@@ -499,219 +65,4 @@ object Util {
else
product
}
-
- def getResId(funDef: FunDef): Option[Identifier] = {
- funDef.fullBody match {
- case Ensuring(_, post) => {
- post match {
- case Lambda(Seq(ValDef(fromRes, _)), _) => Some(fromRes)
- case _ =>
- throw new IllegalStateException("Postcondition with multiple return values!")
- }
- }
- case _ => None
- }
- }
-
- def createAnd(exprs: Seq[Expr]): Expr = {
- val newExprs = exprs.filterNot(conj => conj == tru)
- newExprs match {
- case Seq() => tru
- case Seq(e) => e
- case _ => And(newExprs)
- }
- }
-
- def createOr(exprs: Seq[Expr]): Expr = {
- val newExprs = exprs.filterNot(disj => disj == fls)
- newExprs match {
- case Seq() => fls
- case Seq(e) => e
- case _ => Or(newExprs)
- }
- }
-
- def isNumericType(t: TypeTree) = t match {
- case IntegerType | RealType => true
- case _ => false
- }
-
- //tests if the solver uses nlsat
- def usesNLSat(solver: AbstractZ3Solver) = {
- //check for nlsat
- val x = FreshIdentifier("x", RealType).toVariable
- val testExpr = Equals(Times(x, x), FractionalLiteral(2, 1))
- solver.assertCnstr(testExpr)
- solver.check match {
- case Some(true) => true
- case _ => false
- }
- }
-}
-
-/**
- * maps all real valued variables and literals to new integer variables/literals and
- * performs the reverse mapping
- * Note: this should preserve the template identifier property
- */
-class RealToInt {
-
- val bone = BigInt(1)
- var realToIntId = Map[Identifier, Identifier]()
- var intToRealId = Map[Identifier, Identifier]()
-
- def mapRealToInt(inexpr: Expr): Expr = {
- val transformer = (e: Expr) => e match {
- case FractionalLiteral(num, `bone`) => InfiniteIntegerLiteral(num)
- case FractionalLiteral(_, _) => throw new IllegalStateException("Real literal with non-unit denominator")
- case v @ Variable(realId) if (v.getType == RealType) => {
- val newId = realToIntId.getOrElse(realId, {
- //note: the fresh identifier has to be a template identifier if the original one is a template identifier
- val freshId = if (TemplateIdFactory.IsTemplateIdentifier(realId))
- TemplateIdFactory.freshIdentifier(realId.name, IntegerType)
- else
- FreshIdentifier(realId.name, IntegerType, true)
-
- realToIntId += (realId -> freshId)
- intToRealId += (freshId -> realId)
- freshId
- })
- Variable(newId)
- }
- case _ => e
- }
- simplePostTransform(transformer)(inexpr)
- }
-
- def unmapModel(model: Model): Model = {
- new Model(model.map(pair => {
- val (key, value) = if (intToRealId.contains(pair._1)) {
- (intToRealId(pair._1),
- pair._2 match {
- case InfiniteIntegerLiteral(v) => FractionalLiteral(v.toInt, 1)
- case _ => pair._2
- })
- } else pair
- (key -> value)
- }).toMap)
- }
-
- def mapModel(model: Model): Model = {
- new Model(model.collect {
- case (k, FractionalLiteral(n, bone)) =>
- (realToIntId(k), InfiniteIntegerLiteral(n))
- case (k, v) =>
- if (realToIntId.contains(k)) {
- (realToIntId(k), v)
- } else {
- (k, v)
- }
- }.toMap)
- }
-}
-
-class MultiMap[A, B] extends scala.collection.mutable.HashMap[A, scala.collection.mutable.Set[B]] with scala.collection.mutable.MultiMap[A, B] {
- /**
- * Creates a new map and does not change the existing map
- */
- def append(that: MultiMap[A, B]): MultiMap[A, B] = {
- val newmap = new MultiMap[A, B]()
- this.foreach { case (k, vset) => newmap += (k -> vset) }
- that.foreach {
- case (k, vset) => vset.foreach(v => newmap.addBinding(k, v))
- }
- newmap
- }
-}
-
-/**
- * A multimap that allows duplicate entries
- */
-class OrderedMultiMap[A, B] extends scala.collection.mutable.HashMap[A, scala.collection.mutable.ListBuffer[B]] {
-
- def addBinding(key: A, value: B): this.type = {
- get(key) match {
- case None =>
- val list = new scala.collection.mutable.ListBuffer[B]()
- list += value
- this(key) = list
- case Some(list) =>
- list += value
- }
- this
- }
-
- /**
- * Creates a new map and does not change the existing map
- */
- def append(that: OrderedMultiMap[A, B]): OrderedMultiMap[A, B] = {
- val newmap = new OrderedMultiMap[A, B]()
- this.foreach { case (k, vlist) => newmap += (k -> vlist) }
- that.foreach {
- case (k, vlist) => vlist.foreach(v => newmap.addBinding(k, v))
- }
- newmap
- }
-
- /**
- * Make the value of every key distinct
- */
- def distinct: OrderedMultiMap[A, B] = {
- val newmap = new OrderedMultiMap[A, B]()
- this.foreach { case (k, vlist) => newmap += (k -> vlist.distinct) }
- newmap
- }
}
-
-/**
- * Implements a mapping from Seq[A] to B where Seq[A]
- * is stored as a Trie
- */
-final class TrieMap[A, B] {
- var childrenMap = Map[A, TrieMap[A, B]]()
- var dataMap = Map[A, B]()
-
- @tailrec def addBinding(key: Seq[A], value: B) {
- key match {
- case Seq() =>
- throw new IllegalStateException("Key is empty!!")
- case Seq(x) =>
- //add the value to the dataMap
- if (dataMap.contains(x))
- throw new IllegalStateException("A mapping for key already exists: " + x + " --> " + dataMap(x))
- else
- dataMap += (x -> value)
- case head +: tail => //here, tail has at least one element
- //check if we have an entry for seq(0) if yes go to the children, if not create one
- val child = childrenMap.getOrElse(head, {
- val ch = new TrieMap[A, B]()
- childrenMap += (head -> ch)
- ch
- })
- child.addBinding(tail, value)
- }
- }
-
- @tailrec def lookup(key: Seq[A]): Option[B] = {
- key match {
- case Seq() =>
- throw new IllegalStateException("Key is empty!!")
- case Seq(x) =>
- dataMap.get(x)
- case head +: tail => //here, tail has at least one element
- childrenMap.get(head) match {
- case Some(child) =>
- child.lookup(tail)
- case _ => None
- }
- }
- }
-}
-
-class CounterMap[T] extends scala.collection.mutable.HashMap[T, Int] {
- def inc(v: T) = {
- if (this.contains(v))
- this(v) += 1
- else this += (v -> 1)
- }
-}
\ No newline at end of file
diff --git a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
deleted file mode 100644
index db508eaf7964d394f5e11b98590beaa1532a9d5b..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package purescala
-
-import Common._
-import Definitions._
-import Expressions._
-
-object CompleteAbstractDefinitions extends UnitPhase[Program] {
-
- val name = "Materialize abstract functions"
- val description = "Inject fake choose-like body in abstract definitions"
-
- def apply(ctx: LeonContext, program: Program) = {
- for (u <- program.units; m <- u.modules; fd <- m.definedFunctions; if fd.body.isEmpty) {
- val post = fd.postcondition getOrElse (
- Lambda(Seq(ValDef(FreshIdentifier("res", fd.returnType))), BooleanLiteral(true))
- )
- fd.body = Some(Choose(post))
- }
- }
-
-}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 200a9e167e8d70e076b9d13fc7c301331e127138..c106d1393bcf793a7fe5d6944ecd533d84a42e36 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1474,14 +1474,14 @@ object ExprOps {
val solver = SimpleSolverAPI(sf)
toCheck.forall { cond =>
- solver.solveSAT(cond) match {
- case (Some(false), _) =>
- true
- case (Some(true), model) =>
- false
- case (None, _) =>
- // Should we be optimistic here?
- false
+ solver.solveSAT(cond)._1 match {
+ case Some(false) =>
+ true
+ case Some(true) =>
+ false
+ case None =>
+ // Should we be optimistic here?
+ false
}
}
case _ =>
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 7216652a427e6784142a17f69c730fa61e2ff0aa..b834eb9f1270bca728b2cdbaa63bb98a37b0dd49 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -886,7 +886,7 @@ object Expressions {
/** $encodingof a synthesizable hole in a program. Represented by `???[tpe]`
* in Leon source code.
*
- * A [[Hole]] gets transformed into a [[Choose]] construct during [[leon.synthesis.ConvertHoles the ConvertHoles phase]].
+ * A [[Hole]] gets transformed into a [[Choose]] construct during [[leon.synthesis.ConversionPhase the ConvertHoles phase]].
*/
case class Hole(tpe: TypeTree, alts: Seq[Expr]) extends Expr with Extractable {
val getType = tpe
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 20dbd1eeced9c951221665b2a3136b2225681c86..65fd1de8a934bb802f57a39f95e17721e6e78f95 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -130,7 +130,12 @@ object FunctionClosure extends TransformationPhase {
val freshVals = (inner.paramIds ++ free).map{_.freshen}.map(instantiateType(_, tparamsMap))
val freeMap = (inner.paramIds ++ free).zip(freshVals).toMap
- val newFd = inner.duplicate(inner.id.freshen, inner.tparams ++ tpFresh, freshVals.map(ValDef(_)), instantiateType(inner.returnType, tparamsMap))
+ val newFd = inner.duplicate(
+ inner.id.freshen,
+ inner.tparams ++ tpFresh,
+ freshVals.map(ValDef(_)),
+ instantiateType(inner.returnType, tparamsMap)
+ )
newFd.precondition = Some(and(pc, inner.precOrTrue))
val instBody = instantiateType(
@@ -154,11 +159,7 @@ object FunctionClosure extends TransformationPhase {
override def apply(ctx: LeonContext, program: Program): Program = {
val newUnits = program.units.map { u => u.copy(defs = u.defs map {
case m: ModuleDef =>
- ModuleDef(
- m.id,
- m.definedClasses ++ m.definedFunctions.flatMap(close),
- m.isPackageObject
- )
+ m.copy(defs = m.definedClasses ++ m.definedFunctions.flatMap(close))
case cd =>
cd
})}
diff --git a/src/main/scala/leon/purescala/Quantification.scala b/src/main/scala/leon/purescala/Quantification.scala
index 38fa0ae9f81190096aa4f19cbd5a5a988dbfb249..1b00ed1b41a5053fb07a94695b00f595d54453ba 100644
--- a/src/main/scala/leon/purescala/Quantification.scala
+++ b/src/main/scala/leon/purescala/Quantification.scala
@@ -19,7 +19,7 @@ object Quantification {
qargs: A => Set[B]
): Seq[Set[A]] = {
def rec(oms: Seq[A], mSet: Set[A], qss: Seq[Set[B]]): Seq[Set[A]] = {
- if (qss.exists(_ == quantified)) {
+ if (qss.contains(quantified)) {
Seq(mSet)
} else {
var res = Seq.empty[Set[A]]
@@ -126,12 +126,11 @@ object Quantification {
ctx.reporter.warning("E-matching isn't possible without matchers!")
if (matchers.exists { case (_, args) =>
- args.exists(arg => arg match {
+ args.exists{
case QuantificationMatcher(_, _) => false
case Variable(id) => false
- case _ if (variablesOf(arg) & quantified).nonEmpty => true
- case _ => false
- })
+ case arg => (variablesOf(arg) & quantified).nonEmpty
+ }
}) ctx.reporter.warning("Matcher arguments must have simple form in " + conjunct)
val freeMatchers = matchers.collect { case (Variable(id), args) if free(id) => id -> args }
@@ -143,7 +142,7 @@ object Quantification {
}))
}
- if (id2Quant.filter(_._2.nonEmpty).groupBy(_._2).size >= 1)
+ if (id2Quant.filter(_._2.nonEmpty).groupBy(_._2).nonEmpty)
ctx.reporter.warning("Multiple matchers must provide bijective matching in " + conjunct)
fold[Set[Identifier]] { case (m, children) =>
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index e5a1eaafe1a73c439a846d0c344e489924edf6eb..1f939c96e9ca70c72c22fac6f1b8378864b6458f 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -167,13 +167,12 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val timeoutMs = verifTimeoutMs.getOrElse(3000L)
val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(timeoutMs)
val vctx = VerificationContext(ctx, program, solverf, reporter)
- val vcs = AnalysisPhase.generateVCs(vctx, Seq(fd))
+ val vcs = VerificationPhase.generateVCs(vctx, Seq(fd))
try {
- val report = AnalysisPhase.checkVCs(
+ val report = VerificationPhase.checkVCs(
vctx,
vcs,
- checkInParallel = true,
stopAfter = Some({ (vc, vr) => vr.isInvalid })
)
diff --git a/src/main/scala/leon/solvers/Model.scala b/src/main/scala/leon/solvers/Model.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ab91f594c954805267dd523fd9f82305ab789798
--- /dev/null
+++ b/src/main/scala/leon/solvers/Model.scala
@@ -0,0 +1,80 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package solvers
+
+import purescala.Expressions._
+import purescala.Common.Identifier
+import purescala.ExprOps._
+
+trait AbstractModel[+This <: Model with AbstractModel[This]]
+ extends scala.collection.IterableLike[(Identifier, Expr), This] {
+
+ protected val mapping: Map[Identifier, Expr]
+
+ def fill(allVars: Iterable[Identifier]): This = {
+ val builder = newBuilder
+ builder ++= mapping ++ (allVars.toSet -- mapping.keys).map(id => id -> simplestValue(id.getType))
+ builder.result
+ }
+
+ def ++(mapping: Map[Identifier, Expr]): This = {
+ val builder = newBuilder
+ builder ++= this.mapping ++ mapping
+ builder.result
+ }
+
+ def filter(allVars: Iterable[Identifier]): This = {
+ val builder = newBuilder
+ for (p <- mapping.filterKeys(allVars.toSet)) {
+ builder += p
+ }
+ builder.result
+ }
+
+ def iterator = mapping.iterator
+ def seq = mapping.seq
+
+ def asString(implicit ctx: LeonContext) = {
+ if (mapping.isEmpty) {
+ "Model()"
+ } else {
+ (for ((k,v) <- mapping.toSeq.sortBy(_._1)) yield {
+ f" ${k.asString}%-20s -> ${v.asString}"
+ }).mkString("Model(\n", ",\n", ")")
+ }
+ }
+}
+
+trait AbstractModelBuilder[+This <: Model with AbstractModel[This]]
+ extends scala.collection.mutable.Builder[(Identifier, Expr), This] {
+
+ import scala.collection.mutable.MapBuilder
+ protected val mapBuilder = new MapBuilder[Identifier, Expr, Map[Identifier, Expr]](Map.empty)
+
+ def +=(elem: (Identifier, Expr)): this.type = {
+ mapBuilder += elem
+ this
+ }
+
+ def clear(): Unit = mapBuilder.clear
+}
+
+class Model(protected val mapping: Map[Identifier, Expr])
+ extends AbstractModel[Model]
+ with (Identifier => Expr) {
+
+ def newBuilder = new ModelBuilder
+ def isDefinedAt(id: Identifier): Boolean = mapping.isDefinedAt(id)
+ def get(id: Identifier): Option[Expr] = mapping.get(id)
+ def getOrElse[E >: Expr](id: Identifier, e: E): E = get(id).getOrElse(e)
+ def apply(id: Identifier): Expr = get(id).getOrElse { throw new IllegalArgumentException }
+}
+
+object Model {
+ def empty = new Model(Map.empty)
+}
+
+class ModelBuilder extends AbstractModelBuilder[Model] {
+ def result = new Model(mapBuilder.result)
+}
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 67ed8eae5c0edd8ade7dd9c12adb90a3d0ec84e0..10902ebbf49a409d19d584b2c57c799fc5487d0e 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -3,84 +3,11 @@
package leon
package solvers
-import leon.utils.{Position, DebugSectionSolver, Interruptible}
+import leon.utils.{DebugSectionSolver, Interruptible}
import purescala.Expressions._
-import purescala.Common.{Tree, Identifier}
-import purescala.ExprOps._
+import purescala.Common.Tree
import verification.VC
-trait AbstractModel[+This <: Model with AbstractModel[This]]
- extends scala.collection.IterableLike[(Identifier, Expr), This] {
-
- protected val mapping: Map[Identifier, Expr]
-
- def fill(allVars: Iterable[Identifier]): This = {
- val builder = newBuilder
- builder ++= mapping ++ (allVars.toSet -- mapping.keys).map(id => id -> simplestValue(id.getType))
- builder.result
- }
-
- def ++(mapping: Map[Identifier, Expr]): This = {
- val builder = newBuilder
- builder ++= this.mapping ++ mapping
- builder.result
- }
-
- def filter(allVars: Iterable[Identifier]): This = {
- val builder = newBuilder
- for (p <- mapping.filterKeys(allVars.toSet)) {
- builder += p
- }
- builder.result
- }
-
- def iterator = mapping.iterator
- def seq = mapping.seq
-
- def asString(implicit ctx: LeonContext) = {
- if (mapping.isEmpty) {
- "Model()"
- } else {
- (for ((k,v) <- mapping.toSeq.sortBy(_._1)) yield {
- f" ${k.asString}%-20s -> ${v.asString}"
- }).mkString("Model(\n", ",\n", ")")
- }
- }
-}
-
-trait AbstractModelBuilder[+This <: Model with AbstractModel[This]]
- extends scala.collection.mutable.Builder[(Identifier, Expr), This] {
-
- import scala.collection.mutable.MapBuilder
- protected val mapBuilder = new MapBuilder[Identifier, Expr, Map[Identifier, Expr]](Map.empty)
-
- def +=(elem: (Identifier, Expr)): this.type = {
- mapBuilder += elem
- this
- }
-
- def clear(): Unit = mapBuilder.clear
-}
-
-class Model(protected val mapping: Map[Identifier, Expr])
- extends AbstractModel[Model]
- with (Identifier => Expr) {
-
- def newBuilder = new ModelBuilder
- def isDefinedAt(id: Identifier): Boolean = mapping.isDefinedAt(id)
- def get(id: Identifier): Option[Expr] = mapping.get(id)
- def getOrElse[E >: Expr](id: Identifier, e: E): E = get(id).getOrElse(e)
- def apply(id: Identifier): Expr = get(id).getOrElse { throw new IllegalArgumentException }
-}
-
-object Model {
- def empty = new Model(Map.empty)
-}
-
-class ModelBuilder extends AbstractModelBuilder[Model] {
- def result = new Model(mapBuilder.result)
-}
-
trait Solver extends Interruptible {
def name: String
val context: LeonContext
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 79ee4c3cfdf4d2bf6d514df270fef164455c47ac..4bfc179a10bcdb48a697ccd6b8d33ea85161e725 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -40,18 +40,22 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
// solving
val fs = solvers.map { s =>
Future {
- val result = s.check
- val model: Model = if (result == Some(true)) {
- s.getModel
- } else {
- Model.empty
+ try {
+ val result = s.check
+ val model: Model = if (result == Some(true)) {
+ s.getModel
+ } else {
+ Model.empty
+ }
+ (s, result, model)
+ } catch {
+ case _: StackOverflowError =>
+ context.reporter.warning("Stack Overflow while running solver.check()!")
+ (s, None, Model.empty)
}
- (s, result, model)
}
}
- fs.foreach(_ onFailure { case ex: Throwable => ex.printStackTrace() })
-
val result = Future.find(fs)(_._2.isDefined)
val res = Await.result(result, Duration.Inf) match {
diff --git a/src/main/scala/leon/solvers/isabelle/Component.scala b/src/main/scala/leon/solvers/isabelle/Component.scala
index cf8db26a5d5516222665c2769a005b2eeea74f2e..3b75a8c64fb7a68db86fc30456a53d8df8e2626d 100644
--- a/src/main/scala/leon/solvers/isabelle/Component.scala
+++ b/src/main/scala/leon/solvers/isabelle/Component.scala
@@ -10,7 +10,7 @@ import leon._
object Component extends LeonComponent {
- val name = "isabelle"
+ val name = "Isabelle"
val description = "Isabelle solver"
val leonBase =
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index dfcfbcc3fffa1cc9ae190b169ab1f34ad1bf4310..dc267825c8356451944b5fb6b7f9de5d55504232 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -29,9 +29,9 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
}
object SMTLIBCVC4Component extends LeonComponent {
- val name = "cvc4 solver"
+ val name = "CVC4 solver"
- val description = "Solver invoked when --solvers=smt-cvc4"
+ val description = "Solver invoked with --solvers=smt-cvc4"
val optCVC4Options = new LeonOptionDef[Set[String]] {
val name = "solver:cvc4"
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d76cff69b1a630718632f70e8684ff2426506cd2
--- /dev/null
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -0,0 +1,185 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package synthesis
+
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.ExprOps._
+import purescala.Definitions._
+import purescala.Constructors._
+
+object ConversionPhase extends UnitPhase[Program] {
+ val name = "Eliminate holes, withOracle and abstract definitions"
+ val description = "Convert Holes, withOracle found in bodies and abstract function bodies to equivalent Choose"
+
+ /**
+ * This phase does 3 things:
+ *
+ * 1) Converts a body with "withOracle{ .. }" into a choose construct:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * withOracle { o =>
+ * expr(a,o) ensuring { x => post(x) }
+ * }
+ * }
+ *
+ * gets converted into:
+ *
+ * def foo(a: T) {
+ * require(..a..)
+ * val o = choose { (o) => {
+ * val res = expr(a, o)
+ * pred(res)
+ * }
+ * expr(a,o)
+ * } ensuring { res =>
+ * pred(res)
+ * }
+ *
+ *
+ * 2) Converts a body with "???" into a choose construct:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * expr(a, ???)
+ * } ensuring { x => post(x) }
+ *
+ * gets converted into:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * val h = choose ( h' =>
+ * val res = expr(a, h')
+ * post(res)
+ * )
+ * expr(a, h)
+ * } ensuring { res =>
+ * post(res)
+ * }
+ *
+ * 3) Completes abstract definitions:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * ???
+ * } ensuring { res =>
+ * post(res)
+ * }
+ *
+ * gets converted to:
+ *
+ * def foo(a: T) = {
+ * require(..a..)
+ * choose(x => post(x))
+ * }
+ *
+ */
+
+ def convert(e : Expr, ctx : LeonContext) : Expr = {
+ val (pre, body, post) = breakDownSpecs(e)
+
+ // Ensure that holes are not found in pre and/or post conditions
+ (pre ++ post).foreach {
+ preTraversal{
+ case h : Hole =>
+ ctx.reporter.error(s"Holes are not supported in pre- or postconditions. @ ${h.getPos}")
+ case wo: WithOracle =>
+ ctx.reporter.error(s"WithOracle expressions are not supported in pre- or postconditions: ${wo.asString(ctx)} @ ${wo.getPos}")
+ case _ =>
+ }
+ }
+
+ def toExpr(h: Hole): (Expr, List[Identifier]) = {
+ h.alts match {
+ case Seq() =>
+ val h1 = FreshIdentifier("hole", h.getType, true)
+ (h1.toVariable, List(h1))
+
+ case Seq(v) =>
+ val h1 = FreshIdentifier("hole", BooleanType, true)
+ val h2 = FreshIdentifier("hole", h.getType, true)
+ (IfExpr(h1.toVariable, h2.toVariable, v), List(h1, h2))
+
+ case exs =>
+ var ids: List[Identifier] = Nil
+ val ex = exs.init.foldRight(exs.last)({ (e: Expr, r: Expr) =>
+ val h = FreshIdentifier("hole", BooleanType, true)
+ ids ::= h
+ IfExpr(h.toVariable, e, r)
+ })
+
+ (ex, ids.reverse)
+ }
+ }
+
+ body match {
+ case Some(body) =>
+ var holes = List[Identifier]()
+
+ val withoutHoles = preMap {
+ case h : Hole =>
+ val (expr, ids) = toExpr(h)
+
+ holes ++= ids
+
+ Some(expr)
+ case wo @ WithOracle(os, b) =>
+ withoutSpec(b) map { pred =>
+ val chooseOs = os.map(_.freshen)
+
+ val pred = post.getOrElse( // FIXME: We need to freshen variables
+ Lambda(chooseOs.map(ValDef(_)), BooleanLiteral(true))
+ )
+
+ letTuple(os, Choose(pred), b)
+ }
+ case _ =>
+ None
+ }(body)
+
+ if (holes.nonEmpty) {
+ val cids: List[Identifier] = holes.map(_.freshen)
+ val hToFresh = (holes zip cids.map(_.toVariable)).toMap
+
+ val spec = post match {
+ case Some(post: Lambda) =>
+ val asLet = letTuple(post.args.map(_.id), withoutHoles, post.body)
+
+ Lambda(cids.map(ValDef(_)), replaceFromIDs(hToFresh, asLet))
+
+ case _ =>
+ Lambda(cids.map(ValDef(_)), BooleanLiteral(true))
+ }
+
+ val choose = Choose(spec)
+
+ val newBody = if (holes.size == 1) {
+ replaceFromIDs(Map(holes.head -> choose), withoutHoles)
+ } else {
+ letTuple(holes, choose, withoutHoles)
+ }
+
+ withPostcondition(withPrecondition(newBody, pre), post)
+
+ } else {
+ e
+ }
+
+ case None =>
+ val newPost = post getOrElse Lambda(Seq(ValDef(FreshIdentifier("res", e.getType))), BooleanLiteral(true))
+ withPrecondition(Choose(newPost), pre)
+ }
+ }
+
+
+ def apply(ctx: LeonContext, pgm: Program): Unit = {
+ // TODO: remove side-effects
+ for (fd <- pgm.definedFunctions) {
+ fd.fullBody = convert(fd.fullBody,ctx)
+ }
+ }
+
+}
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
deleted file mode 100644
index a53ff8672082d03873141e21c1f11141281095fd..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ /dev/null
@@ -1,131 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package synthesis
-
-import purescala.Common._
-import purescala.Expressions._
-import purescala.Types._
-import purescala.ExprOps._
-import purescala.Definitions._
-import purescala.Constructors._
-
-object ConvertHoles extends TransformationPhase {
- val name = "Convert Holes to Choose"
- val description = "Convert Holes found in bodies to equivalent Choose"
-
- /**
- * This phase converts a body with "withOracle{ .. }" into a choose construct:
- *
- * def foo(a: T) = {
- * require(..a..)
- * expr(a, ???)
- * } ensuring { x => post(x) }
- *
- * gets converted into:
- *
- * def foo(a: T) {
- * require(..a..)
- * val h = choose ( h' =>
- * val res = expr(a, h')
- * post(res)
- * )
- * expr(a, h)
- * } ensuring { res =>
- * post(res)
- * }
- *
- */
-
- def convertHoles(e : Expr, ctx : LeonContext) : Expr = {
- val (pre, body, post) = breakDownSpecs(e)
-
- // Ensure that holes are not found in pre and/or post conditions
- (pre ++ post).foreach {
- preTraversal{
- case h : Hole =>
- ctx.reporter.error("Holes are not supported in preconditions. @"+ h.getPos)
- case _ =>
- }
- }
-
- body match {
- case Some(body) =>
- var holes = List[Identifier]()
-
- val withoutHoles = preMap {
- case h : Hole =>
- val (expr, ids) = toExpr(h)
-
- holes ++= ids
-
- Some(expr)
- case _ =>
- None
- }(body)
-
- if (holes.nonEmpty) {
- val cids: List[Identifier] = holes.map(_.freshen)
- val hToFresh = (holes zip cids.map(_.toVariable)).toMap
-
- val spec = post match {
- case Some(post: Lambda) =>
- val asLet = letTuple(post.args.map(_.id), withoutHoles, post.body)
-
- Lambda(cids.map(ValDef(_)), replaceFromIDs(hToFresh, asLet))
-
- case _ =>
- Lambda(cids.map(ValDef(_)), BooleanLiteral(true))
- }
-
- val choose = Choose(spec)
-
- val newBody = if (holes.size == 1) {
- replaceFromIDs(Map(holes.head -> choose), withoutHoles)
- } else {
- letTuple(holes, choose, withoutHoles)
- }
-
- withPostcondition(withPrecondition(newBody, pre), post)
-
- } else {
- e
- }
-
- case None => e
- }
- }
-
-
- def apply(ctx: LeonContext, pgm: Program): Program = {
- // TODO: remove side-effects
- for (fd <- pgm.definedFunctions) {
- fd.fullBody = convertHoles(fd.fullBody,ctx)
- }
-
- pgm
- }
-
- def toExpr(h: Hole): (Expr, List[Identifier]) = {
- h.alts match {
- case Seq() =>
- val h1 = FreshIdentifier("hole", h.getType, true)
- (h1.toVariable, List(h1))
-
- case Seq(v) =>
- val h1 = FreshIdentifier("hole", BooleanType, true)
- val h2 = FreshIdentifier("hole", h.getType, true)
- (IfExpr(h1.toVariable, h2.toVariable, v), List(h1, h2))
-
- case exs =>
- var ids: List[Identifier] = Nil
- val ex = exs.init.foldRight(exs.last)({ (e: Expr, r: Expr) =>
- val h = FreshIdentifier("hole", BooleanType, true)
- ids ::= h
- IfExpr(h.toVariable, e, r)
- })
-
- (ex, ids.reverse)
- }
- }
-}
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracle.scala b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
deleted file mode 100644
index ac3785c43e454431ebf18ecc2df4dcec78a6a16b..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/ConvertWithOracle.scala
+++ /dev/null
@@ -1,88 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package synthesis
-
-import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.Definitions._
-import purescala.Constructors._
-
-object ConvertWithOracle extends TransformationPhase {
- val name = "Convert WithOracle to Choose"
- val description = "Convert WithOracle found in bodies to equivalent Choose"
-
- /**
- * This phase converts a body with "withOracle{ .. }" into a choose construct:
- *
- * def foo(a: T) = {
- * require(..a..)
- * withOracle { o =>
- * expr(a,o) ensuring { x => post(x) }
- * }
- * }
- *
- * gets converted into:
- *
- * def foo(a: T) {
- * require(..a..)
- * val o = choose { (o) => {
- * val res = expr(a, o)
- * pred(res)
- * }
- * expr(a,o)
- * } ensuring { res =>
- * pred(res)
- * }
- *
- */
- def apply(ctx: LeonContext, pgm: Program): Program = {
- // TODO: Remove side-effects
-
- pgm.definedFunctions.foreach(fd => {
- if (fd.hasBody) {
- val body = preMap {
- case wo @ WithOracle(os, b) =>
- withoutSpec(b) match {
- case Some(pred) =>
- val chooseOs = os.map(_.freshen)
-
- val pred = postconditionOf(b) match {
- case Some(post) =>
- post // FIXME we need to freshen variables
- case None =>
- Lambda(chooseOs.map(ValDef(_)), BooleanLiteral(true))
- }
-
- Some(letTuple(os, Choose(pred), b))
- case None =>
- None
- }
- case _ => None
- }(fd.body.get)
-
- fd.body = Some(body)
- }
-
- // Ensure that holes are not found in pre and/or post conditions
- fd.precondition.foreach {
- preTraversal{
- case _: WithOracle =>
- ctx.reporter.error("WithOracle expressions are not supported in preconditions. (function "+fd.id.asString(ctx)+")")
- case _ =>
- }
- }
-
- fd.postcondition.foreach {
- preTraversal{
- case _: WithOracle =>
- ctx.reporter.error("WithOracle expressions are not supported in postconditions. (function "+fd.id.asString(ctx)+")")
- case _ =>
- }
- }
-
- })
-
- pgm
- }
-}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 7ed4d56a8a74e5a16301026ff2328ba8243d8716..54e305adf11ebc9314c262b4be5b203df8337771 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -70,7 +70,7 @@ class Synthesizer(val context : LeonContext,
}
def validateSolution(search: Search, sol: Solution, timeout: Duration): (Solution, Boolean) = {
- import verification.AnalysisPhase._
+ import verification.VerificationPhase._
import verification.VerificationContext
reporter.info("Solution requires validation")
diff --git a/src/main/scala/leon/transformations/InstProgSimplifier.scala b/src/main/scala/leon/transformations/InstProgSimplifier.scala
index ff7862db1c535421db229ede3dda6efecad93713..ab650449b58df9897fb89191d3d10bc065b54557 100644
--- a/src/main/scala/leon/transformations/InstProgSimplifier.scala
+++ b/src/main/scala/leon/transformations/InstProgSimplifier.scala
@@ -9,7 +9,10 @@ import purescala.ExprOps._
import purescala.Types._
import leon.purescala.ScalaPrinter
import leon.utils._
-import invariant.util.Util._
+import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
import invariant.util.ExpressionTransformer._
import invariant.structure.FunctionUtils._
import invariant.util.LetTupleSimplification._
diff --git a/src/main/scala/leon/transformations/InstrumentationUtil.scala b/src/main/scala/leon/transformations/InstrumentationUtil.scala
index 427cac483cef7d5ee2b45198a71c1154ee1af999..2c461e466298614ebae30df8a33ff901fea72fa5 100644
--- a/src/main/scala/leon/transformations/InstrumentationUtil.scala
+++ b/src/main/scala/leon/transformations/InstrumentationUtil.scala
@@ -8,6 +8,11 @@ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
import leon.utils.Library
+import invariant.util._
+import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
sealed abstract class Instrumentation {
val getType: TypeTree
@@ -73,7 +78,7 @@ object InstUtil {
}
def getInstMap(fd: FunDef) = {
- val resvar = invariant.util.Util.getResId(fd).get.toVariable // note: every instrumented function has a postcondition
+ val resvar = getResId(fd).get.toVariable // note: every instrumented function has a postcondition
val insts = fd.id.name.split("-").tail // split the name of the function w.r.t '-'
(insts.zipWithIndex).foldLeft(Map[Expr, String]()) {
case (acc, (instName, i)) =>
@@ -82,7 +87,7 @@ object InstUtil {
}
def getInstExpr(fd: FunDef, inst: Instrumentation) = {
- val resvar = invariant.util.Util.getResId(fd).get.toVariable // note: every instrumented function has a postcondition
+ val resvar = getResId(fd).get.toVariable // note: every instrumented function has a postcondition
val insts = fd.id.name.split("-").tail // split the name of the function w.r.t '-'
val index = insts.indexOf(inst.name)
if (index >= 0)
@@ -108,6 +113,8 @@ object InstUtil {
}
def replaceInstruVars(e: Expr, fd: FunDef): Expr = {
- replace(getInstVariableMap(fd), e)
+ val resvar = getResId(fd).get.toVariable
+ val newres = FreshIdentifier(resvar.id.name, resvar.getType).toVariable
+ replace(getInstVariableMap(fd) + (TupleSelect(resvar, 1) -> newres), e)
}
}
diff --git a/src/main/scala/leon/transformations/IntToRealProgram.scala b/src/main/scala/leon/transformations/IntToRealProgram.scala
index dc7ceb5a64ea7d15fedc48bc3fe6c40a7607555b..21229282b398fcc10cd9548ddaead2f25d8087a3 100644
--- a/src/main/scala/leon/transformations/IntToRealProgram.scala
+++ b/src/main/scala/leon/transformations/IntToRealProgram.scala
@@ -10,7 +10,10 @@ import purescala.Types._
import leon.purescala.ScalaPrinter
import invariant.factories._
-import invariant.util.Util._
+import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
import invariant.structure._
abstract class ProgramTypeTransformer {
diff --git a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
index 77b88f71e557d2bdb90470f8e684168574f4d1bc..d17968dc05b789b936554b9c10dbde22ac360dfb 100644
--- a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
+++ b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
@@ -2,7 +2,10 @@ package leon
package transformations
import invariant.factories._
-import invariant.util.Util._
+import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
import invariant.structure.FunctionUtils._
import purescala.ScalaPrinter
@@ -147,7 +150,6 @@ class NonlinearityEliminator(skipAxioms: Boolean, domain: TypeTree) {
Some(replaceFun(simpBody))
} else None
-
//add a new postcondition
newfd.postcondition = if (fd.postcondition.isDefined) {
//we need to handle template and postWoTemplate specially
diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
index 20e3aa0e2bb7912992821e3cb2ced21985820f89..87c5795838b460314d19805cbb8ca6caae4ee233 100644
--- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
+++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
@@ -10,6 +10,9 @@ import purescala.Types._
import leon.purescala.ScalaPrinter
import leon.utils._
import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
import invariant.util.CallGraphUtil
import invariant.structure.FunctionUtils._
import scala.collection.mutable.{Map => MutableMap}
@@ -68,7 +71,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
//create new functions. Augment the return type of a function iff the postcondition uses
//the instrumentation variable or if the function is transitively called from such a function
//note: need not instrument fields
- val funMap = Util.functionsWOFields(program.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
+ val funMap = functionsWOFields(program.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
case (accMap, fd: FunDef) if fd.isTheoryOperation =>
accMap + (fd -> fd)
case (accMap, fd) => {
@@ -160,7 +163,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
else List()
}.toList.distinct
- val newprog = Util.copyProgram(program, (defs: Seq[Definition]) =>
+ val newprog = copyProgram(program, (defs: Seq[Definition]) =>
defs.map {
case fd: FunDef if funMap.contains(fd) =>
funMap(fd)
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 38b770ba19a468977cf8018c2ac7d438140525a5..87d1003150995eb236e5f3abb738450516c5b7f7 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -7,11 +7,10 @@ import leon.purescala._
import leon.purescala.Definitions.Program
import leon.purescala.Quantification.CheckForalls
import leon.solvers.isabelle.AdaptationPhase
-import leon.synthesis.{ConvertWithOracle, ConvertHoles}
import leon.verification.InjectAsserts
-import leon.xlang.XLangDesugaringPhase
+import leon.xlang.{NoXLangFeaturesChecking, XLangDesugaringPhase}
-class PreprocessingPhase(private val desugarXLang: Boolean = false) extends LeonPhase[Program, Program] {
+class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Program, Program] {
val name = "preprocessing"
val description = "Various preprocessings on Leon programs"
@@ -26,13 +25,18 @@ class PreprocessingPhase(private val desugarXLang: Boolean = false) extends Leon
}
}
+ val checkX = if (desugarXLang) {
+ NoopPhase[Program]()
+ } else {
+ NoXLangFeaturesChecking
+ }
+
val pipeBegin =
debugTrees("Program after extraction") andThen
+ checkX andThen
MethodLifting andThen
TypingPhase andThen
- ConvertWithOracle andThen
- ConvertHoles andThen
- CompleteAbstractDefinitions andThen
+ synthesis.ConversionPhase andThen
CheckADTFieldsTypes andThen
InjectAsserts andThen
InliningPhase andThen
@@ -42,7 +46,7 @@ class PreprocessingPhase(private val desugarXLang: Boolean = false) extends Leon
XLangDesugaringPhase andThen
debugTrees("Program after xlang desugaring")
} else {
- xlang.NoXLangFeaturesChecking
+ NoopPhase[Program]()
}
val phases =
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 33511b23c520f980969934e50a9965a3378816e3..b138559afc861169030cced660a622c91410afab 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -5,7 +5,6 @@ package leon.verification
import leon.purescala.Expressions._
import leon.purescala.Definitions._
import leon.purescala.PrettyPrinter
-import leon.purescala.Common._
import leon.utils.Positioned
import leon.solvers._
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index 42d3eba6242ac653b1d5b831dfcdb158acd2789d..2aaa910ab6450c0de300e36ec42ad71d7b073d84 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -11,4 +11,6 @@ case class VerificationContext (
program: Program,
solverFactory: SolverFactory[Solver],
reporter: Reporter
-)
+) {
+ val checkInParallel: Boolean = context.findOptionOrDefault(VerificationPhase.optParallelVCs)
+}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
similarity index 89%
rename from src/main/scala/leon/verification/AnalysisPhase.scala
rename to src/main/scala/leon/verification/VerificationPhase.scala
index 8c6c7d0cef4441a4d62c57214a9cdb39877a1ed2..21119c4e2728c99850e3af0d1c12e498866f771e 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -7,12 +7,17 @@ import purescala.Definitions._
import purescala.ExprOps._
import scala.concurrent.duration._
+import java.lang.System
import solvers._
-object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
- val name = "Analysis"
- val description = "Leon Verification"
+object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
+ val name = "Verification"
+ val description = "Verification of function contracts"
+
+ val optParallelVCs = LeonFlagOptionDef("parallel", "Check verification conditions in parallel", default = false)
+
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(optParallelVCs)
implicit val debugSection = utils.DebugSectionVerification
@@ -89,7 +94,6 @@ object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
def checkVCs(
vctx: VerificationContext,
vcs: Seq[VC],
- checkInParallel: Boolean = false,
stopAfter: Option[(VC, VCResult) => Boolean] = None
): VerificationReport = {
val interruptManager = vctx.context.interruptManager
@@ -98,7 +102,7 @@ object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
val initMap: Map[VC, Option[VCResult]] = vcs.map(v => v -> None).toMap
- val results = if (checkInParallel) {
+ val results = if (vctx.checkInParallel) {
for (vc <- vcs.par if !stop) yield {
val r = checkVC(vctx, vc)
if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
@@ -168,6 +172,9 @@ object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
}
reporter.synchronized {
+ if (vctx.checkInParallel) {
+ reporter.info(s" - Result for '${vc.kind}' VC for ${vc.fd.id} @${vc.getPos}:")
+ }
res.report(vctx)
}
diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst
index c5495f40a99086a3accddd87a7f74fc2769a99a1..5648b042c47f3a252672d698d496a2b3309221a8 100644
--- a/src/sphinx/options.rst
+++ b/src/sphinx/options.rst
@@ -18,7 +18,7 @@ Choosing which Leon feature to use
----------------------------------
The first group of options determine which feature of Leon will be used.
-These options are mutually exclusive. By default, ``--verify`` is chosen.
+These options are mutually exclusive (except when noted). By default, ``--verify`` is chosen.
* ``--eval``
@@ -62,7 +62,7 @@ These options are mutually exclusive. By default, ``--verify`` is chosen.
Additional top-level options
----------------------------
-These options are available by all Leon components:
+These options are available to all Leon components:
* ``--debug=d1,d2,...``
@@ -197,49 +197,19 @@ These options are available by all Leon components:
Support for additional language constructs described in :ref:`xlang`.
These constructs are desugared into :ref:`purescala` before other operations.
-Invariant Inference
--------------------
-
-These options are to be used in conjuction with ``--inferInv`` and ``--instrument``.
-
-* ``--cegis``
-
- Use cegis instead of farkas
-
-* ``--disableInfer``
-
- Disable automatic inference of auxiliary invariants
-
-* ``--fullunroll``
-
- Unroll all calls in every unroll step
-
-* ``--inferTemp``
-
- Infer templates by enumeration
-
-* ``--minbounds``
-
- Tighten the inferred time bounds
-
-* ``--stats-suffix=s``
-
- Specifies the suffix of the statistics file
-
-* ``--usereals``
-
- Interpret the input program as a program over real numbers
-
-* ``--wholeprogram``
+Additional Options (by component)
+---------------------------------
- Perform a non-modular whole program analysis
+The following options relate to specific components in Leon. Bear in mind
+that related components might still use these options, e.g. repair will use
+synthesis options and verification options.
-* ``--withmult``
+Verification
+************
- Do not convert multiplication into a recursive function inside verification conditions
+* ``--parallel``
-Additional Options (by component)
----------------------------------
+ Check verification conditions in parallel.
File Output
***********
@@ -259,8 +229,6 @@ Code Extraction
Synthesis
*********
-These options are also used by repair during the synthesis stage.
-
* ``--cegis:opttimeout``
Consider a time-out of CE-search as untrusted solution.
@@ -366,3 +334,45 @@ Isabelle
library when verifiying a Leon source file. Keeping it enabled prevents
unsound proofs when postconditions or mappings in the library are wrong.
When disabled, a warning is printed.
+
+Invariant Inference
+*******************
+
+These options are to be used in conjunction with ``--inferInv`` and ``--instrument``.
+
+* ``--cegis``
+
+ Use cegis instead of farkas
+
+* ``--disableInfer``
+
+ Disable automatic inference of auxiliary invariants
+
+* ``--fullunroll``
+
+ Unroll all calls in every unroll step
+
+* ``--inferTemp``
+
+ Infer templates by enumeration
+
+* ``--minbounds``
+
+ Tighten the inferred time bounds
+
+* ``--stats-suffix=s``
+
+ Specifies the suffix of the statistics file
+
+* ``--usereals``
+
+ Interpret the input program as a program over real numbers
+
+* ``--wholeprogram``
+
+ Perform a non-modular whole program analysis
+
+* ``--withmult``
+
+ Do not convert multiplication into a recursive function inside verification conditions
+
diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
index 24bd55af32bb3f5f1f2e27f1f9e4913f2a406497..85c898d81548800735be9cdf6b1b718b1e052a29 100644
--- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
+++ b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
@@ -18,46 +18,50 @@ class OrbRegressionSuite extends LeonRegressionSuite {
}
}
- private def testInference(f: File, bound: Int) {
+ private def testInference(f: File, bound: Option[Int] = None) {
- val ctx = createLeonContext("--inferInv", "--minbounds", "--timeout="+bound)
+ val ctx = createLeonContext("--inferInv")
val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)
val processPipe = InferInvariantsPhase
val (ctx3, report) = processPipe.run(ctx2, program)
- val fails = report.conditions.filterNot(_.invariant.isDefined)
- if (!fails.isEmpty)
- fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}")
+ if (report.conditions.isEmpty)
+ fail(s"Nothing was solved")
+ else {
+ val fails = report.conditions.filterNot(_.prettyInv.isDefined)
+ if (!fails.isEmpty)
+ fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}")
+ }
}
forEachFileIn("regression/orb/timing") { f =>
test("Timing: " + f.getName) {
- testInference(f, 50)
+ testInference(f)
}
}
forEachFileIn("regression/orb/stack/") { f =>
test("Stack: " + f.getName) {
- testInference(f, 50)
+ testInference(f)
}
}
forEachFileIn("regression/orb//depth") { f =>
test("Depth: " + f.getName) {
- testInference(f, 50)
+ testInference(f)
}
}
forEachFileIn("regression/orb/numerical") { f =>
test("Numerical: " + f.getName) {
- testInference(f, 50)
+ testInference(f)
}
}
forEachFileIn("regression/orb/combined/") { f =>
test("Multiple Instrumentations: " + f.getName) {
- testInference(f, 50)
+ testInference(f)
}
}
}
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 9fd15b6d4d97f1b8172a5f3704be66c4abd1fffa..50b845f923e2356d1ce4c0c9a27692a78cd30ce5 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -7,6 +7,7 @@ import leon.test._
import leon.utils._
import leon.frontends.scalac.ExtractionPhase
import leon.repair._
+import leon.verification.VerificationPhase
class RepairSuite extends LeonRegressionSuite {
val pipeline = ExtractionPhase andThen
@@ -34,7 +35,8 @@ class RepairSuite extends LeonRegressionSuite {
interruptManager = new InterruptManager(reporter),
options = Seq(
LeonOption(SharedOptions.optFunctions)(Seq(fileToFun(name))),
- LeonOption(SharedOptions.optTimeout)(60L)
+ LeonOption(VerificationPhase.optParallelVCs)(true),
+ LeonOption(SharedOptions.optTimeout)(180L)
)
)
diff --git a/src/test/scala/leon/regression/testcases/TestCasesCompile.scala b/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
index 994a619013f38a6ce51e1b15fcdf9d5ef49cc763..333413721e1b1d1e6f058664997ec53209a0d886 100644
--- a/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
+++ b/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
@@ -4,11 +4,10 @@ package leon.regression.testcases
import leon._
import leon.test._
-import org.scalatest.time.SpanSugar._
import java.io.File
-import org.scalatest.ParallelTestExecution
-class TestCasesCompile extends LeonRegressionSuite {
+abstract class TestCasesCompile(testDir: String) extends LeonRegressionSuite {
+
val pipeline = frontends.scalac.ExtractionPhase andThen new utils.PreprocessingPhase(desugarXLang = true)
private def filesIn(path : String): Seq[File] = {
@@ -19,11 +18,7 @@ class TestCasesCompile extends LeonRegressionSuite {
val baseDir = "regression/testcases/"
- val allTests = (filesIn(baseDir+"repair/") ++
- filesIn(baseDir+"runtime/") ++
- filesIn(baseDir+"synthesis/") ++
- filesIn(baseDir+"verification/") ++
- filesIn(baseDir+"web/")).sortBy(_.getAbsolutePath)
+ val allTests = filesIn(baseDir + testDir)
allTests.foreach { f =>
@@ -45,3 +40,9 @@ class TestCasesCompile extends LeonRegressionSuite {
}
}
}
+
+class TestcasesCompile1 extends TestCasesCompile("repair/")
+class TestcasesCompile2 extends TestCasesCompile("runtime/")
+class TestcasesCompile3 extends TestCasesCompile("synthesis/")
+class TestcasesCompile4 extends TestCasesCompile("verification/")
+class TestcasesCompile5 extends TestCasesCompile("web/")
\ No newline at end of file
diff --git a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
index bd44226988a11516cfadb4eec35174972662d263..d350bd04b4c68f7838676048b47b085b5d54e4b8 100644
--- a/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/LibraryVerificationSuite.scala
@@ -6,13 +6,13 @@ import leon._
import leon.test._
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
-import leon.verification.AnalysisPhase
+import leon.verification.VerificationPhase
class LibraryVerificationSuite extends LeonRegressionSuite {
test("Verify the library") {
val pipeline = ExtractionPhase andThen
new PreprocessingPhase andThen
- AnalysisPhase
+ VerificationPhase
val ctx = Main.processOptions(Seq("--functions=_")).copy(reporter = new TestSilentReporter())
diff --git a/src/test/scala/leon/regression/verification/NewSolversSuite.scala b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
index 6eac7183e9244661e024fdaa9f9cc770c16f7768..6065d8232341060f0f0eeae735961ae8c5e73da3 100644
--- a/src/test/scala/leon/regression/verification/NewSolversSuite.scala
+++ b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
@@ -4,7 +4,7 @@ package leon.regression.verification
import _root_.smtlib.interpreters._
import leon._
-import leon.verification.AnalysisPhase
+import leon.verification.VerificationPhase
/* @EK: Disabled for now as many tests fail
class NewSolversSuite extends VerificationSuite {
diff --git a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
deleted file mode 100644
index c54ec2b5908dc46f68880c598034518653bbc512..0000000000000000000000000000000000000000
--- a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.regression
-package verification
-
-import _root_.smtlib.interpreters._
-
-// If you add another regression test, make sure it contains one object whose name matches the file name
-// This is because we compile all tests from each folder separately.
-class PureScalaVerificationSuite extends VerificationSuite {
-
- val testDir = "regression/verification/purescala/"
-
- val optionVariants: List[List[String]] = {
- val isZ3Available = try {
- Z3Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
-
- val isCVC4Available = try {
- CVC4Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
-
- List(
- List("--feelinglucky"),
- List("--codegen", "--evalground", "--feelinglucky"),
- List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
- ) ++ (
- if (isZ3Available) List(
- List("--solvers=smt-z3", "--feelinglucky")
- ) else Nil
- ) ++ (
- if (isCVC4Available) List(
- List("--solvers=smt-cvc4", "--feelinglucky")
- ) else Nil
- )
- }
-
-}
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index 48fdd416931ffefefed6c3ee1447320a1e185f48..b23fb0c4e3516121a1489752ed89dcb0835ee2d2 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -6,7 +6,7 @@ import leon._
import leon.test._
import leon.utils.UniqueCounter
-import leon.verification.{AnalysisPhase, VerificationReport}
+import leon.verification.{VerificationPhase, VerificationReport}
import leon.purescala.Definitions.Program
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
@@ -15,8 +15,8 @@ import leon.xlang.FixReportLabels
import org.scalatest.{Reporter => _, _}
-// If you add another regression test, make sure it contains one object whose name matches the file name
-// This is because we compile all tests from each folder separately.
+// If you add another regression test, make sure it contains exactly one object, whose name matches the file name.
+// This is because we compile all tests from each folder together.
trait VerificationSuite extends LeonRegressionSuite {
val optionVariants: List[List[String]]
@@ -38,7 +38,7 @@ trait VerificationSuite extends LeonRegressionSuite {
val analysis =
(if (isabelle) AdaptationPhase else NoopPhase[Program]) andThen
- AnalysisPhase andThen
+ VerificationPhase andThen
(if (desugarXLang) FixReportLabels else NoopPhase[VerificationReport])
val ctx = createLeonContext(files:_*)
@@ -91,37 +91,44 @@ trait VerificationSuite extends LeonRegressionSuite {
mkTest(files, cat)(block)
}
- override def run(testName: Option[String], args: Args): Status = {
- forEachFileIn("valid") { output =>
- val Output(report, reporter) = output
- for ((vc, vr) <- report.vrs if vr.isInvalid) {
- fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
- }
- for ((vc, vr) <- report.vrs if vr.isInconclusive) {
- fail(s"The following verification condition was inconclusive: $vc @${vc.getPos}")
- }
- reporter.terminateIfError()
+ protected def testValid() = forEachFileIn("valid") { output =>
+ val Output(report, reporter) = output
+ for ((vc, vr) <- report.vrs if vr.isInvalid) {
+ fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
}
-
- forEachFileIn("invalid") { output =>
- val Output(report, _) = output
- assert(report.totalUnknown === 0,
- "There should not be unknown verification conditions.")
- assert(report.totalInvalid > 0,
- "There should be at least one invalid verification condition.")
+ for ((vc, vr) <- report.vrs if vr.isInconclusive) {
+ fail(s"The following verification condition was inconclusive: $vc @${vc.getPos}")
}
+ reporter.terminateIfError()
+ }
- forEachFileIn("unknown") { output =>
- val Output(report, reporter) = output
- for ((vc, vr) <- report.vrs if vr.isInvalid) {
- fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
- }
- assert(report.totalUnknown > 0,
- "There should be at least one unknown verification condition.")
+ protected def testInvalid() = forEachFileIn("invalid") { output =>
+ val Output(report, _) = output
+ assert(report.totalUnknown === 0,
+ "There should not be unknown verification conditions.")
+ assert(report.totalInvalid > 0,
+ "There should be at least one invalid verification condition.")
+ }
- reporter.terminateIfError()
+ protected def testUnknown() = forEachFileIn("unknown") { output =>
+ val Output(report, reporter) = output
+ for ((vc, vr) <- report.vrs if vr.isInvalid) {
+ fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
}
+ assert(report.totalUnknown > 0,
+ "There should be at least one unknown verification condition.")
+
+ reporter.terminateIfError()
+ }
+ protected def testAll() = {
+ testValid()
+ testInvalid()
+ testUnknown()
+ }
+
+ override def run(testName: Option[String], args: Args): Status = {
+ testAll()
super.run(testName, args)
}
}
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 3a9783e7036ca82d51298b6eb1751e5ee024d46a..8511ebfea95d4d6a412d82922ffb1e6fb870d312 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -4,6 +4,8 @@ package leon.regression.verification
import smtlib.interpreters.Z3Interpreter
+// If you add another regression test, make sure it contains exactly one object, whose name matches the file name.
+// This is because we compile all tests from each folder together.
class XLangVerificationSuite extends VerificationSuite {
val optionVariants: List[List[String]] = {
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d308e840f159a8ab7de49380d920dfc12ee8d2ad
--- /dev/null
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -0,0 +1,71 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.regression.verification
+package purescala
+
+import smtlib.interpreters.{CVC4Interpreter, Z3Interpreter}
+
+// If you add another regression test, make sure it contains one object whose name matches the file name
+// This is because we compile all tests from each folder together.
+abstract class PureScalaVerificationSuite extends VerificationSuite {
+
+ val testDir = "regression/verification/purescala/"
+
+ val isZ3Available = try {
+ Z3Interpreter.buildDefault.free()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ val isCVC4Available = try {
+ CVC4Interpreter.buildDefault.free()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ val opts: List[List[String]] = {
+ List(
+ List("--feelinglucky"),
+ List("--codegen", "--evalground", "--feelinglucky"),
+ List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
+ ) ++ (
+ if (isZ3Available) List(
+ List("--solvers=smt-z3", "--feelinglucky")
+ ) else Nil
+ ) ++ (
+ if (isCVC4Available) List(
+ List("--solvers=smt-cvc4", "--feelinglucky")
+ ) else Nil
+ )
+ }
+
+}
+
+trait PureScalaValidSuite extends PureScalaVerificationSuite {
+ override def testAll() = testValid()
+}
+
+class PureScalaValidSuite1 extends PureScalaValidSuite {
+ val optionVariants = List(opts(0))
+}
+class PureScalaValidSuite2 extends PureScalaValidSuite {
+ val optionVariants = List(opts(1))
+}
+class PureScalaValidSuite3 extends PureScalaValidSuite {
+ val optionVariants = List(opts(2))
+}
+class PureScalaValidSuiteZ3 extends PureScalaValidSuite {
+ val optionVariants = if (isZ3Available) List(opts(3)) else Nil
+}
+class PureScalaValidSuiteCVC4 extends PureScalaValidSuite {
+ val optionVariants = if (isCVC4Available) List(opts(4)) else Nil
+}
+
+class PureScalaInvalidSuite extends PureScalaVerificationSuite {
+ override def testAll() = testInvalid()
+ val optionVariants = opts
+}
diff --git a/testcases/verification/datastructures/BinarySearchTreeQuant.scala b/testcases/verification/datastructures/BinarySearchTreeQuant.scala
index a435e69ca7a0574937f7368e499c5750983133b3..b5b072550da63b0760ebe55b2a5e5c2553249f86 100644
--- a/testcases/verification/datastructures/BinarySearchTreeQuant.scala
+++ b/testcases/verification/datastructures/BinarySearchTreeQuant.scala
@@ -2,41 +2,49 @@ import leon.lang._
import leon.collection._
object BSTSimpler {
- sealed abstract class Tree
+ case object Leaf extends Tree
case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
- case class Leaf() extends Tree
-
- def content(tree: Tree): Set[BigInt] = tree match {
- case Leaf() => Set.empty[BigInt]
- case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
+ sealed abstract class Tree {
+ def isBST: Boolean = this match {
+ case Leaf => true
+ case Node(left, v, right) => {
+ left.isBST && right.isBST &&
+ forall((x:BigInt) => (left.content.contains(x) ==> x < v)) &&
+ forall((x:BigInt) => (right.content.contains(x) ==> v < x))
+ }
+ }
- def isBST(tree: Tree) : Boolean = tree match {
- case Leaf() => true
- case Node(left, v, right) => {
- isBST(left) && isBST(right) &&
- forall((x:BigInt) => (content(left).contains(x) ==> x < v)) &&
- forall((x:BigInt) => (content(right).contains(x) ==> v < x))
+ def content: Set[BigInt] = this match {
+ case Leaf => Set.empty[BigInt]
+ case Node(l, v, r) => l.content ++ Set(v) ++ r.content
}
- }
- def emptySet(): Tree = Leaf()
+ def insert(value: BigInt): Node = {
+ require(isBST)
+ this match {
+ case Leaf => Node(Leaf, value, Leaf)
+ case Node(l, v, r) => (if (v < value) {
+ Node(l, v, r.insert(value))
+ } else if (v > value) {
+ Node(l.insert(value), v, r)
+ } else {
+ Node(l, v, r)
+ })
+ }
+ } ensuring(res => res.isBST && res.content == content ++ Set(value))
- def insert(tree: Tree, value: BigInt): Node = {
- require(isBST(tree))
- tree match {
- case Leaf() => Node(Leaf(), value, Leaf())
- case Node(l, v, r) => (if (v < value) {
- Node(l, v, insert(r, value))
- } else if (v > value) {
- Node(insert(l, value), v, r)
- } else {
- Node(l, v, r)
- })
- }
- } ensuring(res => isBST(res) && content(res) == content(tree) ++ Set(value))
+ def contains(value: BigInt): Boolean = {
+ require(isBST)
+ this match {
+ case Leaf => false
+ case Node(l,v,r) => (if (v < value) {
+ r.contains(value)
+ } else if (v > value) {
+ l.contains(value)
+ } else true)
+ }
+ } ensuring(res => (res == content.contains(value)))
- def createRoot(v: BigInt): Node = {
- Node(Leaf(), v, Leaf())
- } ensuring (content(_) == Set(v))
+ }
+ def empty: Tree = Leaf
}
diff --git a/testcases/web/invariant/01_InsertionSort.scala b/testcases/web/invariant/01_InsertionSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bcf4b8d98f5b37ad1afd229454990d71f24c8b07
--- /dev/null
+++ b/testcases/web/invariant/01_InsertionSort.scala
@@ -0,0 +1,26 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail:List) extends List
+ case class Nil() extends List
+
+ def size(l : List) : BigInt = (l match {
+ case Cons(_, xs) => 1 + size(xs)
+ case _ => 0
+ })
+
+ def sortedIns(e: BigInt, l: List): List = {
+ l match {
+ case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+ case _ => Cons(e,Nil())
+ }
+ } ensuring(res => size(res) == size(l) + 1 && time <= ? * size(l) + ?)
+
+ def sort(l: List): List = (l match {
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ case _ => Nil()
+
+ }) ensuring(res => size(res) == size(l) && time <= ? * (size(l)*size(l)) + ?)
+}
diff --git a/testcases/web/invariant/02_ListOps.scala b/testcases/web/invariant/02_ListOps.scala
new file mode 100644
index 0000000000000000000000000000000000000000..23ca52bbd72b971c0b6915fa9c3fb7576c155a47
--- /dev/null
+++ b/testcases/web/invariant/02_ListOps.scala
@@ -0,0 +1,60 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ })
+
+ def append(l1: List, l2: List): List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => Cons(x, append(xs, l2))
+
+ }) ensuring (res => size(l1) + size(l2) == size(res) && time <= ? *size(l1) + ?)
+
+ def reverseRec(l1: List, l2: List): List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => reverseRec(xs, Cons(x, l2))
+
+ }) ensuring (res => size(l1) + size(l2) == size(res) && time <= ? *size(l1) + ?)
+
+ def reverse(l: List): List = {
+ reverseRec(l, Nil())
+
+ } ensuring (res => size(l) == size(res) && time <= ? * size(l) + ?)
+
+ def reverse2(l: List): List = {
+ l match {
+ case Nil() => l
+ case Cons(hd, tl) => append(reverse2(tl), Cons(hd, Nil()))
+ }
+ } ensuring (res => size(res) == size(l) && time <= ? *(size(l)*size(l)) + ?)
+
+ def remove(elem: BigInt, l: List): List = {
+ l match {
+ case Nil() => Nil()
+ case Cons(hd, tl) => if (hd == elem) remove(elem, tl) else Cons(hd, remove(elem, tl))
+ }
+ } ensuring (res => size(l) >= size(res) && time <= ? *size(l) + ?)
+
+ def contains(list: List, elem: BigInt): Boolean = (list match {
+ case Nil() => false
+ case Cons(x, xs) => x == elem || contains(xs, elem)
+
+ }) ensuring (res => true && time <= ? *size(list) + ?)
+
+ def distinct(l: List): List = (
+ l match {
+ case Nil() => Nil()
+ case Cons(x, xs) => {
+ val newl = distinct(xs)
+ if (contains(newl, x)) newl
+ else Cons(x, newl)
+ }
+ }) ensuring (res => size(l) >= size(res) && time <= ? *(size(l)*size(l)) + ?)
+}
diff --git a/testcases/web/invariant/03_TreeOps.scala b/testcases/web/invariant/03_TreeOps.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6d13fcef7a45ce58846c985daceacb36ae67ca5c
--- /dev/null
+++ b/testcases/web/invariant/03_TreeOps.scala
@@ -0,0 +1,93 @@
+import leon.invariant._
+import leon.instrumentation._
+
+
+object TreeOperations {
+
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Tree
+ case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def listSize(l: List): BigInt = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + listSize(t)
+ })
+
+ def size(t: Tree): BigInt = {
+ t match {
+ case Leaf() => 0
+ case Node(l, x, r) => {
+ size(l) + size(r) + 1
+ }
+ }
+ }
+
+ def height(t: Tree): BigInt = {
+ t match {
+ case Leaf() => 0
+ case Node(l, x, r) => {
+ val hl = height(l)
+ val hr = height(r)
+ if (hl > hr) hl + 1 else hr + 1
+ }
+ }
+ }
+
+ def insert(elem: BigInt, t: Tree): Tree = {
+ t match {
+ case Leaf() => Node(Leaf(), elem, Leaf())
+ case Node(l, x, r) => if (x <= elem) Node(l, x, insert(elem, r))
+ else Node(insert(elem, l), x, r)
+ }
+ } ensuring (res => height(res) <= height(t) + 1 && time <= ? *height(t) + ?)
+
+ def addAll(l: List, t: Tree): Tree = {
+ l match {
+ case Nil() => t
+ case Cons(x, xs) =>{
+ val newt = insert(x, t)
+ addAll(xs, newt)
+ }
+ }
+ } ensuring(_ => time <= ? *(listSize(l) * (height(t) + listSize(l))) + ? *listSize(l) + ?)
+
+ def remove(elem: BigInt, t: Tree): Tree = {
+ t match {
+ case Leaf() => Leaf()
+ case Node(l, x, r) => {
+
+ if (x < elem) Node(l, x, remove(elem, r))
+ else if (x > elem) Node(remove(elem, l), x, r)
+ else {
+ t match {
+ case Node(Leaf(), x, Leaf()) => Leaf()
+ case Node(Leaf(), x, Node(_, rx, _)) => Node(Leaf(), rx, remove(rx, r))
+ case Node(Node(_, lx, _), x, r) => Node(remove(lx, l), lx, r)
+ case _ => Leaf()
+ }
+ }
+ }
+ }
+ } ensuring (res => height(res) <= height(t) && time <= ? *height(t) + ?)
+
+ def removeAll(l: List, t: Tree): Tree = {
+ l match {
+ case Nil() => t
+ case Cons(x, xs) => removeAll(xs, remove(x, t))
+ }
+ } ensuring(_ => time <= ? *(listSize(l) * height(t)) + ? *listSize(l) + ?)
+
+ def contains(elem : BigInt, t : Tree) : Boolean = {
+ t match {
+ case Leaf() => false
+ case Node(l, x, r) =>
+ if(x == elem) true
+ else if (x < elem) contains(elem, r)
+ else contains(elem, l)
+ }
+ } ensuring (_ => time <= ? * height(t) + ?)
+}
\ No newline at end of file
diff --git a/testcases/web/invariant/04_PropositionalLogic.scala b/testcases/web/invariant/04_PropositionalLogic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..afae7b0a0114f64974060c0885dd6d3feff01f2f
--- /dev/null
+++ b/testcases/web/invariant/04_PropositionalLogic.scala
@@ -0,0 +1,114 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object PropositionalLogic {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Literal(id: BigInt) extends Formula
+ case class True() extends Formula
+ case class False() extends Formula
+
+ case class Pair(f: Formula, b: Boolean)
+
+ sealed abstract class List
+ case class Cons(x: Pair, xs: List) extends List
+ case class Nil() extends List
+
+ def size(f : Formula) : BigInt = (f match {
+ case And(lhs, rhs) => size(lhs) + size(rhs) + 1
+ case Or(lhs, rhs) => size(lhs) + size(rhs) + 1
+ case Implies(lhs, rhs) => size(lhs) + size(rhs) + 1
+ case Not(f) => size(f) + 1
+ case _ => 1
+ })
+
+ def removeImplies(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => And(removeImplies(lhs), removeImplies(rhs))
+ case Or(lhs, rhs) => Or(removeImplies(lhs), removeImplies(rhs))
+ case Implies(lhs, rhs) => Or(Not(removeImplies(lhs)),removeImplies(rhs))
+ case Not(f) => Not(removeImplies(f))
+ case _ => f
+
+ }) ensuring(_ => time <= ? * size(f) + ?)
+
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case Not(Literal(_)) => formula
+ case Literal(_) => formula
+ case Not(True()) => False()
+ case Not(False()) => True()
+ case _ => formula
+ }) ensuring(_ => time <= ? * size(formula) + ?)
+
+ def isNNF(f: Formula): Boolean = { f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => false
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case _ => true
+ }} ensuring(_ => time <= ? * size(f) + ?)
+
+ def simplify(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => {
+ val sl = simplify(lhs)
+ val sr = simplify(rhs)
+
+ //if lhs or rhs is false, return false
+ //if lhs is true return rhs
+ //if rhs is true return lhs
+ (sl,sr) match {
+ case (False(), _) => False()
+ case (_, False()) => False()
+ case (True(), _) => sr
+ case (_, True()) => sl
+ case _ => And(sl, sr)
+ }
+ }
+ case Or(lhs, rhs) => {
+ val sl = simplify(lhs)
+ val sr = simplify(rhs)
+
+ //if lhs or rhs is true, return true
+ //if lhs is false return rhs
+ //if rhs is false return lhs
+ (sl,sr) match {
+ case (True(), _) => True()
+ case (_, True()) => True()
+ case (False(), _) => sr
+ case (_, False()) => sl
+ case _ => Or(sl, sr)
+ }
+ }
+ case Implies(lhs, rhs) => {
+ val sl = simplify(lhs)
+ val sr = simplify(rhs)
+
+ //if lhs is false return true
+ //if rhs is true return true
+ //if lhs is true return rhs
+ //if rhs is false return Not(rhs)
+ (sl,sr) match {
+ case (False(), _) => True()
+ case (_, True()) => True()
+ case (True(), _) => sr
+ case (_, False()) => Not(sl)
+ case _ => Implies(sl, sr)
+ }
+ }
+ case Not(True()) => False()
+ case Not(False()) => True()
+ case _ => f
+
+ }) ensuring(_ => time <= ? *size(f) + ?)
+}
diff --git a/testcases/web/invariant/01_Binary_Trie.scala b/testcases/web/invariant/05_BinaryTrie.scala
similarity index 100%
rename from testcases/web/invariant/01_Binary_Trie.scala
rename to testcases/web/invariant/05_BinaryTrie.scala
diff --git a/testcases/web/invariant/06_String_Buffer.scala b/testcases/web/invariant/06_StringBuffer.scala
similarity index 100%
rename from testcases/web/invariant/06_String_Buffer.scala
rename to testcases/web/invariant/06_StringBuffer.scala
diff --git a/testcases/web/invariant/03_List_Concat.scala b/testcases/web/invariant/07_ConcatVariations.scala
similarity index 100%
rename from testcases/web/invariant/03_List_Concat.scala
rename to testcases/web/invariant/07_ConcatVariations.scala
diff --git a/testcases/web/invariant/05_Leftist_Heap.scala b/testcases/web/invariant/08_LeftistHeap.scala
similarity index 100%
rename from testcases/web/invariant/05_Leftist_Heap.scala
rename to testcases/web/invariant/08_LeftistHeap.scala
diff --git a/testcases/web/invariant/04_Red_Black_Tree.scala b/testcases/web/invariant/09_RedBlackTree.scala
similarity index 100%
rename from testcases/web/invariant/04_Red_Black_Tree.scala
rename to testcases/web/invariant/09_RedBlackTree.scala
diff --git a/testcases/web/invariant/02_Binomial_Heap.scala b/testcases/web/invariant/10_BinomialHeap.scala
similarity index 100%
rename from testcases/web/invariant/02_Binomial_Heap.scala
rename to testcases/web/invariant/10_BinomialHeap.scala
diff --git a/testcases/web/invariant/11_Amortized_BigNums.scala b/testcases/web/invariant/11_Amortized_BigNums.scala
new file mode 100644
index 0000000000000000000000000000000000000000..883d1f45ab8752668070699c840edd7a3de160b9
--- /dev/null
+++ b/testcases/web/invariant/11_Amortized_BigNums.scala
@@ -0,0 +1,50 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object BigNums {
+ sealed abstract class BigNum
+ case class Cons(head: BigInt, tail: BigNum) extends BigNum
+ case class Nil() extends BigNum
+
+ def incrTime(l: BigNum) : BigInt = {
+ l match {
+ case Nil() => 1
+ case Cons(x, tail) =>
+ if(x == 0) 1
+ else 1 + incrTime(tail)
+ }
+ }
+
+ def potentialIncr(l: BigNum) : BigInt = {
+ l match {
+ case Nil() => 0
+ case Cons(x, tail) =>
+ if(x == 0) potentialIncr(tail)
+ else 1 + potentialIncr(tail)
+ }
+ }
+
+ def increment(l: BigNum) : BigNum = {
+ l match {
+ case Nil() => Cons(1,l)
+ case Cons(x, tail) =>
+ if(x == 0) Cons(1, tail)
+ else Cons(0, increment(tail))
+ }
+ } ensuring (res => time <= ? * incrTime(l) + ? && incrTime(l) + potentialIncr(res) - potentialIncr(l) <= ?)
+
+ /**
+ * Nop is the number of operations
+ */
+ def incrUntil(nop: BigInt, l: BigNum) : BigNum = {
+ if(nop == 0) l
+ else {
+ incrUntil(nop-1, increment(l))
+ }
+ } ensuring (res => time <= ? * nop + ? * potentialIncr(l) + ?)
+
+ def count(nop: BigInt) : BigNum = {
+ incrUntil(nop, Nil())
+ } ensuring (res => time <= ? * nop + ?)
+
+}
diff --git a/testcases/web/invariant/12_Par_Folds.scala b/testcases/web/invariant/12_Par_Folds.scala
new file mode 100755
index 0000000000000000000000000000000000000000..5c4f51d119e18aa74d1fc0c263094a5cf6966a42
--- /dev/null
+++ b/testcases/web/invariant/12_Par_Folds.scala
@@ -0,0 +1,81 @@
+import leon.instrumentation._
+import leon.invariant._
+
+object TreeMaps {
+
+ sealed abstract class Tree
+ case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def height(t: Tree): BigInt = {
+ t match {
+ case Leaf() => 0
+ case Node(l, x, r) => {
+ val hl = height(l)
+ val hr = height(r)
+ if (hl > hr) hl + 1 else hr + 1
+ }
+ }
+ }
+
+ def parallelSearch(elem : BigInt, t : Tree) : Boolean = {
+ t match {
+ case Leaf() => false
+ case Node(l, x, r) =>
+ if(x == elem) true
+ else {
+ val r1 = parallelSearch(elem, r)
+ val r2 = parallelSearch(elem, l)
+ if(r1 || r2) true
+ else false
+ }
+ }
+ } ensuring(_ => depth <= ? * height(t) + ?)
+
+
+ def squareMap(t : Tree) : Tree = {
+ t match {
+ case Leaf() => t
+ case Node(l, x, r) =>
+ val nl = squareMap(l)
+ val nr = squareMap(r)
+ Node(nl, x*x, nr)
+ }
+ } ensuring (_ => depth <= ? * height(t) + ?)
+
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List): BigInt = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ })
+
+ def fact(n : BigInt) : BigInt = {
+ require(n >= 0)
+
+ if(n == 1 || n == 0) BigInt(1)
+ else n * fact(n-1)
+
+ } ensuring(_ => depth <= ? * n + ?)
+
+ def descending(l: List, k: BigInt) : Boolean = {
+ l match {
+ case Nil() => true
+ case Cons(x, t) => x > 0 && x <= k && descending(t, x-1)
+ }
+ }
+
+ def factMap(l: List, k: BigInt): List = {
+ require(descending(l, k) && k >= 0)
+
+ l match {
+ case Nil() => Nil()
+ case Cons(x, t) => {
+ val f = fact(x)
+ Cons(f, factMap(t, x-1))
+ }
+
+ }} ensuring(_ => depth <= ? * k + ?)
+}
\ No newline at end of file
diff --git a/testcases/web/invariant/13_Par_MSort.scala b/testcases/web/invariant/13_Par_MSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8a818137eb32a3f9eb63297a6219faf219cec4eb
--- /dev/null
+++ b/testcases/web/invariant/13_Par_MSort.scala
@@ -0,0 +1,57 @@
+import leon.instrumentation._
+import leon.invariant._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List): BigInt = {
+ l match {
+ case Nil() => BigInt(0)
+ case Cons(x, xs) => 1 + size(xs)
+ }
+ } ensuring (res => res >= 0)
+
+ def length(l: List): BigInt = {
+ l match {
+ case Nil() => BigInt(0)
+ case Cons(x, xs) => 1 + length(xs)
+ }
+ } ensuring (res => res >= 0 && res == size(l) && depth <= ? * size(l) + ?)
+
+ def split(l: List, n: BigInt): (List, List) = {
+ require(n >= 0 && n <= size(l))
+ if (n <= 0) (Nil(), l)
+ else
+ l match {
+ case Nil() => (Nil(), l)
+ case Cons(x, xs) => {
+ val (fst, snd) = split(xs, n - 1)
+ (Cons(x, fst), snd)
+ }
+ }
+ } ensuring (res => size(res._2) == size(l) - n && size(res._1) == n && depth <= ? * n + ?)
+
+ def merge(l1: List, l2: List): List = (l2 match {
+ case Nil() => l1
+ case Cons(x, xs) =>
+ l1 match {
+ case Nil() => l2
+ case Cons(y, ys) =>
+ if (y < x)
+ Cons(y, merge(ys, l2))
+ else
+ Cons(x, merge(l1, xs))
+ }
+ }) ensuring (res => size(l1) + size(l2) == size(res) && depth <= ? * size(l1) + ? * size(l2) + ?)
+
+ def mergeSort(l: List): List = (l match {
+ case Nil() => l
+ case Cons(x, Nil()) => l
+ case _ =>
+ val (fst, snd) = split(l, length(l) / 2)
+ merge(mergeSort(fst), mergeSort(snd))
+
+ }) ensuring (res => size(res) == size(l) && depth <= ? * size(l) + ?)
+}
diff --git a/testcases/web/invariant/14_Par_PropLogic.scala b/testcases/web/invariant/14_Par_PropLogic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..096dc8f60377a5dd10ad94f3fbd0ddf33c3f6481
--- /dev/null
+++ b/testcases/web/invariant/14_Par_PropLogic.scala
@@ -0,0 +1,113 @@
+import leon.instrumentation._
+import leon.invariant._
+import leon.annotation._
+
+object PropLogicDepth {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Literal(id: BigInt) extends Formula
+ case class True() extends Formula
+ case class False() extends Formula
+
+ def max(x: BigInt, y: BigInt) = if (x >= y) x else y
+
+ def nestingDepth(f: Formula): BigInt = (f match {
+ case And(lhs, rhs) => max(nestingDepth(lhs), nestingDepth(rhs)) + 1
+ case Or(lhs, rhs) => max(nestingDepth(lhs), nestingDepth(rhs)) + 1
+ case Implies(lhs, rhs) => max(nestingDepth(lhs), nestingDepth(rhs)) + 1
+ case Not(f) => nestingDepth(f) + 1
+ case _ => 1
+ })
+
+ def removeImplies(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => And(removeImplies(lhs), removeImplies(rhs))
+ case Or(lhs, rhs) => Or(removeImplies(lhs), removeImplies(rhs))
+ case Implies(lhs, rhs) => Or(Not(removeImplies(lhs)), removeImplies(rhs))
+ case Not(f) => Not(removeImplies(f))
+ case _ => f
+
+ }) ensuring (_ => depth <= ? * nestingDepth(f) + ?)
+
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case Not(Literal(_)) => formula
+ case Literal(_) => formula
+ case Not(True()) => False()
+ case Not(False()) => True()
+ case _ => formula
+ }) ensuring (_ => depth <= ? * nestingDepth(formula) + ?)
+
+ def isNNF(f: Formula): Boolean = {
+ f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => false
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case _ => true
+ }
+ } ensuring (_ => depth <= ? * nestingDepth(f) + ?)
+
+ def simplify(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => {
+ val sl = simplify(lhs)
+ val sr = simplify(rhs)
+
+ //if lhs or rhs is false, return false
+ //if lhs is true return rhs
+ //if rhs is true return lhs
+ (sl, sr) match {
+ case (False(), _) => False()
+ case (_, False()) => False()
+ case (True(), _) => sr
+ case (_, True()) => sl
+ case _ => And(sl, sr)
+ }
+ }
+ case Or(lhs, rhs) => {
+ val sl = simplify(lhs)
+ val sr = simplify(rhs)
+
+ //if lhs or rhs is true, return true
+ //if lhs is false return rhs
+ //if rhs is false return lhs
+ (sl, sr) match {
+ case (True(), _) => True()
+ case (_, True()) => True()
+ case (False(), _) => sr
+ case (_, False()) => sl
+ case _ => Or(sl, sr)
+ }
+ }
+ case Implies(lhs, rhs) => {
+ val sl = simplify(lhs)
+ val sr = simplify(rhs)
+
+ //if lhs is false return true
+ //if rhs is true return true
+ //if lhs is true return rhs
+ //if rhs is false return Not(rhs)
+ (sl, sr) match {
+ case (False(), _) => True()
+ case (_, True()) => True()
+ case (True(), _) => sr
+ case (_, False()) => Not(sl)
+ case _ => Implies(sl, sr)
+ }
+ }
+ case Not(True()) => False()
+ case Not(False()) => True()
+ case _ => f
+
+ }) ensuring (_ => depth <= ? * nestingDepth(f) + ?)
+}
\ No newline at end of file
diff --git a/testcases/web/invariant/15_Numerical_SeeSaw.scala b/testcases/web/invariant/15_Numerical_SeeSaw.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bb08b70e78145a64d2eadc7e9ca4eec721b0babb
--- /dev/null
+++ b/testcases/web/invariant/15_Numerical_SeeSaw.scala
@@ -0,0 +1,15 @@
+object SeeSaw {
+ def s(x: BigInt, y: BigInt, z: BigInt): BigInt = {
+ require(y >= 0)
+ if (x >= 100) {
+ y
+ } else if (x <= z) {
+ s(x + 1, y + 2, z)
+ } else if (x <= z + 9) {
+ s(x + 1, y + 3, z)
+ } else {
+ s(x + 2, y + 1, z)
+ }
+ } ensuring (res => (100 - x <= 2 * res))
+ // postcondition is not inductive
+}
\ No newline at end of file