From 0c050e1658a9fd83c193d66159061e9a434a3512 Mon Sep 17 00:00:00 2001
From: Ravi <ravi.kandhadai@epfl.ch>
Date: Sun, 24 Jan 2016 15:08:40 +0100
Subject: [PATCH] Minor changes
---
src/main/scala/leon/Main.scala | 1 -
.../scala/leon/invariant/templateSolvers/TemplateSolver.scala | 2 +-
src/main/scala/leon/laziness/LazinessEliminationPhase.scala | 3 +++
3 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 579e1803c..71b49841f 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -57,7 +57,6 @@ object Main {
val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
val optLazyEval = LeonFlagOptionDef("lazy", "Handles programs that may use the lazy construct", false)
- //val optMemoize = LeonFlagOptionDef("memoize", "Handles programs that uses memoization", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval)
diff --git a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
index 032ace5c3..a85a7d4f5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
@@ -25,7 +25,7 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
protected val tru = BooleanLiteral(true)
//protected val zero = IntLiteral(0)
- private val dumpVCtoConsole = true
+ private val dumpVCtoConsole = false
private val dumpVCasText = false
/**
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 0c54c5570..abfd45aac 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -56,6 +56,9 @@ object LazinessEliminationPhase extends TransformationPhase {
// options that control behavior
val optRefEquality = LeonFlagOptionDef("refEq", "Uses reference equality for comparing closures", false)
+ val optUseOrb = LeonFlagOptionDef("useOrb", "Use Orb to infer constants", false)
+
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(optUseOrb)
/**
* TODO: add inlining annotations for optimization.
--
GitLab