fix(FPA): Do not look for particular substitution in theories (OCamlP…

…ro#1122)

Simpler version of the fix from OCamlPro#1113 for the 2.5.x release branch.

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

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

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
 

tests/issues/1111.ae

@@ -0,0 +1,4 @@
+logic r : real
+
+goal g : r <>
+  float32(NearestTiesToEven, 12960.0087890625 * float32(NearestTiesToEven, 12960.008976179617))

tests/issues/1111.expected

@@ -0,0 +1,2 @@
+
+unknown