search

dreal / dreal4

Automated Reasoning in Nonlinear Theories of Reals
https://dreal.github.io
Apache License 2.0
151 stars 32 forks source link

Questions regarding the API #303

Closed juliusbrehme closed 1 year ago

juliusbrehme commented 1 year ago

Hello everyone,

I am trying to integrate the dReal4 SMT solver into the JavaSMT API and I have a few questions regarding the dReal4 API.

First of all I would like to know if floating points are supported in dReal. Furthermore, is there an existential quantifier? I have seen, that it is possible to use forall(const Variable& vars, const Formula&) to get a formula quantified by variables vars. Is there something like that for an existential quantifier as well, so that it is possible to use in nested formulas as well?

Finally I would like to know if there is a function that expects a string in smt-lib2 format and outputs a formula. Also is there a function, that expects a formula and outputs a string in smt-lib2 format?

Thanks in advance.

juliusbrehme commented 1 year ago

The Type of a Variable can be CONTINUOUS. Is that a floating point or a real?

soonhokong commented 1 year ago

Hi @juliusbrehme ,

First of all I would like to know if floating points are supported in dReal.

We use floating points to represent Real numbers. dReal only supports NRA and NRIA theories, not FP theory.

Furthermore, is there an existential quantifier? I have seen, that it is possible to use forall(const Variable& vars, const Formula&) to get a formula quantified by variables vars. Is there something like that for an existential quantifier as well, so that it is possible to use in nested formulas as well?

No. We allow at most one level of quantifier alternation. So everything should either a 'exists' formula or 'exists-forall' formula.

Finally I would like to know if there is a function that expects a string in smt-lib2 format and outputs a formula. Also is there a function, that expects a formula and outputs a string in smt-lib2 format?

Not exactly. But we do have https://github.com/dreal/dreal4/blob/master/dreal/symbolic/test/prefix_printer_test.cc .

The Type of a Variable can be CONTINUOUS. Is that a floating point or a real?

Real.