this was the thought, but it doesn't quite work

- i want to register the solver but it doesn't work well
  due to the way that dependencies work.

_CoqProject

@@ -1,10 +1,11 @@
 -I src
--R theories SMT
+-Q theories SMT
 
 -I $(COQLIB)/user-contrib/PluginUtils/
 
-# src/smtTactic.ml4
+src/smtTactic.ml4
 src/solver.mli
 src/solver.ml
+src/z3solver.ml
 
-theories/Tactic.v
+theories/Tactic.v

src/smtTactic.ml4

@@ -13,67 +13,85 @@ DECLARE PLUGIN "smtTactic"
 
 module SmtTactic
 : sig
-    val smtTactic : string option -> unit Proofview.tactic
-    val register_smt_solver : string -> (bool -> unit Proofview.tactic) -> unit
+    val smtTactic : ?debug:bool -> string option -> unit Proofview.tactic
+    val register_smt_solver : string -> (string -> bool -> unit Proofview.tactic) -> unit
   end =
 struct
 
   let contrib_name = "smt-check"
 
-  module Smap =
-    Map.Make
-      (struct
-        type t = string
-        let compare = String.compare
-      end)
+  module Scmp =
+  struct
+    type t = string
+    let compare = String.compare
+  end
+  module Smap = Map.Make (Scmp)
 
-  let all_solvers = ref Smap.empty
+  let smt_debug = ref true
 
-  let register_smt_solver name solver =
+  let all_solvers : (string -> bool -> unit Proofview.tactic) Smap.t ref =
+    ref Smap.empty
+
+  let register_smt_solver (name : string) solver =
     all_solvers := Smap.add name solver !all_solvers
 
-  type SmtSolver =
-  { name : string
-  ; run : bool -> unit Proofview.tactic }
+  type smtSolver =
+    { name : string
+    ; run : bool -> unit Proofview.tactic }
 
-  let pr_SmtSolver s = Pp.(str s.name)
+  let the_solver    =
+    ref { name = "<unset>"
+        ; run = fun _ ->
+            Tacticals.New.tclFAIL 0 Pp.(str "solver not set") }
 
   let smt_parser s =
-    if s = "z3" then
-      SmtLib2 s
-    else if Str.string_match (Str.regexp "smtlib2: (.+)") s 0 then
-      SmtLib2 (Str.matched_group 1 s)
-    else raise (Failure "invalid solver")
-
-  let the_solver    = ref
-  let smt_reader () = Pp.string_of_ppcmds (pr_SmtSolver "z3")
-  let smt_setter s  = the_solver := smt_parser s
+    let (name, args) =
+      try
+        let split = String.index s ':' in
+        let first = String.sub s 0 (split - 1) in
+        let arg = String.sub s split (String.length s - split) in
+        (first, arg)
+      with
+        Not_found -> (s,"")
+    in
+    try
+      let solver = Smap.find name !all_solvers in
+      { name =
+          if args = "" then name
+          else name ^ ": " ^ args
+      ; run = solver args }
+    with
+      Not_found ->
+      raise (Failure ("Unknown solver: " ^ name))
+
+  let smt_reader () = !the_solver.name
+  let smt_setter s =
+    the_solver := smt_parser s
 
   let _ =
-    declare_string_option
-      { opt_sync = false
+    Goptions.(declare_string_option
+      { optsync  = false
       ; optdepr  = false
       ; optkey   = ["SMT"; "Solver"]
       ; optname  = "set the smt solver for the smt-check plugin to use"
       ; optread  = smt_reader
-      ; optwrite = smt_setter }
+      ; optwrite = smt_setter })
 
   let _ =
-    declare_bool_option
-      { opt_sync = false
+    Goptions.(declare_bool_option
+      { optsync  = false
       ; optdepr  = false
       ; optkey   = ["SMT"; "Debug"]
       ; optname  = "print debugging output"
-      ; optread  = smt_reader
-      ; optwrite = smt_setter }
-
+      ; optread  = (fun () -> !smt_debug)
+      ; optwrite = (:=) smt_debug })
 
   (** This is the entry-point to the tactic **)
-  let smtTactic = function
-      None -> !the_solver !smt_debug
+  let smtTactic ?debug = function
+      None -> (!the_solver).run (Option.default !smt_debug debug)
     | Some solver ->
       try
-        Smap.find solver !all_solvers !smt_debug
+        (smt_parser solver).run (Option.default !smt_debug debug)
       with
         Not_found ->
         let msg = Pp.(str "No SMT solver named: " ++ qstring solver) in
@@ -82,13 +100,13 @@ struct
 end
 
 TACTIC EXTEND smt_tac_solve
-  | ["smt" "solve"]     ->     [SmtTactic.smtTactic None]
+  | ["smt" "solve"] -> [SmtTactic.smtTactic None]
 END;;
 
-TACTIC EXTEND smt_tac_solve_with
-  | ["smt" "solve" "calling" string(s)] -> [SmtTactic.smtTactic (Some s)]
+TACTIC EXTEND smt_tac_solve_dbg
+  | ["smt" "solve_dbg"] -> [SmtTactic.smtTactic ~debug:true None]
 END;;
 
-TACTIC EXTEND smg_tac_solve_dbg
-  | ["smt" "solve_dbg"] ->     [SmtTactic.with_debugging SmtTactic.smtTactic None]
+TACTIC EXTEND smt_tac_solve_calling
+  | ["smt" "solve" "calling" string(s)] -> [SmtTactic.smtTactic (Some s)]
 END;;

src/solver.ml

@@ -15,9 +15,12 @@ sig
   val parse_hypothesis : Environ.env -> Evd.evar_map ->
     Names.Id.t -> Term.constr -> instance -> instance
 
