added interface for CVC4 extensions
authorblanchet
Wed Sep 17 16:53:39 2014 +0200 (2014-09-17)
changeset 58360dee1fd1cc631
parent 58359 3782c7b0d1cc
child 58361 7f2b3b6f6ad1
added interface for CVC4 extensions
src/HOL/SMT.thy
src/HOL/Tools/SMT/cvc4_interface.ML
src/HOL/Tools/SMT/smt_datatypes.ML
src/HOL/Tools/SMT/smt_systems.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
     1.1 --- a/src/HOL/SMT.thy	Wed Sep 17 16:20:13 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Sep 17 16:53:39 2014 +0200
     1.3 @@ -112,15 +112,16 @@
     1.4  ML_file "Tools/SMT/z3_proof.ML"
     1.5  ML_file "Tools/SMT/z3_isar.ML"
     1.6  ML_file "Tools/SMT/smt_solver.ML"
     1.7 +ML_file "Tools/SMT/cvc4_interface.ML"
     1.8 +ML_file "Tools/SMT/verit_proof.ML"
     1.9 +ML_file "Tools/SMT/verit_isar.ML"
    1.10 +ML_file "Tools/SMT/verit_proof_parse.ML"
    1.11  ML_file "Tools/SMT/z3_interface.ML"
    1.12  ML_file "Tools/SMT/z3_replay_util.ML"
    1.13  ML_file "Tools/SMT/z3_replay_literals.ML"
    1.14  ML_file "Tools/SMT/z3_replay_rules.ML"
    1.15  ML_file "Tools/SMT/z3_replay_methods.ML"
    1.16  ML_file "Tools/SMT/z3_replay.ML"
    1.17 -ML_file "Tools/SMT/verit_proof.ML"
    1.18 -ML_file "Tools/SMT/verit_isar.ML"
    1.19 -ML_file "Tools/SMT/verit_proof_parse.ML"
    1.20  ML_file "Tools/SMT/smt_systems.ML"
    1.21  
    1.22  method_setup smt = {*
    1.23 @@ -196,6 +197,14 @@
    1.24  declare [[smt_infer_triggers = false]]
    1.25  
    1.26  text {*
    1.27 +Enable the following option to use built-in support for datatypes,
    1.28 +codatatypes, and records in CVC4. Currently, this is implemented only
    1.29 +in oracle mode.
    1.30 +*}
    1.31 +
    1.32 +declare [[cvc4_extensions = false]]
    1.33 +
    1.34 +text {*
    1.35  Enable the following option to use built-in support for div/mod, datatypes,
    1.36  and records in Z3. Currently, this is implemented only in oracle mode.
    1.37  *}
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/SMT/cvc4_interface.ML	Wed Sep 17 16:53:39 2014 +0200
     2.3 @@ -0,0 +1,31 @@
     2.4 +(*  Title:      HOL/Tools/SMT/cvc4_interface.ML
     2.5 +    Author:     Sascha Boehme, TU Muenchen
     2.6 +
     2.7 +Interface to CVC4 based on an extended version of SMT-LIB.
     2.8 +*)
     2.9 +
    2.10 +signature CVC4_INTERFACE =
    2.11 +sig
    2.12 +  val smtlib_cvc4C: SMT_Util.class
    2.13 +end;
    2.14 +
    2.15 +structure CVC4_Interface: CVC4_INTERFACE =
    2.16 +struct
    2.17 +
    2.18 +val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
    2.19 +
    2.20 +
    2.21 +(* interface *)
    2.22 +
    2.23 +local
    2.24 +  fun translate_config ctxt =
    2.25 +    {logic = K "", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
    2.26 +     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
    2.27 +in
    2.28 +
    2.29 +val _ =
    2.30 +  Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
    2.31 +
    2.32 +end
    2.33 +
    2.34 +end;
     3.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 16:20:13 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Sep 17 16:53:39 2014 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  signature SMT_DATATYPES =
     3.6  sig
     3.7 -  val add_decls: typ ->
     3.8 +  val add_decls: BNF_Util.fp_kind -> typ ->
     3.9      (typ * (term * term list) list) list list * Proof.context ->
    3.10      (typ * (term * term list) list) list list * Proof.context
    3.11  end;
    3.12 @@ -63,7 +63,7 @@
    3.13          [] => ([], ctxt)
    3.14        | info :: _ => (get_typedef_decl info T Ts, ctxt)))
    3.15  
    3.16 -fun add_decls T (declss, ctxt) =
    3.17 +fun add_decls fp T (declss, ctxt) =
    3.18    let
    3.19      fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
    3.20  
     4.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Sep 17 16:20:13 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Wed Sep 17 16:53:39 2014 +0200
     4.3 @@ -66,16 +66,22 @@
     4.4  
     4.5  (* CVC4 *)
     4.6  
     4.7 +val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
     4.8 +
     4.9  local
    4.10    fun cvc4_options ctxt = [
    4.11      "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    4.12      "--lang=smt2",
    4.13      "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
    4.14 +
    4.15 +  fun select_class ctxt =
    4.16 +    if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
    4.17 +    else SMTLIB_Interface.smtlibC
    4.18  in
    4.19  
    4.20  val cvc4: SMT_Solver.solver_config = {
    4.21    name = "cvc4",
    4.22 -  class = K SMTLIB_Interface.smtlibC,
    4.23 +  class = select_class,
    4.24    avail = make_avail "CVC4",
    4.25    command = make_command "CVC4",
    4.26    options = cvc4_options,
     5.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 17 16:20:13 2014 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Sep 17 16:53:39 2014 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4      funcs: (string * (string list * string)) list }
     5.5    type config = {
     5.6      logic: term list -> string,
     5.7 -    has_datatypes: bool,
     5.8 +    fp_kinds: BNF_Util.fp_kind list,
     5.9      serialize: (string * string) list -> string list -> sign -> sterm list -> string }
    5.10    type replay_data = {
    5.11      context: Proof.context,
    5.12 @@ -66,7 +66,7 @@
    5.13  
    5.14  type config = {
    5.15    logic: term list -> string,
    5.16 -  has_datatypes: bool,
    5.17 +  fp_kinds: BNF_Util.fp_kind list,
    5.18    serialize: (string * string) list -> string list -> sign -> sterm list -> string }
    5.19  
    5.20  type replay_data = {
    5.21 @@ -139,7 +139,8 @@
    5.22  
    5.23  fun collect_datatypes_and_records (tr_context, ctxt) ts =
    5.24    let
    5.25 -    val (declss, ctxt') = fold (Term.fold_types SMT_Datatypes.add_decls) ts ([], ctxt)
    5.26 +    val (declss, ctxt') =
    5.27 +      fold (Term.fold_types (SMT_Datatypes.add_decls BNF_Util.Least_FP)) ts ([], ctxt)
    5.28  
    5.29      fun is_decl_typ T = exists (exists (equal T o fst)) declss
    5.30  
    5.31 @@ -478,7 +479,7 @@
    5.32  
    5.33  fun translate ctxt smt_options comments ithms =
    5.34    let
    5.35 -    val {logic, has_datatypes, serialize} = get_config ctxt
    5.36 +    val {logic, fp_kinds, serialize} = get_config ctxt
    5.37  
    5.38      fun no_dtyps (tr_context, ctxt) ts =
    5.39        ((Termtab.empty, [], tr_context, ctxt), ts)
    5.40 @@ -487,7 +488,8 @@
    5.41  
    5.42      val ((funcs, dtyps, tr_context, ctxt1), ts2) =
    5.43        ((empty_tr_context, ctxt), ts1)
    5.44 -      |-> (if has_datatypes then collect_datatypes_and_records else no_dtyps)
    5.45 +      |-> (if member (op =) fp_kinds BNF_Util.Least_FP then collect_datatypes_and_records
    5.46 +        else no_dtyps)
    5.47  
    5.48      fun is_binder (Const (@{const_name Let}, _) $ _) = true
    5.49        | is_binder t = Lambda_Lifting.is_quantifier t
     6.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Sep 17 16:20:13 2014 +0200
     6.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Sep 17 16:53:39 2014 +0200
     6.3 @@ -153,7 +153,7 @@
     6.4  
     6.5  fun translate_config ctxt = {
     6.6    logic = choose_logic ctxt,
     6.7 -  has_datatypes = false,
     6.8 +  fp_kinds = [],
     6.9    serialize = serialize}
    6.10  
    6.11  val _ = Theory.setup (Context.theory_map
     7.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Sep 17 16:20:13 2014 +0200
     7.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Sep 17 16:53:39 2014 +0200
     7.3 @@ -31,7 +31,7 @@
     7.4  
     7.5  local
     7.6    fun translate_config ctxt =
     7.7 -    {logic = K "", has_datatypes = true,
     7.8 +    {logic = K "", fp_kinds = [BNF_Util.Least_FP],
     7.9       serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
    7.10  
    7.11    fun is_div_mod @{const div (int)} = true