From cfe3ec2c213189d98652ef7bcc357896a841d05a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 10 May 2024 11:44:26 +0200 Subject: [PATCH] fix(FPA): Separate semantic triggers upon trigger construction Currently, the theories are responsible for populating the `semantic` field of triggers when a lemma with semantic triggers is added to the theory (call to `assume_th_elt`). This means that such a lemma lives for some time *without* semantic triggers: in particular, it is initially created using `mk_forall` without semantic triggers. During that call, the guard in `find_particular_subst` preventing the "particular substitution" optimization from triggering for lemmas with semantic trigger is ignored; which means that the "particular substitution" optimization is actually applied to lemmas with semantic triggers. In particular, this optimization makes the lemma `float_of_pos_pow_of_two` in the FPA theory unsound, because it removes the check that `x` is actually a power of two, and causes #1111. This patch makes the `Expr` module responsible for separating syntaxic and semantic triggers, rather than the theory. This ensures that a lemma with semantic triggers never appears as having no semantic triggers. In order to make sure this invariant is properly maintained, the `trigger` type is again made private to the `Expr` module. This required moving from sorting code from the `Matching` module to the `Expr` module, also ensuring that triggers are properly sorted for matching purposes at all times. Fixes #1111 --- src/lib/frontend/cnf.ml | 8 +- src/lib/frontend/d_cnf.ml | 9 +- src/lib/reasoners/intervalCalculus.ml | 50 +---- src/lib/reasoners/matching.ml | 18 +- src/lib/structures/expr.ml | 79 ++++--- src/lib/structures/expr.mli | 5 +- tests/dune.inc | 294 +++++++++++++++++++++++++- tests/issues/1111.ae | 4 + tests/issues/1111.expected | 0 9 files changed, 360 insertions(+), 107 deletions(-) create mode 100644 tests/issues/1111.ae create mode 100644 tests/issues/1111.expected diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 4720e046e3..54dc4d9e07 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -177,15 +177,9 @@ let rec make_term quant_basename t = and make_trigger ~in_theory name quant_basename hyp (e, from_user) = let content = List.map (make_term quant_basename) e in - let t_depth = - List.fold_left (fun z t -> max z (E.depth t)) 0 content in (* clean trigger: remove useless terms in multi-triggers after inlining of lets*) - let trigger = - { E.content ; t_depth; semantic = []; (* will be set by theories *) - hyp; from_user; - } - in + let trigger = E.mk_trigger ~user:from_user ~hyp content in E.clean_trigger ~in_theory name trigger and make_form name_base ~toplevel f loc ~decl_kind : E.t = diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 7de1379313..a4035f1203 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1655,14 +1655,11 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind mk_expr ~loc ~name_base ~decl_kind in let content = List.map mk_expr e in - let t_depth = - List.fold_left (fun z t -> max z (E.depth t)) 0 content in (* clean trigger: remove useless terms in multi-triggers after inlining of lets*) - let trigger = - { E.content; t_depth; semantic = []; (* will be set by theories *) - hyp; from_user; } - in + let trigger = E.mk_trigger ~user:from_user ~hyp content in + if not in_theory && not (Lists.is_empty trigger.semantic) then + Errors.typing_error ThSemTriggerError loc; E.clean_trigger ~in_theory name trigger (** Preprocesses the body of a goal by: diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index ac25097a0f..fb9cfa7654 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -2481,48 +2481,6 @@ let instantiate ~do_syntactic_matching match_terms env uf selector = env, insts -let separate_semantic_triggers = - fun th_form -> - let { E.user_trs; _ } as q = - match E.form_view th_form with - | E.Lemma q -> q - | E.Unit _ | E.Clause _ | E.Literal _ | E.Skolem _ - | E.Let _ | E.Iff _ | E.Xor _ -> assert false - in - let r_triggers = - List.rev_map - (fun tr -> - (* because sem-triggers will be set by theories *) - assert (tr.E.semantic == []); - let syn, sem = - List.fold_left - (fun (syn, sem) t -> - match E.term_view t with - | { E.f = Symbols.In (lb, ub); xs = [x]; _ } -> - syn, (E.Interval (x, lb, ub)) :: sem - - | { E.f = Symbols.MapsTo x; xs = [t]; _ } -> - syn, (E.MapsTo (x, t)) :: sem - - | { E.f = Sy.Op Not_theory_constant; xs = [x]; _ } -> - syn, (E.NotTheoryConst x) :: sem - - | { E.f = Sy.Op Is_theory_constant; xs = [x]; _ } -> - syn, (E.IsTheoryConst x) :: sem - - | { E.f = Sy.Op Linear_dependency; xs = [x;y]; _ } -> - syn, (E.LinearDependency(x,y)) :: sem - - | _ -> t::syn, sem - )([], []) (List.rev tr.E.content) - in - {tr with E.content = syn; semantic = sem} - )user_trs - in - E.mk_forall - q.E.name q.E.loc q.E.binders (List.rev r_triggers) q.E.main - ~toplevel:true ~decl_kind:E.Dtheory - let assume_th_elt t th_elt dep = let { Expr.axiom_kind; ax_form; th_name; extends; _ } = th_elt in let kd_str = @@ -2530,15 +2488,13 @@ let assume_th_elt t th_elt dep = in match extends with | Util.NIA | Util.NRA | Util.FPA | Util.RIA -> - let th_form = separate_semantic_triggers ax_form in - let th_elt = {th_elt with Expr.ax_form} in if get_debug_fpa () >= 2 then Printer.print_dbg ~module_name:"IntervalCalculus" ~function_name:"assume_th_elt" "[Theory %s][%s] %a" - th_name kd_str E.print th_form; - assert (not (ME.mem th_form t.th_axioms)); - {t with th_axioms = ME.add th_form (th_elt, dep) t.th_axioms} + th_name kd_str E.print ax_form; + assert (not (ME.mem ax_form t.th_axioms)); + {t with th_axioms = ME.add ax_form (th_elt, dep) t.th_axioms} | _ -> t diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index 798a56ce65..2441240da1 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -482,19 +482,10 @@ module Make (X : Arg) : S with type theory = X.t = struct Debug.match_pats_modulo pat lsubsts; List.fold_left (match_one_pat mconf env tbox pat) [] lsubsts - let pat_weight s t = - let sf = (Expr.term_view s).f in - let tf = (Expr.term_view t).f in - match sf, tf with - | Symbols.Name _, Symbols.Op _ -> -1 - | Symbols.Op _, Symbols.Name _ -> 1 - | _ -> Expr.(depth t - depth s) - let matching mconf env tbox pat_info = let open Matching_types in let pats = pat_info.trigger in let pats_list = pats.E.content in - Options.heavy_assert (fun () -> Lists.is_sorted pat_weight pats_list); Debug.matching pats; if List.length pats_list > Options.get_max_multi_triggers_size () then pat_info, [] @@ -610,21 +601,16 @@ module Make (X : Arg) : S with type theory = X.t = struct module HE = Hashtbl.Make (E) - let sort_pats tr = - let content = List.stable_sort pat_weight tr.E.content in - { tr with content } - let triggers_of, clear_triggers_of_trs_tbl = let trs_tbl = HEI.create 101 in let triggers_of q mconf = match q.E.user_trs with - | _::_ as l -> List.map sort_pats l + | _::_ as l -> l | [] -> try HEI.find trs_tbl (q.E.main, mconf) with Not_found -> let trs = E.make_triggers q.E.main q.E.binders q.E.kind mconf - |> List.map sort_pats in HEI.add trs_tbl (q.E.main, mconf) trs; trs @@ -641,7 +627,6 @@ module Make (X : Arg) : S with type theory = X.t = struct with Not_found -> let trs = E.resolution_triggers ~is_back:true q - |> List.map sort_pats in HE.add trs_tbl q.E.main trs; trs @@ -658,7 +643,6 @@ module Make (X : Arg) : S with type theory = X.t = struct with Not_found -> let trs = E.resolution_triggers ~is_back:false q - |> List.map sort_pats in HE.add trs_tbl q.E.main trs; trs diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index ca04c910b8..c19347c4ad 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -95,8 +95,6 @@ and semantic_trigger = and trigger = { content : t list; - (* this field is filled (with a part of 'content' field) by theories - when assume_th_elt is called *) semantic : semantic_trigger list; hyp : t list; t_depth : int; @@ -843,6 +841,50 @@ let is_ite s = match s with | Sy.Op Sy.Tite -> true | _ -> false +let pat_weight s t = + let sf = (term_view s).f in + let tf = (term_view t).f in + match sf, tf with + | Symbols.Name _, Symbols.Op _ -> -1 + | Symbols.Op _, Symbols.Name _ -> 1 + | _ -> depth t - depth s + +let separate_semantic_triggers content = + let syn, sem = + List.fold_left + (fun (syn, sem) t -> + match term_view t with + | { f = Symbols.In (lb, ub); xs = [x]; _ } -> + syn, (Interval (x, lb, ub)) :: sem + + | { f = Symbols.MapsTo x; xs = [t]; _ } -> + syn, (MapsTo (x, t)) :: sem + + | { f = Sy.Op Not_theory_constant; xs = [x]; _ } -> + syn, (NotTheoryConst x) :: sem + + | { f = Sy.Op Is_theory_constant; xs = [x]; _ } -> + syn, (IsTheoryConst x) :: sem + + | { f = Sy.Op Linear_dependency; xs = [x;y]; _ } -> + syn, (LinearDependency(x,y)) :: sem + + | _ -> t::syn, sem + )([], []) (List.rev content) + in + syn, sem + +let mk_trigger ?user:(from_user = false) ?depth ?(hyp = []) content = + let t_depth = + match depth with + | Some t_depth -> t_depth + | None -> + List.fold_left (fun z t -> max z t.depth) 0 content + in + let content = List.stable_sort pat_weight content in + let content, semantic = separate_semantic_triggers content in + { content ; semantic ; hyp ; t_depth ; from_user } + let mk_term s l ty = assert (match s with Sy.Lit _ | Sy.Form _ -> false | _ -> true); let d = match l with @@ -1375,9 +1417,11 @@ let rec apply_subst_aux (s_t, s_ty) t = and apply_subst_trigger subst ({ content; _ } as tr) = {tr with - content = List.map (apply_subst_aux subst) content; - (* semantic_trigger = done on theory side *) - (* hyp = done on theory side *) + content = + List.rev_map (apply_subst_aux subst) content |> + List.stable_sort pat_weight + (* semantic_trigger = done on theory side *) + (* hyp = done on theory side *) } (* *1* We should never subst formulas inside termes. We could allow to @@ -1643,12 +1687,7 @@ let resolution_triggers ~is_back { kind; main = f; binders; _ } = | Dpredicate t | Dfunction t -> if type_info t != Ty.Tbool then [] else - [ { content = [t]; - hyp = []; - semantic = []; - t_depth = t.depth; - from_user = false; - } ] + [ mk_trigger ~depth:t.depth [t] ] | Dtheory | Dobjective -> [] | Daxiom | Dgoal -> @@ -1664,12 +1703,7 @@ let resolution_triggers ~is_back { kind; main = f; binders; _ } = TSet.exists (cand_is_more_general t) others then acc else - { content = [t]; - hyp = []; - semantic = []; - t_depth = t.depth; - from_user = false; - } :: acc + mk_trigger ~depth:t.depth [t] ::acc )cand [] let free_type_vars_as_types e = @@ -2212,6 +2246,7 @@ module Triggers = struct if sz_l = sz_s then trig else let content = TMap.fold (fun t _ acc -> t :: acc) res [] in + let content = List.stable_sort pat_weight content in if Options.get_verbose () then Printer.print_dbg ~module_name:"Cnf" ~function_name:"clean_trigger" @@ -2258,15 +2293,7 @@ module Triggers = struct aux vars (STRS.empty, Var.Map.empty) e let triggers_of_list l = - List.map - (fun content -> - { content; - semantic = []; - hyp = []; - from_user = false; - t_depth = List.fold_left (fun z t -> max z (depth t)) 0 content - } - ) l + List.map mk_trigger l (* Should return false iff lit_view fails with Failure _, but this version does not build the literal view. *) diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index 5a7526ca17..e5299c81db 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -91,10 +91,8 @@ and semantic_trigger = | IsTheoryConst of t | LinearDependency of t * t -and trigger = (*private*) { +and trigger = private { content : t list; - (* this field is filled (with a part of 'content' field) by theories - when assume_th_elt is called *) semantic : semantic_trigger list; hyp : t list; t_depth : int; @@ -192,6 +190,7 @@ val print_tagged_classes : Format.formatter -> Set.t list -> unit (** smart constructors for terms *) +val mk_trigger : ?user:bool -> ?depth:int -> ?hyp:t list -> t list -> trigger val mk_term : Symbols.t -> t list -> Ty.t -> t val vrai : t val faux : t diff --git a/tests/dune.inc b/tests/dune.inc index 3e6b147edf..5e4c0a5aae 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 1111_optimize.output) + (deps (:input 1111.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 1111_optimize.output) + (alias runtest) + (package alt-ergo) + (action + (diff 1111.expected 1111_optimize.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 (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps 1111_ci_cdcl_no_minimal_bj.output) + (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 (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 1111_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (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 (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 1111_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (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 (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 1111_ci_no_tableaux_cdcl_in_instantiation.output) + (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 (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 1111_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (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 (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps 1111_ci_tableaux_cdcl_no_minimal_bj.output) + (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 (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps 1111_cdcl.output) + (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 (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps 1111_tableaux_cdcl.output) + (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 (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps 1111_tableaux.output) + (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 (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) + (rule + (deps 1111_legacy.output) + (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 (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps 1111_dolmen.output) + (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 (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (deps 1111_fpa.output) + (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 0000000000..4b0104bb0e --- /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 0000000000..e69de29bb2