From 48cf7d01a99221e54c6c8ac52868fc6fa0dc0416 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 3 Jan 2024 09:32:55 +0100 Subject: [PATCH] Use an ADT to discriminate free graph and constant graph --- src/lib/structures/modelMap.ml | 99 +++++++++++++---------- tests/issues/854/function.models.expected | 2 +- tests/issues/854/original.models.expected | 2 +- tests/issues/854/twice_eq.models.expected | 4 +- tests/models/complete_2.models.expected | 4 +- 5 files changed, 62 insertions(+), 49 deletions(-) diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index 2e377928d5..c4cd5134f7 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -31,7 +31,14 @@ module X = Shostak.Combine module Sy = Symbols -module Graph = struct +(* The type of this module represents a model value for a function [f] by a + finite set of constraints of the form: + f(e_1, ..., e_n) = e + where [e_i] and [e] are model terms according to [Expr.is_model_term]. + + As functions in the SMT-LIB standard are total, one of the expressions [e] + above is used as the default value of the function. *) +module Constraints = struct module M = Map.Make (struct type t = Expr.t list [@@deriving ord] @@ -42,14 +49,12 @@ module Graph = struct let empty = M.empty let add = M.add let map = M.map - let cardinal = M.cardinal - let choose = M.choose (* 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]. The function [inverse] of this module constructs a map of all the - non-empty fibers of the function represented by its graph. *) + non-empty fibers of the function represented by a set of constraints. *) module Fiber = struct include Set.Make (struct type t = Expr.t list [@@deriving ord] @@ -58,8 +63,8 @@ module Graph = struct let pp_arg ppf (ctr, 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: + (* For an argument (x_1, ..., x_n) of the function, prints the SMT-LIB + formula: (and (= arg_0 x_1)(= arg_1 x2) ... (= arg_n x_n)). *) let pp_args ppf = function @@ -69,8 +74,7 @@ module Graph = struct | args -> Fmt.pf ppf "(and %a)" Fmt.(iter_bindings ~sep:sp List.iteri pp_arg) args - (* For a fiber [x; y; z; ...] of the function represented by the graph, - prints the SMT-LIB formula: + (* For a fiber [x; y; z; ...] of the function, prints the SMT-LIB formula: (or (and (= arg_0 x_0) (= arg_1 x_1) ...) (and (= arg_0 y_0) (= arg_1 y_1) ...) @@ -86,17 +90,18 @@ module Graph = struct Fmt.pf ppf "(or %a)" (Fmt.iter ~sep:Fmt.sp iter pp_args) fiber end - (* Compute all the fibers of the function represented by the graph. *) - let inverse graph = + (* Compute all the fibers of the function represented by the set of + constraints [c]. *) + let inverse c = M.fold (fun arg_vals ret_val acc -> match Expr.Map.find_opt ret_val acc with | Some fib -> Expr.Map.add ret_val (Fiber.add arg_vals fib) acc | None -> Expr.Map.add ret_val (Fiber.of_list [arg_vals]) acc - ) graph Expr.Map.empty + ) c Expr.Map.empty - let pp_inverse ppf rel = + let pp_inverse ppf c = let rec aux ppf seq = match seq () with | Seq.Nil -> () @@ -108,7 +113,7 @@ module Graph = struct Expr.pp_smtlib ret_val aux seq in - aux ppf (Expr.Map.to_seq rel) + aux ppf (Expr.Map.to_seq c) end module P = Map.Make @@ -118,8 +123,15 @@ module P = Map.Make let compare = Id.compare_typed end) +type graph = + | Free of Expr.t + (* Represents a graph without any constraint. The expression is + an abstract value. *) + + | C of Constraints.t + type t = { - values : Graph.t P.t; + values : graph P.t; suspicious : bool; } @@ -127,35 +139,21 @@ let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } = if List.compare_lengths arg_tys arg_vals <> 0 then Fmt.invalid_arg "The arity of the symbol %a doesn't agree the number of \ arguments" Id.pp id; - let graph = - try - let graph = P.find sy values in - (* If the graph associated with [sy] contains only an abstract value, - it means there is no constraint on this graph. We replace it by - the graph with the only constraint given by [arg_vals] and - [ret_val]. *) - if Graph.cardinal graph = 1 then - let _, value = Graph.choose graph in - let Expr.{ f; _ } = Expr.term_view value in - match f with - | Sy.Name { hs; _ } - when Id.Namespace.Abstract.is_id (Hstring.view hs) -> - Graph.empty - | _ -> graph - else - graph - with Not_found -> Graph.empty in - let values = P.add sy (Graph.add arg_vals ret_val graph) values in + let constraints = + match P.find sy values with + | C g -> g + | Free _ | exception Not_found -> Constraints.empty + in + let values = + P.add sy (C (Constraints.add arg_vals ret_val constraints)) values + in { values; suspicious } let empty ~suspicious declared_ids = let values = List.fold_left - (fun values ((_, arg_tys, ret_ty) as sy) -> - let arg_vals = List.map Expr.mk_abstract arg_tys in - let ret_val = Expr.mk_abstract ret_ty in - let graph = Graph.add arg_vals ret_val Graph.empty in - P.add sy graph values + (fun values ((_, _, ret_ty) as sy) -> + P.add sy (Free (Expr.mk_abstract ret_ty)) values ) P.empty declared_ids in @@ -178,22 +176,37 @@ let rec subst_in_term id e c = 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 + + let values = + P.map + (fun graph -> + match graph with + | C constraints -> C (Constraints.map (subst_in_term id e) constraints) + | Free a -> Free (subst_in_term id e a) + ) 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 = Expr.Map.cardinal inverse_rel = 1 in +let pp_define_fun ~is_constant pp ppf ((id, arg_tys, ret_ty), a) = 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 Fmt.(list ~sep:sp (pp_named_arg_ty ~unused:is_constant)) named_arg_tys Ty.pp_smtlib ret_ty - Graph.pp_inverse inverse_rel + pp a + +let pp_define_fun ppf (sy, graph) = + match graph with + | Free a -> + pp_define_fun ~is_constant:true Expr.pp_smtlib ppf (sy, a) + + | C constraints -> + let inverse_rel = Constraints.inverse constraints in + let is_constant = Expr.Map.cardinal inverse_rel = 1 in + pp_define_fun ~is_constant Constraints.pp_inverse ppf (sy, inverse_rel) let pp ppf {values; suspicious} = if suspicious then begin diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected index 88a28c7d83..6e5eeb8fb5 100644 --- a/tests/issues/854/function.models.expected +++ b/tests/issues/854/function.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) (define-fun a () Int 0) (define-fun f ((_arg_0 Int)) Int 0) (define-fun a1 () Int 0) diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected index 8fbfb8105b..7d40ab42e2 100644 --- a/tests/issues/854/original.models.expected +++ b/tests/issues/854/original.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected index c51afd4a71..ee4c1de0d3 100644 --- a/tests/issues/854/twice_eq.models.expected +++ b/tests/issues/854/twice_eq.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref)) - (define-fun another_mk ((_arg_0 Int)) intref (as @a6 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/models/complete_2.models.expected b/tests/models/complete_2.models.expected index 1ba0943423..09be592338 100644 --- a/tests/models/complete_2.models.expected +++ b/tests/models/complete_2.models.expected @@ -1,6 +1,6 @@ unknown ( - (define-fun x () Int (as @a2 Int)) - (define-fun f ((_arg_0 Int)) Int (as @a1 Int)) + (define-fun x () Int (as @a1 Int)) + (define-fun f ((_arg_0 Int)) Int (as @a0 Int)) )