Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adding dReal to JavaSMT #313 #328

Open
wants to merge 157 commits into
base: master
Choose a base branch
from
Open

Adding dReal to JavaSMT #313 #328

wants to merge 157 commits into from

Conversation

juliusbrehme
Copy link

Integrating dReal to JavaSMT.

Problems with dReal:

  • dReal does not support UF's
  • dReal does not support existential quantifier
  • dReal uses delta-precision, therefore Integer formulas are unsound:
    • Example: x_1 != x_2 && x_1 < 1 && x_2 < 1 && 0 <= x_1 && 0 <= x_2 should be unsatisfiable, but it is not (see Issue)
    • Division with Integer does not work correctly (see Issue)
    • Because integer division does not work properly, the result of modularCongruence() in IntegerFormulaManager is not always correct, because integer division is used.
  • It is not possible to create an integer number with BigInteger, only if the number is smaller than 1.0E9.

juliusbrehme and others added 30 commits July 16, 2023 14:56
@juliusbrehme
init dreal4
5ede66e
@juliusbrehme
added QuantifiedFormulaManager
531966c
@juliusbrehme
Updated to use QuantifiedFormulaManager and implemented the rest of N…
dacfc77 
…umeralFormulaManager
@juliusbrehme
added getType to DRealTerm
9a4d26d
@juliusbrehme
implemented visit-Method
f3e49bf
@juliusbrehme
remove wrong Documentation
346d7f7
@juliusbrehme
added explaination to why that class is needed
1328bbc
@juliusbrehme
implemented callFunctionImpl
ca3c95f
@juliusbrehme
changed TFunctDecl from DRealTerm to FunctionDeclarationKind
7073df5
@juliusbrehme
added Method to get the type when splitting formula into Expressions
2d9b8ca
@juliusbrehme
Changed DRealTerm to generic class
fdbc185
@juliusbrehme
implemented FormulaCreator
075e00e
@juliusbrehme
Use Wildcard Operator, so that there are no raw types
053b3c7
@juliusbrehme
Added VariableSet to getQuantifiedVariabes and modified CheckSat, so …
6ccb739 
…that it does not use optional
@juliusbrehme
added visitQuantified in visit-method
db32be5
@juliusbrehme
added isUnsat and addConstraint to TheoremProver
a817e9d
@juliusbrehme
init NativeAPITest
ab59f77
@juliusbrehme
init Model
7898073
@juliusbrehme
added dReal to SolverContextFactory
c9a0e15
@juliusbrehme
corrected add and substract methods
2860dde
@juliusbrehme
addded HashMap to store Variables for only creating new Variables
6e5b0ab
@juliusbrehme
changed Type when creating Formulas from Expression in <, <=, etc.
f7afde7
@juliusbrehme
corrected equals method
a6ba7cc
@juliusbrehme
added pLoader dreal
f3555dd
@juliusbrehme
overwritte addImpl and orImpl
f2d784b
@juliusbrehme
implemented rest of TheoremProver
19f75ef
@juliusbrehme
override substitute-method
37bc31f
@juliusbrehme
fixed iterater used in visit and added pow(x,-1) in visit, when negat…
4e7a4a9 
…e is called
@juliusbrehme
added evalImpl
4af6a01
@juliusbrehme
corrected negate method to inverse variable/number
318bf7d
@juliusbrehme juliusbrehme linked an issue Aug 24, 2023 that may be closed by this pull request
Adding dReal to JavaSMT #313
Open
@juliusbrehme
Copy link
Author

Proposal for integrating trigonometric functions:

dReal does support trigonometric functions. Trigonometric functions are not supported in JavaSMT, but this could be implemented in RationalFormula. Other solvers do support them as well, like Z3.
dReal has the following trigonometric functions, they can be found in expression.h and in Dreal.java:

  • sin()
  • cos()
  • tan()
  • asin()
  • acos()
  • atan()
  • atan2()
  • sinh()
  • cosh()
  • tanh()

