From 6c04a5e7b4a4e056a9b016f2b512376958c77dfd Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 22 Mar 2024 15:45:09 +0100 Subject: [PATCH 01/24] Model generation for ADT theory This PR implements the model generation for ADT. The model generation is done by the casesplit mechanism in `Adt_rel`. - If `--enable-adts-cs` is present, we do casesplits by choosing a delayed destructor as before after asserting. - If there is no more delayed constructors, we look for a domain which contains a tightenable constructor (that is a constructor without payload) and we choose the domain as small as possible as it does in the `Enum` theory. - If we are in model generation, we can also choose constructors with payload (but we still choose first constructors without payload). - The termination of the model generation is ensured by a topological sorting during the parsing of the ADTs declarations. --- alt-ergo-lib.opam | 1 + alt-ergo-lib.opam.locked | 1 + dune-project | 1 + shell.nix | 1 + src/lib/dune | 3 +- src/lib/frontend/d_cnf.ml | 37 ++--- src/lib/frontend/typechecker.ml | 5 + src/lib/reasoners/adt.ml | 21 ++- src/lib/reasoners/adt_rel.ml | 148 +++++++++++++---- src/lib/reasoners/fun_sat.ml | 3 +- src/lib/reasoners/satml_frontend.ml | 3 +- src/lib/reasoners/shostak.ml | 3 +- src/lib/reasoners/uf.ml | 10 +- src/lib/structures/symbols.ml | 2 +- src/lib/structures/uid.mli | 5 +- src/lib/util/nest.ml | 210 +++++++++++++++++++++++++ src/lib/util/nest.mli | 57 +++++++ tests/dune.inc | 131 +++++++++++++++ tests/models/adt/arith.models.expected | 8 + tests/models/adt/arith.models.smt2 | 18 +++ tests/models/adt/list.models.expected | 8 + tests/models/adt/list.models.smt2 | 15 ++ tests/models/adt/rec.models.expected | 5 + tests/models/adt/rec.models.smt2 | 10 ++ tests/models/adt/rec2.models.expected | 5 + tests/models/adt/rec2.models.smt2 | 10 ++ tests/models/adt/rec3.models.expected | 5 + tests/models/adt/rec3.models.smt2 | 10 ++ tests/models/adt/small.models.expected | 5 + tests/models/adt/small.models.smt2 | 11 ++ 30 files changed, 684 insertions(+), 68 deletions(-) create mode 100644 src/lib/util/nest.ml create mode 100644 src/lib/util/nest.mli create mode 100644 tests/models/adt/arith.models.expected create mode 100644 tests/models/adt/arith.models.smt2 create mode 100644 tests/models/adt/list.models.expected create mode 100644 tests/models/adt/list.models.smt2 create mode 100644 tests/models/adt/rec.models.expected create mode 100644 tests/models/adt/rec.models.smt2 create mode 100644 tests/models/adt/rec2.models.expected create mode 100644 tests/models/adt/rec2.models.smt2 create mode 100644 tests/models/adt/rec3.models.expected create mode 100644 tests/models/adt/rec3.models.smt2 create mode 100644 tests/models/adt/small.models.expected create mode 100644 tests/models/adt/small.models.smt2 diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index a2d48a46d0..ec1a1698c5 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -31,6 +31,7 @@ depends: [ "odoc" {with-doc} "ppx_deriving" "stdcompat" + "bheap" ] conflicts: [ "ppxlib" {< "0.30.0"} diff --git a/alt-ergo-lib.opam.locked b/alt-ergo-lib.opam.locked index 0def9a7a84..13d8cb1cdf 100644 --- a/alt-ergo-lib.opam.locked +++ b/alt-ergo-lib.opam.locked @@ -62,6 +62,7 @@ depends: [ "uutf" {= "1.0.3"} "yojson" {= "2.1.1"} "zarith" {= "1.13"} + "bheap" {= "2.0.0"} ] build: [ ["dune" "subst"] {dev} diff --git a/dune-project b/dune-project index 080b1bae9e..b3609a90b6 100644 --- a/dune-project +++ b/dune-project @@ -91,6 +91,7 @@ See more details on http://alt-ergo.ocamlpro.com/" (odoc :with-doc) ppx_deriving stdcompat + bheap ) (conflicts (ppxlib (< 0.30.0)) diff --git a/shell.nix b/shell.nix index 6311586340..20d6707974 100644 --- a/shell.nix +++ b/shell.nix @@ -43,5 +43,6 @@ pkgs.mkShell { stdcompat landmarks landmarks-ppx + bheap ]; } diff --git a/src/lib/dune b/src/lib/dune index 0cf1a7cb24..60e43008be 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -25,6 +25,7 @@ alt_ergo_prelude fmt stdcompat + bheap ) (preprocess (pps @@ -61,7 +62,7 @@ Emap Gc_debug Hconsing Hstring Heap Lists Loc MyUnix Numbers Uqueue Options Timers Util Vec Version Steps Printer My_zip - Theories + Theories Nest ) (js_of_ocaml diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 6f8d8c1179..9498487cb0 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -556,10 +556,11 @@ and handle_ty_app ?(update = false) ty_c l = let mk_ty_decl (ty_c: DE.ty_cst) = match DT.definition ty_c with | Some ( - Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } + Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt ) -> (* Records and adts that only have one case are treated in the same way, and considered as records. *) + Nest.add_nest [adt]; let tyvl = Cache.store_ty_vars_ret id_ty in let rev_lbs = Array.fold_left ( @@ -580,9 +581,8 @@ let mk_ty_decl (ty_c: DE.ty_cst) = let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in Cache.store_ty ty_c ty - | Some ( - (Adt { cases; _ } as _adt) - ) -> + | Some ((Adt { cases; _ } as adt)) -> + Nest.add_nest [adt]; let uid = Uid.of_dolmen ty_c in let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in let rev_cs, is_enum = @@ -594,7 +594,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) = if Array.length dstrs = 0 then true else ( - let ty = Ty.t_adt (Uid.of_dolmen ty_c) tyvl in + let ty = Ty.t_adt uid tyvl in Cache.store_ty ty_c ty; false ) @@ -681,10 +681,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = in Cache.store_ty ty_c ty - | Tadt (hs, tyl), - Some ( - Adt { cases; ty = ty_c; _ } - ) -> + | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) -> let rev_cs = Array.fold_left ( fun accl DE.{ cstr; dstrs; _ } -> @@ -714,19 +711,21 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = List.fold_left ( fun (acc, ca) ty_c -> match DT.definition ty_c with - | Some (Adt { record; cases; _ }) as df + | Some (Adt { record; cases; _ } as df) when not record && Array.length cases > 1 -> df :: acc, true - | df -> df :: acc, ca + | Some (Adt _ as df) -> + df :: acc, ca + | Some Abstract | None -> + assert false ) ([], false) tdl in + Nest.add_nest rev_tdefs; let rev_l = List.fold_left ( fun acc tdef -> match tdef with - | Some ( - (DE.Adt { cases; record; ty = ty_c; }) as adt - ) -> + | DE.Adt { cases; record; ty = ty_c; } as adt -> let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in let cns, is_enum = @@ -737,7 +736,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = ) cases ([], true) in let uid = Uid.of_dolmen ty_c in - if is_enum + if is_enum && not contains_adts then ( let ty = Ty.tsum uid cns in Cache.store_ty ty_c ty; @@ -754,8 +753,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = Cache.store_ty ty_c ty; (ty, Some adt) :: acc ) - | None - | Some Abstract -> + | Abstract -> assert false (* unreachable in the second iteration *) ) [] (List.rev rev_tdefs) in @@ -979,8 +977,7 @@ let rec mk_expr | B.Constructor _ -> let ty = dty_to_ty term_ty in - let sy = Sy.Op (Sy.Constr (Uid.of_dolmen tcst)) in - E.mk_term sy [] ty + E.mk_constr (Uid.of_dolmen tcst) [] ty | _ -> unsupported "Constant term %a" DE.Term.print term end @@ -1349,7 +1346,7 @@ let rec mk_expr let ty = dty_to_ty term_ty in begin match ty with | Ty.Tadt (_, _) -> - let sy = Sy.Op (Sy.Constr (Uid.of_dolmen tcst)) in + let sy = Sy.constr @@ Uid.of_dolmen tcst in let l = List.map (fun t -> aux_mk_expr t) args in E.mk_term sy l ty | Ty.Trecord _ -> diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 7056b933da..8f4747c46f 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -2567,6 +2567,11 @@ let rec type_decl (acc, env) d assertion_stack = | TypeDecl l -> let not_rec, are_rec = partition_non_rec l in + let not_rec, are_rec = + if Lists.is_empty are_rec then not_rec, are_rec + else [], List.rev_append not_rec are_rec + in + (* A. Typing types that are not recursive *) let acc, env = List.fold_left diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 5e7b64b537..5fab09d5e4 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -401,12 +401,17 @@ module Shostak (X : ALIEN) = struct let assign_value _ _ _ = - Printer.print_err - "[ADTs.models] assign_value currently not implemented"; - raise (Util.Not_implemented "Models for ADTs") - - let to_model_term _r = - Printer.print_err - "[ADTs.models] to_model_term currently not implemented"; - raise (Util.Not_implemented "Models for ADTs") + (* Model generation is performed by the casesplit mechanism + in [Adt_rel]. *) + None + + let to_model_term r = + match embed r with + | Constr { c_name; c_ty; c_args } -> + let args = Lists.try_map (fun (_, arg) -> X.to_model_term arg) c_args in + Option.bind args @@ fun args -> + Some (E.mk_constr c_name args c_ty) + + | Select _ -> None + | Alien a -> X.to_model_term a end diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index c2a04e390d..f242c07965 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -36,6 +36,15 @@ module LR = Uf.LX module Th = Shostak.Adt module SLR = Set.Make(LR) +module TSet = Set.Make + (struct + type t = Uid.t + + (* We use a dedicated total order on the constructor to ensure + the termination of the model generation. *) + let compare = Nest.compare + end) + let timer = Timers.M_Adt module Domain = struct @@ -43,27 +52,37 @@ module Domain = struct assigned to the semantic value has to use a constructor lying in the domain. *) type t = { - constrs : Uid.Set.t; + constrs : TSet.t; + (* The constructors are sorted by the module [Topological_order] + in order to ensure the termination of the model generation. *) + ex : Ex.t; } exception Inconsistent of Ex.t + let[@inline always] cardinal { constrs; _ } = TSet.cardinal constrs + + let[@inline always] choose { constrs; _ } = + (* We choose the minimal element to ensure the termination of + model generation. *) + TSet.min_elt constrs + let[@inline always] as_singleton { constrs; ex } = - if Uid.Set.cardinal constrs = 1 then - Some (Uid.Set.choose constrs, ex) + if TSet.cardinal constrs = 1 then + Some (TSet.choose constrs, ex) else None let domain ~constrs ex = - if Uid.Set.is_empty constrs then + if TSet.is_empty constrs then raise @@ Inconsistent ex else { constrs; ex } - let[@inline always] singleton ~ex c = { constrs = Uid.Set.singleton c; ex } + let[@inline always] singleton ~ex c = { constrs = TSet.singleton c; ex } - let[@inline always] subset d1 d2 = Uid.Set.subset d1.constrs d2.constrs + let[@inline always] subset d1 d2 = TSet.subset d1.constrs d2.constrs let unknown ty = match ty with @@ -73,31 +92,31 @@ module Domain = struct let constrs = List.fold_left (fun acc Ty.{ constr; _ } -> - Uid.Set.add constr acc - ) Uid.Set.empty body + TSet.add constr acc + ) TSet.empty body in - assert (not @@ Uid.Set.is_empty constrs); + assert (not @@ TSet.is_empty constrs); { constrs; ex = Ex.empty } | _ -> (* Only ADT values can have a domain. This case shouldn't happen since we check the type of semantic values in both [add] and [assume]. *) assert false - let equal d1 d2 = Uid.Set.equal d1.constrs d2.constrs + let equal d1 d2 = TSet.equal d1.constrs d2.constrs let pp ppf d = Fmt.(braces @@ - iter ~sep:comma Uid.Set.iter Uid.pp) ppf d.constrs; + iter ~sep:comma TSet.iter Uid.pp) ppf d.constrs; if Options.(get_verbose () || get_unsat_core ()) then Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex let intersect ~ex d1 d2 = - let constrs = Uid.Set.inter d1.constrs d2.constrs in + let constrs = TSet.inter d1.constrs d2.constrs in let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in domain ~constrs ex let remove ~ex c d = - let constrs = Uid.Set.remove c d.constrs in + let constrs = TSet.remove c d.constrs in let ex = Ex.union ex d.ex in domain ~constrs ex end @@ -209,6 +228,8 @@ module Domains = struct ) t.changed acc in acc, { t with changed = SX.empty } + + let fold f t = MX.fold f t.domains end let calc_destructor d e uf = @@ -568,43 +589,108 @@ exception Found of X.r * Uid.t (* Pick a delayed destructor application in [env.delayed]. Returns [None] if there is no delayed destructor. *) -let pick_delayed_destructor env = +let pick_delayed_destructor env uf = + let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in try Rel_utils.Delayed.iter_delayed (fun r sy _e -> match sy with - | Sy.Destruct d -> - raise_notrace @@ Found (r, d) + | Sy.Destruct destr -> + let d = Domains.get r ds in + if Domain.cardinal d > 1 then + raise_notrace @@ Found (r, destr) + else + () | _ -> () ) env.delayed; None with Found (r, d) -> Some (r, d) +let is_enum ty c = + match ty with + | Ty.Tadt (name, params) -> + let Adt cases = Ty.type_body name params in + Lists.is_empty @@ Ty.assoc_destrs c cases + | _ -> assert false + +let pick_tightenable_domain ~for_model uf = + let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in + Domains.fold + (fun r d best -> + let rr, _ = Uf.find_r uf r in + match Th.embed rr with + | Constr _ -> + best + | _ -> + let cd = Domain.cardinal d in + let c = Domain.choose d in + if for_model || is_enum (X.type_info r) c then + match best with + | Some (n, _, _) when n <= cd -> best + | Some _ | None -> Some (cd, r, c) + else + best + ) ds None + +let can_split env n = + let m = Options.get_max_split () in + Numbers.Q.(compare (mult n env.size_splits) m) <= 0 || Numbers.Q.sign m < 0 + +let (let*) = Option.bind + (* Do a case-split by choosing a semantic value [r] and constructor [c] for which there are delayed destructor applications and propagate the literal [(not (_ is c) r)]. *) +let case_split_destructor env uf = + if not @@ Options.get_enable_adts_cs () then + None + else + let* r, d = pick_delayed_destructor env uf in + let c = constr_of_destr (X.type_info r) d in + Some (LR.mkv_builtin false (Sy.IsConstr c) [r]) + +(* Do a case-split by choosing a semantic value [r] whose the domain is as + small as possible. + + If [for_model] is [false], we consider only constructors without payload. In + particular, if [r] has no constructors without payload in its domain, we + don't case-split on it. *) +let case_split_best ~for_model env uf = + let* n, r, c = pick_tightenable_domain ~for_model uf in + let n = Numbers.Q.from_int n in + if for_model || can_split env n then + let _, cons = Option.get @@ build_constr_eq r c in + let nr, ctx = X.make cons in + assert (Lists.is_empty ctx); + Some (LR.mkv_eq r nr) + else + None + let case_split env uf ~for_model = - if Options.get_disable_adts () || not (Options.get_enable_adts_cs()) - then + if Options.get_disable_adts () then [] else begin - assert (not for_model); - if Options.get_debug_adt () then - Debug.pp_domains "before cs" - (Uf.GlobalDomains.find (module Domains) (Uf.domains uf)); - match pick_delayed_destructor env with - | Some (r, d) -> - if Options.get_debug_adt () then + let cs = + match case_split_destructor env uf with + | Some _ as cs -> + assert (not (Options.get_enable_adts_cs ()) || not for_model); + cs + | None -> case_split_best ~for_model env uf + in + match cs with + | Some cs -> + if Options.get_debug_adt () then begin + Debug.pp_domains "before cs" + (Uf.GlobalDomains.find (module Domains) (Uf.domains uf)); Printer.print_dbg ~flushed:false ~module_name:"Adt_rel" ~function_name:"case_split" - "found r = %a and d = %a@ " X.print r Uid.pp d; - (* CS on negative version would be better in general. *) - let c = constr_of_destr (X.type_info r) d in - let cs = LR.mkv_builtin false (Sy.IsConstr c) [r] in - [ cs, true, Th_util.CS (Th_util.Th_adt, two) ] + "Assume %a" (Xliteral.print_view X.print) cs; + end; + [ cs, true, Th_util.CS (Th_util.Th_adt, two)] | None -> - Debug.no_case_split (); + if Options.get_debug_adt () then + Debug.no_case_split (); [] end diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 2956b40ce0..e7b00d676f 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1885,7 +1885,8 @@ module Make (Th : Theory.S) = struct Expr.reinit_cache (); Hstring.reinit_cache (); Shostak.Combine.reinit_cache (); - Uf.reinit_cache () + Uf.reinit_cache (); + Nest.reinit () let () = Steps.save_steps (); diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index aaf94087ef..0a3ed11f7a 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1393,7 +1393,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Expr.reinit_cache (); Hstring.reinit_cache (); Shostak.Combine.reinit_cache (); - Uf.reinit_cache () + Uf.reinit_cache (); + Nest.reinit () let () = Steps.save_steps (); diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 7a97695997..898070ff53 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -440,7 +440,8 @@ struct not (Options.get_restricted ()) && (RECORDS.is_mine_symb sb ty || BITV.is_mine_symb sb ty || - ENUM.is_mine_symb sb ty) + ENUM.is_mine_symb sb ty || + ADT.is_mine_symb sb ty) let is_a_leaf r = match r.v with | Term _ | Ac _ -> true diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 69759a5a84..9b2b6f2a3a 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1163,6 +1163,10 @@ type cache = { to ensure we don't generate twice an abstract value for a given symbol. *) } +let is_destructor = function + | Sy.Op (Destruct _) -> true + | _ -> false + (* The environment of the union-find contains almost a first-order model. There are two situations that require some computations to retrieve an appropriate model value: @@ -1179,9 +1183,9 @@ let compute_concrete_model_of_val cache = and get_abstract_for = Cache.get_abstract_for cache.abstracts in fun env t ((mdl, mrepr) as acc) -> let { E.f; xs; ty; _ } = E.term_view t in - if X.is_solvable_theory_symbol f ty - || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t - || E.equal t E.vrai || E.equal t E.faux + if X.is_solvable_theory_symbol f ty || is_destructor f + || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t + || E.equal t E.vrai || E.equal t E.faux then (* These terms are built-in interpreted ones and we don't have to produce a definition for them. *) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 7c64153965..d433db81e6 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -144,7 +144,7 @@ let bitv s = | _ -> assert false) Z.zero s in Bitv (String.length s, biv) let real r = Real (Q.of_string r) -let constr s = Op (Constr s) +let constr c = Op (Constr c) let destruct s = Op (Destruct s) let mk_bound kind sort ~is_open ~is_lower = diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index 801d7bd15b..bef18656d2 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -30,7 +30,10 @@ module DE = Dolmen.Std.Expr -type t +type t = private + | Hstring : Hstring.t -> t + | Dolmen : 'a DE.id -> t + (* | Cstr : DE.term_cst DE.id -> t *) val of_dolmen : 'a DE.Id.t -> t val of_string : string -> t diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml new file mode 100644 index 0000000000..73bb040c8e --- /dev/null +++ b/src/lib/util/nest.ml @@ -0,0 +1,210 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +module DStd = Dolmen.Std +module DE = DStd.Expr +module DT = DE.Ty +module B = Dolmen.Std.Builtin +open DE + +type t = Dolmen.Std.Expr.ty_def list + +(* Recall that a (directed) hypergraph is a set of nodes and hyperedges where + hyperedges join subsets of nodes. + + To generate our total order on constructors of a same nest, we build + in the function [build_graph] a hypergraph where: + - the set of nodes is the set of all the constructors of the nest; + - for each type [ty] of the nest, we denote by S(ty) the set + of all the constructors of this type and G(ty) the set of + the constructors with an argument of type [ty]. + + Forall the type [ty] of the nest, there is a an edge from S(ty) to + G(ty). + + In particular, our graph has exactly one outgoing hyperedge per node. *) + +(* Node of the hypergraph. *) +type node = { + id : term_cst; + (* Dolmen constructor identifier. *) + + weight : int; + (* This weight is used to prioritize constructors with less destructors + during the sorting (see [add_nest]). *) + + mutable outgoing : edge; + (* Hyperedge from a subset S in S(ty) to a subset G in G(ty) where [ty] is + the type of [id]. At the beginning, we have S = S(ty) and G = G(ty). + + One use a double indirection because this hyperedge is shared between + all the elements of S. *) + + mutable in_degree : int; + (* Number of hyperedges into this constructor. *) +} + +(* Type of a hyperedge. *) +and edge = node list ref + +module Heap = struct + include Binary_heap.Make + (struct + type t = node + let compare { weight = w1; _ } { weight = w2; _ } = w1 - w2 + end) + + let create = + let dummy_edge : node list ref = ref [] in + let dummy = { + id = Term.Const.Int.int "0" (* dummy *); + outgoing = dummy_edge; + in_degree = -1; + weight = -1; + } + in + create ~dummy +end + +let (let*) = Option.bind + +(* Return the type definition of the return type of the destructor [dstr]. *) +let def_of_dstr dstr = + let* ty_cst = + match dstr with + | DE.{ builtin = B.Destructor _; id_ty; _ } -> + begin match DT.view id_ty with + | `Arrow (_, ty) -> + begin match DT.view ty with + | `App (`Generic ty_cst, _) -> Some ty_cst + | _ -> None + end + | _ -> None + end + | _ -> assert false + in + DT.definition ty_cst + +(* Build the hypergraph of dependencies between the constructors of the + nest [defs]. + + @return a heap that contains all the nodes of this graph without ingoing + hyperedges. *) +let build_graph (defs : ty_def list) : Heap.t = + let map : (ty_def, edge) Hashtbl.t = Hashtbl.create 17 in + let hp : Heap.t = Heap.create 17 in + List.iter (fun d -> Hashtbl.add map d (ref [])) defs; + List.iter + (fun def -> + match def with + | Abstract -> assert false + | Adt { cases; _ } -> + Array.iter + (fun { cstr; dstrs; _ } -> + let node = { + id = cstr; + outgoing = Hashtbl.find map def; + in_degree = -1; (* dummy value *) + weight = Array.length dstrs + } + in + let in_degree = + Array.fold_left + (fun acc2 dstr -> + let d = let* dstr in def_of_dstr dstr in + match d with + | Some d -> + begin match Hashtbl.find map d with + | used_by -> + used_by := node :: !used_by; + acc2 + 1 + | exception Not_found -> + acc2 + end + | None -> acc2 + ) 0 dstrs + in + node.in_degree <- in_degree; + if in_degree = 0 then Heap.add hp node + ) cases + ) defs; + hp + +module H = Hashtbl.Make (Uid) + +(* Internal state used to store the current order. *) +let add_cstr, find_weight, reinit = + let ctr = ref 0 in + let order : int H.t = H.create 100 in + (* add_weight *) + (fun cstr -> + H.add order cstr !ctr; + incr ctr), + (* find_weight *) + (fun cstr -> + try + H.find order cstr + with Not_found -> + Fmt.failwith "cannot find uid %a" Uid.pp cstr), + (* reinit *) + (fun () -> + ctr := 0; + H.clear order) + +(* Sort the constructors of the nest using a sorting based on the + Kahn's algorithm. *) +let add_nest n = + let hp = build_graph n in + while not @@ Heap.is_empty hp do + (* Loop invariant: the set of nodes in heap [hp] is exactly + the set of the nodes of the graph without ingoing hyperedge. *) + let { id; outgoing; in_degree; _ } = Heap.pop_minimum hp in + add_cstr @@ Uid.of_dolmen id; + assert (in_degree = 0); + outgoing := + List.filter_map + (fun node -> + assert (node.in_degree > 0); + let node = { node with in_degree = node.in_degree - 1 } in + if node.in_degree = 0 then ( + Heap.add hp node; + None + ) else ( + Some node + ) + ) !outgoing + done + +let compare (id1 : Uid.t) (id2 : Uid.t) = + match id1, id2 with + | Dolmen _, Dolmen _ -> + find_weight id1 - find_weight id2 + | _ -> + Uid.compare id1 id2 diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli new file mode 100644 index 0000000000..035184c1f0 --- /dev/null +++ b/src/lib/util/nest.mli @@ -0,0 +1,57 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +module DE = Dolmen.Std.Expr + +(** The purpose of this module is to construct a total order on ADT + constructors to ensure the termination of model generation for + this theory. + + By [nest], we mean the set of all the constructors in a mutually + recursive definition of ADTs. + + Before comparing constructors with [compare], the complete + nests to which they belong have to be added with [add_nest]. *) + +type t = DE.ty_def list +(** Type of nest. *) + +val add_nest : t -> unit +(** [add_nest defs] sorts and adds the nest [defs] in the current + internal order. + + {b Note:} Assume that [defs] is a complete nest (in any order). *) + +val compare : Uid.t -> Uid.t -> int +(** [compare id1 id2] compares the identifier [id1] and [id2] with + the order generated by [add_nest] if they are both Dolmen identifiers. *) + +val reinit : unit -> unit +(** [reinit ()] resets the internal order. *) diff --git a/tests/dune.inc b/tests/dune.inc index 70477ddb97..88dec1477f 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -194871,6 +194871,137 @@ ; Auto-generated part end ; File auto-generated by gentests +; Auto-generated part begin +(subdir models/adt + (rule + (target small.models_dolmen.output) + (deps (:input small.models.smt2)) + (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 small.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff small.models.expected small.models_dolmen.output))) + (rule + (target rec3.models_dolmen.output) + (deps (:input rec3.models.smt2)) + (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 rec3.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff rec3.models.expected rec3.models_dolmen.output))) + (rule + (target rec2.models_dolmen.output) + (deps (:input rec2.models.smt2)) + (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 rec2.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff rec2.models.expected rec2.models_dolmen.output))) + (rule + (target rec.models_dolmen.output) + (deps (:input rec.models.smt2)) + (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 rec.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff rec.models.expected rec.models_dolmen.output))) + (rule + (target list.models_dolmen.output) + (deps (:input list.models.smt2)) + (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 list.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff list.models.expected list.models_dolmen.output))) + (rule + (target arith.models_dolmen.output) + (deps (:input arith.models.smt2)) + (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 arith.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff arith.models.expected arith.models_dolmen.output)))) +; Auto-generated part end +; File auto-generated by gentests + ; Auto-generated part begin (subdir models/arith (rule diff --git a/tests/models/adt/arith.models.expected b/tests/models/adt/arith.models.expected new file mode 100644 index 0000000000..7da79872d1 --- /dev/null +++ b/tests/models/adt/arith.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun a () Data (cons1 2.0 0.0)) + (define-fun b () Data (cons3 0.0)) + (define-fun x () Real 2.0) + (define-fun y () Real 0.0) +) diff --git a/tests/models/adt/arith.models.smt2 b/tests/models/adt/arith.models.smt2 new file mode 100644 index 0000000000..e1bb697759 --- /dev/null +++ b/tests/models/adt/arith.models.smt2 @@ -0,0 +1,18 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatype Data ( + (cons1 (d1 Real) (d2 Real)) + (cons2) + (cons3 (d3 Real)) +)) +(declare-const a Data) +(declare-const b Data) +(declare-const x Real) +(declare-const y Real) +(assert ((_ is cons1) a)) +(assert ((_ is cons3) b)) +(assert (= (d1 a) x)) +(assert (= (d3 b) y)) +(assert (= (d1 a) (- 2 (d3 b)))) +(check-sat) +(get-model) diff --git a/tests/models/adt/list.models.expected b/tests/models/adt/list.models.expected new file mode 100644 index 0000000000..07eb25ebba --- /dev/null +++ b/tests/models/adt/list.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun a () List empty) + (define-fun b () List empty) + (define-fun c () List (cons 0 empty)) + (define-fun d () List empty) +) diff --git a/tests/models/adt/list.models.smt2 b/tests/models/adt/list.models.smt2 new file mode 100644 index 0000000000..33dda60ccf --- /dev/null +++ b/tests/models/adt/list.models.smt2 @@ -0,0 +1,15 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatype List ( + (empty) + (cons (head Int) (tail List)) +)) +(declare-const a List) +(declare-const b List) +(declare-const c List) +(declare-const d List) +(assert (= (tail a) b)) +(assert ((_ is cons) c)) +(assert (= (tail c) d)) +(check-sat) +(get-model) diff --git a/tests/models/adt/rec.models.expected b/tests/models/adt/rec.models.expected new file mode 100644 index 0000000000..3cac54112e --- /dev/null +++ b/tests/models/adt/rec.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () data (cons1 cons2)) +) diff --git a/tests/models/adt/rec.models.smt2 b/tests/models/adt/rec.models.smt2 new file mode 100644 index 0000000000..d724e94f5b --- /dev/null +++ b/tests/models/adt/rec.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatype data ( + (cons1 (d1 data)) + (cons2) +)) +(declare-const a data) +(assert ((_ is cons1) a)) +(check-sat) +(get-model) diff --git a/tests/models/adt/rec2.models.expected b/tests/models/adt/rec2.models.expected new file mode 100644 index 0000000000..d5a224aa49 --- /dev/null +++ b/tests/models/adt/rec2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () data1 (cons1 (cons2 cons4))) +) diff --git a/tests/models/adt/rec2.models.smt2 b/tests/models/adt/rec2.models.smt2 new file mode 100644 index 0000000000..511d9a5a83 --- /dev/null +++ b/tests/models/adt/rec2.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes ((data1 0) (data2 0)) ( + ((cons1 (d1 data1)) (cons2 (d2 data2))) + ((cons3 (d3 data1)) (cons4)) +)) +(declare-const a data1) +(assert ((_ is cons1) a)) +(check-sat) +(get-model) diff --git a/tests/models/adt/rec3.models.expected b/tests/models/adt/rec3.models.expected new file mode 100644 index 0000000000..2714125021 --- /dev/null +++ b/tests/models/adt/rec3.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () data1 (cons1 (cons2 (cons4 0 1)))) +) diff --git a/tests/models/adt/rec3.models.smt2 b/tests/models/adt/rec3.models.smt2 new file mode 100644 index 0000000000..6b23dc3f0d --- /dev/null +++ b/tests/models/adt/rec3.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes ((data1 0) (data2 0)) ( + ((cons1 (d1 data1)) (cons2 (d2 data2))) + ((cons3 (d3 data1)) (cons4 (d4 Int) (d5 Int))) +)) +(declare-const a data1) +(assert ((_ is cons1) a)) +(check-sat) +(get-model) diff --git a/tests/models/adt/small.models.expected b/tests/models/adt/small.models.expected new file mode 100644 index 0000000000..a0f6a5ba55 --- /dev/null +++ b/tests/models/adt/small.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () data1 (cons1 (cons2 (cons5 false)))) +) diff --git a/tests/models/adt/small.models.smt2 b/tests/models/adt/small.models.smt2 new file mode 100644 index 0000000000..b03dd5902a --- /dev/null +++ b/tests/models/adt/small.models.smt2 @@ -0,0 +1,11 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes ((data1 0) (data2 0)) ( + ((cons1 (d1 data1)) (cons2 (d2 data2))) + ((cons3 (d3 data1)) (cons4 (d4 Int) (d5 Int) (d6 Bool)) + (cons5 (d7 Bool))) +)) +(declare-const a data1) +(assert ((_ is cons1) a)) +(check-sat) +(get-model) From b82ccd9e22df1a0f56570f0db8313774e064ac0c Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 23 May 2024 11:37:06 +0200 Subject: [PATCH 02/24] Use the Heap of Alt-Ergo --- alt-ergo-lib.opam | 1 - alt-ergo-lib.opam.locked | 1 - dune-project | 1 - shell.nix | 1 - src/lib/dune | 1 - src/lib/frontend/typechecker.ml | 5 --- src/lib/reasoners/satml.ml | 6 +-- src/lib/util/heap.ml | 65 ++++++++++++++++++--------------- src/lib/util/heap.mli | 44 +++++++++++++++++++--- src/lib/util/nest.ml | 45 +++++++++++------------ 10 files changed, 98 insertions(+), 72 deletions(-) diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index ec1a1698c5..a2d48a46d0 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -31,7 +31,6 @@ depends: [ "odoc" {with-doc} "ppx_deriving" "stdcompat" - "bheap" ] conflicts: [ "ppxlib" {< "0.30.0"} diff --git a/alt-ergo-lib.opam.locked b/alt-ergo-lib.opam.locked index 13d8cb1cdf..0def9a7a84 100644 --- a/alt-ergo-lib.opam.locked +++ b/alt-ergo-lib.opam.locked @@ -62,7 +62,6 @@ depends: [ "uutf" {= "1.0.3"} "yojson" {= "2.1.1"} "zarith" {= "1.13"} - "bheap" {= "2.0.0"} ] build: [ ["dune" "subst"] {dev} diff --git a/dune-project b/dune-project index b3609a90b6..080b1bae9e 100644 --- a/dune-project +++ b/dune-project @@ -91,7 +91,6 @@ See more details on http://alt-ergo.ocamlpro.com/" (odoc :with-doc) ppx_deriving stdcompat - bheap ) (conflicts (ppxlib (< 0.30.0)) diff --git a/shell.nix b/shell.nix index 20d6707974..6311586340 100644 --- a/shell.nix +++ b/shell.nix @@ -43,6 +43,5 @@ pkgs.mkShell { stdcompat landmarks landmarks-ppx - bheap ]; } diff --git a/src/lib/dune b/src/lib/dune index 60e43008be..aef40ae5a6 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -25,7 +25,6 @@ alt_ergo_prelude fmt stdcompat - bheap ) (preprocess (pps diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 8f4747c46f..7056b933da 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -2567,11 +2567,6 @@ let rec type_decl (acc, env) d assertion_stack = | TypeDecl l -> let not_rec, are_rec = partition_non_rec l in - let not_rec, are_rec = - if Lists.is_empty are_rec then not_rec, are_rec - else [], List.rev_append not_rec are_rec - in - (* A. Typing types that are not recursive *) let acc, env = List.fold_left diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index c797d3ea94..0e4e2bfdbb 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -143,7 +143,7 @@ end module MFF = FF.Map module SFF = FF.Set -module Vheap = Heap.Make(struct +module Vheap = Heap.MakeRanked(struct type t = Atom.var let index (a : t) = a.hindex @@ -478,7 +478,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct simpDB_props = 0; - order = Vheap.make 0 Atom.dummy_var; (* sera mis a jour dans solve *) + order = Vheap.create 0 Atom.dummy_var; (* sera mis a jour dans solve *) progress_estimate = 0.; @@ -1827,7 +1827,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct env.next_split <- None; pick_branch_aux env atom | None -> - match Vheap.remove_min env.order with + match Vheap.pop_minimum env.order with | v -> pick_branch_aux env v.na | exception Not_found -> if Options.get_cdcl_tableaux_inst () then diff --git a/src/lib/util/heap.ml b/src/lib/util/heap.ml index 44f7f61991..c4d903afda 100644 --- a/src/lib/util/heap.ml +++ b/src/lib/util/heap.ml @@ -35,33 +35,7 @@ module type RankedType = sig val compare : t -> t -> int end -module type S = sig - type elt - - type t - - val make : int -> elt -> t - - val in_heap : elt -> bool - - val decrease : t -> elt -> unit - - val increase : t -> elt -> unit - - val size : t -> int - - val is_empty : t -> bool - - val insert : t -> elt -> unit - - val grow_to_by_double : t -> int -> unit - - val remove_min : t -> elt - - val filter : t -> (elt -> bool) -> unit -end - -module Make(Rank : RankedType) = struct +module MakeRanked(Rank : RankedType) = struct type elt = Rank.t type t = { heap : elt Vec.t } [@@unboxed] @@ -69,7 +43,7 @@ module Make(Rank : RankedType) = struct (* Negative value; used to indicate an element is not in the heap *) let absent = -1 - let make sz dummy = { heap = Vec.make ~dummy sz } + let create sz dummy = { heap = Vec.make ~dummy sz } let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *) let[@inline] right i = (i + 1) lsl 1 (* (i + 1) * 2*) @@ -148,7 +122,7 @@ module Make(Rank : RankedType) = struct let[@inline] grow_to_by_double { heap } sz = Vec.grow_to_by_double heap sz - let remove_min ({ heap } as s) = + let pop_minimum ({ heap } as s) = match Vec.size heap with | 0 -> raise Not_found | 1 -> @@ -165,3 +139,36 @@ module Make(Rank : RankedType) = struct if Vec.size s.heap > 1 then percolate_down s y; x end + +module type OrderedTypeDefault = sig + type t + + val compare : t -> t -> int + + val default : t +end + +module MakeOrdered(V : OrderedTypeDefault) = struct + type entry = { value : V.t ; mutable index : int } + type elt = V.t + + module H = MakeRanked + (struct + type t = entry + + let index e = e.index + + let set_index e i = e.index <- i + + let compare x y = V.compare x.value y.value + end) + + let entry value = { value ; index = -1 } + + type t = H.t + + let create n = H.create n (entry V.default) + let is_empty = H.is_empty + let insert h v = H.insert h (entry v) + let pop_minimum h = (H.pop_minimum h).value +end diff --git a/src/lib/util/heap.mli b/src/lib/util/heap.mli index 388db8c4c4..ab2cab51fa 100644 --- a/src/lib/util/heap.mli +++ b/src/lib/util/heap.mli @@ -62,13 +62,14 @@ end (** {2 Priority heaps} *) -module type S = sig - type elt +module MakeRanked(Rank : RankedType) : sig + type elt = Rank.t + (** The type of elements of the heap. *) type t (** The type of heaps. *) - val make : int -> elt -> t + val create : int -> elt -> t (** Create a heap with the given initial size and dummy element. *) val in_heap : elt -> bool @@ -87,13 +88,13 @@ module type S = sig (** Is the heap empty ? *) val insert : t -> elt -> unit - (** Inset a new element in the heap. *) + (** Insert a new element in the heap. *) val grow_to_by_double: t -> int -> unit (** Grow the size of the heap by multiplying it by 2 until it is at least the size specified. *) - val remove_min : t -> elt + val pop_minimum : t -> elt (** Remove the minimum element from the heap and return it. @raise Not_found if the heap is empty. *) @@ -102,4 +103,35 @@ module type S = sig (** Filter elements in the heap. *) end -module Make(Rank : RankedType) : S with type elt = Rank.t +(** {2 Ordered priority heaps} *) + +module type OrderedTypeDefault = sig + type t + + val compare : t -> t -> int + + val default : t + (** Dummy value used in the heap. *) +end + +module MakeOrdered(V : OrderedTypeDefault) : sig + type elt = V.t + (** The type of elements of the heap. *) + + type t + (** The type of heaps. *) + + val create : int -> t + (** Create a heap with the given initial size. *) + + val is_empty : t -> bool + (** Is the heap empty ? *) + + val insert : t -> elt -> unit + (** Insert a new element in the heap. *) + + val pop_minimum : t -> elt + (** Remove the minimum element from the heap and return it. + + @raise Not_found if the heap is empty. *) +end diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 73bb040c8e..a71218f0c2 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -74,24 +74,21 @@ type node = { (* Type of a hyperedge. *) and edge = node list ref -module Heap = struct - include Binary_heap.Make - (struct - type t = node - let compare { weight = w1; _ } { weight = w2; _ } = w1 - w2 - end) - - let create = - let dummy_edge : node list ref = ref [] in - let dummy = { - id = Term.Const.Int.int "0" (* dummy *); - outgoing = dummy_edge; - in_degree = -1; - weight = -1; - } - in - create ~dummy -end +module Hp = + Heap.MakeOrdered + (struct + type t = node + let compare { weight = w1; _ } { weight = w2; _ } = w1 - w2 + + let default = + let dummy_edge : node list ref = ref [] in + { + id = Term.Const.Int.int "0" (* dummy *); + outgoing = dummy_edge; + in_degree = -1; + weight = -1; + } + end) let (let*) = Option.bind @@ -117,9 +114,9 @@ let def_of_dstr dstr = @return a heap that contains all the nodes of this graph without ingoing hyperedges. *) -let build_graph (defs : ty_def list) : Heap.t = +let build_graph (defs : ty_def list) : Hp.t = let map : (ty_def, edge) Hashtbl.t = Hashtbl.create 17 in - let hp : Heap.t = Heap.create 17 in + let hp : Hp.t = Hp.create 17 in List.iter (fun d -> Hashtbl.add map d (ref [])) defs; List.iter (fun def -> @@ -152,7 +149,7 @@ let build_graph (defs : ty_def list) : Heap.t = ) 0 dstrs in node.in_degree <- in_degree; - if in_degree = 0 then Heap.add hp node + if in_degree = 0 then Hp.insert hp node ) cases ) defs; hp @@ -182,10 +179,10 @@ let add_cstr, find_weight, reinit = Kahn's algorithm. *) let add_nest n = let hp = build_graph n in - while not @@ Heap.is_empty hp do + while not @@ Hp.is_empty hp do (* Loop invariant: the set of nodes in heap [hp] is exactly the set of the nodes of the graph without ingoing hyperedge. *) - let { id; outgoing; in_degree; _ } = Heap.pop_minimum hp in + let { id; outgoing; in_degree; _ } = Hp.pop_minimum hp in add_cstr @@ Uid.of_dolmen id; assert (in_degree = 0); outgoing := @@ -194,7 +191,7 @@ let add_nest n = assert (node.in_degree > 0); let node = { node with in_degree = node.in_degree - 1 } in if node.in_degree = 0 then ( - Heap.add hp node; + Hp.insert hp node; None ) else ( Some node From 7ca41b5a82f1b3a940a0ff29cae4ad17c88ec2f1 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 23 May 2024 11:59:28 +0200 Subject: [PATCH 03/24] poetry --- src/lib/reasoners/adt_rel.ml | 5 +---- src/lib/util/nest.ml | 24 +++++++++++++----------- src/lib/util/nest.mli | 11 +++++++---- 3 files changed, 21 insertions(+), 19 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index f242c07965..ed4d1041fc 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -40,7 +40,7 @@ module TSet = Set.Make (struct type t = Uid.t - (* We use a dedicated total order on the constructor to ensure + (* We use a dedicated total order on the constructors to ensure the termination of the model generation. *) let compare = Nest.compare end) @@ -53,9 +53,6 @@ module Domain = struct domain. *) type t = { constrs : TSet.t; - (* The constructors are sorted by the module [Topological_order] - in order to ensure the termination of the model generation. *) - ex : Ex.t; } diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index a71218f0c2..c4de466828 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -36,18 +36,20 @@ open DE type t = Dolmen.Std.Expr.ty_def list -(* Recall that a (directed) hypergraph is a set of nodes and hyperedges where - hyperedges join subsets of nodes. +(* A nest is the set of all the constructors in a mutually recursive definition + of ADTs. - To generate our total order on constructors of a same nest, we build - in the function [build_graph] a hypergraph where: - - the set of nodes is the set of all the constructors of the nest; - - for each type [ty] of the nest, we denote by S(ty) the set - of all the constructors of this type and G(ty) the set of - the constructors with an argument of type [ty]. + For each type ty of a nest, we denote by S(ty) the set of all the + constructors of this type in this nest and G(ty) the set of the constructors + with an argument of type ty in this nest. - Forall the type [ty] of the nest, there is a an edge from S(ty) to - G(ty). + Recall that a (directed) hypergraph is a set of nodes and hyperedges between + subsets of these nodes. + + To generate our total order of a nest, we build in [build_graph] a hypergraph + where: + - the nodes are all the constructors of the nest; + - for all type ty of the nest, there is a a hyperedge from S(ty) to G(ty). In particular, our graph has exactly one outgoing hyperedge per node. *) @@ -61,7 +63,7 @@ type node = { during the sorting (see [add_nest]). *) mutable outgoing : edge; - (* Hyperedge from a subset S in S(ty) to a subset G in G(ty) where [ty] is + (* Hyperedge from a subset S in S(ty) to a subset G in G(ty) where ty is the type of [id]. At the beginning, we have S = S(ty) and G = G(ty). One use a double indirection because this hyperedge is shared between diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index 035184c1f0..f3ea09e79e 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -34,11 +34,11 @@ module DE = Dolmen.Std.Expr constructors to ensure the termination of model generation for this theory. - By [nest], we mean the set of all the constructors in a mutually + By nest, we mean the set of all the constructors in a mutually recursive definition of ADTs. Before comparing constructors with [compare], the complete - nests to which they belong have to be added with [add_nest]. *) + nest to which they belong have to be added with [add_nest]. *) type t = DE.ty_def list (** Type of nest. *) @@ -50,8 +50,11 @@ val add_nest : t -> unit {b Note:} Assume that [defs] is a complete nest (in any order). *) val compare : Uid.t -> Uid.t -> int -(** [compare id1 id2] compares the identifier [id1] and [id2] with - the order generated by [add_nest] if they are both Dolmen identifiers. *) +(** [compare id1 id2] compares the constructors [id1] and [id2] with + the order generated by [add_nest] if they are both Dolmen identifiers. + + @raise Failure if the nests of the constructors [id1] and [id2] haven't + been added with [add_nest] before. *) val reinit : unit -> unit (** [reinit ()] resets the internal order. *) From b9a0a3d7a717e6f8126c26bbba3ba6d737e72bb6 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 23 May 2024 12:27:15 +0200 Subject: [PATCH 04/24] Improve performance of `pick_tightenable_domain` --- src/lib/reasoners/adt_rel.ml | 77 ++++++++++++++++++++++++------------ 1 file changed, 52 insertions(+), 25 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index ed4d1041fc..185d5717b8 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -133,6 +133,10 @@ module Domains = struct We don't store domains for constructors and selectors. *) + enums : Uid.t MX.t; + (** Map of tracked representatives for which the next constructor is an + enum. This field is used for sake of performance. *) + changed : SX.t; (** Representatives whose domain has changed since the last flush in [propagation]. *) @@ -147,14 +151,30 @@ module Domains = struct ) ppf t.domains - let empty = { domains = MX.empty; changed = SX.empty } + let empty = { domains = MX.empty; enums = MX.empty; changed = SX.empty } let filter_ty = is_adt_ty + let is_enum r d = + match X.type_info r with + | Ty.Tadt (name, params) -> + let Adt cases = Ty.type_body name params in + let c = Domain.choose d in + if Lists.is_empty @@ Ty.assoc_destrs c cases then + Some c + else + None + | _ -> assert false + let internal_update r nd t = let domains = MX.add r nd t.domains in + let enums = + match is_enum r nd with + | Some c -> MX.add r c t.enums + | None -> MX.remove r t.enums + in let changed = SX.add r t.changed in - { domains; changed } + { domains; enums; changed } let get r t = match Th.embed r with @@ -192,8 +212,9 @@ module Domains = struct let remove r t = let domains = MX.remove r t.domains in + let enums = MX.remove r t.enums in let changed = SX.remove r t.changed in - { domains ; changed } + { domains ; enums; changed } exception Inconsistent = Domain.Inconsistent @@ -227,6 +248,8 @@ module Domains = struct acc, { t with changed = SX.empty } let fold f t = MX.fold f t.domains + + let fold_enums f t = MX.fold f t.enums end let calc_destructor d e uf = @@ -604,31 +627,35 @@ let pick_delayed_destructor env uf = None with Found (r, d) -> Some (r, d) -let is_enum ty c = - match ty with - | Ty.Tadt (name, params) -> - let Adt cases = Ty.type_body name params in - Lists.is_empty @@ Ty.assoc_destrs c cases - | _ -> assert false - let pick_tightenable_domain ~for_model uf = let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in - Domains.fold - (fun r d best -> - let rr, _ = Uf.find_r uf r in - match Th.embed rr with - | Constr _ -> - best - | _ -> + let r = Domains.fold_enums + (fun r c best -> + let rr, _ = Uf.find_r uf r in + let d = Domains.get rr ds in let cd = Domain.cardinal d in - let c = Domain.choose d in - if for_model || is_enum (X.type_info r) c then - match best with - | Some (n, _, _) when n <= cd -> best - | Some _ | None -> Some (cd, r, c) - else - best - ) ds None + match Th.embed rr, best with + | Constr _, _ -> best + | _, Some (n, _, _) when n <= cd -> best + | _ -> Some (cd, r, c) + ) ds None + in + match r with + | Some _ as r -> r + | None -> + if for_model then + Domains.fold + (fun r d best -> + let rr, _ = Uf.find_r uf r in + let cd = Domain.cardinal d in + match Th.embed rr, best with + | Constr _, _ -> best + | _, Some (n, _, _) when n <= cd -> best + | _ -> + let c = Domain.choose d in + Some (cd, r, c) + ) ds None + else None let can_split env n = let m = Options.get_max_split () in From 5af24ebedd9ebefb4641337864e04acffc74b672 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 23 May 2024 14:29:03 +0200 Subject: [PATCH 05/24] final clean up --- src/lib/reasoners/adt_rel.ml | 133 +++++++++++++++++------------------ src/lib/structures/uid.mli | 1 - src/lib/util/nest.ml | 2 +- src/lib/util/util.ml | 5 ++ src/lib/util/util.mli | 3 + 5 files changed, 72 insertions(+), 72 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 185d5717b8..ab8e784f55 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -135,7 +135,8 @@ module Domains = struct enums : Uid.t MX.t; (** Map of tracked representatives for which the next constructor is an - enum. This field is used for sake of performance. *) + enum. This field is used for sake of performance during casesplit + rounds. *) changed : SX.t; (** Representatives whose domain has changed since the last flush @@ -607,80 +608,75 @@ let constr_of_destr ty d = exception Found of X.r * Uid.t -(* Pick a delayed destructor application in [env.delayed]. Returns [None] - if there is no delayed destructor. *) -let pick_delayed_destructor env uf = - let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in - try - Rel_utils.Delayed.iter_delayed - (fun r sy _e -> - match sy with - | Sy.Destruct destr -> - let d = Domains.get r ds in - if Domain.cardinal d > 1 then - raise_notrace @@ Found (r, destr) - else - () - | _ -> - () - ) env.delayed; - None - with Found (r, d) -> Some (r, d) - -let pick_tightenable_domain ~for_model uf = - let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in - let r = Domains.fold_enums - (fun r c best -> - let rr, _ = Uf.find_r uf r in - let d = Domains.get rr ds in - let cd = Domain.cardinal d in - match Th.embed rr, best with - | Constr _, _ -> best - | _, Some (n, _, _) when n <= cd -> best - | _ -> Some (cd, r, c) - ) ds None - in - match r with - | Some _ as r -> r - | None -> - if for_model then - Domains.fold - (fun r d best -> - let rr, _ = Uf.find_r uf r in - let cd = Domain.cardinal d in - match Th.embed rr, best with - | Constr _, _ -> best - | _, Some (n, _, _) when n <= cd -> best - | _ -> - let c = Domain.choose d in - Some (cd, r, c) - ) ds None - else None - let can_split env n = let m = Options.get_max_split () in Numbers.Q.(compare (mult n env.size_splits) m) <= 0 || Numbers.Q.sign m < 0 let (let*) = Option.bind -(* Do a case-split by choosing a semantic value [r] and constructor [c] +(* Do a casesplit by choosing a semantic value [r] and constructor [c] for which there are delayed destructor applications and propagate the literal [(not (_ is c) r)]. *) -let case_split_destructor env uf = +let split_delayed_destructor env uf = if not @@ Options.get_enable_adts_cs () then None else - let* r, d = pick_delayed_destructor env uf in - let c = constr_of_destr (X.type_info r) d in - Some (LR.mkv_builtin false (Sy.IsConstr c) [r]) + let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in + try + Rel_utils.Delayed.iter_delayed + (fun r sy _e -> + match sy with + | Sy.Destruct destr -> + let d = Domains.get r ds in + if Domain.cardinal d > 1 then + raise_notrace @@ Found (r, destr) + else + () + | _ -> + () + ) env.delayed; + None + with Found (r, d) -> + let c = constr_of_destr (X.type_info r) d in + Some (LR.mkv_builtin false (Sy.IsConstr c) [r]) + +(* Pick a enum constructor in a tracked domain with minimal cardinal. + Returns [None] if there is no such constructor. *) +let pick_enum ds uf = + Domains.fold_enums + (fun r c best -> + let rr, _ = Uf.find_r uf r in + let d = Domains.get rr ds in + let cd = Domain.cardinal d in + match Th.embed rr, best with + | Constr _, _ -> best + | _, Some (n, _, _) when n <= cd -> best + | _ -> Some (cd, r, c) + ) ds None + +(* Pick a constructor in a tracked domain with minimal cardinal. + Returns [None] if there is no such constructor. *) +let pick_best ~for_model ds uf = + if for_model then + Domains.fold + (fun r d best -> + let rr, _ = Uf.find_r uf r in + let cd = Domain.cardinal d in + match Th.embed rr, best with + | Constr _, _ -> best + | _, Some (n, _, _) when n <= cd -> best + | _ -> + let c = Domain.choose d in + Some (cd, r, c) + ) ds None + else None -(* Do a case-split by choosing a semantic value [r] whose the domain is as - small as possible. +let pick_tightenable_domain ~for_model uf = + let open Util in + let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in + (pick_enum ds pick_best ~for_model ds) uf - If [for_model] is [false], we consider only constructors without payload. In - particular, if [r] has no constructors without payload in its domain, we - don't case-split on it. *) -let case_split_best ~for_model env uf = +let split_best_domain ~for_model env uf = let* n, r, c = pick_tightenable_domain ~for_model uf in let n = Numbers.Q.from_int n in if for_model || can_split env n then @@ -691,18 +687,15 @@ let case_split_best ~for_model env uf = else None +let next_casesplit ~for_model env = + let open Util in + (split_delayed_destructor env) (split_best_domain ~for_model env) + let case_split env uf ~for_model = if Options.get_disable_adts () then [] else begin - let cs = - match case_split_destructor env uf with - | Some _ as cs -> - assert (not (Options.get_enable_adts_cs ()) || not for_model); - cs - | None -> case_split_best ~for_model env uf - in - match cs with + match next_casesplit ~for_model env uf with | Some cs -> if Options.get_debug_adt () then begin Debug.pp_domains "before cs" diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index bef18656d2..de7909ca69 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -33,7 +33,6 @@ module DE = Dolmen.Std.Expr type t = private | Hstring : Hstring.t -> t | Dolmen : 'a DE.id -> t - (* | Cstr : DE.term_cst DE.id -> t *) val of_dolmen : 'a DE.Id.t -> t val of_string : string -> t diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index c4de466828..685f6671c8 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -36,7 +36,7 @@ open DE type t = Dolmen.Std.Expr.ty_def list -(* A nest is the set of all the constructors in a mutually recursive definition +(* A nest is the set of all the constructors of a mutually recursive definition of ADTs. For each type ty of a nest, we denote by S(ty) the set of all the diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index afb881b3c8..fde6456f07 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -205,3 +205,8 @@ let rec print_list_pp ~sep ~pp fmt = function let internal_error msg = Format.kasprintf (fun s -> raise (Internal_error s)) msg + +let () f g x = + match f x with + | Some _ as r -> r + | None -> g x diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 3beb249659..e44249338e 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -135,3 +135,6 @@ val print_list_pp: Format.formatter -> 'a list -> unit val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a + +val () : ('a -> 'b option) -> ('a -> 'b option) -> 'a -> 'b option +(** [(f g) x] returns [f x] if [f x] succeeded, [g x] otherwise. *) From 5bb2d0472cc8e43522bfe5d92add3a3361df3462 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 23 May 2024 14:46:36 +0200 Subject: [PATCH 06/24] fix for old OCaml versions --- src/lib/util/nest.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 685f6671c8..95bd123805 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -137,7 +137,7 @@ let build_graph (defs : ty_def list) : Hp.t = let in_degree = Array.fold_left (fun acc2 dstr -> - let d = let* dstr in def_of_dstr dstr in + let d = let* dstr = dstr in def_of_dstr dstr in match d with | Some d -> begin match Hashtbl.find map d with From 64fe662367e1f2fb5ad6cfb609a0d00163113927 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 24 May 2024 10:48:36 +0200 Subject: [PATCH 07/24] Disable casesplit for enum constructors --- src/lib/reasoners/adt_rel.ml | 83 ++++++++---------------------------- src/lib/util/nest.ml | 24 +++++------ 2 files changed, 27 insertions(+), 80 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index ab8e784f55..cc2eb81ca3 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -133,11 +133,6 @@ module Domains = struct We don't store domains for constructors and selectors. *) - enums : Uid.t MX.t; - (** Map of tracked representatives for which the next constructor is an - enum. This field is used for sake of performance during casesplit - rounds. *) - changed : SX.t; (** Representatives whose domain has changed since the last flush in [propagation]. *) @@ -152,30 +147,14 @@ module Domains = struct ) ppf t.domains - let empty = { domains = MX.empty; enums = MX.empty; changed = SX.empty } + let empty = { domains = MX.empty; changed = SX.empty } let filter_ty = is_adt_ty - let is_enum r d = - match X.type_info r with - | Ty.Tadt (name, params) -> - let Adt cases = Ty.type_body name params in - let c = Domain.choose d in - if Lists.is_empty @@ Ty.assoc_destrs c cases then - Some c - else - None - | _ -> assert false - let internal_update r nd t = let domains = MX.add r nd t.domains in - let enums = - match is_enum r nd with - | Some c -> MX.add r c t.enums - | None -> MX.remove r t.enums - in let changed = SX.add r t.changed in - { domains; enums; changed } + { domains; changed } let get r t = match Th.embed r with @@ -213,9 +192,8 @@ module Domains = struct let remove r t = let domains = MX.remove r t.domains in - let enums = MX.remove r t.enums in let changed = SX.remove r t.changed in - { domains ; enums; changed } + { domains ; changed } exception Inconsistent = Domain.Inconsistent @@ -249,8 +227,6 @@ module Domains = struct acc, { t with changed = SX.empty } let fold f t = MX.fold f t.domains - - let fold_enums f t = MX.fold f t.enums end let calc_destructor d e uf = @@ -608,10 +584,6 @@ let constr_of_destr ty d = exception Found of X.r * Uid.t -let can_split env n = - let m = Options.get_max_split () in - Numbers.Q.(compare (mult n env.size_splits) m) <= 0 || Numbers.Q.sign m < 0 - let (let*) = Option.bind (* Do a casesplit by choosing a semantic value [r] and constructor [c] @@ -640,56 +612,35 @@ let split_delayed_destructor env uf = let c = constr_of_destr (X.type_info r) d in Some (LR.mkv_builtin false (Sy.IsConstr c) [r]) -(* Pick a enum constructor in a tracked domain with minimal cardinal. +(* Pick a constructor in a tracked domain with minimal cardinal. Returns [None] if there is no such constructor. *) -let pick_enum ds uf = - Domains.fold_enums - (fun r c best -> +let pick_best ds uf = + Domains.fold + (fun r d best -> let rr, _ = Uf.find_r uf r in - let d = Domains.get rr ds in let cd = Domain.cardinal d in match Th.embed rr, best with | Constr _, _ -> best | _, Some (n, _, _) when n <= cd -> best - | _ -> Some (cd, r, c) + | _ -> + let c = Domain.choose d in + Some (cd, r, c) ) ds None -(* Pick a constructor in a tracked domain with minimal cardinal. - Returns [None] if there is no such constructor. *) -let pick_best ~for_model ds uf = - if for_model then - Domains.fold - (fun r d best -> - let rr, _ = Uf.find_r uf r in - let cd = Domain.cardinal d in - match Th.embed rr, best with - | Constr _, _ -> best - | _, Some (n, _, _) when n <= cd -> best - | _ -> - let c = Domain.choose d in - Some (cd, r, c) - ) ds None - else None - -let pick_tightenable_domain ~for_model uf = - let open Util in - let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in - (pick_enum ds pick_best ~for_model ds) uf - -let split_best_domain ~for_model env uf = - let* n, r, c = pick_tightenable_domain ~for_model uf in - let n = Numbers.Q.from_int n in - if for_model || can_split env n then +let split_best_domain ~for_model uf = + if not for_model then + None + else + let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in + let* _, r, c = pick_best ds uf in let _, cons = Option.get @@ build_constr_eq r c in let nr, ctx = X.make cons in assert (Lists.is_empty ctx); Some (LR.mkv_eq r nr) - else - None let next_casesplit ~for_model env = let open Util in - (split_delayed_destructor env) (split_best_domain ~for_model env) + (split_delayed_destructor env) (split_best_domain ~for_model) let case_split env uf ~for_model = if Options.get_disable_adts () then diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 95bd123805..b2f4b1a385 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -49,9 +49,9 @@ type t = Dolmen.Std.Expr.ty_def list To generate our total order of a nest, we build in [build_graph] a hypergraph where: - the nodes are all the constructors of the nest; - - for all type ty of the nest, there is a a hyperedge from S(ty) to G(ty). + - for all type ty of the nest, there is a hyperedge from S(ty) to G(ty). - In particular, our graph has exactly one outgoing hyperedge per node. *) + In particular, our graph has exactly one outgoing hyperedge per node. *) (* Node of the hypergraph. *) type node = { @@ -187,18 +187,14 @@ let add_nest n = let { id; outgoing; in_degree; _ } = Hp.pop_minimum hp in add_cstr @@ Uid.of_dolmen id; assert (in_degree = 0); - outgoing := - List.filter_map - (fun node -> - assert (node.in_degree > 0); - let node = { node with in_degree = node.in_degree - 1 } in - if node.in_degree = 0 then ( - Hp.insert hp node; - None - ) else ( - Some node - ) - ) !outgoing + List.iter + (fun node -> + assert (node.in_degree > 0); + node.in_degree <- node.in_degree - 1; + if node.in_degree = 0 then + Hp.insert hp node + ) !outgoing; + outgoing := []; done let compare (id1 : Uid.t) (id2 : Uid.t) = From 9133c973e21013d6e043118aaa1f6ed7186c9a98 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 16:46:22 +0200 Subject: [PATCH 08/24] Case-split spelling --- src/lib/reasoners/adt.ml | 2 +- src/lib/reasoners/adt_rel.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 5fab09d5e4..f6091d907d 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -401,7 +401,7 @@ module Shostak (X : ALIEN) = struct let assign_value _ _ _ = - (* Model generation is performed by the casesplit mechanism + (* Model generation is performed by the case-split mechanism in [Adt_rel]. *) None diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index cc2eb81ca3..413fd38334 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -586,7 +586,7 @@ exception Found of X.r * Uid.t let (let*) = Option.bind -(* Do a casesplit by choosing a semantic value [r] and constructor [c] +(* Do a cases-plit by choosing a semantic value [r] and constructor [c] for which there are delayed destructor applications and propagate the literal [(not (_ is c) r)]. *) let split_delayed_destructor env uf = @@ -638,7 +638,7 @@ let split_best_domain ~for_model uf = assert (Lists.is_empty ctx); Some (LR.mkv_eq r nr) -let next_casesplit ~for_model env = +let next_case_split ~for_model env = let open Util in (split_delayed_destructor env) (split_best_domain ~for_model) @@ -646,7 +646,7 @@ let case_split env uf ~for_model = if Options.get_disable_adts () then [] else begin - match next_casesplit ~for_model env uf with + match next_case_split ~for_model env uf with | Some cs -> if Options.get_debug_adt () then begin Debug.pp_domains "before cs" From 2177dd69dcb9b1be96b380884a2ce8e94f0b8d5a Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 16:47:41 +0200 Subject: [PATCH 09/24] Remove useless Uf.find_r --- src/lib/reasoners/adt_rel.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 413fd38334..cff6cf0b54 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -614,12 +614,11 @@ let split_delayed_destructor env uf = (* Pick a constructor in a tracked domain with minimal cardinal. Returns [None] if there is no such constructor. *) -let pick_best ds uf = +let pick_best ds = Domains.fold (fun r d best -> - let rr, _ = Uf.find_r uf r in let cd = Domain.cardinal d in - match Th.embed rr, best with + match Th.embed r, best with | Constr _, _ -> best | _, Some (n, _, _) when n <= cd -> best | _ -> @@ -632,7 +631,7 @@ let split_best_domain ~for_model uf = None else let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in - let* _, r, c = pick_best ds uf in + let* _, r, c = pick_best ds in let _, cons = Option.get @@ build_constr_eq r c in let nr, ctx = X.make cons in assert (Lists.is_empty ctx); From 460b1be979e38615fa2e32e668a3a33cbb28fb0e Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 16:50:15 +0200 Subject: [PATCH 10/24] Simplify return type of `pick_best` --- src/lib/reasoners/adt_rel.ml | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index cff6cf0b54..d9f0d5564f 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -615,23 +615,26 @@ let split_delayed_destructor env uf = (* Pick a constructor in a tracked domain with minimal cardinal. Returns [None] if there is no such constructor. *) let pick_best ds = - Domains.fold - (fun r d best -> - let cd = Domain.cardinal d in - match Th.embed r, best with - | Constr _, _ -> best - | _, Some (n, _, _) when n <= cd -> best - | _ -> - let c = Domain.choose d in - Some (cd, r, c) - ) ds None + let* _, r, c = + Domains.fold + (fun r d best -> + let cd = Domain.cardinal d in + match Th.embed r, best with + | Constr _, _ -> best + | _, Some (n, _, _) when n <= cd -> best + | _ -> + let c = Domain.choose d in + Some (cd, r, c) + ) ds None + in + Some (r, c) let split_best_domain ~for_model uf = if not for_model then None else let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in - let* _, r, c = pick_best ds in + let* r, c = pick_best ds in let _, cons = Option.get @@ build_constr_eq r c in let nr, ctx = X.make cons in assert (Lists.is_empty ctx); From 70d25ebf229e2128cbb446f23e3d5823149a7866 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 16:51:45 +0200 Subject: [PATCH 11/24] Add comment for empty ctx of `X.make` --- src/lib/reasoners/adt_rel.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index d9f0d5564f..c7f8c5ce96 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -636,6 +636,10 @@ let split_best_domain ~for_model uf = let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in let* r, c = pick_best ds in let _, cons = Option.get @@ build_constr_eq r c in + (* In the current implementation of `X.make`, we produce + a nonempty context only for interpreted semantic values + of the `Arith` and `Records` theories. The semantic + values `cons` never involves such values. *) let nr, ctx = X.make cons in assert (Lists.is_empty ctx); Some (LR.mkv_eq r nr) From 9f775c78e6079de9d966c0c44208e9f824fffc5f Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 16:57:01 +0200 Subject: [PATCH 12/24] poetry --- src/lib/util/nest.ml | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index b2f4b1a385..c43fc28342 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -162,20 +162,18 @@ module H = Hashtbl.Make (Uid) let add_cstr, find_weight, reinit = let ctr = ref 0 in let order : int H.t = H.create 100 in - (* add_weight *) - (fun cstr -> - H.add order cstr !ctr; - incr ctr), - (* find_weight *) - (fun cstr -> - try - H.find order cstr - with Not_found -> - Fmt.failwith "cannot find uid %a" Uid.pp cstr), - (* reinit *) - (fun () -> - ctr := 0; - H.clear order) + let add_cstr cstr = + H.add order cstr !ctr; + incr ctr + and find_weight cstr = + try + H.find order cstr + with Not_found -> + Fmt.failwith "cannot find uid %a" Uid.pp cstr + and reinit () = + ctr := 0; + H.clear order + in add_cstr, find_weight, reinit (* Sort the constructors of the nest using a sorting based on the Kahn's algorithm. *) From 2580bf2dce094bdab7e6866ec793162e484e25ce Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 16:58:00 +0200 Subject: [PATCH 13/24] genetive again... --- src/lib/util/nest.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index c43fc28342..02a9b542b5 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -175,7 +175,7 @@ let add_cstr, find_weight, reinit = H.clear order in add_cstr, find_weight, reinit -(* Sort the constructors of the nest using a sorting based on the +(* Sort the constructors of the nest using a sorting based on Kahn's algorithm. *) let add_nest n = let hp = build_graph n in From 1225740a255e980eb66e99e66c0b3020fc462391 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 16:59:08 +0200 Subject: [PATCH 14/24] Use formal writing --- src/lib/reasoners/adt_rel.ml | 2 +- src/lib/reasoners/enum_rel.ml | 2 +- src/lib/reasoners/theory.ml | 2 +- src/lib/util/nest.mli | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index c7f8c5ce96..0cfef13870 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -345,7 +345,7 @@ let assume_th_elt t th_elt _ = This function alone isn't sufficient to produce a complete decision procedure for the ADT theory. For instance, let's assume we have three semantic values [r1], [r2] and [r3] whose the domain is `{C1, C2}`. It's - clear that `(distinct r1 r2 r3)` is unsatisfiable but we haven't enough + clear that `(distinct r1 r2 r3)` is unsatisfiable but we have not enough information to discover this contradiction. We plan to support model generation for ADT. As a by-product, we will got diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml index f8ddac6655..094cf510df 100644 --- a/src/lib/reasoners/enum_rel.ml +++ b/src/lib/reasoners/enum_rel.ml @@ -268,7 +268,7 @@ let tighten_domain rr nd domains = This function alone isn't sufficient to produce a complete decision procedure for the Enum theory. For instance, let's assume we have three semantic values [r1], [r2] and [r3] whose the domain is `{C1, C2}`. It's - clear that `(distinct r1 r2 r3)` is unsatisfiable but we haven't enough + clear that `(distinct r1 r2 r3)` is unsatisfiable but we have not enough information to discover this contradiction. Now, if we produce a case-split for one of these semantic values, diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 9c0a59ee5c..7b51a8fc6a 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -525,7 +525,7 @@ module Main_Default : S = struct let r = try if t.choices == [] then - (* We haven't make choice yet. Initialize the environment + (* We have not make choice yet. Initialize the environment [gamma_finite] with [gamma]. *) let t = reset_case_split_env t in look_for_sat ~for_model t [] [] diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index f3ea09e79e..c621131b90 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -53,7 +53,7 @@ val compare : Uid.t -> Uid.t -> int (** [compare id1 id2] compares the constructors [id1] and [id2] with the order generated by [add_nest] if they are both Dolmen identifiers. - @raise Failure if the nests of the constructors [id1] and [id2] haven't + @raise Failure if the nests of the constructors [id1] and [id2] have not been added with [add_nest] before. *) val reinit : unit -> unit From 2ac96a1c10ef2f2b21a42a8b2f693a2c87867399 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 17:02:16 +0200 Subject: [PATCH 15/24] Remove `open DE` --- src/lib/util/nest.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 02a9b542b5..8651a52075 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -32,7 +32,6 @@ module DStd = Dolmen.Std module DE = DStd.Expr module DT = DE.Ty module B = Dolmen.Std.Builtin -open DE type t = Dolmen.Std.Expr.ty_def list @@ -55,7 +54,7 @@ type t = Dolmen.Std.Expr.ty_def list (* Node of the hypergraph. *) type node = { - id : term_cst; + id : DE.term_cst; (* Dolmen constructor identifier. *) weight : int; @@ -85,7 +84,7 @@ module Hp = let default = let dummy_edge : node list ref = ref [] in { - id = Term.Const.Int.int "0" (* dummy *); + id = DE.Term.Const.Int.int "0" (* dummy *); outgoing = dummy_edge; in_degree = -1; weight = -1; @@ -116,17 +115,17 @@ let def_of_dstr dstr = @return a heap that contains all the nodes of this graph without ingoing hyperedges. *) -let build_graph (defs : ty_def list) : Hp.t = - let map : (ty_def, edge) Hashtbl.t = Hashtbl.create 17 in +let build_graph (defs : DE.ty_def list) : Hp.t = + let map : (DE.ty_def, edge) Hashtbl.t = Hashtbl.create 17 in let hp : Hp.t = Hp.create 17 in List.iter (fun d -> Hashtbl.add map d (ref [])) defs; List.iter (fun def -> match def with - | Abstract -> assert false - | Adt { cases; _ } -> + | DE.Abstract -> assert false + | DE.Adt { cases; _ } -> Array.iter - (fun { cstr; dstrs; _ } -> + (fun DE.{ cstr; dstrs; _ } -> let node = { id = cstr; outgoing = Hashtbl.find map def; From 7a648aaf05d74023674589be4d3d679b77d6fe96 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 17:14:57 +0200 Subject: [PATCH 16/24] Rollback `split_delayed_destructor` --- src/lib/reasoners/adt_rel.ml | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 0cfef13870..c29686cb7e 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -589,23 +589,16 @@ let (let*) = Option.bind (* Do a cases-plit by choosing a semantic value [r] and constructor [c] for which there are delayed destructor applications and propagate the literal [(not (_ is c) r)]. *) -let split_delayed_destructor env uf = +let split_delayed_destructor env _uf = if not @@ Options.get_enable_adts_cs () then None else - let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in try Rel_utils.Delayed.iter_delayed (fun r sy _e -> match sy with - | Sy.Destruct destr -> - let d = Domains.get r ds in - if Domain.cardinal d > 1 then - raise_notrace @@ Found (r, destr) - else - () - | _ -> - () + | Sy.Destruct destr -> raise_notrace @@ Found (r, destr) + | _ -> () ) env.delayed; None with Found (r, d) -> From cddb65d61f9e7c7913ff8177a5917701b7decac3 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 17:17:45 +0200 Subject: [PATCH 17/24] Remove my fancy operator `` --- src/lib/reasoners/adt_rel.ml | 9 +++++---- src/lib/util/util.ml | 5 ----- src/lib/util/util.mli | 3 --- 3 files changed, 5 insertions(+), 12 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index c29686cb7e..af7d51914e 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -589,7 +589,7 @@ let (let*) = Option.bind (* Do a cases-plit by choosing a semantic value [r] and constructor [c] for which there are delayed destructor applications and propagate the literal [(not (_ is c) r)]. *) -let split_delayed_destructor env _uf = +let split_delayed_destructor env = if not @@ Options.get_enable_adts_cs () then None else @@ -637,9 +637,10 @@ let split_best_domain ~for_model uf = assert (Lists.is_empty ctx); Some (LR.mkv_eq r nr) -let next_case_split ~for_model env = - let open Util in - (split_delayed_destructor env) (split_best_domain ~for_model) +let next_case_split ~for_model env uf = + match split_delayed_destructor env with + | Some _ as r -> r + | None -> split_best_domain ~for_model uf let case_split env uf ~for_model = if Options.get_disable_adts () then diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index fde6456f07..afb881b3c8 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -205,8 +205,3 @@ let rec print_list_pp ~sep ~pp fmt = function let internal_error msg = Format.kasprintf (fun s -> raise (Internal_error s)) msg - -let () f g x = - match f x with - | Some _ as r -> r - | None -> g x diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index e44249338e..3beb249659 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -135,6 +135,3 @@ val print_list_pp: Format.formatter -> 'a list -> unit val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a - -val () : ('a -> 'b option) -> ('a -> 'b option) -> 'a -> 'b option -(** [(f g) x] returns [f x] if [f x] succeeded, [g x] otherwise. *) From c0b49e62b0b2177aef5eb4602c87e6e40c732a1d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 3 Jun 2024 17:20:33 +0200 Subject: [PATCH 18/24] rename `pop_minimun` to `pop_min` --- src/lib/reasoners/satml.ml | 2 +- src/lib/util/heap.ml | 4 ++-- src/lib/util/heap.mli | 4 ++-- src/lib/util/nest.ml | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 0e4e2bfdbb..87244a43d9 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1827,7 +1827,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct env.next_split <- None; pick_branch_aux env atom | None -> - match Vheap.pop_minimum env.order with + match Vheap.pop_min env.order with | v -> pick_branch_aux env v.na | exception Not_found -> if Options.get_cdcl_tableaux_inst () then diff --git a/src/lib/util/heap.ml b/src/lib/util/heap.ml index c4d903afda..da5e77aad0 100644 --- a/src/lib/util/heap.ml +++ b/src/lib/util/heap.ml @@ -122,7 +122,7 @@ module MakeRanked(Rank : RankedType) = struct let[@inline] grow_to_by_double { heap } sz = Vec.grow_to_by_double heap sz - let pop_minimum ({ heap } as s) = + let pop_min ({ heap } as s) = match Vec.size heap with | 0 -> raise Not_found | 1 -> @@ -170,5 +170,5 @@ module MakeOrdered(V : OrderedTypeDefault) = struct let create n = H.create n (entry V.default) let is_empty = H.is_empty let insert h v = H.insert h (entry v) - let pop_minimum h = (H.pop_minimum h).value + let pop_min h = (H.pop_min h).value end diff --git a/src/lib/util/heap.mli b/src/lib/util/heap.mli index ab2cab51fa..d532b1ee91 100644 --- a/src/lib/util/heap.mli +++ b/src/lib/util/heap.mli @@ -94,7 +94,7 @@ module MakeRanked(Rank : RankedType) : sig (** Grow the size of the heap by multiplying it by 2 until it is at least the size specified. *) - val pop_minimum : t -> elt + val pop_min : t -> elt (** Remove the minimum element from the heap and return it. @raise Not_found if the heap is empty. *) @@ -130,7 +130,7 @@ module MakeOrdered(V : OrderedTypeDefault) : sig val insert : t -> elt -> unit (** Insert a new element in the heap. *) - val pop_minimum : t -> elt + val pop_min : t -> elt (** Remove the minimum element from the heap and return it. @raise Not_found if the heap is empty. *) diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 8651a52075..2db3a2c805 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -181,7 +181,7 @@ let add_nest n = while not @@ Hp.is_empty hp do (* Loop invariant: the set of nodes in heap [hp] is exactly the set of the nodes of the graph without ingoing hyperedge. *) - let { id; outgoing; in_degree; _ } = Hp.pop_minimum hp in + let { id; outgoing; in_degree; _ } = Hp.pop_min hp in add_cstr @@ Uid.of_dolmen id; assert (in_degree = 0); List.iter From dc6faaccc9d84f36f244a243fa3b614f99f0bfbf Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 5 Jun 2024 18:10:15 +0200 Subject: [PATCH 19/24] Remove outdated comment Alt-Ergo answers `unsat` for this test on both `v2.5.4` and `next` instead of producing a wrong model. `Z3` answers `unsat` too but `cvc 5` answers `unknown`. --- src/lib/reasoners/fun_sat.ml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index e7b00d676f..3a56a50ba7 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1275,10 +1275,6 @@ module Make (Th : Theory.S) = struct match Options.get_instantiation_heuristic () with | INormal -> (* TODO: check if this test still produces a wrong model. *) - (* S: This seems spurious! - On example UFDT/20170428-Barrett/cdt-cade2015/data/gandl/cotree/ - x2015_09_10_16_49_52_978_1009894.smt_in.smt2, - this returns a wrong model. *) update_model_and_return_unknown env (Options.get_last_interpretation ()) ~unknown_reason:Incomplete (* may becomes ModelGen *) From 52d3bc5e8851bcae9ea3e43730f0ced739922685 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 7 Jun 2024 13:23:20 +0200 Subject: [PATCH 20/24] remove let-punning --- src/lib/util/nest.ml | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 2db3a2c805..2c9ca573fd 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -135,18 +135,14 @@ let build_graph (defs : DE.ty_def list) : Hp.t = in let in_degree = Array.fold_left - (fun acc2 dstr -> - let d = let* dstr = dstr in def_of_dstr dstr in - match d with + (fun acc dstr -> + match Option.bind dstr def_of_dstr with | Some d -> begin match Hashtbl.find map d with - | used_by -> - used_by := node :: !used_by; - acc2 + 1 - | exception Not_found -> - acc2 + | edge -> edge := node :: !edge; acc + 1 + | exception Not_found -> acc end - | None -> acc2 + | None -> acc ) 0 dstrs in node.in_degree <- in_degree; From 375339ad0f519d0f9d876792db1e6ebae0922797 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 10 Jun 2024 15:04:55 +0200 Subject: [PATCH 21/24] Add a TODO comment for pending destructors --- src/lib/reasoners/uf.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 9b2b6f2a3a..4774e072d9 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1183,6 +1183,10 @@ let compute_concrete_model_of_val cache = and get_abstract_for = Cache.get_abstract_for cache.abstracts in fun env t ((mdl, mrepr) as acc) -> let { E.f; xs; ty; _ } = E.term_view t in + (* TODO: We have to filter out destructors here as we don't consider + pending destructors as solvable theory symbols of the ADT theory. + We should check if these symbols can be defined as solvable to + remove this particular case here. *) if X.is_solvable_theory_symbol f ty || is_destructor f || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t || E.equal t E.vrai || E.equal t E.faux From 8a42861551008baeb01afdab30ba8b20f09f03b0 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 10 Jun 2024 15:23:41 +0200 Subject: [PATCH 22/24] Fix headers of Nest --- src/lib/util/nest.ml | 14 +------------- src/lib/util/nest.mli | 14 +------------- 2 files changed, 2 insertions(+), 26 deletions(-) diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml index 2c9ca573fd..ac42686f82 100644 --- a/src/lib/util/nest.ml +++ b/src/lib/util/nest.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,18 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* Until 2013, some parts of this code were released under *) -(* the Apache Software License version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index c621131b90..456d2b81a3 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,18 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* Until 2013, some parts of this code were released under *) -(* the Apache Software License version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) From ce456f6895e898047a962e8bd4028936d384cdfc Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 10 Jun 2024 15:39:31 +0200 Subject: [PATCH 23/24] send enum adt to the legacy adt theory --- 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 9498487cb0..99a1dc603d 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -736,7 +736,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) = ) cases ([], true) in let uid = Uid.of_dolmen ty_c in - if is_enum && not contains_adts + if is_enum then ( let ty = Ty.tsum uid cns in Cache.store_ty ty_c ty; From 280eb2f6fbddb33b7170d6a86e893fbe5342b702 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 10 Jun 2024 18:18:09 +0200 Subject: [PATCH 24/24] Clarify doc of reinit --- src/lib/util/nest.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli index 456d2b81a3..47777be59e 100644 --- a/src/lib/util/nest.mli +++ b/src/lib/util/nest.mli @@ -45,4 +45,4 @@ val compare : Uid.t -> Uid.t -> int been added with [add_nest] before. *) val reinit : unit -> unit -(** [reinit ()] resets the internal order. *) +(** [reinit ()] clears all the registered constructors by [add_nest]. *)