dreal4
dreal4 copied to clipboard
dreal
Automated Reasoning in Nonlinear Theories of Reals
i trained some feed forward neural networks using the mnist dataset with the sigmoid activation and converted them into the smt2 format. now i want to test specific records of...
Hi, I'm looking to install and use dreal, but running the provided dependency installation script resulted in the following error on a 2021 Mac 12.2.1 using an M1 Pro Chip,...
We've found some issues with the current version of ibex that we're using (ibex-2.7.4 + custom patches). We will use ibex-2.8.6 instead. Action items: - [ ] Update `libibex-dev` in...
Hello, Is there a documentation for the python bindings somewhere? I am really struggling with figuring out the provided options in python. The python examples on the repo are very...
With the following input, and precision=0.001 : (set-logic QF_NRA) (declare-fun x () Real) (declare-fun y () Real) (declare-fun z () Real) (declare-fun s1 () Real [1.0,4.0]) (declare-fun s2 () Real...
(declare-fun c () Real) (declare-fun d () Real) (assert (
## Summary When using very large integers in dReal, unexpected rounding occurs. ## Example ```lisp (set-logic QF_NRA) ; 9000000000000000 = 9e15 (assert (not (= (+ 9000000000000000 9000000000000001) (+ 9000000000000000 9000000000000000))))...
I would like to use function that convert smt2 file to AST(abstract syntax tree) in python API. Can I use these functions in dreal? If so, Can you please point...
I would like to do some proofs of the form: f is an uninterpreted function fp is the derivative of f -- an uninterpreted function such that fp(x) = df/dx...
