From e439db26e15117c737f796db422b25ea6b0bc7cf Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Tue, 20 Oct 2015 17:12:24 +0200
Subject: [PATCH] Adding supports for analyzing selected functions in Orb
---
.gitignore | 1 +
.../engine/CompositionalTemplateSolver.scala | 22 ++--
.../invariant/engine/ConstraintTracker.scala | 6 +-
.../engine/InferInvariantsPhase.scala | 117 ++++--------------
.../invariant/engine/InferenceContext.scala | 115 ++++++++++++++---
.../invariant/engine/InferenceEngine.scala | 61 ++++-----
.../invariant/engine/InferenceReport.scala | 12 +-
.../invariant/engine/RefinementEngine.scala | 3 +-
.../invariant/engine/SpecInstatiator.scala | 3 +-
.../invariant/engine/TemplateEnumerator.scala | 78 ++++++------
.../engine/UnfoldingTemplateSolver.scala | 29 +++--
.../factories/TemplateSolverFactory.scala | 10 +-
.../templateSolvers/CegisSolver.scala | 13 +-
.../templateSolvers/FarkasLemmaSolver.scala | 15 +--
.../templateSolvers/NLTemplateSolver.scala | 14 +--
.../NLTemplateSolverWithMult.scala | 4 +-
.../templateSolvers/TemplateSolver.scala | 7 +-
.../scala/leon/invariant/util/Minimizer.scala | 16 +--
src/main/scala/leon/invariant/util/Util.scala | 5 +
19 files changed, 265 insertions(+), 266 deletions(-)
diff --git a/.gitignore b/.gitignore
index 057efa0f3..4ef5b5eae 100644
--- a/.gitignore
+++ b/.gitignore
@@ -54,3 +54,4 @@ out-classes
# Isabelle
contrib
+/bin/
diff --git a/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala b/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
index 4c443b3f6..94ee3377c 100644
--- a/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/CompositionalTemplateSolver.scala
@@ -21,7 +21,7 @@ import leon.invariant.factories.TemplateSolverFactory
import leon.invariant.util.Minimizer
import leon.solvers.Model
-class CompositionalTimeBoundSolver(ctx: InferenceContext, rootFd: FunDef)
+class CompositionalTimeBoundSolver(ctx: InferenceContext, prog: Program, rootFd: FunDef)
extends FunctionTemplateSolver {
val printIntermediatePrograms = false
@@ -30,7 +30,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 +45,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 +81,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 +118,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 +148,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 +161,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 +204,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 e50b50bb8..3058a267e 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 4bc1e245f..0b48c1e8c 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,26 +32,19 @@ 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
+ //default values for flags
val dumpStats = false
- var timeout: Int = 15
-
- //defualt true flags
- var modularlyAnalyze = true
+ var vcTimeout: Int = 15
var targettedUnroll = true
-
- //default false flags
var tightBounds = false
var withmult = false
var inferTemp = false
@@ -68,89 +57,33 @@ object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
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 ("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 ("inferTemp", true) =>
+ inferTemp = true
+ case ("cegis", true) =>
+ useCegis = true
+ case ("vcTimeout", timeOut: Int) =>
+ vcTimeout = 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 inferctx = new InferenceContext(program, ctx,
+ targettedUnroll, autoInference, dumpStats, tightBounds,
+ withmult, usereals, inferTemp, useCegis, vcTimeout,
+ maxCegisBound, statsSuff)
val report = (new InferenceEngine(inferctx)).run()
//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 = VerificationPhase
- 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 bf3d83845..506fbb139 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -1,32 +1,107 @@
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
/**
* @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,
+ 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 vcTimeout: Int, //in secs
+ val maxCegisBound: Int,
+ val statsSuffix: String) {
val reporter = leonContext.reporter
+ val functionsToInfer = leonContext.findOption(SharedOptions.optFunctions)
+ val totalTimeout = leonContext.findOption(SharedOptions.optTimeout)
+
+ 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
+ Util.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 = Util.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 03202f9db..e3965bfb1 100644
--- a/src/main/scala/leon/invariant/engine/InferenceEngine.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
@@ -20,6 +20,7 @@ import invariant.util.Util._
import invariant.structure._
import invariant.structure.FunctionUtils._
import leon.invariant.factories.TemplateFactory
+import transformations._
/**
* @author ravi
@@ -30,7 +31,7 @@ class InferenceEngine(ctx: InferenceContext) {
def run(): InferenceReport = {
val reporter = ctx.reporter
- val program = ctx.program
+ val program = ctx.inferProgram
reporter.info("Running Inference Engine...")
//register a shutdownhook
@@ -40,15 +41,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)
//println("Inferrence did not succeeded for functions: "+functionsToAnalyze.filterNot(succeededFuncs.contains _).map(_.id))
} else {
var remFuncs = functionsToAnalyze
@@ -57,7 +62,7 @@ class InferenceEngine(ctx: InferenceContext) {
breakable {
while (b <= maxCegisBound) {
Stats.updateCumStats(1, "CegisBoundsTried")
- val succeededFuncs = analyseProgram(remFuncs)
+ val succeededFuncs = analyseProgram(program, remFuncs)
remFuncs = remFuncs.filterNot(succeededFuncs.contains _)
if (remFuncs.isEmpty) break;
b += 5 //increase bounds in steps of 5
@@ -75,12 +80,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,17 +99,20 @@ 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]): 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") ||
@@ -117,27 +125,26 @@ class InferenceEngine(ctx: InferenceContext) {
//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)
+ new CompositionalTimeBoundSolver(ctx, prog, funDef)
else
- new UnfoldingTemplateSolver(currCtx, funDef)
+ 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)) =>
val funsWithTemplates = inferredFuns.filter { fd =>
- val origFd = Util.functionByName(fd.id.name, ctx.program).get
+ val origFd = Util.functionByName(fd.id.name, startProg).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 origFd = Util.functionByName(fd.id.name, startProg).get
val inv = TemplateInstantiator.getAllInvariants(model.get,
Map(origFd -> origFd.getTemplate))
// record the inferred invariants
@@ -151,15 +158,13 @@ class InferenceEngine(ctx: InferenceContext) {
funsWithTemplates.collect {
case fd if fd.hasTemplate => fd -> fd.getTemplate
}.toMap)
- if (ctx.modularlyAnalyze) {
- // 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
- prog
+ // 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)
+
case _ =>
reporter.info("- Exhausted all templates, cannot infer invariants")
val ic = new InferenceCondition(None, origFun)
diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala
index 26337c6ff..97d7de298 100644
--- a/src/main/scala/leon/invariant/engine/InferenceReport.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala
@@ -30,8 +30,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] =
@@ -86,17 +86,17 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContex
case cd if cd.invariant.isDefined =>
cd.fd -> cd.invariant.get
}.toMap
- Util.assignTemplateAndCojoinPost(funToTmpl, ctx.program)
+ Util.assignTemplateAndCojoinPost(funToTmpl, program)
}
def finalProgramWoInstrumentation: Program = {
- val funToUninstFun = ctx.program.definedFunctions.foldLeft(Map[FunDef, FunDef]()) {
+ val funToUninstFun = program.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 Util.functionByName(uninstFunName, ctx.initProgram)
if (uninstFdOpt.isDefined) {
acc + (fd -> uninstFdOpt.get)
} else acc
@@ -106,6 +106,6 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContex
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)
+ Util.assignTemplateAndCojoinPost(Map(), ctx.initProgram, funToPost, uniqueIdDisplay = false)
}
}
\ 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 cce8a3cb4..bf07342b2 100644
--- a/src/main/scala/leon/invariant/engine/RefinementEngine.scala
+++ b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
@@ -18,11 +18,10 @@ import FunctionUtils._
//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
diff --git a/src/main/scala/leon/invariant/engine/SpecInstatiator.scala b/src/main/scala/leon/invariant/engine/SpecInstatiator.scala
index 9961df293..f356edb81 100644
--- a/src/main/scala/leon/invariant/engine/SpecInstatiator.scala
+++ b/src/main/scala/leon/invariant/engine/SpecInstatiator.scala
@@ -22,7 +22,7 @@ import invariant.util.Util._
import invariant.structure._
import FunctionUtils._
-class SpecInstantiator(ctx: InferenceContext, ctrTracker: ConstraintTracker) {
+class SpecInstantiator(ctx: InferenceContext, program: Program, ctrTracker: ConstraintTracker) {
val verbose = false
@@ -31,7 +31,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]()
diff --git a/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala b/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
index 17bfdee4b..9b21ea7b5 100644
--- a/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
+++ b/src/main/scala/leon/invariant/engine/TemplateEnumerator.scala
@@ -11,7 +11,7 @@ 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._
@@ -19,39 +19,38 @@ import invariant.util._
import invariant.structure._
/**
- * 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 +58,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 +81,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
@@ -152,10 +150,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 5a806fa3c..ab05a1747 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._
@@ -35,14 +36,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 +55,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)
}
diff --git a/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala b/src/main/scala/leon/invariant/factories/TemplateSolverFactory.scala
index 25abefa22..469317998 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/templateSolvers/CegisSolver.scala b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
index 305bd98e3..ac64938bc 100644
--- a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
@@ -18,11 +18,9 @@ import invariant.structure._
import invariant.structure.FunctionUtils._
import leon.invariant.util.RealValuedExprEvaluator._
-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]]) = {
@@ -40,7 +38,7 @@ class CegisSolver(ctx: InferenceContext,
val formula = Util.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 +49,7 @@ class CegisSolver(ctx: InferenceContext,
}
class CegisCore(ctx: InferenceContext,
- timeout: Int,
+ program: Program, timeout: Int,
cegisSolver: TemplateSolver) {
val fls = BooleanLiteral(false)
@@ -60,7 +58,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
diff --git a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index 6e80c4749..14f62ae7c 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -24,7 +24,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 +39,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 +54,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)
}
@@ -263,7 +258,7 @@ 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"
+ val filename = program.modules.last.id + "-nlctr" + FileCountGUID.getID + ".smt2"
if (Util.atomNum(simpctrs) >= 5) {
if (solveAsBitvectors)
Util.toZ3SMTLIB(simpctrs, filename, "QF_BV", leonctx, program, useBitvectors = true, bitvecSize = bvsize)
@@ -279,9 +274,7 @@ class FarkasLemmaSolver(ctx: InferenceContext) {
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
}
val solver = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => innerSolver), timeout * 1000))
if (verbose) reporter.info("solving...")
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 47901d3b9..5063a284c 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -27,8 +27,9 @@ 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])
+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 +50,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
@@ -355,7 +355,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, this)
val (res, ctr, model) = cegisSolver.solve(tempIds, expr, precond, solveAsInt = false, initModel)
if (!res.isDefined)
reporter.info("cegis timed-out on the disjunct...")
@@ -471,7 +471,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 = {
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
index 10a232e3f..f3628be51 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
@@ -17,9 +17,9 @@ import invariant.factories._
import invariant.util._
import invariant.structure._
-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)
diff --git a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
index 9b360c2db..61bdc8bf5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
@@ -33,7 +33,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 +72,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,10 +86,6 @@ 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) {
diff --git a/src/main/scala/leon/invariant/util/Minimizer.scala b/src/main/scala/leon/invariant/util/Minimizer.scala
index 78e82db2d..cec35bff1 100644
--- a/src/main/scala/leon/invariant/util/Minimizer.scala
+++ b/src/main/scala/leon/invariant/util/Minimizer.scala
@@ -17,7 +17,7 @@ import invariant.factories._
import leon.invariant.templateSolvers.ExtendedUFSolver
import leon.invariant.util.RealValuedExprEvaluator._
-class Minimizer(ctx: InferenceContext) {
+class Minimizer(ctx: InferenceContext, program: Program) {
val verbose = false
val debugMinimization = false
@@ -26,14 +26,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
@@ -59,8 +56,7 @@ class Minimizer(ctx: InferenceContext) {
// 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))
+ new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), ctx.vcTimeout * 1000))
reporter.info("minimizing...")
var currentModel = initModel
@@ -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/Util.scala b/src/main/scala/leon/invariant/util/Util.scala
index 5a101569e..53af2083a 100644
--- a/src/main/scala/leon/invariant/util/Util.scala
+++ b/src/main/scala/leon/invariant/util/Util.scala
@@ -98,6 +98,11 @@ object Util {
val tru = BooleanLiteral(true)
val fls = BooleanLiteral(false)
+ 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
--
GitLab