From 6130ccbeb00352931e46ad35fc4599fc8255e3de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Mon, 13 May 2024 15:07:08 +0200 Subject: [PATCH] fix(FPA): Do not look for particular substitution in theories (#1122) Simpler version of the fix from #1113 for the 2.5.x release branch. --- src/lib/frontend/d_cnf.ml | 2 + src/lib/structures/expr.ml | 8 +- tests/dune.inc | 254 ++++++++++++++++++++++++++++++++++++- tests/issues/1111.ae | 4 + tests/issues/1111.expected | 2 + 5 files changed, 266 insertions(+), 4 deletions(-) create mode 100644 tests/issues/1111.ae create mode 100644 tests/issues/1111.expected diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index c63843a78..bc7554323 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1065,6 +1065,8 @@ let rec mk_expr "main" term of the interval. For instance, [e in [i, ?]] becomes `semantic_trigger (let x = e in i ≤ x)`. *) + if decl_kind != E.Dtheory then + Errors.typing_error ThSemTriggerError loc; let xs, trigger = Option.value ~default:([], trigger) @@ destruct_let trigger in diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 53adde375..d10d7505a 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1437,7 +1437,7 @@ and mk_forall_bis (q : quantified) = if SMap.is_empty binders && Ty.Svty.is_empty q.main.vty then q.main else let q = {q with binders} in - match find_particular_subst binders q.user_trs q.main with + match find_particular_subst q.kind binders q.user_trs q.main with | None -> mk_forall_ter q | Some sbs -> @@ -1476,8 +1476,10 @@ and find_particular_subst = | _ -> () in - fun binders trs f -> - if not (Ty.Svty.is_empty f.vty) || has_hypotheses trs || + fun decl_kind binders trs f -> + (* https://github.com/OCamlPro/alt-ergo/issues/1111 *) + let in_theory = decl_kind == Dtheory in + if in_theory || not (Ty.Svty.is_empty f.vty) || has_hypotheses trs || has_semantic_triggers trs then None diff --git a/tests/dune.inc b/tests/dune.inc index c794bd6e6..6ef64891f 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -172983,7 +172983,259 @@ (alias runtest-quick) (package alt-ergo) (action - (diff 340.expected 340_fpa.output)))) + (diff 340.expected 340_fpa.output))) + (rule + (target 1111_ci_cdcl_no_minimal_bj.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1111.expected 1111_ci_cdcl_no_minimal_bj.output))) + (rule + (target 1111_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff + 1111.expected + 1111_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 1111_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff + 1111.expected + 1111_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 1111_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1111.expected 1111_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target 1111_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff + 1111.expected + 1111_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target 1111_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff 1111.expected 1111_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target 1111_cdcl.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver CDCL + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1111.expected 1111_cdcl.output))) + (rule + (target 1111_tableaux_cdcl.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1111.expected 1111_tableaux_cdcl.output))) + (rule + (target 1111_tableaux.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend dolmen + --timelimit=2 + --sat-solver Tableaux + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1111.expected 1111_tableaux.output))) + (rule + (target 1111_legacy.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --frontend legacy + --timelimit=2 + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1111.expected 1111_legacy.output))) + (rule + (target 1111_dolmen.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --timelimit=2 + --frontend dolmen + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1111.expected 1111_dolmen.output))) + (rule + (target 1111_fpa.output) + (deps (:input 1111.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --output=smtlib2 + --timelimit=2 + --enable-theories fpa + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 1111.expected 1111_fpa.output)))) ; Auto-generated part end ; File auto-generated by gentests diff --git a/tests/issues/1111.ae b/tests/issues/1111.ae new file mode 100644 index 000000000..4b0104bb0 --- /dev/null +++ b/tests/issues/1111.ae @@ -0,0 +1,4 @@ +logic r : real + +goal g : r <> + float32(NearestTiesToEven, 12960.0087890625 * float32(NearestTiesToEven, 12960.008976179617)) diff --git a/tests/issues/1111.expected b/tests/issues/1111.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/1111.expected @@ -0,0 +1,2 @@ + +unknown