encoding : array (and other lskept) for smt2 with logic instantiation

drivers/z3_smtv2_array.drv

+(* Why driver for SMT syntax *)
+
+prelude ";;; this is a prelude for Z3"
+prelude "(set-logic AUFNIRA)"
+
+printer "smtv2"
+filename "%f-%t-%g.smt"
+
+valid "^unsat"
+unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
+time "why3cpulimit time : %s s"
+
+
+(* À discuter *)
+transformation "simplify_recursive_definition"
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_smt"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "select_array_symbol_in_goal"
+transformation "instantiate_lsymbol"
+transformation "encoding_smt"
+
+theory BuiltIn
+  syntax type int   "Int"
+  syntax type real  "Real"
+  syntax logic (=)  "(= %1 %2)"
+end
+
+theory int.Int
+
+  prelude ";;; this is a prelude for Z3 integer arithmetic"
+
+  syntax logic zero "0"
+  syntax logic one  "1"
+
+  syntax logic (+)  "(+ %1 %2)"
+  syntax logic (-)  "(- %1 %2)"
+  syntax logic (*)  "(* %1 %2)"
+  syntax logic (-_) "(- %1)"
+
+  syntax logic (<=) "(<= %1 %2)"
+  syntax logic (<)  "(< %1 %2)"
+  syntax logic (>=) "(>= %1 %2)"
+  syntax logic (>)  "(> %1 %2)"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+
+  meta "encoding : kept" type int
+
+end
+
+
+theory real.Real
+
+  prelude ";;; this is a prelude for Z3 real arithmetic"
+
+  syntax logic zero "0.0"
+  syntax logic one  "1.0"
+
+  syntax logic (+)  "(+ %1 %2)"
+  syntax logic (-)  "(- %1 %2)"
+  syntax logic (*)  "(* %1 %2)"
+  syntax logic (/)  "(/ %1 %2)"
+  syntax logic (-_) "(- %1)"
+  syntax logic inv  "(/ 1.0 %1)"
+
+  syntax logic (<=) "(<= %1 %2)"
+  syntax logic (<)  "(< %1 %2)"
+  syntax logic (>=) "(>= %1 %2)"
+  syntax logic (>)  "(> %1 %2)"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Inverse
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+
+  meta "encoding : kept" type real
+
+end
+
+(*
+(* L'encodage des types sommes bloquent cette théorie builtin *)
+theory bool.Bool
+   syntax type bool   "bool"
+   syntax logic True  "true"
+   syntax logic False "false"
+   syntax logic andb  "(and %1 %2)"
+   syntax logic orb   "(or %1 %2)"
+   syntax logic xorb  "(xor %1 %2)"
+   syntax logic notb  "(not %1)"
+   meta cloned "encoding_decorate : kept" type bool
+end
+*)
+
+
+theory int.EuclideanDivision
+   syntax logic div "(div %1 %2)"
+   syntax logic mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+
+theory transform.array.Array
+  syntax cloned logic get "(select %1 %2)"
+  syntax cloned logic set "(store %1 %2 %3)"
+  remove cloned prop Select_eq
+  remove cloned prop Select_neq
+
+end
+
+(*
+theory real.FromInt
+  syntax logic from_int "(from_int %1)"
+  remove prop Add
+  remove prop Sub
+  remove prop Mul
+  remove prop Neg
+end
+*)
+
+(*
+theory real.Truncate
+  syntax logic floor "(to_int %1)"
+  remove prop Floor_down
+  remove prop Floor_monotonic
+end
+*)
+
+theory array.Array
+  syntax type t "(Array %1 %2)"
+  meta "encoding : lskept" logic get
+  meta "encoding : lskept" logic set
+  meta "encoding : lskept" logic create_const
+  meta "smt_dist_syntax" logic get, "(select %1 %2)"
+  meta "smt_dist_syntax" logic set, "(store %1 %2 %3)"
+  meta "smt_dist_syntax" logic create_const, "(const[%t0] %1)"
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

src/core/printer.ml

@@ -86,6 +86,7 @@ let iter_group expr iter_fun text =
   iter 0 false
 
 let regexp_arg_pos = Str.regexp "%\\([0-9]+\\)"
+let regexp_arg_pos_typed = Str.regexp "%\\([t]?[0-9]+\\)"
 
 exception BadSyntaxIndex of int
 exception BadSyntaxArity of int * int
@@ -98,6 +99,23 @@ let check_syntax s len =
   in
   iter_group regexp_arg_pos arg s
 
+
+let check_syntax_typed s len ret =
+  let arg s =
+    let grp = (Str.matched_group 1 s) in
+    if grp.[0] = 't'
+    then
+      let grp = String.sub grp 1 (String.length grp - 1) in
+      let i = int_of_string grp in
+      if i < 0 || (not ret && i = 0) then raise (BadSyntaxIndex i);
+      if i > len then raise (BadSyntaxArity (len,i));
+    else
+      let i = int_of_string grp in
+      if i <= 0 then raise (BadSyntaxIndex i);
+      if i > len then raise (BadSyntaxArity (len,i));
+  in
+  iter_group regexp_arg_pos_typed arg s
+
 let syntax_arguments s print fmt l =
   let args = Array.of_list l in
   let repl_fun s fmt =
@@ -105,6 +123,22 @@ let syntax_arguments s print fmt l =
     print fmt args.(i-1) in
   global_substitute_fmt regexp_arg_pos repl_fun s fmt
 
+let syntax_arguments_typed s print_arg print_type t fmt l =
+  let args = Array.of_list l in
+  let repl_fun s fmt =
+    let grp = (Str.matched_group 1 s) in
+    if grp.[0] = 't'
+    then
+      let grp = String.sub grp 1 (String.length grp - 1) in
+      let i = int_of_string grp in
+      if i = 0
+      then print_type fmt (Util.of_option t).t_ty
+      else print_type fmt args.(i-1).t_ty
+    else
+      let i = int_of_string grp in
+      print_arg fmt args.(i-1) in
+  global_substitute_fmt regexp_arg_pos_typed repl_fun s fmt
+
 (** {2 use printers} *)
 
 let print_prelude fmt pl =
@@ -142,7 +176,7 @@ let syntax_type ts s =
   create_meta meta_syntax_type [MAts ts; MAstr s]
 
 let syntax_logic ls s =
-  check_syntax s (List.length ls.ls_args);
+  check_syntax_typed s (List.length ls.ls_args) (ls.ls_value <> None);
   create_meta meta_syntax_logic [MAls ls; MAstr s]
 
 let remove_prop pr =

src/core/printer.mli

@@ -64,6 +64,12 @@ val syntax_arguments : string -> 'a pp -> 'a list pp
 (** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
      the list l using the template templ and the printer print_arg *)
 
+val syntax_arguments_typed : string -> term pp -> ty pp ->
+  term option -> term list pp
+(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
+     the list l using the template templ and the printer print_arg *)
+
+
 (** {2 exceptions to use in transformations and printers} *)
 
 exception UnsupportedTysymbol   of tysymbol   * string

src/core/trans.ml

@@ -37,6 +37,8 @@ let apply f x = f x
 let identity   x =  x
 let identity_l x = [x]
 
+let return x = fun _ -> x
+
 let conv_res c f x = c (f x)
 
 let singleton f x = [f x]

src/core/trans.mli

@@ -35,6 +35,7 @@ val identity   : task trans
 val identity_l : task tlist
 
 val singleton : 'a trans -> 'a tlist
+val return    : 'a -> 'a trans
 
 val compose   : task trans -> 'a trans -> 'a trans
 val compose_l : task tlist -> 'a tlist -> 'a tlist

src/printer/smt2.ml

@@ -53,7 +53,7 @@ let ident_printer =
       "get-option"; "get-proof"; "get-unsat-core"; "get-value"; "pop"; "push";
       "set-logic"; "set-info"; "set-option";
        (** for security *)
-      "Bool";"unsat";"sat";"true";"false"]
+      "Bool";"unsat";"sat";"true";"false";"select";"store"]
   in
   let san = sanitizer char_to_alpha char_to_alnumus in
   create_ident_printer bls ~sanitizer:san
