From c2780506cb85e0ae4829bddf079c53108cdfd70d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 19 Jul 2023 10:24:32 +0200 Subject: [PATCH 1/4] Support for user-defined symbols --- src/lib/frontend/d_cnf.ml | 2 +- src/lib/frontend/models.ml | 2 +- src/lib/reasoners/ac.ml | 2 +- src/lib/reasoners/theory.ml | 2 +- src/lib/structures/expr.ml | 6 +++--- src/lib/structures/modelMap.ml | 9 ++++++++- src/lib/structures/satml_types.ml | 3 ++- src/lib/structures/symbols.ml | 16 +++++++++------- src/lib/structures/symbols.mli | 4 ++-- 9 files changed, 28 insertions(+), 18 deletions(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 2eb02e0dd..fff2ebcf7 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1850,7 +1850,7 @@ let make dloc_file acc stmt = match def with | `Term_def (_, ({ path; _ } as tcst), _, _, _) -> let name_base = get_basename path in - let sy = Sy.name name_base in + let sy = Sy.name ~user_defined:true name_base in Cache.store_sy tcst sy | `Type_alias _ -> () | `Instanceof _ -> diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 43d05cef0..0cdc01935 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -191,7 +191,7 @@ module Pp_smtlib_term = struct | Sy.In(lb, rb), [t] -> fprintf fmt "(%a in %a, %a)" print t Sy.print_bound lb Sy.print_bound rb - | Sy.Name (n,_), l -> begin + | Sy.Name (n, _, _), l -> begin let constraint_name = try let constraint_name,_,_ = (MS.find (Hstring.view n) !constraints) in diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index 54826d974..e9bdf4bb9 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -164,7 +164,7 @@ module Make (X : Sig.X) = struct | Some ac when Sy.equal sy ac.h -> r, acc | None -> r, acc | Some _ -> match Expr.term_view t with - | { Expr.f = Sy.Name (hs, Sy.Ac); xs; ty; _ } -> + | { Expr.f = Sy.Name (hs, Sy.Ac, _); xs; ty; _ } -> let aro_sy = Sy.name ("@" ^ (HS.view hs)) in let aro_t = Expr.mk_term aro_sy xs ty in let eq = Expr.mk_eq ~iff:false aro_t t in diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 30afa6301..04ebaa1e6 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -105,7 +105,7 @@ module Main_Default : S = struct SE.fold (fun t mp -> match E.term_view t with - | { E.f = Sy.Name (hs, ((Sy.Ac | Sy.Other) as is_ac)); + | { E.f = Sy.Name (hs, ((Sy.Ac | Sy.Other) as is_ac), _); xs; ty; _ } -> let xs = List.map E.type_info xs in let xs, ty = diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7060ec1fd..32b6271ae 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -813,13 +813,13 @@ let is_real t = t.ty == Ty.Treal let is_fresh t = match t with - | { f = Sy.Name (hs,_); xs = []; _ } -> + | { f = Sy.Name (hs, _, _); xs = []; _ } -> Hstring.is_fresh_string (Hstring.view hs) | _ -> false let is_fresh_skolem t = match t with - | { f = Sy.Name (hs,_); _ } -> Hstring.is_fresh_skolem (Hstring.view hs) + | { f = Sy.Name (hs, _, _); _ } -> Hstring.is_fresh_skolem (Hstring.view hs) | _ -> false let name_of_lemma f = @@ -2305,7 +2305,7 @@ module Triggers = struct | { f = Op _; _ } -> if eq exclude e then acc else e :: acc - | { f = Name (_, _); _ } -> + | { f = Name (_, _, _); _ } -> if eq exclude e then acc else e :: acc | { f = ( True | False | Void | Int _ | Real _ diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index cef5c17ad..10d60ffe8 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -87,7 +87,14 @@ let add p v mp = if V.mem v prof_p then mp else P.add p (V.add v prof_p) mp -let iter = P.iter +let iter f = + P.iter (fun ((sy, _, _) as key) value -> + match sy with + | Sy.Name (_, _, true) -> + (* We don't print constants defined by the user. *) + () + | _ -> f key value + ) let fold = P.fold diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml index 648ab9aae..e2081a907 100644 --- a/src/lib/structures/satml_types.ml +++ b/src/lib/structures/satml_types.ml @@ -926,7 +926,8 @@ module Flat_Formula : FLAT_FORMULA = struct let mk_new_proxy n = let hs = Hs.make ("PROXY__" ^ (string_of_int n)) in - let sy = Symbols.Name(hs, Symbols.Other) in + (* TODO: we should use a smart constructor here. *) + let sy = Symbols.Name (hs, Symbols.Other, false) in E.mk_term sy [] Ty.Tbool let get_proxy_of f proxies_mp = diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 942c87793..3e9331a85 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -85,7 +85,7 @@ type t = | True | False | Void - | Name of Hstring.t * name_kind + | Name of Hstring.t * name_kind * bool | Int of Hstring.t | Real of Hstring.t | Bitv of string @@ -99,7 +99,9 @@ type t = type s = t -let name ?(kind=Other) s = Name (Hstring.make s, kind) +let name ?(kind=Other) ?(user_defined=false) s = + Name (Hstring.make s, kind, user_defined) + let var s = Var s let int i = Int (Hstring.make i) let real r = Real (Hstring.make r) @@ -117,7 +119,7 @@ let mk_in b1 b2 = let mk_maps_to x = MapsTo x let is_ac x = match x with - | Name(_, Ac) -> true + | Name(_, Ac, _) -> true | _ -> false let underscore = @@ -203,7 +205,7 @@ let compare s1 s2 = | Int h1, Int h2 | Real h1, Real h2 -> Hstring.compare h1 h2 | Var v1, Var v2 | MapsTo v1, MapsTo v2 -> Var.compare v1 v2 - | Name (h1, k1), Name (h2, k2) -> + | Name (h1, k1, _), Name (h2, k2, _) -> let c = Hstring.compare h1 h2 in if c <> 0 then c else compare_kinds k1 k2 | Bitv s1, Bitv s2 -> String.compare s1 s2 @@ -230,8 +232,8 @@ let hash x = | Let -> 3 | Bitv s -> 19 * Hashtbl.hash s + 3 | In (b1, b2) -> 19 * (Hashtbl.hash b1 + Hashtbl.hash b2) + 4 - | Name (n,Ac) -> 19 * Hstring.hash n + 5 - | Name (n,Other) -> 19 * Hstring.hash n + 6 + | Name (n, Ac, _) -> 19 * Hstring.hash n + 5 + | Name (n, Other, _) -> 19 * Hstring.hash n + 6 | Int n | Real n -> 19 * Hstring.hash n + 7 | Var v -> 19 * Var.hash v + 8 | MapsTo v -> 19 * Var.hash v + 9 @@ -274,7 +276,7 @@ let string_of_form f = match f with | F_Xor -> "xor" let to_string ?(show_vars=true) x = match x with - | Name (n,_) -> Hstring.view n + | Name (n, _, _) -> Hstring.view n | Var v when show_vars -> Format.sprintf "'%s'" (Var.to_string v) | Var v -> Var.to_string v | Int n -> Hstring.view n diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index af08b9c59..e0d798a8d 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -84,7 +84,7 @@ type t = | True | False | Void - | Name of Hstring.t * name_kind + | Name of Hstring.t * name_kind * bool | Int of Hstring.t | Real of Hstring.t | Bitv of string @@ -96,7 +96,7 @@ type t = | MapsTo of Var.t | Let -val name : ?kind:name_kind -> string -> t +val name : ?kind:name_kind -> ?user_defined:bool -> string -> t val var : Var.t -> t val underscore : t val int : string -> t From 372b0573757d079ba13bf540ca56312fbdf4bce5 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 19 Jul 2023 15:11:13 +0200 Subject: [PATCH 2/4] Add support for user-defined symbols in the legacy frontend --- src/lib/frontend/typechecker.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 3074ba921..6b5a528cd 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -2367,7 +2367,7 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) = assert (not is_recursive); (* Abstract types are not recursive *) acc, env -let declare_fun env loc n ?ret_ty l = +let declare_fun env loc n ?(user_defined=false) ?ret_ty l = check_duplicate_params l; let infix, ty = let l = List.map (fun (_,_,x) -> x) l in @@ -2377,7 +2377,7 @@ let declare_fun env loc n ?ret_ty l = | Some ty -> PPeq, PFunction(l,ty) in - let mk_symb hs = Symbols.name hs ~kind:Symbols.Other in + let mk_symb hs = Symbols.name hs ~user_defined ~kind:Symbols.Other in let tlogic, env = Env.add_logics env mk_symb [n] ty loc in (* TODO *) env, infix, tlogic @@ -2409,7 +2409,9 @@ let define_fun (acc, env) loc n l tlogic ?ret_ty infix e = (td_a, env)::acc, env let type_fun (acc, env) loc n l ?ret_ty e = - let env, infix, tlogic = declare_fun env loc n ?ret_ty l in + let env, infix, tlogic = + declare_fun env loc n ~user_defined:true ?ret_ty l + in define_fun (acc, env) loc n l tlogic ?ret_ty infix e let rec type_decl (acc, env) d assertion_stack = From c740ca826e9d12362901582ad524e5d237c898bd Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 19 Jul 2023 15:31:37 +0200 Subject: [PATCH 3/4] Add tests and fix the expected file of bool1.models.smt2 --- tests/models/bool/bool1.models.expected | 1 - tests/models/issues/715/715_1.models.ae | 6 ++++++ tests/models/issues/715/715_1.models.expected | 2 ++ tests/models/issues/715/715_2.models.expected | 5 +++++ tests/models/issues/715/715_2.models.smt2 | 8 ++++++++ 5 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 tests/models/issues/715/715_1.models.ae create mode 100644 tests/models/issues/715/715_1.models.expected create mode 100644 tests/models/issues/715/715_2.models.expected create mode 100644 tests/models/issues/715/715_2.models.smt2 diff --git a/tests/models/bool/bool1.models.expected b/tests/models/bool/bool1.models.expected index d75528555..0ccd1ace6 100644 --- a/tests/models/bool/bool1.models.expected +++ b/tests/models/bool/bool1.models.expected @@ -7,5 +7,4 @@ unknown ( (define-fun p () Bool true) (define-fun q () Bool true) - (define-fun nq () Bool true) ) diff --git a/tests/models/issues/715/715_1.models.ae b/tests/models/issues/715/715_1.models.ae new file mode 100644 index 000000000..84ef6c34f --- /dev/null +++ b/tests/models/issues/715/715_1.models.ae @@ -0,0 +1,6 @@ +logic f: int + +(* This function is user-defined and shouldn't appear in the output model. *) +function g(x: int, y: int) : int = x + y + +check_sat t: f = 0 diff --git a/tests/models/issues/715/715_1.models.expected b/tests/models/issues/715/715_1.models.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/models/issues/715/715_1.models.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/models/issues/715/715_2.models.expected b/tests/models/issues/715/715_2.models.expected new file mode 100644 index 000000000..966bb2f29 --- /dev/null +++ b/tests/models/issues/715/715_2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun f () Int 0) +) diff --git a/tests/models/issues/715/715_2.models.smt2 b/tests/models/issues/715/715_2.models.smt2 new file mode 100644 index 000000000..93a28138c --- /dev/null +++ b/tests/models/issues/715/715_2.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const f Int) +(assert (= f 0)) +; This function is user-defined and shouldn't appear in the output model. +(define-fun g ((x Int) (y Int)) Int (+ x y)) +(check-sat) +(get-model) From 227e15e7c97703ce21605d9669bef379c0c9dd32 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 19 Jul 2023 18:22:11 +0200 Subject: [PATCH 4/4] Rename user_defined to defined --- src/lib/frontend/d_cnf.ml | 2 +- src/lib/frontend/typechecker.ml | 6 +++--- src/lib/structures/symbols.ml | 4 ++-- src/lib/structures/symbols.mli | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index fff2ebcf7..f2173c77c 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1850,7 +1850,7 @@ let make dloc_file acc stmt = match def with | `Term_def (_, ({ path; _ } as tcst), _, _, _) -> let name_base = get_basename path in - let sy = Sy.name ~user_defined:true name_base in + let sy = Sy.name ~defined:true name_base in Cache.store_sy tcst sy | `Type_alias _ -> () | `Instanceof _ -> diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 6b5a528cd..7caf6d2c4 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -2367,7 +2367,7 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) = assert (not is_recursive); (* Abstract types are not recursive *) acc, env -let declare_fun env loc n ?(user_defined=false) ?ret_ty l = +let declare_fun env loc n ?(defined=false) ?ret_ty l = check_duplicate_params l; let infix, ty = let l = List.map (fun (_,_,x) -> x) l in @@ -2377,7 +2377,7 @@ let declare_fun env loc n ?(user_defined=false) ?ret_ty l = | Some ty -> PPeq, PFunction(l,ty) in - let mk_symb hs = Symbols.name hs ~user_defined ~kind:Symbols.Other in + let mk_symb hs = Symbols.name hs ~defined ~kind:Symbols.Other in let tlogic, env = Env.add_logics env mk_symb [n] ty loc in (* TODO *) env, infix, tlogic @@ -2410,7 +2410,7 @@ let define_fun (acc, env) loc n l tlogic ?ret_ty infix e = let type_fun (acc, env) loc n l ?ret_ty e = let env, infix, tlogic = - declare_fun env loc n ~user_defined:true ?ret_ty l + declare_fun env loc n ~defined:true ?ret_ty l in define_fun (acc, env) loc n l tlogic ?ret_ty infix e diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 3e9331a85..e0fa1cef6 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -99,8 +99,8 @@ type t = type s = t -let name ?(kind=Other) ?(user_defined=false) s = - Name (Hstring.make s, kind, user_defined) +let name ?(kind=Other) ?(defined=false) s = + Name (Hstring.make s, kind, defined) let var s = Var s let int i = Int (Hstring.make i) diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index e0d798a8d..6cf275e44 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -96,7 +96,7 @@ type t = | MapsTo of Var.t | Let -val name : ?kind:name_kind -> ?user_defined:bool -> string -> t +val name : ?kind:name_kind -> ?defined:bool -> string -> t val var : Var.t -> t val underscore : t val int : string -> t