path: root/src/zchaff/zchaff.ml

(**************************************************************************)
(*                                                                        *)
(*     SMTCoq                                                             *)
(*     Copyright (C) 2011 - 2021                                          *)
(*                                                                        *)
(*     See file "AUTHORS" for the list of authors                         *)
(*                                                                        *)
(*   This file is distributed under the terms of the CeCILL-C licence     *)
(*                                                                        *)
(**************************************************************************)


open CoqTerms
open SmtForm
open SmtCertif
open SmtTrace
open SatAtom
open SmtMisc


(* Detection of trivial clauses *)

let rec is_trivial cl =
  match cl with
  | l :: cl ->
      let nl = Form.neg l in
      List.exists (fun l' -> Form.equal nl l') cl || is_trivial cl
  | [] -> false


(* Pretty printing *)

let string_of_op = function
  | Ftrue -> "true"
  | Ffalse -> "false"
  | Fand -> "and"
  | For -> "or"
  | Fxor -> "xor"
  | Fimp -> "imp"
  | Fiff -> "iff"
  | Fite -> "ite"
  | Fnot2 i -> "!"^string_of_int i
  | Fforall _ -> assert false

let rec pp_form fmt l =
  Format.fprintf fmt "(#%i %a %a)" (Form.to_lit l)pp_sign l pp_pform (Form.pform l)
and pp_sign fmt l =
  if Form.is_pos l then ()
  else Format.fprintf fmt "-"
and pp_pform fmt p =
  match p with
  | Fatom x -> Format.fprintf fmt "x%i" x
  | Fapp(op,args) ->
      Format.fprintf fmt "%s" (string_of_op op);
      Array.iter (fun a -> Format.fprintf fmt "%a " pp_form a) args
  (* Nothing to do with ZChaff *)
  | FbbT _ -> assert false

let pp_value fmt c =
  match c.value with
  | Some cl ->
      Format.fprintf fmt "VAL = {";
      List.iter (Format.fprintf fmt "%a " pp_form) cl;
      Format.fprintf fmt "}@."
  | _ -> Format.fprintf fmt "Val = empty@."


let pp_kind fmt c =
  match c.kind with
  | Root -> Format.fprintf fmt "Root"
  | Res res ->
      Format.fprintf fmt "(Res %i %i " res.rc1.id res.rc2.id;
      List.iter (fun c -> Format.fprintf fmt "%i " c.id) res.rtail;
      Format.fprintf fmt ") "
  | Other other ->
    begin match other with
    | ImmFlatten (c,l) ->
	Format.fprintf fmt "(ImmFlatten %i %a)"
	  c.id pp_form l
    | True -> Format.fprintf fmt "True"
    | False -> Format.fprintf fmt "False"
    | BuildDef l -> Format.fprintf fmt "(BuildDef %a)" pp_form l
    | BuildDef2 l -> Format.fprintf fmt "(BuildDef2 %a)" pp_form l
    | BuildProj (l,i) -> Format.fprintf fmt "(BuildProj %a %i)" pp_form l i
    | ImmBuildProj (c,i) ->Format.fprintf fmt "(ImmBuildProj %i %i)" c.id i
    | ImmBuildDef c -> Format.fprintf fmt "(ImmBuildDef %i)" c.id
    | ImmBuildDef2 c -> Format.fprintf fmt "(ImmBuildDef %i)" c.id
    | _ -> assert false
    end
  | Same c -> Format.fprintf fmt "(Same %i)" c.id

let rec pp_trace fmt c =
  Format.fprintf fmt "%i = %a %a" c.id pp_kind c pp_value c;
  if c.next <> None then pp_trace fmt (next c)


(******************************************************************************)
(** Given a cnf (dimacs) files and a resolve_trace build                      *)
(*  the corresponding object                                                  *)
(******************************************************************************)


let import_cnf filename =
  let nvars, first, last = CnfParser.parse_cnf filename in
  let reloc = Hashtbl.create 17 in
  let count = ref 0 in
  let r = ref first in
  while !r.next <> None do
    if not (is_trivial (get_val !r)) then begin
      Hashtbl.add reloc !count !r;
      incr count
    end;
    r := next !r
  done;
  if not (is_trivial (get_val !r)) then Hashtbl.add reloc !count !r;
  nvars,first,last,reloc

