From af77783ecb09a45bf3ca21990983a2792d1c5e43 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 30 Apr 2024 03:39:34 +0200
Subject: [PATCH 1/6] Fix issue 1099

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.
---
 src/lib/frontend/d_cnf.ml  |   4 +-
 tests/dune.inc             | 272 ++++++++++++++++++++++++++++++++++++-
 tests/issues/1099.ae       |   8 ++
 tests/issues/1099.expected |   2 +
 4 files changed, 283 insertions(+), 3 deletions(-)
 create mode 100644 tests/issues/1099.ae
 create mode 100644 tests/issues/1099.expected

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 516e99f48..df7320068 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -1473,7 +1473,7 @@ let rec mk_expr
 
       | Binder ((Forall (tyvl, tvl) | Exists (tyvl, tvl)) as e, body) ->
         if tvl == []
-        then (Cache.store_tyvl tyvl; aux_mk_expr ~toplevel body)
+        then (Cache.store_tyvl tyvl; aux_mk_expr ~toplevel:false body)
         else
           let name =
             if !name_tag = 0 then name_base
@@ -1518,7 +1518,7 @@ let rec mk_expr
             end
           in
           let in_theory = decl_kind == E.Dtheory in
-          let f = aux_mk_expr ~toplevel body in
+          let f = aux_mk_expr ~toplevel:false body in
           let qbody = E.purify_form f in
           (*  All the triggers that are encoutered at this level are assumed
               to be user-defined. *)
diff --git a/tests/dune.inc b/tests/dune.inc
index 88dec1477..e40934009 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -180084,7 +180084,277 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff 1111.expected 1111_fpa.output))))
+       (diff 1111.expected 1111_fpa.output)))
+  (rule
+   (target 1099_ci_cdcl_no_minimal_bj.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps 1099_ci_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 1099_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps 1099_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output)))
+  (rule
+   (target 1099_ci_no_tableaux_cdcl_in_instantiation.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-instantiation
+             %{input})))))))
+  (rule
+   (deps 1099_ci_no_tableaux_cdcl_in_instantiation.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_no_tableaux_cdcl_in_instantiation.output)))
+  (rule
+   (target 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-tableaux-cdcl-in-theories
+             %{input})))))))
+  (rule
+   (deps 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output)))
+  (rule
+   (target 1099_ci_tableaux_cdcl_no_minimal_bj.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL-Tableaux
+             --no-minimal-bj
+             %{input})))))))
+  (rule
+   (deps 1099_ci_tableaux_cdcl_no_minimal_bj.output)
+    (alias runtest-ci)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_ci_tableaux_cdcl_no_minimal_bj.output)))
+  (rule
+   (target 1099_cdcl.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver CDCL
+             %{input})))))))
+  (rule
+   (deps 1099_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_cdcl.output)))
+  (rule
+   (target 1099_tableaux_cdcl.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux-CDCL
+             %{input})))))))
+  (rule
+   (deps 1099_tableaux_cdcl.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_tableaux_cdcl.output)))
+  (rule
+   (target 1099_tableaux.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (deps 1099_tableaux.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_tableaux.output)))
+  (rule
+   (target 1099_legacy.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend legacy
+             %{input})))))))
+  (rule
+   (deps 1099_legacy.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_legacy.output)))
+  (rule
+   (target 1099_dolmen.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps 1099_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_dolmen.output)))
+  (rule
+   (target 1099_fpa.output)
+   (deps (:input 1099.ae))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --enable-theories fpa
+             %{input})))))))
+  (rule
+   (deps 1099_fpa.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff 1099.expected 1099_fpa.output))))
 ; Auto-generated part end
 ; File auto-generated by gentests
 
