From 959bf7b5a53e037d6bda8c8699cae94cd635eaa9 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 2 Jan 2024 11:11:36 +0100 Subject: [PATCH] Generate complete model This PR fixes the issue #778. The suggested solution by this PR is as follows: - Collect user-declared symbols in `D_cnf`; - As the function `make` of the module `D_cnf` returns a list of commands, we add a new command `Decl` in `Frontend` to declare symbols; - The declared symbols are given to the SAT solver through a new function `declaration` in `sat_solver_sig`. - These symbols are collected in vectors and we keep indexes in another PR in order to manage properly the push/pop mechanism. - Finally the declared symbols are given to `Uf` and we create the empty model with them. Another annoying point comes from the current datastructure used in `ModelMap`. The type of `ModelMap` saves model values in the form of graphs. A graph is a finite set of constraints but there is no appropriate representation for the graph without constraints. Let's imagine we have the input: ```smt2 (set-option :produce-models true) (set-logic ALL) (declare-fun (Int) Int) (check-sat) (get-model) ``` We expect an output as follows: ```smt2 ( (define-fun f (_x Int) (@a as Int)) ) ``` But `Graph.empty` cannot hold the abstract value `@a`. A naive solution consists in using an ADT: ```ocaml type graph = | Empty of Id.typed | G of Graph.t ``` But we'll add an extra indirection. Probably the best solution would be to use a custom datastructure instead of a map to store the constraints. In this PR, we detect in `ModelMap.add` if the only constraint in the graph is of the form `something -> abstract value`. In this case we remove this constraint. This solution isn't perfect as explained in issue #1018. The biggest drawback of this solution is the fact we have to declare symbols in the SAT API, otherwise models returned by `get_model` could be incomplete. --- src/lib/frontend/d_cnf.ml | 58 ++++++++++++++----- src/lib/frontend/frontend.ml | 8 +++ src/lib/frontend/models.ml | 2 +- src/lib/reasoners/ccx.ml | 9 ++- src/lib/reasoners/ccx.mli | 5 +- src/lib/reasoners/fun_sat.ml | 14 ++++- src/lib/reasoners/fun_sat.mli | 2 + src/lib/reasoners/fun_sat_frontend.ml | 3 + src/lib/reasoners/sat_solver_sig.ml | 7 +++ src/lib/reasoners/sat_solver_sig.mli | 7 +++ src/lib/reasoners/satml_frontend.ml | 16 ++++- src/lib/reasoners/theory.ml | 11 +++- src/lib/reasoners/theory.mli | 5 +- src/lib/reasoners/uf.ml | 8 +-- src/lib/reasoners/uf.mli | 6 +- src/lib/structures/commands.ml | 7 +++ src/lib/structures/commands.mli | 1 + src/lib/structures/id.ml | 4 ++ src/lib/structures/id.mli | 2 + src/lib/structures/modelMap.ml | 41 ++++++++++++- src/lib/structures/modelMap.mli | 2 +- tests/cram.t/run.t | 3 +- tests/dune.inc | 21 +++++++ tests/issues/555.models.expected | 4 +- tests/issues/854/function.models.expected | 2 +- tests/issues/854/original.models.expected | 2 +- tests/issues/854/twice_eq.models.expected | 4 +- tests/models/arith/arith11.optimize.expected | 1 + tests/models/array/array1.models.expected | 4 +- .../array/embedded-array.models.expected | 6 +- tests/models/bool/bool2.models.expected | 1 + tests/models/complete_models.models.expected | 36 ++++++++++++ tests/models/complete_models.models.smt2 | 24 ++++++++ 33 files changed, 276 insertions(+), 50 deletions(-) create mode 100644 tests/models/complete_models.models.expected create mode 100644 tests/models/complete_models.models.smt2 diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index c7545a8ee..259c737ab 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -53,6 +53,12 @@ module HT = Hashtbl.Make( let hash = Fun.id end) +module DeclSet = Set.Make + (struct + type t = Id.typed + let compare = Id.compare_typed + end) + (** Helper function: returns the basename of a dolmen path, since in AE the problems are contained in one-file (for now at least), the path is irrelevant and only the basename matters *) @@ -701,8 +707,15 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) = end in Cache.store_sy tcst sy; + Cache.store_ty_vars id_ty; (* Adding polymorphic types to the cache. *) - Cache.store_ty_vars id_ty + let arg_tys, ret_ty = + match DT.view id_ty with + | `Arrow (arg_tys, ret_ty) -> + List.map dty_to_ty arg_tys, dty_to_ty ret_ty + | _ -> [], dty_to_ty id_ty + in + (Hstring.make name, arg_tys, ret_ty) (** Handles the definitions of a list of mutually recursive types. - If one of the types is an ADT, the ADTs that have only one case are @@ -2087,14 +2100,24 @@ let make dloc_file acc stmt = assert false ) defs - | {contents = `Decls [td]; _ } -> - begin match td with - | `Type_decl (td, _def) -> mk_ty_decl td - | `Term_decl td -> mk_term_decl td - end; - acc + | {contents = `Decls [td]; loc; _ } -> + let decl = match td with + | `Type_decl (td, _def) -> + mk_ty_decl td; + None + + | `Term_decl td -> + Some (mk_term_decl td) + in + begin match decl with + | Some d -> + let st_loc = dl_to_ael dloc_file loc in + C.{ st_decl = Decl d; st_loc } :: acc + | None -> + acc + end - | {contents = `Decls dcl; _ } -> + | {contents = `Decls dcl; loc; _ } -> let rec aux acc tdl = (* for now, when acc has more than one element it is assumed that the types are mutually recursive. Which is not necessarily the case. @@ -2107,21 +2130,24 @@ let make dloc_file acc stmt = | [otd] -> mk_ty_decl otd | _ -> mk_mr_ty_decls (List.rev acc) end; - mk_term_decl td; - aux [] tl + let st_loc = dl_to_ael dloc_file loc in + C.{ st_decl = Decl (mk_term_decl td); st_loc } :: aux [] tl | `Type_decl (td, _def) :: tl -> aux (td :: acc) tl | [] -> - begin match acc with - | [] -> () - | [otd] -> mk_ty_decl otd - | _ -> mk_mr_ty_decls (List.rev acc) + begin + let () = + match acc with + | [] -> () + | [otd] -> mk_ty_decl otd + | _ -> mk_mr_ty_decls (List.rev acc) + in + [] end in - aux [] dcl; - acc + aux [] dcl @ acc | { contents = `Set_logic _ | `Set_info _ | `Get_info _ ; _ } -> acc diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 10808c3cf..bf5738549 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -302,6 +302,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc}) else Ex.empty + let internal_decl ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit = + ignore loc; + match env.res with + | `Sat | `Unknown -> + SAT.declare env.sat_env id + | `Unsat -> () + let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit = ignore loc; Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack) @@ -443,6 +450,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct let process_decl ?(hook_on_status=(fun _ -> ignore)) env d = try match d.st_decl with + | Decl id -> check_if_over (internal_decl ~loc:d.st_loc id) env | Push n -> check_if_over (internal_push ~loc:d.st_loc n) env | Pop n -> check_if_over (internal_pop ~loc:d.st_loc n) env | Assume (n, f, mf) -> diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 457475278..eefc11ce7 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -43,7 +43,7 @@ type t = { let empty = { propositional = Expr.Set.empty; - model = ModelMap.empty ~suspicious:false; + model = ModelMap.empty ~suspicious:false []; term_values = Expr.Map.empty; } diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index b52c4327c..9eebb0527 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -86,7 +86,10 @@ module type S = sig Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t -> t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances - val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t + val extract_concrete_model : + prop_model:Expr.Set.t -> + declared_ids:Id.typed list -> + t -> Models.t end @@ -748,6 +751,6 @@ module Main : S = struct in Uf.term_repr env.uf t - let extract_concrete_model ~prop_model env = - Uf.extract_concrete_model ~prop_model env.uf + let extract_concrete_model ~prop_model ~declared_ids env = + Uf.extract_concrete_model ~prop_model ~declared_ids env.uf end diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index 6d6894a17..e8844ac96 100644 --- a/src/lib/reasoners/ccx.mli +++ b/src/lib/reasoners/ccx.mli @@ -77,7 +77,10 @@ module type S = sig Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t -> t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances - val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t + val extract_concrete_model : + prop_model:Expr.Set.t -> + declared_ids:Id.typed list -> + t -> Models.t end diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index d943a0045..5e3a73ca0 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -177,6 +177,8 @@ module Make (Th : Theory.S) = struct unit_facts_cache : (E.gformula * Ex.t) ME.t ref; last_saved_model : Models.t Lazy.t option ref; unknown_reason : Sat_solver_sig.unknown_reason option; + declare_ids : Id.typed Vec.t; + declare_lim : int Vec.t; } let reset_refs () = @@ -1123,7 +1125,8 @@ module Make (Th : Theory.S) = struct else begin try (* also performs case-split and pushes pending atoms to CS *) - let model, _ = Th.compute_concrete_model env.tbox in + let declared_ids = Vec.to_list env.declare_ids in + let model, _ = Th.compute_concrete_model ~declared_ids env.tbox in env.last_saved_model := Some model; env with Ex.Inconsistent (expl, classes) -> @@ -1611,6 +1614,10 @@ module Make (Th : Theory.S) = struct "solved with backward!"; raise e + let declare env id = + Vec.push env.declare_ids id; + env + let push env to_push = if Options.get_tableaux_cdcl () then Errors.run_error @@ -1626,6 +1633,7 @@ module Make (Th : Theory.S) = struct let guards = ME.add new_guard (mk_gf new_guard "" true true,Ex.empty) acc.guards.guards in + Vec.push env.declare_lim (Vec.size env.declare_ids); {acc with guards = { acc.guards with current_guard = new_guard; @@ -1656,6 +1664,8 @@ module Make (Th : Theory.S) = struct in acc.model_gen_phase := false; env.last_saved_model := None; + let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in + Vec.shrink env.declare_ids lim; {acc with inst; guards = { acc.guards with @@ -1837,6 +1847,8 @@ module Make (Th : Theory.S) = struct add_inst = selector; last_saved_model = ref None; unknown_reason = None; + declare_ids = Vec.make 17 ~dummy:Id.dummy_typed; + declare_lim = Vec.make 17 ~dummy:(-1); } in assume env gf_true Ex.empty diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli index 1e9ba0719..93264b351 100644 --- a/src/lib/reasoners/fun_sat.mli +++ b/src/lib/reasoners/fun_sat.mli @@ -38,6 +38,8 @@ module Make (Th : Theory.S) : sig val empty : ?selector:(Expr.t -> bool) -> unit -> t + val declare : t -> Id.typed -> t + val push : t -> int -> t val pop : t -> int -> t diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml index 789854334..ef5c7e921 100644 --- a/src/lib/reasoners/fun_sat_frontend.ml +++ b/src/lib/reasoners/fun_sat_frontend.ml @@ -45,6 +45,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | FS.Unsat expl -> raise (Unsat expl) | FS.I_dont_know e -> env := e; raise I_dont_know + let declare t id = + t := FS.declare !t id + let push t i = exn_handler (fun env -> t := FS.push env i) t let pop t i = exn_handler (fun env -> t := FS.pop env i) t diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index d6c568215..d5ff19deb 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -78,6 +78,13 @@ module type S = sig The optional argument [selector] is used to filter ground facts discovered by the instantiation engine. *) + val declare : t -> Id.typed -> unit + (** [declare env id] declares a new identifier [id]. + + If the environment [env] isn't unsatisfiable and the model generation + is enabled, the solver produces a model term for [id] which can be + retrieved with [get_model]. *) + val push : t -> int -> unit (** [push env n] adds [n] new assertion levels in [env]. diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 7b6939fcd..852308080 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -58,6 +58,13 @@ module type S = sig The optional argument [selector] is used to filter ground facts discovered by the instantiation engine. *) + val declare : t -> Id.typed -> unit + (** [declare env id] declares a new identifier [id]. + + If the environment [env] isn't unsatisfiable and the model generation + is enabled, the solver produces a model term for [id] which can be + retrieved with [get_model]. *) + val push : t -> int -> unit (** [push env n] adds [n] new assertion levels in [env]. diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 6547ddde6..6dfda28ce 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -67,6 +67,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct mutable unknown_reason : Sat_solver_sig.unknown_reason option; (** The reason why satml raised [I_dont_know] if it does; [None] by default. *) + declare_ids : Id.typed Vec.t; + declare_lim : int Vec.t; } let empty_guards () = { @@ -97,6 +99,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct last_saved_model = None; last_saved_objectives = None; unknown_reason = None; + declare_ids = Vec.make 17 ~dummy:Id.dummy_typed; + declare_lim = Vec.make 17 ~dummy:(-1); } exception Sat @@ -965,8 +969,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct if compute then begin try (* also performs case-split and pushes pending atoms to CS *) + let declared_ids = Vec.to_list env.declare_ids in let model, objectives = - Th.compute_concrete_model (SAT.current_tbox env.satml) + Th.compute_concrete_model ~declared_ids (SAT.current_tbox env.satml) in env.last_saved_model <- Some model; env.last_saved_objectives <- Some objectives; @@ -1204,6 +1209,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct expr_guard, atom_guard | _ -> assert false + let declare env id = Vec.push env.declare_ids id + let push env to_push = Util.loop ~f:(fun _n () () -> try @@ -1211,7 +1218,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct SAT.push env.satml atom_guard; Stack.push expr_guard env.guards.stack_guard; Steps.push_steps (); - env.guards.current_guard <- expr_guard + env.guards.current_guard <- expr_guard; + Vec.push env.declare_lim (Vec.size env.declare_ids) with | Util.Step_limit_reached _ -> (* This function should be called without step limit @@ -1234,7 +1242,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct env.last_saved_model <- None; env.last_saved_objectives <- None; env.inst <- inst; - env.guards.current_guard <- b + env.guards.current_guard <- b; + let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in + Vec.shrink env.declare_ids lim ) ~max:to_pop ~elt:() diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 4c5a76ff6..1d721a77f 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -61,7 +61,10 @@ module type S = sig val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t val add_term : t -> Expr.t -> add_in_cs:bool -> t - val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t + val compute_concrete_model : + t -> + declared_ids:Id.typed list -> + Models.t Lazy.t * Objective.Model.t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t val theories_instances : @@ -879,13 +882,14 @@ module Main_Default : S = struct let get_real_env t = t.gamma let get_case_split_env t = t.gamma_finite - let compute_concrete_model env = + let compute_concrete_model env ~declared_ids = let { gamma_finite; assumed_set; objectives; _ }, _ = do_case_split_aux env ~for_model:true in lazy ( CC_X.extract_concrete_model ~prop_model:assumed_set + ~declared_ids gamma_finite ), objectives @@ -940,7 +944,8 @@ module Main_Empty : S = struct let get_case_split_env _ = CC_X.empty let do_case_split env _ = env, E.Set.empty let add_term env _ ~add_in_cs:_ = env - let compute_concrete_model _env = lazy Models.empty, Objective.Model.empty + let compute_concrete_model _env ~declared_ids:_ = + lazy Models.empty, Objective.Model.empty let assume_th_elt e _ _ = e let theories_instances ~do_syntactic_matching:_ _ e _ _ _ = e, [] diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index c7e8f71eb..c0f916c74 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -54,7 +54,10 @@ module type S = sig val add_term : t -> Expr.t -> add_in_cs:bool -> t - val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t + val compute_concrete_model : + t -> + declared_ids:Id.typed list -> + Models.t Lazy.t * Objective.Model.t val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t val theories_instances : diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index c22bcff25..d0f106108 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1167,11 +1167,11 @@ let compute_concrete_model_of_val cache = let extract_concrete_model cache = let compute_concrete_model_of_val = compute_concrete_model_of_val cache in let get_abstract_for = Cache.get_abstract_for cache.abstracts - in fun ~prop_model env -> + in fun ~prop_model ~declared_ids env -> let terms, suspicious = terms env in let model, mrepr = MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc) - terms (ModelMap.empty ~suspicious, ME.empty) + terms (ModelMap.empty ~suspicious declared_ids, ME.empty) in let model = Hashtbl.fold (fun t vals mdl -> @@ -1212,9 +1212,9 @@ let extract_concrete_model cache = in { Models.propositional = prop_model; model; term_values = mrepr } -let extract_concrete_model ~prop_model = +let extract_concrete_model ~prop_model ~declared_ids = let cache : cache = { array_selects = Hashtbl.create 17; abstracts = Hashtbl.create 17; } - in fun env -> extract_concrete_model cache ~prop_model env + in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index 40fd47cd1..9eef6b30c 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -72,7 +72,11 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t (** {2 Counterexample function} *) (** Compute a counterexample using the Uf environment *) -val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t +val extract_concrete_model : + prop_model:Expr.Set.t -> + declared_ids:Id.typed list -> + t -> + Models.t (** saves the module's cache *) val save_cache : unit -> unit diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index c539128ba..5c26fa59b 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -31,6 +31,7 @@ (* Sat entry *) type sat_decl_aux = + | Decl of Id.typed | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t Typed.rwt_rule) list @@ -46,6 +47,12 @@ type sat_tdecl = { } let print_aux fmt = function + | Decl (id, arg_tys, ret_ty) -> + Fmt.pf fmt "declare %a with type (%a) -> %a" + Id.pp id + Fmt.(list ~sep:comma Ty.print) arg_tys + Ty.print ret_ty + | Assume (name, e, b) -> Format.fprintf fmt "assume %s(%b): @[%a@]" name b Expr.print e | PredDef (e, name) -> diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index 320da889c..800c58f10 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -31,6 +31,7 @@ (* Sat entry *) type sat_decl_aux = + | Decl of Id.typed | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t Typed.rwt_rule) list diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index e6d8a74f3..62624c385 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -81,3 +81,7 @@ module Namespace = struct Skolem.reset_fresh_cpt (); Abstract.reset_fresh_cpt () end + +let dummy_typed = + let id = Namespace.Internal.fresh () |> Hstring.make in + (id, [], Ty.Tunit) diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli index a011bd36e..a48fc43c8 100644 --- a/src/lib/structures/id.mli +++ b/src/lib/structures/id.mli @@ -36,6 +36,8 @@ type typed = t * Ty.t list * Ty.t - Types of its arguments. - The returned type. *) +val dummy_typed : typed + val compare_typed : typed -> typed -> int val equal : t -> t -> bool val show : t -> string diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index e28af0ef3..8a0e68928 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -42,6 +42,8 @@ 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]. @@ -125,12 +127,45 @@ 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 P.find sy values with Not_found -> Graph.empty in + 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 { values; suspicious } -let empty ~suspicious = { values = P.empty; suspicious } +module DeclSets = Set.Make + (struct + type t = Id.typed + let compare = Id.compare_typed + end) + +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 + ) + P.empty declared_ids + in + { values; suspicious } let rec subst_in_term id e c = let Expr.{ f; xs; ty = ty'; _ } = Expr.term_view c in diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index b0f90b7f1..b2d03124c 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -35,7 +35,7 @@ val add : Id.typed -> 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]. *) -val empty : suspicious:bool -> t +val empty : suspicious:bool -> Id.typed list -> t (** An empty model. The [suspicious] flag is used to remember that this model may be wrong as it involves symbols from theories for which the model generation is known to be incomplete. *) diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 1aa6dc1e5..6e3bf96b8 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -12,7 +12,8 @@ appropriate here. ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (as @a3 (Array Int Int))) ) Now we will test some semantic triggers. diff --git a/tests/dune.inc b/tests/dune.inc index 26d82ad68..e5b9775fc 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -209726,6 +209726,27 @@ ; Auto-generated part begin (subdir models + (rule + (target complete_models.models_dolmen.output) + (deps (:input complete_models.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 complete_models.models_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff complete_models.models.expected complete_models.models_dolmen.output))) (rule (target check_sat.models_dolmen.output) (deps (:input check_sat.models.ae)) diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected index 086ba7ffb..b35225efb 100644 --- a/tests/issues/555.models.expected +++ b/tests/issues/555.models.expected @@ -3,6 +3,6 @@ unknown ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) ) diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected index bb0b49fe0..88a28c7d8 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 @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 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 9198abbbf..8fbfb8105 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 @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 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 f18c7f58e..c51afd4a7 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 @a0 intref)) - (define-fun another_mk ((_arg_0 Int)) intref (as @a0 intref)) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref)) + (define-fun another_mk ((_arg_0 Int)) intref (as @a6 intref)) (define-fun a () Int 0) (define-fun a1 () Int 0) ) diff --git a/tests/models/arith/arith11.optimize.expected b/tests/models/arith/arith11.optimize.expected index 99f7450f0..722135b53 100644 --- a/tests/models/arith/arith11.optimize.expected +++ b/tests/models/arith/arith11.optimize.expected @@ -4,6 +4,7 @@ unknown (define-fun p1 () Bool false) (define-fun p2 () Bool true) (define-fun x () Real 2.0) + (define-fun y () Real (as @a3 Real)) ) (objectives (x 2.0) diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected index 086ba7ffb..b35225efb 100644 --- a/tests/models/array/array1.models.expected +++ b/tests/models/array/array1.models.expected @@ -3,6 +3,6 @@ unknown ( (define-fun x () Int 0) (define-fun y () Int 0) - (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0)) - (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0)) + (define-fun a1 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) ) diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected index dd6a80ae9..057bc1a6c 100644 --- a/tests/models/array/embedded-array.models.expected +++ b/tests/models/array/embedded-array.models.expected @@ -1,8 +1,8 @@ unknown ( - (define-fun s () S (as @a0 S)) + (define-fun s () S (as @a2 S)) (define-fun x () Pair - (pair (store (as @a1 (Array Int S)) 0 s) - (store (as @a1 (Array Int S)) 0 s))) + (pair (store (as @a3 (Array Int S)) 0 s) + (store (as @a3 (Array Int S)) 0 s))) ) diff --git a/tests/models/bool/bool2.models.expected b/tests/models/bool/bool2.models.expected index e0f6879b8..7d4b0eed7 100644 --- a/tests/models/bool/bool2.models.expected +++ b/tests/models/bool/bool2.models.expected @@ -2,6 +2,7 @@ unknown ( (define-fun x () Bool false) + (define-fun y () Bool (as @a1 Bool)) ) ((notx true)) diff --git a/tests/models/complete_models.models.expected b/tests/models/complete_models.models.expected new file mode 100644 index 000000000..49667d5f1 --- /dev/null +++ b/tests/models/complete_models.models.expected @@ -0,0 +1,36 @@ + +unknown +( + (define-fun x () Int (as @a0 Int)) +) + +unknown +( + (define-fun x () Int 5) + (define-fun y () Int (as @a2 Int)) +) + +unknown +( + (define-fun x () Int 6) +) + +unknown +( + (define-fun x () Int 6) + (define-fun z () S (as @a5 S)) +) + +unknown +( + (define-fun x () Int 6) + (define-fun z () S (as @a7 S)) + (define-fun f ((_arg_0 Int)) Int (as @a9 Int)) +) + +unknown +( + (define-fun x () Int 6) + (define-fun z () S (as @a11 S)) + (define-fun f ((_arg_0 Int)) Int 2) +) diff --git a/tests/models/complete_models.models.smt2 b/tests/models/complete_models.models.smt2 new file mode 100644 index 000000000..c65cf1d89 --- /dev/null +++ b/tests/models/complete_models.models.smt2 @@ -0,0 +1,24 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-const x Int) +(check-sat) +(get-model) +(push 1) +(declare-const y Int) +(assert (= x 5)) +(check-sat) +(get-model) +(pop 1) +(assert (= x 6)) +(check-sat) +(get-model) +(declare-sort S 0) +(declare-const z S) +(check-sat) +(get-model) +(declare-fun f (Int) Int) +(check-sat) +(get-model) +(assert (= (f 5) 2)) +(check-sat) +(get-model)