(*open dimacsTools;;*)

(* Functions for parsing the DIMACS-compliant output of SAT solvers,
   This is generic. Parser for minisat proof log is in minisatParse.ml  *)

(*
** Use Binaryset to encode mapping between HOL variable names
** and DIMACS  variable numbers as a set of string*int pairs.
*)

(*
** substringContains s ss
** tests whether substring ss contains string s
*)

let substringContains s ss =
  let re = Str.regexp_string s in
  match
    (try Str.search_forward re ss 0 with
      Not_found -> -1) with
    -1 -> false
  | _  -> true


(*
** parseSat (s1,s2) ss
** returns a list of numbers corresponding to the tokenised
** substring of ss (tokenised wrt Char.isSpace) that starts immediately
** after the first occurrence of s1 and ends just before the first
** occurrence of s2 that is after the first occurrence of s1
*)

let parseSat (s1,s2) ss =
  let p1 = Str.search_forward (Str.regexp s1) ss 0 in
  let p2 = Str.search_backward (Str.regexp s2) ss (String.length ss) in
  let ss1 = Str.string_before ss p2 in
  let ss2 = Str.string_after ss1 (p1+String.length s1) in
  let ssl = Str.split (Str.regexp "[ \n\t\r]") ss2 in
  List.map int_of_string ssl


(*
** invokeSat solver t
** invokes solver on t and returns SOME s (where s is the satisfying instance
** as a string of integers) or NONE, if unsatisfiable
*)

(*
** Reference containing last command used to invoke a SAT solver
*)

let sat_command = ref "undef"

(*
** Test for success of the result of Process.system
** N.B. isSuccess expected to primitive in next release of
** Moscow ML, and Process.status will lose eqtype status
*)

let satdir = "";;

(* if fname is NONE, then use a temp file, otherwise assume fname.cnf alredy exists*)
let invokeSat sat_solver fname t vc =
  let {name=name;
       url=url;
       executable=executable;
       good_exit=good_exit;
       notime_run=notime_run;
       time_run=time_run;
       only_true=only_true;
       failure_string=failure_string;
       start_string=start_string;
       end_string=end_string} = sat_solver in
  let var_count  =
    match vc with
      Some n -> n |
      None -> List.length(variables t) in
  let tmp        =
    match fname with
      Some fnm ->
        (initSatVarMap var_count;
         ignore (termToDimacs t); (*FIXME: this regenerates sat_var_map:
                                    better to save/load it*)
         fnm)
    | None     -> termToDimacsFile None t var_count in
  let infile     = tmp ^ ".cnf" in
  let outfile    = tmp ^ "." ^ name in
  let ex         = Filename.concat satdir executable in
  let run_cmd    = notime_run ex (infile,outfile) in
  let _          = (sat_command := run_cmd) in
  let code       = Sys.command run_cmd in
  let _          =
    if ((name = "minisat") or (name = "minisatp") or (code = good_exit))
    then ()
    else print_string("Warning:\n Failure signalled by\n " ^ run_cmd ^ "\n") in
  let ins        = Pervasives.open_in outfile in
  let sat_res    = input_all ins in
  let _          = close_in ins in
  let result     = substringContains failure_string sat_res in
  if result
  then None
  else
    let model1 = parseSat(start_string,end_string) sat_res in
    let model2 =
      if only_true
      then model1
        @
          (List.map
             (fun n -> 0-n)
             (subtract (List.map snd (snd(showSatVarMap()))) model1))
      else model1 in
    Some (List.map intToLiteral model2)


(*
** satOracle sat_solver t
** invokes sat_solver on t and returns a theorem tagged by the solver name
** of the form |- (l1 /\ ... ln) ==> t (satisfied with literals l1,...,ln)
** or |- ~t (failure)
*)

let satOracle sat_solver t =
  let res = invokeSat sat_solver None t None in
  match res with
    Some l -> mk_thm ([], mk_imp(list_mk_conj l, t))
  | None   -> mk_thm ([], mk_neg t)

(*
** satProve sat_solver t
** invokes sat_solver on t and if a model is found then
** then it is verified using proof in HOL and a theorem
** |- (l1 /\ ... /\ ln) ==> t is returned
** (where l1,...,ln are the literals making up the model);
** Raises satProveError if no model is found.
** Raises satCheckError if the found model is bogus
*)

(*
** satCheck [l1,...,ln] t
** attempts to prove (l1 /\ ... /\ ln) ==> t
** if it succeeds then the theorem is returned, else
** exception satCheckError is raised
*)

let EQT_Imp1 = TAUT `!b. b ==> (b<=>T)`
let EQF_Imp1 = TAUT `!b. (~b) ==> (b<=>F)`
let EQT_Imp2 = TAUT `!b. (b<=>T) ==> b`;;

exception Sat_check_error

let satCheck model t =
 try
   let mtm  = list_mk_conj model in
   let th1  = ASSUME mtm in
   let thl  = List.map
       (fun th ->
         if is_neg(concl th)
         then MP (SPEC (dest_neg(concl th)) EQF_Imp1) th
         else MP (SPEC (concl th) EQT_Imp1) th)
       (CONJUNCTS th1) in
   let th3 = SUBS_CONV thl t in
   let th4 = CONV_RULE(RAND_CONV(REWRITE_CONV[])) th3 in
   let th5 = MP (SPEC t EQT_Imp2) th4 in
   DISCH mtm th5
 with
   Sys.Break -> raise Sys.Break
 | _         -> raise Sat_check_error;;

exception Sat_prove_error

(* old interface by MJCG. assumes t is in cnf; only for finding SAT *)
let satProve sat_solver t  =
 match invokeSat sat_solver None t None with
   Some model -> satCheck model t
 | None       -> raise Sat_prove_error