diff --git a/src/main/scala/leon/invariant/factories/AxiomFactory.scala b/src/main/scala/leon/invariant/factories/AxiomFactory.scala
index 907db46ab1cf1fbd4efcc19f58ae5867142575f6..ebc33562c87f6db9c7b9db7514524956eb2eb3a3 100644
--- a/src/main/scala/leon/invariant/factories/AxiomFactory.scala
+++ b/src/main/scala/leon/invariant/factories/AxiomFactory.scala
@@ -25,19 +25,19 @@ class AxiomFactory(ctx : InferenceContext) {
(callee.isMonotonic || callee.isDistributive)
}
- def unaryAxiom(call: Call) : (Expr,Expr) = {
+ def unaryAxiom(call: Call): (Expr, Expr) = {
val callee = call.fi.tfd.fd
val tfd = call.fi.tfd
- if(callee.isCommutative) {
+ if (callee.isCommutative) {
//note: commutativity is defined only for binary operations
val Seq(a1, a2) = call.fi.args
- val newret = TVarFactory.createTemp("cm").toVariable
- val newfi = FunctionInvocation(tfd,Seq(a2,a1))
- val newcall = Call(newret,newfi)
+ val newret = TVarFactory.createTempDefault("cm").toVariable
+ val newfi = FunctionInvocation(tfd, Seq(a2, a1))
+ val newcall = Call(newret, newfi)
(tru, And(newcall.toExpr, Equals(newret, call.retexpr)))
} else
- throw new IllegalStateException("Call does not have unary axiom: "+call)
+ throw new IllegalStateException("Call does not have unary axiom: " + call)
}
def binaryAxiom(call1: Call, call2: Call): Seq[(Expr,Expr)] = {
@@ -81,7 +81,7 @@ class AxiomFactory(ctx : InferenceContext) {
val r1 = call1.retexpr
val r2 = call2.retexpr
- val dret2 = TVarFactory.createTemp("dt", IntegerType).toVariable
+ val dret2 = TVarFactory.createTempDefault("dt", IntegerType).toVariable
val dcall2 = Call(dret2, FunctionInvocation(tfd,Seq(Plus(a1,a2),b2)))
(LessEquals(b1,b2), And(LessEquals(Plus(r1,r2),dret2), dcall2.toExpr))
}
diff --git a/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala b/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
index dbcdc4c5e1a2de62fb5a1c1e81ebe17b4449a584..fcf786d2845ea699fa541c131a81eaabbaf5649f 100644
--- a/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
+++ b/src/main/scala/leon/invariant/factories/TemplateInstantiator.scala
@@ -20,18 +20,13 @@ object TemplateInstantiator {
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 = getTemplateVars(template)
val tempVarMap: Map[Expr, Expr] = tempvars.map((v) => {
(v, model(v.id))
}).toMap
-
val instTemplate = instantiate(template, tempVarMap, prettyInv)
- //now unflatten it
- val comprTemp = ExpressionTransformer.unFlatten(instTemplate, freevars)
+ val comprTemp = ExpressionTransformer.unFlatten(instTemplate)
(fd, comprTemp)
})
invs
diff --git a/src/main/scala/leon/invariant/structure/Formula.scala b/src/main/scala/leon/invariant/structure/Formula.scala
index c17711e102877861010359256ff902ad7d51d70b..83440a9fc9fd6ac54d54ceab6070e4110643ad02 100644
--- a/src/main/scala/leon/invariant/structure/Formula.scala
+++ b/src/main/scala/leon/invariant/structure/Formula.scala
@@ -18,12 +18,18 @@ import invariant.util._
import leon.solvers.Model
import Util._
import PredicateUtil._
+import TVarFactory._
/**
* Data associated with a call
*/
class CallData(val guard : Variable, val parents: List[FunDef])
+object Formula {
+ // a context for creating blockers
+ val blockContext = newContext
+}
+
/**
* Representation of an expression as a set of implications.
* 'initexpr' is required to be in negation normal form and And/Ors have been pulled up
@@ -31,6 +37,8 @@ class CallData(val guard : Variable, val parents: List[FunDef])
*/
class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
+ import Formula._
+
val fls = BooleanLiteral(false)
val tru = BooleanLiteral(true)
val useImplies = false
@@ -90,7 +98,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
case And(atms) => atms
case _ => Seq(arg)
}
- val g = TVarFactory.createTemp("b", BooleanType).toVariable
+ val g = createTemp("b", BooleanType, blockContext).toVariable
newDisjGuards :+= g
//println("atoms: "+atoms)
val ctrs = getCtrsFromExprs(g, atoms)
@@ -99,7 +107,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
}
}
//create a temporary for Or
- val gor = TVarFactory.createTemp("b", BooleanType).toVariable
+ val gor = createTemp("b", BooleanType, blockContext).toVariable
val newor = createOr(newargs)
conjuncts += (gor -> newor)
gor
@@ -109,7 +117,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
arg
} else {
//if the expression has template variables then we separate it using guards
- val g = TVarFactory.createTemp("b", BooleanType).toVariable
+ val g = createTemp("b", BooleanType, blockContext).toVariable
newDisjGuards :+= g
val ctrs = getCtrsFromExprs(g, Seq(arg))
disjuncts += (g -> ctrs)
@@ -133,7 +141,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext) {
case And(atms) => atms
case _ => Seq(f1)
}
- val g = TVarFactory.createTemp("b", BooleanType).toVariable
+ val g = createTemp("b", BooleanType, blockContext).toVariable
val ctrs = getCtrsFromExprs(g, atoms)
newDisjGuards :+= g
disjuncts += (g -> ctrs)
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index d4d72a507b3f204170cee0e99b9522dc7e1ffc66..31f9e8b470adfd0ad6df2e86f658ebc843d32f9c 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -42,10 +42,10 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val debugAxioms = false
val verifyInvariant = false
val debugReducedFormula = false
- val trackUnpackedVCCTime = false
+ val trackUnpackedVCCTime = true
//print flags
- val verbose = false
+ val verbose = true
val printCounterExample = false
val printPathToConsole = false
val dumpPathAsSMTLIB = false
@@ -60,7 +60,6 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
private val startFromEarlierModel = true
private val disableCegis = true
private val useIncrementalSolvingForVCs = true
- private val useCVCToCheckVCs = false
private val usePortfolio = false // portfolio has a bug in incremental solving
//this is private mutable state used by initialized during every call to 'solve' and used by 'solveUNSAT'
@@ -78,15 +77,14 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
ctrTracker.getVC(fd).splitParamPart
}
- def getSolver =
- if(this.usePortfolio) {
- new PortfolioSolver(leonctx, Seq(new SMTLIBCVC4Solver(leonctx, program),
- new SMTLIBZ3Solver(leonctx, program))) with TimeoutSolver
- }
- else if (this.useCVCToCheckVCs)
- new SMTLIBCVC4Solver(leonctx, program) with TimeoutSolver
- else
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver
+ val solverFactory =
+ if (this.usePortfolio) {
+ if (this.useIncrementalSolvingForVCs)
+ throw new IllegalArgumentException("Cannot perform incremental solving with portfolio solvers!")
+ SolverFactory(() => new PortfolioSolver(leonctx, Seq(new SMTLIBCVC4Solver(leonctx, program),
+ new SMTLIBZ3Solver(leonctx, program))) with TimeoutSolver)
+ } else
+ SolverFactory.uninterpreted(leonctx, program)
def initVCSolvers = {
funcVCs.keys.foreach { fd =>
@@ -100,7 +98,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
throw new IllegalStateException("Non-param Part has both integers and reals: " + rest)
if (!ctx.abort) { // this is required to ensure that solvers are not created after interrupts
- val vcSolver = getSolver
+ val vcSolver = solverFactory.getNewSolver()
vcSolver.assertCnstr(rest)
if (debugIncrementalVC) {
@@ -393,7 +391,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val tempVarMap: Map[Expr, Expr] = inModel.map((elem) => (elem._1.toVariable, elem._2)).toMap
val solver =
if (this.useIncrementalSolvingForVCs) vcSolvers(fd)
- else getSolver
+ else solverFactory.getNewSolver()
val instExpr = if (this.useIncrementalSolvingForVCs) {
val instParamPart = instantiateTemplate(this.paramParts(fd), tempVarMap)
And(instParamPart, disableCounterExs)
@@ -451,7 +449,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
Stats.updateCounterStats(atomNum(upVCinst), "UP-VC-size", "disjuncts")
t1 = System.currentTimeMillis()
- val (res2, _) = SimpleSolverAPI(SolverFactory(() => getSolver)).solveSAT(upVCinst)
+ val (res2, _) = SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())).solveSAT(upVCinst)
val unpackedTime = System.currentTimeMillis() - t1
if (res != res2) {
throw new IllegalStateException("Unpacked VC produces different result: " + upVCinst)
diff --git a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
index 6886b98bd77fabf7c13ce7cdcd88c1361245b49e..83ed0a86b86675b41a55b60b30783f79645bcfb5 100644
--- a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
+++ b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
@@ -12,6 +12,7 @@ import purescala.ScalaPrinter
import leon.invariant.factories.TemplateIdFactory
import PredicateUtil._
import Util._
+import TVarFactory._
/**
* A collection of transformation on expressions and some utility methods.
@@ -26,6 +27,15 @@ object ExpressionTransformer {
val fls = BooleanLiteral(false)
val bone = BigInt(1)
+ // identifier for temporaries that are generated during flattening
+ val flatContext = newContext
+ // temporaries generated during conversion of field selects to ADT constructions
+ val fieldSelContext = newContext
+ // conversion of other language constructs
+ val langContext = newContext
+
+ def createFlatTemp(name: String, tpe: TypeTree = Untyped) = createTemp(name, tpe, flatContext)
+
/**
* This function conjoins the conjuncts created by 'transfomer' within the clauses containing Expr.
* This is meant to be used by operations that may flatten subexpression using existential quantifiers.
@@ -77,7 +87,7 @@ object ExpressionTransformer {
e match {
// Handle asserts here. Return flattened body as the result
case as @ Assert(pred, _, body) => {
- val freshvar = TVarFactory.createTemp("asrtres", e.getType).toVariable
+ val freshvar = createFlatTemp("asrtres", e.getType).toVariable
val newexpr = Equals(freshvar, body)
val resset = transform(newexpr, insideFunction)
(freshvar, resset._2 + resset._1)
@@ -85,7 +95,7 @@ object ExpressionTransformer {
//handles division by constant
case Division(lhs, rhs @ InfiniteIntegerLiteral(v)) => {
//this models floor and not integer division
- val quo = TVarFactory.createTemp("q", IntegerType).toVariable
+ val quo = createTemp("q", IntegerType, langContext).toVariable
var possibs = Seq[Expr]()
for (i <- v - 1 to 0 by -1) {
if (i == 0) possibs :+= Equals(lhs, Times(rhs, quo))
@@ -100,8 +110,8 @@ object ExpressionTransformer {
//handles division by variables
case Division(lhs, rhs) => {
//this models floor and not integer division
- val quo = TVarFactory.createTemp("q", IntegerType).toVariable
- val rem = TVarFactory.createTemp("r", IntegerType).toVariable
+ val quo = createTemp("q", IntegerType, langContext).toVariable
+ val rem = createTemp("r", IntegerType, langContext).toVariable
val mult = multop(quo, rhs)
val divsem = Equals(lhs, Plus(mult, rem))
//TODO: here, we have to use |rhs|
@@ -111,7 +121,7 @@ object ExpressionTransformer {
}
case err @ Error(_, msg) => {
//replace this by a fresh variable of the error type
- (TVarFactory.createTemp("err", err.getType).toVariable, Set[Expr]())
+ (createTemp("err", err.getType, langContext).toVariable, Set[Expr]())
}
case Equals(lhs, rhs) => {
val (nexp1, ncjs1) = transform(lhs, true)
@@ -119,7 +129,7 @@ object ExpressionTransformer {
(Equals(nexp1, nexp2), ncjs1 ++ ncjs2)
}
case IfExpr(cond, thn, elze) => {
- val freshvar = TVarFactory.createTemp("ifres", e.getType).toVariable
+ val freshvar = createTemp("ifres", e.getType, langContext).toVariable
val newexpr = Or(And(cond, Equals(freshvar, thn)), And(Not(cond), Equals(freshvar, elze)))
val resset = transform(newexpr, insideFunction)
(freshvar, resset._2 + resset._1)
@@ -150,7 +160,7 @@ object ExpressionTransformer {
val (resvalue2, cjs) = resvalue match {
case t: Terminal => (t, Seq())
case _ => {
- val freshres = TVarFactory.createTemp("tres", resvalue.getType).toVariable
+ val freshres = createTemp("tres", resvalue.getType, langContext).toVariable
(freshres, Seq(Equals(freshres, resvalue)))
}
}
@@ -195,86 +205,69 @@ object ExpressionTransformer {
*/
def flattenFunc(e: Expr, insideFunction: Boolean): (Expr, Set[Expr]) = {
e match {
- case fi @ FunctionInvocation(fd, args) => {
- //now also flatten the args. The following is slightly tricky
+ case fi @ FunctionInvocation(fd, args) =>
val (newargs, newConjuncts) = flattenArgs(args, true)
- //create a new equality in UIFs
val newfi = FunctionInvocation(fd, newargs)
- //create a new variable to represent the function
- val freshResVar = Variable(TVarFactory.createTemp("r", fi.getType))
+ val freshResVar = Variable(createFlatTemp("r", fi.getType))
val res = (freshResVar, newConjuncts + Equals(freshResVar, newfi))
res
- }
- case inst @ IsInstanceOf(e1, cd) => {
+
+ case inst @ IsInstanceOf(e1, cd) =>
//replace e by a variable
val (newargs, newcjs) = flattenArgs(Seq(e1), true)
var newConjuncts = newcjs
-
val freshArg = newargs(0)
val newInst = IsInstanceOf(freshArg, cd)
- val freshResVar = Variable(TVarFactory.createTemp("ci", inst.getType))
+ val freshResVar = Variable(createFlatTemp("ci", inst.getType))
newConjuncts += Equals(freshResVar, newInst)
(freshResVar, newConjuncts)
- }
- case cs @ CaseClassSelector(cd, e1, sel) => {
+
+ case cs @ CaseClassSelector(cd, e1, sel) =>
val (newargs, newcjs) = flattenArgs(Seq(e1), true)
var newConjuncts = newcjs
-
val freshArg = newargs(0)
val newCS = CaseClassSelector(cd, freshArg, sel)
- val freshResVar = Variable(TVarFactory.createTemp("cs", cs.getType))
+ val freshResVar = Variable(createFlatTemp("cs", cs.getType))
newConjuncts += Equals(freshResVar, newCS)
-
(freshResVar, newConjuncts)
- }
- case ts @ TupleSelect(e1, index) => {
+
+ case ts @ TupleSelect(e1, index) =>
val (newargs, newcjs) = flattenArgs(Seq(e1), true)
var newConjuncts = newcjs
-
val freshArg = newargs(0)
val newTS = TupleSelect(freshArg, index)
- val freshResVar = Variable(TVarFactory.createTemp("ts", ts.getType))
+ val freshResVar = Variable(createFlatTemp("ts", ts.getType))
newConjuncts += Equals(freshResVar, newTS)
-
(freshResVar, newConjuncts)
- }
- case cc @ CaseClass(cd, args) => {
+ case cc @ CaseClass(cd, args) =>
val (newargs, newcjs) = flattenArgs(args, true)
var newConjuncts = newcjs
-
val newCC = CaseClass(cd, newargs)
- val freshResVar = Variable(TVarFactory.createTemp("cc", cc.getType))
+ val freshResVar = Variable(createFlatTemp("cc", cc.getType))
newConjuncts += Equals(freshResVar, newCC)
-
(freshResVar, newConjuncts)
- }
+
case tp @ Tuple(args) => {
val (newargs, newcjs) = flattenArgs(args, true)
var newConjuncts = newcjs
-
val newTP = Tuple(newargs)
- val freshResVar = Variable(TVarFactory.createTemp("tp", tp.getType))
- // if(freshResVar.id.toString == "tp6"){
- // println("Creating temporary tp6 type: "+tp.getType+" expr: "+tp)
- // throw new IllegalStateException("")
- // }
+ val freshResVar = Variable(createFlatTemp("tp", tp.getType))
newConjuncts += Equals(freshResVar, newTP)
-
(freshResVar, newConjuncts)
}
case SetUnion(_, _) | ElementOfSet(_, _) | SubsetOf(_, _) =>
val Operator(args, op) = e
val (Seq(a1, a2), newcjs) = flattenArgs(args, true)
val newexpr = op(Seq(a1, a2))
- val freshResVar = Variable(TVarFactory.createTemp("set", e.getType))
+ val freshResVar = Variable(createFlatTemp("set", e.getType))
(freshResVar, newcjs + Equals(freshResVar, newexpr))
case fs @ FiniteSet(es, typ) =>
val args = es.toSeq
val (nargs, newcjs) = flattenArgs(args, true)
val newexpr = FiniteSet(nargs.toSet, typ)
- val freshResVar = Variable(TVarFactory.createTemp("fset", fs.getType))
+ val freshResVar = Variable(createFlatTemp("fset", fs.getType))
(freshResVar, newcjs + Equals(freshResVar, newexpr))
case _ => conjoinWithinClause(e, flattenFunc, insideFunction)
@@ -286,25 +279,20 @@ object ExpressionTransformer {
val newargs = args.map {
case v: Variable => v
case r: ResultVariable => r
- case arg => {
+ case arg =>
val (nexpr, ncjs) = flattenFunc(arg, insideFunction)
-
newConjuncts ++= ncjs
-
nexpr match {
case v: Variable => v
case r: ResultVariable => r
- case _ => {
- val freshArgVar = Variable(TVarFactory.createTemp("arg", arg.getType))
+ case _ =>
+ val freshArgVar = Variable(createFlatTemp("arg", arg.getType))
newConjuncts += Equals(freshArgVar, nexpr)
freshArgVar
- }
}
- }
}
(newargs, newConjuncts)
}
-
val (nexp, ncjs) = flattenFunc(inExpr, false)
if (ncjs.nonEmpty) {
createAnd(nexp +: ncjs.toSeq)
@@ -339,10 +327,6 @@ object ExpressionTransformer {
*/
def TransformNot(expr: Expr, retainNEQ: Boolean = false): Expr = { // retainIff : Boolean = false
def nnf(inExpr: Expr): Expr = {
-// if(inExpr.getType == Untyped){
-// testHelp(inExpr)
-// println(s"Warning: $inExpr is untyped")
-// }
if (inExpr.getType != BooleanType) inExpr
else {
inExpr match {
@@ -440,7 +424,7 @@ object ExpressionTransformer {
if (fld.id == ccfld) r
else {
//create a dummy identifier there
- TVarFactory.createDummy(fld.getType).toVariable
+ createTemp("fld", fld.getType, fieldSelContext).toVariable
}
})
Equals(ccvar, CaseClass(cd, args))
@@ -458,7 +442,7 @@ object ExpressionTransformer {
if (i == index) r
else {
//create a dummy identifier there (note that here we have to use i-1)
- TVarFactory.createDummy(tupleType.bases(i - 1)).toVariable
+ createTemp("fld", tupleType.bases(i - 1), fieldSelContext).toVariable
}
})
Equals(tpvar, Tuple(args))
@@ -483,24 +467,23 @@ object ExpressionTransformer {
}
/**
- * This is the inverse operation of flattening, this is mostly
- * used to produce a readable formula.
- * Freevars is a set of identifiers that are program variables
- * This assumes that temporary identifiers (which are not freevars) are not reused across clauses.
+ * This is the inverse operation of flattening.
+ * This is used to produce a readable formula or more efficiently
+ * solvable formulas.
*/
- def unFlatten(ine: Expr, freevars: Set[Identifier]): Expr = {
- var tempMap = Map[Expr, Expr]()
- val newinst = simplePostTransform {
- case e @ Equals(v @ Variable(id), rhs @ _) if !freevars.contains(id) =>
- if (tempMap.contains(v)) e
+ def unFlatten(ine: Expr): Expr = {
+ var idMap = Map[Identifier, Expr]()
+ val newe = simplePostTransform {
+ case e @ Equals(Variable(id), rhs @ _) if isTemp(id, flatContext) =>
+ if (idMap.contains(id)) e
else {
- tempMap += (v -> rhs)
+ idMap += (id -> rhs)
tru
}
case e => e
}(ine)
- val closure = (e: Expr) => replace(tempMap, e)
- fix(closure)(newinst)
+ val closure = (e: Expr) => replaceFromIDs(idMap, e)
+ fix(closure)(newe)
}
/**
@@ -532,7 +515,6 @@ object ExpressionTransformer {
* TODO: fix this
*/
def isSubExpr(key: Expr, expr: Expr): Boolean = {
-
var found = false
simplePostTransform {
case e if (e == key) =>
@@ -546,7 +528,6 @@ object ExpressionTransformer {
* Some simplification rules (keep adding more and more rules)
*/
def simplify(expr: Expr): Expr = {
-
//Note: some simplification are already performed by the class constructors (see Tree.scala)
simplePostTransform {
case Equals(lhs, rhs) if (lhs == rhs) => tru
@@ -600,8 +581,6 @@ object ExpressionTransformer {
else args.forall(arg => uniOP(arg, 2))
}
case t: Terminal => true
- /*case u @ UnaryOperator(e1, op) => uniOP(e1, seen)
- case b @ BinaryOperator(e1, e2, op) => uniOP(e1, seen) && uniOP(e2, seen)*/
case n @ Operator(args, op) => args.forall(arg => uniOP(arg, seen))
}
diff --git a/src/main/scala/leon/invariant/util/LetTupleSimplification.scala b/src/main/scala/leon/invariant/util/LetTupleSimplification.scala
index 7052328e10adc9faa832c2907bca6832924b3993..641f6045e004df79be1a30fccf24b385c490a384 100644
--- a/src/main/scala/leon/invariant/util/LetTupleSimplification.scala
+++ b/src/main/scala/leon/invariant/util/LetTupleSimplification.scala
@@ -12,10 +12,10 @@ import java.io._
import purescala.ScalaPrinter
import leon.utils._
import PredicateUtil._
-
import invariant.structure.Call
import invariant.structure.FunctionUtils._
import leon.transformations.InstUtil._
+import TVarFactory._
/**
* A collection of transformation on expressions and some utility methods.
@@ -29,6 +29,8 @@ object LetTupleSimplification {
val tru = BooleanLiteral(true)
val fls = BooleanLiteral(false)
val bone = BigInt(1)
+ // fresh ids created during simplification
+ val simpContext = newContext
def letSanityChecks(ine: Expr) = {
simplePostTransform(_ match {
@@ -62,7 +64,7 @@ object LetTupleSimplification {
case TupleType(argTypes) =>
var freshBinders = Set[Identifier]()
def freshBinder(typ: TypeTree) = {
- val freshid = TVarFactory.createTemp(binderId.name, typ)
+ val freshid = createTemp(binderId.name, typ, simpContext)
freshBinders += freshid
freshid.toVariable
}
@@ -235,7 +237,7 @@ object LetTupleSimplification {
//here we can use 'b' in 'body'
Let(id, v, body(b))
case _ =>
- val mt = TVarFactory.createTemp("mt", value.getType)
+ val mt = createTemp("mt", value.getType, simpContext)
Let(mt, value, body(mt.toVariable))
}
}
diff --git a/src/main/scala/leon/invariant/util/SolverUtil.scala b/src/main/scala/leon/invariant/util/SolverUtil.scala
index 466ec1d2def3831b42c1f0b4bc6eaad3351ef716..6b4641e039887bd734fee18e0a33e37f83221b23 100644
--- a/src/main/scala/leon/invariant/util/SolverUtil.scala
+++ b/src/main/scala/leon/invariant/util/SolverUtil.scala
@@ -70,7 +70,7 @@ object SolverUtil {
val solver = new ExtendedUFSolver(ctx, prog)
val newe = simplePostTransform {
case e@(And(_) | Or(_)) => {
- val v = TVarFactory.createTemp("a", BooleanType).toVariable
+ val v = TVarFactory.createTempDefault("a", BooleanType).toVariable
newEqs += (v -> e)
val newe = Equals(v, e)
@@ -106,8 +106,7 @@ object SolverUtil {
solver.free
//cores
- ExpressionTransformer.unFlatten(cores,
- variablesOf(ine).filterNot(TVarFactory.isTemporary _))
+ ExpressionTransformer.unFlatten(cores)
}
//tests if the solver uses nlsat
diff --git a/src/main/scala/leon/invariant/util/TVarFactory.scala b/src/main/scala/leon/invariant/util/TVarFactory.scala
index 6743e802b27ef44b1b966555d6965130373b5f8b..7fdebb008ec6529914c4f40aeb6451ed22f9aaef 100644
--- a/src/main/scala/leon/invariant/util/TVarFactory.scala
+++ b/src/main/scala/leon/invariant/util/TVarFactory.scala
@@ -3,26 +3,33 @@ package invariant.util
import purescala.Common._
import purescala.Types._
-import scala.collection.mutable.{ Set => MutableSet}
+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]()
+ type Context = Int
+ val temporaries = MutableMap[Context, MutableSet[Identifier]]()
+ private var context: Context = 0
- def createTemp(name: String, tpe: TypeTree = Untyped): Identifier = {
+ def newContext = {
+ context += 1
+ temporaries += (context -> MutableSet())
+ context
+ }
+ val defaultContext = newContext
+
+ def createTemp(name: String, tpe: TypeTree = Untyped, context: Context): Identifier = {
val freshid = FreshIdentifier(name, tpe, true)
- temporaries.add(freshid)
+ temporaries(context) += freshid
freshid
}
- def createDummy(tpe: TypeTree): Identifier = {
- val freshid = FreshIdentifier("dy", tpe, true)
- dummyIds.add(freshid)
+ def createTempDefault(name: String, tpe: TypeTree = Untyped): Identifier = {
+ val freshid = FreshIdentifier(name, tpe, true)
+ temporaries(defaultContext) += freshid
freshid
}
- def isTemporary(id: Identifier): Boolean = temporaries.contains(id)
- def isDummy(id: Identifier): Boolean = dummyIds.contains(id)
+ def isTemp(id: Identifier, context: Context): Boolean =
+ temporaries.contains(context) && temporaries(context)(id)
}
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 929ee38e2f5c9d3712f48a146d730f0f62f65fbd..439dc5f8b7ed81492581df370e41554276e14d0b 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -51,7 +51,7 @@ object LazinessEliminationPhase extends TransformationPhase {
val dumpProgWOInstSpecs = true
val dumpInstrumentedProgram = true
val debugSolvers = false
- val skipStateVerification = false
+ val skipStateVerification = true
val skipResourceVerification = false
val name = "Laziness Elimination Phase"
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index 41375996956a49d5f3d61fe74add146d04266440..3f1a8ce00c9830eae59eb171e1d6096c61018091 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -134,7 +134,7 @@ object LazyVerificationPhase {
val funsToCheck = p.definedFunctions.filter(shouldGenerateVC)
if (useOrb) {
// create an inference context
- val inferOpts = Main.processOptions(Seq("--disableInfer", "--assumepreInf", "--minbounds"))
+ val inferOpts = Main.processOptions(Seq("--disableInfer", "--assumepreInf", "--minbounds","--solvers=smt-cvc4"))
val ctxForInf = LeonContext(checkCtx.reporter, checkCtx.interruptManager,
inferOpts.options ++ checkCtx.options)
val inferctx = new InferenceContext(p, ctxForInf)
diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
index 85c898d81548800735be9cdf6b1b718b1e052a29..ebde5cc5d0e1d93638b0e4698306196827f8eaa5 100644
--- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
+++ b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
@@ -19,8 +19,7 @@ class OrbRegressionSuite extends LeonRegressionSuite {
}
private def testInference(f: File, bound: Option[Int] = None) {
-
- val ctx = createLeonContext("--inferInv")
+ val ctx = createLeonContext("--inferInv","--solvers=smt-z3")
val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)