diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala
index c5984d28e1a3834801bca79ddd28f35b4c96f0d8..e18803b95cc67c60cb2f67b304c94cfbf9503674 100644
--- a/src/main/scala/leon/invariant/engine/InferenceReport.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala
@@ -34,7 +34,12 @@ class InferenceCondition(invs: Seq[Expr], funDef: FunDef)
simplifyArithmetic(InstUtil.replaceInstruVars(multToTimes(inv), fd))) match {
case Seq() => None
case Seq(inv) => Some(inv)
- case invs => Some(And(invs))
+ case invs =>
+ invs.map(ExpressionTransformer.simplify _).filter(_ != tru) match {
+ case Seq() => Some(tru)
+ case Seq(ninv) => Some(ninv)
+ case ninvs => Some(And(ninvs))
+ }
}
def status: String = prettyInv match {
diff --git a/src/main/scala/leon/transformations/InstProgSimplifier.scala b/src/main/scala/leon/transformations/InstProgSimplifier.scala
index ff7862db1c535421db229ede3dda6efecad93713..ab650449b58df9897fb89191d3d10bc065b54557 100644
--- a/src/main/scala/leon/transformations/InstProgSimplifier.scala
+++ b/src/main/scala/leon/transformations/InstProgSimplifier.scala
@@ -9,7 +9,10 @@ import purescala.ExprOps._
import purescala.Types._
import leon.purescala.ScalaPrinter
import leon.utils._
-import invariant.util.Util._
+import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
import invariant.util.ExpressionTransformer._
import invariant.structure.FunctionUtils._
import invariant.util.LetTupleSimplification._
diff --git a/src/main/scala/leon/transformations/InstrumentationUtil.scala b/src/main/scala/leon/transformations/InstrumentationUtil.scala
index 427cac483cef7d5ee2b45198a71c1154ee1af999..915defecf041a1f9c821f61619f789c8a408388e 100644
--- a/src/main/scala/leon/transformations/InstrumentationUtil.scala
+++ b/src/main/scala/leon/transformations/InstrumentationUtil.scala
@@ -8,6 +8,11 @@ import purescala.ExprOps._
import purescala.Extractors._
import purescala.Types._
import leon.utils.Library
+import invariant.util._
+import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
sealed abstract class Instrumentation {
val getType: TypeTree
@@ -73,7 +78,7 @@ object InstUtil {
}
def getInstMap(fd: FunDef) = {
- val resvar = invariant.util.Util.getResId(fd).get.toVariable // note: every instrumented function has a postcondition
+ val resvar = getResId(fd).get.toVariable // note: every instrumented function has a postcondition
val insts = fd.id.name.split("-").tail // split the name of the function w.r.t '-'
(insts.zipWithIndex).foldLeft(Map[Expr, String]()) {
case (acc, (instName, i)) =>
@@ -82,7 +87,7 @@ object InstUtil {
}
def getInstExpr(fd: FunDef, inst: Instrumentation) = {
- val resvar = invariant.util.Util.getResId(fd).get.toVariable // note: every instrumented function has a postcondition
+ val resvar = getResId(fd).get.toVariable // note: every instrumented function has a postcondition
val insts = fd.id.name.split("-").tail // split the name of the function w.r.t '-'
val index = insts.indexOf(inst.name)
if (index >= 0)
diff --git a/src/main/scala/leon/transformations/IntToRealProgram.scala b/src/main/scala/leon/transformations/IntToRealProgram.scala
index dc7ceb5a64ea7d15fedc48bc3fe6c40a7607555b..21229282b398fcc10cd9548ddaead2f25d8087a3 100644
--- a/src/main/scala/leon/transformations/IntToRealProgram.scala
+++ b/src/main/scala/leon/transformations/IntToRealProgram.scala
@@ -10,7 +10,10 @@ import purescala.Types._
import leon.purescala.ScalaPrinter
import invariant.factories._
-import invariant.util.Util._
+import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
import invariant.structure._
abstract class ProgramTypeTransformer {
diff --git a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
index 77b88f71e557d2bdb90470f8e684168574f4d1bc..d17968dc05b789b936554b9c10dbde22ac360dfb 100644
--- a/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
+++ b/src/main/scala/leon/transformations/NonlinearityEliminationPhase.scala
@@ -2,7 +2,10 @@ package leon
package transformations
import invariant.factories._
-import invariant.util.Util._
+import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
import invariant.structure.FunctionUtils._
import purescala.ScalaPrinter
@@ -147,7 +150,6 @@ class NonlinearityEliminator(skipAxioms: Boolean, domain: TypeTree) {
Some(replaceFun(simpBody))
} else None
-
//add a new postcondition
newfd.postcondition = if (fd.postcondition.isDefined) {
//we need to handle template and postWoTemplate specially
diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
index 20e3aa0e2bb7912992821e3cb2ced21985820f89..87c5795838b460314d19805cbb8ca6caae4ee233 100644
--- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
+++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
@@ -10,6 +10,9 @@ import purescala.Types._
import leon.purescala.ScalaPrinter
import leon.utils._
import invariant.util._
+import Util._
+import ProgramUtil._
+import PredicateUtil._
import invariant.util.CallGraphUtil
import invariant.structure.FunctionUtils._
import scala.collection.mutable.{Map => MutableMap}
@@ -68,7 +71,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
//create new functions. Augment the return type of a function iff the postcondition uses
//the instrumentation variable or if the function is transitively called from such a function
//note: need not instrument fields
- val funMap = Util.functionsWOFields(program.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
+ val funMap = functionsWOFields(program.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
case (accMap, fd: FunDef) if fd.isTheoryOperation =>
accMap + (fd -> fd)
case (accMap, fd) => {
@@ -160,7 +163,7 @@ class SerialInstrumenter(ctx: LeonContext, program: Program) {
else List()
}.toList.distinct
- val newprog = Util.copyProgram(program, (defs: Seq[Definition]) =>
+ val newprog = copyProgram(program, (defs: Seq[Definition]) =>
defs.map {
case fd: FunDef if funMap.contains(fd) =>
funMap(fd)
diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
index 79b15f3fcb860e3e4b69becf5bafe05aba9a2992..85c898d81548800735be9cdf6b1b718b1e052a29 100644
--- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
+++ b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
@@ -18,46 +18,50 @@ class OrbRegressionSuite extends LeonRegressionSuite {
}
}
- private def testInference(f: File, bound: Int) {
+ private def testInference(f: File, bound: Option[Int] = None) {
- val ctx = createLeonContext("--inferInv", "--minbounds", "--timeout="+bound)
+ val ctx = createLeonContext("--inferInv")
val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)
val processPipe = InferInvariantsPhase
val (ctx3, report) = processPipe.run(ctx2, program)
- val fails = report.conditions.filterNot(_.invariant.isDefined)
- if (!fails.isEmpty)
- fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}")
+ if (report.conditions.isEmpty)
+ fail(s"Nothing was solved")
+ else {
+ val fails = report.conditions.filterNot(_.prettyInv.isDefined)
+ if (!fails.isEmpty)
+ fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}")
+ }
}
forEachFileIn("regression/orb/timing") { f =>
test("Timing: " + f.getName) {
- testInference(f, 200)
+ testInference(f)
}
}
forEachFileIn("regression/orb/stack/") { f =>
test("Stack: " + f.getName) {
- testInference(f, 200)
+ testInference(f)
}
}
forEachFileIn("regression/orb//depth") { f =>
test("Depth: " + f.getName) {
- testInference(f, 200)
+ testInference(f)
}
}
forEachFileIn("regression/orb/numerical") { f =>
test("Numerical: " + f.getName) {
- testInference(f, 200)
+ testInference(f)
}
}
forEachFileIn("regression/orb/combined/") { f =>
test("Multiple Instrumentations: " + f.getName) {
- testInference(f, 200)
+ testInference(f)
}
}
}