diff --git a/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala
deleted file mode 100755
index 35eadb6b13575236ae07267069eefe33e34219e8..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala
+++ /dev/null
@@ -1,80 +0,0 @@
-//package leon.synthesis.condabd
-//package rules
-//
-//import leon.purescala.Trees._
-//import leon.purescala.Common._
-//import leon.purescala.TypeTrees._
-//import leon.purescala.TreeOps._
-//import leon.purescala.Extractors._
-//import leon.purescala.Definitions._
-//import leon.synthesis._
-//import leon.solvers.{ Solver, TimeoutSolver }
-//import leon.evaluators.CodeGenEvaluator
-//
-//import examples.InputExamples._
-//import evaluation._
-//
-//import leon.StopwatchCollections
-//
-//case object ConditionAbductionSynthesisImmediate extends Rule("Condition abduction synthesis (immediate).") {
-// def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
-//
-// p.xs match {
-// case givenVariable :: Nil =>
-// val solver = new TimeoutSolver(sctx.solver, 500L)
-// val program = sctx.program
-// val reporter = sctx.reporter
-//
-// val desiredType = givenVariable.getType
-// val holeFunDef = sctx.functionContext.get
-//
-// // temporary hack, should not mutate FunDef
-// val oldPostcondition = holeFunDef.postcondition
-// val oldPrecondition = holeFunDef.precondition
-//
-// try {
-// val freshResID = FreshIdentifier("result").setType(holeFunDef.returnType)
-// val freshResVar = Variable(freshResID)
-//
-// val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
-// def getInputExamples = {
-// () =>
-// getDataGenInputExamples(codeGenEval, p,
-// 200, 6000, Some(p.as)) ++
-// getDataGenInputExamplesRandomIntegers(codeGenEval, p,
-// 200, 6000, Some(p.as) // bound the random geenerator
-// , 5)
-// }
-//
-// val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 1000)
-//
-// holeFunDef.postcondition = Some(replace(
-// Map(givenVariable.toVariable -> ResultVariable().setType(holeFunDef.returnType)), p.phi))
-// holeFunDef.precondition = Some(p.pc)
-//
-// val synthesizer = new SynthesizerForRuleExamples(
-// solver, solver.getNewSolver, program, desiredType, holeFunDef, p, sctx, evaluationStrategy,
-// 20, 1,
-// reporter = reporter,
-// introduceExamples = getInputExamples,
-// numberOfTestsInIteration = 25,
-// numberOfCheckInIteration = 2)
-//
-// synthesizer.synthesize match {
-// case EmptyReport => None
-// case FullReport(resFunDef, _) =>
-// List(
-// RuleInstantiation.immediateSuccess(p, this,
-// Solution(resFunDef.getPrecondition, Set.empty, resFunDef.body.get)))
-// }
-// } finally {
-// holeFunDef.postcondition = oldPostcondition
-// holeFunDef.precondition = oldPrecondition
-// }
-// case _ =>
-// throw new RuntimeException("Rule is not applicable for more than one output variable.")
-// Nil
-// }
-//
-// }
-//}
diff --git a/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
index 21f63f6c4e61891062bb08dc25ac9823f78f2da1..49cacd1f311df3aee16e1b5e422f964f9b1624e8 100755
--- a/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -33,24 +33,23 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
// temporary hack, should not mutate FunDef
val oldPostcondition = holeFunDef.postcondition
-
+
try {
val freshResID = FreshIdentifier("result").setType(holeFunDef.returnType)
val freshResVar = Variable(freshResID)
-
+
val codeGenEval = new CodeGenEvaluator(sctx.context, sctx.program)
def getInputExamples = {
() =>
//getDataGenInputExamples(sctx.context, sctx.program, codeGenEval, p,
- // 100, 6000, Some(p.as)) ++
+ // 100, 6000, Some(p.as)) ++
getDataGenInputExamplesRandomIntegers(sctx.context, sctx.program, codeGenEval, p,
- 100, 6000, Some(p.as)
- // bound the random geenerator
- ,10)
+ 100, 6000, Some(p.as)
+ // bound the random geenerator
+ ,10)
}
-
- val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 5000)
-
+
+ val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 5000)
holeFunDef.postcondition = Some((givenVariable, p.phi))
val synthesizer = new SynthesizerForRuleExamples(
@@ -58,9 +57,9 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
20, 1,
reporter = reporter,
introduceExamples = getInputExamples,
- numberOfTestsInIteration = 25,
- numberOfCheckInIteration = 2
- )
+ numberOfTestsInIteration = 25,
+ numberOfCheckInIteration = 2
+ )
synthesizer.synthesize match {
case EmptyReport => RuleApplicationImpossible
@@ -69,7 +68,7 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
println("Compilation time: " + StopwatchCollections.get("Compilation").getMillis)
RuleSuccess(
Solution(BooleanLiteral(true), Set.empty, Tuple(Seq(resFunDef.body.get))),
- isTrusted = !synthesizer.verifier.isTimeoutUsed
+ isTrusted = !synthesizer.verifier.isTimeoutUsed
)
}
} catch {
@@ -84,9 +83,7 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
}
})
case _ =>
-// throw new RuntimeException("Rule is not applicable for more than one output variable.")
Nil
}
-
}
}