PV4 ⊧ dRealproduces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

SMT-LIB v2

Expected output

"unsat" or "$\delta$-sat"

Internals

• dReal focuses on formulas over real numbers. "Its special strength is in handling problems that involve a wide range of nonlinear real functions." (Source: https://dreal.github.io/)
• It can handle $\exists \forall$-formulas with most standard elementary, trigonometric and hyberbolic functions (e.g. power, exp, log, root, sin, cos, tan, arcsin, arccos, arctan, sinh, cosh, tanh), etc.

It uses IBEX-lib, CLP, NLopt, PicoSAT and capd