From f88e636c77e2df943aeae879cd1838df0cc4fc6a Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Mon, 15 Feb 2016 17:23:50 +0100
Subject: [PATCH] Integrating Orb with lazy verification
---
.../engine/UnfoldingTemplateSolver.scala | 25 +++++-----
.../leon/laziness/LazyVerificationPhase.scala | 8 ++--
vcs-temp | 48 -------------------
3 files changed, 14 insertions(+), 67 deletions(-)
delete mode 100644 vcs-temp
diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
index 6ae355f4c..a5e48d447 100644
--- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
@@ -247,23 +247,20 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
} else {
(augmentedProg, newFundefs(rootFd))
}
- //println("New Root: "+newroot)
- import leon.solvers.smtlib.SMTLIBZ3Solver
- import leon.solvers.combinators.UnrollingSolver
- val dummySolFactory = new leon.solvers.SolverFactory[SMTLIBZ3Solver] {
- def getNewSolver() = new SMTLIBZ3Solver(ctx.leonContext, program)
- }
- val vericontext = VerificationContext(ctx.leonContext, newprog, dummySolFactory, reporter)
+ // TODO: note here we must reuse the created vc, instead of creating default VC
+ val solFactory = SolverFactory.uninterpreted(ctx.leonContext, newprog)
+ val vericontext = VerificationContext(ctx.leonContext, newprog, solFactory, reporter)
val defaultTactic = new DefaultTactic(vericontext)
- val vc = defaultTactic.generatePostconditions(newroot)(0)
+ val vc = defaultTactic.generatePostconditions(newroot).head
+ solveUsingLeon(ctx.leonContext, newprog, vc)
+ }
+ import leon.solvers._
+ import leon.solvers.combinators.UnrollingSolver
+ def solveUsingLeon(leonctx: LeonContext, p: Program, vc: VC) = {
+ val solFactory = SolverFactory.uninterpreted(leonctx, program)
val verifyTimeout = 5
- // val fairZ3 = new SimpleSolverAPI(
- // new TimeoutSolverFactory(SolverFactory(() =>
- // new FairZ3Solver(ctx.leonContext, newprog) with TimeoutSolver),
- // verifyTimeout * 1000))
- val smtUnrollZ3 = new UnrollingSolver(ctx.leonContext, program,
- new SMTLIBZ3Solver(ctx.leonContext, program)) with TimeoutSolver
+ val smtUnrollZ3 = new UnrollingSolver(ctx.leonContext, program, solFactory.getNewSolver()) with TimeoutSolver
smtUnrollZ3.setTimeout(verifyTimeout * 1000)
smtUnrollZ3.assertVC(vc)
smtUnrollZ3.check match {
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index c39a34581..e17548465 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -190,8 +190,7 @@ object LazyVerificationPhase {
letsBody match {
case And(args) =>
val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
- (letsCons(createAnd(instSpecs)),
- letsCons(createAnd(rest)))
+ (letsCons(createAnd(instSpecs)), letsCons(createAnd(rest)))
case _ =>
(l, Util.tru)
}
@@ -223,12 +222,11 @@ object LazyVerificationPhase {
class VCSolver(ctx: InferenceContext, p: Program, rootFd: FunDef) extends
UnfoldingTemplateSolver(ctx, p, rootFd) {
+
override def constructVC(fd: FunDef): (Expr, Expr) = {
- val (ants, post, tmpl) = createVC(fd)
+ val (ants, post, tmpl) = createVC(rootFd)
val conseq = matchToIfThenElse(createAnd(Seq(post, tmpl.getOrElse(Util.tru))))
(matchToIfThenElse(ants), conseq)
}
-
- override def verifyInvariant(newposts: Map[FunDef, Expr]) = (Some(false), Model.empty)
}
}
diff --git a/vcs-temp b/vcs-temp
deleted file mode 100644
index 26603979f..000000000
--- a/vcs-temp
+++ /dev/null
@@ -1,48 +0,0 @@
-b376 == (!ci50 && ci50 == l1.isInstanceOf[Cons0]) &&
-b388 == (r219 - r220 <= BigInt(0) && r217 == (ts53, fld42) && r219 == size23(ts53) && r220 == size23(cs17)) &&
-b382 == (ci48 && ci48 == l1.isInstanceOf[Cons0] && ci49 && l1 == Cons0(fld38, cs14) && ci49 == cs14.isInstanceOf[Nil0] && ifres24 == tp8 && cc4 == Nil0() && arg846 + BigInt(-6) == BigInt(0) && tp8 == (cc4, arg846)) &&
-b387 == (cs17 == cc7 && cc7 == Nil0()) &&
-b385 == (-ts52 + BigInt(8) < BigInt(0)) &&
-b379 == (b389 && ci52 && ci52 == l1.isInstanceOf[Cons0] && ifres25 == tp9 && cc5 == Cons0(cs16, ts50) && arg847 == Cons0(cs16, fld34) && tp9 == (cc5, arg848) && e20 == (ts50, fld35) && e20 == (fld36, ts51) && (arg848 - ts51) + BigInt(-9) == BigInt(0) && arg847 == l1 && e20 == r217 && arg849 == l1 && arg849 == Cons0(fld37, cs17) && r217 == removeLast-time10(cs17)) &&
-b383 == (b378 && ifres24 == ifres25 && b381) &&
-b386 == (l1 != cc3 && cc3 == Nil0() && res117 == tp7 && bd1 == (ts48, fld39) && bd1 == (fld40, ts49) && tp7 == (ts48, ts49) && b384 && bd1 == ifres24 && b385 && res117 == (fld41, ts52) && r218 == size23(l1)) &&
-b377 == (!ci51 && l1 == Cons0(fld33, cs15) && ci51 == cs15.isInstanceOf[Nil0]) &&
-b380 == (!ci53 && ci53 == l1.isInstanceOf[Cons0] && ifres25 == tp10 && cc6 == Nil0() && arg850 + BigInt(-6) == BigInt(0) && tp10 == (cc6, arg850)) &&
-b378 == (b376 || b377) &&
-b381 == (b379 || b380) &&
-b384 == (b382 || b383) &&
-b389 == (b387 || b388) &&
-b386
-
-
-b376 == !l1.isInstanceOf[Cons0] &&
-b388 == (size23(ts53) - size23(Nil0()) <= BigInt(0)) &&
-b382 == (l1.isInstanceOf[Cons0] && cs14.isInstanceOf[Nil0] && l1 == Cons0(fld38, cs14) && ifres24 == (Nil0(), arg846) && arg846 + BigInt(-6) == BigInt(0)) &&
-b387 == (true && true) &&
-b385 == (-ts52 + BigInt(8) < BigInt(0)) &&
-b379 == (b389 && l1.isInstanceOf[Cons0] && ifres25 == (Cons0(cs16, ts50), arg848) && e20 == (ts50, fld35) && e20 == (fld36, ts51) && (arg848 - ts51) + BigInt(-9) == BigInt(0) && Cons0(cs16, fld34) == l1 && e20 == (ts53, fld42) && l1 == Cons0(fld37, Nil0()) && (ts53, fld42) == removeLast-time10(Nil0())) &&
-b383 == (b378 && ifres24 == ifres25 && b381) &&
-b386 == (l1 != Nil0() && res117 == (ts48, ts49) && bd1 == (ts48, fld39) && bd1 == (fld40, ts49) && b384 && bd1 == ifres24 && b385 && res117 == (fld41, ts52)) &&
-b377 == (!cs15.isInstanceOf[Nil0] && l1 == Cons0(fld33, cs15)) &&
-b380 == (!l1.isInstanceOf[Cons0] && ifres25 == (Nil0(), arg850) && arg850 + BigInt(-6) == BigInt(0)) &&
-b378 == (b376 || b377) &&
-b381 == (b379 || b380) &&
-b384 == (b382 || b383) &&
-b389 == (b387 || b388) &&
-b386
-
-
-b389 == ((cs17 == Nil0()) || (size23(ts53) - size23(cs17) <= BigInt(0) && r217 == (ts53, fld42))) &&
-
-b379 == (b389 && l1.isInstanceOf[Cons0] && ifres25 == (Cons0(cs16, ts50), arg848) && e20 == (ts50, fld35) && e20 == (fld36, ts51) && (arg848 - ts51) + BigInt(-9) == BigInt(0) && Cons0(cs16, fld34) == l1 && e20 == (ts53, fld42) && l1 == Cons0(fld37, Nil0()) && (ts53, fld42) == removeLast-time10(Nil0())) &&
-
-b380 == (!l1.isInstanceOf[Cons0] && ifres25 == (Nil0(), arg850) && arg850 + BigInt(-6) == BigInt(0)) &&
-
-(l1 != Nil0() && res117 == (ts48, ts49) && bd1 == (ts48, fld39) && bd1 == (fld40, ts49) && ((l1.isInstanceOf[Cons0] && cs14.isInstanceOf[Nil0] && l1 == Cons0(fld38, cs14) && ifres24 == (Nil0(), arg846) && arg846 + BigInt(-6) == BigInt(0)) ||
-((!l1.isInstanceOf[Cons0] || (!cs15.isInstanceOf[Nil0] && l1 == Cons0(fld33, cs15))) && ifres24 == ifres25 &&
-(b379 || b380)))
-&& bd1 == ifres24 &&
-(-ts52 + BigInt(8) < BigInt(0)) && res117 == (fld41, ts52)) &&
-
-What happenned to
-???? r218 == size23(l1)) ???
--
GitLab