diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index f7744e058e3dff28f22afd580f53749f0f485165..78fc476dd8ab9f3b8bc70010a40e021e2424f367 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -19,13 +19,14 @@ object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
val optCegis = LeonFlagOptionDef("cegis", "use cegis instead of farkas", false)
val optStatsSuffix = LeonStringOptionDef("stats-suffix", "the suffix of the statistics file", "", "s")
val optVCTimeout = LeonLongOptionDef("vcTimeout", "Timeout after T seconds when trying to prove a verification condition", 20, "s")
+ val optNLTimeout = LeonLongOptionDef("nlTimeout", "Timeout after T seconds when trying to solve nonlinear constraints", 20, "s")
val optDisableInfer = LeonFlagOptionDef("disableInfer", "Disable automatic inference of auxiliary invariants", false)
val optAssumePre = LeonFlagOptionDef("assumepreInf", "Assume preconditions of callees during unrolling", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optFunctionUnroll, optWithMult, optUseReals,
optMinBounds, optInferTemp, optCegis, optStatsSuffix, optVCTimeout,
- optDisableInfer, optAssumePre)
+ optNLTimeout, optDisableInfer, optAssumePre)
def apply(ctx: LeonContext, program: Program): InferenceReport = {
val inferctx = new InferenceContext(program, ctx)
diff --git a/src/main/scala/leon/invariant/engine/InferenceContext.scala b/src/main/scala/leon/invariant/engine/InferenceContext.scala
index d94c46fd637ae23561c848c3a182aa0420767d56..966a79dc691007a71c2bf1ec0e28331f9d1a1332 100644
--- a/src/main/scala/leon/invariant/engine/InferenceContext.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceContext.scala
@@ -37,6 +37,7 @@ class InferenceContext(val initProgram: Program, val leonContext: LeonContext) {
// the following options have default values
val vcTimeout = leonContext.findOption(optVCTimeout).getOrElse(15L) // in secs
+ val nlTimeout = leonContext.findOption(optNLTimeout).getOrElse(15L)
val totalTimeout = leonContext.findOption(SharedOptions.optTimeout) // in secs
val functionsToInfer = leonContext.findOption(SharedOptions.optFunctions)
val reporter = leonContext.reporter
diff --git a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index a4e20f61a7424ee59724b8cf4374cecbcaf84f9f..05067d675264b854ff7f4f279187988696b9e348 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -37,7 +37,7 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
val leonctx = ctx.leonContext
val reporter = ctx.reporter
- val timeout = ctx.vcTimeout // Note: we are using vcTimeout here as well
+ val timeout = ctx.nlTimeout // Note: we are using vcTimeout here as well
/**
* This procedure produces a set of constraints that need to be satisfiable for the
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 7f60be3ae639a29a051ec501e13a4d96e26b3174..f4e63e0c095bc6fd99a3cb12023bf28a4dcae510 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -45,7 +45,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
val trackUnpackedVCCTime = false
//print flags
- val verbose = false
+ val verbose = true
val printCounterExample = false
val printPathToConsole = false
val dumpPathAsSMTLIB = false
@@ -61,10 +61,10 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
private val disableCegis = true
private val useIncrementalSolvingForVCs = true
private val useCVCToCheckVCs = true
+ 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'
protected var funcVCs = Map[FunDef, Expr]()
- //TODO: can incremental solving be trusted ? There were problems earlier.
protected var vcSolvers = Map[FunDef, Solver with TimeoutSolver]()
protected var paramParts = Map[FunDef, Expr]()
protected var simpleParts = Map[FunDef, Expr]()
@@ -78,6 +78,16 @@ 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
+
def initVCSolvers = {
funcVCs.keys.foreach { fd =>
val (paramPart, rest) = if (ctx.usereals) {
@@ -90,11 +100,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 =
- if (this.useCVCToCheckVCs)
- new SMTLIBCVC4Solver(leonctx, program) with TimeoutSolver
- else
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver
+ val vcSolver = getSolver
vcSolver.assertCnstr(rest)
if (debugIncrementalVC) {
@@ -387,7 +393,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 new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver
+ else getSolver
val instExpr = if (this.useIncrementalSolvingForVCs) {
val instParamPart = instantiateTemplate(this.paramParts(fd), tempVarMap)
And(instParamPart, disableCounterExs)
@@ -445,7 +451,7 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
Stats.updateCounterStats(atomNum(upVCinst), "UP-VC-size", "disjuncts")
t1 = System.currentTimeMillis()
- val (res2, _) = SimpleSolverAPI(SolverFactory(() => new SMTLIBZ3Solver(leonctx, program))).solveSAT(upVCinst)
+ val (res2, _) = SimpleSolverAPI(SolverFactory(() => getSolver)).solveSAT(upVCinst)
val unpackedTime = System.currentTimeMillis() - t1
if (res != res2) {
throw new IllegalStateException("Unpacked VC produces different result: " + upVCinst)
@@ -495,42 +501,50 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
}
/**
- * Evaluator for a predicate that is a simple equality/inequality between two variables
+ * Evaluator for a predicate that is a simple equality/inequality between two variables.
+ * Some expressions may not be evaluatable, so we return none in those cases.
*/
- protected def predEval(model: Model): (Expr => Boolean) = {
+ protected def predEval(model: Model): (Expr => Option[Boolean]) = {
if (ctx.usereals) realEval(model)
else intEval(model)
}
- protected def intEval(model: Model): (Expr => Boolean) = {
+ protected def intEval(model: Model): (Expr => Option[Boolean]) = {
def modelVal(id: Identifier): BigInt = {
val InfiniteIntegerLiteral(v) = model(id)
v
}
- def eval: (Expr => Boolean) = {
- case And(args) => args.forall(eval)
- // case Iff(Variable(id1), Variable(id2)) => model(id1) == model(id2)
- case Equals(Variable(id1), Variable(id2)) => model(id1) == model(id2) //note: ADTs can also be compared for equality
- case LessEquals(Variable(id1), Variable(id2)) => modelVal(id1) <= modelVal(id2)
- case GreaterEquals(Variable(id1), Variable(id2)) => modelVal(id1) >= modelVal(id2)
- case GreaterThan(Variable(id1), Variable(id2)) => modelVal(id1) > modelVal(id2)
- case LessThan(Variable(id1), Variable(id2)) => modelVal(id1) < modelVal(id2)
+ def eval: (Expr => Option[Boolean]) = {
+ case And(args) =>
+ val argres = args.map(eval)
+ if(argres.exists(!_.isDefined)) None
+ else
+ Some(argres.forall(_.get))
+ case Equals(Variable(id1), Variable(id2)) =>
+ if(model.isDefinedAt(id1) &&
+ model.isDefinedAt(id2))
+ Some(model(id1) == model(id2)) //note: ADTs can also be compared for equality
+ else None
+ case LessEquals(Variable(id1), Variable(id2)) => Some(modelVal(id1) <= modelVal(id2))
+ case GreaterEquals(Variable(id1), Variable(id2)) => Some(modelVal(id1) >= modelVal(id2))
+ case GreaterThan(Variable(id1), Variable(id2)) => Some(modelVal(id1) > modelVal(id2))
+ case LessThan(Variable(id1), Variable(id2)) => Some(modelVal(id1) < modelVal(id2))
case e => throw new IllegalStateException("Predicate not handled: " + e)
}
eval
}
- protected def realEval(model: Model): (Expr => Boolean) = {
+ protected def realEval(model: Model): (Expr => Option[Boolean]) = {
def modelVal(id: Identifier): FractionalLiteral = {
//println("Identifier: "+id)
model(id).asInstanceOf[FractionalLiteral]
}
{
- case Equals(Variable(id1), Variable(id2)) => model(id1) == model(id2) //note: ADTs can also be compared for equality
+ case Equals(Variable(id1), Variable(id2)) => Some(model(id1) == model(id2)) //note: ADTs can also be compared for equality
case e@Operator(Seq(Variable(id1), Variable(id2)), op) if (e.isInstanceOf[LessThan]
|| e.isInstanceOf[LessEquals] || e.isInstanceOf[GreaterThan]
|| e.isInstanceOf[GreaterEquals]) => {
- evaluateRealPredicate(op(Seq(modelVal(id1), modelVal(id2))))
+ Some(evaluateRealPredicate(op(Seq(modelVal(id1), modelVal(id2)))))
}
case e => throw new IllegalStateException("Predicate not handled: " + e)
}
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
index d67955ff9efd38dd9c5c70b0684b04b5cda1661b..4fc681eb284daf192c3477b11f24078888fba9b4 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala
@@ -13,9 +13,9 @@ import invariant.structure._
import Util._
import PredicateUtil._
-class NLTemplateSolverWithMult(ctx : InferenceContext, program: Program, rootFun: FunDef,
- ctrTracker: ConstraintTracker, minimizer: Option[(Expr, Model) => Model])
- extends NLTemplateSolver(ctx, program, rootFun, ctrTracker, minimizer) {
+class NLTemplateSolverWithMult(ctx: InferenceContext, program: Program, rootFun: FunDef,
+ ctrTracker: ConstraintTracker, minimizer: Option[(Expr, Model) => Model])
+ extends NLTemplateSolver(ctx, program, rootFun, ctrTracker, minimizer) {
val axiomFactory = new AxiomFactory(ctx)
@@ -25,47 +25,47 @@ class NLTemplateSolverWithMult(ctx : InferenceContext, program: Program, rootFun
nlvc
}
- override def splitVC(fd: FunDef) : (Expr,Expr) = {
+ override def splitVC(fd: FunDef): (Expr, Expr) = {
val (paramPart, rest) = ctrTracker.getVC(fd).splitParamPart
- (multToTimes(paramPart),multToTimes(rest))
+ (multToTimes(paramPart), multToTimes(rest))
}
- override def axiomsForTheory(formula : Formula, calls: Set[Call], model: Model) : Seq[Constraint] = {
+ override def axiomsForTheory(formula: Formula, calls: Set[Call], model: Model): Seq[Constraint] = {
//in the sequel we instantiate axioms for multiplication
val inst1 = unaryMultAxioms(formula, calls, predEval(model))
- val inst2 = binaryMultAxioms(formula,calls, predEval(model))
+ val inst2 = binaryMultAxioms(formula, calls, predEval(model))
val multCtrs = (inst1 ++ inst2).flatMap {
case And(args) => args.map(ConstraintUtil.createConstriant _)
- case e => Seq(ConstraintUtil.createConstriant(e))
+ case e => Seq(ConstraintUtil.createConstriant(e))
}
Stats.updateCounterStats(multCtrs.size, "MultAxiomBlowup", "disjuncts")
- ctx.reporter.info("Number of multiplication induced predicates: "+multCtrs.size)
+ ctx.reporter.info("Number of multiplication induced predicates: " + multCtrs.size)
multCtrs
}
- def chooseSATPredicate(expr: Expr, predEval: (Expr => Boolean)): Expr = {
- val norme = ExpressionTransformer.normalizeExpr(expr,ctx.multOp)
+ def chooseSATPredicate(expr: Expr, predEval: (Expr => Option[Boolean])): Expr = {
+ val norme = ExpressionTransformer.normalizeExpr(expr, ctx.multOp)
val preds = norme match {
- case Or(args) => args
+ case Or(args) => args
case Operator(_, _) => Seq(norme)
- case _ => throw new IllegalStateException("Not(ant) is not in expected format: " + norme)
+ case _ => throw new IllegalStateException("Not(ant) is not in expected format: " + norme)
}
//pick the first predicate that holds true
- preds.collectFirst { case pred @ _ if predEval(pred) => pred }.get
+ preds.collectFirst { case pred @ _ if predEval(pred).get => pred }.get
}
- def isMultOp(call : Call) : Boolean = {
+ def isMultOp(call: Call): Boolean = {
isMultFunctions(call.fi.tfd.fd)
}
- def unaryMultAxioms(formula: Formula, calls: Set[Call], predEval: (Expr => Boolean)) : Seq[Expr] = {
+ def unaryMultAxioms(formula: Formula, calls: Set[Call], predEval: (Expr => Option[Boolean])): Seq[Expr] = {
val axioms = calls.flatMap {
- case call@_ if (isMultOp(call) && axiomFactory.hasUnaryAxiom(call)) => {
- val (ant,conseq) = axiomFactory.unaryAxiom(call)
- if(predEval(ant))
- Seq(ant,conseq)
+ case call @ _ if (isMultOp(call) && axiomFactory.hasUnaryAxiom(call)) => {
+ val (ant, conseq) = axiomFactory.unaryAxiom(call)
+ if (predEval(ant).get)
+ Seq(ant, conseq)
else
Seq(chooseSATPredicate(Not(ant), predEval))
}
@@ -74,19 +74,19 @@ class NLTemplateSolverWithMult(ctx : InferenceContext, program: Program, rootFun
axioms.toSeq
}
- def binaryMultAxioms(formula: Formula, calls: Set[Call], predEval: (Expr => Boolean)) : Seq[Expr] = {
+ def binaryMultAxioms(formula: Formula, calls: Set[Call], predEval: (Expr => Option[Boolean])): Seq[Expr] = {
val mults = calls.filter(call => isMultOp(call) && axiomFactory.hasBinaryAxiom(call))
- val product = 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)
+ ctx.reporter.info("Theory axioms: " + product.size)
Stats.updateCumStats(product.size, "-Total-theory-axioms")
val newpreds = product.flatMap(pair => {
val axiomInsts = axiomFactory.binaryAxiom(pair._1, pair._2)
axiomInsts.flatMap {
- case (ant,conseq) if predEval(ant) => Seq(ant,conseq) //if axiom-pre holds.
- case (ant,_) => Seq(chooseSATPredicate(Not(ant), predEval)) //if axiom-pre does not hold.
+ case (ant, conseq) if predEval(ant).get => Seq(ant, conseq) //if axiom-pre holds.
+ case (ant, _) => Seq(chooseSATPredicate(Not(ant), predEval)) //if axiom-pre does not hold.
}
})
newpreds.toSeq
diff --git a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
index 6b2aa300b2792f7f86b5f01565ee783731f8d863..93d2608fff979e00d910cfd752c7368efeb2c810 100644
--- a/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala
@@ -40,9 +40,9 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
if (mayAlias(call, call2)) {
call match {
- case Equals(_, fin : FunctionInvocation) => functions += 1
- case Equals(_, tup : Tuple) => tuples += 1
- case _ => adts += 1
+ case Equals(_, fin: FunctionInvocation) => functions += 1
+ case Equals(_, tup: Tuple) => tuples += 1
+ case _ => adts += 1
}
if (debugAliases)
println("Aliases: " + call + "," + call2)
@@ -62,7 +62,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
j += 1
acc ++ pairs
})
- if(verbose) reporter.info("Number of compatible calls: " + product.size)
+ if (verbose) reporter.info("Number of compatible calls: " + product.size)
/*reporter.info("Compatible Tuples: "+tuples)
reporter.info("Compatible Functions+ADTs: "+(functions+adts))*/
Stats.updateCounterStats(product.size, "Compatible-Calls", "disjuncts")
@@ -77,24 +77,25 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
* The calls could be functions calls or ADT constructor calls.
* 'predEval' is an evaluator that evaluates a predicate to a boolean value
*/
- def constraintsForCalls(calls: Set[Expr], predEval: (Expr => Boolean)): Seq[Expr] = {
+ def constraintsForCalls(calls: Set[Expr], predEval: (Expr => Option[Boolean])): Seq[Expr] = {
//check if two calls (to functions or ADT cons) have the same value in the model
- def doesAlias(call1: Expr, call2: Expr): Boolean = {
+ def doesAlias(call1: Expr, call2: Expr): Option[Boolean] = {
val Operator(Seq(r1 @ Variable(_), _), _) = call1
val Operator(Seq(r2 @ Variable(_), _), _) = call2
- val resEquals = predEval(Equals(r1, r2))
- if (resEquals) {
- if (isCallExpr(call1)) {
+ predEval(Equals(r1, r2)) match {
+ case Some(true) if isCallExpr(call1) =>
val (ants, _) = axiomatizeCalls(call1, call2)
- val antsHold = ants.forall(ant => {
+ val antsEvals = ants.map(ant => {
val Operator(Seq(lvar @ Variable(_), rvar @ Variable(_)), _) = ant
- //(model(lid) == model(rid))
predEval(Equals(lvar, rvar))
})
- antsHold
- } else true
- } else false
+ // return `false` if at least one argument is false
+ if (antsEvals.exists(_ == Some(false))) Some(false)
+ else if (antsEvals.exists(!_.isDefined)) None // here, we cannot decide if the call is true or false
+ else Some(true)
+ case r => r
+ }
}
def predForEquality(call1: Expr, call2: Expr): Seq[Expr] = {
@@ -115,7 +116,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
else false
}
}
- case e@_ => throw new IllegalStateException("Not an equality or Iff: " + e)
+ case e @ _ => throw new IllegalStateException("Not an equality or Iff: " + e)
}
preds
}
@@ -139,7 +140,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
ants.foreach(eq =>
if (unsatOtherEq.isEmpty) {
eq match {
- case Equals(lhs @ Variable(_), rhs @ Variable(_)) if !predEval(Equals(lhs, rhs)) => {
+ case Equals(lhs @ Variable(_), rhs @ Variable(_)) if predEval(Equals(lhs, rhs)) == Some(false) => { // there must exist at least one such predicate
if (lhs.getType != Int32Type && lhs.getType != RealType && lhs.getType != IntegerType)
unsatOtherEq = Some(eq)
else if (unsatIntEq.isEmpty)
@@ -153,21 +154,11 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
//pick the constraint a < b or a > b that is satisfied
val Equals(lhs @ Variable(_), rhs @ Variable(_)) = unsatIntEq.get
val lLTr = LessThan(lhs, rhs)
- val atom = if (predEval(lLTr)) lLTr
- else GreaterThan(lhs, rhs)
- /*val InfiniteIntegerLiteral(lval) = model(lid)
- val InfiniteIntegerLiteral(rval) = model(rid)
- val atom = if (lval < rval) LessThan(lhs, rhs)
- else if (lval > rval) GreaterThan(lhs, rhs)
- else throw new IllegalStateException("Models are equal!!")*/
-
- /*if (ants.exists(_ match {
- case Equals(l, r) if (l.getType != Int32Type && l.getType != RealType && l.getType != BooleanType && l.getType != IntegerType) => true
- case _ => false
- })) {
- Stats.updateCumStats(1, "Diseq-blowup")
- }*/
- Seq(atom)
+ predEval(lLTr) match {
+ case Some(true) => Seq(lLTr)
+ case Some(false) => Seq(GreaterThan(lhs, rhs))
+ case _ => Seq() // actually this case cannot happen.
+ }
} else throw new IllegalStateException("All arguments are equal: " + (call1, call2))
}
}
@@ -177,21 +168,22 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
val product = collectCompatibleCalls(calls)
val newctrs = product.foldLeft(Seq[Expr]())((acc, pair) => {
val (call1, call2) = (pair._1, pair._2)
- //println("Assertionizing "+call1+" , call2: "+call2)
+ //note: here it suffices to check for adjacency and not reachability of calls (i.e, exprs).
+ //This is because the transitive equalities (corresponding to rechability) are encoded by the generated equalities.
if (!eqGraph.BFSReach(call1, call2) && !neqSet.contains((call1, call2)) && !neqSet.contains((call2, call1))) {
- if (doesAlias(call1, call2)) {
- eqGraph.addEdge(call1, call2)
- //note: here it suffices to check for adjacency and not reachability of calls (i.e, exprs).
- //This is because the transitive equalities (corresponding to rechability) are encoded by the generated equalities.
- acc ++ predForEquality(call1, call2)
-
- } else {
- neqSet ++= Set((call1, call2))
- acc ++ predForDisequality(call1, call2)
+ doesAlias(call1, call2) match {
+ case Some(true) =>
+ eqGraph.addEdge(call1, call2)
+ acc ++ predForEquality(call1, call2)
+ case Some(false) =>
+ neqSet ++= Set((call1, call2))
+ acc ++ predForDisequality(call1, call2)
+ case _ =>
+ // in this case, we construct a weaker disjunct by dropping this predicate
+ acc
}
} else acc
})
-
//reporter.info("Number of equal calls: " + eqGraph.getEdgeCount)
newctrs
}
@@ -203,22 +195,6 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
* TODO: handling generic can become very trickier here.
*/
def mayAlias(e1: Expr, e2: Expr): Boolean = {
- //check if call and call2 are compatible
- /*(e1, e2) match {
- case (Equals(_, FunctionInvocation(fd1, _)), Equals(_, FunctionInvocation(fd2, _))) if (fd1.id == fd2.id) => true
- case (Equals(_, CaseClass(cd1, _)), Equals(_, CaseClass(cd2, _))) if (cd1.id == cd2.id) => true
- case (Equals(_, tp1 @ Tuple(e1)), Equals(_, tp2 @ Tuple(e2))) => {
- //get the types and check if the types are compatible
- val TupleType(tps1) = tp1.getType
- val TupleType(tps2) = tp2.getType
- (tps1 zip tps2).forall(pair => {
- val (t1, t2) = pair
- val lub = TypeOps.leastUpperBound(t1, t2)
- (lub == Some(t1) || lub == Some(t2))
- })
- }
- case _ => false
- }*/
(e1, e2) match {
case (Equals(_, FunctionInvocation(fd1, _)), Equals(_, FunctionInvocation(fd2, _))) => {
(fd1.id == fd2.id && fd1.fd.tparams == fd2.fd.tparams)
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 867ba31ab448e8648ae4cfa69fc1aa97ec84fa8c..c40e38a9c15e0e941c88a883d158241331b9a74d 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -50,7 +50,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/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 10902ebbf49a409d19d584b2c57c799fc5487d0e..bc58705858d6ef833e67d0d701438be859c2915e 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -45,7 +45,7 @@ trait Solver extends Interruptible {
protected def unsupported(t: Tree, str: String): Nothing = {
val err = SolverUnsupportedError(t, this, Some(str))
- leonContext.reporter.warning(err.getMessage)
+ //leonContext.reporter.warning(str)
throw err
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 86cf40f474e62859acfd1fe2c0953e588590d6df..466e49c0cbd42ebeaf3336248536b8bb79da5191 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -53,7 +53,6 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
}
case _ =>
}
-
new Model(model)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index eac8f47f948f5eceb8c728c900c15d31fc8fd310..f9f8e386c628c3550983afece5a984197e3e07ba 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -57,7 +57,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
val t = SSymbol("T")
setSort = Some(s)
- val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
+ val arraySort = Sort(SMTIdentifier(SSymbol("Array")),
Seq(Sort(SMTIdentifier(t)), BoolSort()))
val cmd = DefineSort(s, Seq(t), arraySort)
@@ -76,7 +76,6 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
val n = s.name.split("!").toList.last
GenericValue(tp, n.toInt)
-
case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe)) =>
if (letDefs contains k) {
// Need to recover value form function model
diff --git a/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala b/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
index 5ae81cbc13502a6b42e1a91ae71d6f7095c24fe3..7a3b07008d178147ba92d166323cdc4ad16fbe27 100644
--- a/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
+++ b/testcases/lazy-datastructures/withOrb/RealTimeQueue.scala
@@ -102,11 +102,11 @@ object RealTimeQueue {
createQ(q.f, Cons(x, q.r), q.s)
} ensuring (res => res.valid && time <= ?)
- def dequeue[T](q: Queue[T]): Queue[T] = {
+ /*def dequeue[T](q: Queue[T]): Queue[T] = {
require(!q.isEmpty && q.valid)
q.f.value match {
case SCons(x, nf) =>
createQ(nf, q.r, q.s)
}
- } ensuring (res => res.valid && time <= ?)
+ } ensuring (res => res.valid && time <= ?)*/
}