@@ -67,6 +67,7 @@ type info = {
   info_rem : Sid.t;
   use_trigger : bool;
   barrays : (ty*ty) Mts.t;
+  complex_type : ty Hty.t;
 }
 
 let rec print_type info fmt ty = match ty.ty_node with
@@ -75,14 +76,41 @@ let rec print_type info fmt ty = match ty.ty_node with
       | Some s -> syntax_arguments s (print_type info) fmt []
       | None -> fprintf fmt "%a" print_ident ts.ts_name
   end
-  | Tyapp (_, _) -> unsupported "smt : you must encode the complexe type"
+  | Tyapp (ts, l) ->
+     begin match query_syntax info.info_syn ts.ts_name with
+      | Some s -> syntax_arguments s (print_type info) fmt l
+      | None -> fprintf fmt "(%a %a)" print_ident ts.ts_name
+        (print_list space (print_type info)) l
+     end
+
+let find_complex_type info fmt f =
+  let iter () ty =
+    match ty.ty_node with
+      | Tyapp (_,_::_) when not (Hty.mem info.complex_type ty) ->
+        let id = id_fresh (Pp.string_of_wnl Pretty.print_ty ty) in
+        let ts = create_tysymbol id [] None in
+        let cty = ty_app ts [] in
+        fprintf fmt "(define-sorts ((%a %a)))@."
+          print_ident ts.ts_name
+          (print_type info) ty;
+        Hty.add info.complex_type ty cty
+      | _ -> ()
+  in
+  f_ty_fold iter () f
+
+let print_type info fmt ty =
+  print_type info fmt
+    (try
+       Hty.find info.complex_type ty
+     with Not_found -> ty)
 
 (* and print_tyapp info fmt = function *)
 (*   | [] -> () *)
 (*   | [ty] -> fprintf fmt "%a " (print_type info) ty *)
 (*   | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl *)
 
