From 8da2850284722142882c6498e044257550ac280b Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 11 Dec 2023 17:34:23 +0100 Subject: [PATCH] Only use `Expr.t` to store model values As arrays can occur into model values, we need to use `Expr.t` to represent them. We cannot produce the appropriate model term with `Arrays.to_model_term` because we haven't semantic values for arrays. Instead we perform two passes on a pre-model generating with `X.to_model_term`. - The first pass collects all the values of arrays and generates a model term for each array. If the array was declared by the user, we add it to the model. - The second pass substitutes all the array identifiers in the pre-model by model terms we have generated in the first pass. --- src/lib/reasoners/records.ml | 3 +- src/lib/reasoners/uf.ml | 41 +++++++---- src/lib/structures/errors.ml | 18 +++++ src/lib/structures/errors.mli | 9 +++ src/lib/structures/expr.ml | 10 ++- src/lib/structures/expr.mli | 5 ++ src/lib/structures/id.ml | 2 + src/lib/structures/id.mli | 1 + src/lib/structures/modelMap.ml | 69 +++++++++---------- src/lib/structures/modelMap.mli | 22 +++--- tests/dune.inc | 21 ++++++ .../array/embedded-array.models.expected | 8 +++ tests/models/array/embedded-array.models.smt2 | 10 +++ 13 files changed, 152 insertions(+), 67 deletions(-) create mode 100644 tests/models/array/embedded-array.models.expected create mode 100644 tests/models/array/embedded-array.models.smt2 diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index ae4164e27..8bbc3b333 100644 --- a/src/lib/reasoners/records.ml +++ b/src/lib/reasoners/records.ml @@ -439,7 +439,8 @@ module Shostak (X : ALIEN) = struct Option.bind l @@ fun l -> Some (E.mk_term Sy.(Op Record) l ty) - | Other (a, _) -> X.to_model_term a + | Other (a, _) -> + X.to_model_term a | Access _ -> None in fun r -> to_model_term (embed r) end diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index ac15dcdce..54edbc0b1 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1065,8 +1065,7 @@ let terms env = (* Helper functions used by the caches during the computation of the model. *) module Cache = struct - let store_array_get arrays_cache (t : Expr.t) (i : ModelMap.Value.t) - (v : ModelMap.Value.t) = + let store_array_get arrays_cache (t : Expr.t) (i : Expr.t) (v : Expr.t) = match Hashtbl.find_opt arrays_cache t with | Some values -> Hashtbl.replace values i v @@ -1080,17 +1079,17 @@ module Cache = struct match Hashtbl.find_opt abstracts_cache r with | Some abstract -> abstract | None -> - let abstract = Id.Namespace.Abstract.fresh () |> Hstring.make in + let abstract = Expr.mk_abstract (Expr.type_info t) in Hashtbl.add abstracts_cache r abstract; abstract end type cache = { - array_selects: (Expr.t, (ModelMap.Value.t, ModelMap.Value.t) Hashtbl.t) + array_selects: (Expr.t, (Expr.t, Expr.t) Hashtbl.t) Hashtbl.t; (** Stores all the get accesses to arrays. *) - abstracts: (r, Id.t) Hashtbl.t; + abstracts: (r, Expr.t) Hashtbl.t; (** Stores all the abstract values generated. This cache is necessary to ensure we don't generate twice an abstract value for a given symbol. *) } @@ -1131,7 +1130,7 @@ let compute_concrete_model_of_val cache = List.fold_left (fun (arg_vals, arg_tys, mrepr) arg -> let rep_arg, mrepr = model_repr_of_term arg env mrepr in - ModelMap.Value.Constant rep_arg :: arg_vals, + rep_arg :: arg_vals, (Expr.type_info arg) :: arg_tys, mrepr ) @@ -1152,9 +1151,9 @@ let compute_concrete_model_of_val cache = | Sy.Op Sy.Set, _, _ -> acc - | Sy.Op Sy.Get, [Constant a; i], _ -> + | Sy.Op Sy.Get, [a; i], _ -> begin - store_array_select a i (Constant ret_rep); + store_array_select a i ret_rep; acc end @@ -1165,9 +1164,8 @@ let compute_concrete_model_of_val cache = (* We cannot produce a concrete value as the type is abstract. In this case, we produce an abstract value with the appropriate type. *) - let abstract = get_abstract_for env t in - ModelMap.Value.Abstract (abstract, ty) - | _ -> ModelMap.Value.Constant ret_rep + get_abstract_for env t + | _ -> ret_rep in ModelMap.(add (id, arg_tys, ty) arg_vals value mdl), mrepr @@ -1188,7 +1186,6 @@ let extract_concrete_model cache = terms (ModelMap.empty ~suspicious, ME.empty) in let model = - let open ModelMap.Value in Hashtbl.fold (fun t vals mdl -> (* We produce a fresh identifiant for abstract value in order to prevent any capture. *) @@ -1196,8 +1193,8 @@ let extract_concrete_model cache = let ty = Expr.type_info t in let arr_val = Hashtbl.fold (fun i v arr_val -> - Store (arr_val, i, v) - ) vals (Abstract (abstract, ty)) + Expr.ArraysEx.store arr_val i v + ) vals abstract in let id = let Expr.{ f; _ } = Expr.term_view t in @@ -1208,7 +1205,21 @@ let extract_concrete_model cache = [array_selects]. *) assert false in - ModelMap.add (id, [], ty) [] arr_val mdl + let mdl = + if not @@ Id.Namespace.Internal.is_id (Hstring.view id) then + ModelMap.add (id, [], ty) [] arr_val mdl + else + (* Internal identifiers can occur here if we need to generate + a model term for an embedded array but this array isn't itself + declared by the user. *) + mdl + in + (* We need to update the model [mdl] in order to substitute all the + occurrences of the array identifier [id] by an appropriate model + term. This cannot be performed while computing the model with + `compute_concrete_model_of_val` because we need to first iterate + on all the union-find environment to collect array values. *) + ModelMap.subst id arr_val mdl ) cache.array_selects model in { Models.propositional = prop_model; model; term_values = mrepr } diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index d0ec32d90..035620094 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -89,6 +89,10 @@ type mode_error = | Invalid_set_option of string | Forbidden_command of string +type model_error = + | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_not_model_term of Expr.t + type error = | Parser_error of string | Lexical_error of Loc.t * string @@ -98,6 +102,7 @@ type error = | Warning_as_error | Dolmen_error of (int * string) | Mode_error of Util.mode * mode_error + | Model_error of model_error exception Error of error @@ -252,6 +257,18 @@ let report_mode_error fmt = function | Forbidden_command s -> fprintf fmt "Command %s" s +let report_model_error ppf = function + | Subst_type_clash (id, ty1, ty2) -> + Fmt.pf ppf + "Cannot substitute the identifier %a of type %a by an expression of \ + type %a" + Id.pp id + Ty.pp_smtlib ty1 + Ty.pp_smtlib ty2 + + | Subst_not_model_term e -> + Fmt.pf ppf "The expression %a is not a model term" Expr.print e + let report fmt = function | Parser_error s -> Format.fprintf fmt "Parser Error: %s" s; @@ -277,3 +294,4 @@ let report fmt = function "Invalid action during %a mode: %a" Util.pp_mode mode report_mode_error merr; + | Model_error err -> report_model_error fmt err diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index b0ca4ddc0..f9d8284e9 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -97,6 +97,11 @@ type mode_error = | Invalid_set_option of string | Forbidden_command of string +(** Errors raised while using models. *) +type model_error = + | Subst_type_clash of Id.t * Ty.t * Ty.t + | Subst_not_model_term of Expr.t + (** All types of error that can be raised *) type error = | Parser_error of string (** Error used at parser loading *) @@ -107,9 +112,13 @@ type error = | Warning_as_error | Dolmen_error of (int * string) (** Error code + description raised by dolmen. *) + | Mode_error of Util.mode * mode_error (** Error used when performing actions forbidden in some modes. *) + | Model_error of model_error + (** Error raised while using models. *) + (** {2 Exceptions } *) exception Error of error diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 5e54ef036..1582c3820 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -440,6 +440,10 @@ module SmtPrinter = struct | Sy.False, [] -> Fmt.pf ppf "false" + | Sy.Name { hs = n; _ }, [] + when Id.Namespace.Abstract.is_id (Hstring.view n) -> + Fmt.pf ppf "(as %a %a)" Id.pp n Ty.pp_smtlib ty + | Sy.Name { hs = n; _ }, [] -> Symbols.pp_name ppf (Hstring.view n) | Sy.Name { hs = n; _ }, _ :: _ -> @@ -903,6 +907,10 @@ let void = mk_term (Sy.Void) [] Ty.Tunit let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty +let mk_abstract ty = + let id = Id.Namespace.Abstract.fresh () |> Hstring.make in + mk_term (Sy.Name { hs = id; defined = false; kind = Other }) [] ty + let is_internal_name t = match t with | { f; xs = []; _ } -> Sy.is_fresh_internal_name f @@ -1025,7 +1033,7 @@ let mk_ite cond th el = let rec is_model_term e = match e.f, e.xs with - | (Op Constr _ | Op Record), xs -> List.for_all is_model_term xs + | (Op Constr _ | Op Record | Op Set), xs -> List.for_all is_model_term xs | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index aa7d0d36d..4f62f992b 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -202,6 +202,11 @@ val int : string -> t val real : string -> t val bitv : string -> Ty.t -> t val fresh_name : Ty.t -> t + +val mk_abstract : Ty.t -> t +(** [mk_abstract ty] creates an abstract model term of type [ty]. + This function is intended to be used only in models. *) + val pred : t -> t (** smart constructors for literals *) diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index 78a9992d3..e34de223f 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -30,6 +30,8 @@ type t = Hstring.t [@@deriving ord] +let equal = Hstring.equal + let pp ppf id = Dolmen.Smtlib2.Script.Poly.Print.id ppf (Dolmen.Std.Name.simple (Hstring.view id)) diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli index 900f05dc9..0b2434918 100644 --- a/src/lib/structures/id.mli +++ b/src/lib/structures/id.mli @@ -30,6 +30,7 @@ type t = Hstring.t [@@deriving ord] +val equal : t -> t -> bool val show : t -> string val pp : t Fmt.t diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index 33e731057..2b7fb096f 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -33,40 +33,17 @@ module Sy = Symbols type sy = Id.t * Ty.t list * Ty.t [@@deriving ord] -module Value = struct - type t = - | Abstract of Id.t * Ty.t - | Store of t * t * t - | Constant of Expr.t - [@@deriving ord] - - let rec pp ppf v = - match v with - | Abstract (id, ty) -> - Fmt.pf ppf "(as %a %a)" Id.pp id Ty.pp_smtlib ty - | Store (arr, i, v) -> - Fmt.pf ppf "(@[store@ %a@ %a %a)@]" - pp arr pp i pp v - | Constant e -> - Expr.pp_smtlib ppf e - - module Map = Map.Make (struct - type nonrec t = t - - let compare = compare - end) -end - module Graph = struct module M = Map.Make (struct - type t = Value.t list [@@deriving ord] + type t = Expr.t list [@@deriving ord] end) - type t = Value.t M.t + type t = Expr.t M.t let empty = M.empty let add = M.add + let map = M.map (* A fiber of the function [f] over a value [v] is the set of all the values in the domain of [f] whose the image by [f] is [v]. @@ -75,11 +52,11 @@ module Graph = struct non-empty fibers of the function represented by its graph. *) module Fiber = struct include Set.Make (struct - type t = Value.t list [@@deriving ord] + type t = Expr.t list [@@deriving ord] end) let pp_arg ppf (ctr, arg) = - Fmt.pf ppf "(= arg_%i %a)" ctr Value.pp arg + Fmt.pf ppf "(= arg_%i %a)" ctr Expr.pp_smtlib arg (* For an argument (x_1, ..., x_n) of the function represented by the graph, prints the SMT-LIB formula: @@ -112,26 +89,26 @@ module Graph = struct (* Compute all the fibers of the function represented by the graph. *) let inverse graph = M.fold (fun arg_vals ret_val acc -> - match Value.Map.find_opt ret_val acc with + match Expr.Map.find_opt ret_val acc with | Some fib -> - Value.Map.add ret_val (Fiber.add arg_vals fib) acc + Expr.Map.add ret_val (Fiber.add arg_vals fib) acc | None -> - Value.Map.add ret_val (Fiber.of_list [arg_vals]) acc - ) graph Value.Map.empty + Expr.Map.add ret_val (Fiber.of_list [arg_vals]) acc + ) graph Expr.Map.empty let pp_inverse ppf rel = let rec aux ppf seq = match seq () with | Seq.Nil -> () | Cons ((ret_val, _), seq) when Stdcompat.Seq.is_empty seq -> - Fmt.pf ppf "%a" Value.pp ret_val + Fmt.pf ppf "%a" Expr.pp_smtlib ret_val | Cons ((ret_val, fiber), seq) -> Fmt.pf ppf "(@[ite %a@ %a@ %a)@]" Fiber.pp fiber - Value.pp ret_val + Expr.pp_smtlib ret_val aux seq in - aux ppf (Value.Map.to_seq rel) + aux ppf (Expr.Map.to_seq rel) end module P = Map.Make @@ -157,13 +134,33 @@ let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } = let empty ~suspicious = { values = P.empty; suspicious } +let rec subst_in_term id e c = + let Expr.{ f; xs; ty = ty'; _ } = Expr.term_view c in + match f, xs with + | Sy.Name { hs = id'; _ }, [] when Id.equal id id' -> + let ty = Expr.type_info e in + if not @@ Ty.equal ty ty' then + raise (Errors.Error (Model_error (Subst_type_clash (id, ty', ty)))); + e + | _ -> + begin + let xs = List.map (subst_in_term id e) xs in + Expr.mk_term f xs ty' + end + +let subst id e { values; suspicious } = + if not @@ Expr.is_model_term e then + raise (Errors.Error (Model_error (Subst_not_model_term e))); + let values = P.map (Graph.map (subst_in_term id e)) values in + { values; suspicious } + let pp_named_arg_ty ~unused ppf (arg_name, arg_ty) = let pp_unused ppf unused = if unused then Fmt.pf ppf "_" else () in Fmt.pf ppf "(%aarg_%i %a)" pp_unused unused arg_name Ty.pp_smtlib arg_ty let pp_define_fun ppf ((id, arg_tys, ret_ty), graph) = let inverse_rel = Graph.inverse graph in - let is_constant = Value.Map.cardinal inverse_rel = 1 in + let is_constant = Expr.Map.cardinal inverse_rel = 1 in let named_arg_tys = List.mapi (fun i arg_ty -> (i, arg_ty)) arg_tys in Fmt.pf ppf "(@[define-fun %a (%a) %a@ %a)@]" Id.pp id diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index d7421ed67..9d8e9f0ec 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -34,23 +34,10 @@ type sy = Id.t * Ty.t list * Ty.t - The types of its arguments. - The returned type. *) -module Value : sig - type t = - | Abstract of Id.t * Ty.t - | Store of t * t * t - | Constant of Expr.t - (** [Constant e] represents a constant value [e]. The expression - [e] is always a constant according to [Expr.is_model_term]. *) - - val pp : t Fmt.t - (** [pp ppf v] prints the model value [v] on the formatter [ppf] using the - SMT-LIB format. *) -end - type t (** Type of model. *) -val add : sy -> Value.t list -> Value.t -> t -> t +val add : sy -> Expr.t list -> Expr.t -> t -> t (** [add sy args ret mdl] adds the binding [args -> ret] to the partial graph associated with the symbol [sy]. *) @@ -59,6 +46,13 @@ val empty : suspicious:bool -> t model may be wrong as it involves symbols from theories for which the model generation is known to be incomplete. *) +val subst : Id.t -> Expr.t -> t -> t +(** [subst id e mdl] substitutes all the occurrences of the identifier [id] + in the model [mdl] by the model term [e]. + + @Raise Error if the expression [e] is not a model term or the type of + [e] doesn't agree with some occurrence of [id] in the model. *) + val pp : t Fmt.t (** [pp ppf mdl] prints the model [mdl] on the formatter [ppf] using the SMT-LIB format. *) diff --git a/tests/dune.inc b/tests/dune.inc index 9e960611d..26d82ad68 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -210019,6 +210019,27 @@ ; Auto-generated part begin (subdir models/array + (rule + (target embedded-array.models_dolmen.output) + (deps (:input embedded-array.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 embedded-array.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff embedded-array.models.expected embedded-array.models_dolmen.output))) (rule (target array1.models_dolmen.output) (deps (:input array1.models.smt2)) diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected new file mode 100644 index 000000000..dd6a80ae9 --- /dev/null +++ b/tests/models/array/embedded-array.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun s () S (as @a0 S)) + (define-fun x () Pair + (pair (store (as @a1 (Array Int S)) 0 s) + (store (as @a1 (Array Int S)) 0 s))) +) diff --git a/tests/models/array/embedded-array.models.smt2 b/tests/models/array/embedded-array.models.smt2 new file mode 100644 index 000000000..fa76cb828 --- /dev/null +++ b/tests/models/array/embedded-array.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-sort S 0) +(declare-const s S) +(declare-datatype Pair ((pair (first (Array Int S)) (second (Array Int S))))) +(declare-const x Pair) +(assert (= (select (first x) 0) s)) +(assert (= (first x) (second x))) +(check-sat) +(get-model)