# HG changeset patch
# User blanchet
# Date 1410965619 -7200
# Node ID dee1fd1cc631fbae2b418e517d81b6c51d20b17a
# Parent  3782c7b0d1cc604d89444022a606da65b0cb3dd6
added interface for CVC4 extensions

diff -r 3782c7b0d1cc -r dee1fd1cc631 src/HOL/SMT.thy
--- 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.
 *}
diff -r 3782c7b0d1cc -r dee1fd1cc631 src/HOL/Tools/SMT/cvc4_interface.ML
--- /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;
diff -r 3782c7b0d1cc -r dee1fd1cc631 src/HOL/Tools/SMT/smt_datatypes.ML
--- 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
 
diff -r 3782c7b0d1cc -r dee1fd1cc631 src/HOL/Tools/SMT/smt_systems.ML
--- 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,
diff -r 3782c7b0d1cc -r dee1fd1cc631 src/HOL/Tools/SMT/smt_translate.ML
--- 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
diff -r 3782c7b0d1cc -r dee1fd1cc631 src/HOL/Tools/SMT/smtlib_interface.ML
--- 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
diff -r 3782c7b0d1cc -r dee1fd1cc631 src/HOL/Tools/SMT/z3_interface.ML
--- 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