From cfb4587e26623318f432c7e3e21711afc2b966e7 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 12 Jan 2015 16:28:10 +0100 Subject: Initial import of SMTCoq v1.2 --- src/trace/coqTerms.ml | 187 ++++++++++++ src/trace/satAtom.ml | 65 ++++ src/trace/smtAtom.ml | 748 +++++++++++++++++++++++++++++++++++++++++++++++ src/trace/smtAtom.mli | 175 +++++++++++ src/trace/smtCertif.ml | 140 +++++++++ src/trace/smtCnf.ml | 264 +++++++++++++++++ src/trace/smtForm.ml | 510 ++++++++++++++++++++++++++++++++ src/trace/smtForm.mli | 99 +++++++ src/trace/smtMisc.ml | 47 +++ src/trace/smtTrace.ml | 465 +++++++++++++++++++++++++++++ src/trace/smt_tactic.ml4 | 55 ++++ 11 files changed, 2755 insertions(+) create mode 100644 src/trace/coqTerms.ml create mode 100644 src/trace/satAtom.ml create mode 100644 src/trace/smtAtom.ml create mode 100644 src/trace/smtAtom.mli create mode 100644 src/trace/smtCertif.ml create mode 100644 src/trace/smtCnf.ml create mode 100644 src/trace/smtForm.ml create mode 100644 src/trace/smtForm.mli create mode 100644 src/trace/smtMisc.ml create mode 100644 src/trace/smtTrace.ml create mode 100644 src/trace/smt_tactic.ml4 (limited to 'src/trace') diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml new file mode 100644 index 0000000..1ee6448 --- /dev/null +++ b/src/trace/coqTerms.ml @@ -0,0 +1,187 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +open Coqlib + +let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) + +(* Int63 *) +let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]] + +let cint = gen_constant int63_modules "int" +let ceq63 = gen_constant int63_modules "eqb" + +(* PArray *) +let parray_modules = [["Coq";"Array";"PArray"]] + +let carray = gen_constant parray_modules "array" + +(* Positive *) +let positive_modules = [["Coq";"Numbers";"BinNums"]; + ["Coq";"PArith";"BinPosDef";"Pos"]] + +let cpositive = gen_constant positive_modules "positive" +let cxI = gen_constant positive_modules "xI" +let cxO = gen_constant positive_modules "xO" +let cxH = gen_constant positive_modules "xH" +let ceqbP = gen_constant positive_modules "eqb" + +(* Z *) +let z_modules = [["Coq";"Numbers";"BinNums"]; + ["Coq";"ZArith";"BinInt"]; + ["Coq";"ZArith";"BinInt";"Z"]] + +let cZ = gen_constant z_modules "Z" +let cZ0 = gen_constant z_modules "Z0" +let cZpos = gen_constant z_modules "Zpos" +let cZneg = gen_constant z_modules "Zneg" +let copp = gen_constant z_modules "opp" +let cadd = gen_constant z_modules "add" +let csub = gen_constant z_modules "sub" +let cmul = gen_constant z_modules "mul" +let cltb = gen_constant z_modules "ltb" +let cleb = gen_constant z_modules "leb" +let cgeb = gen_constant z_modules "geb" +let cgtb = gen_constant z_modules "gtb" +(* Je ne comprends pas pourquoi ça fonctionne avec Zeq_bool et pas avec + Z.eqb *) +(* let ceqbZ = gen_constant z_modules "eqb" *) +let ceqbZ = gen_constant [["Coq";"ZArith";"Zbool"]] "Zeq_bool" + +(* Booleans *) +let bool_modules = [["Coq";"Bool";"Bool"]] + +let cbool = gen_constant init_modules "bool" +let ctrue = gen_constant init_modules "true" +let cfalse = gen_constant init_modules "false" +let candb = gen_constant init_modules "andb" +let corb = gen_constant init_modules "orb" +let cxorb = gen_constant init_modules "xorb" +let cnegb = gen_constant init_modules "negb" +let cimplb = gen_constant init_modules "implb" +let ceqb = gen_constant bool_modules "eqb" +let cifb = gen_constant bool_modules "ifb" +let creflect = gen_constant bool_modules "reflect" + +(* Lists *) +let clist = gen_constant init_modules "list" +let cnil = gen_constant init_modules "nil" +let ccons = gen_constant init_modules "cons" + + +(* Option *) +let coption = gen_constant init_modules "option" +let cSome = gen_constant init_modules "Some" +let cNone = gen_constant init_modules "None" + +(* Pairs *) +let cpair = gen_constant init_modules "pair" + +(* Logical Operators *) +let cnot = gen_constant init_modules "not" +let ceq = gen_constant init_modules "eq" +let crefl_equal = gen_constant init_modules "eq_refl" + +(* SMT_terms *) + +let smt_modules = [ ["SMTCoq";"Misc"]; + ["SMTCoq";"State"]; + ["SMTCoq";"SMT_terms"]; + ["SMTCoq";"SMT_terms";"Typ"]; + ["SMTCoq";"SMT_terms";"Form"]; + ["SMTCoq";"SMT_terms";"Atom"] + ] + +let cdistinct = gen_constant smt_modules "distinct" + +let ctype = gen_constant smt_modules "type" +let cTZ = gen_constant smt_modules "TZ" +let cTbool = gen_constant smt_modules "Tbool" +let cTpositive = gen_constant smt_modules "Tpositive" +let cTindex = gen_constant smt_modules "Tindex" + +let ctyp_eqb = gen_constant smt_modules "typ_eqb" +let cTyp_eqb = gen_constant smt_modules "Typ_eqb" +let cte_carrier = gen_constant smt_modules "te_carrier" +let cte_eqb = gen_constant smt_modules "te_eqb" +let cunit_typ_eqb = gen_constant smt_modules "unit_typ_eqb" + +let ctval = gen_constant smt_modules "tval" +let cTval = gen_constant smt_modules "Tval" + +let cCO_xH = gen_constant smt_modules "CO_xH" +let cCO_Z0 = gen_constant smt_modules "CO_Z0" + +let cUO_xO = gen_constant smt_modules "UO_xO" +let cUO_xI = gen_constant smt_modules "UO_xI" +let cUO_Zpos = gen_constant smt_modules "UO_Zpos" +let cUO_Zneg = gen_constant smt_modules "UO_Zneg" +let cUO_Zopp = gen_constant smt_modules "UO_Zopp" + +let cBO_Zplus = gen_constant smt_modules "BO_Zplus" +let cBO_Zminus = gen_constant smt_modules "BO_Zminus" +let cBO_Zmult = gen_constant smt_modules "BO_Zmult" +let cBO_Zlt = gen_constant smt_modules "BO_Zlt" +let cBO_Zle = gen_constant smt_modules "BO_Zle" +let cBO_Zge = gen_constant smt_modules "BO_Zge" +let cBO_Zgt = gen_constant smt_modules "BO_Zgt" +let cBO_eq = gen_constant smt_modules "BO_eq" + +let cNO_distinct = gen_constant smt_modules "NO_distinct" + +let catom = gen_constant smt_modules "atom" +let cAcop = gen_constant smt_modules "Acop" +let cAuop = gen_constant smt_modules "Auop" +let cAbop = gen_constant smt_modules "Abop" +let cAnop = gen_constant smt_modules "Anop" +let cAapp = gen_constant smt_modules "Aapp" + +let cform = gen_constant smt_modules "form" +let cFatom = gen_constant smt_modules "Fatom" +let cFtrue = gen_constant smt_modules "Ftrue" +let cFfalse = gen_constant smt_modules "Ffalse" +let cFnot2 = gen_constant smt_modules "Fnot2" +let cFand = gen_constant smt_modules "Fand" +let cFor = gen_constant smt_modules "For" +let cFxor = gen_constant smt_modules "Fxor" +let cFimp = gen_constant smt_modules "Fimp" +let cFiff = gen_constant smt_modules "Fiff" +let cFite = gen_constant smt_modules "Fite" + +let cis_true = gen_constant smt_modules "is_true" + +let make_certif_ops modules = + (gen_constant modules "step", + gen_constant modules "Res", gen_constant modules "ImmFlatten", + gen_constant modules "CTrue", gen_constant modules "CFalse", + gen_constant modules "BuildDef", gen_constant modules "BuildDef2", + gen_constant modules "BuildProj", + gen_constant modules "ImmBuildProj", gen_constant modules"ImmBuildDef", + gen_constant modules"ImmBuildDef2", + gen_constant modules "EqTr", gen_constant modules "EqCgr", gen_constant modules "EqCgrP", + gen_constant modules "LiaMicromega", gen_constant modules "LiaDiseq", gen_constant modules "SplArith", gen_constant modules "SplDistinctElim") + + +(** Usefull construction *) + +let ceq_refl_true = + lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|]) + +let eq_refl_true () = Lazy.force ceq_refl_true + +let vm_cast_true t = + Term.mkCast(eq_refl_true (), + Term.VMcast, + SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]) diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml new file mode 100644 index 0000000..ca72504 --- /dev/null +++ b/src/trace/satAtom.ml @@ -0,0 +1,65 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +open SmtMisc +open CoqTerms + +module Atom = + struct + + type t = int + + let index a = a + + let equal a1 a2 = a1 == a2 + + let is_bool_type a = true + + type reify_tbl = + { mutable count : int; + tbl : (Term.constr, int) Hashtbl.t + } + + let create () = + { count = 0; + tbl = Hashtbl.create 17 } + + let declare reify a = + let res = reify.count in + Hashtbl.add reify.tbl a res; + reify.count <- res + 1; + res + + let get reify a = + try Hashtbl.find reify.tbl a + with Not_found -> declare reify a + + let atom_tbl reify = + let t = Array.make (reify.count + 1) (Lazy.force ctrue) in + let set c i = t.(i) <- c in + Hashtbl.iter set reify.tbl; + t + + let interp_tbl reify = + Term.mkArray (Lazy.force cbool, atom_tbl reify) + + end + +module Form = SmtForm.Make(Atom) +module Trace = SmtTrace.MakeOpt(Form) +module Cnf = SmtCnf.MakeCnf(Form) + + + diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml new file mode 100644 index 0000000..3164692 --- /dev/null +++ b/src/trace/smtAtom.ml @@ -0,0 +1,748 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +open SmtMisc +open CoqTerms + +(** Syntaxified version of Coq type *) +type indexed_type = Term.constr gen_hashed + +let dummy_indexed_type i = {index = i; hval = Term.mkProp} +let indexed_type_index i = i.index + +type btype = + | TZ + | Tbool + | Tpositive + | Tindex of indexed_type + +module Btype = + struct + + let index_tbl = Hashtbl.create 17 + + let index_to_coq i = + let i = i.index in + try Hashtbl.find index_tbl i + with Not_found -> + let interp = mklApp cTindex [|mkInt i|] in + Hashtbl.add index_tbl i interp; + interp + + let equal t1 t2 = + match t1,t2 with + | Tindex i, Tindex j -> i.index == j.index + | _ -> t1 == t2 + + let to_coq = function + | TZ -> Lazy.force cTZ + | Tbool -> Lazy.force cTbool + | Tpositive -> Lazy.force cTpositive + | Tindex i -> index_to_coq i + + let to_smt fmt = function + | TZ -> Format.fprintf fmt "Int" + | Tbool -> Format.fprintf fmt "Bool" + | Tpositive -> Format.fprintf fmt "Int" + | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index + + (* reify table *) + type reify_tbl = + { mutable count : int; + tbl : (Term.constr, btype) Hashtbl.t + } + + let create () = + let htbl = Hashtbl.create 17 in + Hashtbl.add htbl (Lazy.force cZ) TZ; + Hashtbl.add htbl (Lazy.force cbool) Tbool; + (* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *) + { count = 0; + tbl = htbl } + + let declare reify t typ_eqb = + (* TODO: allows to have only typ_eqb *) + assert (not (Hashtbl.mem reify.tbl t)); + let res = Tindex {index = reify.count; hval = typ_eqb} in + Hashtbl.add reify.tbl t res; + reify.count <- reify.count + 1; + res + + let of_coq reify t = + try + Hashtbl.find reify.tbl t + with | Not_found -> + let eq_t = declare_new_variable (Names.id_of_string "eq") (Term.mkArrow t (Term.mkArrow t (Lazy.force cbool))) in + let x = mkName "x" in + let y = mkName "y" in + let rx = Term.mkRel 2 in + let ry = Term.mkRel 1 in + let eq_refl = Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in + let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl")) eq_refl in + let ce = mklApp cTyp_eqb [|t;eq_t;eq_refl_v|] in + declare reify t ce + + let interp_tbl reify = + let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_eqb) in + let set _ = function + | Tindex it -> t.(it.index) <- it.hval + | _ -> () in + Hashtbl.iter set reify.tbl; + Term.mkArray (Lazy.force ctyp_eqb, t) + + let to_list reify = + let set _ t acc = match t with + | Tindex it -> (it.index,it)::acc + | _ -> acc in + Hashtbl.fold set reify.tbl [] + + let interp_to_coq reify = function + | TZ -> Lazy.force cZ + | Tbool -> Lazy.force cbool + | Tpositive -> Lazy.force cpositive + | Tindex c -> mklApp cte_carrier [|c.hval|] + + end + +(** Operators *) + +type cop = + | CO_xH + | CO_Z0 + +type uop = + | UO_xO + | UO_xI + | UO_Zpos + | UO_Zneg + | UO_Zopp + +type bop = + | BO_Zplus + | BO_Zminus + | BO_Zmult + | BO_Zlt + | BO_Zle + | BO_Zge + | BO_Zgt + | BO_eq of btype + +type nop = + | NO_distinct of btype + +type op_def = { + tparams : btype array; + tres : btype; + op_val : Term.constr } + +type indexed_op = op_def gen_hashed + +let dummy_indexed_op i dom codom = {index = i; hval = {tparams = dom; tres = codom; op_val = Term.mkProp}} +let indexed_op_index op = op.index + +type op = + | Cop of cop + | Uop of uop + | Bop of bop + | Nop of nop + | Iop of indexed_op + +module Op = + struct + let c_to_coq = function + | CO_xH -> Lazy.force cCO_xH + | CO_Z0 -> Lazy.force cCO_Z0 + + let c_type_of = function + | CO_xH -> Tpositive + | CO_Z0 -> TZ + + let interp_cop = function + | CO_xH -> Lazy.force cxH + | CO_Z0 -> Lazy.force cZ0 + + let u_to_coq = function + | UO_xO -> Lazy.force cUO_xO + | UO_xI -> Lazy.force cUO_xI + | UO_Zpos -> Lazy.force cUO_Zpos + | UO_Zneg -> Lazy.force cUO_Zneg + | UO_Zopp -> Lazy.force cUO_Zopp + + let u_type_of = function + | UO_xO | UO_xI -> Tpositive + | UO_Zpos | UO_Zneg | UO_Zopp -> TZ + + let u_type_arg = function + | UO_xO | UO_xI | UO_Zpos | UO_Zneg -> Tpositive + | UO_Zopp -> TZ + + let interp_uop = function + | UO_xO -> Lazy.force cxO + | UO_xI -> Lazy.force cxI + | UO_Zpos -> Lazy.force cZpos + | UO_Zneg -> Lazy.force cZneg + | UO_Zopp -> Lazy.force copp + + let eq_tbl = Hashtbl.create 17 + + let eq_to_coq t = + try Hashtbl.find eq_tbl t + with Not_found -> + let op = mklApp cBO_eq [|Btype.to_coq t|] in + Hashtbl.add eq_tbl t op; + op + + let b_to_coq = function + | BO_Zplus -> Lazy.force cBO_Zplus + | BO_Zminus -> Lazy.force cBO_Zminus + | BO_Zmult -> Lazy.force cBO_Zmult + | BO_Zlt -> Lazy.force cBO_Zlt + | BO_Zle -> Lazy.force cBO_Zle + | BO_Zge -> Lazy.force cBO_Zge + | BO_Zgt -> Lazy.force cBO_Zgt + | BO_eq t -> eq_to_coq t + + let b_type_of = function + | BO_Zplus | BO_Zminus | BO_Zmult -> TZ + | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt | BO_eq _ -> Tbool + + let b_type_args = function + | BO_Zplus | BO_Zminus | BO_Zmult + | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt -> (TZ,TZ) + | BO_eq t -> (t,t) + + let interp_eq = function + | TZ -> Lazy.force ceqbZ + | Tbool -> Lazy.force ceqb + | Tpositive -> Lazy.force ceqbP + | Tindex i -> mklApp cte_eqb [|i.hval|] + + let interp_bop = function + | BO_Zplus -> Lazy.force cadd + | BO_Zminus -> Lazy.force csub + | BO_Zmult -> Lazy.force cmul + | BO_Zlt -> Lazy.force cltb + | BO_Zle -> Lazy.force cleb + | BO_Zge -> Lazy.force cgeb + | BO_Zgt -> Lazy.force cgtb + | BO_eq t -> interp_eq t + + let n_to_coq = function + | NO_distinct t -> mklApp cNO_distinct [|Btype.to_coq t|] + + let n_type_of = function + | NO_distinct _ -> Tbool + + let n_type_args = function + | NO_distinct ty -> ty + + let interp_distinct = function + | TZ -> Lazy.force cZ + | Tbool -> Lazy.force cbool + | Tpositive -> Lazy.force cpositive + | Tindex i -> mklApp cte_carrier [|i.hval|] + + let interp_nop = function + | NO_distinct ty -> mklApp cdistinct [|interp_distinct ty;interp_eq ty|] + + let i_to_coq i = mkInt i.index + + let i_type_of i = i.hval.tres + + let i_type_args i = i.hval.tparams + + (* reify table *) + type reify_tbl = + { mutable count : int; + tbl : (Term.constr, indexed_op) Hashtbl.t + } + + let create () = + { count = 0; + tbl = Hashtbl.create 17 } + + let declare reify op tparams tres = + assert (not (Hashtbl.mem reify.tbl op)); + let v = { tparams = tparams; tres = tres; op_val = op } in + let res = {index = reify.count; hval = v } in + Hashtbl.add reify.tbl op res; + reify.count <- reify.count + 1; + res + + let of_coq reify op = + Hashtbl.find reify.tbl op + + + let interp_tbl tval mk_Tval reify = + let t = Array.make (reify.count + 1) + (mk_Tval [||] Tbool (Lazy.force ctrue)) in + let set _ v = + t.(v.index) <- mk_Tval v.hval.tparams v.hval.tres v.hval.op_val in + Hashtbl.iter set reify.tbl; + Term.mkArray (tval, t) + + let to_list reify = + let set _ op acc = + let value = op.hval in + (op.index,value.tparams,value.tres,op)::acc in + Hashtbl.fold set reify.tbl [] + + let c_equal op1 op2 = op1 == op2 + + let u_equal op1 op2 = op1 == op2 + + let b_equal op1 op2 = + match op1,op2 with + | BO_eq t1, BO_eq t2 -> Btype.equal t1 t2 + | _ -> op1 == op2 + + let n_equal op1 op2 = + match op1,op2 with + | NO_distinct t1, NO_distinct t2 -> Btype.equal t1 t2 + + let i_equal op1 op2 = op1.index == op2.index + + end + + +(** Definition of atoms *) + +type atom = + | Acop of cop + | Auop of uop * hatom + | Abop of bop * hatom * hatom + | Anop of nop * hatom array + | Aapp of indexed_op * hatom array + +and hatom = atom gen_hashed + +(* let pp_acop = function *) +(* | CO_xH -> "CO_xH" *) +(* | CO_Z0 -> "CO_Z0" *) + +(* let pp_auop = function *) +(* | UO_xO -> "UO_xO" *) +(* | UO_xI -> "UO_xI" *) +(* | UO_Zpos -> "UO_Zpos" *) +(* | UO_Zneg -> "UO_Zneg" *) +(* | UO_Zopp -> "UO_Zopp" *) + +(* let pp_abop = function *) +(* | BO_Zplus -> "BO_Zplus" *) +(* | BO_Zminus -> "BO_Zminus" *) +(* | BO_Zmult -> "BO_Zmult" *) +(* | BO_Zlt -> "BO_Zlt" *) +(* | BO_Zle -> "BO_Zle" *) +(* | BO_Zge -> "BO_Zge" *) +(* | BO_Zgt -> "BO_Zgt" *) +(* | BO_eq _ -> "(BO_eq ??)" *) + +(* let rec pp_atom = function *) +(* | Acop c -> "(Acop "^(pp_acop c)^")" *) +(* | Auop (u,b) -> "(Auop "^(pp_auop u)^" "^(pp_atom b.hval)^")" *) +(* | Abop (b,c,d) -> "(Abop "^(pp_abop b)^" "^(pp_atom c.hval)^" "^(pp_atom d.hval)^")" *) +(* | Aapp (op,a) -> "(Aapp "^(string_of_int op.index)^" ("^(Array.fold_left (fun acc h -> acc^" "^(pp_atom h.hval)) "" a)^"))" *) + +module HashedAtom = + struct + type t = atom + + let equal a b = + match a, b with + | Acop opa, Acop opb -> Op.c_equal opa opb + | Auop(opa,ha), Auop(opb,hb) -> Op.u_equal opa opb && ha.index == hb.index + | Abop(opa,ha1,ha2), Abop(opb,hb1,hb2) -> + Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index + | Anop (opa,ha), Anop (opb,hb) -> + let na = Array.length ha in + let nb = Array.length hb in + let i = ref (-1) in + Op.n_equal opa opb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha + | Aapp (va,ha), Aapp (vb,hb) -> + let na = Array.length ha in + let nb = Array.length hb in + let i = ref (-1) in + Op.i_equal va vb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha + | _, _ -> false + + let hash = function + | Acop op -> ((Hashtbl.hash op) lsl 3) lxor 1 + | Auop (op,h) -> + (( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2 + | Abop (op,h1,h2) -> + (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3 + | Anop (op, args) -> + let hash_args = + match Array.length args with + | 0 -> 0 + | 1 -> args.(0).index + | 2 -> args.(1).index lsl 2 + args.(0).index + | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in + (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4 + | Aapp (op, args) -> + let hash_args = + match Array.length args with + | 0 -> 0 + | 1 -> args.(0).index + | 2 -> args.(1).index lsl 2 + args.(0).index + | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in + (hash_args lsl 5 + op.index lsl 3) lxor 4 + + end + +module HashAtom = Hashtbl.Make(HashedAtom) + +module Atom = + struct + + type t = hatom + + let atom h = h.hval + let index h = h.index + + let equal h1 h2 = h1.index == h2.index + + let type_of h = + match h.hval with + | Acop op -> Op.c_type_of op + | Auop (op,_) -> Op.u_type_of op + | Abop (op,_,_) -> Op.b_type_of op + | Anop (op,_) -> Op.n_type_of op + | Aapp (op,_) -> Op.i_type_of op + + let is_bool_type h = Btype.equal (type_of h) Tbool + + + let rec compute_int = function + | Acop c -> + (match c with + | CO_xH -> 1 + | CO_Z0 -> 0) + | Auop (op,h) -> + (match op with + | UO_xO -> 2*(compute_hint h) + | UO_xI -> 2*(compute_hint h) + 1 + | UO_Zpos -> compute_hint h + | UO_Zneg -> - (compute_hint h) + | UO_Zopp -> assert false) + | _ -> assert false + + and compute_hint h = compute_int (atom h) + + let to_smt_int fmt i = + let s1 = if i < 0 then "(- " else "" in + let s2 = if i < 0 then ")" else "" in + let j = if i < 0 then -i else i in + Format.fprintf fmt "%s%i%s" s1 j s2 + + let rec to_smt fmt h = to_smt_atom fmt (atom h) + + and to_smt_atom fmt = function + | Acop _ as a -> to_smt_int fmt (compute_int a) + | Auop (UO_Zopp,h) -> + Format.fprintf fmt "(- "; + to_smt fmt h; + Format.fprintf fmt ")" + | Auop _ as a -> to_smt_int fmt (compute_int a) + | Abop (op,h1,h2) -> to_smt_bop fmt op h1 h2 + | Anop (op,a) -> to_smt_nop fmt op a + | Aapp (op,a) -> + if Array.length a = 0 then ( + Format.fprintf fmt "op_%i" op.index; + ) else ( + Format.fprintf fmt "(op_%i" op.index; + Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a; + Format.fprintf fmt ")" + ) + + and to_smt_bop fmt op h1 h2 = + let s = match op with + | BO_Zplus -> "+" + | BO_Zminus -> "-" + | BO_Zmult -> "*" + | BO_Zlt -> "<" + | BO_Zle -> "<=" + | BO_Zge -> ">=" + | BO_Zgt -> ">" + | BO_eq _ -> "=" in + Format.fprintf fmt "(%s " s; + to_smt fmt h1; + Format.fprintf fmt " "; + to_smt fmt h2; + Format.fprintf fmt ")" + + and to_smt_nop fmt op a = + let s = match op with + | NO_distinct _ -> "distinct" in + Format.fprintf fmt "(%s" s; + Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a; + Format.fprintf fmt ")" + + + + exception NotWellTyped of atom + + let check a = + match a with + | Acop _ -> () + | Auop(op,h) -> + if not (Btype.equal (Op.u_type_arg op) (type_of h)) then + raise (NotWellTyped a) + | Abop(op,h1,h2) -> + let (t1,t2) = Op.b_type_args op in + if not (Btype.equal t1 (type_of h1) && Btype.equal t2 (type_of h2)) + then raise (NotWellTyped a) + | Anop(op,ha) -> + let ty = Op.n_type_args op in + Array.iter (fun h -> if not (Btype.equal ty (type_of h)) then raise (NotWellTyped a)) ha + | Aapp(op,args) -> + let tparams = Op.i_type_args op in + Array.iteri (fun i t -> + if not (Btype.equal t (type_of args.(i))) then + raise (NotWellTyped a)) tparams + + type reify_tbl = + { mutable count : int; + tbl : hatom HashAtom.t + } + + let create () = + { count = 0; + tbl = HashAtom.create 17 } + + let clear reify = + reify.count <- 0; + HashAtom.clear reify.tbl + + let declare reify a = + check a; + let res = {index = reify.count; hval = a} in + HashAtom.add reify.tbl a res; + reify.count <- reify.count + 1; + res + + let get reify a = + try HashAtom.find reify.tbl a + with Not_found -> declare reify a + + + (** Given a coq term, build the corresponding atom *) + type coq_cst = + | CCxH + | CCZ0 + | CCxO + | CCxI + | CCZpos + | CCZneg + | CCZopp + | CCZplus + | CCZminus + | CCZmult + | CCZlt + | CCZle + | CCZge + | CCZgt + | CCeqb + | CCeqbP + | CCeqbZ + | CCunknown + + let op_tbl () = + let tbl = Hashtbl.create 29 in + let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in + List.iter add + [ cxH,CCxH; cZ0,CCZ0; + cxO,CCxO; cxI,CCxI; cZpos,CCZpos; cZneg,CCZneg; copp,CCZopp; + cadd,CCZplus; csub,CCZminus; cmul,CCZmult; cltb,CCZlt; + cleb,CCZle; cgeb,CCZge; cgtb,CCZgt; ceqb,CCeqb; ceqbP,CCeqbP; + ceqbZ, CCeqbZ + ]; + tbl + + let op_tbl = lazy (op_tbl ()) + + let of_coq rt ro reify env sigma c = + let op_tbl = Lazy.force op_tbl in + let get_cst c = + try Hashtbl.find op_tbl c with Not_found -> CCunknown in + let mk_cop op = get reify (Acop op) in + let rec mk_hatom h = + let c, args = Term.decompose_app h in + match get_cst c with + | CCxH -> mk_cop CO_xH + | CCZ0 -> mk_cop CO_Z0 + | CCxO -> mk_uop UO_xO args + | CCxI -> mk_uop UO_xI args + | CCZpos -> mk_uop UO_Zpos args + | CCZneg -> mk_uop UO_Zneg args + | CCZopp -> mk_uop UO_Zopp args + | CCZplus -> mk_bop BO_Zplus args + | CCZminus -> mk_bop BO_Zminus args + | CCZmult -> mk_bop BO_Zmult args + | CCZlt -> mk_bop BO_Zlt args + | CCZle -> mk_bop BO_Zle args + | CCZge -> mk_bop BO_Zge args + | CCZgt -> mk_bop BO_Zgt args + | CCeqb -> mk_bop (BO_eq Tbool) args + | CCeqbP -> mk_bop (BO_eq Tpositive) args + | CCeqbZ -> mk_bop (BO_eq TZ) args + | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h) + + and mk_uop op = function + | [a] -> let h = mk_hatom a in get reify (Auop (op,h)) + | _ -> assert false + + and mk_bop op = function + | [a1;a2] -> + let h1 = mk_hatom a1 in + let h2 = mk_hatom a2 in + get reify (Abop (op,h1,h2)) + | _ -> assert false + + and mk_unknown c args ty = + let hargs = Array.of_list (List.map mk_hatom args) in + let op = + try Op.of_coq ro c + with | Not_found -> + let targs = Array.map type_of hargs in + let tres = Btype.of_coq rt ty in + Op.declare ro c targs tres in + get reify (Aapp (op,hargs)) in + + mk_hatom c + + + let to_coq h = mkInt h.index + + let a_to_coq a = + match a with + | Acop op -> mklApp cAcop [|Op.c_to_coq op|] + | Auop (op,h) -> mklApp cAuop [|Op.u_to_coq op; to_coq h|] + | Abop (op,h1,h2) -> + mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|] + | Anop (op,ha) -> + let cop = Op.n_to_coq op in + let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) ha (mklApp cnil [|Lazy.force cint|]) in + mklApp cAnop [|cop; cargs|] + | Aapp (op,args) -> + let cop = Op.i_to_coq op in + let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) args (mklApp cnil [|Lazy.force cint|]) in + mklApp cAapp [|cop; cargs|] + + let dft_atom = lazy (mklApp cAcop [| Lazy.force cCO_xH |]) + + let to_array reify dft f = + let t = Array.make (reify.count + 1) dft in + let set _ h = t.(h.index) <- f h.hval in + HashAtom.iter set reify.tbl; + t + + let interp_tbl reify = + let t = to_array reify (Lazy.force dft_atom) a_to_coq in + Term.mkArray (Lazy.force catom, t) + + + (** Producing a Coq term corresponding to the interpretation of an atom *) + let interp_to_coq atom_tbl a = + let rec interp_atom a = + let l = index a in + try Hashtbl.find atom_tbl l + with Not_found -> + let pc = + match atom a with + | Acop c -> Op.interp_cop c + | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|]) + | Abop (op,h1,h2) -> Term.mkApp (Op.interp_bop op, [|interp_atom h1; interp_atom h2|]) + | Anop (NO_distinct ty as op,ha) -> + let cop = Op.interp_nop op in + let typ = Op.interp_distinct ty in + let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in + Term.mkApp (cop,[|cargs|]) + | Aapp (op,t) -> Term.mkApp (op.hval.op_val, Array.map interp_atom t) in + Hashtbl.add atom_tbl l pc; + pc in + interp_atom a + + + (* Generation of atoms *) + + let mk_nop op reify a = get reify (Anop (op,a)) + + let mk_binop op reify h1 h2 = get reify (Abop (op, h1, h2)) + + let mk_unop op reify h = get reify (Auop (op, h)) + + let rec hatom_pos_of_int reify i = + if i <= 1 then + get reify (Acop CO_xH) + else + if i land 1 = 0 + then mk_unop UO_xO reify (hatom_pos_of_int reify (i lsr 1)) + else mk_unop UO_xI reify (hatom_pos_of_int reify (i lsr 1)) + + let hatom_Z_of_int reify i = + if i = 0 then + get reify (Acop CO_Z0) + else + if i > 0 + then mk_unop UO_Zpos reify (hatom_pos_of_int reify i) + else mk_unop UO_Zneg reify (hatom_pos_of_int reify (-i)) + + let rec hatom_pos_of_bigint reify i = + if Big_int.le_big_int i Big_int.unit_big_int then + get reify (Acop CO_xH) + else + let (q,r) = Big_int.quomod_big_int i (Big_int.big_int_of_int 2) in + if Big_int.eq_big_int r Big_int.zero_big_int then + mk_unop UO_xO reify (hatom_pos_of_bigint reify q) + else + mk_unop UO_xI reify (hatom_pos_of_bigint reify q) + + let hatom_Z_of_bigint reify i = + if Big_int.eq_big_int i Big_int.zero_big_int then + get reify (Acop CO_Z0) + else + if Big_int.gt_big_int i Big_int.zero_big_int then + mk_unop UO_Zpos reify (hatom_pos_of_bigint reify i) + else + mk_unop UO_Zneg reify (hatom_pos_of_bigint reify (Big_int.minus_big_int i)) + + let mk_eq reify ty h1 h2 = + let op = BO_eq ty in + try + HashAtom.find reify.tbl (Abop (op, h1, h2)) + with + | Not_found -> + try + HashAtom.find reify.tbl (Abop (op, h2, h1)) + with + | Not_found -> + declare reify (Abop (op, h1, h2)) + + let mk_lt = mk_binop BO_Zlt + let mk_le = mk_binop BO_Zle + let mk_gt = mk_binop BO_Zgt + let mk_ge = mk_binop BO_Zge + let mk_plus = mk_binop BO_Zplus + let mk_minus = mk_binop BO_Zminus + let mk_mult = mk_binop BO_Zmult + let mk_opp = mk_unop UO_Zopp + let mk_distinct reify ty = mk_nop (NO_distinct ty) reify + + end + + +module Form = SmtForm.Make(Atom) +module Trace = SmtTrace.MakeOpt(Form) diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli new file mode 100644 index 0000000..8eadb49 --- /dev/null +++ b/src/trace/smtAtom.mli @@ -0,0 +1,175 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +type indexed_type + +val dummy_indexed_type: int -> indexed_type +val indexed_type_index : indexed_type -> int + +type btype = + | TZ + | Tbool + | Tpositive + | Tindex of indexed_type + +module Btype : + sig + + val equal : btype -> btype -> bool + + val to_coq : btype -> Term.constr + + val to_smt : Format.formatter -> btype -> unit + + type reify_tbl + + val create : unit -> reify_tbl + + val declare : reify_tbl -> Term.constr -> Term.constr -> btype + + val of_coq : reify_tbl -> Term.constr -> btype + + val interp_tbl : reify_tbl -> Term.constr + + val to_list : reify_tbl -> (int * indexed_type) list + + val interp_to_coq : reify_tbl -> btype -> Term.constr + + end + +(** Operators *) + +type cop = + | CO_xH + | CO_Z0 + +type uop = + | UO_xO + | UO_xI + | UO_Zpos + | UO_Zneg + | UO_Zopp + +type bop = + | BO_Zplus + | BO_Zminus + | BO_Zmult + | BO_Zlt + | BO_Zle + | BO_Zge + | BO_Zgt + | BO_eq of btype + +type nop = + | NO_distinct of btype + +type indexed_op + +val dummy_indexed_op: int -> btype array -> btype -> indexed_op +val indexed_op_index : indexed_op -> int + +module Op : + sig + + type reify_tbl + + val create : unit -> reify_tbl + + val declare : reify_tbl -> Term.constr -> btype array -> btype -> indexed_op + + val of_coq : reify_tbl -> Term.constr -> indexed_op + + val interp_tbl : Term.constr -> + (btype array -> btype -> Term.constr -> Term.constr) -> + reify_tbl -> Term.constr + + val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list + + end + + +(** Definition of atoms *) + +type hatom + +type atom = + | Acop of cop + | Auop of uop * hatom + | Abop of bop * hatom * hatom + | Anop of nop * hatom array + | Aapp of indexed_op * hatom array + + + +module Atom : + sig + + type t = hatom + + val equal : hatom -> hatom -> bool + + val index : hatom -> int + + val atom : hatom -> atom + + val type_of : hatom -> btype + + val to_smt : Format.formatter -> t -> unit + + exception NotWellTyped of atom + + type reify_tbl + + val create : unit -> reify_tbl + + val clear : reify_tbl -> unit + + val get : reify_tbl -> atom -> hatom + + (** Given a coq term, build the corresponding atom *) + val of_coq : Btype.reify_tbl -> Op.reify_tbl -> reify_tbl -> + Environ.env -> Evd.evar_map -> Term.constr -> t + + val to_coq : hatom -> Term.constr + + val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array + + val interp_tbl : reify_tbl -> Term.constr + + val interp_to_coq : (int, Term.constr) Hashtbl.t -> + t -> Term.constr + + (* Generation of atoms *) + val hatom_Z_of_int : reify_tbl -> int -> hatom + val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> hatom + val mk_eq : reify_tbl -> btype -> hatom -> hatom -> hatom + val mk_lt : reify_tbl -> hatom -> hatom -> hatom + val mk_le : reify_tbl -> hatom -> hatom -> hatom + val mk_gt : reify_tbl -> hatom -> hatom -> hatom + val mk_ge : reify_tbl -> hatom -> hatom -> hatom + val mk_plus : reify_tbl -> hatom -> hatom -> hatom + val mk_minus : reify_tbl -> hatom -> hatom -> hatom + val mk_mult : reify_tbl -> hatom -> hatom -> hatom + val mk_opp : reify_tbl -> hatom -> hatom + val mk_distinct : reify_tbl -> btype -> hatom array -> hatom + + end + + +module Form : SmtForm.FORM with type hatom = hatom +module Trace : sig + val share_prefix : Form.t SmtCertif.clause -> int -> unit +end diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml new file mode 100644 index 0000000..76036a5 --- /dev/null +++ b/src/trace/smtCertif.ml @@ -0,0 +1,140 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +open SmtForm + +type used = int + +type clause_id = int + +type 'hform rule = + | ImmFlatten of 'hform clause * 'hform + + (* CNF Transformations *) + | True + (* * true : {true} + *) + | False + (* * false : {(not false)} + *) + | BuildDef of 'hform (* the first literal of the clause *) + (* * and_neg : {(and a_1 ... a_n) (not a_1) ... (not a_n)} + * or_pos : {(not (or a_1 ... a_n)) a_1 ... a_n} + * implies_pos : {(not (implies a b)) (not a) b} + * xor_pos1 : {(not (xor a b)) a b} + * xor_neg1 : {(xor a b) a (not b)} + * equiv_pos1 : {(not (iff a b)) a (not b)} + * equiv_neg1 : {(iff a b) (not a) (not b)} + * ite_pos1 : {(not (if_then_else a b c)) a c} + * ite_neg1 : {(if_then_else a b c) a (not c)} + *) + | BuildDef2 of 'hform (* the first literal of the clause *) + (* * xor_pos2 : {(not (xor a b)) (not a) (not b)} + * xor_neg2 : {(xor a b) (not a) b} + * equiv_pos2 : {(not (iff a b)) (not a) b} + * equiv_neg2 : {(iff a b) a b} + * ite_pos2 : {(not (if_then_else a b c)) (not a) b} + * ite_neg2 : {(if_then_else a b c) (not a) (not b)} + + *) + | BuildProj of 'hform * int + (* * or_neg : {(or a_1 ... a_n) (not a_i)} + * and_pos : {(not (and a_1 ... a_n)) a_i} + * implies_neg1 : {(implies a b) a} + * implies_neg2 : {(implies a b) (not b)} + *) + + (* Immediate CNF transformation : CNF transformation + Reso *) + | ImmBuildDef of 'hform clause + (* * not_and : {(not (and a_1 ... a_n))} --> {(not a_1) ... (not a_n)} + * or : {(or a_1 ... a_n)} --> {a_1 ... a_n} + * implies : {(implies a b)} --> {(not a) b} + * xor1 : {(xor a b)} --> {a b} + * not_xor1 : {(not (xor a b))} --> {a (not b)} + * equiv2 : {(iff a b)} --> {a (not b)} + * not_equiv2 : {(not (iff a b))} --> {(not a) (not b)} + * ite1 : {(if_then_else a b c)} --> {a c} + * not_ite1 : {(not (if_then_else a b c))} --> {a (not c)} + *) + | ImmBuildDef2 of 'hform clause + (* * xor2 : {(xor a b)} --> {(not a) (not b)} + * not_xor2 : {(not (xor a b))} --> {(not a) b} + * equiv1 : {(iff a b)} --> {(not a) b} + * not_equiv1 : {(not (iff a b))} --> {a b} + * ite2 : {(if_then_else a b c)} --> {(not a) b} + * not_ite2 : {(not (if_then_else a b c))} --> {(not a) (not b)} + *) + | ImmBuildProj of 'hform clause * int + (* * and : {(and a_1 ... a_n)} --> {a_i} + * not_or : {(not (or a_1 ... a_n))} --> {(not a_i)} + * not_implies1 : {(not (implies a b))} --> {a} + * not_implies2 : {(not (implies a b))} --> {(not b)} + *) + + (* Equality *) + | EqTr of 'hform * 'hform list + (* * eq_reflexive : {(= x x)} + * eq_transitive : {(not (= x_1 x_2)) ... (not (= x_{n-1} x_n)) (= x_1 x_n)} + *) + | EqCgr of 'hform * ('hform option) list + (* * eq_congruent : {(not (= x_1 y_1)) ... (not (= x_n y_n)) + (= (f x_1 ... x_n) (f y_1 ... y_n))} + *) + | EqCgrP of 'hform * 'hform * ('hform option) list + (* * eq_congruent_pred : {(not (= x_1 y_1)) ... (not (= x_n y_n)) + (not (p x_1 ... x_n)) (p y_1 ... y_n)} + *) + + (* Linear arithmetic *) + | LiaMicromega of 'hform list * Certificate.Mc.zArithProof list + | LiaDiseq of 'hform + + (* Arithmetic simplifications *) + | SplArith of 'hform clause * 'hform * Certificate.Mc.zArithProof list + + (* Elimination of operators *) + | SplDistinctElim of 'hform clause * 'hform + +and 'hform clause = { + id : clause_id; + mutable kind : 'hform clause_kind; + mutable pos : int option; + mutable used : used; + mutable prev : 'hform clause option; + mutable next : 'hform clause option; + value : 'hform list option + (* This field should be defined for rules which can create atoms : + EqTr, EqCgr, EqCgrP, Lia, Dlde, Lra *) +} + +and 'hform clause_kind = + | Root + | Same of 'hform clause + | Res of 'hform resolution + | Other of 'hform rule + +and 'hform resolution = { + mutable rc1 : 'hform clause; + mutable rc2 : 'hform clause; + mutable rtail : 'hform clause list} + +let used_clauses r = + match r with + | ImmBuildProj (c, _) | ImmBuildDef c | ImmBuildDef2 c + | ImmFlatten (c,_) | SplArith (c,_,_) | SplDistinctElim (c,_) -> [c] + | True | False | BuildDef _ | BuildDef2 _ | BuildProj _ + | EqTr _ | EqCgr _ | EqCgrP _ + | LiaMicromega _ | LiaDiseq _ -> [] diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml new file mode 100644 index 0000000..d159db0 --- /dev/null +++ b/src/trace/smtCnf.ml @@ -0,0 +1,264 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +open SmtForm +open SmtCertif +open SmtTrace + +module MakeCnf (Form:FORM) = + struct + + type form_info = + | Immediate of bool (* true if the positive literal is set *) + | Done (* means that the equivalence clauses have been generated *) + | Todo (* nothing has been done, process the cnf transformation *) + + let info = Hashtbl.create 17 + + let init_last = + let last = SmtTrace.mk_scertif Root None in + SmtTrace.clear (); + last + + let last = ref init_last + + let cnf_todo = ref [] + + let clear () = + Hashtbl.clear info; + last := init_last; + cnf_todo := [] + + let push_cnf args = cnf_todo := args :: !cnf_todo + + let get_info l = + try Hashtbl.find info (Form.index l) + with Not_found -> Todo + + let set_done l = + Hashtbl.add info (Form.index l) Done + + let set_immediate l = + Hashtbl.add info (Form.index l) (Immediate (Form.is_pos l)) + + let test_immediate l = + match get_info l with + | Immediate b -> b = Form.is_pos l + | _ -> false + + let check_trivial cl = + List.exists test_immediate cl + + let link_Other other cl = + if not (check_trivial cl) then + let c = mkOther other (Some cl) in + link !last c; + last := c + + let both_lit l = if Form.is_pos l then Form.neg l,l else l, Form.neg l + + let or_of_imp args = + Array.mapi (fun i l -> + if i = Array.length args - 1 then l else Form.neg l) args + + let rec cnf l = + match get_info l with + | Immediate _ | Done -> () + | Todo -> + match Form.pform l with + | Fatom _ -> () + + | Fapp (op,args) -> + match op with + | Ftrue | Ffalse -> () + + | Fand -> + let nl,pl = both_lit l in + let nargs = Array.map Form.neg args in + link_Other (BuildDef pl) (pl::Array.to_list nargs); + Array.iteri (fun i l' -> + link_Other (BuildProj (nl,i)) [nl;l']) args; + set_done l; + Array.iter cnf args + + | For -> + let nl,pl = both_lit l in + link_Other (BuildDef nl) (nl::Array.to_list args); + Array.iteri (fun i l' -> + link_Other (BuildProj(pl,i)) [pl;Form.neg l']) args; + set_done l; + Array.iter cnf args + + | Fimp -> + let args = or_of_imp args in + let nl,pl = both_lit l in + link_Other (BuildDef nl) (nl::Array.to_list args); + Array.iteri (fun i l' -> + link_Other (BuildProj(pl,i)) [pl;Form.neg l']) args; + set_done l; + Array.iter cnf args + + | Fxor -> + let nl,pl = both_lit l in + let a, b = args.(0), args.(1) in + let na, nb = Form.neg a, Form.neg b in + link_Other (BuildDef nl) [nl;a;b]; + link_Other (BuildDef pl) [pl;a;nb]; + link_Other (BuildDef2 nl) [nl;na;nb]; + link_Other (BuildDef2 pl) [pl;na;b]; + set_done l; + cnf a; + cnf b + + | Fiff -> + let nl,pl = both_lit l in + let a, b = args.(0), args.(1) in + let na, nb = Form.neg a, Form.neg b in + link_Other (BuildDef nl) [nl;a;nb]; + link_Other (BuildDef pl) [pl;na;nb]; + link_Other (BuildDef2 nl) [pl;na;b]; + link_Other (BuildDef2 pl) [pl;a;b]; + set_done l; + cnf a; + cnf b + + | Fite -> + let nl,pl = both_lit l in + let a, b, c = args.(0), args.(1), args.(2) in + let na, nb, nc = Form.neg a, Form.neg b, Form.neg c in + link_Other (BuildDef nl) [nl;a;c]; + link_Other (BuildDef pl) [pl;a;nc]; + link_Other (BuildDef2 nl) [nl;na;b]; + link_Other (BuildDef2 pl) [pl;na;nb]; + set_done l; + cnf a; + cnf b; + cnf c + + | Fnot2 _ -> cnf args.(0) + + exception Cnf_done + + let rec imm_link_Other other l = + if not (test_immediate l) then + let c = mkOther other (Some [l]) in + link !last c; + last := c; + imm_cnf c + + and imm_cnf c = + let l = + match c.value with + | Some [l] -> + begin match Form.pform l with + | Fapp (Fnot2 _, args) -> + let l' = args.(0) in + if Form.is_pos l then l' + else Form.neg l' + | _ -> l + end + | _ -> assert false in + match get_info l with + | Immediate b -> if b = Form.is_neg l then raise Cnf_done + | Done -> assert false + | Todo -> + set_immediate l; + + match Form.pform l with + | Fatom _ -> () + + | Fapp (op,args) -> + match op with + | Ftrue | Ffalse -> () + + | Fand -> + if Form.is_pos l then + Array.iteri (fun i l' -> + imm_link_Other (ImmBuildProj(c,i)) l') args + else begin + let nargs = Array.map Form.neg args in + link_Other (ImmBuildDef c) (Array.to_list nargs); + push_cnf args + end + + | For -> + if Form.is_pos l then begin + link_Other (ImmBuildDef c) (Array.to_list args); + push_cnf args + end else + Array.iteri (fun i l' -> + imm_link_Other (ImmBuildProj(c,i)) (Form.neg l')) args + + | Fimp -> + let args = or_of_imp args in + if Form.is_pos l then begin + link_Other (ImmBuildDef c) (Array.to_list args); + push_cnf args + end else + Array.iteri (fun i l' -> + imm_link_Other (ImmBuildProj(c,i)) (Form.neg l')) args + + | Fxor -> + let args1 = + if Form.is_pos l then [args.(0);args.(1)] + else [args.(0);Form.neg args.(1)] in + let args2 = + if Form.is_pos l then [Form.neg args.(0);Form.neg args.(1)] + else [Form.neg args.(0); args.(1)] in + link_Other (ImmBuildDef c) args1; + link_Other (ImmBuildDef2 c) args2; + push_cnf args + + | Fiff -> + let args1 = + if Form.is_pos l then [args.(0);Form.neg args.(1)] + else [Form.neg args.(0);Form.neg args.(1)] in + let args2 = + if Form.is_pos l then [Form.neg args.(0);args.(1)] + else [args.(0); args.(1)] in + link_Other (ImmBuildDef c) args1; + link_Other (ImmBuildDef2 c) args2; + push_cnf args + + | Fite -> + let args1 = + if Form.is_pos l then [args.(0);Form.neg args.(2)] + else [args.(0);Form.neg args.(2)] in + let args2 = + if Form.is_pos l then [Form.neg args.(0);args.(1)] + else [Form.neg args.(0); Form.neg args.(1)] in + link_Other (ImmBuildDef c) args1; + link_Other (ImmBuildDef2 c) args2; + push_cnf args + + | Fnot2 _ -> assert false + + let make_cnf reify c = + let ftrue = Form.get reify (Fapp(Ftrue, [||])) in + let ffalse = Form.get reify (Fapp(Ffalse, [||])) in + last := c; + link_Other True [ftrue]; + link_Other False [Form.neg ffalse]; + (try + imm_cnf c; + List.iter (Array.iter cnf) !cnf_todo + with Cnf_done -> ()); + let res = !last in + clear (); + res + + end + diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml new file mode 100644 index 0000000..6075b3f --- /dev/null +++ b/src/trace/smtForm.ml @@ -0,0 +1,510 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) +open Util +open SmtMisc +open CoqTerms +open Errors + +module type ATOM = + sig + + type t + val index : t -> int + + val equal : t -> t -> bool + + val is_bool_type : t -> bool + + end + + +type fop = + | Ftrue + | Ffalse + | Fand + | For + | Fxor + | Fimp + | Fiff + | Fite + | Fnot2 of int + +type ('a,'f) gen_pform = + | Fatom of 'a + | Fapp of fop * 'f array + + +module type FORM = + sig + type hatom + type t + type pform = (hatom, t) gen_pform + + val pform_true : pform + val pform_false : pform + + val equal : t -> t -> bool + + val to_lit : t -> int + val index : t -> int + val pform : t -> pform + + val neg : t -> t + val is_pos : t -> bool + val is_neg : t -> bool + + val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit + + (* Building formula from positive formula *) + exception NotWellTyped of pform + type reify + val create : unit -> reify + val clear : reify -> unit + val get : reify -> pform -> t + + (** Give a coq term, build the corresponding formula *) + val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t + + (** Flattening of [Fand] and [For], removing of [Fnot2] *) + val flatten : reify -> t -> t + + (** Producing Coq terms *) + + val to_coq : t -> Term.constr + + val pform_tbl : reify -> pform array + + val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array + val interp_tbl : reify -> Term.constr * Term.constr + val nvars : reify -> int + (** Producing a Coq term corresponding to the interpretation + of a formula *) + (** [interp_atom] map [hatom] to coq term, it is better if it produce + shared terms. *) + val interp_to_coq : + (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> + t -> Term.constr + end + +module Make (Atom:ATOM) = + struct + + type hatom = Atom.t + + type pform = (Atom.t, t) gen_pform + + and hpform = pform gen_hashed + + and t = + | Pos of hpform + | Neg of hpform + + let pform_true = Fapp (Ftrue,[||]) + let pform_false = Fapp (Ffalse,[||]) + + let equal h1 h2 = + match h1, h2 with + | Pos hp1, Pos hp2 -> hp1.index == hp2.index + | Neg hp1, Neg hp2 -> hp1.index == hp2.index + | _, _ -> false + + let index = function + | Pos hp -> hp.index + | Neg hp -> hp.index + + let to_lit = function + | Pos hp -> hp.index * 2 + | Neg hp -> hp.index * 2 + 1 + + let neg = function + | Pos hp -> Neg hp + | Neg hp -> Pos hp + + let is_pos = function + | Pos _ -> true + | _ -> false + + let is_neg = function + | Neg _ -> true + | _ -> false + + let pform = function + | Pos hp -> hp.hval + | Neg hp -> hp.hval + + + let rec to_smt atom_to_smt fmt = function + | Pos hp -> to_smt_pform atom_to_smt fmt hp.hval + | Neg hp -> + Format.fprintf fmt "(not "; + to_smt_pform atom_to_smt fmt hp.hval; + Format.fprintf fmt ")" + + and to_smt_pform atom_to_smt fmt = function + | Fatom a -> atom_to_smt fmt a + | Fapp (op,args) -> to_smt_op atom_to_smt fmt op args + + and to_smt_op atom_to_smt fmt op args = + let s = match op with + | Ftrue -> "true" + | Ffalse -> "false" + | Fand -> "and" + | For -> "or" + | Fxor -> "xor" + | Fimp -> "=>" + | Fiff -> "=" + | Fite -> "ite" + | Fnot2 _ -> "" in + let (s1,s2) = if Array.length args = 0 then ("","") else ("(",")") in + Format.fprintf fmt "%s%s" s1 s; + Array.iter (fun h -> Format.fprintf fmt " "; to_smt atom_to_smt fmt h) args; + Format.fprintf fmt "%s" s2 + + + module HashedForm = + struct + + type t = pform + + let equal pf1 pf2 = + match pf1, pf2 with + | Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2 + | Fapp(op1,args1), Fapp(op2,args2) -> + op1 = op2 && + Array.length args1 == Array.length args2 && + (try + for i = 0 to Array.length args1 - 1 do + if not (equal args1.(i) args2.(i)) then raise Not_found + done; + true + with Not_found -> false) + | _, _ -> false + + let hash pf = + match pf with + | Fatom ha1 -> Atom.index ha1 * 2 + | Fapp(op, args) -> + let hash_args = + match Array.length args with + | 0 -> 0 + | 1 -> to_lit args.(0) + | 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0) + | _ -> + (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 + + to_lit args.(0) in + (hash_args * 10 + Hashtbl.hash op) * 2 + 1 + + end + + module HashForm = Hashtbl.Make (HashedForm) + + type reify = { + mutable count : int; + tbl : t HashForm.t + } + + exception NotWellTyped of pform + + let check pf = + match pf with + | Fatom ha -> if not (Atom.is_bool_type ha) then raise (NotWellTyped pf) + | Fapp (op, args) -> + match op with + | Ftrue | Ffalse -> + if Array.length args <> 0 then raise (NotWellTyped pf) + | Fnot2 _ -> + if Array.length args <> 1 then raise (NotWellTyped pf) + | Fand | For -> () + | Fxor | Fimp | Fiff -> + if Array.length args <> 2 then raise (NotWellTyped pf) + | Fite -> + if Array.length args <> 3 then raise (NotWellTyped pf) + + let declare reify pf = + check pf; + let res = Pos {index = reify.count; hval = pf} in + HashForm.add reify.tbl pf res; + reify.count <- reify.count + 1; + res + + let create () = + let reify = + { count = 0; + tbl = HashForm.create 17 } in + let _ = declare reify pform_true in + let _ = declare reify pform_false in + reify + + let clear r = + r.count <- 0; + HashForm.clear r.tbl; + let _ = declare r pform_true in + let _ = declare r pform_false in + () + + let get reify pf = + try HashForm.find reify.tbl pf + with Not_found -> declare reify pf + + + (** Given a coq term, build the corresponding formula *) + type coq_cst = + | CCtrue + | CCfalse + | CCnot + | CCand + | CCor + | CCxor + | CCimp + | CCiff + | CCifb + | CCunknown + + let op_tbl () = + let tbl = Hashtbl.create 29 in + let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in + List.iter add + [ + ctrue,CCtrue; cfalse,CCfalse; + candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot; + ceqb,CCiff; cifb,CCifb ]; + tbl + + let op_tbl = lazy (op_tbl ()) + + let empty_args = [||] + + let of_coq atom_of_coq reify c = + let op_tbl = Lazy.force op_tbl in + let get_cst c = + try Hashtbl.find op_tbl c with Not_found -> CCunknown in + let rec mk_hform h = + let c, args = Term.decompose_app h in + match get_cst c with + | CCtrue -> get reify (Fapp(Ftrue,empty_args)) + | CCfalse -> get reify (Fapp(Ffalse,empty_args)) + | CCnot -> mk_fnot 1 args + | CCand -> mk_fand [] args + | CCor -> mk_for [] args + | CCxor -> op2 (fun l -> Fapp(Fxor,l)) args + | CCiff -> op2 (fun l -> Fapp(Fiff,l)) args + | CCimp -> + (match args with + | [b1;b2] -> + let l1 = mk_hform b1 in + let l2 = mk_hform b2 in + get reify (Fapp (Fimp, [|l1;l2|])) + | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for implb") + | CCifb -> + (* We should also be able to syntaxify if then else *) + begin match args with + | [b1;b2;b3] -> + let l1 = mk_hform b1 in + let l2 = mk_hform b2 in + let l3 = mk_hform b3 in + get reify (Fapp(Fite, [|l1;l2;l3|])) + | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for ifb" + end + | _ -> + let a = atom_of_coq h in + get reify (Fatom a) + + and op2 f args = + match args with + | [b1;b2] -> + let l1 = mk_hform b1 in + let l2 = mk_hform b2 in + get reify (f [|l1; l2|]) + | _ -> error "SmtForm.Form.of_coq: wrong number of arguments" + + and mk_fnot i args = + match args with + | [t] -> + let c,args = Term.decompose_app t in + if c = Lazy.force cnegb then + mk_fnot (i+1) args + else + let q,r = i lsr 1 , i land 1 in + let l = mk_hform t in + let l = if r = 0 then l else neg l in + if q = 0 then l + else get reify (Fapp(Fnot2 q, [|l|])) + | _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for negb" + + and mk_fand acc args = + match args with + | [t1;t2] -> + let l2 = mk_hform t2 in + let c, args = Term.decompose_app t1 in + if c = Lazy.force candb then + mk_fand (l2::acc) args + else + let l1 = mk_hform t1 in + get reify (Fapp(Fand, Array.of_list (l1::l2::acc))) + | _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for andb" + + and mk_for acc args = + match args with + | [t1;t2] -> + let l2 = mk_hform t2 in + let c, args = Term.decompose_app t1 in + if c = Lazy.force corb then + mk_for (l2::acc) args + else + let l1 = mk_hform t1 in + get reify (Fapp(For, Array.of_list (l1::l2::acc))) + | _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in + + let l = mk_hform c in + l + + (** Flattening of Fand and For, removing of Fnot2 *) + let set_sign f f' = + if is_pos f then f' else neg f' + + let rec flatten reify f = + match pform f with + | Fatom _ -> f + | Fapp(Fnot2 _,args) -> set_sign f (flatten reify args.(0)) + | Fapp(Fand, args) -> set_sign f (flatten_and reify [] (Array.to_list args)) + | Fapp(For,args) -> set_sign f (flatten_or reify [] (Array.to_list args)) + | Fapp(op,args) -> + (* TODO change Fimp into For ? *) + set_sign f (get reify (Fapp(op, Array.map (flatten reify) args))) + + and flatten_and reify acc args = + match args with + | [] -> get reify (Fapp(Fand, Array.of_list (List.rev acc))) + | a::args -> + (* TODO change (not For) and (not Fimp) into Fand *) + match pform a with + | Fapp(Fand, args') when is_pos a -> + let args = Array.fold_right (fun a args -> a::args) args' args in + flatten_and reify acc args + | _ -> flatten_and reify (flatten reify a :: acc) args + + and flatten_or reify acc args = + (* TODO change Fimp and (not Fand) into For *) + match args with + | [] -> get reify (Fapp(For, Array.of_list (List.rev acc))) + | a::args -> + match pform a with + | Fapp(For, args') when is_pos a -> + let args = Array.fold_right (fun a args -> a::args) args' args in + flatten_or reify acc args + | _ -> flatten_or reify (flatten reify a :: acc) args + + (** Producing Coq terms *) + + let to_coq hf = mkInt (to_lit hf) + + let args_to_coq args = + let cargs = Array.make (Array.length args + 1) (mkInt 0) in + Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args; + Term.mkArray (Lazy.force cint, cargs) + + let pf_to_coq = function + | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|] + | Fapp(op,args) -> + match op with + | Ftrue -> Lazy.force cFtrue + | Ffalse -> Lazy.force cFfalse + | Fand -> mklApp cFand [| args_to_coq args|] + | For -> mklApp cFor [| args_to_coq args|] + | Fimp -> mklApp cFimp [| args_to_coq args|] + | Fxor -> mklApp cFxor (Array.map to_coq args) + | Fiff -> mklApp cFiff (Array.map to_coq args) + | Fite -> mklApp cFite (Array.map to_coq args) + | Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|] + + let pform_tbl reify = + let t = Array.make reify.count pform_true in + let set _ h = + match h with + | Pos hp -> t.(hp.index) <- hp.hval + | _ -> assert false in + HashForm.iter set reify.tbl; + t + + let to_array reify dft f = + let t = Array.make (reify.count + 1) dft in + let set _ h = + match h with + | Pos hp -> t.(hp.index) <- f hp.hval + | _ -> assert false in + HashForm.iter set reify.tbl; + (reify.count, t) + + let interp_tbl reify = + let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in + (mkInt i, Term.mkArray (Lazy.force cform, t)) + + let nvars reify = reify.count + (** Producing a Coq term corresponding to the interpretation of a formula *) + (** [interp_atom] map [Atom.t] to coq term, it is better if it produce + shared terms. *) + let interp_to_coq interp_atom form_tbl f = + let rec interp_form f = + let l = to_lit f in + try Hashtbl.find form_tbl l + with Not_found -> + if is_neg f then + let pc = interp_form (neg f) in + let nc = mklApp cnegb [|pc|] in + Hashtbl.add form_tbl l nc; + nc + else + let pc = + match pform f with + | Fatom a -> interp_atom a + | Fapp(op, args) -> + match op with + | Ftrue -> Lazy.force ctrue + | Ffalse -> Lazy.force cfalse + | Fand -> interp_args candb args + | For -> interp_args corb args + | Fxor -> interp_args cxorb args + | Fimp -> + let r = ref (interp_form args.(Array.length args - 1)) in + for i = Array.length args - 2 downto 0 do + r := mklApp cimplb [|interp_form args.(i); !r|] + done; + !r + | Fiff -> interp_args ceqb args + | Fite -> + (* TODO with if here *) + mklApp cifb (Array.map interp_form args) + | Fnot2 n -> + let r = ref (interp_form args.(0)) in + for i = 1 to n do r := mklApp cnegb [|!r|] done; + !r in + Hashtbl.add form_tbl l pc; + pc + and interp_args op args = + let r = ref (interp_form args.(0)) in + for i = 1 to Array.length args - 1 do + r := mklApp op [|!r;interp_form args.(i)|] + done; + !r in + interp_form f + + end + + + + + + + diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli new file mode 100644 index 0000000..118ecf5 --- /dev/null +++ b/src/trace/smtForm.mli @@ -0,0 +1,99 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +module type ATOM = + sig + + type t + val index : t -> int + + val equal : t -> t -> bool + + val is_bool_type : t -> bool + + end + + +type fop = + | Ftrue + | Ffalse + | Fand + | For + | Fxor + | Fimp + | Fiff + | Fite + | Fnot2 of int + + +type ('a,'f) gen_pform = + | Fatom of 'a + | Fapp of fop * 'f array + +module type FORM = + sig + type hatom + type t + type pform = (hatom, t) gen_pform + + val pform_true : pform + val pform_false : pform + + val equal : t -> t -> bool + + val to_lit : t -> int + val index : t -> int + val pform : t -> pform + + val neg : t -> t + val is_pos : t -> bool + val is_neg : t -> bool + + val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit + + (* Building formula from positive formula *) + exception NotWellTyped of pform + type reify + val create : unit -> reify + val clear : reify -> unit + val get : reify -> pform -> t + + (** Given a coq term, build the corresponding formula *) + val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t + + (** Flattening of [Fand] and [For], removing of [Fnot2] *) + val flatten : reify -> t -> t + + (** Producing Coq terms *) + + val to_coq : t -> Term.constr + + val pform_tbl : reify -> pform array + + val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array + val interp_tbl : reify -> Term.constr * Term.constr + val nvars : reify -> int + (** Producing a Coq term corresponding to the interpretation + of a formula *) + (** [interp_atom] map [hatom] to coq term, it is better if it produce + shared terms. *) + val interp_to_coq : + (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> + t -> Term.constr + end + +module Make (Atom:ATOM) : FORM with type hatom = Atom.t + + diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml new file mode 100644 index 0000000..02e5f26 --- /dev/null +++ b/src/trace/smtMisc.ml @@ -0,0 +1,47 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +(** Sharing of coq Int *) +let cInt_tbl = Hashtbl.create 17 + +let mkInt i = + try Hashtbl.find cInt_tbl i + with Not_found -> + let ci = Term.mkInt (Uint63.of_int i) in + Hashtbl.add cInt_tbl i ci; + ci + +(** Generic representation of shared object *) +type 'a gen_hashed = { index : int; hval : 'a } + +(** Functions over constr *) + +let mklApp f args = Term.mkApp (Lazy.force f, args) + +(* TODO : Set -> Type *) +let coqtype = lazy Term.mkSet + +let declare_new_type t = + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (Pp.dummy_loc,t); + Term.mkVar t + +let declare_new_variable v constr_t = + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Pp.dummy_loc,v); + Term.mkVar v + +let mkName s = + let id = Names.id_of_string s in + Names.Name id diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml new file mode 100644 index 0000000..8420ca1 --- /dev/null +++ b/src/trace/smtTrace.ml @@ -0,0 +1,465 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) +open SmtMisc +open CoqTerms +open SmtCertif + +let notUsed = 0 + +let next_id = ref 0 + +let clear () = next_id := 0 + +let next_id () = + let id = !next_id in + incr next_id; + id + +(** Basic functions over small certificates *) + +let mk_scertif kind ov = + { + id = next_id (); + kind = kind; + pos = None; + used = notUsed; + prev = None; + next = None; + value = ov + } + +(** Roots *) + + +let mkRootGen ov = + let pos = next_id () in + { + id = pos; + kind = Root; + pos = Some pos; + used = notUsed; + prev = None; + next = None; + value = ov + } + +(* let mkRoot = mkRootGen None *) +let mkRootV v = mkRootGen (Some v) + +let isRoot k = k == Root + +(** Resolutions *) + +let mkRes c1 c2 tl = + mk_scertif (Res { rc1 = c1; rc2 = c2; rtail = tl }) None + +let isRes k = + match k with + | Res _ -> true + | _ -> false + + +(** Other *) + +let mkOther r ov = mk_scertif (Other r) ov + + +(** Moving into the trace *) +let next c = + match c.next with + | Some c1 -> c1 + | None -> assert false + +let has_prev c = + match c.prev with + | Some _ -> true + | None -> false + +let prev c = + match c.prev with + | Some c1 -> c1 + | None -> Printf.printf "prev %i\n" c.id;flush stdout;assert false + +let link c1 c2 = + c1.next <- Some c2; + c2.prev <- Some c1 + +let clear_links c = + c.prev <- None; + c.next <- None + +let skip c = + link (prev c) (next c); + clear_links c + +let insert_before c cprev = + link (prev c) cprev; + link cprev c + +let get_res c s = + match c.kind with + | Res res -> res + | _ -> Printf.printf "get_res %s\n" s; assert false + +let get_other c s = + match c.kind with + | Other res -> res + | _ -> Printf.printf "get_other %s\n" s; assert false + +let get_val c = + match c.value with + | None -> assert false + | Some cl -> cl + +let rec repr c = + match c.kind with + | Root | Res _ | Other _ -> c + | Same c -> repr c + +let set_same c nc = + c.kind <- Same (repr nc); + skip c + +let rec get_pos c = + match c.kind with + | Root | Res _ | Other _ -> + begin match c.pos with + | Some n -> n + | _ -> assert false + end + | Same c -> get_pos c + +let eq_clause c1 c2 = (repr c1).id = (repr c2).id + +(* Selection of useful rules *) +let select c = + let mark c = + if not (isRoot c.kind) then c.used <- 1 in + mark c; + let r = ref c in + while not (isRoot !r.kind) do + let p = prev !r in + (match !r.kind with + | Res res -> + if !r.used == 1 then begin + !r.used <- notUsed; + (* let res = get_res !r "select" in *) + mark res.rc1; mark res.rc2; + List.iter mark res.rtail + end else + skip !r; + | Same _ -> + skip !r + | _ -> + if !r.used == 1 then + begin + !r.used <- notUsed; + let rl = get_other !r "select" in + List.iter mark (used_clauses rl) + end + else skip !r; + ); + r := p + done + + + + +(* Compute the number of occurence of each_clause *) + +let rec occur c = + match c.kind with + | Root -> c.used <- c.used + 1 + | Res res -> + if c.used == notUsed then + begin occur res.rc1; occur res.rc2; List.iter occur res.rtail end; + c.used <- c.used + 1 + | Other res -> + if c.used == notUsed then List.iter occur (used_clauses res); + c.used <- c.used + 1; + | Same c' -> + occur c'; + c.used <- c.used + 1 + +(* Allocate clause *) + +let alloc c = + let free_pos = ref [] in + + (* free the unused roots *) + + let r = ref c in + while isRoot !r.kind do + if !r.used == notUsed then begin + free_pos := get_pos !r :: !free_pos; + end; + r := next !r; + done; + + (* r is the first clause defined by resolution or another rule, + normaly the first used *) + let last_set = ref (get_pos (prev !r)) in + + let decr_clause c = + let rc = repr c in + assert (rc.used > notUsed); + rc.used <- rc.used - 1; + if rc.used = notUsed then + free_pos := get_pos rc :: !free_pos in + + let decr_res res = + decr_clause res.rc1; + decr_clause res.rc2; + List.iter decr_clause res.rtail in + + let decr_other o = + List.iter decr_clause (used_clauses o) in + + while !r.next <> None do + let n = next !r in + assert (!r.used <> notUsed); + if isRes !r.kind then + decr_res (get_res !r "alloc") + else + decr_other (get_other !r "alloc"); + begin match !free_pos with + | p::free -> free_pos := free; !r.pos <- Some p + | _ -> incr last_set; !r.pos <- Some !last_set + end; + r := n + done; + begin match !free_pos with + | p::free -> free_pos := free; !r.pos <- Some p + | _ -> incr last_set; !r.pos <- Some !last_set + end; + !last_set + + +(* A naive allocation for debugging *) + +let naive_alloc c = + let r = ref c in + while isRoot !r.kind do + r := next !r + done; + let last_set = ref (get_pos (prev !r)) in + while !r.next <> None do + let n = next !r in + incr last_set; !r.pos <- Some !last_set; + r := n + done; + incr last_set; !r.pos <- Some !last_set; + !last_set + + +(* This function is currently inlined in verit/verit.ml and zchaff/zchaff.ml *) + +let build_certif first_root confl = + select confl; + occur confl; + alloc first_root + + +let to_coq to_lit (cstep, + cRes, cImmFlatten, + cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj, + cImmBuildProj,cImmBuildDef,cImmBuildDef2, + cEqTr, cEqCgr, cEqCgrP, + cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim) confl = + let out_f f = to_lit f in + let out_c c = mkInt (get_pos c) in + let step_to_coq c = + match c.kind with + | Res res -> + let size = List.length res.rtail + 3 in + let args = Array.make size (mkInt 0) in + args.(0) <- mkInt (get_pos res.rc1); + args.(1) <- mkInt (get_pos res.rc2); + let l = ref res.rtail in + for i = 2 to size - 2 do + match !l with + | c::tl -> + args.(i) <- mkInt (get_pos c); + l := tl + | _ -> assert false + done; + mklApp cRes [|mkInt (get_pos c); Term.mkArray (Lazy.force cint, args)|] + | Other other -> + begin match other with + | ImmFlatten (c',f) -> mklApp cImmFlatten [|out_c c;out_c c'; out_f f|] + | True -> mklApp cTrue [|out_c c|] + | False -> mklApp cFalse [|out_c c|] + | BuildDef f -> mklApp cBuildDef [|out_c c; out_f f|] + | BuildDef2 f -> mklApp cBuildDef2 [|out_c c;out_f f|] + | BuildProj (f, i) -> mklApp cBuildProj [|out_c c; out_f f;mkInt i|] + | ImmBuildDef c' -> mklApp cImmBuildDef [|out_c c; out_c c'|] + | ImmBuildDef2 c' -> mklApp cImmBuildDef2 [|out_c c;out_c c'|] + | ImmBuildProj(c', i) -> mklApp cImmBuildProj [|out_c c; out_c c';mkInt i|] + | EqTr (f, fl) -> + let res = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) fl (mklApp cnil [|Lazy.force cint|]) in + mklApp cEqTr [|out_c c; out_f f; res|] + | EqCgr (f, fl) -> + let res = List.fold_right (fun f l -> mklApp ccons [|mklApp coption [|Lazy.force cint|]; (match f with | Some f -> mklApp cSome [|Lazy.force cint; out_f f|] | None -> mklApp cNone [|Lazy.force cint|]); l|]) fl (mklApp cnil [|mklApp coption [|Lazy.force cint|]|]) in + mklApp cEqCgr [|out_c c; out_f f; res|] + | EqCgrP (f1, f2, fl) -> + let res = List.fold_right (fun f l -> mklApp ccons [|mklApp coption [|Lazy.force cint|]; (match f with | Some f -> mklApp cSome [|Lazy.force cint; out_f f|] | None -> mklApp cNone [|Lazy.force cint|]); l|]) fl (mklApp cnil [|mklApp coption [|Lazy.force cint|]|]) in + mklApp cEqCgrP [|out_c c; out_f f1; out_f f2; res|] + | LiaMicromega (cl,d) -> + let cl' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in + let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in + mklApp cLiaMicromega [|out_c c; cl'; c'|] + | LiaDiseq l -> mklApp cLiaDiseq [|out_c c; out_f l|] + | SplArith (orig,res,l) -> + let res' = out_f res in + let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in + mklApp cSplArith [|out_c c; out_c orig; res'; l'|] + | SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|] + end + | _ -> assert false in + let step = Lazy.force cstep in + let def_step = + mklApp cRes [|mkInt 0; Term.mkArray (Lazy.force cint, [|mkInt 0|]) |] in + let r = ref confl in + let nc = ref 0 in + while not (isRoot !r.kind) do r := prev !r; incr nc done; + let last_root = !r in + let size = !nc in + let max = (Parray.trunc_size (Uint63.of_int 4194303)) - 1 in + let q,r1 = size / max, size mod max in + + let trace = + let len = if r1 = 0 then q + 1 else q + 2 in + Array.make len (Term.mkArray (step, [|def_step|])) in + for j = 0 to q - 1 do + let tracej = Array.make (Parray.trunc_size (Uint63.of_int 4194303)) def_step in + for i = 0 to max - 1 do + r := next !r; + tracej.(i) <- step_to_coq !r; + done; + trace.(j) <- Term.mkArray (step, tracej) + done; + if r1 <> 0 then begin + let traceq = Array.make (r1 + 1) def_step in + for i = 0 to r1-1 do + r := next !r; + traceq.(i) <- step_to_coq !r; + done; + trace.(q) <- Term.mkArray (step, traceq) + end; + + (Term.mkArray (mklApp carray [|step|], trace), last_root) + + + +(** Optimization of the trace *) + +module MakeOpt (Form:SmtForm.FORM) = + struct + (* Share the certificate building a common clause *) + let share_value c = + let tbl = Hashtbl.create 17 in + let to_lits v = List.map (Form.to_lit) v in + let process c = + match c.value with + | None -> () + | Some v -> + let lits = to_lits v in + try + let c' = Hashtbl.find tbl lits in + set_same c c' + with Not_found -> Hashtbl.add tbl lits c in + let r = ref c in + while !r.next <> None do + let next = next !r in + process !r; + r := next + done; + process !r + + (* Sharing of the common prefix *) + + module HashedHeadRes = + struct + + type t = Form.t resolution + + let equal r1 r2 = + eq_clause r1.rc1 r2.rc1 && eq_clause r1.rc2 r2.rc2 + + let hash r = (repr r.rc1).id * 19 + (repr r.rc2).id + + end + + module HRtbl = Hashtbl.Make (HashedHeadRes) + + let common_head tl1 tl2 = + let rec aux rhd tl1 tl2 = + match tl1, tl2 with + | [], _ -> List.rev rhd, tl1, tl2 + | _, [] -> List.rev rhd, tl1, tl2 + | c1::tl1', c2::tl2' -> + if eq_clause c1 c2 then aux (repr c1 :: rhd) tl1' tl2' + else List.rev rhd, tl1, tl2 + in aux [] tl1 tl2 + + let share_prefix first_c n = + let tbl = HRtbl.create (min n Sys.max_array_length) in + let rec share c2 = + if isRes c2.kind then ( + let res2 = get_res c2 "share_prefix1" in + try + let c1 = HRtbl.find tbl res2 in + let res1 = get_res c1 "share_prefix2" in + (* res1 and res2 have the same head *) + let head, tl1, tl2 = common_head res1.rtail res2.rtail in + match tl1, tl2 with + | [], [] -> + set_same c2 c1; + | [], c2'::tl2' -> + res2.rc1 <- c1; + res2.rc2 <- c2'; + res2.rtail <- tl2'; + share c2 + | c1'::tl1', [] -> + skip c2; + HRtbl.remove tbl res1; + insert_before c1 c2; + res1.rc1 <- c2; + res1.rc2 <- c1'; + res1.rtail <- tl1'; + share c1 + | c1'::tl1', c2'::tl2' -> + let c = mkRes res1.rc1 res1.rc2 head in + HRtbl.remove tbl res1; + insert_before c1 c; + res1.rc1 <- c; + res1.rc2 <- c1'; + res1.rtail <- tl1'; + res2.rc1 <- c; + res2.rc2 <- c2'; + res2.rtail <- tl2'; + share c; + share c1; + share c2 + with Not_found -> HRtbl.add tbl res2 c2 + ) in + let r = ref first_c in + while !r.next <> None do + let n = next !r in + share !r; + r := n + done + + end diff --git a/src/trace/smt_tactic.ml4 b/src/trace/smt_tactic.ml4 new file mode 100644 index 0000000..219810d --- /dev/null +++ b/src/trace/smt_tactic.ml4 @@ -0,0 +1,55 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +VERNAC COMMAND EXTEND Parse_certif_zchaff +| [ "Parse_certif_zchaff" + ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] -> + [ + Zchaff.parse_certif dimacs trace fdimacs fproof + ] +| [ "Zchaff_Checker" string(fdimacs) string(fproof) ] -> + [ + Zchaff.checker fdimacs fproof + ] +| [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] -> + [ + Zchaff.theorem name fdimacs fproof + ] +END + +VERNAC COMMAND EXTEND Parse_certif_verit +| [ "Parse_certif_verit" + ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] -> + [ + Verit.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof + ] +| [ "Verit_Checker" string(fsmt) string(fproof) ] -> + [ + Verit.checker fsmt fproof + ] +| [ "Verit_Theorem" ident(name) string(fsmt) string(fproof) ] -> + [ + Verit.theorem name fsmt fproof + ] +END + +TACTIC EXTEND zchaff +| [ "zchaff" ] -> [ Zchaff.tactic ] +END + +TACTIC EXTEND verit +| [ "verit" ] -> [ Verit.tactic ] +END -- cgit