dReal: An SMT Solver for Nonlinear Theories over the Reals^*

Sicun Gao, Soonho Kong, and Edmund M. Clarke

Abstract. We describe the open-source tool dReal, an SMT solver for nonlinear formulas over the reals. The tool can handle various nonlinear real functions such as polynomials, trigonometric functions, exponential functions, etc. dReal implements the framework of -complete decision procedures: It returns either unsat or -sat on input formulas, where is a numerical error bound specified by the user. dReal also produces certificates of correctness for both -sat (a solution) and unsat answers (a proof of unsatisfiability).

^*This research was sponsored by the National Science Foundation grants no. DMS1068829, no. CNS0926181 and no. CNS0931985, the GSRC under contract no. 1041377, the Semiconductor Research Corporation under contract no. 2005TJ1366, and the Office of Naval Research under award no. N000141010188.

LNAI 7898, p. 208 ff.

Full article in PDF | BibTeX

lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013