From b63cebb736982f07487cb32000e5f2e726f2ce01 Mon Sep 17 00:00:00 2001
From: Ivan Kuraj <ivan.kuraj@epfl.ch>
Date: Thu, 26 Sep 2013 21:53:04 +0200
Subject: [PATCH] Moved code to appropriate packages and formatted sources
---
.../synthesis/condabd}/Report.scala | 2 +-
.../synthesis/condabd}/SynthesisInfo.scala | 2 +-
.../condabd}/SynthesizerExamples.scala | 19 ++++++-----
.../evaluation/CodeGenExampleRunner.scala | 8 ++---
.../evaluation/DefaultExampleRunner.scala | 8 ++---
.../evaluation/EvaluationStrategy.scala | 8 ++---
.../condabd}/evaluation/ExampleRunner.scala | 6 ++--
.../synthesis/condabd}/examples/Example.scala | 2 +-
.../condabd}/examples/InputExamples.scala | 2 +-
.../synthesis/condabd}/insynth/InSynth.scala | 15 +++++----
.../condabd}/insynth/leon/CommonTypes.scala | 2 +-
.../insynth/leon/DomainTypeTransformer.scala | 2 +-
.../insynth/leon/LeonDeclaration.scala | 2 +-
.../leon/ReconstructionExpression.scala | 2 +-
.../insynth/leon/TypeTransformer.scala | 2 +-
.../leon/loader/DeclarationFactory.scala | 7 ++--
.../insynth/leon/loader/LoadSpec.scala | 2 +-
.../condabd}/insynth/leon/loader/Loader.scala | 4 +--
.../insynth/leon/loader/PreLoader.scala | 6 ++--
.../insynth/leon/query}/LeonQuery.scala | 5 +--
.../leon/query}/LeonQueryBuilder.scala | 5 +--
.../insynth/reconstruction/Output.scala | 2 +-
.../reconstruction/Reconstructor.scala | 5 +--
.../codegen/CodeGenerator.scala | 16 ++++-----
.../condabd}/ranking/Candidate.scala | 6 ++--
.../condabd}/ranking/Evaluation.scala | 4 +--
.../synthesis/condabd}/ranking/Ranker.scala | 2 +-
.../condabd}/refinement/Filter.scala | 6 ++--
.../condabd}/refinement/VariableRefiner.scala | 4 +--
.../refinement/VariableSolverRefiner.scala | 22 ++++++-------
...ConditionAbductionSynthesisImmediate.scala | 6 ++--
.../ConditionAbductionSynthesisTwoPhase.scala | 6 ++--
.../verification/AbstractVerifier.scala | 25 +++++++-------
.../verification/RelaxedVerifier.scala | 22 +++++++------
.../condabd}/verification/Verifier.scala | 22 +++++++------
.../test/condabd}/EvaluationTest.scala | 13 ++++----
.../test/condabd}/FilterTest.scala | 10 +++---
.../test/condabd}/VariableRefinerTest.scala | 9 +++--
.../condabd}/VariableSolverRefinerTest.scala | 11 +++----
.../test/condabd}/VerifierTest.scala | 15 +++++----
.../condabd}/enumeration/EnumeratorTest.scala | 32 ++++++++----------
.../test/condabd}/insynth/InSynthTest.scala | 33 ++++++++-----------
.../condabd}/insynth/loader/LoaderTest.scala | 7 ++--
.../reconstruction/CodeGeneratorTest.scala | 9 ++---
.../reconstruction/ReconstructorTest.scala | 8 +++--
.../insynth/testutil/CommonDeclarations.scala | 6 ++--
.../insynth/testutil/CommonLambda.scala | 5 +--
.../testutil/CommonLeonExpressions.scala | 2 +-
.../insynth/testutil/CommonProofTrees.scala | 4 +--
.../insynth/testutil/CommonUtils.scala | 4 +--
.../test/condabd}/util/Scaffold.scala | 1 +
.../{ => leon/test/condabd}/util/Utils.scala | 1 +
52 files changed, 220 insertions(+), 209 deletions(-)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/Report.scala (98%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/SynthesisInfo.scala (98%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/SynthesizerExamples.scala (99%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/evaluation/CodeGenExampleRunner.scala (97%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/evaluation/DefaultExampleRunner.scala (95%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/evaluation/EvaluationStrategy.scala (97%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/evaluation/ExampleRunner.scala (91%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/examples/Example.scala (87%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/examples/InputExamples.scala (99%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/InSynth.scala (89%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/CommonTypes.scala (89%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/DomainTypeTransformer.scala (97%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/LeonDeclaration.scala (97%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/ReconstructionExpression.scala (97%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/TypeTransformer.scala (97%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/loader/DeclarationFactory.scala (94%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/loader/LoadSpec.scala (56%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/loader/Loader.scala (97%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/leon/loader/PreLoader.scala (97%)
rename src/main/scala/{insynth/leon => leon/synthesis/condabd/insynth/leon/query}/LeonQuery.scala (82%)
rename src/main/scala/{insynth/leon => leon/synthesis/condabd/insynth/leon/query}/LeonQueryBuilder.scala (89%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/reconstruction/Output.scala (87%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/reconstruction/Reconstructor.scala (89%)
rename src/main/scala/{ => leon/synthesis/condabd}/insynth/reconstruction/codegen/CodeGenerator.scala (93%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/ranking/Candidate.scala (96%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/ranking/Evaluation.scala (97%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/ranking/Ranker.scala (99%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/refinement/Filter.scala (98%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/refinement/VariableRefiner.scala (97%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/refinement/VariableSolverRefiner.scala (91%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/rules/ConditionAbductionSynthesisImmediate.scala (97%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/rules/ConditionAbductionSynthesisTwoPhase.scala (97%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/verification/AbstractVerifier.scala (90%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/verification/RelaxedVerifier.scala (86%)
rename src/main/scala/{lesynth => leon/synthesis/condabd}/verification/Verifier.scala (84%)
rename src/test/scala/{lesynth => leon/test/condabd}/EvaluationTest.scala (97%)
rename src/test/scala/{lesynth => leon/test/condabd}/FilterTest.scala (97%)
rename src/test/scala/{lesynth => leon/test/condabd}/VariableRefinerTest.scala (95%)
rename src/test/scala/{lesynth => leon/test/condabd}/VariableSolverRefinerTest.scala (97%)
rename src/test/scala/{lesynth => leon/test/condabd}/VerifierTest.scala (94%)
rename src/test/scala/{lesynth => leon/test/condabd}/enumeration/EnumeratorTest.scala (95%)
rename src/test/scala/{ => leon/test/condabd}/insynth/InSynthTest.scala (93%)
rename src/test/scala/{ => leon/test/condabd}/insynth/loader/LoaderTest.scala (96%)
rename src/test/scala/{ => leon/test/condabd}/insynth/reconstruction/CodeGeneratorTest.scala (89%)
rename src/test/scala/{ => leon/test/condabd}/insynth/reconstruction/ReconstructorTest.scala (91%)
rename src/test/scala/{ => leon/test/condabd}/insynth/testutil/CommonDeclarations.scala (94%)
rename src/test/scala/{ => leon/test/condabd}/insynth/testutil/CommonLambda.scala (97%)
rename src/test/scala/{ => leon/test/condabd}/insynth/testutil/CommonLeonExpressions.scala (95%)
rename src/test/scala/{ => leon/test/condabd}/insynth/testutil/CommonProofTrees.scala (97%)
rename src/test/scala/{ => leon/test/condabd}/insynth/testutil/CommonUtils.scala (82%)
rename src/test/scala/{ => leon/test/condabd}/util/Scaffold.scala (98%)
rename src/test/scala/{ => leon/test/condabd}/util/Utils.scala (96%)
diff --git a/src/main/scala/lesynth/Report.scala b/src/main/scala/leon/synthesis/condabd/Report.scala
similarity index 98%
rename from src/main/scala/lesynth/Report.scala
rename to src/main/scala/leon/synthesis/condabd/Report.scala
index 372784d03..caf012459 100755
--- a/src/main/scala/lesynth/Report.scala
+++ b/src/main/scala/leon/synthesis/condabd/Report.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
diff --git a/src/main/scala/lesynth/SynthesisInfo.scala b/src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
similarity index 98%
rename from src/main/scala/lesynth/SynthesisInfo.scala
rename to src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
index e438d2471..e4825a166 100644
--- a/src/main/scala/lesynth/SynthesisInfo.scala
+++ b/src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
import leon.StopwatchCollections
diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
similarity index 99%
rename from src/main/scala/lesynth/SynthesizerExamples.scala
rename to src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
index a66557c4d..beea692e6 100755
--- a/src/main/scala/lesynth/SynthesizerExamples.scala
+++ b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
import scala.collection.mutable.{ PriorityQueue, ArrayBuffer, HashSet }
@@ -20,17 +20,20 @@ import leon.evaluators.EvaluationResults
import leon.evaluators._
import leon.synthesis.{ Problem, SynthesisContext }
-import insynth.{ Solver => _, _ }
+import insynth._
import insynth.leon.loader._
import insynth.leon.{ LeonDeclaration => Declaration, _ }
-import insynth.engine._
import insynth.reconstruction.Output
-import insynth.util.logging.HasLogger
-import lesynth.examples._
-import lesynth.evaluation._
-import lesynth.ranking._
-import lesynth.refinement._
+import _root_.insynth.{ Solver => _, _ }
+import _root_.insynth.engine._
+import _root_.insynth.util.logging.HasLogger
+
+import examples._
+import evaluation._
+import ranking._
+import refinement._
+import verification._
import SynthesisInfo._
import SynthesisInfo.Action._
diff --git a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
similarity index 97%
rename from src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
rename to src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
index a24e93558..d6fd0911c 100644
--- a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package evaluation
import scala.collection.mutable.ArrayBuffer
@@ -12,10 +12,10 @@ import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
import leon.codegen.CodeGenEvalParams
-import lesynth.examples._
-import lesynth.ranking._
+import examples._
+import ranking._
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonContext,
candidates: Seq[Candidate], inputExamples: Seq[Example],
diff --git a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
similarity index 95%
rename from src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
rename to src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
index 45a22e558..e6930d7b5 100644
--- a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package evaluation
import scala.collection.mutable.ArrayBuffer
@@ -11,10 +11,10 @@ import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
-import lesynth.examples._
-import lesynth.ranking._
+import examples._
+import ranking._
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
case class DefaultExampleRunner(program: Program, funDef: FunDef, ctx: LeonContext,
candidates: Seq[Candidate], inputExamples: Seq[Example],
diff --git a/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala b/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
similarity index 97%
rename from src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
rename to src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
index 36ed41c3c..1ab73543a 100644
--- a/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package evaluation
import leon._
@@ -11,10 +11,10 @@ import leon.purescala.TreeOps
import leon.codegen.CodeGenEvalParams
import insynth.reconstruction.Output
-import insynth.util.logging._
+import _root_.insynth.util.logging._
-import lesynth.ranking._
-import lesynth.examples._
+import ranking._
+import examples._
trait EvaluationStrategy extends HasLogger {
def getRanker(candidatePairs: IndexedSeq[(Output)], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]): Ranker
diff --git a/src/main/scala/lesynth/evaluation/ExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
similarity index 91%
rename from src/main/scala/lesynth/evaluation/ExampleRunner.scala
rename to src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
index c93a8fa99..b57e1bd07 100644
--- a/src/main/scala/lesynth/evaluation/ExampleRunner.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package evaluation
import scala.collection.mutable.ArrayBuffer
@@ -8,9 +8,9 @@ import leon.purescala.Common.Identifier
import leon.evaluators._
import leon.evaluators.EvaluationResults.Result
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
-import lesynth.examples.Example
+import examples.Example
abstract class ExampleRunner(inputExamples: Seq[Example]) extends HasLogger {
diff --git a/src/main/scala/lesynth/examples/Example.scala b/src/main/scala/leon/synthesis/condabd/examples/Example.scala
similarity index 87%
rename from src/main/scala/lesynth/examples/Example.scala
rename to src/main/scala/leon/synthesis/condabd/examples/Example.scala
index 10a47e48c..2a9abdb5f 100644
--- a/src/main/scala/lesynth/examples/Example.scala
+++ b/src/main/scala/leon/synthesis/condabd/examples/Example.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package examples
import leon.purescala.Trees._
diff --git a/src/main/scala/lesynth/examples/InputExamples.scala b/src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
similarity index 99%
rename from src/main/scala/lesynth/examples/InputExamples.scala
rename to src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
index 9336f5337..d4732049c 100755
--- a/src/main/scala/lesynth/examples/InputExamples.scala
+++ b/src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package examples
import leon.purescala.TypeTrees._
diff --git a/src/main/scala/insynth/InSynth.scala b/src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
similarity index 89%
rename from src/main/scala/insynth/InSynth.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
index 3646bad45..5dea8c9a8 100644
--- a/src/main/scala/insynth/InSynth.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
@@ -1,14 +1,15 @@
-package insynth
+package leon.synthesis.condabd.insynth
-import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFactory }
-import insynth.reconstruction.codegen.CodeGenerator
-import insynth.reconstruction.Reconstructor
+import reconstruction.codegen.CodeGenerator
+import reconstruction.Reconstructor
+import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFactory }
+import insynth.Solver
import insynth.engine.InitialEnvironmentBuilder
-import insynth.leon.{ LeonDeclaration => Declaration }
-import insynth.leon.loader.LeonLoader
-import insynth.leon.LeonQueryBuilder
+import leon.{ LeonDeclaration => Declaration }
+import leon.loader.LeonLoader
+import leon.query.LeonQueryBuilder
import _root_.leon.purescala.Definitions.Program
import _root_.leon.purescala.TypeTrees.{ TypeTree => Type }
diff --git a/src/main/scala/insynth/leon/CommonTypes.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
similarity index 89%
rename from src/main/scala/insynth/leon/CommonTypes.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
index 1e7f5ba62..50c78fac0 100644
--- a/src/main/scala/insynth/leon/CommonTypes.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
diff --git a/src/main/scala/insynth/leon/DomainTypeTransformer.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
similarity index 97%
rename from src/main/scala/insynth/leon/DomainTypeTransformer.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
index 7c37f3322..1ff79a4f9 100644
--- a/src/main/scala/insynth/leon/DomainTypeTransformer.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import insynth.structures._
diff --git a/src/main/scala/insynth/leon/LeonDeclaration.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
similarity index 97%
rename from src/main/scala/insynth/leon/LeonDeclaration.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
index 229b18395..ec910fcc0 100644
--- a/src/main/scala/insynth/leon/LeonDeclaration.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import insynth.structures.SuccinctType
import insynth.structures.Weight._
diff --git a/src/main/scala/insynth/leon/ReconstructionExpression.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
similarity index 97%
rename from src/main/scala/insynth/leon/ReconstructionExpression.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
index 3d9692e45..67db5ee32 100644
--- a/src/main/scala/insynth/leon/ReconstructionExpression.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import leon.purescala.TypeTrees.{ TypeTree => LeonType }
import leon.purescala.Trees.Expr
diff --git a/src/main/scala/insynth/leon/TypeTransformer.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
similarity index 97%
rename from src/main/scala/insynth/leon/TypeTransformer.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
index e22d48ba8..9ddff7a91 100644
--- a/src/main/scala/insynth/leon/TypeTransformer.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import insynth.structures._
diff --git a/src/main/scala/insynth/leon/loader/DeclarationFactory.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
similarity index 94%
rename from src/main/scala/insynth/leon/loader/DeclarationFactory.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
index 809de1141..27e1294e5 100644
--- a/src/main/scala/insynth/leon/loader/DeclarationFactory.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
@@ -1,9 +1,10 @@
-package insynth.leon.loader
+package leon.synthesis.condabd.insynth.leon.loader
+
+import leon.synthesis.condabd.insynth.leon.{ LeonDeclaration => Declaration, _ }
+import leon.synthesis.condabd.insynth.leon.TypeTransformer
-import insynth.leon.{ LeonDeclaration => Declaration, _ }
import insynth.engine.InitialEnvironmentBuilder
import insynth.structures.{ SuccinctType => InSynthType, Variable => InSynthVariable, _ }
-import insynth.leon.TypeTransformer
import leon.purescala.Definitions._
import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
diff --git a/src/main/scala/insynth/leon/loader/LoadSpec.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
similarity index 56%
rename from src/main/scala/insynth/leon/loader/LoadSpec.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
index 835e1f8fc..2bd618183 100644
--- a/src/main/scala/insynth/leon/loader/LoadSpec.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
@@ -1,4 +1,4 @@
-package insynth.leon.loader
+package leon.synthesis.condabd.insynth.leon.loader
/** defines what to load in the PreLoader */
class LoadSpec {
diff --git a/src/main/scala/insynth/leon/loader/Loader.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
similarity index 97%
rename from src/main/scala/insynth/leon/loader/Loader.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
index 5a7a90805..f703f8ae0 100644
--- a/src/main/scala/insynth/leon/loader/Loader.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
@@ -1,6 +1,6 @@
-package insynth.leon.loader
+package leon.synthesis.condabd.insynth.leon.loader
-import insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression, ImmediateExpression, UnaryReconstructionExpression }
+import leon.synthesis.condabd.insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression, ImmediateExpression, UnaryReconstructionExpression }
import insynth.structures.{ SuccinctType => InSynthType }
import insynth.load.Loader
import insynth.util.logging.HasLogger
diff --git a/src/main/scala/insynth/leon/loader/PreLoader.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
similarity index 97%
rename from src/main/scala/insynth/leon/loader/PreLoader.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
index 2a1d6fe0a..47223b5a9 100644
--- a/src/main/scala/insynth/leon/loader/PreLoader.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
@@ -1,7 +1,9 @@
-package insynth.leon.loader
+package leon.synthesis.condabd.insynth.leon.loader
+import leon.synthesis.condabd.insynth.leon.{
+ LeonDeclaration => Declaration, NaryReconstructionExpression => NAE, ImmediateExpression => IE
+}
import insynth.structures.{ SuccinctType => InSynthType }
-import insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression => NAE, ImmediateExpression => IE }
import insynth.engine.InitialEnvironmentBuilder
import leon.purescala.Definitions.{ Program, FunDef }
diff --git a/src/main/scala/insynth/leon/LeonQuery.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
similarity index 82%
rename from src/main/scala/insynth/leon/LeonQuery.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
index 9b4ba6d16..f2947b60c 100644
--- a/src/main/scala/insynth/leon/LeonQuery.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
@@ -1,6 +1,7 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
+package query
-import insynth.leon.loader.DeclarationFactory
+import loader.DeclarationFactory
import insynth.engine.InitialSender
import insynth.structures.SuccinctType
import insynth.query.Query
diff --git a/src/main/scala/insynth/leon/LeonQueryBuilder.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
similarity index 89%
rename from src/main/scala/insynth/leon/LeonQueryBuilder.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
index e78ef6e7b..177240b41 100644
--- a/src/main/scala/insynth/leon/LeonQueryBuilder.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
@@ -1,10 +1,11 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
+package query
import insynth.query._
import insynth.engine.InitialSender
import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
-import insynth.leon.loader.DeclarationFactory
+import loader.DeclarationFactory
import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
import leon.purescala.Common.FreshIdentifier
diff --git a/src/main/scala/insynth/reconstruction/Output.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
similarity index 87%
rename from src/main/scala/insynth/reconstruction/Output.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
index 0f0a13a99..d4929d82b 100644
--- a/src/main/scala/insynth/reconstruction/Output.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
@@ -1,4 +1,4 @@
-package insynth.reconstruction
+package leon.synthesis.condabd.insynth.reconstruction
import insynth.structures.Weight._
import leon.purescala.Trees.Expr
diff --git a/src/main/scala/insynth/reconstruction/Reconstructor.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
similarity index 89%
rename from src/main/scala/insynth/reconstruction/Reconstructor.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
index a1e6506c1..389d50788 100644
--- a/src/main/scala/insynth/reconstruction/Reconstructor.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
@@ -1,9 +1,10 @@
-package insynth.reconstruction
+package leon.synthesis.condabd.insynth.reconstruction
import insynth.structures.{ SimpleNode, Weight }
import insynth.reconstruction.stream.{ Node => LambdaNode, _ }
+import insynth.reconstruction._
-import insynth.reconstruction.codegen.CodeGenerator
+import codegen.CodeGenerator
import insynth.util.format.{ FormatSuccinctNode, FormatStreamUtils }
import insynth.util.logging.HasLogger
diff --git a/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
similarity index 93%
rename from src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
index ae1f93441..0342dcc0d 100644
--- a/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
@@ -1,19 +1,19 @@
-package insynth.reconstruction.codegen
+package leon
+package synthesis.condabd.insynth
+package reconstruction.codegen
import scala.text.Document
import scala.text.Document.empty
-import insynth.leon._
+import leon._
import insynth.reconstruction.stream._
-
import insynth.structures.Function
-
import insynth.util.logging.HasLogger
-import leon.purescala.Trees.{ Expr }
-import leon.purescala.TypeTrees.{ TypeTree => DomainType, FunctionType }
-import leon.purescala.{ TypeTrees => domain }
-import leon.purescala.Trees.{ Expr => CodeGenOutput }
+import purescala.Trees.{ Expr }
+import purescala.TypeTrees.{ TypeTree => DomainType, FunctionType }
+import purescala.{ TypeTrees => domain }
+import purescala.Trees.{ Expr => CodeGenOutput }
/**
* class that converts an intermediate tree into a list of output elements (elements
diff --git a/src/main/scala/lesynth/ranking/Candidate.scala b/src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
similarity index 96%
rename from src/main/scala/lesynth/ranking/Candidate.scala
rename to src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
index 761a0e2b3..1c073f879 100644
--- a/src/main/scala/lesynth/ranking/Candidate.scala
+++ b/src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package ranking
import leon.purescala.Trees._
@@ -8,8 +8,8 @@ import leon.purescala.TypeTrees._
import leon.purescala.TreeOps
import insynth.reconstruction.Output
-import insynth.structures.Weight._
-import insynth.util.logging.HasLogger
+import _root_.insynth.structures.Weight._
+import _root_.insynth.util.logging.HasLogger
object Candidate {
private var _freshResultVariable: Identifier = _
diff --git a/src/main/scala/lesynth/ranking/Evaluation.scala b/src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
similarity index 97%
rename from src/main/scala/lesynth/ranking/Evaluation.scala
rename to src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
index 7186b689d..88472e33d 100644
--- a/src/main/scala/lesynth/ranking/Evaluation.scala
+++ b/src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
@@ -1,7 +1,7 @@
-package lesynth
+package leon.synthesis.condabd
package ranking
-import lesynth.evaluation._
+import evaluation._
case class Evaluation(exampleRunner: ExampleRunner) {
diff --git a/src/main/scala/lesynth/ranking/Ranker.scala b/src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
similarity index 99%
rename from src/main/scala/lesynth/ranking/Ranker.scala
rename to src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
index 39c4f753a..3654b69e7 100644
--- a/src/main/scala/lesynth/ranking/Ranker.scala
+++ b/src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package ranking
import scala.util.control.Breaks._
diff --git a/src/main/scala/lesynth/refinement/Filter.scala b/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
similarity index 98%
rename from src/main/scala/lesynth/refinement/Filter.scala
rename to src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
index 90c6f25de..b524d66a4 100755
--- a/src/main/scala/lesynth/refinement/Filter.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
@@ -1,5 +1,5 @@
-package lesynth
-package refinement
+package leon.synthesis
+package condabd.refinement
import scala.collection.mutable._
@@ -10,7 +10,7 @@ import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
import leon.plugin.ExtractionPhase
-import insynth.leon.loader.LeonLoader
+import condabd.insynth.leon.loader.LeonLoader
import insynth.util.logging.HasLogger
/**
diff --git a/src/main/scala/lesynth/refinement/VariableRefiner.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
similarity index 97%
rename from src/main/scala/lesynth/refinement/VariableRefiner.scala
rename to src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
index df821f62f..07c9ed8db 100755
--- a/src/main/scala/lesynth/refinement/VariableRefiner.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package refinement
import scala.collection.mutable.{Map => MutableMap}
@@ -13,7 +13,7 @@ import leon.purescala.Common.{ Identifier, FreshIdentifier }
import insynth.leon.loader._
import insynth.leon.{ LeonDeclaration => Declaration, _ }
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
// each variable of super type can actually have a subtype
// get sine declaration maps to be able to refine them
diff --git a/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
similarity index 91%
rename from src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
rename to src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
index 59ec68fcc..45adc6a24 100755
--- a/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
@@ -1,23 +1,23 @@
-package lesynth
+package leon
+package synthesis.condabd
package refinement
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
-import leon._
-import leon.purescala.Extractors._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.Definitions._
-import leon.solvers._
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.synthesis.Problem
+import purescala.Extractors._
+import purescala.TypeTrees._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.Definitions._
+import purescala.Common.{ Identifier, FreshIdentifier }
+import solvers._
+import synthesis.Problem
import insynth.leon.loader._
import insynth.leon._
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
// each variable of super type can actually have a subtype
// get sine declaration maps to be able to refine them
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala
similarity index 97%
rename from src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
rename to src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala
index 5feec355e..35eadb6b1 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
+++ b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala
@@ -1,4 +1,4 @@
-//package lesynth
+//package leon.synthesis.condabd
//package rules
//
//import leon.purescala.Trees._
@@ -11,8 +11,8 @@
//import leon.solvers.{ Solver, TimeoutSolver }
//import leon.evaluators.CodeGenEvaluator
//
-//import lesynth.examples.InputExamples._
-//import lesynth.evaluation._
+//import examples.InputExamples._
+//import evaluation._
//
//import leon.StopwatchCollections
//
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
similarity index 97%
rename from src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
rename to src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
index 95324fce6..21f63f6c4 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package rules
import leon.purescala.Trees._
@@ -11,8 +11,8 @@ import leon.synthesis._
import leon.solvers._
import leon.evaluators.CodeGenEvaluator
-import lesynth.examples.InputExamples._
-import lesynth.evaluation._
+import examples.InputExamples._
+import evaluation._
import leon.StopwatchCollections
diff --git a/src/main/scala/lesynth/verification/AbstractVerifier.scala b/src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
similarity index 90%
rename from src/main/scala/lesynth/verification/AbstractVerifier.scala
rename to src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
index 0508293bb..b9922e255 100644
--- a/src/main/scala/lesynth/verification/AbstractVerifier.scala
+++ b/src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
@@ -1,18 +1,19 @@
-package lesynth
+package leon
+package synthesis
+package condabd
+package verification
-import leon.solvers._
-import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.Extractors._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.synthesis._
+import solvers._
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Definitions._
-import insynth.util.logging._
+import _root_.insynth.util.logging._
-abstract class AbstractVerifier(solverf: SolverFactory[Solver], p: Problem,
- synthInfo: SynthesisInfo)
+abstract class AbstractVerifier(solverf: SolverFactory[Solver], p: Problem, synthInfo: SynthesisInfo)
extends HasLogger {
val solver = solverf.getNewSolver
diff --git a/src/main/scala/lesynth/verification/RelaxedVerifier.scala b/src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
similarity index 86%
rename from src/main/scala/lesynth/verification/RelaxedVerifier.scala
rename to src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
index 91d8b0946..2dfa87843 100644
--- a/src/main/scala/lesynth/verification/RelaxedVerifier.scala
+++ b/src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
@@ -1,15 +1,17 @@
-package lesynth
+package leon
+package synthesis
+package condabd
+package verification
-import leon.solvers._
-import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.Extractors._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.synthesis._
+import solvers._
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Definitions._
-import insynth.util.logging._
+import _root_.insynth.util.logging._
class RelaxedVerifier(solverf: SolverFactory[Solver], p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
extends AbstractVerifier(solverf, p, synthInfo) with HasLogger {
diff --git a/src/main/scala/lesynth/verification/Verifier.scala b/src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
similarity index 84%
rename from src/main/scala/lesynth/verification/Verifier.scala
rename to src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
index eda23f3f2..c1c74a38a 100644
--- a/src/main/scala/lesynth/verification/Verifier.scala
+++ b/src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
@@ -1,15 +1,17 @@
-package lesynth
+package leon
+package synthesis
+package condabd
+package verification
-import leon.solvers._
-import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.Extractors._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.synthesis._
+import solvers._
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Definitions._
-import insynth.util.logging._
+import _root_.insynth.util.logging._
class Verifier(solverf: SolverFactory[Solver], p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
extends AbstractVerifier(solverf, p, synthInfo) with HasLogger {
diff --git a/src/test/scala/lesynth/EvaluationTest.scala b/src/test/scala/leon/test/condabd/EvaluationTest.scala
similarity index 97%
rename from src/test/scala/lesynth/EvaluationTest.scala
rename to src/test/scala/leon/test/condabd/EvaluationTest.scala
index 59b04e930..ef7d53911 100644
--- a/src/test/scala/lesynth/EvaluationTest.scala
+++ b/src/test/scala/leon/test/condabd/EvaluationTest.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.test.condabd
import org.scalatest.FunSuite
import org.scalatest.matchers.ShouldMatchers._
@@ -14,13 +14,12 @@ import leon.codegen.CodeGenEvalParams
import leon.purescala.TypeTrees._
import leon.evaluators.EvaluationResults._
-import lesynth.examples.InputExamples
-import lesynth.evaluation.CodeGenEvaluationStrategy
-import lesynth.ranking.Candidate
-import insynth.reconstruction.Output
-import lesynth.examples.Example
+import leon.synthesis.condabd.examples._
+import leon.synthesis.condabd.evaluation.CodeGenEvaluationStrategy
+import leon.synthesis.condabd.ranking.Candidate
+import leon.synthesis.condabd.insynth.reconstruction.Output
-import _root_.util.Scaffold
+import util.Scaffold
// TODO codegen evaluator params should be used but not yet in master
class EvaluationTest extends FunSuite {
diff --git a/src/test/scala/lesynth/FilterTest.scala b/src/test/scala/leon/test/condabd/FilterTest.scala
similarity index 97%
rename from src/test/scala/lesynth/FilterTest.scala
rename to src/test/scala/leon/test/condabd/FilterTest.scala
index a308510fa..d439df536 100644
--- a/src/test/scala/lesynth/FilterTest.scala
+++ b/src/test/scala/leon/test/condabd/FilterTest.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.test.condabd
import scala.util.Random
@@ -6,17 +6,17 @@ import org.junit.Assert._
import org.junit.{ Test, Ignore, Before }
import org.scalatest.junit.JUnitSuite
-import insynth.leon.loader.LeonLoader
-import insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader.LeonLoader
+import leon.synthesis.condabd.insynth.leon._
import _root_.leon.purescala.Trees._
import _root_.leon.purescala.TypeTrees._
import _root_.leon.purescala._
import _root_.leon.purescala.Definitions._
-import lesynth.refinement._
+import leon.synthesis.condabd.refinement._
-import _root_.util._
+import util._
class FilterTest extends JUnitSuite {
diff --git a/src/test/scala/lesynth/VariableRefinerTest.scala b/src/test/scala/leon/test/condabd/VariableRefinerTest.scala
similarity index 95%
rename from src/test/scala/lesynth/VariableRefinerTest.scala
rename to src/test/scala/leon/test/condabd/VariableRefinerTest.scala
index dcaae9ee1..c6b9f43ad 100644
--- a/src/test/scala/lesynth/VariableRefinerTest.scala
+++ b/src/test/scala/leon/test/condabd/VariableRefinerTest.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.test.condabd
import scala.util.Random
@@ -10,11 +10,10 @@ import leon.purescala.Common._
import leon.purescala.TypeTrees._
import leon.purescala.Trees._
-import insynth.leon._
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.refinement._
-import lesynth.refinement._
-
-import _root_.util.Scaffold._
+import util.Scaffold._
class VariableRefinerTest extends FunSpec with GivenWhenThen {
diff --git a/src/test/scala/lesynth/VariableSolverRefinerTest.scala b/src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala
similarity index 97%
rename from src/test/scala/lesynth/VariableSolverRefinerTest.scala
rename to src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala
index 52175cd08..dc1d945ca 100644
--- a/src/test/scala/lesynth/VariableSolverRefinerTest.scala
+++ b/src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.test.condabd
import scala.util.Random
@@ -11,12 +11,11 @@ import leon.purescala.TypeTrees._
import leon.purescala.Trees._
import insynth._
-import insynth.leon._
-import insynth.leon.loader._
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
+import leon.synthesis.condabd.refinement._
-import lesynth.refinement._
-
-import _root_.util._
+import util._
class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
diff --git a/src/test/scala/lesynth/VerifierTest.scala b/src/test/scala/leon/test/condabd/VerifierTest.scala
similarity index 94%
rename from src/test/scala/lesynth/VerifierTest.scala
rename to src/test/scala/leon/test/condabd/VerifierTest.scala
index 7a41d0e76..de88e347c 100644
--- a/src/test/scala/lesynth/VerifierTest.scala
+++ b/src/test/scala/leon/test/condabd/VerifierTest.scala
@@ -1,21 +1,22 @@
-package lesynth
+package leon.test.condabd
import org.junit.Assert._
import org.junit._
import org.scalatest._
import org.scalatest.matchers._
-import insynth.leon.loader.LeonLoader
+import leon.synthesis.condabd.insynth.leon.loader.LeonLoader
+import leon.synthesis.condabd.verification._
-import _root_.leon.purescala._
-import _root_.leon.evaluators._
-import _root_.leon.solvers._
-import _root_.leon.purescala.Trees._
+import leon.purescala._
+import leon.evaluators._
+import leon.solvers._
+import leon.purescala.Trees._
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.synthesis.Problem
-import _root_.util._
+import util._
class VerifierTest extends FunSpec {
diff --git a/src/test/scala/lesynth/enumeration/EnumeratorTest.scala b/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
similarity index 95%
rename from src/test/scala/lesynth/enumeration/EnumeratorTest.scala
rename to src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
index 6e54425f8..fff9381c3 100644
--- a/src/test/scala/lesynth/enumeration/EnumeratorTest.scala
+++ b/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
@@ -1,15 +1,15 @@
-package lesynth
+package leon.test.condabd
-import insynth.InSynth
-import insynth.leon._
-import insynth.leon.loader._
-import insynth.engine._
+import leon.synthesis.condabd.insynth.InSynth
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
+import leon.synthesis.condabd.insynth.reconstruction.codegen._
+import leon.synthesis.condabd.insynth.reconstruction.Output
-import insynth.reconstruction._
-import insynth.reconstruction.{ stream => lambda }
-import insynth.reconstruction.stream.{ OrderedStreamFactory }
-import insynth.reconstruction.codegen._
-import insynth.reconstruction.Output
+import _root_.insynth.engine._
+import _root_.insynth.reconstruction._
+import _root_.insynth.reconstruction.{ stream => lambda }
+import _root_.insynth.reconstruction.stream.{ OrderedStreamFactory }
import _root_.leon._
import _root_.leon.purescala._
@@ -17,20 +17,16 @@ import _root_.leon.purescala.Definitions._
import _root_.leon.purescala.Common._
import _root_.leon.purescala.TypeTrees._
import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
+import _root_.insynth.util.format._
+import _root_.insynth.util._
-import lesynth.refinement._
-//import lesynth.examples._
-//import lesynth.evaluation.CodeGenEvaluationStrategy
-//import lesynth.ranking.Candidate
+import leon.synthesis.condabd.refinement._
import org.junit.{ Test, Ignore }
import org.junit.Assert._
import org.scalatest.junit.JUnitSuite
-import insynth.util.format._
-import insynth.util._
-
-import _root_.util._
+import util._
import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
diff --git a/src/test/scala/insynth/InSynthTest.scala b/src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
similarity index 93%
rename from src/test/scala/insynth/InSynthTest.scala
rename to src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
index acf730adf..a7dee3aa7 100644
--- a/src/test/scala/insynth/InSynthTest.scala
+++ b/src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
@@ -1,35 +1,30 @@
+package leon.test.condabd
package insynth
-import insynth.leon._
-import insynth.leon.loader._
-import insynth.engine._
+import leon.synthesis.condabd.insynth.InSynth
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
+import leon.synthesis.condabd.insynth.reconstruction.codegen._
+import leon.synthesis.condabd.insynth.reconstruction.Output
-import insynth.reconstruction._
-import insynth.reconstruction.{ stream => lambda }
-import insynth.reconstruction.stream.{ OrderedStreamFactory }
-import insynth.reconstruction.codegen._
-import insynth.reconstruction.Output
+import _root_.insynth.engine._
+import _root_.insynth.reconstruction._
+import _root_.insynth.reconstruction.{ stream => lambda }
+import _root_.insynth.reconstruction.stream.{ OrderedStreamFactory }
+import _root_.insynth.util.format._
+import _root_.insynth.util._
import _root_.leon.purescala.Definitions._
import _root_.leon.purescala.Common._
import _root_.leon.purescala.TypeTrees._
import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
-//import lesynth.refinement._
-//import lesynth.examples._
-//import lesynth.evaluation.CodeGenEvaluationStrategy
-//import lesynth.ranking.Candidate
-
import org.junit.{ Test, Ignore }
import org.junit.Assert._
import org.scalatest.junit.JUnitSuite
-import insynth.util.format._
-import insynth.util._
-
-import _root_.util._
-
-import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
+import util._
+import testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
// TODO test abstractions (vals)
class InSynthTest extends JUnitSuite {
diff --git a/src/test/scala/insynth/loader/LoaderTest.scala b/src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
similarity index 96%
rename from src/test/scala/insynth/loader/LoaderTest.scala
rename to src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
index 5982957f7..40f98eda8 100644
--- a/src/test/scala/insynth/loader/LoaderTest.scala
+++ b/src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
@@ -1,10 +1,11 @@
+package leon.test.condabd
package insynth
package loader
-import _root_.util._
+import util._
-import insynth.leon._
-import insynth.leon.loader._
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
import _root_.leon.purescala.Definitions._
import _root_.leon.purescala.Common._
diff --git a/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala b/src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
similarity index 89%
rename from src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
rename to src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
index 3d86a6fd8..c5a7f5bcb 100644
--- a/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
+++ b/src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
@@ -1,14 +1,15 @@
-package insynth.reconstruction
+package leon.test.condabd.insynth
+package reconstruction
import org.junit.Assert._
import org.junit.{ Test, Ignore }
import org.scalatest.junit.JUnitSuite
-import insynth.reconstruction.codegen.CodeGenerator
+import leon.synthesis.condabd.insynth.reconstruction.codegen.CodeGenerator
-import leon.purescala.Trees._
+import _root_.leon.purescala.Trees._
-import insynth.testutil.{ CommonLambda, CommonDeclarations }
+import testutil.{ CommonLambda, CommonDeclarations }
// NOTE function cannot return function in Leon, no need to test that
diff --git a/src/test/scala/insynth/reconstruction/ReconstructorTest.scala b/src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
similarity index 91%
rename from src/test/scala/insynth/reconstruction/ReconstructorTest.scala
rename to src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
index 177f2e01e..c57ef877e 100644
--- a/src/test/scala/insynth/reconstruction/ReconstructorTest.scala
+++ b/src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
@@ -1,17 +1,19 @@
-package insynth.reconstruction
+package leon.test.condabd.insynth
+package reconstruction
import org.junit.{ Test, Ignore, BeforeClass, AfterClass }
import org.junit.Assert._
import org.scalatest.junit.JUnitSuite
-import insynth.reconstruction.codegen.CodeGenerator
+import leon.synthesis.condabd.insynth.reconstruction.codegen.CodeGenerator
+import leon.synthesis.condabd.insynth.reconstruction._
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ FreshIdentifier }
import leon.purescala.TypeTrees._
import leon.purescala.Trees.{ Variable => LeonVariable, _ }
-import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLeonExpressions, CommonUtils }
+import testutil.{ CommonProofTrees, CommonDeclarations, CommonLeonExpressions, CommonUtils }
class ReconstructorTest extends JUnitSuite {
diff --git a/src/test/scala/insynth/testutil/CommonDeclarations.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
similarity index 94%
rename from src/test/scala/insynth/testutil/CommonDeclarations.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
index faca9b3b2..8fb24261f 100644
--- a/src/test/scala/insynth/testutil/CommonDeclarations.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
@@ -1,4 +1,4 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
@@ -6,8 +6,8 @@ import org.junit.Assert._
import org.junit.Test
import org.junit.Ignore
-import insynth.leon.loader.DeclarationFactory._
-import insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader.DeclarationFactory._
+import leon.synthesis.condabd.insynth.leon._
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ FreshIdentifier }
diff --git a/src/test/scala/insynth/testutil/CommonLambda.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
similarity index 97%
rename from src/test/scala/insynth/testutil/CommonLambda.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
index e5dc73cb4..4ff98d922 100644
--- a/src/test/scala/insynth/testutil/CommonLambda.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
@@ -1,6 +1,7 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
-import insynth.leon.{ LeonQueryBuilder => QueryBuilder, _ }
+import leon.synthesis.condabd.insynth.leon.query.{ LeonQueryBuilder => QueryBuilder, _ }
+import leon.synthesis.condabd.insynth.leon._
import insynth.reconstruction.stream._
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
diff --git a/src/test/scala/insynth/testutil/CommonLeonExpressions.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
similarity index 95%
rename from src/test/scala/insynth/testutil/CommonLeonExpressions.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
index 1ab08d1b4..7576d3a08 100644
--- a/src/test/scala/insynth/testutil/CommonLeonExpressions.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
@@ -1,4 +1,4 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ FreshIdentifier }
diff --git a/src/test/scala/insynth/testutil/CommonProofTrees.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
similarity index 97%
rename from src/test/scala/insynth/testutil/CommonProofTrees.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
index 82f5adac4..2cf742e76 100644
--- a/src/test/scala/insynth/testutil/CommonProofTrees.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
@@ -1,4 +1,4 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
@@ -6,7 +6,7 @@ import org.junit.Assert._
import org.junit.Test
import org.junit.Ignore
-import insynth.leon.{ LeonQueryBuilder => QueryBuilder, _ }
+import leon.synthesis.condabd.insynth.leon.query.{ LeonQueryBuilder => QueryBuilder, _ }
import insynth.structures._
import leon.purescala.TypeTrees._
diff --git a/src/test/scala/insynth/testutil/CommonUtils.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
similarity index 82%
rename from src/test/scala/insynth/testutil/CommonUtils.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
index 406452b93..c0e9c24ae 100644
--- a/src/test/scala/insynth/testutil/CommonUtils.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
@@ -1,8 +1,8 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
import org.junit.Assert._
-import insynth.reconstruction.Output
+import leon.synthesis.condabd.insynth.reconstruction.Output
object CommonUtils {
diff --git a/src/test/scala/util/Scaffold.scala b/src/test/scala/leon/test/condabd/util/Scaffold.scala
similarity index 98%
rename from src/test/scala/util/Scaffold.scala
rename to src/test/scala/leon/test/condabd/util/Scaffold.scala
index fd31cdc20..253fc7054 100644
--- a/src/test/scala/util/Scaffold.scala
+++ b/src/test/scala/leon/test/condabd/util/Scaffold.scala
@@ -1,3 +1,4 @@
+package leon.test.condabd
package util
import org.scalatest.FunSuite
diff --git a/src/test/scala/util/Utils.scala b/src/test/scala/leon/test/condabd/util/Utils.scala
similarity index 96%
rename from src/test/scala/util/Utils.scala
rename to src/test/scala/leon/test/condabd/util/Utils.scala
index dd72243f0..36c7ddf7d 100644
--- a/src/test/scala/util/Utils.scala
+++ b/src/test/scala/leon/test/condabd/util/Utils.scala
@@ -1,3 +1,4 @@
+package leon.test.condabd
package util
import org.scalatest.FunSuite
--
GitLab