Fix issue 1099

[Halbaroth]

The D_cnf module didn't use the flag toplevel as it was done in Cnf. This flag is important because the Expr AST doesn't store quantified type variables with binders as it does for the term variable. Instead, we use a prenex polymorphism approach, which means the quantified type variables are at the top level only.

I believe this PR fixes the issue #1099. I'll check it on Marvin.

NB: I think this bug didn't make Alt-Ergo unsound.

[hra687261]

I think its worth adding a test with forall _: x. forall _: y. exist ... to make sure that the behavior is correct in this case as well. I am not sure but it is possible that in this case, both x and y should be seen as toplevel quantified type variables, I am also not sure if Dolmen or AE simplifies forall _: x. forall _: y. exist ... to forall _: x, _: y. exist ....

[Gbury]

Dolmen should indeed aggregate together consecutive quantifications (assuming that there are no trigger annotations in the middle).

[Halbaroth]

I think its worth adding a test with forall _: x. forall _: y. exist ... to make sure that the behavior is correct in this case as well. I am not sure but it is possible that in this case, both x and y should be seen as toplevel quantified type variables, I am also not sure if Dolmen or AE simplifies forall _: x. forall _: y. exist ... to forall _: x, _: y. exist ....

I'll check, thanks ;)

[Halbaroth]

The new fix has been tested. We got +19-0. I believe that we lost these tests with Dolmen only.

I did a mistake in the previous patch because I thought that mk_expr in D_cnf was only call on non-toplevel formulas. In fact mk_form is called on toplevel formulas and this function calls mk_expr with the toplevel flag as true.

So if you call mk_form on a polymorphic axiom, the first forall binder will only contain all the type variables but no term variables. For instance, with the following input:

type 'a t
logic c : 'a t
axiom a : forall x : int. x = x + 1 and c <> c
goal g : false

Dolmen generated the above term for the axiom a: ∀ w1 : Type. ∀ x : int. (x = (x + 1)) ∧ (Distinct ( t(w1) ) (c w1) (c w1))

I believe we should never get a non-toplevel forall binder with type variable. I added an assertion to enforce this invariant. @Gbury maybe this case can happen in SMT-LIB v3?

I will run a last test on ae-format to ensure the failwith is never raised.

[Gbury]

I don't think this should happen in smtlibv3 (but it's been a long time since I looked at its specification).

However, one of the reasons that dolmen does not enforce type quantification at top-level is that there are a few cases where solvers might be able to / want to handle a type quantification that is not at top-level (or at least, that depends on the definition of top-level). For instance:

• a formula such as not (exists a : type. ....) which could easily arise out of a negated goal
• a formula such as (forall a: type. ...) and (forall b: type. ....), and so on...

All in all, I think it's probably better to leave to solvers the task of defining which type quantifications they can handle ? But I'm open to suggestions, ^^

[Halbaroth]

I agree. We should clarify what is supposed to be a top level formula in Alt-Ergo. I think we should test this PR on psmt2 files.

[Halbaroth]

To clarify the meaning of top level in Alt-Ergo, I wrote a better commentary:

      Determine if the quantified formula is at the top level of an asserted
      formula.

      An {e asserted formula} is a formula introduced by {e (assert ...)} or
      generated by a function definition with {e (define-fun ...)}.

      By {e top level}, we mean that the quantified formula is not
      contained in another quantified formula, but the formula can be a
      subformula.

      For instance, the subformula ∀y:int. ¬G(y) of the asserted formula
      ¬(∀y:int. ¬G(y)) is also considered at the top level.

      Notice that quantifiers of the same kind are packed as much as possible.
      For instance, if we assert the formula:
        ∀α. ∀x:list α. ∃y:α. F(x, y)
      Then the two universal quantifiers are packed in a same top level formula
      but the subformula ∃y:α. F(x, y) is not at the top level.

I also tested if we can quantify types in inner formula with the psmt format. We cannot! For instance, the following assertion is refused by Dolmen:

(set-logic ALL)
(declare-sort t 1)
(declare-fun P (Int) Bool)
(assert (forall ((x Int))
  (=> (P x)
      (par (a) (forall ((x (t a)) (y (t a))) (= x y))))))
(check-sat)

So the assertion I added in D_cnf is fine. Actually, if the frontend produces a formula with inner quantified type variable, the solver is not designed to manage this kind of quantifiers and accepting to reason on a problem with such formulas in the context could be unsound. It is safer to refuse immediately to continue.