# HG changeset patch
# User blanchet
# Date 1504024223 -7200
# Node ID 4df6b0ae900dd8877008dbe21ff0968377cab983
# Parent  e5d82cf3c3877ee2b2cea5fb368f62cfe3ed20f5
towards support for HO SMT-LIB

diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/SMT.thy	Tue Aug 29 18:30:23 2017 +0200
@@ -1,12 +1,13 @@
 (*  Title:      HOL/SMT.thy
     Author:     Sascha Boehme, TU Muenchen
+    Author:     Jasmin Blanchette, VU Amsterdam
 *)
 
 section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
 
 theory SMT
-imports Divides
-keywords "smt_status" :: diag
+  imports Divides
+  keywords "smt_status" :: diag
 begin
 
 subsection \<open>A skolemization tactic and proof method\<close>
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/cvc4_interface.ML
--- a/src/HOL/Tools/SMT/cvc4_interface.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -7,24 +7,30 @@
 signature CVC4_INTERFACE =
 sig
   val smtlib_cvc4C: SMT_Util.class
+  val hosmtlib_cvc4C: SMT_Util.class
 end;
 
 structure CVC4_Interface: CVC4_INTERFACE =
 struct
 
-val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
+val cvc4C = ["cvc4"]
+val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
+val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
 
 
 (* interface *)
 
 local
