Stack Overflow
Stack Overflow

Questions tagged [dreal]

dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.

dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as first-order logic formulas over the real numbers. Its special strength is in handling problems that involve a wide range of nonlinear real functions.

Source: https://dreal.github.io/

7 questions
31
votes
2 answers

How to use gprof with cmake

I have looked at dozens of tutorials for profiling with gprof. I'm trying to work with code for the SMT solver dReal. To build the program, I first installed g++-4.8, Bison, Flex, and Cmake. Then to build dReal, the instructions said to execute the…
Phdetermined
  • 411
  • 1
  • 4
  • 5
1
vote
1 answer

Some questions about dReal: delta-satisfiability, parameter with 0.0, doing the same in Z3 and obtaining sat/unsat result

I am starting with dReal and I have a set of questions about it. These questions are based on the tutorial we can find in https://github.com/dreal/dreal4, section "Python bindings", with the following code: from dreal import * x = Variable("x") y =…
Theo Deep
  • 666
  • 4
  • 15
1
vote
1 answer

Dreal4 Forall() SMT

I would like to use the Dreal4 SMT solver to check the following condition of a control lyapunov function: there exists a u contained with in the set U for all x contained within the set X for which V(x,u) is negative. (I am calling V(x,u) the lie…
mrEqualsMc
  • 23
  • 3
1
vote
1 answer

Converting type() of a symbolic variable that is compatible with another toolbox in Python

For my assignment, I use two SMT solvers, z3 and dReal. While I do computations in z3 by introducing variables as symbolic variables (sympy), However, dReal requires its own custom variable type called "dreal._dreal_py.Variable". from dreal import *…
Acad
  • 161
  • 5
0
votes
1 answer

env: python2.7: No such file or directory

I tried to install dreal following the instructions in https://pypi.org/project/dreal/. But it failed. The error is 'env: python2.7: No such file or directory'. I guess it is an error related to the Mac OS Monterey? Any help would be appreciated! If…
Qing
  • 11
0
votes
1 answer

SMT solvers for real closed fields (e.g., trascendentals and infinitesimals) in practise? Z3, MetiTarski, dReal

I would like to delve into the capability of SMT solvers to deal with trascendental and infinitesimal elements. Thus, I just read the paper on computing in real closed fields https://www.cl.cam.ac.uk/~gp351/infinitesimals.pdf and I would like to…
Theo Deep
  • 666
  • 4
  • 15
0
votes
1 answer

dReal SMT solver counterexamples

Does the dReal SMT solver return counterexamples? I have seen examples where :produce-models is true, but I do not know how to generate counterexamples. Also, the dReach tool has a --visualize option, so it would seem that dReal would need to…
Mike Whalen
  • 33
  • 4