let import_cnf_trace reloc filename first last =
  (* Format.fprintf Format.err_formatter "init@."; *)
  (* pp_trace Format.err_formatter first; *)
  let confl = ZchaffParser.parse_proof reloc filename last in
  (* Format.fprintf Format.err_formatter "zchaff@."; *)
  (* pp_trace Format.err_formatter first; *)
  SmtTrace.select confl;
  (* Format.fprintf Format.err_formatter "select@."; *)
  (* pp_trace Format.err_formatter first; *)
  Trace.share_prefix first (2 * last.id);
  (* Format.fprintf Format.err_formatter "share_prefix@."; *)
  (* pp_trace Format.err_formatter first; *)
  occur confl;
  let res = alloc first, confl in
  res

let make_roots first last =
  let cint = Lazy.force cint in
  let roots = Array.make (last.id + 2) (CoqTerms.mkArray (cint, Array.make 1 (mkInt 0))) in
  let mk_elem l =
    let x = match Form.pform l with
    | Fatom x -> x + 2
    | _ -> assert false  in
    mkInt (if Form.is_pos l then x lsl 1 else (x lsl 1) lxor 1) in
  let r = ref first in
  while !r.id < last.id do
    let root = Array.of_list (get_val !r) in
    let croot = Array.make (Array.length root + 1) (mkInt 0) in
    Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
    roots.(!r.id) <- CoqTerms.mkArray (cint, croot);
    r := next !r
  done;
  let root = Array.of_list (get_val !r) in
  let croot = Array.make (Array.length root + 1) (mkInt 0) in
  Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
  roots.(!r.id) <- CoqTerms.mkArray (cint, croot);

  CoqTerms.mkArray (mklApp carray [|cint|], roots)

let interp_roots first last =
  let tbl = Hashtbl.create 17 in
  let mk_elem l =
    let x = match Form.pform l with
    | Fatom x -> x
    | _ -> assert false in
    let ph = x lsl 1 in
    let h = if Form.is_pos l then ph else ph lxor 1 in
    try Hashtbl.find tbl h
    with Not_found ->
      let p = CoqInterface.mkApp (CoqInterface.mkRel 1, [|mkInt (x+1)|]) in
      let np = mklApp cnegb [|p|] in
      Hashtbl.add tbl ph p;
      Hashtbl.add tbl (ph lxor 1) np;
      if Form.is_pos l then p else np in
  let interp_root c =
    match get_val c with
    | [] -> Lazy.force cfalse
    | l :: cl ->
	List.fold_left (fun acc l -> mklApp corb [|acc; mk_elem l|])
	  (mk_elem l) cl in
  let res = ref (interp_root first) in
  if first.id <> last.id then begin
    let r = ref (next first) in
    while !r.id <= last.id do
      res := mklApp candb [|!res;interp_root !r|];
      r := next !r
    done;
  end;
  !res

let certif_ops = CoqTerms.csat_checker_certif_ops
let cCertif = CoqTerms.csat_checker_Certif

let parse_certif dimacs trace fdimacs ftrace =
  SmtTrace.clear ();
  let _,first,last,reloc = import_cnf fdimacs in
  let d = make_roots first last in
  let ce1 = CoqInterface.mkUConst d in
  let _ = CoqInterface.declare_constant dimacs ce1 in

  let max_id, confl = import_cnf_trace reloc ftrace first last in
  let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in
  let certif =
   mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
  let ce2 = CoqInterface.mkUConst certif in
  let _ = CoqInterface.declare_constant trace ce2 in
  ()

let cdimacs = CoqTerms.csat_checker_dimacs
let ccertif = CoqTerms.csat_checker_certif
let ctheorem_checker = CoqTerms.csat_checker_theorem_checker
let cchecker = CoqTerms.csat_checker_checker

