From 1be1c40a32404c4c5673642acda84956ba4d3ff8 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 30 Apr 2024 03:39:34 +0200 Subject: [PATCH] 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 | 294 ++++++++++++++++++++++++++++++++++++- tests/issues/1099.ae | 8 + tests/issues/1099.expected | 2 + 4 files changed, 305 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 7448d199e7..c6ecc3dd84 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 @@ -1520,7 +1520,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 3e6b147edf..6fd1f902ce 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -194422,7 +194422,299 @@ (alias runtest-quick) (package alt-ergo) (action - (diff 340.expected 340_fpa.output)))) + (diff 340.expected 340_fpa.output))) + (rule + (target 1099_optimize.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 + --optimize + %{input}))))))) + (rule + (deps 1099_optimize.output) + (alias runtest) + (package alt-ergo) + (action + (diff 1099.expected 1099_optimize.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 0000000000..f68308d026 --- /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 0000000000..a6e005255c --- /dev/null +++ b/tests/issues/1099.expected @@ -0,0 +1,2 @@ + +unknown