Skip to content
Snippets Groups Projects
Commit 0c050e16 authored by Ravi's avatar Ravi
Browse files

Minor changes

parent 413ea2e8
No related branches found
No related tags found
No related merge requests found
...@@ -57,7 +57,6 @@ object Main { ...@@ -57,7 +57,6 @@ object Main {
val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false) 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 optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
val optLazyEval = LeonFlagOptionDef("lazy", "Handles programs that may use the lazy construct", 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]] = override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval) Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv, optLazyEval)
......
...@@ -25,7 +25,7 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef, ...@@ -25,7 +25,7 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
protected val tru = BooleanLiteral(true) protected val tru = BooleanLiteral(true)
//protected val zero = IntLiteral(0) //protected val zero = IntLiteral(0)
private val dumpVCtoConsole = true private val dumpVCtoConsole = false
private val dumpVCasText = false private val dumpVCasText = false
/** /**
......
...@@ -56,6 +56,9 @@ object LazinessEliminationPhase extends TransformationPhase { ...@@ -56,6 +56,9 @@ object LazinessEliminationPhase extends TransformationPhase {
// options that control behavior // options that control behavior
val optRefEquality = LeonFlagOptionDef("refEq", "Uses reference equality for comparing closures", false) 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. * TODO: add inlining annotations for optimization.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment