creating branch for new satsolver: Princess

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12585 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
initial commit to support Princess. You need to have three libraries in your library-path: princess.jar (download from http://www.philipp.ruemmer.org/princess.shtml), scala-library.jar and lib/scala-actors.jar (Scala must be in version 2.10.3, other version will cause strange ClassNotFound-Exceptions). Currently CPAchecker can solve simple files with a correct result, but Princess needs much more memory than other solvers (for those simple files) and the JVM does not quit after printing the result (Scala-related bug?).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12586 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
some small fixes

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12603 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
some cleanup, adding code for escaping names (ugly, but working), adding cache for declared functions.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12618 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
enabling proof-construction in Princess.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12619 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
removing code for escaping string, the new version of Princess allows to disable 'sanitise'. cleanup.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12621 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding close-method to PrincessFormulaMgr. Currently it is not called in a default analysis.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12631 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding code for simplification. when checking formulas, Princess behaves very similiar to earlier versions of SMTinterpol: It first visits all sub-formulas of a formula.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12632 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
fix wrong cast

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12633 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
fixing NullPointer and wrong type of ModelValue.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12638 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
create Numbers directly, instead of using the Environment.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12649 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
switching from single-stack to multi-stack-behaviour. Princess allows to add 'externally' declared symbols to the current SimpleAPI (this allows to copy them from another instance of SimpleAPI). Each Theorem- orInterpolating-Solver has now its own instance of SimpleAPI. Princess also removes symbols from the solver-stack after pop-operations. Now those symbols are re-added after pop.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12650 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
flag for interpolationis only used in InterpolatingProver.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12654 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
fixing and implementing allsat

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12659 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding initial code for 'abbreviation' of formulas. currently not used, because we do not revert abbreviations, where needed.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12703 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
bugfix

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12704 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
renaming

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12713 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
merge from trunk

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12717 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
adding Junit-test. All Solvers should have the same behaviour.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12718 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
removing outdated TODOs

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/Princess@12719 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c