-  val write_instance : pretty:bool -> out_channel -> instance -> unit
+  val write_instance : ?pretty:bool -> Format.formatter -> instance -> unit
 
   val get_variable : string -> instance -> Term.constr
+
+  (* Returning [None] means the conclusion *)
+  val get_hypothesis : string -> instance -> Names.identifier option
 end
 
 module ParseOnlyProp (P : Instance) :
@@ -42,7 +45,7 @@ struct
 
   let write_instance = P.write_instance
   let get_variable = P.get_variable
-
+  let get_hypothesis = P.get_hypothesis
 end
 
 type smt_result =
@@ -57,8 +60,9 @@ sig
   val execute : instance -> smt_result
 end
 
-module Solver (Parse : Instance)
-              (Exec : Exec with type instance = Parse.instance) : Solver =
+module Make
+    (Parse : Instance)
+    (Exec : Exec with type instance = Parse.instance) : Solver =
 struct
   open Parse
   open Exec
@@ -105,7 +109,7 @@ struct
 end
 
 
-module RealInstance =
+module RealInstance : Instance =
 struct
 
   module Std = Coqstd.Std
@@ -338,82 +342,8 @@ struct
       None -> raise Not_found
     | Some x -> x
 
-end
-
-module Z3Exec =
-struct
-  open RealInstance
-
-  type instance = RealInstance.instance
-
-  let debug x =
-    Pp.msg_debug (x ())
-
-  let ptrn_success = Str.regexp "^unsat (\\([^)]*\\))"
-  let ptrn_failure = Str.regexp "^sat ([^)]*) (model\\(.+\\)) ?$"
-  let ptrn_unknown = Str.regexp "^unknown"
-  let ptrn_split = Str.regexp " "
-
-  let ptrn_def = Str.regexp "(define-fun \\(\\w+\\) () Real[ \n\r\t]+(?\\(-? [0-9]*.[0-9]*\\))?)"
-
-  let extract_model inst =
-    let rec extract_model start result =
-      debug (fun _ -> Pp.(str "extract model: " ++ fnl () ++
-                          str (String.sub result start (String.length result - start)) ++ fnl ())) ;
-      try
-        let _ = Str.search_forward ptrn_def result start in
-        let var = RealInstance.get_variable (Str.matched_group 1 result) inst in
-        let value = Str.matched_group 2 result in
-        (var, value) :: extract_model (Str.match_end ()) result
-      with
-        Not_found -> []
-    in extract_model
-
-  let parse_result inst result =
-    let _ =
-      debug (fun _ -> Pp.(str "Z3 output" ++ fnl () ++ str result))
-    in
-    let result = Str.global_replace (Str.regexp (Str.quote "\n")) " " result in
-    let result = Str.global_replace (Str.regexp (Str.quote "\r")) "" result in
-    if Str.string_partial_match ptrn_success result 0 then
-      let lst = Str.matched_group 1 result in
-      let names = Str.split ptrn_split lst in
-      let (concl, hyps) = List.partition (fun x -> x = conclusion_name) names in
-      Unsat (concl = [],
-             List.map Names.id_of_string hyps)
-    else if Str.string_match ptrn_failure result 0 then
-      let result = Str.matched_group 1 result in
-      Sat (extract_model inst 0 result)
-    else if Str.string_match ptrn_unknown result 0 then
-      Unknown
-    else
-      let _ = Format.eprintf "Bad Z3 output:\n%s" result in
-      assert false
-
-  let execute inst =
-    let (in_channel,out_channel) = Unix.open_process "z3 -in -smt2" in
-    let _ =
-      begin
-	let fmt = Format.formatter_of_out_channel out_channel in
-	Format.fprintf fmt "(set-option :produce-unsat-cores true)\n" ;
-	Format.fprintf fmt "(set-option :produce-models true)\n" ;
-        RealInstance.write_instance fmt inst ;
-	Format.fprintf fmt "(check-sat)\n(get-unsat-core)\n(get-model)" ;
-	Format.pp_print_flush fmt () ;
-	flush out_channel ;
-	close_out out_channel
-      end
-    in
-    let buffer_size = 2048 in
-    let buffer = Buffer.create buffer_size in
-    let string = Bytes.create buffer_size in
-    let chars_read = ref 1 in
-    while !chars_read <> 0 do
-      chars_read := input in_channel string 0 buffer_size;
-      Buffer.add_substring buffer string 0 !chars_read
-    done;
-    ignore (Unix.close_process (in_channel, out_channel));
-    let result = Buffer.contents buffer in
-    parse_result inst result
+  let get_hypothesis x inst =
+    if x = conclusion_name then None
+    else Some (Names.id_of_string x)
 
 end

src/solver.mli

@@ -14,9 +14,12 @@ sig
   val parse_hypothesis : Environ.env -> Evd.evar_map ->
     Names.Id.t -> Term.constr -> instance -> instance
 
-  val write_instance : pretty:bool -> out_channel -> instance -> unit
+  val write_instance : ?pretty:bool -> Format.formatter -> instance -> unit
 
   val get_variable : string -> instance -> Term.constr
+
+  (* Returning [None] means the conclusion *)
+  val get_hypothesis : string -> instance -> Names.identifier option
 end
 
 module ParseOnlyProp (I : Instance) : Instance with type instance = I.instance
@@ -33,5 +36,8 @@ sig
   val execute : instance -> smt_result
 end
 
-module Solver (Parse : Instance)
-              (Exec : Exec with type instance = Parse.instance) : Solver
+module Make
+    (Parse : Instance)
+    (Exec : Exec with type instance = Parse.instance) : Solver
+
+module RealInstance : Instance