diff --git a/tests/issues/1099.ae b/tests/issues/1099.ae
new file mode 100644
index 000000000..f68308d02
--- /dev/null
+++ b/tests/issues/1099.ae
@@ -0,0 +1,8 @@
+type 'a t
+logic p : 'a t, unit -> prop
+logic f : 'a t -> prop
+logic r : unit t
+
+axiom a : forall s:'a t. exists n:unit. p(s, n)
+
+goal g : f(r)
diff --git a/tests/issues/1099.expected b/tests/issues/1099.expected
new file mode 100644
index 000000000..a6e005255
--- /dev/null
+++ b/tests/issues/1099.expected
@@ -0,0 +1,2 @@
+
+unknown

From 90d0ff8cf0e26b0d6e9842ab83f0abaf87a94823 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 2 May 2024 14:21:50 +0200
Subject: [PATCH 2/6] Attempt to fix regressions

---
 src/lib/frontend/d_cnf.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index df7320068..8d94389f6 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -1473,7 +1473,7 @@ let rec mk_expr
 
       | Binder ((Forall (tyvl, tvl) | Exists (tyvl, tvl)) as e, body) ->
         if tvl == []
-        then (Cache.store_tyvl tyvl; aux_mk_expr ~toplevel:false body)
+        then (Cache.store_tyvl tyvl; aux_mk_expr ~toplevel body)
         else
           let name =
             if !name_tag = 0 then name_base

From de37c066c011fc3872b732ac51ffd50ba6bfb46f Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Fri, 3 May 2024 15:54:44 +0200
Subject: [PATCH 3/6] Enforce prenex polymorphism

Alt-Ergo only supports prenex polymorphism. This commit
adds a failwith clause in `D_cnf` to enforce this property.
---
 src/lib/frontend/d_cnf.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 8d94389f6..fe1fff77c 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -1472,8 +1472,14 @@ let rec mk_expr
         ) body binders
 
       | Binder ((Forall (tyvl, tvl) | Exists (tyvl, tvl)) as e, body) ->
-        if tvl == []
-        then (Cache.store_tyvl tyvl; aux_mk_expr ~toplevel body)
+        if not toplevel && tyvl != [] then
+          Fmt.failwith "Non-prenex polymorphism in the term %a"
+            DE.Term.print term
+        else if tvl == []
+        then begin
+          Cache.store_tyvl tyvl;
+          aux_mk_expr ~toplevel:true body
+        end
         else
           let name =
             if !name_tag = 0 then name_base

From 2d823b59a3536727f18f35c8107d607f32a391a5 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 13:16:10 +0200
Subject: [PATCH 4/6] Clarify the meaning of top level in quantified type

---
 src/lib/structures/expr.mli | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index c9b6e1d60..ed4be0ea7 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -72,7 +72,25 @@ and quantified = private {
   (** The underlying formula. *)
 
   toplevel : bool;
-  (** Determine if the quantified formula is at the top level.
+  (** 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.
+
       This flag is important for the prenex polymorphism.
       - If this flag is [true], all the free type variables of [main]
         are implicitely considered as quantified.

From 45174bfc6584744156280270ca2e55f1ee901439 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 17:22:47 +0200
Subject: [PATCH 5/6] Clarify the documentation

---
 src/lib/structures/expr.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index ed4be0ea7..10c2b293b 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -79,8 +79,7 @@ and quantified = private {
       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.
+      a subformula of another quantified formula.
 
       For instance, the subformula ∀y:int. ¬G(y) of the asserted formula
       ¬(∀y:int. ¬G(y)) is also considered at the top level.

From ca3d3d1ffd1b2fd1c8b7a7057cfe5718678d7df6 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 17:23:57 +0200
Subject: [PATCH 6/6] Poetry

---
 src/lib/structures/expr.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index 10c2b293b..4922692f9 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -75,8 +75,8 @@ and quantified = private {
   (** 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 ...)}.
+      An {e asserted formula} is a formula introduced by [(assert ...)] or
+      generated by a function definition with [(define-fun ...)].
 
       By {e top level}, we mean that the quantified formula is not
       a subformula of another quantified formula.