let theorems interp name fdimacs ftrace =
  SmtTrace.clear ();
  let _,first,last,reloc = import_cnf fdimacs in
  let d = make_roots first last in

  let max_id, confl = import_cnf_trace reloc ftrace first last in
  let (tres,_,_) =
    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in
  let certif =
   mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in

  let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in
  let vtype = CoqInterface.mkArrow (Lazy.force cint) (Lazy.force cbool) in
  let theorem_type =
    CoqInterface.mkProd (CoqInterface.mkName "v", vtype, theorem_concl) in
  let theorem_proof_cast =
    CoqInterface.mkCast (
        CoqInterface.mkLetIn (CoqInterface.mkName "d", d, Lazy.force cdimacs,
        CoqInterface.mkLetIn (CoqInterface.mkName "c", certif, Lazy.force ccertif,
        CoqInterface.mkLambda (CoqInterface.mkName "v", vtype,
        mklApp ctheorem_checker
               [| CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*);
		  vm_cast_true_no_check
		    (mklApp cchecker [|CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*)|]);
                  CoqInterface.mkRel 1(*v*)|]))),
      CoqInterface.vmcast,
      theorem_type)
  in
  let theorem_proof_nocast =
    CoqInterface.mkLetIn (CoqInterface.mkName "d", d, Lazy.force cdimacs,
    CoqInterface.mkLetIn (CoqInterface.mkName "c", certif, Lazy.force ccertif,
    CoqInterface.mkLambda (CoqInterface.mkName "v", vtype,
    mklApp ctheorem_checker
           [| CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*)|])))
  in
  let ce = CoqInterface.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in
  let _ = CoqInterface.declare_constant name ce in
  ()

let theorem = theorems (fun _ -> interp_roots)
let theorem_abs =
  theorems (fun d _ _ -> mklApp csat_checker_valid [|mklApp csat_checker_interp_var [|CoqInterface.mkRel 1(*v*)|]; d|])


let checker fdimacs ftrace =
  SmtTrace.clear ();
  let _,first,last,reloc = import_cnf fdimacs in
  let d = make_roots first last in

  let max_id, confl = import_cnf_trace reloc ftrace first last in
  let (tres,_,_) =
    SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in
  let certif =
    mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in

  let tm = mklApp cchecker [|d; certif|] in

  let res = CoqInterface.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
  Format.eprintf "     = %s\n     : bool@."
    (if CoqInterface.eq_constr res (Lazy.force CoqTerms.ctrue) then
        "true" else "false")





(******************************************************************************)
(** Given a Coq formula build the proof                                       *)
(******************************************************************************)

let export_clause fmt cl =
  List.iter
    (fun l -> Format.fprintf fmt "%s%i "
	(if Form.is_pos l then "" else "-") (Form.index l + 1)) cl;
  Format.fprintf fmt "0@\n"

let export out_channel nvars first =
  let fmt = Format.formatter_of_out_channel out_channel in
  let reloc = Hashtbl.create 17 in
  let count = ref 0 in
  (* count the number of non trivial clause *)
  let r = ref first in
  let add_count c =
    match c.value with
    | Some cl -> if not (is_trivial cl) then incr count
    | _ -> () in
  while !r.next <> None do add_count !r; r := next !r done;
  add_count !r;
  Format.fprintf fmt "p cnf %i %i@." nvars !count;
  count := 0; r := first;
  (* ouput clause *)
  let out c =
    match c.value with
    | Some cl ->
	if not (is_trivial cl) then begin
	  Hashtbl.add reloc !count c;
	  incr count;
	  export_clause fmt cl
	end
    | None -> assert false in
  while !r.next <> None do out !r; r := next !r done;
  out !r;
  Format.fprintf fmt "@.";
  reloc, !r


(* Call zchaff *)

let call_zchaff nvars root =
  let (filename, outchan) = Filename.open_temp_file "zchaff_coq" ".cnf" in
  let resfilename = (Filename.chop_extension filename)^".zlog" in
  let reloc, last = export outchan nvars root in
  close_out outchan;
  let command = "zchaff " ^ filename ^ " > " ^ resfilename in
  Format.eprintf "%s@." command;
  let t0 = Sys.time () in
  let exit_code = Sys.command command in
  let t1 = Sys.time () in
  Format.eprintf "Zchaff = %.5f@." (t1-.t0);
  if exit_code <> 0 then
    failwith ("Zchaff.call_zchaff: command " ^ command ^
	        " exited with code " ^ (string_of_int exit_code));
  let logfilename = (Filename.chop_extension filename) ^ ".log" in
  let command2 = "mv resolve_trace "^logfilename in
  let exit_code2 = Sys.command command2 in
  if exit_code2 <> 0 then
      failwith ("Zchaff.call_zchaff: command " ^ command2 ^
                  " exited with code " ^ (string_of_int exit_code2) ^
        "\nDid you forget to turn on Zchaff proof production?" );
  (* import_cnf_trace reloc logfilename root last  *)
  (reloc, resfilename, logfilename, last)


