epfl-lara/leon — pull request #38 by kaptoxic (2013-09-26 21:12:23+00:00)
Title: Topic: Condition Abduction

Okay, finally, the condition abduction branch should be ready for a PR.
It unfortunately took me a surprisingly lot of time to refactor the code (even moving the code to appropriate packages was cubersome). InSynth lives in a separate repo, while the code here strictly deals with Leon, CA, and usage of InSynth within Leon.

### TODO
* There are some errors when CA is executed presumably because the CodeGen parameter implementation for maximum number of invocations is not yet merge into master (as suggested by Etienne, as well as to make a PR nevertheless)
* I did not format the code (as Etienne suggested) since I was not sure if I will make it right and follow the right style, thus we may want to amend the last commit (I would also suggest using ScalaStyle for easier enforcing of the code style)

#### Some notes:
* the package with condition abduction is named *condabd* instead of *lesynth*
* this package is located in the the *leon/synthesis*
* the package name reflects the rule name and is not *InSynth* because it only uses InSynth for enumeration of terms
* InSynth code is no longer there - everything is refactored out to a new repo (you got the email), while there is a new .jar in unmanaged/common
* *insynth* is a subpackage of *condabd* and modifies InSynth so that it can be used in Leon
* the only thing that modifies the existing Leon code should be the return of the good old *FunctionType*