--- a/src/HOL/SMT.thy Wed Sep 17 16:20:13 2014 +0200
+++ b/src/HOL/SMT.thy Wed Sep 17 16:53:39 2014 +0200
@@ -112,15 +112,16 @@
ML_file "Tools/SMT/z3_proof.ML"
ML_file "Tools/SMT/z3_isar.ML"
ML_file "Tools/SMT/smt_solver.ML"
+ML_file "Tools/SMT/cvc4_interface.ML"
+ML_file "Tools/SMT/verit_proof.ML"
+ML_file "Tools/SMT/verit_isar.ML"
+ML_file "Tools/SMT/verit_proof_parse.ML"
ML_file "Tools/SMT/z3_interface.ML"
ML_file "Tools/SMT/z3_replay_util.ML"
ML_file "Tools/SMT/z3_replay_literals.ML"
ML_file "Tools/SMT/z3_replay_rules.ML"
ML_file "Tools/SMT/z3_replay_methods.ML"
ML_file "Tools/SMT/z3_replay.ML"
-ML_file "Tools/SMT/verit_proof.ML"
-ML_file "Tools/SMT/verit_isar.ML"
-ML_file "Tools/SMT/verit_proof_parse.ML"
ML_file "Tools/SMT/smt_systems.ML"
method_setup smt = {*
@@ -196,6 +197,14 @@
declare [[smt_infer_triggers = false]]
text {*
+Enable the following option to use built-in support for datatypes,
+codatatypes, and records in CVC4. Currently, this is implemented only
+in oracle mode.
+*}
+
+declare [[cvc4_extensions = false]]
+
+text {*
Enable the following option to use built-in support for div/mod, datatypes,
and records in Z3. Currently, this is implemented only in oracle mode.
*}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML Wed Sep 17 16:53:39 2014 +0200
@@ -0,0 +1,31 @@
+(* Title: HOL/Tools/SMT/cvc4_interface.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Interface to CVC4 based on an extended version of SMT-LIB.
+*)
+
+signature CVC4_INTERFACE =
+sig
+ val smtlib_cvc4C: SMT_Util.class
+end;
+
+structure CVC4_Interface: CVC4_INTERFACE =
+struct
+
+val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
+
+
+(* interface *)
+
+local
+ fun translate_config ctxt =
+ {logic = K "", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+ serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+in
+
+val _ =
+ Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
+
+end
+
+end;
--- a/src/HOL/Tools/SMT/smt_datatypes.ML Wed Sep 17 16:20:13 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML Wed Sep 17 16:53:39 2014 +0200
@@ -7,7 +7,7 @@
signature SMT_DATATYPES =
sig
- val add_decls: typ ->
+ val add_decls: BNF_Util.fp_kind -> typ ->
(typ * (term * term list) list) list list * Proof.context ->
(typ * (term * term list) list) list list * Proof.context
end;
@@ -63,7 +63,7 @@
[] => ([], ctxt)
| info :: _ => (get_typedef_decl info T Ts, ctxt)))
-fun add_decls T (declss, ctxt) =
+fun add_decls fp T (declss, ctxt) =
let
fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
--- a/src/HOL/Tools/SMT/smt_systems.ML Wed Sep 17 16:20:13 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Wed Sep 17 16:53:39 2014 +0200
@@ -66,16 +66,22 @@
(* CVC4 *)
+val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
+
local
fun cvc4_options ctxt = [
"--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
"--lang=smt2",
"--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
in
val cvc4: SMT_Solver.solver_config = {
name = "cvc4",
- class = K SMTLIB_Interface.smtlibC,
+ class = select_class,
avail = make_avail "CVC4",
command = make_command "CVC4",
options = cvc4_options,
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Sep 17 16:20:13 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Sep 17 16:53:39 2014 +0200
@@ -23,7 +23,7 @@
funcs: (string * (string list * string)) list }
type config = {
logic: term list -> string,
- has_datatypes: bool,
+ fp_kinds: BNF_Util.fp_kind list,
serialize: (string * string) list -> string list -> sign -> sterm list -> string }
type replay_data = {
context: Proof.context,
@@ -66,7 +66,7 @@
type config = {
logic: term list -> string,
- has_datatypes: bool,
+ fp_kinds: BNF_Util.fp_kind list,
serialize: (string * string) list -> string list -> sign -> sterm list -> string }
type replay_data = {
@@ -139,7 +139,8 @@
fun collect_datatypes_and_records (tr_context, ctxt) ts =
let
- val (declss, ctxt') = fold (Term.fold_types SMT_Datatypes.add_decls) ts ([], ctxt)
+ val (declss, ctxt') =
+ fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Least_FP)) ts ([], ctxt)
fun is_decl_typ T = exists (exists (equal T o fst)) declss
@@ -478,7 +479,7 @@
fun translate ctxt smt_options comments ithms =
let
- val {logic, has_datatypes, serialize} = get_config ctxt
+ val {logic, fp_kinds, serialize} = get_config ctxt
fun no_dtyps (tr_context, ctxt) ts =
((Termtab.empty, [], tr_context, ctxt), ts)
@@ -487,7 +488,8 @@
val ((funcs, dtyps, tr_context, ctxt1), ts2) =
((empty_tr_context, ctxt), ts1)
- |-> (if has_datatypes then collect_datatypes_and_records else no_dtyps)
+ |-> (if member (op =) fp_kinds BNF_Util.Least_FP then collect_datatypes_and_records
+ else no_dtyps)
fun is_binder (Const (@{const_name Let}, _) $ _) = true
| is_binder t = Lambda_Lifting.is_quantifier t
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Wed Sep 17 16:20:13 2014 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Sep 17 16:53:39 2014 +0200
@@ -153,7 +153,7 @@
fun translate_config ctxt = {
logic = choose_logic ctxt,
- has_datatypes = false,
+ fp_kinds = [],
serialize = serialize}
val _ = Theory.setup (Context.theory_map
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Sep 17 16:20:13 2014 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Sep 17 16:53:39 2014 +0200
@@ -31,7 +31,7 @@
local
fun translate_config ctxt =
- {logic = K "", has_datatypes = true,
+ {logic = K "", fp_kinds = [BNF_Util.Least_FP],
serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
fun is_div_mod @{const div (int)} = true