Fixed backwards SSA index computation: gaps were possible.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13701 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Added several parameters to the block operator to support backwards predicate
analysis.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13702 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
A first infrastructure for computation of program constraints/relations.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13703 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Optional simplification of abstraction formulas (easier to debug/read)

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13704 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Transferred the handling of the conversion from assignment to assumption to CBinaryExpressionBuilder.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13705 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Implemented lookup methods for CProgramScope

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13706 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
When printing a counterexample, the model may sometimes contain values that do not fit into the specified type, so the value must be cast to the type.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13707 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Deleted the WP-CPA; it was integrated into PredicateCPA.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13708 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Replaced the boolean flag "backwards" by a corresponding ENUM.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13709 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
New interface RelationView; use of enum AnalysisDirection in PredicateCPA.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13710 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Renaming.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13711 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Renmaing

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13712 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Deleted unused config files.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13713 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Deleted the old backwards config for the predicate analysis.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13714 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
New config files that seperate WP inference and the backwards
predicate-analysis.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13715 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Merge FormulaCreator and AbstractFormulaCreator.
As the interface FormulaCreator is not exposed to other packages,
we do not need this distinction.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13716 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove duplicate function AbstractFormulaManager.getTerm(),
which is also present as FormulaCreator.extractInfo().

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13717 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix SmtInterpolModel: we need to use the environment of the Prover
class, not the main environment
(in the future, these might be different).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13718 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Export of weakest preconditions.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13719 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove all the is* methods from NumeralFormulaManager and
BitvectorFormulaManager (e.g., isAdd, isLessThan, etc.).
Only exception for now is isEqual,
which has one user.
All other methods were never used.
Implementing them is work when adding a new solver,
several of them are buggy,
and best is to never use these kinds of methods anyway.
Otherwise you run into trouble for example
when a new solver is added that does different preprocessing on
formulas.
For example, it is not guaranteed that isFoo(makeFoo(...))
returns true, because a lot of solvers rewrite formulas automatically,
and might replace the operator Foo with something else.
Furthermore, solvers can introduce more operators,
such that we can have formulas for which all is* methods return false.

The problems with these methods can even be seen
from the comments inside them.

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