(* Build the problem that it may be understoof by zchaff *)

let certif_ops = CoqTerms.ccnf_checker_certif_ops
let ccertif = CoqTerms.ccnf_checker_certif
let cCertif = CoqTerms.ccnf_checker_Certif
let cchecker_b_correct = CoqTerms.ccnf_checker_checker_b_correct
let cchecker_b = CoqTerms.ccnf_checker_checker_b
let cchecker_eq_correct = CoqTerms.ccnf_checker_checker_eq_correct
let cchecker_eq = CoqTerms.ccnf_checker_checker_eq

let build_body reify_atom reify_form l b (max_id, confl) vm_cast =
  let ntvar = CoqInterface.mkName "t_var" in
  let ntform = CoqInterface.mkName "t_form" in
  let nc = CoqInterface.mkName "c" in
  let tvar = Atom.interp_tbl reify_atom in
  let _, tform = Form.interp_tbl reify_form in
  let (tres,_,_) =
    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in
  let certif =
    mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
  let vtvar = CoqInterface.mkRel 3 in
  let vtform = CoqInterface.mkRel 2 in
  let vc = CoqInterface.mkRel 1 in
  let add_lets t =
    CoqInterface.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
    CoqInterface.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
    CoqInterface.mkLetIn (nc, certif, Lazy.force ccertif,
    t)))
  in
  let cbc =
    add_lets
      (mklApp cchecker_b [|vtform;l;b;vc|]) |> vm_cast in
  let proof_cast =
    add_lets
      (mklApp cchecker_b_correct [|vtvar; vtform; l; b; vc; cbc|])
  in
  let proof_nocast =
    add_lets
      (mklApp cchecker_b_correct [|vtvar; vtform; l; b; vc|])
  in
  (proof_cast, proof_nocast)


let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast =
  let ntvar = CoqInterface.mkName "t_var" in
  let ntform = CoqInterface.mkName "t_form" in
  let nc = CoqInterface.mkName "c" in
  let tvar = Atom.interp_tbl reify_atom in
  let _, tform = Form.interp_tbl reify_form in
  let (tres,_,_) =
    SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in
  let certif =
    mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
  let vtvar = CoqInterface.mkRel 3 in
  let vtform = CoqInterface.mkRel 2 in
  let vc = CoqInterface.mkRel 1 in
  let add_lets t =
    CoqInterface.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
    CoqInterface.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
    CoqInterface.mkLetIn (nc, certif, Lazy.force ccertif,
    t)))
  in
  let ceqc = add_lets (mklApp cchecker_eq [|vtform;l1;l2;l;vc|])
                 |> vm_cast in
  let proof_cast =
    add_lets
      (mklApp cchecker_eq_correct [|vtvar; vtform; l1; l2; l; vc; ceqc|])
  in
  let proof_nocast =
    add_lets (mklApp cchecker_eq_correct [|vtvar; vtform; l1; l2; l; vc|])
  in
  (proof_cast, proof_nocast)

