From 1f2deec434353da76e5a4225d1f4a6a9b99716ff Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 20 Nov 2013 16:53:17 +0100
Subject: [PATCH] Have Condition Abduction work at least in manual mode
---
src/main/scala/leon/synthesis/SynthesisPhase.scala | 6 +++++-
.../scala/leon/synthesis/condabd/SynthesizerExamples.scala | 1 -
2 files changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index f430ceef6..a4eaaa451 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -99,7 +99,11 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
}
if (options.manualSearch) {
- options = options.copy(rules = rules.AsChoose +: options.rules)
+ options = options.copy(
+ rules = rules.AsChoose +:
+ condabd.rules.ConditionAbductionSynthesisTwoPhase +:
+ options.rules
+ )
}
options
diff --git a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
index d1b0622b7..9e7f018eb 100755
--- a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
+++ b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
@@ -652,7 +652,6 @@ class SynthesizerForRuleExamples(
, _root_.leon.codegen.CodeGenParams(maxFunctionInvocations = 500, checkContracts = true))
val res = _evaluator.eval(newCandidate, exMapping)
- println(res)
// if (newCandidate.toString contains "tree.value < value")
// interactivePause
--
GitLab