juliusbrehme and others added 24 commits August 28, 2023 10:34
@juliusbrehme
added SolverRace to compare performance between solvers solving ratio…
fc071bf 
…nal formulas
@juliusbrehme
updated the assertion
a98d7b7
@juliusbrehme
format source code
f013b66
@juliusbrehme
added private constructor for utility class
2ad3549
@juliusbrehme
use of preconditions
6ad85d4
@juliusbrehme
removed unnecassary ;
cc7b8dc
@daniel-raffler
DReal: Removed 2 project files from the repository.
ff425ff
@daniel-raffler
DReal: Moved native code to /lib and remove an object file that shoul…
7e1adae 
…d not have been included.
@daniel-raffler
DReal: Fixed a typo in a class name.
8a973c6
@daniel-raffler
Merge remote-tracking branch 'refs/remotes/origin/master' into 313-ad…
84912b7 
…ding-dreal-to-javasmt

# Conflicts:
#	src/org/sosy_lab/java_smt/test/BooleanFormulaSubjectTest.java
#	src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java
#	src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java
#	src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.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/SolverTheoriesTest.java
@daniel-raffler
DReal: Moved handling of the assertion stack from DReal4TheoremProver…
1d77a80 
… to its superclass AbstractProver.
@daniel-raffler
DReal: Updated build instruction for Ubuntu 23.10
dc0484e
@daniel-raffler
DReal: Added missing step
e339dca
@daniel-raffler
DReal: Updated build documentation
f2af4b3
@daniel-raffler
DReal: Added skeleton build script for the backend.
a25d764
@daniel-raffler
DReal: Fixed formatting
bb272a2
@daniel-raffler
DReal: Fixed crashes in ModelTest and ModelEvaluationTest. There seem…
172b017 
…s to be an issue with Expression.getVariables, which was patched into the SWIG code. I've added a workaround for now, but the proper way to do it would be to add a SWIG script and recreate the bindings from there.
@daniel-raffler
DReal: Fixed library loading in DReal4NativeAPITest
b62b272
@daniel-raffler
DReal: Fixed getVariablesTest from DReal4NativeAPITest (See 172b017)
5f39ba6
@daniel-raffler
DReal: Blacklisted dReal for some tests in SolverStackTest0
c1c1bd6
@daniel-raffler
DReal: Use requireUnsatCore in a tests that used to check manually.
9baa309
@daniel-raffler
DReal: Added missing license information
045f894
@daniel-raffler
DReal: Added a proper build script for dReal.
263756d
@daniel-raffler
DReal: Remove dReal build files in 'ant clean' task.
97068ef
@daniel-raffler
Copy link
Contributor

I've just added a build script for packaging the dReal solver backend. It is still quite basic and will only repackage the binaries that are povided by the dReal team. Building the project ourselves is quite involved as it depends on libibex and the build tool bazel, neither of which is available in the Ubuntu repositories. They can be installed from ppa, but this still requires root access.

Also note that the library does have quite a few dependencies that will have to be installed locally:

daniel@ZenBook:~/workspace/java-smt$ ldd libdreal-4.21.06.2-gf93bdcc.so
libnlopt.so.0 => /lib/x86_64-linux-gnu/libnlopt.so.0 (0x0000758d78bfd000)
libClpSolver.so.1 => /lib/x86_64-linux-gnu/libClpSolver.so.1 (0x0000758d78ab7000)
libClp.so.1 => /lib/x86_64-linux-gnu/libClp.so.1 (0x0000758d7893e000)
libCoinUtils.so.3 => /lib/x86_64-linux-gnu/libCoinUtils.so.3 (0x0000758d78825000)
liblapack.so.3 => /lib/x86_64-linux-gnu/liblapack.so.3 (0x0000758d78000000)
libblas.so.3 => /lib/x86_64-linux-gnu/libblas.so.3 (0x0000758d78789000)
libopenblas.so.0 => /lib/x86_64-linux-gnu/libopenblas.so.0 (0x0000758d75528000)
...

@baierd Could you upload the binaries, please?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Adding dReal to JavaSMT
3 participants
@juliusbrehme @daniel-raffler @baierd