diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 0720d28cd7..03cf6b7d97 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -35,7 +35,7 @@ module E = Expr type t = { propositional : Expr.Set.t; model : ModelMap.t; - terms_values : (Shostak.Combine.r * string) Expr.Map.t + terms_values : Expr.t Expr.Map.t } let empty = { diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index 8aa748cfcf..f9e3d42499 100644 --- a/src/lib/frontend/models.mli +++ b/src/lib/frontend/models.mli @@ -33,7 +33,7 @@ type t = { propositional : Expr.Set.t; model : ModelMap.t; - terms_values : (Shostak.Combine.r * string) Expr.Map.t + terms_values : Expr.t Expr.Map.t (** A map from terms to their values in the model (as a representative of type X.r and as a string. *) } diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index dcdb35286d..8144b1eb4f 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -325,7 +325,7 @@ module Make (X : Sig.X) = struct let module SX = Set.Make(struct type t=r let compare = X.hash_cmp end) in let exception Found of Expr.t in fun r distincts eq -> - if List.exists (fun (t,(_:r)) -> Expr.const_term t) eq then + if List.exists (fun (t,(_:r)) -> Expr.is_const_term t) eq then None else (*match X.ac_extract r with diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 6f9bd472ed..fb69af36e1 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -441,9 +441,8 @@ module Shostak (X : ALIEN) = struct "[ADTs.models] assign_value currently not implemented"; raise (Util.Not_implemented "Models for ADTs") - let choose_adequate_model _ _ _ = + let to_const_term _r = Printer.print_err - "[ADTs.models] choose_adequate_model currently not implemented"; + "[ADTs.models] to_const_term currently not implemented"; raise (Util.Not_implemented "Models for ADTs") - end diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 9fa3a8a2f7..15c8aca22e 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -809,49 +809,11 @@ module Shostak cpt := Q.add Q.one (max_constant distincts !cpt); Some (term_of_cst (Q.to_string !cpt), true) - let pp_constant ppf r = + let to_const_term r = match P.is_const (embed r), X.type_info r with - | Some q, Ty.Tint -> - assert (Z.equal (Q.den q) Z.one); - let i = Q.num q in - if Z.sign i = -1 then - Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i) - else - Fmt.pf ppf "%a" Z.pp_print i - | Some q, Ty.Treal -> - if Z.equal (Q.den q) Z.one then - Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) - else if Q.sign q = -1 then - Fmt.pf ppf "(/ (- %a) %a)" - Z.pp_print (Z.abs (Q.num q)) - Z.pp_print (Q.den q) - else - Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) - | _ -> assert false - - let choose_adequate_model t r l = - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Arith" ~function_name:"choose_adequate_model" - "choose_adequate_model for %a" E.print t; - let l = List.filter (fun (_, r) -> P.is_const (embed r) != None) l in - let r = - match l with - | [] -> - (* We do this, because terms of some semantic values created - by CS are not created and added to UF *) - if (P.is_const (embed r) == None) then begin - Printer.print_dbg - ~module_name:"Arith" ~function_name:"choose_adequate_model" - "no adequate model found for %a" X.print r; - assert false - end; - r - - | (_,r)::l -> - List.iter (fun (_,x) -> assert (X.equal x r)) l; - r - in - r, Fmt.str "%a" pp_constant r - + | Some i, Ty.Tint -> + assert (Z.equal (Q.den i) Z.one); + Some (Expr.Ints.of_Z (Q.num i)) + | Some q, Ty.Treal -> Some (Expr.Reals.of_Q q) + | _ -> None end diff --git a/src/lib/reasoners/arrays.ml b/src/lib/reasoners/arrays.ml index 624dbd91e8..b6981c6a96 100644 --- a/src/lib/reasoners/arrays.ml +++ b/src/lib/reasoners/arrays.ml @@ -60,28 +60,12 @@ module Shostak (X : ALIEN) = struct let abstract_selectors _ _ = assert false let solve _ _ = assert false let assign_value r _ eq = - if List.exists (fun (t,_) -> Expr.const_term t) eq then None + if List.exists (fun (t,_) -> Expr.is_const_term t) eq then None else match X.term_extract r with | Some _, true -> Some (Expr.fresh_name (X.type_info r), false) | _ -> assert false - let choose_adequate_model _ _ l = - let acc = - List.fold_left - (fun acc (s, r) -> - if not (Expr.const_term s) then acc - else - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - ) None l - in - match acc with - | Some (_, r) -> - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - - | _ -> assert false - + let to_const_term _r = assert false end diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 6aa75af21f..6e93c62e3f 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1536,34 +1536,14 @@ module Shostak(X : ALIEN) = struct let bv = String.make sz '0' in Some (E.bitv bv (Ty.Tbitv sz), true) - let choose_adequate_model t r l = - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Bitv" ~function_name:"choose_adequate_model" - "choose_adequate_model for %a" E.print t; - let l = List.map (fun (t, r) -> (t, r, embed r)) l in - let l = List.filter (fun (_, _, a) -> is_cte_abstract a) l in - let r, a = - match l with - | [] -> - let a = embed r in - assert (is_cte_abstract a); - r, a - | (_, r, a) :: l -> - List.iter (fun (_, x, _) -> assert (X.equal x r)) l; - r, a - in - let s = - List.map (function - | { bv = Cte b; sz } -> - Z.format ("%0" ^ string_of_int sz ^ "b") b - | _ -> - (* Cannot happen because [a] must satisfy [is_cte_abstract] at this - point. *) - assert false - ) a - |> String.concat "" - in - r, "#b" ^ s - + let to_const_term r = + match embed r with + | [{ bv = Cte b; sz }] -> + let s = Z.format ("%0" ^ string_of_int sz ^ "b") b in + Some (Expr.bitv s Ty.(Tbitv sz)) + | _ :: _ -> + Fmt.pr "HERE@."; + None + | _ -> + None end diff --git a/src/lib/reasoners/enum.ml b/src/lib/reasoners/enum.ml index 320ca57067..54763d441c 100644 --- a/src/lib/reasoners/enum.ml +++ b/src/lib/reasoners/enum.ml @@ -195,21 +195,9 @@ module Shostak (X : ALIEN) = struct Thus we don't need to guess new values here. *) None - let choose_adequate_model _ r l = - let l = - List.filter - (fun (_, r) -> match embed r with Cons _ -> true | _ -> false) l - in - let r = match l with - | (_,r)::l -> - List.iter (fun (_,x) -> assert (X.equal x r)) l; - r - - | [] -> - (* We do this, because terms of some semantic values created - by CS are not created and added to UF *) - match embed r with Cons _ -> r | _ -> assert false - in - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - + let to_const_term r = + match embed r with + | Cons (hs, ty) -> + Some (E.mk_term Sy.(Op (Constr hs)) [] ty) + | Alien a -> X.to_const_term a end diff --git a/src/lib/reasoners/ite.ml b/src/lib/reasoners/ite.ml index a601512886..96f6b19382 100644 --- a/src/lib/reasoners/ite.ml +++ b/src/lib/reasoners/ite.ml @@ -60,5 +60,5 @@ module Shostak (X : ALIEN) = struct let abstract_selectors _ _ = assert false let solve _ _ = assert false let assign_value _ _ _ = assert false - let choose_adequate_model _ _ _ = assert false + let to_const_term _r = assert false end diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index cd75c0ea89..0b2521708e 100644 --- a/src/lib/reasoners/records.ml +++ b/src/lib/reasoners/records.ml @@ -30,6 +30,7 @@ module Hs = Hstring module E = Expr +module Sy = Symbols type 'a abstract = | Record of (Hs.t * 'a abstract) list * Ty.t @@ -414,7 +415,7 @@ module Shostak (X : ALIEN) = struct | Access _ -> None | Record (_, ty) -> - if List.exists (fun (t,_) -> Expr.const_term t) eq + if List.exists (fun (t,_) -> Expr.is_const_term t) eq then None else Some (Expr.fresh_name ty, false) @@ -426,20 +427,19 @@ module Shostak (X : ALIEN) = struct Some (s, false) (* false <-> not a case-split *) | _ -> assert false - let choose_adequate_model _ _ l = - let acc = - List.fold_left - (fun acc (s, r) -> - if not (Expr.const_term s) then acc - else - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - ) None l - in - match acc with - | Some (_,r) -> - r, Format.asprintf "%a" X.print r (* it's a EUF constant *) - | _ -> assert false + let to_const_term = + let rec to_const_term r = + match r with + | Record (fields, ty) -> + (* We can ignore the names of fields as they are inlined in the + type [ty] of the record. *) + let l = + Lists.try_map (fun (_name, rf) -> to_const_term rf) fields + in + Option.bind l @@ fun l -> + Some (E.mk_term Sy.(Op Record) l ty) + | Other (a, _) -> X.to_const_term a + | Access _ -> None + in fun r -> to_const_term (embed r) end diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index fcac113412..52d6034c00 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -270,6 +270,23 @@ struct | Ac _ -> None, false (* SYLVAIN : TODO *) | Term t -> Some t, true + let to_const_term r = + let res = + match r.v with + | Arith _ -> ARITH.to_const_term r + | Records _ -> RECORDS.to_const_term r + | Bitv _ -> BITV.to_const_term r + | Arrays _ -> ARRAYS.to_const_term r + | Enum _ -> ENUM.to_const_term r + | Adt _ -> ADT.to_const_term r + | Ite _ -> ITE.to_const_term r + | Term t when Expr.is_const_term t -> Some t + | Ac _ | Term _ -> None + in + Option.bind res @@ fun t -> + assert (Expr.is_const_term t); + Some t + let top () = term_embed Expr.vrai let bot () = term_embed Expr.faux @@ -369,7 +386,14 @@ struct | Enum t -> ENUM.is_constant t | Adt t -> ADT.is_constant t | Ite t -> ITE.is_constant t - | Ac _ | Term _ -> false + | Term t -> + begin + let Expr.{ f; xs; _ } = Expr.term_view t in + match f, xs with + | Symbols.(True | False | Void), [] -> true + | _ -> false + end + | Ac _ -> false let subst p v r = if equal p v then r @@ -646,8 +670,8 @@ struct end | Term t, ty -> (* case disable_adts() handled here *) - if Expr.const_term t || - List.exists (fun (t,_) -> Expr.const_term t) eq then None + if Expr.is_const_term t || + List.exists (fun (t,_) -> Expr.is_const_term t) eq then None else Some (Expr.fresh_name ty, false) (* false <-> not a case-split *) | _ -> (* There is no model-generation support for the AC symbols yet. @@ -663,66 +687,6 @@ struct | None -> Format.asprintf "None" | Some(res, _is_cs) -> Format.asprintf "%a" Expr.print res); opt - - let choose_adequate_model t rep l = - let r, pprint = - match Expr.type_info t with - | Ty.Tint - | Ty.Treal -> ARITH.choose_adequate_model t rep l - | Ty.Tbitv _ -> BITV.choose_adequate_model t rep l - | Ty.Tsum _ -> ENUM.choose_adequate_model t rep l - | Ty.Tadt _ when not (Options.get_disable_adts()) -> - ADT.choose_adequate_model t rep l - | Ty.Trecord _ -> RECORDS.choose_adequate_model t rep l - | Ty.Tfarray _ -> ARRAYS.choose_adequate_model t rep l - | Ty.Tbool -> - (* case split is now supposed to be done for internal bools if - needed as well *) - assert (is_bool_const rep); - rep, Format.asprintf "%a" print rep - | _ -> - let acc = - List.fold_left - (fun acc (s, r) -> - if Expr.const_term s then - match acc with - | Some(s', _) when Expr.compare s' s > 0 -> acc - | _ -> Some (s, r) - else - acc - ) None l - in - let r = - match acc with - | Some (_,r) -> r - | None -> - match term_extract rep with - | Some t, true when Expr.const_term t -> rep - | _ -> - let print_aux fmt (t,r) = - Format.fprintf fmt "> impossible case: %a -- %a@ " - Expr.print t - print r - in - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Shostak" ~function_name:"choose_adequate_model" - "@[What to choose for term %a with rep %a?\ - %a@]" - Expr.print t - print rep - (Printer.pp_list_no_space print_aux) l; - assert false - in - r, Format.asprintf "%a" print r (* it's a EUF constant *) - in - if Options.get_debug_interpretation () then - Printer.print_dbg - ~module_name:"Shostak" ~function_name:"choose_adequate_model" - "%a selected as a model for %a" - print r Expr.print t; - r, pprint - end and TARITH : Polynome.T diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index cc6075f4b0..77335efc48 100644 --- a/src/lib/reasoners/sig.mli +++ b/src/lib/reasoners/sig.mli @@ -128,11 +128,7 @@ module type SHOSTAK = sig [Some (t, false)], then there must be no context in which [solve r (fst X.make t)] raises [Unsolvable]. You have been warned! *) - (* choose the value to print and how to print it for the given term. - The second term is its representative. The list is its equivalence class - *) - val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string - + val to_const_term : r -> Expr.t option end module type X = sig @@ -191,8 +187,5 @@ module type X = sig val assign_value : r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option - (* choose the value to print and how to print it for the given term. - The second term is its representative. The list is its equivalence class - *) - val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string + val to_const_term : r -> Expr.t option end diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index dbccbfd94c..6d5c40ba75 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1005,36 +1005,27 @@ let reinit_cache () = LX.reinit_cache () (**** Counter examples functions ****) -let is_a_good_model_value r = - match X.leaves r with - [] -> true - | [r'] -> X.equal r r' - | _ -> false - -let is_const_term r = - match X.term_extract r with - | Some t, _ -> - E.const_term t - | _ -> - (* Cannot test for theories which don't implement [term_extract]. *) - true - let model_repr_of_term t env mrepr = try ME.find t mrepr, mrepr with Not_found -> let mk = try ME.find t env.make with Not_found -> assert false in - let rep,_ = try MapX.find mk env.repr with Not_found -> assert false in + let rep, _ = try MapX.find mk env.repr with Not_found -> assert false in let cls = - try SE.elements (MapX.find rep env.classes) + try + Expr.Set.elements (MapX.find rep env.classes) + |> List.map (fun t -> Expr.Map.find t env.make) + |> List.filter X.is_constant with Not_found -> assert false in - let cls = - try List.rev_map (fun s -> s, ME.find s env.make) cls - with Not_found -> assert false + let tt = + match cls with + | [] -> + X.to_const_term rep + | r :: _ -> X.to_const_term r in - let rep, string_repr = X.choose_adequate_model t rep cls in - assert (is_a_good_model_value rep && is_const_term rep); - (rep, string_repr), ME.add t (rep, string_repr) mrepr + match tt with + | Some tt -> tt, ME.add t tt mrepr + | None -> assert false (* Caches used during the computation of the model. All these caches are flushed before generating a new model. *) @@ -1042,14 +1033,12 @@ module Cache = struct (* Stores all the get accesses to arrays. *) let arrays_cache = Hashtbl.create 17 - (* Stores all the accesses to records. *) - let records_cache = Hashtbl.create 17 - (* Stores all the abstract values generated. This cache is necessary to ensure we don't generate twice an abstract value for a given symbol. *) let abstracts_cache = Hashtbl.create 17 - let store_array_get (t : Expr.t) (i : ModelMap.Value.t) v = + let store_array_get (t : Expr.t) (i : ModelMap.Value.t) + (v : ModelMap.Value.t) = match Hashtbl.find_opt arrays_cache t with | Some values -> Hashtbl.replace values i v @@ -1058,21 +1047,7 @@ module Cache = struct Hashtbl.add values i v; Hashtbl.add arrays_cache t values - let store_record_decl (sy, args_ty, args) r = - match Hashtbl.find_opt records_cache r with - | Some _ -> () - | None -> - let values = Hashtbl.create 17 in - Hashtbl.add records_cache r (sy, args_ty, args, values) - - let store_record_access decl field v = - match Hashtbl.find_opt records_cache decl with - | Some (_sy, _args_ty, _args, values) -> - Hashtbl.replace values field v - | None -> - assert false - - let get_abstract_for env t = + let get_abstract_for env (t : Expr.t) = let r, _ = find env t in match Hashtbl.find_opt abstracts_cache r with | Some abstract -> abstract @@ -1083,19 +1058,12 @@ module Cache = struct let clear () = Hashtbl.clear arrays_cache; - Hashtbl.clear records_cache; Hashtbl.clear abstracts_cache end -let is_forbidden_symbol f ty = - (* Keep record constructors because models.ml expects them to be there *) - (X.is_solvable_theory_symbol f ty - && not (Shostak.Records.is_mine_symb f ty)) - || Sy.is_internal f - let compute_concrete_model_of_val env t ((mdl, mrepr) as acc) = let { E.f; xs; ty; _ } = E.term_view t in - if is_forbidden_symbol f ty + 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 then @@ -1106,15 +1074,13 @@ let compute_concrete_model_of_val env t ((mdl, mrepr) as acc) = List.fold_left (fun (arg_vals, arg_tys, mrepr) arg -> let rep_arg, mrepr = model_repr_of_term arg env mrepr in - assert (is_a_good_model_value (fst rep_arg)); - rep_arg :: arg_vals, + ModelMap.Value.Constant rep_arg :: arg_vals, (Expr.type_info arg) :: arg_tys, mrepr ) ([], [], mrepr) (List.rev xs) in let ret_rep, mrepr = model_repr_of_term t env mrepr in - assert (is_a_good_model_value (fst ret_rep)); match f, arg_vals, ty with | Sy.Name _, [], Ty.Tfarray _ -> begin @@ -1132,36 +1098,13 @@ let compute_concrete_model_of_val env t ((mdl, mrepr) as acc) = never a user-defined array and has to be ignored. *) acc - | Sy.Op Sy.Get, [(a, _); (_, i)], _ -> + | Sy.Op Sy.Get, [Constant a; i], _ -> begin - match X.term_extract a with - | Some ta, true -> - let Expr.{ xs = xs_ta; _ } = - Expr.term_view ta - in - assert (xs_ta == []); - Cache.store_array_get ta ModelMap.Value.(Constant i) ModelMap.Value.(Constant (ret_rep |> snd)); - acc - | _ -> - (* There is no semantic values for arrays, which means an array - is directly represented as a term. *) - assert false + Cache.store_array_get a i (Constant ret_rep); + acc end - | Sy.Name { hs = id; _ }, _, Ty.Trecord _ -> - let r, _ = find env t in - let arg_vals = - List.map - (fun arg_val -> ModelMap.Value.(Constant (arg_val |> snd))) arg_vals - in - Cache.store_record_decl (id, arg_tys, arg_vals) r; - acc - | Sy.Name { hs = id; _ }, _, _ -> - let arg_vals = - List.map - (fun arg_val -> ModelMap.Value.(Constant (arg_val |> snd))) arg_vals - in let value = match ty with | Ty.Text _ -> @@ -1169,24 +1112,16 @@ let compute_concrete_model_of_val env t ((mdl, mrepr) as acc) = In this case, we produce an abstract value with the appropriate type. *) let abstract = Cache.get_abstract_for env t in - ModelMap.Value.(Abstract (abstract, arg_tys, ty)) - | _ -> ModelMap.Value.(Constant (ret_rep |> snd)) + ModelMap.Value.Abstract (abstract, ty) + | _ -> ModelMap.Value.Constant ret_rep in let mdl = ModelMap.(add (id, arg_tys, ty) arg_vals value mdl) in mdl, mrepr - | Sy.(Op Access field), [(r, _)], _ -> - begin - let r, _ = find_r env r in - Cache.store_record_access r (Hstring.view field) (ret_rep |> snd); - mdl, mrepr - end - | _ -> - Fmt.pr "Unexpected term %a@." Expr.print t; - assert false + mdl, mrepr end (* A map of expressions / terms, ordered by depth first, and then by @@ -1210,12 +1145,11 @@ let is_suspicious_name hs = (* The model generation is known to be imcomplete for FPA and Bitvector theories. *) let is_suspicious_symbol = function - | Sy.Op (Float | Abs_int | Abs_real | Sqrt_real_default + | Sy.Op (Float | Abs_int | Abs_real | Sqrt_real | Sqrt_real_default | Sqrt_real_excess | Real_of_int | Int_floor | Int_ceil | Max_int | Max_real | Min_int | Min_real | Integer_log2 | Integer_round) -> not (Options.get_theory_preludes () |> List.mem Theories.Fpa) - | Sy.Op (BVand | BVor) -> true | Symbols.Name { hs; _ } when is_suspicious_name hs -> true | _ -> false @@ -1235,9 +1169,32 @@ let terms env = let compute_concrete_model env = Cache.clear (); let terms, suspicious = terms env in - MED.fold - (fun t _mk acc -> compute_concrete_model_of_val env t acc - ) terms (ModelMap.empty ~suspicious, Expr.Map.empty) + let mdl, mrepr = + MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc) + terms (ModelMap.empty ~suspicious, ME.empty) + in + let mdl = + 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. *) + let abstract = Cache.get_abstract_for env t in + 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)) + in + let id = + let Expr.{ f; _ } = Expr.term_view t in + match f with + | Sy.Name { hs; _ } -> hs + | _ -> assert false + in + ModelMap.add (id, [], ty) [] arr_val mdl + ) Cache.arrays_cache mdl + in + (mdl, mrepr) let extract_concrete_model ~prop_model env = let model, mrepr = compute_concrete_model env in diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index a2f5510dc8..1184c56332 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -313,6 +313,16 @@ module SmtPrinter = struct | Sy.Real q when Q.(equal q zero) -> true | _ -> false + let pp_rational ppf q = + if Z.equal (Q.den q) Z.one then + Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) + else if Q.sign q = -1 then + Fmt.pf ppf "(/ (- %a) %a)" + Z.pp_print (Z.abs (Q.num q)) + Z.pp_print (Q.den q) + else + Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) + let pp_binder ppf (var, ty) = Fmt.pf ppf "(%a %a)" Var.print var Ty.pp_smtlib ty @@ -415,6 +425,9 @@ module SmtPrinter = struct | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op + | Sy.Op Minus, [e1; { f = Sy.Real q; _ }] when is_zero e1.f -> + pp_rational ppf (Q.neg q) + | Sy.Op Minus, [e1; e2] when is_zero e1.f -> Fmt.pf ppf "@[<2>(- %a@])" pp e2 @@ -443,14 +456,7 @@ module SmtPrinter = struct Fmt.pf ppf "%a" Z.pp_print i | Sy.Real q, [] -> - if Z.equal (Q.den q) Z.one then - Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) - else if Q.sign q = -1 then - Fmt.pf ppf "(/ (- %a) %a)" - Z.pp_print (Z.abs (Q.num q)) - Z.pp_print (Q.den q) - else - Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) + pp_rational ppf q | Sy.Bitv (n, s), [] -> Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s) @@ -671,6 +677,8 @@ let print_list_sep sep = let print_list ppf = print_list_sep "," ppf +let pp_smtlib = SmtPrinter.pp + let pp_binders ppf = if Options.get_output_smtlib () then SmtPrinter.pp_binders ppf @@ -1015,14 +1023,24 @@ let mk_ite cond th el = if ty == Ty.Tbool then mk_if cond th el else mk_term (Sy.Op Sy.Tite) [cond; th; el] ty -let [@inline always] const_term e = - (* we use this function because depth is currently not correct to +let rec is_const_term e = + match e.f, e.xs with + | (Op Constr _ | Op Record), xs -> + List.for_all is_const_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 + | (True | False | Void | Name _ | Int _ | Real _ | Bitv _ | Var _), [] -> true + | _ -> false + +let[@inline always] const_term e = + (* We use this function because depth is currently not correct to detect constants (not incremented in some situations due to - some regression) *) + some regression). *) match e.f with - | Sy.Form _ | Sy.Lit _ | Sy.Let -> false - | True | False | Void | Name _ | Int _ | Real _ | Bitv _ - | Op _ | Var _ | In _ | MapsTo _ -> + | Sy.Form _ | Sy.Lit _ | Sy.Let -> false + | True | False | Void | Name _ | Int _ | Real _ | Bitv _ | Op _ + | Var _ | In _ | MapsTo _ -> let res = (e.xs == []) in assert (res == (depth e <= 1)); res @@ -3106,3 +3124,20 @@ module BV = struct let bvsgt s t = bvslt t s let bvsge s t = bvsle t s end + +(** Constructors from the smtlib theory of functional arrays with + extensionality logic. + + https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml *) +module ArraysEx = struct + let select a i = + let rty = + match type_info a with + | Tfarray (_, rty) -> rty + | _ -> invalid_arg "[Expr.ArraysEx.select]" + in + mk_term Sy.(Op Get) [a; i] rty + + let store a i v = + mk_term Sy.(Op Set) [a; i; v] (type_info a) +end diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index ad16a9377b..3be146c515 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -151,6 +151,10 @@ val print_list : Format.formatter -> t list -> unit val print_list_sep : string -> Format.formatter -> t list -> unit val print_triggers : Format.formatter -> trigger list -> unit +val pp_smtlib : t Fmt.t +(** [pp_smtlib ppf e] prints the expression [e] on the formatter + [ppf] using the SMT-LIB standard. *) + (** Comparison and hashing functions *) val compare : t -> t -> int @@ -326,8 +330,13 @@ val print_th_elt : Format.formatter -> th_elt -> unit val is_pure : t -> bool -val const_term : t -> bool -(** return true iff the given argument is a term without arguments *) +val is_const_term : t -> bool +(** [is_const_term e] checks if the expression [e] is a constant terms. + A constant term can be: + - A record definition involving only constant terms. + - A constructor application involving only constant terms, + - A literal of a basic type (integer, real, boolean, unit or bitvector), + - A variable or an application of function of arity [0]. *) val save_cache: unit -> unit (** Saves the modules cache *) @@ -473,3 +482,12 @@ module BV : sig val bvlshr : t -> t -> t val bvashr : t -> t -> t end + +(** Constructors from the smtlib theory of functional arrays with + extensionality logic. + + https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml *) +module ArraysEx : sig + val select : t -> t -> t + val store : t -> t -> t -> t +end diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index fbba3c3ece..33e7310570 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -34,37 +34,21 @@ module Sy = Symbols type sy = Id.t * Ty.t list * Ty.t [@@deriving ord] module Value = struct - type array = - | AbstractArray of Id.t * Ty.t * Ty.t - | Store of array * t * t - - and t = - | Abstract of sy - | Constant of string - | Array of array - | Record of string * t list + type t = + | Abstract of Id.t * Ty.t + | Store of t * t * t + | Constant of Expr.t [@@deriving ord] - let rec pp_array ppf arr = - match arr with - | AbstractArray (id, ty_key, ty_val) -> - Fmt.pf ppf "(as %a %a)" Id.pp id Ty.pp_smtlib - (Ty.Tfarray (ty_key, ty_val)) - | Store (arr, i, v) -> - Fmt.pf ppf "(@[store@ %a@ %a %a)@]" - pp_array arr pp i pp v - - and pp ppf v = + let rec pp ppf v = match v with - | Abstract (id, _, ty) -> + | Abstract (id, ty) -> Fmt.pf ppf "(as %a %a)" Id.pp id Ty.pp_smtlib ty - | Constant s -> - Fmt.string ppf s - | Array arr -> pp_array ppf arr - | Record (id, fields) -> - Fmt.pf ppf "(@[%s %a)@]" - (Util.quoted_string id) - Fmt.(list ~sep:sp pp) fields + | 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 diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index c030d7cf41..00e52bb203 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -32,15 +32,12 @@ type sy = Id.t * Ty.t list * Ty.t (** Typed symbol of function. *) module Value : sig - type array = - | AbstractArray of Id.t * Ty.t * Ty.t - | Store of array * t * t - - and t = - | Abstract of sy - | Constant of string - | Array of array - | Record of string * t list + 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_const_term]. *) val pp : t Fmt.t (** [pp ppf v] prints the model value [v] on the formatter [ppf] using the diff --git a/src/lib/util/lists.ml b/src/lib/util/lists.ml index f959ac1a1c..10b9389aee 100644 --- a/src/lib/util/lists.ml +++ b/src/lib/util/lists.ml @@ -51,3 +51,11 @@ let apply_right f l = )([], true) l in (if same then l else List.rev res), same + +let rec try_map f l = + match l with + | [] -> Some [] + | x :: xs -> + Option.bind (f x) @@ fun y -> + Option.bind (try_map f xs) @@ fun ys -> + Some (y :: ys) diff --git a/src/lib/util/lists.mli b/src/lib/util/lists.mli index 01cb2555bd..8cf8eb0fee 100644 --- a/src/lib/util/lists.mli +++ b/src/lib/util/lists.mli @@ -47,3 +47,7 @@ val apply : ('a -> 'a) -> 'a list -> 'a list * bool val apply_right : ('a -> 'a) -> ('b * 'a) list -> ('b * 'a) list * bool (** similar to function apply, but the elements of the list are couples **) + +val try_map : ('a -> 'b option) -> 'a list -> 'b list option +(** [try_map f l] is similar to [List.map f l] but the function [f] + may fail and the iterator shortcuts the computation. *) diff --git a/tests/models/arith/arith5.optimize.expected b/tests/models/arith/arith5.optimize.expected index 68d4b0380d..e886d13329 100644 --- a/tests/models/arith/arith5.optimize.expected +++ b/tests/models/arith/arith5.optimize.expected @@ -6,5 +6,5 @@ unknown (define-fun z () Real (/ (- 7) 9)) ) (objectives - (x (- (/ 1 18))) + (x (/ (- 1) 18)) ) \ No newline at end of file diff --git a/tests/models/arith/arith7.optimize.expected b/tests/models/arith/arith7.optimize.expected index 1771da7871..1d670f3fac 100644 --- a/tests/models/arith/arith7.optimize.expected +++ b/tests/models/arith/arith7.optimize.expected @@ -1,5 +1,7 @@ unknown +; This model is a best-effort. It includes symbols +; for which model generation is known to be incomplete. ( (define-fun x () Real (/ 7 20)) (define-fun y () Real 1.0) diff --git a/tests/models/records/record1.models.expected b/tests/models/records/record1.models.expected index c8d49e1713..da5e88f8f6 100644 --- a/tests/models/records/record1.models.expected +++ b/tests/models/records/record1.models.expected @@ -1,5 +1,5 @@ unknown ( - (define-fun a () Pair (pair 5 (as @a0 Int))) + (define-fun a () Pair (pair 5 0)) ) diff --git a/tests/models/records/record2.models.expected b/tests/models/records/record2.models.expected index dd311dd1bf..d95838e695 100644 --- a/tests/models/records/record2.models.expected +++ b/tests/models/records/record2.models.expected @@ -1,5 +1,5 @@ unknown ( - (define-fun f ((_arg_0 Int)) Pair (pair 5 (as @a0 Int))) + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) ) diff --git a/tests/models/records/record3.models.expected b/tests/models/records/record3.models.expected index a01fc94fb6..b478bf755b 100644 --- a/tests/models/records/record3.models.expected +++ b/tests/models/records/record3.models.expected @@ -1,7 +1,7 @@ unknown ( - (define-fun f ((_arg_0 Int)) Pair (pair 5 (as @a0 Int))) + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) (define-fun x () Int 0) (define-fun y () Int 5) )