let get_arguments concl =
  let f, args = CoqInterface.decompose_app concl in
  match args with
  | [ty;a;b] when (CoqInterface.eq_constr f (Lazy.force ceq)) && (CoqInterface.eq_constr ty (Lazy.force cbool)) -> a, b
  | [a] when (CoqInterface.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
  | _ -> failwith ("Zchaff.get_arguments :can only deal with equality over bool")


(* Check that the result is Unsat, otherwise raise a model *)

exception Sat of int list
exception Finished

let input_int file =
  let rec input_int acc flag =
    let c = input_char file in
    if c = '-' then
      input_int acc true
    else if c = '0' then
      input_int (10*acc) flag
    else if c = '1' then
      input_int (10*acc+1) flag
    else if c = '2' then
      input_int (10*acc+2) flag
    else if c = '3' then
      input_int (10*acc+3) flag
    else if c = '4' then
      input_int (10*acc+4) flag
    else if c = '5' then
      input_int (10*acc+5) flag
    else if c = '6' then
      input_int (10*acc+6) flag
    else if c = '7' then
      input_int (10*acc+7) flag
    else if c = '8' then
      input_int (10*acc+8) flag
    else if c = '9' then
      input_int (10*acc+9) flag
    else if c = ' ' then
      if flag then -acc else acc
    else raise Finished in
  input_int 0 false

let check_unsat filename =
  let f = open_in filename in
  let rec get_model acc =
    try
      let i = input_int f in
      get_model (i::acc)
    with
      | Finished -> acc in
  try
    while true do
      let l = input_line f in
      let n = String.length l in
      if n >= 8 && String.sub l 0 8 = "Instance" then
        if n >= 20 && String.sub l 9 11 = "Satisfiable" then
          raise (Sat (get_model []))
        else
          raise End_of_file
    done
  with
    | End_of_file -> close_in f


(* Pre-process the proof given by zchaff *)

let make_proof pform_tbl atom_tbl env reify_form l =
  let fl = Form.flatten reify_form l in
  let root = SmtTrace.mkRootV [l] in
  let _ =
    if Form.equal l fl then Cnf.make_cnf reify_form root
    else
      let first_c = SmtTrace.mkOther (ImmFlatten(root,fl)) (Some [fl]) in
      SmtTrace.link root first_c;
      Cnf.make_cnf reify_form first_c in
  let (reloc, resfilename, logfilename, last) =
    call_zchaff (Form.nvars reify_form) root in
  (try check_unsat resfilename with
    | Sat model -> CoqInterface.error (List.fold_left (fun acc i ->
      let index = if i > 0 then i-1 else -i-1 in
      let ispos = i > 0 in
      try (
        let f = pform_tbl.(index) in
        match f with
          | Fatom a ->
            let t = atom_tbl.(a) in
            let value = if ispos then " = true" else " = false" in
            acc^"  "^(Pp.string_of_ppcmds (CoqInterface.pr_constr_env env t))^value
          | Fapp _ -> acc
          (* Nothing to do with ZChaff *)
          | FbbT _ -> assert false
      ) with | Invalid_argument _ -> acc (* Because cnf computation does not put the new formulas in the table... Perhaps it should? *)
    ) "zchaff found a counterexample:\n" model)
  );
  import_cnf_trace reloc logfilename root last


(* The whole tactic *)

let core_tactic vm_cast env sigma concl =
  SmtTrace.clear ();

  let (forall_let, concl) = Term.decompose_prod_assum concl in
  let a, b = get_arguments concl in
  let reify_atom = Atom.create () in
  let reify_form = Form.create () in
  let (body_cast, body_nocast) =
    if ((CoqInterface.eq_constr b (Lazy.force ctrue)) || (CoqInterface.eq_constr b (Lazy.force cfalse))) then
      let l = Form.of_coq (Atom.get reify_atom) reify_form a in
      let l' = if (CoqInterface.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
      let atom_tbl = Atom.atom_tbl reify_atom in
      let pform_tbl = Form.pform_tbl reify_form in
      let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l' in
      build_body reify_atom reify_form (Form.to_coq l) b max_id_confl (vm_cast env)
    else
      let l1 = Form.of_coq (Atom.get reify_atom) reify_form a in
      let l2 = Form.of_coq (Atom.get reify_atom) reify_form b in
      let l = Form.neg (Form.get reify_form (Fapp(Fiff,[|l1;l2|]))) in
      let atom_tbl = Atom.atom_tbl reify_atom in
      let pform_tbl = Form.pform_tbl reify_form in
      let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l in
      build_body_eq reify_atom reify_form
	(Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl (vm_cast env)
  in

  let compose_lam_assum forall_let body =
    List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in
  let res_cast = compose_lam_assum forall_let body_cast in
  let res_nocast = compose_lam_assum forall_let body_nocast in

  (CoqInterface.tclTHEN
     (CoqInterface.set_evars_tac res_nocast)
     (CoqInterface.vm_cast_no_check res_cast))


let tactic () = CoqInterface.tclTHEN Tactics.intros (CoqInterface.mk_tactic (core_tactic vm_cast_true))
let tactic_no_check () = CoqInterface.tclTHEN Tactics.intros (CoqInterface.mk_tactic (core_tactic (fun _ -> vm_cast_true_no_check)))