# HG changeset patch
# User blanchet
# Date 1402585323 -7200
# Node ID 9a5729600ba94abbb67e5edfb50c6d1890cc21ca
# Parent  a40edeaa01b11ec834f1e4e4a884ce9ac6fe933f
added support for CVC4 in SMT2

diff -r a40edeaa01b1 -r 9a5729600ba9 src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/SMT2.thy	Thu Jun 12 17:02:03 2014 +0200
@@ -393,11 +393,4 @@
 hide_type (open) symb_list pattern
 hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod
 
-declare [[smt2_solver = cvc3]]
-
-lemma "2 + 2 = (4::int)"
-using [[smt2_trace]]
-apply smt2
-done
-
 end
diff -r a40edeaa01b1 -r 9a5729600ba9 src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -62,6 +62,30 @@
 end
 
 
+(* CVC4 *)
+
+local
+  fun cvc4_options ctxt = [
+    "--random-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+    "--lang=smt2",
+    "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT2_Config.timeout))]
+in
+
+val cvc4: SMT2_Solver.solver_config = {
+  name = "cvc4",
+  class = K SMTLIB2_Interface.smtlib2C,
+  avail = make_avail "CVC4",
+  command = make_command "CVC4",
+  options = cvc4_options,
+  smt_options = [],
+  default_max_relevant = 400 (* FUDGE *),
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  parse_proof = NONE,
+  replay = NONE }
+
+end
+
+
 (* Z3 *)
 
 datatype z3_non_commercial =
@@ -135,6 +159,7 @@
 
 val _ = Theory.setup (
   SMT2_Solver.add_solver cvc3 #>
+  SMT2_Solver.add_solver cvc4 #>
   SMT2_Solver.add_solver z3)
 
 end;