314 adding the abstract numeric domains of the apron library as smt solver

[winnieros]

Integration of the APRON Numeric Abstract Domain Library as a quasi SMT solver supporting Integer, Rational and Boolean. Problems with the implementation:

• Apron doesn't support UFs, no evaluation with CPAchecker possible;
• limited functionalities of Boolean;
• Abstract interpretation uses overapproximation of the value set which leads to unsound results; that does not go in line with SMT; no possibility was found to inform the user about possible overapproximation;
• Model is not trustworthy; ex.: x = 3, y = 1/2 gives ]-infinity, infinity[ as value set for x = y +3 for both x and y;
• Prover can only guarantee for isUnsat(); !isUnsat() can mean SAT or UNKNOWN but it is not possible to further specify such result;

[daniel-raffler]

@baierd The code looks good so far. Can you upload the solver backend to Ivy? (Note that the binaries will depend on system supplied MPFR and GMP libraries. If this is a problem we can probably still change our build script to include them with the installation.)

This is what I used to build the binaries: ant publish-apron -Dapron.path=/home/daniel/workspace/apron-JavaSMT -Dapron.customRev=0.9.14

(We need the apron version from your fork for this: git clone [email protected]:baierd/apron-JavaSMT.git)

[daniel-raffler]

(We need the apron version from your fork for this: git clone [email protected]:baierd/apron-JavaSMT.git)

I could also create a patch from your changes and include it with JavaSMT. This is probably easier to maintain than keeping the fork updated?