From cabdf4ad087498ee876db37ce1019a32f38e2d19 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 22 Mar 2024 15:45:09 +0100 Subject: [PATCH] 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 we turn model generation on, we performs casesplits even if the flag `--enable-adts-cs` isn't present in the command line. - The termination of the model generation is a bit tricky in the case of mutually recursive ADT. Please see the tests added for some complicated examples. I hope that I caught all the corner cases. To ensure the termination, the basic idea is to sort ADT's constructors in the module `Ty` during the parsing and to use the fact that the SMT-LIB standard only accepts well-founded ADT. We choose constructors in domains with the following order: - Constructor with the less destructors using the same nest; - Constructor with the less destructors using another nest of the same mutually recursive declaration; --- src/bin/common/solving_loop.ml | 1 + src/lib/reasoners/adt.ml | 21 ++-- src/lib/reasoners/adt_rel.ml | 38 ++++++- src/lib/reasoners/shostak.ml | 3 +- src/lib/reasoners/uf.ml | 10 +- src/lib/structures/ty.ml | 140 +++++++++++++++++-------- src/lib/util/lists.ml | 3 + src/lib/util/lists.mli | 4 + tests/dune.inc | 110 +++++++++++++++++++ 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 ++ 19 files changed, 364 insertions(+), 60 deletions(-) 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 diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index e8362b605f..3cd7b2584b 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -579,6 +579,7 @@ let main () = st | ":produce-models", Symbol { name = Simple "true"; _ } -> Options.set_interpretation ILast; + Options.set_enable_adts_cs true; st | ":produce-models", Symbol { name = Simple "false"; _ } -> Options.set_interpretation INone; diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index bdc1211d06..a5b9eac68e 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -405,12 +405,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_term Sy.(Op (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 c7ab64bb47..b6d38b2a96 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -52,6 +52,10 @@ module Domain = struct exception Inconsistent of Ex.t + let[@inline always] cardinal { constrs; _ } = HSS.cardinal constrs + + let[@inline always] choose { constrs; _ } = HSS.choose constrs + let[@inline always] as_singleton { constrs; ex } = if HSS.cardinal constrs = 1 then Some (HSS.choose constrs, ex) @@ -202,6 +206,8 @@ module Domains = struct ) t.changed acc in acc, { t with changed = SX.empty } + + let iter f t = MX.iter f t.domains end let calc_destructor d e uf = @@ -603,8 +609,12 @@ let pick_delayed_destructor env = 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 env.domains in + if Domain.cardinal d > 1 then + raise_notrace @@ Found (r, destr) + else + () | _ -> () ) env.delayed; @@ -615,11 +625,31 @@ let pick_delayed_destructor env = for which there are delayed destructor applications and propagate the literal [(not (_ is c) r)]. *) let case_split env _uf ~for_model = - if Options.get_disable_adts () || not (Options.get_enable_adts_cs()) + if Options.get_disable_adts () + || not (Options.get_enable_adts_cs () || for_model) then [] + else if for_model then + try + Domains.iter + (fun r d -> + if Domain.cardinal d > 1 then + let c = Domain.choose d in + raise_notrace @@ Found (r, c) + ) env.domains; + [] + with Found (r, c) -> + match build_constr_eq r c with + | Some (_, cons) -> + let nr, _ = X.make cons in + let cs = LR.mkv_eq r nr in + if Options.get_debug_adt () then + Printer.print_dbg ~flushed:false + ~module_name:"Adt_rel" ~function_name:"case_split" + "Assume %a = %a" X.print r Hstring.print c; + [ cs, true, Th_util.CS (Th_util.Th_adt, two) ] + | None -> assert false else begin - assert (not for_model); if Options.get_debug_adt () then Debug.pp_env "before cs" env; match pick_delayed_destructor env with | Some (r, d) -> diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 7a70701add..adb97b5a07 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -443,7 +443,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 53ccef25ed..790d0907de 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1068,6 +1068,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: @@ -1084,9 +1088,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/ty.ml b/src/lib/structures/ty.ml index 141559cca1..7ac9e1fea8 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -463,54 +463,55 @@ module Decls = struct MH.add name {decl = (params, body); instances = MTY.empty} !decls let body name args = + let {decl = (params, body); instances} = MH.find name !decls in try - let {decl = (params, body); instances} = MH.find name !decls in - try - if compare_list params args = 0 then body - else MTY.find args instances - (* should I instantiate if not found ?? *) - with Not_found -> - let params, body = fresh_type params body in - (*if true || get_debug_adt () then*) - let sbt = - try - List.fold_left2 - (fun sbt vty ty -> - let vty = shorten vty in - match vty with - | Tvar { value = Some _ ; _ } -> assert false - | Tvar {v ; value = None} -> - if equal vty ty then sbt else M.add v ty sbt - | _ -> - Printer.print_err "vty = %a and ty = %a" - print vty print ty; - assert false - )M.empty params args - with Invalid_argument _ -> assert false - in - let body = match body with - | Adt cases -> - Adt( - List.map - (fun {constr; destrs} -> - {constr; - destrs = - List.map (fun (d, ty) -> d, apply_subst sbt ty) destrs } - ) cases - ) - in - let params = List.map (fun ty -> apply_subst sbt ty) params in - add name params body; - body + if compare_list params args = 0 then body + else MTY.find args instances + (* should I instantiate if not found ?? *) with Not_found -> - Printer.print_err "%a not found" Hstring.print name; - assert false + let params, body = fresh_type params body in + (*if true || get_debug_adt () then*) + let sbt = + try + List.fold_left2 + (fun sbt vty ty -> + let vty = shorten vty in + match vty with + | Tvar { value = Some _ ; _ } -> assert false + | Tvar {v ; value = None} -> + if equal vty ty then sbt else M.add v ty sbt + | _ -> + Printer.print_err "vty = %a and ty = %a" + print vty print ty; + assert false + )M.empty params args + with Invalid_argument _ -> assert false + in + let body = match body with + | Adt cases -> + Adt( + List.map + (fun {constr; destrs} -> + {constr; + destrs = + List.map (fun (d, ty) -> d, apply_subst sbt ty) destrs } + ) cases + ) + in + let params = List.map (fun ty -> apply_subst sbt ty) params in + add name params body; + body let reinit () = decls := MH.empty end -let type_body name args = Decls.body name args +let type_body name args = + try + Decls.body name args + with Not_found -> + Printer.print_err "%a not found" Hstring.print name; + assert false (* smart constructors *) @@ -524,6 +525,56 @@ let fresh_empty_text = let tsum s lc = Tsum (Hstring.make s, List.map Hstring.make lc) +(* Count the number of occurences of the nest of [name] in the signature + of payload [l]. *) +let count_same_nest name l = + Lists.sum + (fun (_, ty) -> + match ty with + | Tadt (name', _) when Hstring.equal name name' -> 1 + | _ -> 0 + ) l + +(* Count the number of occurences of the (mutually recursive) ADT type of + [name] in the signature of payload [l]. *) +let count_same_adt name l = + Lists.sum + (fun (_, ty) -> + match ty with + | Tadt (name', params) -> + (* TODO: this is a hackish way to check that `name'` and `name` are + two nests of the same mutually recursive ADT. We should store + ADT's nests in a data structure as it's done in Dolmen. *) + begin try + let Adt cases = Decls.body name' params in + List.exists + (fun { destrs; _ } -> + List.exists + (fun (_, ty') -> + match ty' with + | Tadt (name'', _) -> Hstring.equal name name'' + | _ -> false + ) destrs + ) cases + |> Bool.to_int + with Not_found -> + (* If we haven't already register the nest [name'], it means that + [name] and [name'] are two nests of the same ADT. *) + 1 + end + | _ -> 0 + ) l + +(* Comparison function used to ensure the termination of the model + generation for recursive ADT values. *) +let cons_weight name (_, l1) (_, l2) = + let c = count_same_nest name l1 - count_same_nest name l2 in + if c <> 0 then c + else + let c = count_same_adt name l1 - count_same_adt name l2 in + if c <> 0 then c + else List.compare_lengths l1 l2 + let t_adt ?(body=None) s ty_vars = let hs = Hstring.make s in let ty = Tadt (hs, ty_vars) in @@ -545,12 +596,13 @@ let t_adt ?(body=None) s ty_vars = Decls.add hs ty_vars (Adt cases) | Some cases -> let cases = - List.map (fun (s, l) -> + List.stable_sort (cons_weight hs) cases |> + List.map (fun (c, l) -> let l = List.map (fun (d, e) -> Hstring.make d, e) l in - {constr = Hstring.make s; destrs = l} - ) cases + {constr = Hstring.make c; destrs = l} + ) in Decls.add hs ty_vars (Adt cases) end; diff --git a/src/lib/util/lists.ml b/src/lib/util/lists.ml index 87409ad160..4ccf351c7f 100644 --- a/src/lib/util/lists.ml +++ b/src/lib/util/lists.ml @@ -64,3 +64,6 @@ let rec is_sorted cmp l = match l with | x :: y :: xs -> cmp x y <= 0 && is_sorted cmp (y :: xs) | [_] | [] -> true + +let sum f l = + List.fold_left (fun sum i -> sum + f i) 0 l diff --git a/src/lib/util/lists.mli b/src/lib/util/lists.mli index 82103e5832..20b8079329 100644 --- a/src/lib/util/lists.mli +++ b/src/lib/util/lists.mli @@ -55,3 +55,7 @@ val try_map : ('a -> 'b option) -> 'a list -> 'b list option val is_sorted : ('a -> 'a -> int) -> 'a list -> bool (** [is_sorted cmp l] checks that [l] is sorted for the comparison function [cmp]. *) + +val sum : ('a -> int) -> 'a list -> int +(** [sum f l] computes the sum [f a1 + f a2 + ...] where + [l = [a1; a2; ...]]. *) diff --git a/tests/dune.inc b/tests/dune.inc index 3e6b147edf..1431c59d72 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -210397,6 +210397,116 @@ ; Auto-generated part end ; File auto-generated by gentests +; Auto-generated part begin +(subdir models/adt + (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)