False unsat in forall problem

[cgd8d]

The following problem reports unsat:

(set-logic QF_NRA)
(set-info :precision 0.001)

(declare-fun x () Real [-10, 10])
(declare-fun forall y () Real [-10, 10])
(assert (
    forall (
        (y Real)
    )
    (not (and (>= y 0) (>= x 0)))
))
(check-sat)
(exit)

This problem should be satisfied by any negative x, so I believe reporting unsat is incorrect. A proof file is generated, but empty.

[soonhokong]

@cgd8d, thanks for the report. This and #243 are related issues.

For now, the support for exist-forall problems is still in its experimental stage. Given a ∃x.∀y.f(x,y) where f(x, y) is an arbitrary quantifier-free first-order logic formula, we ask users to do the pre-processing to NNF/CNF-ize f(x, y) into ∧∨ g_(i,j)(x, y), and then re-write the initial problem ∃x.∀y.f(x,y) into ∃x.∧∀y.∨g_(i,j)(x,y). This is the most general syntactic form that the current implementation of dReal can handle.

Of course, the future plan is to do this preprocessing internally. However, for now, users are responsible for doing this.

[soonhokong]

In this particular example, try the following pre-processed problem:

(set-logic QF_NRA)
(set-info :precision 0.001)
(declare-fun x () Real [-10, 10])
(declare-fun forall y () Real [-10, 10])
(assert (forall ((y Real))
                (or (< y 0) (< x 0))))
(check-sat)
(exit)

It should give you the expected delta-sat result.

[cgd8d]

Yep, that works -- thanks for your explanation!