-  fun translate_config ctxt =
-    {logic = K "(set-logic ALL_SUPPORTED)\n", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
-     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+  fun translate_config order ctxt =
+    {order = order,
+     logic = K "(set-logic ALL_SUPPORTED)\n",
+     fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+     serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
 in
 
-val _ =
-  Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
+val _ = Theory.setup (Context.theory_map
+  (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
+   SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))
 
 end
 
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -11,11 +11,11 @@
 
   (*built-in types*)
   val add_builtin_typ: SMT_Util.class ->
-    typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
+    typ * (typ -> (string * typ list) option) * (typ -> int -> string option) -> Context.generic ->
     Context.generic
   val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic ->
     Context.generic
-  val dest_builtin_typ: Proof.context -> typ -> string option
+  val dest_builtin_typ: Proof.context -> typ -> (string * typ list) option
   val is_builtin_typ_ext: Proof.context -> typ -> bool
 
   (*built-in numbers*)
@@ -93,7 +93,8 @@
 structure Builtins = Generic_Data
 (
   type T =
-    (Proof.context -> typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
+    (Proof.context -> typ -> bool,
+     (typ -> (string * typ list) option) * (typ -> int -> string option)) ttab *
     (term list bfun, bfunr option bfun) btab
   val empty = ([], Symtab.empty)
   val extend = I
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -32,6 +32,7 @@
   val statistics: bool Config.T
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
+  val higher_order: bool Config.T
   val nat_as_int: bool Config.T
   val infer_triggers: bool Config.T
   val debug_files: string Config.T
@@ -180,6 +181,7 @@
 val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
 val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
 val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
+val higher_order = Attrib.setup_config_bool @{binding smt_higher_order} (K false)
 val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
 val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
 val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -32,7 +32,7 @@
 
 val setup_builtins =
   SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
-    (@{typ real}, K (SOME "Real"), real_num) #>
+    (@{typ real}, K (SOME ("Real", [])), real_num) #>
   fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
     (@{const less (real)}, "<"),
     (@{const less_eq (real)}, "<="),
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -62,6 +62,7 @@
 
 end
 
+
 (* CVC4 *)
 
 val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
@@ -75,8 +76,16 @@
     "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
 
   fun select_class ctxt =
-    if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
-    else SMTLIB_Interface.smtlibC
+    if Config.get ctxt cvc4_extensions then
+      if Config.get ctxt SMT_Config.higher_order then
+        CVC4_Interface.hosmtlib_cvc4C
+      else
+        CVC4_Interface.smtlib_cvc4C
+    else
+      if Config.get ctxt SMT_Config.higher_order then
+        SMTLIB_Interface.hosmtlibC
+      else
+        SMTLIB_Interface.smtlibC
 in
 
 val cvc4: SMT_Solver.solver_config = {
@@ -93,11 +102,20 @@
 
 end
 
+
 (* veriT *)
 
+local
+  fun select_class ctxt =
+    if Config.get ctxt SMT_Config.higher_order then
+      SMTLIB_Interface.hosmtlibC
+    else
+      SMTLIB_Interface.smtlibC
+in
+
 val veriT: SMT_Solver.solver_config = {
   name = "verit",
-  class = K SMTLIB_Interface.smtlibC,
+  class = select_class,
   avail = make_avail "VERIT",
   command = make_command "VERIT",
   options = (fn ctxt => [
@@ -113,6 +131,9 @@
   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
   replay = NONE }
 
+end
+
+
 (* Z3 *)
 
 val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -10,8 +10,8 @@
   datatype squant = SForall | SExists
   datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
   datatype sterm =
-    SVar of int |
-    SApp of string * sterm list |
+    SVar of int * sterm list |
+    SConst of string * sterm list |
     SQua of squant * string list * sterm spattern list * sterm
 
   (*translation configuration*)
@@ -21,6 +21,7 @@
     dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
     funcs: (string * (string list * string)) list }
   type config = {
+    order: SMT_Util.order,
     logic: term list -> string,
     fp_kinds: BNF_Util.fp_kind list,
     serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -50,8 +51,8 @@
   SPat of 'a list | SNoPat of 'a list
 
 datatype sterm =
-  SVar of int |
-  SApp of string * sterm list |
+  SVar of int * sterm list |
+  SConst of string * sterm list |
   SQua of squant * string list * sterm spattern list * sterm
 
 
@@ -64,6 +65,7 @@
   funcs: (string * (string list * string)) list }
 
 type config = {
+  order: SMT_Util.order,
   logic: term list -> string,
   fp_kinds: BNF_Util.fp_kind list,
   serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -147,7 +149,7 @@
 
     fun add_typ' T proper =
       (case SMT_Builtin.dest_builtin_typ ctxt' T of
-        SOME n => pair n
+        SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *)
       | NONE => add_typ T proper)
 
     fun tr_select sel =
@@ -425,11 +427,12 @@
       | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
       | transT (T as Type _) =
           (case SMT_Builtin.dest_builtin_typ ctxt T of
-            SOME n => pair n
+            SOME (n, []) => pair n
+          | SOME (n, Ts) =>
+            fold_map transT Ts
+            #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns)))
           | NONE => add_typ T true)
 
-    fun app n ts = SApp (n, ts)
-
     fun trans t =
       (case Term.strip_comb t of
         (Const (qn, _), [Abs (_, T, t1)]) =>
@@ -440,17 +443,17 @@
           | NONE => raise TERM ("unsupported quantifier", [t]))
       | (u as Const (c as (_, T)), ts) =>
           (case builtin ctxt c ts of
-            SOME (n, _, us, _) => fold_map trans us #>> app n
-          | NONE => transs u T ts)
-      | (u as Free (_, T), ts) => transs u T ts
-      | (Bound i, []) => pair (SVar i)
+            SOME (n, _, us, _) => fold_map trans us #>> curry SConst n
+          | NONE => trans_applied_fun u T ts)
+      | (u as Free (_, T), ts) => trans_applied_fun u T ts
+      | (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar
       | _ => raise TERM ("bad SMT term", [t]))
 
-    and transs t T ts =
+    and trans_applied_fun t T ts =
       let val (Us, U) = SMT_Util.dest_funT (length ts) T
       in
         fold_map transT Us ##>> transT U #-> (fn Up =>
-          add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
+          add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst)
       end
 
     val (us, trx') = fold_map trans ts trx
@@ -480,7 +483,7 @@
 
 fun translate ctxt smt_options comments ithms =
   let
-    val {logic, fp_kinds, serialize} = get_config ctxt
+    val {order, logic, fp_kinds, serialize} = get_config ctxt
 
     fun no_dtyps (tr_context, ctxt) ts =
       ((Termtab.empty, [], tr_context, ctxt), ts)
@@ -510,10 +513,14 @@
       |> rpair ctxt1
       |-> Lambda_Lifting.lift_lambdas NONE is_binder
       |-> (fn (ts', ll_defs) => fn ctxt' =>
-          (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs)))
-
+        let
+          val ts'' = map mk_trigger ll_defs @ ts'
+            |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs
+        in
+          (ctxt', (ts'', ll_defs))
+        end)
     val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
-      |>> apfst (cons fun_app_eq)
+      |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
   in
     (ts4, tr_context)
     |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smt_util.ML
--- a/src/HOL/Tools/SMT/smt_util.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -10,6 +10,8 @@
   val repeat: ('a -> 'a option) -> 'a -> 'a
   val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
 
+  datatype order = First_Order | Higher_Order
+
   (*class dictionaries*)
   type class = string list
   val basicC: class
@@ -79,6 +81,11 @@
   in rep end
 
 
+(* order *)
+
+datatype order = First_Order | Higher_Order
+
+
 (* class dictionaries *)
 
 type class = string list
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -8,8 +8,9 @@
 signature SMTLIB_INTERFACE =
 sig
   val smtlibC: SMT_Util.class
+  val hosmtlibC: SMT_Util.class
   val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
-  val translate_config: Proof.context -> SMT_Translate.config
+  val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
   val assert_name_of_index: int -> string
   val assert_index_of_name: string -> int
   val assert_prefix : string
@@ -18,7 +19,10 @@
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
 struct
 
-val smtlibC = ["smtlib"]
+val hoC = ["ho"]
+
+val smtlibC = ["smtlib"]   (* SMT-LIB 2 *)
+val hosmtlibC = smtlibC @ hoC   (* possibly SMT-LIB 3 *)
 
 
 (* builtins *)
@@ -36,9 +40,11 @@
 in
 
 val setup_builtins =
+  SMT_Builtin.add_builtin_typ hosmtlibC
+    (@{typ "'a => 'b"}, fn Type (@{type_name fun}, Ts) => SOME ("->", Ts), K (K NONE)) #>
   fold (SMT_Builtin.add_builtin_typ smtlibC) [
-    (@{typ bool}, K (SOME "Bool"), K (K NONE)),
-    (@{typ int}, K (SOME "Int"), int_num)] #>
+    (@{typ bool}, K (SOME ("Bool", [])), K (K NONE)),
+    (@{typ int}, K (SOME ("Int", [])), int_num)] #>
   fold (SMT_Builtin.add_builtin_fun' smtlibC) [
     (@{const True}, "true"),
     (@{const False}, "false"),
@@ -90,9 +96,11 @@
 
 fun var i = "?v" ^ string_of_int i
 
-fun tree_of_sterm l (SMT_Translate.SVar i) = SMTLIB.Sym (var (l - i - 1))
-  | tree_of_sterm _ (SMT_Translate.SApp (n, [])) = SMTLIB.Sym n
-  | tree_of_sterm l (SMT_Translate.SApp (n, ts)) =
+fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1))
+  | tree_of_sterm l (SMT_Translate.SVar (i, ts)) =
+      SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts)
+  | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n
+  | tree_of_sterm l (SMT_Translate.SConst (n, ts)) =
       SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
   | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
       let
@@ -157,13 +165,15 @@
 
 (* interface *)
 
-fun translate_config ctxt = {
+fun translate_config order ctxt = {
+  order = order,
   logic = choose_logic ctxt,
   fp_kinds = [],
   serialize = serialize}
 
 val _ = Theory.setup (Context.theory_map
   (setup_builtins #>
-   SMT_Translate.add_config (smtlibC, translate_config)))
+   SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #>
+   SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order)))
 
 end;
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -24,15 +24,19 @@
 structure Z3_Interface: Z3_INTERFACE =
 struct
 
-val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
+val z3C = ["z3"]
+
+val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C
 
 
 (* interface *)
 
 local
   fun translate_config ctxt =
-    {logic = K "", fp_kinds = [BNF_Util.Least_FP],
-     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+    {order = SMT_Util.First_Order,
+     logic = K "",
+     fp_kinds = [BNF_Util.Least_FP],
+     serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
 
   fun is_div_mod @{const divide (int)} = true
     | is_div_mod @{const modulo (int)} = true
diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Word/Tools/smt_word.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -28,7 +28,8 @@
   fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
   fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
 
-  fun word_typ (Type (@{type_name word}, [T])) = Option.map (index1 "BitVec") (try dest_binT T)
+  fun word_typ (Type (@{type_name word}, [T])) =
+      Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
     | word_typ _ = NONE
 
   fun word_num (Type (@{type_name word}, [T])) k =