Fix 715 (#741)

* Support for user-defined symbols

* Add support for user-defined symbols in the legacy frontend

* Add tests and fix the expected file of bool1.models.smt2

* Rename user_defined to defined

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 ~defined:true name_base in
             Cache.store_sy tcst sy
           | `Type_alias _ -> ()
           | `Instanceof _ ->

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

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 ?(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 ~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 ~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 =

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

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 =

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 _

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
 

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 =

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) ?(defined=false) s =
+  Name (Hstring.make s, kind, 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

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 -> ?defined:bool -> string -> t
 val var : Var.t -> t
 val underscore : t
 val int : string -> t

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)
 )

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

tests/models/issues/715/715_1.models.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/models/issues/715/715_2.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun f () Int 0)
+)

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)