-let print_type info fmt = catch_unsupportedType (print_type info fmt)
+let print_type info fmt =
+  catch_unsupportedType (print_type info fmt)
 
 let print_type_value info fmt = function
   | None -> fprintf fmt "Bool"
@@ -96,7 +124,8 @@ let print_var fmt {vs_name = id} =
   fprintf fmt "%s" n
 
 let print_typed_var info fmt vs =
-  fprintf fmt "(%a %a)" print_var vs (print_type info) vs.vs_ty
+  fprintf fmt "(%a %a)" print_var vs
+    (print_type info) vs.vs_ty
 
 let print_var_list info fmt vsl =
   print_list space (print_typed_var info) fmt vsl
@@ -109,7 +138,8 @@ let rec print_term info fmt t = match t.t_node with
 	"%s.0" "(* %s.0 %s.0)" "(/ %s.0 %s.0)" fmt c
   | Tvar v -> print_var fmt v
   | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
-      | Some s -> syntax_arguments s (print_term info) fmt tl
+      | Some s -> syntax_arguments_typed s (print_term info)
+        (print_type info) (Some t) fmt tl
       | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
           | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
           | _ -> fprintf fmt "@[(%a@ %a)@]"
@@ -132,7 +162,8 @@ and print_fmla info fmt f = match f.f_node with
   | Fapp ({ ls_name = id }, []) ->
       print_ident fmt id
   | Fapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
-      | Some s -> syntax_arguments s (print_term info) fmt tl
+      | Some s -> syntax_arguments_typed s (print_term info)
+        (print_type info) None fmt tl
       | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
           | [] -> fprintf fmt "%a" print_ident ls.ls_name
           | _ -> fprintf fmt "(%a@ %a)"
@@ -144,12 +175,12 @@ and print_fmla info fmt f = match f.f_node with
       (* TODO trigger dépend des capacités du prover : 2 printers?
       smtwithtriggers/smtstrict *)
       if tl = [] then
-        fprintf fmt "@[(%s (%a) %a)@]"
+        fprintf fmt "@[(%s@ (%a)@ %a)@]"
           q
           (print_var_list info) vl
           (print_fmla info) f
       else
-        fprintf fmt "@[(%s (%a) (! %a %a))@]"
+        fprintf fmt "@[(%s@ (%a)@ (! %a %a))@]"
           q
           (print_var_list info) vl
           (print_fmla info) f
@@ -192,24 +223,31 @@ and print_triggers info fmt = function
     (print_triggers info) l
 
 let print_logic_binder info fmt v =
-  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
+  fprintf fmt "%a: %a" print_ident v.vs_name
+    (print_type info) v.vs_ty
 
 let print_type_decl info fmt = function
   | ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
   | ts, Tabstract when ts.ts_args = [] ->
     begin try
+      (* keep this hack for compatibility with smtv1 *)
       let key,elt = Mts.find ts info.barrays in
-      fprintf fmt "(define-sort ((%a  (array %a %a))))"
+      fprintf fmt "(define-sorts (%a  (Array %a %a)))"
         print_ident ts.ts_name
-        (print_type info) key (print_type info) elt; true
+        (print_type info) key
+        (print_type info) elt; true
     with Not_found ->
       fprintf fmt "(declare-sort %a 0)" print_ident ts.ts_name; true end
