src/HOL/Tools/SMT/smt_systems.ML
changeset 58360 dee1fd1cc631
parent 58061 3d060f43accb
child 58491 5ddbc170e46c
     1.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Sep 17 16:20:13 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Wed Sep 17 16:53:39 2014 +0200
     1.3 @@ -66,16 +66,22 @@
     1.4  
     1.5  (* CVC4 *)
     1.6  
     1.7 +val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
     1.8 +
     1.9  local
    1.10    fun cvc4_options ctxt = [
    1.11      "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    1.12      "--lang=smt2",
    1.13      "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
    1.14 +
    1.15 +  fun select_class ctxt =
    1.16 +    if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
    1.17 +    else SMTLIB_Interface.smtlibC
    1.18  in
    1.19  
    1.20  val cvc4: SMT_Solver.solver_config = {
    1.21    name = "cvc4",
    1.22 -  class = K SMTLIB_Interface.smtlibC,
    1.23 +  class = select_class,
    1.24    avail = make_avail "CVC4",
    1.25    command = make_command "CVC4",
    1.26    options = cvc4_options,