--- 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>
--- 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
--- 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
--- 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 "")
--- 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)}, "<="),
--- 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)
--- 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
--- 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
--- 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;
--- 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
--- 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 =