-  | _, Tabstract -> unsupported
-          "smtv2 : type with argument are not supported"
+  | ts, Tabstract when ts.ts_def = None ->
+    let len = List.length ts.ts_args in
+    fprintf fmt "(declare-sort %a %i)" print_ident ts.ts_name len; true
+  | _, Tabstract -> false
   | _, Talgebraic _ -> unsupported
           "smtv2 : algebraic type are not supported"
 
-let print_logic_decl info fmt (ls,ld) = match ld with
+let print_logic_decl info fmt (ls,ld) =
+  if not (Mid.mem ls.ls_name info.info_syn) then
+  match ld with
   | None ->
     fprintf fmt "@[<hov 2>(declare-fun %a (%a) %a)@]@\n"
       print_ident ls.ls_name
@@ -236,10 +274,12 @@ let print_decl info fmt d = match d.d_node with
       "smt : inductive definition are not supported"
   | Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
   | Dprop (Paxiom, pr, f) ->
+    find_complex_type info fmt f;
       fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a)@]@\n"
         pr.pr_name.id_string
         (print_fmla info) f; true
   | Dprop (Pgoal, pr, f) ->
+    find_complex_type info fmt f;
       fprintf fmt "@[(assert@\n";
       fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
       (match id_from_user pr.pr_name with
@@ -267,14 +307,35 @@ let barrays task =
       | _ -> assert false in
   Task.on_meta Encoding_arrays.meta_mono_array fold Mts.empty task
 
+let meta_dist_syntax =
+  Theory.register_meta "smt_dist_syntax" [MTlsymbol;MTstring]
+
+let distingued =
+  let dist_syntax mls = function
+    | [MAls ls;MAstr s] -> Mls.add ls s mls
+    | _ -> assert false in
+  let dist_dist syntax mls = function
+    | [MAls ls;MAls lsdis] ->
+      begin try
+              Mid.add lsdis.ls_name (Mls.find ls syntax) mls
+        with Not_found -> mls end
+    | _ -> assert false in
+  Trans.on_meta meta_dist_syntax (fun syntax ->
+    let syntax = List.fold_left dist_syntax Mls.empty syntax in
+    Trans.on_meta Encoding_arrays.meta_lsdis (fun dis ->
+      let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
+      Trans.return dis2))
+
 let print_task pr thpr fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
-    info_syn = get_syntax_map task;
+    info_syn = Mid.union (fun _ _ s -> Some s)
+      (get_syntax_map task) (Trans.apply distingued task);
     info_rem = get_remove_set task;
     use_trigger = false;
     barrays = barrays task;
+    complex_type = Hty.create 5;
   }
   in
   let decls = Task.task_decls task in

src/transform/encoding.mli

@@ -22,6 +22,8 @@ open Theory
 open Task
 open Trans
 
+val debug : Debug.flag
+
 val meta_kept : meta
 val meta_kept_array : meta
 val meta_base : meta

src/transform/encoding_arrays.ml

@@ -27,7 +27,7 @@ open Task
 open Decl
 open Encoding
 
-(*
+
 (* Ce type est utiliser pour indiquer un underscore *)
 let tv_dumb = create_tvsymbol (id_fresh "Dumb")
 let ty_dumb = ty_var tv_dumb
@@ -50,26 +50,14 @@ module Mtyl = Map.Make(OHTyl)
 module Htyl = Hashtbl.Make(OHTyl)
 
 (* The environnement of the transformation between two decl (* unmutable *) *)
-type env = {
-  keep : ty Mty.t;
-  poly_ts : tysymbol;
-  edefined_lsymbol : lsymbol Mtyl.t Mls.t;
-}
-
-(* The environnement of the transformation during
-   the transformation of a formula *)
-type menv = {
-  env : env;
-  mutable defined_lsymbol : lsymbol Mtyl.t Mls.t;
-  mutable undef_lsymbol : Sls.t;
-}
+type env = lsymbol Mtyl.t Mls.t
 
 let print_env fmt menv =
   Format.fprintf fmt "defined_lsymbol (%a)@."
     (Pp.print_iter2 Mls.iter Pp.semi Pp.comma Pretty.print_ls
        (Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
           (Pp.print_list Pp.space Pretty.print_ty)
-          Pretty.print_ls)) menv.defined_lsymbol
+          Pretty.print_ls)) menv
 
 (* let create_arrays th = *)
 (*   { *)
@@ -103,97 +91,107 @@ let find_arrays menv ty =
   (*   arrays *)
 *)
 
-let projty menv ty = Mty.find_default ty ty menv.env.keep
-
-let conv_vs menv tvar vsvar vs =
+let find_logic env p tl tyv =
+  if ls_equal p ps_equ then p else
+    try