314 adding the abstract numeric domains of the apron library as smt solver#346
314 adding the abstract numeric domains of the apron library as smt solver#346
Conversation
Merge branch '314-adding-the-abstract-numeric-domains-of-the-apron-library-as-smt-solver' of github.com:sosy-lab/java-smt into 314-adding-the-abstract-numeric-domains-of-the-apron-library-as-smt-solver
baierd
left a comment
baierd
left a comment
There was a problem hiding this comment.
Some minor points to address before we can merge.
|
|
||
| public class ApronApiTest { | ||
|
|
||
| public static Manager manager = new PolkaEq(); |
There was a problem hiding this comment.
Can you add a small description as to what PolkaEQ is for people not fimilar with abstract numeric domains?
|
|
||
| @Override | ||
| protected ApronNode not(ApronNode pParam1) { | ||
| throw new UnsupportedOperationException("Apron does not support not() operations."); |
There was a problem hiding this comment.
You could add a comment about the possibility of transforming the formula into negation normal form, as discussed in your talk.
| } | ||
| } | ||
|
|
||
| private ApronNode getComplexValue(ApronNode pNode) { |
There was a problem hiding this comment.
The method is quite big, maybe it would be good to split it up.
src/org/sosy_lab/java_smt/solvers/apron/ApronRationalFormulaManager.java
Outdated
Show resolved
Hide resolved
| } | ||
| return first; | ||
| } | ||
| return null; |
There was a problem hiding this comment.
Is null the correct return here?
Maybe throw an exception instead?
There was a problem hiding this comment.
I'm returning 0 now.
…ding-the-abstract-numeric-domains-of-the-apron-library-as-smt-solver # Conflicts: # .gitignore # build/build-publish-solvers.xml # lib/ivy.xml # src/org/sosy_lab/java_smt/test/BooleanFormulaSubjectTest.java # src/org/sosy_lab/java_smt/test/FormulaManagerTest.java # src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java # src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java # src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java # src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java # src/org/sosy_lab/java_smt/test/SolverBasedTest0.java # src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java # src/org/sosy_lab/java_smt/test/SolverStackTest.java # src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java
…actProver to manage its assertion stack.
|
@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: (We need the |
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? |
…ot match any of the special cases. This is necessary as default values don't work properly and the argument may not have been fully substituted. In that case it's not a value at all and we need to return 'null'.
|
@kfriedberger we should decide if we want to add this Apron based SMT solver to JavaSMT or not. It has the same limitations as dReal due to being based on abstract interpretation. However, we could try using ELINA instead of Apron, which seems to be more precise and faster. However, both projects seem to be abandoned. |
3 participants
Integration of the APRON Numeric Abstract Domain Library as a quasi SMT solver supporting Integer, Rational and Boolean.
Problems with the implementation:
x = 3, y = 1/2gives]-infinity, infinity[as value set forx = y +3for bothxandy;