From e2683e1e653a1b6872a886f4b99218e2803f7a74 Mon Sep 17 00:00:00 2001 From: vblot <24938579+vblot@users.noreply.github.com> Date: Wed, 7 Jul 2021 08:55:25 +0200 Subject: use native integers (#96) --- src/trace/coqInterface.ml | 26 ++++++-------------------- src/trace/coqInterface.mli | 2 +- src/trace/coqTerms.ml | 2 +- src/trace/smtBtype.ml | 2 +- 4 files changed, 9 insertions(+), 23 deletions(-) (limited to 'src/trace') diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml index 36f4337..b462881 100644 --- a/src/trace/coqInterface.ml +++ b/src/trace/coqInterface.ml @@ -112,26 +112,12 @@ let init_modules = Coqlib.init_modules (* Int63 *) -let int63_modules = [["SMTCoq";"Int63";"Int63Native"]] - -(* 31-bits integers are "called" 63 bits (this is sound) *) -let int31_module = [["Coq";"Numbers";"Cyclic";"Int31";"Int31"]] -let cD0 = gen_constant int31_module "D0" -let cD1 = gen_constant int31_module "D1" -let cI31 = gen_constant int31_module "I31" - -let mkInt : int -> constr = fun i -> - let a = Array.make 31 (Lazy.force cD0) in - let j = ref i in - let k = ref 30 in - while !j <> 0 do - if !j land 1 = 1 then a.(!k) <- Lazy.force cD1; - j := !j lsr 1; - decr k - done; - mkApp (Lazy.force cI31, a) - -let cint = gen_constant int31_module "int31" +let int63_module = [["Coq";"Numbers";"Cyclic";"Int63";"Int63"]] + +let mkInt : int -> Constr.constr = + fun i -> Constr.mkInt (Uint63.of_int i) + +let cint = gen_constant int63_module "int" (* PArray *) diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli index 104f3f9..38d78d8 100644 --- a/src/trace/coqInterface.mli +++ b/src/trace/coqInterface.mli @@ -65,7 +65,7 @@ val init_modules : string list list (* Int63 *) -val int63_modules : string list list +val int63_module : string list list val mkInt : int -> constr val cint : constr lazy_t diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 1c4ee81..67392bb 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -18,7 +18,7 @@ let gen_constant = CoqInterface.gen_constant (* Int63 *) let cint = CoqInterface.cint -let ceq63 = gen_constant CoqInterface.int63_modules "eqb" +let ceq63 = gen_constant CoqInterface.int63_module "eqb" (* PArray *) let carray = gen_constant CoqInterface.parray_modules "array" diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index c9aad70..d091758 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -51,7 +51,7 @@ let index_tbl = Hashtbl.create 17 let index_to_coq i = try Hashtbl.find index_tbl i with Not_found -> - let interp = mklApp cTindex [|mkInt i|] in + let interp = mklApp cTindex [|mkN i|] in Hashtbl.add index_tbl i interp; interp -- cgit From a8863500307f01b9df6d13b19db61066d219c553 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Mon, 30 Aug 2021 16:35:40 +0200 Subject: Rename directory because MacOS FS is case-insensitive --- src/trace/coqInterface.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/trace') diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml index b462881..81a22c9 100644 --- a/src/trace/coqInterface.ml +++ b/src/trace/coqInterface.ml @@ -121,7 +121,7 @@ let cint = gen_constant int63_module "int" (* PArray *) -let parray_modules = [["SMTCoq";"Array";"PArray"]] +let parray_modules = [["SMTCoq";"PArray";"PArray"]] let cmake = gen_constant parray_modules "make" let cset = gen_constant parray_modules "set" -- cgit From ad5ddae0406770990bc43bc10cc753470c7e27af Mon Sep 17 00:00:00 2001 From: vblot <24938579+vblot@users.noreply.github.com> Date: Wed, 8 Sep 2021 11:25:50 +0200 Subject: generalize polymorphic arguments detection --- src/trace/smtAtom.ml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'src/trace') diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 2710eb2..1d608e6 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -1343,15 +1343,18 @@ module Atom = let rec collect_types = function | [] -> ([],[]) | x::xs as l -> - let ty = Structures.retyping_get_type_of env sigma x in - if Constr.iskind ty || - let c, _ = Structures.decompose_app ty in - Structures.eq_constr c (Lazy.force cCompDec) - then - let (l1, l2) = collect_types xs in - (x::l1, l2) - else - ([], l) + let (l1, l2) = collect_types xs in + match l1 with + | [] -> + let ty = Structures.retyping_get_type_of env sigma x in + if Constr.iskind ty || + let c, _ = Structures.decompose_app ty in + Structures.eq_constr c (Lazy.force cCompDec) + then + (x::[], xs) + else + ([], l) + | _ -> (x::l1, l2) in let (args1, args2) = collect_types args in let c, args = -- cgit From abe0badbe84a90bae4f20541781609ed0ebb3fb9 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 14 Oct 2021 17:07:25 +0200 Subject: Small optim --- src/trace/smtAtom.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/trace') diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 1d608e6..06e1472 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -1351,7 +1351,7 @@ module Atom = let c, _ = Structures.decompose_app ty in Structures.eq_constr c (Lazy.force cCompDec) then - (x::[], xs) + ([x], xs) else ([], l) | _ -> (x::l1, l2) -- cgit From bd346e44c8993b758013d98855b71404e4d0ad7f Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 7 Dec 2021 18:53:40 +0100 Subject: Solved bug in delayed ComDec --- src/trace/smtBtype.ml | 5 ++--- src/trace/smtMisc.ml | 2 +- src/trace/smtMisc.mli | 2 +- 3 files changed, 4 insertions(+), 5 deletions(-) (limited to 'src/trace') diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 3b6d107..7c08157 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -304,10 +304,9 @@ let of_coq_compdec reify t compdec = (match i.hval with | CompDec _ -> ty | Delayed _ -> - Hashtbl.remove reify.tbl t; let ce = mklApp cTyp_compdec [|t; compdec|] in - let res = Tindex {index = i.index; hval = CompDec ce} in - Hashtbl.add reify.tbl t res; + i.hval <- CompDec ce; + let res = Tindex i in res ) | _ -> ty diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 2080a64..e4747dd 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -21,7 +21,7 @@ let mkInt i = ci (** Generic representation of shared object *) -type 'a gen_hashed = { index : int; hval : 'a } +type 'a gen_hashed = { index : int; mutable hval : 'a } (** Functions over constr *) diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index a6f5db8..6378627 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -12,7 +12,7 @@ val cInt_tbl : (int, Structures.constr) Hashtbl.t val mkInt : int -> Structures.constr -type 'a gen_hashed = { index : int; hval : 'a; } +type 'a gen_hashed = { index : int; mutable hval : 'a; } val mklApp : Structures.constr Lazy.t -> Structures.constr array -> Structures.constr val string_of_name_def : string -> Structures.name -> string val string_coq_constr : Structures.constr -> string -- cgit From c163813243e1b38b7d8c10b49d78a728d747e0e5 Mon Sep 17 00:00:00 2001 From: ckeller Date: Tue, 15 Feb 2022 18:27:33 +0100 Subject: Use the Register mechanism (#104) --- src/trace/coqInterface.ml | 32 --- src/trace/coqInterface.mli | 11 - src/trace/coqTerms.ml | 575 +++++++++++++++++++++++++++------------------ src/trace/coqTerms.mli | 487 ++++++++++++++++++++++---------------- src/trace/satAtom.ml | 2 +- src/trace/smtAtom.ml | 4 +- src/trace/smtBtype.ml | 2 +- src/trace/smtCommands.ml | 130 +++++----- src/trace/smtForm.ml | 4 +- src/trace/smtTrace.ml | 8 +- 10 files changed, 694 insertions(+), 561 deletions(-) (limited to 'src/trace') diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml index 81a22c9..65cd99c 100644 --- a/src/trace/coqInterface.ml +++ b/src/trace/coqInterface.ml @@ -103,41 +103,13 @@ type econstr = EConstr.t let econstr_of_constr = EConstr.of_constr -(* Modules *) -let gen_constant_in_modules s m n = - (* UnivGen.constr_of_monomorphic_global will crash on universe polymorphic constants *) - UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n -let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) -let init_modules = Coqlib.init_modules - - (* Int63 *) -let int63_module = [["Coq";"Numbers";"Cyclic";"Int63";"Int63"]] - let mkInt : int -> Constr.constr = fun i -> Constr.mkInt (Uint63.of_int i) -let cint = gen_constant int63_module "int" - (* PArray *) -let parray_modules = [["SMTCoq";"PArray";"PArray"]] - -let cmake = gen_constant parray_modules "make" -let cset = gen_constant parray_modules "set" - let max_array_size : int = 4194302 -let mkArray : Constr.types * Constr.t array -> Constr.t = - fun (ty, a) -> - let l = (Array.length a) - 1 in - snd (Array.fold_left (fun (i,acc) c -> - let acc' = - if i = l then - acc - else - mkApp (Lazy.force cset, [|ty; acc; mkInt i; c|]) in - (i+1,acc') - ) (0, mkApp (Lazy.force cmake, [|ty; mkInt l; a.(l)|])) a) (* Traces *) @@ -158,10 +130,6 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = module Micromega_plugin_Micromega = Micromega_plugin.Micromega module Micromega_plugin_Certificate = Micromega_plugin.Certificate -let micromega_coq_proofTerm = - (* Cannot contain evars *) - lazy (gen_constant_in_modules "ZMicromega" [["Coq"; "micromega";"ZMicromega"]] "ZArithProof") - let micromega_dump_proof_term p = (* Cannot contain evars *) EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli index 38d78d8..857303c 100644 --- a/src/trace/coqInterface.mli +++ b/src/trace/coqInterface.mli @@ -59,21 +59,12 @@ type econstr = EConstr.t val econstr_of_constr : constr -> econstr -(* Modules *) -val gen_constant : string list list -> string -> constr lazy_t -val init_modules : string list list - - (* Int63 *) -val int63_module : string list list val mkInt : int -> constr -val cint : constr lazy_t (* PArray *) -val parray_modules : string list list val max_array_size : int -val mkArray : types * constr array -> constr (* Traces *) @@ -91,8 +82,6 @@ val mkTrace : (* Micromega *) module Micromega_plugin_Micromega = Micromega_plugin.Micromega module Micromega_plugin_Certificate = Micromega_plugin.Certificate - -val micromega_coq_proofTerm : constr lazy_t val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 67392bb..1dc5af0 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -13,276 +13,371 @@ open SmtMisc -let gen_constant = CoqInterface.gen_constant +type coqTerm = CoqInterface.constr lazy_t + +let gc prefix constant = + lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref (prefix ^ "." ^ constant))) (* Int63 *) -let cint = CoqInterface.cint -let ceq63 = gen_constant CoqInterface.int63_module "eqb" +let int63_prefix = "num.int63" +let int63_gc = gc int63_prefix +let cint = int63_gc "type" +let ceq63 = int63_gc "eqb" (* PArray *) -let carray = gen_constant CoqInterface.parray_modules "array" +let array_prefix = "array.array" +let array_gc = gc array_prefix +let carray = array_gc "type" +let cmake = array_gc "make" +let cset = array_gc "set" (* is_true *) -let cis_true = gen_constant CoqInterface.init_modules "is_true" +let cis_true = gc "core.is_true" "is_true" (* nat *) -let cnat = gen_constant CoqInterface.init_modules "nat" -let cO = gen_constant CoqInterface.init_modules "O" -let cS = gen_constant CoqInterface.init_modules "S" +let nat_prefix = "num.nat" +let nat_gc = gc nat_prefix +let cnat = nat_gc "type" +let cO = nat_gc "O" +let cS = nat_gc "S" (* 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" +let positive_prefix = "num.pos" +let positive_gc = gc positive_prefix +let cpositive = positive_gc "type" +let cxI = positive_gc "xI" +let cxO = positive_gc "xO" +let cxH = positive_gc "xH" +let ceqbP = positive_gc "eqb" (* N *) -let n_modules = [["Coq";"NArith";"BinNat";"N"]] - -let cN = gen_constant positive_modules "N" -let cN0 = gen_constant positive_modules "N0" -let cNpos = gen_constant positive_modules "Npos" - -let cof_nat = gen_constant n_modules "of_nat" - +let n_prefix = "num.N" +let n_gc = gc n_prefix +let cN = n_gc "type" +let cN0 = n_gc "N0" +let cNpos = n_gc "Npos" +let cof_nat = n_gc "of_nat" (* 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" -let ceqbZ = gen_constant z_modules "eqb" -(* let cZeqbsym = gen_constant z_modules "eqb_sym" *) +let z_prefix = "num.Z" +let z_gc = gc z_prefix +let cZ = z_gc "type" +let cZ0 = z_gc "Z0" +let cZpos = z_gc "Zpos" +let cZneg = z_gc "Zneg" +let copp = z_gc "opp" +let cadd = z_gc "add" +let csub = z_gc "sub" +let cmul = z_gc "mul" +let cltb = z_gc "ltb" +let cleb = z_gc "leb" +let cgeb = z_gc "geb" +let cgtb = z_gc "gtb" +let ceqbZ = z_gc "eqb" (* Booleans *) -let bool_modules = [["Coq";"Bool";"Bool"]] - -let cbool = gen_constant CoqInterface.init_modules "bool" -let ctrue = gen_constant CoqInterface.init_modules "true" -let cfalse = gen_constant CoqInterface.init_modules "false" -let candb = gen_constant CoqInterface.init_modules "andb" -let corb = gen_constant CoqInterface.init_modules "orb" -let cxorb = gen_constant CoqInterface.init_modules "xorb" -let cnegb = gen_constant CoqInterface.init_modules "negb" -let cimplb = gen_constant CoqInterface.init_modules "implb" -let ceqb = gen_constant bool_modules "eqb" -let cifb = gen_constant bool_modules "ifb" -let ciff = gen_constant CoqInterface.init_modules "iff" -let creflect = gen_constant bool_modules "reflect" +let bool_prefix = "core.bool" +let bool_gc = gc bool_prefix +let cbool = bool_gc "type" +let ctrue = bool_gc "true" +let cfalse = bool_gc "false" +let candb = bool_gc "andb" +let corb = bool_gc "orb" +let cxorb = bool_gc "xorb" +let cnegb = bool_gc "negb" +let cimplb = bool_gc "implb" +let ceqb = bool_gc "eqb" +let cifb = bool_gc "ifb" +let creflect = bool_gc "reflect" (* Lists *) -let clist = gen_constant CoqInterface.init_modules "list" -let cnil = gen_constant CoqInterface.init_modules "nil" -let ccons = gen_constant CoqInterface.init_modules "cons" -let clength = gen_constant CoqInterface.init_modules "length" +let list_prefix = "core.list" +let list_gc = gc list_prefix +let clist = list_gc "type" +let cnil = list_gc "nil" +let ccons = list_gc "cons" +let clength = list_gc "length" (* Option *) -let coption = gen_constant CoqInterface.init_modules "option" -let cSome = gen_constant CoqInterface.init_modules "Some" -let cNone = gen_constant CoqInterface.init_modules "None" +let option_prefix = "core.option" +let option_gc = gc option_prefix +let coption = option_gc "type" +let cSome = option_gc "Some" +let cNone = option_gc "None" (* Pairs *) -let cpair = gen_constant CoqInterface.init_modules "pair" -let cprod = gen_constant CoqInterface.init_modules "prod" +let pair_prefix = "core.prod" +let pair_gc = gc pair_prefix +let cpair = pair_gc "intro" +let cprod = pair_gc "type" (* Dependent pairs *) -let csigT = gen_constant CoqInterface.init_modules "sigT" -(* let cprojT1 = gen_constant CoqInterface.init_modules "projT1" *) -(* let cprojT2 = gen_constant CoqInterface.init_modules "projT2" *) -(* let cprojT3 = gen_constant CoqInterface.init_modules "projT3" *) - -(* let csigT2 = gen_constant CoqInterface.init_modules "sigT2" *) -(* let csigT_of_sigT2 = gen_constant CoqInterface.init_modules "sigT_of_sigT2" *) +let sigT_prefix = "core.sigT" +let sigT_gc = gc sigT_prefix +let csigT = sigT_gc "type" (* Logical Operators *) -let cnot = gen_constant CoqInterface.init_modules "not" -let ceq = gen_constant CoqInterface.init_modules "eq" -let crefl_equal = gen_constant CoqInterface.init_modules "eq_refl" -let cconj = gen_constant CoqInterface.init_modules "conj" -let cand = gen_constant CoqInterface.init_modules "and" +let cnot = gc "core.not" "type" +let cconj = gc "core.and" "conj" +let cand = gc "core.and" "type" +let ciff = gc "core.iff" "type" + +(* Equality *) +let eq_prefix = "core.eq" +let eq_gc = gc eq_prefix +let ceq = eq_gc "type" +let crefl_equal = eq_gc "refl" + +(* Micromega *) +let micromega_prefix = "micromega.ZMicromega" +let micromega_gc = gc micromega_prefix +let micromega_coq_proofTerm = micromega_gc "ZArithProof" (* Bit vectors *) -let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]] -let cbitvector = gen_constant bv_modules "bitvector" -let cof_bits = gen_constant bv_modules "of_bits" -(* let c_of_bits = gen_constant bv_modules "_of_bits" *) -let cbitOf = gen_constant bv_modules "bitOf" -let cbv_eq = gen_constant bv_modules "bv_eq" -let cbv_not = gen_constant bv_modules "bv_not" -let cbv_neg = gen_constant bv_modules "bv_neg" -let cbv_and = gen_constant bv_modules "bv_and" -let cbv_or = gen_constant bv_modules "bv_or" -let cbv_xor = gen_constant bv_modules "bv_xor" -let cbv_add = gen_constant bv_modules "bv_add" -let cbv_mult = gen_constant bv_modules "bv_mult" -let cbv_ult = gen_constant bv_modules "bv_ult" -let cbv_slt = gen_constant bv_modules "bv_slt" -let cbv_concat = gen_constant bv_modules "bv_concat" -let cbv_extr = gen_constant bv_modules "bv_extr" -let cbv_zextn = gen_constant bv_modules "bv_zextn" -let cbv_sextn = gen_constant bv_modules "bv_sextn" -let cbv_shl = gen_constant bv_modules "bv_shl" -let cbv_shr = gen_constant bv_modules "bv_shr" - +let bv_prefix = "SMTCoq.bva.BVList.BITVECTOR_LIST" +let bv_gc = gc bv_prefix +let cbitvector = bv_gc "bitvector" +let cof_bits = bv_gc "of_bits" +let cbitOf = bv_gc "bitOf" +let cbv_eq = bv_gc "bv_eq" +let cbv_not = bv_gc "bv_not" +let cbv_neg = bv_gc "bv_neg" +let cbv_and = bv_gc "bv_and" +let cbv_or = bv_gc "bv_or" +let cbv_xor = bv_gc "bv_xor" +let cbv_add = bv_gc "bv_add" +let cbv_mult = bv_gc "bv_mult" +let cbv_ult = bv_gc "bv_ult" +let cbv_slt = bv_gc "bv_slt" +let cbv_concat = bv_gc "bv_concat" +let cbv_extr = bv_gc "bv_extr" +let cbv_zextn = bv_gc "bv_zextn" +let cbv_sextn = bv_gc "bv_sextn" +let cbv_shl = bv_gc "bv_shl" +let cbv_shr = bv_gc "bv_shr" (* Arrays *) -let array_modules = [["SMTCoq";"array";"FArray"]] -let cfarray = gen_constant array_modules "FArray.farray" -let cselect = gen_constant array_modules "select" -let cstore = gen_constant array_modules "store" -let cdiff = gen_constant array_modules "diff" -let cequalarray = gen_constant array_modules "FArray.equal" - -(* OrderedType *) -(* let cOrderedTypeCompare = - * gen_constant [["Coq";"Structures";"OrderedType"]] "Compare" *) - -(* 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 cState_C_t = gen_constant [["SMTCoq";"State";"C"]] "t" -let cState_S_t = gen_constant [["SMTCoq";"State";"S"]] "t" - -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 cTBV = gen_constant smt_modules "TBV" -let cTFArray = gen_constant smt_modules "TFArray" -let cTindex = gen_constant smt_modules "Tindex" - -(* let ct_i = gen_constant smt_modules "t_i" *) -let cinterp_t = gen_constant smt_modules "Typ.interp" -let cdec_interp = gen_constant smt_modules "dec_interp" -let cord_interp = gen_constant smt_modules "ord_interp" -let ccomp_interp = gen_constant smt_modules "comp_interp" -let cinh_interp = gen_constant smt_modules "inh_interp" - -let cinterp_eqb = gen_constant smt_modules "i_eqb" -(* let cinterp_eqb_eqb = gen_constant smt_modules "i_eqb_eqb" *) - -let classes_modules = [["SMTCoq";"classes";"SMT_classes"]; - ["SMTCoq";"classes";"SMT_classes_instances"]] - -let ctyp_compdec = gen_constant classes_modules "typ_compdec" -let cTyp_compdec = gen_constant classes_modules "Typ_compdec" -(* let ctyp_compdec_from = gen_constant classes_modules "typ_compdec_from" *) -let cunit_typ_compdec = gen_constant classes_modules "unit_typ_compdec" -let cte_carrier = gen_constant classes_modules "te_carrier" -let cte_compdec = gen_constant classes_modules "te_compdec" -let ceqb_of_compdec = gen_constant classes_modules "eqb_of_compdec" -let cCompDec = gen_constant classes_modules "CompDec" - -let cbool_compdec = gen_constant classes_modules "bool_compdec" -let cZ_compdec = gen_constant classes_modules "Z_compdec" -let cPositive_compdec = gen_constant classes_modules "Positive_compdec" -let cBV_compdec = gen_constant classes_modules "BV_compdec" -let cFArray_compdec = gen_constant classes_modules "FArray_compdec" - -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 cCO_BV = gen_constant smt_modules "CO_BV" - -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 cUO_BVbitOf = gen_constant smt_modules "UO_BVbitOf" -let cUO_BVnot = gen_constant smt_modules "UO_BVnot" -let cUO_BVneg = gen_constant smt_modules "UO_BVneg" -let cUO_BVextr = gen_constant smt_modules "UO_BVextr" -let cUO_BVzextn = gen_constant smt_modules "UO_BVzextn" -let cUO_BVsextn = gen_constant smt_modules "UO_BVsextn" - -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 cBO_BVand = gen_constant smt_modules "BO_BVand" -let cBO_BVor = gen_constant smt_modules "BO_BVor" -let cBO_BVxor = gen_constant smt_modules "BO_BVxor" -let cBO_BVadd = gen_constant smt_modules "BO_BVadd" -let cBO_BVmult = gen_constant smt_modules "BO_BVmult" -let cBO_BVult = gen_constant smt_modules "BO_BVult" -let cBO_BVslt = gen_constant smt_modules "BO_BVslt" -let cBO_BVconcat = gen_constant smt_modules "BO_BVconcat" -let cBO_BVshl = gen_constant smt_modules "BO_BVshl" -let cBO_BVshr = gen_constant smt_modules "BO_BVshr" -let cBO_select = gen_constant smt_modules "BO_select" -let cBO_diffarray = gen_constant smt_modules "BO_diffarray" - -let cTO_store = gen_constant smt_modules "TO_store" - -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 cAtop = gen_constant smt_modules "Atop" -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 cFbbT = gen_constant smt_modules "FbbT" - -let cvalid_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "valid" -let cinterp_var_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "interp_var" - -let make_certif_ops modules args = +let array_prefix = "SMTCoq.array.FArray" +let array_gc = gc array_prefix +let cfarray = array_gc "farray" +let cselect = array_gc "select" +let cstore = array_gc "store" +let cdiff = array_gc "diff" +let cequalarray = array_gc "equal" + +(* SMTCoq terms *) +let state_prefix = "SMTCoq.State" +let state_gc = gc state_prefix +let cState_C_t = state_gc "C.t" +let cState_S_t = state_gc "S.t" + +let misc_prefix = "SMTCoq.Misc" +let misc_gc = gc misc_prefix +let cdistinct = misc_gc "distinct" + +let terms_prefix = "SMTCoq.SMT_terms" +let terms_gc = gc terms_prefix + +let ctype = terms_gc "Typ.type" +let cTZ = terms_gc "Typ.TZ" +let cTbool = terms_gc "Typ.Tbool" +let cTpositive = terms_gc "Typ.Tpositive" +let cTBV = terms_gc "Typ.TBV" +let cTFArray = terms_gc "Typ.TFArray" +let cTindex = terms_gc "Typ.Tindex" + +let cinterp_t = terms_gc "Typ.interp" +let cdec_interp = terms_gc "Typ.dec_interp" +let cord_interp = terms_gc "Typ.ord_interp" +let ccomp_interp = terms_gc "Typ.comp_interp" +let cinh_interp = terms_gc "Typ.inh_interp" + +let cinterp_eqb = terms_gc "Typ.i_eqb" + +let ctval = terms_gc "Atom.tval" +let cTval = terms_gc "Atom.Tval" + +let cCO_xH = terms_gc "Atom.CO_xH" +let cCO_Z0 = terms_gc "Atom.CO_Z0" +let cCO_BV = terms_gc "Atom.CO_BV" + +let cUO_xO = terms_gc "Atom.UO_xO" +let cUO_xI = terms_gc "Atom.UO_xI" +let cUO_Zpos = terms_gc "Atom.UO_Zpos" +let cUO_Zneg = terms_gc "Atom.UO_Zneg" +let cUO_Zopp = terms_gc "Atom.UO_Zopp" +let cUO_BVbitOf = terms_gc "Atom.UO_BVbitOf" +let cUO_BVnot = terms_gc "Atom.UO_BVnot" +let cUO_BVneg = terms_gc "Atom.UO_BVneg" +let cUO_BVextr = terms_gc "Atom.UO_BVextr" +let cUO_BVzextn = terms_gc "Atom.UO_BVzextn" +let cUO_BVsextn = terms_gc "Atom.UO_BVsextn" + +let cBO_Zplus = terms_gc "Atom.BO_Zplus" +let cBO_Zminus = terms_gc "Atom.BO_Zminus" +let cBO_Zmult = terms_gc "Atom.BO_Zmult" +let cBO_Zlt = terms_gc "Atom.BO_Zlt" +let cBO_Zle = terms_gc "Atom.BO_Zle" +let cBO_Zge = terms_gc "Atom.BO_Zge" +let cBO_Zgt = terms_gc "Atom.BO_Zgt" +let cBO_eq = terms_gc "Atom.BO_eq" +let cBO_BVand = terms_gc "Atom.BO_BVand" +let cBO_BVor = terms_gc "Atom.BO_BVor" +let cBO_BVxor = terms_gc "Atom.BO_BVxor" +let cBO_BVadd = terms_gc "Atom.BO_BVadd" +let cBO_BVmult = terms_gc "Atom.BO_BVmult" +let cBO_BVult = terms_gc "Atom.BO_BVult" +let cBO_BVslt = terms_gc "Atom.BO_BVslt" +let cBO_BVconcat = terms_gc "Atom.BO_BVconcat" +let cBO_BVshl = terms_gc "Atom.BO_BVshl" +let cBO_BVshr = terms_gc "Atom.BO_BVshr" +let cBO_select = terms_gc "Atom.BO_select" +let cBO_diffarray = terms_gc "Atom.BO_diffarray" + +let cTO_store = terms_gc "Atom.TO_store" + +let cNO_distinct = terms_gc "Atom.NO_distinct" + +let catom = terms_gc "Atom.atom" +let cAcop = terms_gc "Atom.Acop" +let cAuop = terms_gc "Atom.Auop" +let cAbop = terms_gc "Atom.Abop" +let cAtop = terms_gc "Atom.Atop" +let cAnop = terms_gc "Atom.Anop" +let cAapp = terms_gc "Atom.Aapp" + +let cform = terms_gc "Form.form" +let cFatom = terms_gc "Form.Fatom" +let cFtrue = terms_gc "Form.Ftrue" +let cFfalse = terms_gc "Form.Ffalse" +let cFnot2 = terms_gc "Form.Fnot2" +let cFand = terms_gc "Form.Fand" +let cFor = terms_gc "Form.For" +let cFxor = terms_gc "Form.Fxor" +let cFimp = terms_gc "Form.Fimp" +let cFiff = terms_gc "Form.Fiff" +let cFite = terms_gc "Form.Fite" +let cFbbT = terms_gc "Form.FbbT" + +(* SMTCoq Classes *) +let classes_prefix = "SMTCoq.classes.SMT_classes" +let classes_gc = gc classes_prefix +let ctyp_compdec = classes_gc "typ_compdec" +let cTyp_compdec = classes_gc "Typ_compdec" +let cte_carrier = classes_gc "te_carrier" +let cte_compdec = classes_gc "te_compdec" +let ceqb_of_compdec = classes_gc "eqb_of_compdec" +let cCompDec = classes_gc "CompDec" + +let classesi_prefix = "SMTCoq.classes.SMT_classes_instances" +let classesi_gc = gc classesi_prefix +let cunit_typ_compdec = classesi_gc "unit_typ_compdec" +let cbool_compdec = classesi_gc "bool_compdec" +let cZ_compdec = classesi_gc "Z_compdec" +let cPositive_compdec = classesi_gc "Positive_compdec" +let cBV_compdec = classesi_gc "BV_compdec" +let cFArray_compdec = classesi_gc "FArray_compdec" + +(* SMTCoq Trace *) +let sat_checker_prefix = "SMTCoq.Trace.Sat_Checker" +let sat_checker_gc = gc sat_checker_prefix +let csat_checker_valid = sat_checker_gc "valid" +let csat_checker_interp_var = sat_checker_gc "interp_var" +let csat_checker_Certif = sat_checker_gc "Certif" +let csat_checker_dimacs = sat_checker_gc "dimacs" +let csat_checker_certif = sat_checker_gc "certif" +let csat_checker_theorem_checker = sat_checker_gc "theorem_checker" +let csat_checker_checker = sat_checker_gc "checker" + +let cnf_checker_prefix = "SMTCoq.Trace.Cnf_Checker" +let cnf_checker_gc = gc cnf_checker_prefix +let ccnf_checker_certif = cnf_checker_gc "certif" +let ccnf_checker_Certif = cnf_checker_gc "Certif" +let ccnf_checker_checker_b_correct = cnf_checker_gc "checker_b_correct" +let ccnf_checker_checker_b = cnf_checker_gc "checker_b" +let ccnf_checker_checker_eq_correct = cnf_checker_gc "checker_eq_correct" +let ccnf_checker_checker_eq = cnf_checker_gc "checker_eq" + +let euf_checker_prefix = "SMTCoq.Trace.Euf_Checker" +let euf_checker_gc = gc euf_checker_prefix +let ceuf_checker_Certif = euf_checker_gc "Certif" +let ceuf_checker_certif = euf_checker_gc "certif" +let ceuf_checker_checker = euf_checker_gc "checker" +let ceuf_checker_checker_correct = euf_checker_gc "checker_correct" +let ceuf_checker_checker_b_correct = euf_checker_gc "checker_b_correct" +let ceuf_checker_checker_b = euf_checker_gc "checker_b" +let ceuf_checker_checker_eq_correct = euf_checker_gc "checker_eq_correct" +let ceuf_checker_checker_eq = euf_checker_gc "checker_eq" +let ceuf_checker_checker_debug = euf_checker_gc "checker_debug" +let ceuf_checker_name_step = euf_checker_gc "name_step" +let ceuf_checker_Name_Res = euf_checker_gc "Name_Res" +let ceuf_checker_Name_Weaken = euf_checker_gc "Name_Weaken" +let ceuf_checker_Name_ImmFlatten = euf_checker_gc "Name_ImmFlatten" +let ceuf_checker_Name_CTrue = euf_checker_gc "Name_CTrue" +let ceuf_checker_Name_CFalse = euf_checker_gc "Name_CFalse" +let ceuf_checker_Name_BuildDef = euf_checker_gc "Name_BuildDef" +let ceuf_checker_Name_BuildDef2 = euf_checker_gc "Name_BuildDef2" +let ceuf_checker_Name_BuildProj = euf_checker_gc "Name_BuildProj" +let ceuf_checker_Name_ImmBuildDef = euf_checker_gc "Name_ImmBuildDef" +let ceuf_checker_Name_ImmBuildDef2 = euf_checker_gc "Name_ImmBuildDef2" +let ceuf_checker_Name_ImmBuildProj = euf_checker_gc "Name_ImmBuildProj" +let ceuf_checker_Name_EqTr = euf_checker_gc "Name_EqTr" +let ceuf_checker_Name_EqCgr = euf_checker_gc "Name_EqCgr" +let ceuf_checker_Name_EqCgrP = euf_checker_gc "Name_EqCgrP" +let ceuf_checker_Name_LiaMicromega = euf_checker_gc "Name_LiaMicromega" +let ceuf_checker_Name_LiaDiseq = euf_checker_gc "Name_LiaDiseq" +let ceuf_checker_Name_SplArith = euf_checker_gc "Name_SplArith" +let ceuf_checker_Name_SplDistinctElim = euf_checker_gc "Name_SplDistinctElim" +let ceuf_checker_Name_BBVar = euf_checker_gc "Name_BBVar" +let ceuf_checker_Name_BBConst = euf_checker_gc "Name_BBConst" +let ceuf_checker_Name_BBOp = euf_checker_gc "Name_BBOp" +let ceuf_checker_Name_BBNot = euf_checker_gc "Name_BBNot" +let ceuf_checker_Name_BBNeg = euf_checker_gc "Name_BBNeg" +let ceuf_checker_Name_BBAdd = euf_checker_gc "Name_BBAdd" +let ceuf_checker_Name_BBConcat = euf_checker_gc "Name_BBConcat" +let ceuf_checker_Name_BBMul = euf_checker_gc "Name_BBMul" +let ceuf_checker_Name_BBUlt = euf_checker_gc "Name_BBUlt" +let ceuf_checker_Name_BBSlt = euf_checker_gc "Name_BBSlt" +let ceuf_checker_Name_BBEq = euf_checker_gc "Name_BBEq" +let ceuf_checker_Name_BBDiseq = euf_checker_gc "Name_BBDiseq" +let ceuf_checker_Name_BBExtract = euf_checker_gc "Name_BBExtract" +let ceuf_checker_Name_BBZextend = euf_checker_gc "Name_BBZextend" +let ceuf_checker_Name_BBSextend = euf_checker_gc "Name_BBSextend" +let ceuf_checker_Name_BBShl = euf_checker_gc "Name_BBShl" +let ceuf_checker_Name_BBShr = euf_checker_gc "Name_BBShr" +let ceuf_checker_Name_RowEq = euf_checker_gc "Name_RowEq" +let ceuf_checker_Name_RowNeq = euf_checker_gc "Name_RowNeq" +let ceuf_checker_Name_Ext = euf_checker_gc "Name_Ext" +let ceuf_checker_Name_Hole = euf_checker_gc "Name_Hole" + +type certif_ops = + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm +let make_certif_ops prefix args = + let gc = gc prefix in let gen_constant c = match args with - | Some args -> lazy (mklApp (gen_constant modules c) args) - | None -> gen_constant modules c in + | Some args -> lazy (mklApp (gc c) args) + | None -> gc c in (gen_constant "step", gen_constant "Res", gen_constant "Weaken", gen_constant "ImmFlatten", gen_constant "CTrue", gen_constant "CFalse", gen_constant "BuildDef", gen_constant "BuildDef2", gen_constant "BuildProj", - gen_constant "ImmBuildProj", gen_constant"ImmBuildDef", + gen_constant "ImmBuildProj", gen_constant "ImmBuildDef", gen_constant"ImmBuildDef2", gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP", gen_constant "LiaMicromega", gen_constant "LiaDiseq", @@ -296,6 +391,9 @@ let make_certif_ops modules args = gen_constant "BBShl", gen_constant "BBShr", gen_constant "RowEq", gen_constant "RowNeq", gen_constant "Ext", gen_constant "Hole", gen_constant "ForallInst") +let csat_checker_certif_ops = make_certif_ops sat_checker_prefix None +let ccnf_checker_certif_ops = make_certif_ops cnf_checker_prefix None +let ceuf_checker_certif_ops = make_certif_ops euf_checker_prefix (** Useful constructions *) @@ -352,6 +450,19 @@ let rec mk_bv_list = function | b :: bv -> mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|] +(* Compute an array *) +let mkArray : Constr.types * Constr.t array -> Constr.t = + fun (ty, a) -> + let l = (Array.length a) - 1 in + snd (Array.fold_left (fun (i,acc) c -> + let acc' = + if i = l then + acc + else + mklApp cset [|ty; acc; mkInt i; c|] in + (i+1,acc') + ) (0, mklApp cmake [|ty; mkInt l; a.(l)|]) a) + (* Reification *) let mk_bool b = diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index 92acbb6..b5b1a0b 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -10,249 +10,322 @@ (**************************************************************************) -val gen_constant : string list list -> string -> CoqInterface.constr lazy_t +type coqTerm = CoqInterface.constr lazy_t (* Int63 *) -val cint : CoqInterface.constr lazy_t -val ceq63 : CoqInterface.constr lazy_t +val cint : coqTerm +val ceq63 : coqTerm (* PArray *) -val carray : CoqInterface.constr lazy_t +val carray : coqTerm +val cmake : coqTerm +val cset : coqTerm + +(* is_true *) +val cis_true : coqTerm (* nat *) -val cnat : CoqInterface.constr lazy_t -val cO : CoqInterface.constr lazy_t -val cS : CoqInterface.constr lazy_t +val cnat : coqTerm +val cO : coqTerm +val cS : coqTerm (* Positive *) -val cpositive : CoqInterface.constr lazy_t -val cxI : CoqInterface.constr lazy_t -val cxO : CoqInterface.constr lazy_t -val cxH : CoqInterface.constr lazy_t -val ceqbP : CoqInterface.constr lazy_t +val cpositive : coqTerm +val cxI : coqTerm +val cxO : coqTerm +val cxH : coqTerm +val ceqbP : coqTerm (* N *) -val cN : CoqInterface.constr lazy_t -val cN0 : CoqInterface.constr lazy_t -val cNpos : CoqInterface.constr lazy_t -val cof_nat : CoqInterface.constr lazy_t +val cN : coqTerm +val cN0 : coqTerm +val cNpos : coqTerm +val cof_nat : coqTerm (* Z *) -val cZ : CoqInterface.constr lazy_t -val cZ0 : CoqInterface.constr lazy_t -val cZpos : CoqInterface.constr lazy_t -val cZneg : CoqInterface.constr lazy_t -val copp : CoqInterface.constr lazy_t -val cadd : CoqInterface.constr lazy_t -val csub : CoqInterface.constr lazy_t -val cmul : CoqInterface.constr lazy_t -val cltb : CoqInterface.constr lazy_t -val cleb : CoqInterface.constr lazy_t -val cgeb : CoqInterface.constr lazy_t -val cgtb : CoqInterface.constr lazy_t -val ceqbZ : CoqInterface.constr lazy_t +val cZ : coqTerm +val cZ0 : coqTerm +val cZpos : coqTerm +val cZneg : coqTerm +val copp : coqTerm +val cadd : coqTerm +val csub : coqTerm +val cmul : coqTerm +val cltb : coqTerm +val cleb : coqTerm +val cgeb : coqTerm +val cgtb : coqTerm +val ceqbZ : coqTerm (* Booleans *) -val cbool : CoqInterface.constr lazy_t -val ctrue : CoqInterface.constr lazy_t -val cfalse : CoqInterface.constr lazy_t -val candb : CoqInterface.constr lazy_t -val corb : CoqInterface.constr lazy_t -val cxorb : CoqInterface.constr lazy_t -val cnegb : CoqInterface.constr lazy_t -val cimplb : CoqInterface.constr lazy_t -val ceqb : CoqInterface.constr lazy_t -val cifb : CoqInterface.constr lazy_t -val ciff : CoqInterface.constr lazy_t -val creflect : CoqInterface.constr lazy_t +val cbool : coqTerm +val ctrue : coqTerm +val cfalse : coqTerm +val candb : coqTerm +val corb : coqTerm +val cxorb : coqTerm +val cnegb : coqTerm +val cimplb : coqTerm +val ceqb : coqTerm +val cifb : coqTerm +val creflect : coqTerm (* Lists *) -val clist : CoqInterface.constr lazy_t -val cnil : CoqInterface.constr lazy_t -val ccons : CoqInterface.constr lazy_t -val clength : CoqInterface.constr lazy_t +val clist : coqTerm +val cnil : coqTerm +val ccons : coqTerm +val clength : coqTerm (* Option *) -val coption : CoqInterface.constr lazy_t -val cSome : CoqInterface.constr lazy_t -val cNone : CoqInterface.constr lazy_t +val coption : coqTerm +val cSome : coqTerm +val cNone : coqTerm (* Pairs *) -val cpair : CoqInterface.constr lazy_t -val cprod : CoqInterface.constr lazy_t +val cpair : coqTerm +val cprod : coqTerm (* Dependent pairs *) -val csigT : CoqInterface.constr lazy_t +val csigT : coqTerm (* Logical Operators *) -val cnot : CoqInterface.constr lazy_t -val ceq : CoqInterface.constr lazy_t -val crefl_equal : CoqInterface.constr lazy_t -val cconj : CoqInterface.constr lazy_t -val cand : CoqInterface.constr lazy_t +val cnot : coqTerm +val cconj : coqTerm +val cand : coqTerm +val ciff : coqTerm + +(* Equality *) +val ceq : coqTerm +val crefl_equal : coqTerm + +(* Micromega *) +val micromega_coq_proofTerm : coqTerm (* Bit vectors *) -val cbitvector : CoqInterface.constr lazy_t -val cof_bits : CoqInterface.constr lazy_t -val cbitOf : CoqInterface.constr lazy_t -val cbv_eq : CoqInterface.constr lazy_t -val cbv_not : CoqInterface.constr lazy_t -val cbv_neg : CoqInterface.constr lazy_t -val cbv_and : CoqInterface.constr lazy_t -val cbv_or : CoqInterface.constr lazy_t -val cbv_xor : CoqInterface.constr lazy_t -val cbv_add : CoqInterface.constr lazy_t -val cbv_mult : CoqInterface.constr lazy_t -val cbv_ult : CoqInterface.constr lazy_t -val cbv_slt : CoqInterface.constr lazy_t -val cbv_concat : CoqInterface.constr lazy_t -val cbv_extr : CoqInterface.constr lazy_t -val cbv_zextn : CoqInterface.constr lazy_t -val cbv_sextn : CoqInterface.constr lazy_t -val cbv_shl : CoqInterface.constr lazy_t -val cbv_shr : CoqInterface.constr lazy_t +val cbitvector : coqTerm +val cof_bits : coqTerm +val cbitOf : coqTerm +val cbv_eq : coqTerm +val cbv_not : coqTerm +val cbv_neg : coqTerm +val cbv_and : coqTerm +val cbv_or : coqTerm +val cbv_xor : coqTerm +val cbv_add : coqTerm +val cbv_mult : coqTerm +val cbv_ult : coqTerm +val cbv_slt : coqTerm +val cbv_concat : coqTerm +val cbv_extr : coqTerm +val cbv_zextn : coqTerm +val cbv_sextn : coqTerm +val cbv_shl : coqTerm +val cbv_shr : coqTerm (* Arrays *) -val cfarray : CoqInterface.constr lazy_t -val cselect : CoqInterface.constr lazy_t -val cstore : CoqInterface.constr lazy_t -val cdiff : CoqInterface.constr lazy_t -val cequalarray : CoqInterface.constr lazy_t - -(* OrderedType *) - -(* SMT_terms *) -val cState_C_t : CoqInterface.constr lazy_t -val cState_S_t : CoqInterface.constr lazy_t - -val cdistinct : CoqInterface.constr lazy_t - -val ctype : CoqInterface.constr lazy_t -val cTZ : CoqInterface.constr lazy_t -val cTbool : CoqInterface.constr lazy_t -val cTpositive : CoqInterface.constr lazy_t -val cTBV : CoqInterface.constr lazy_t -val cTFArray : CoqInterface.constr lazy_t -val cTindex : CoqInterface.constr lazy_t - -val cinterp_t : CoqInterface.constr lazy_t -val cdec_interp : CoqInterface.constr lazy_t -val cord_interp : CoqInterface.constr lazy_t -val ccomp_interp : CoqInterface.constr lazy_t -val cinh_interp : CoqInterface.constr lazy_t - -val cinterp_eqb : CoqInterface.constr lazy_t - -val ctyp_compdec : CoqInterface.constr lazy_t -val cTyp_compdec : CoqInterface.constr lazy_t -val cunit_typ_compdec : CoqInterface.constr lazy_t -val cte_carrier : CoqInterface.constr lazy_t -val cte_compdec : CoqInterface.constr lazy_t -val ceqb_of_compdec : CoqInterface.constr lazy_t -val cCompDec : CoqInterface.constr lazy_t - -val cbool_compdec : CoqInterface.constr lazy_t -val cZ_compdec : CoqInterface.constr lazy_t -val cPositive_compdec : CoqInterface.constr lazy_t -val cBV_compdec : CoqInterface.constr lazy_t -val cFArray_compdec : CoqInterface.constr lazy_t - -val ctval : CoqInterface.constr lazy_t -val cTval : CoqInterface.constr lazy_t - -val cCO_xH : CoqInterface.constr lazy_t -val cCO_Z0 : CoqInterface.constr lazy_t -val cCO_BV : CoqInterface.constr lazy_t - -val cUO_xO : CoqInterface.constr lazy_t -val cUO_xI : CoqInterface.constr lazy_t -val cUO_Zpos : CoqInterface.constr lazy_t -val cUO_Zneg : CoqInterface.constr lazy_t -val cUO_Zopp : CoqInterface.constr lazy_t -val cUO_BVbitOf : CoqInterface.constr lazy_t -val cUO_BVnot : CoqInterface.constr lazy_t -val cUO_BVneg : CoqInterface.constr lazy_t -val cUO_BVextr : CoqInterface.constr lazy_t -val cUO_BVzextn : CoqInterface.constr lazy_t -val cUO_BVsextn : CoqInterface.constr lazy_t - -val cBO_Zplus : CoqInterface.constr lazy_t -val cBO_Zminus : CoqInterface.constr lazy_t -val cBO_Zmult : CoqInterface.constr lazy_t -val cBO_Zlt : CoqInterface.constr lazy_t -val cBO_Zle : CoqInterface.constr lazy_t -val cBO_Zge : CoqInterface.constr lazy_t -val cBO_Zgt : CoqInterface.constr lazy_t -val cBO_eq : CoqInterface.constr lazy_t -val cBO_BVand : CoqInterface.constr lazy_t -val cBO_BVor : CoqInterface.constr lazy_t -val cBO_BVxor : CoqInterface.constr lazy_t -val cBO_BVadd : CoqInterface.constr lazy_t -val cBO_BVmult : CoqInterface.constr lazy_t -val cBO_BVult : CoqInterface.constr lazy_t -val cBO_BVslt : CoqInterface.constr lazy_t -val cBO_BVconcat : CoqInterface.constr lazy_t -val cBO_BVshl : CoqInterface.constr lazy_t -val cBO_BVshr : CoqInterface.constr lazy_t -val cBO_select : CoqInterface.constr lazy_t -val cBO_diffarray : CoqInterface.constr lazy_t - -val cTO_store : CoqInterface.constr lazy_t - -val cNO_distinct : CoqInterface.constr lazy_t - -val catom : CoqInterface.constr lazy_t -val cAcop : CoqInterface.constr lazy_t -val cAuop : CoqInterface.constr lazy_t -val cAbop : CoqInterface.constr lazy_t -val cAtop : CoqInterface.constr lazy_t -val cAnop : CoqInterface.constr lazy_t -val cAapp : CoqInterface.constr lazy_t - -val cform : CoqInterface.constr lazy_t -val cFatom : CoqInterface.constr lazy_t -val cFtrue : CoqInterface.constr lazy_t -val cFfalse : CoqInterface.constr lazy_t -val cFnot2 : CoqInterface.constr lazy_t -val cFand : CoqInterface.constr lazy_t -val cFor : CoqInterface.constr lazy_t -val cFxor : CoqInterface.constr lazy_t -val cFimp : CoqInterface.constr lazy_t -val cFiff : CoqInterface.constr lazy_t -val cFite : CoqInterface.constr lazy_t -val cFbbT : CoqInterface.constr lazy_t - -val cis_true : CoqInterface.constr lazy_t - -val cvalid_sat_checker : CoqInterface.constr lazy_t -val cinterp_var_sat_checker : CoqInterface.constr lazy_t - -val make_certif_ops : - string list list -> - CoqInterface.constr array option -> - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * - CoqInterface.constr lazy_t * CoqInterface.constr lazy_t +val cfarray : coqTerm +val cselect : coqTerm +val cstore : coqTerm +val cdiff : coqTerm +val cequalarray : coqTerm + +(* SMTCoq terms *) +val cState_C_t : coqTerm +val cState_S_t : coqTerm + +val cdistinct : coqTerm + +val ctype : coqTerm +val cTZ : coqTerm +val cTbool : coqTerm +val cTpositive : coqTerm +val cTBV : coqTerm +val cTFArray : coqTerm +val cTindex : coqTerm + +val cinterp_t : coqTerm +val cdec_interp : coqTerm +val cord_interp : coqTerm +val ccomp_interp : coqTerm +val cinh_interp : coqTerm + +val cinterp_eqb : coqTerm + +val ctval : coqTerm +val cTval : coqTerm + +val cCO_xH : coqTerm +val cCO_Z0 : coqTerm +val cCO_BV : coqTerm + +val cUO_xO : coqTerm +val cUO_xI : coqTerm +val cUO_Zpos : coqTerm +val cUO_Zneg : coqTerm +val cUO_Zopp : coqTerm +val cUO_BVbitOf : coqTerm +val cUO_BVnot : coqTerm +val cUO_BVneg : coqTerm +val cUO_BVextr : coqTerm +val cUO_BVzextn : coqTerm +val cUO_BVsextn : coqTerm + +val cBO_Zplus : coqTerm +val cBO_Zminus : coqTerm +val cBO_Zmult : coqTerm +val cBO_Zlt : coqTerm +val cBO_Zle : coqTerm +val cBO_Zge : coqTerm +val cBO_Zgt : coqTerm +val cBO_eq : coqTerm +val cBO_BVand : coqTerm +val cBO_BVor : coqTerm +val cBO_BVxor : coqTerm +val cBO_BVadd : coqTerm +val cBO_BVmult : coqTerm +val cBO_BVult : coqTerm +val cBO_BVslt : coqTerm +val cBO_BVconcat : coqTerm +val cBO_BVshl : coqTerm +val cBO_BVshr : coqTerm +val cBO_select : coqTerm +val cBO_diffarray : coqTerm + +val cTO_store : coqTerm + +val cNO_distinct : coqTerm + +val catom : coqTerm +val cAcop : coqTerm +val cAuop : coqTerm +val cAbop : coqTerm +val cAtop : coqTerm +val cAnop : coqTerm +val cAapp : coqTerm + +val cform : coqTerm +val cFatom : coqTerm +val cFtrue : coqTerm +val cFfalse : coqTerm +val cFnot2 : coqTerm +val cFand : coqTerm +val cFor : coqTerm +val cFxor : coqTerm +val cFimp : coqTerm +val cFiff : coqTerm +val cFite : coqTerm +val cFbbT : coqTerm + +(* SMTCoq Classes *) +val ctyp_compdec : coqTerm +val cTyp_compdec : coqTerm +val cte_carrier : coqTerm +val cte_compdec : coqTerm +val ceqb_of_compdec : coqTerm +val cCompDec : coqTerm + +val cunit_typ_compdec : coqTerm +val cbool_compdec : coqTerm +val cZ_compdec : coqTerm +val cPositive_compdec : coqTerm +val cBV_compdec : coqTerm +val cFArray_compdec : coqTerm + +(* SMTCoq Trace *) +type certif_ops = + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm * coqTerm * + coqTerm * coqTerm + +val csat_checker_valid : coqTerm +val csat_checker_interp_var : coqTerm +val csat_checker_Certif : coqTerm +val csat_checker_dimacs : coqTerm +val csat_checker_certif : coqTerm +val csat_checker_theorem_checker : coqTerm +val csat_checker_checker : coqTerm +val csat_checker_certif_ops : certif_ops + +val ccnf_checker_certif : coqTerm +val ccnf_checker_Certif : coqTerm +val ccnf_checker_checker_b_correct : coqTerm +val ccnf_checker_checker_b : coqTerm +val ccnf_checker_checker_eq_correct : coqTerm +val ccnf_checker_checker_eq : coqTerm +val ccnf_checker_certif_ops : certif_ops + +val ceuf_checker_Certif : coqTerm +val ceuf_checker_certif : coqTerm +val ceuf_checker_checker : coqTerm +val ceuf_checker_checker_correct : coqTerm +val ceuf_checker_checker_b_correct : coqTerm +val ceuf_checker_checker_b : coqTerm +val ceuf_checker_checker_eq_correct : coqTerm +val ceuf_checker_checker_eq : coqTerm +val ceuf_checker_checker_debug : coqTerm +val ceuf_checker_name_step : coqTerm +val ceuf_checker_Name_Res : coqTerm +val ceuf_checker_Name_Weaken : coqTerm +val ceuf_checker_Name_ImmFlatten : coqTerm +val ceuf_checker_Name_CTrue : coqTerm +val ceuf_checker_Name_CFalse : coqTerm +val ceuf_checker_Name_BuildDef : coqTerm +val ceuf_checker_Name_BuildDef2 : coqTerm +val ceuf_checker_Name_BuildProj : coqTerm +val ceuf_checker_Name_ImmBuildDef : coqTerm +val ceuf_checker_Name_ImmBuildDef2 : coqTerm +val ceuf_checker_Name_ImmBuildProj : coqTerm +val ceuf_checker_Name_EqTr : coqTerm +val ceuf_checker_Name_EqCgr : coqTerm +val ceuf_checker_Name_EqCgrP : coqTerm +val ceuf_checker_Name_LiaMicromega : coqTerm +val ceuf_checker_Name_LiaDiseq : coqTerm +val ceuf_checker_Name_SplArith : coqTerm +val ceuf_checker_Name_SplDistinctElim : coqTerm +val ceuf_checker_Name_BBVar : coqTerm +val ceuf_checker_Name_BBConst : coqTerm +val ceuf_checker_Name_BBOp : coqTerm +val ceuf_checker_Name_BBNot : coqTerm +val ceuf_checker_Name_BBNeg : coqTerm +val ceuf_checker_Name_BBAdd : coqTerm +val ceuf_checker_Name_BBConcat : coqTerm +val ceuf_checker_Name_BBMul : coqTerm +val ceuf_checker_Name_BBUlt : coqTerm +val ceuf_checker_Name_BBSlt : coqTerm +val ceuf_checker_Name_BBEq : coqTerm +val ceuf_checker_Name_BBDiseq : coqTerm +val ceuf_checker_Name_BBExtract : coqTerm +val ceuf_checker_Name_BBZextend : coqTerm +val ceuf_checker_Name_BBSextend : coqTerm +val ceuf_checker_Name_BBShl : coqTerm +val ceuf_checker_Name_BBShr : coqTerm +val ceuf_checker_Name_RowEq : coqTerm +val ceuf_checker_Name_RowNeq : coqTerm +val ceuf_checker_Name_Ext : coqTerm +val ceuf_checker_Name_Hole : coqTerm +val ceuf_checker_certif_ops : CoqInterface.constr array option -> certif_ops + (* Some constructions *) -val ceq_refl_true : CoqInterface.constr lazy_t +val ceq_refl_true : coqTerm val eq_refl_true : unit -> CoqInterface.constr val vm_cast_true_no_check : CoqInterface.constr -> CoqInterface.constr val vm_cast_true : Environ.env -> CoqInterface.constr -> CoqInterface.constr val mkNat : int -> CoqInterface.constr val mkN : int -> CoqInterface.constr val mk_bv_list : bool list -> CoqInterface.constr +val mkArray : Constr.types * Constr.t array -> Constr.t (* Reification *) val mk_bool : CoqInterface.constr -> bool diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml index 0296c88..ff648a9 100644 --- a/src/trace/satAtom.ml +++ b/src/trace/satAtom.ml @@ -51,7 +51,7 @@ module Atom = t let interp_tbl reify = - CoqInterface.mkArray (Lazy.force cbool, atom_tbl reify) + CoqTerms.mkArray (Lazy.force cbool, atom_tbl reify) let logic _ = SL.empty diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 9697882..6447ae7 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -385,7 +385,7 @@ module Op = let index, hval = destruct "destruct on a Rel: called by set in interp_tbl" op in t.(index) <- mk_Tval hval.tparams hval.tres hval.op_val in Hashtbl.iter set reify.tbl; - CoqInterface.mkArray (tval, t) + CoqTerms.mkArray (tval, t) let to_list reify = let set _ op acc = @@ -1435,7 +1435,7 @@ module Atom = let interp_tbl reify = let t = to_array reify (Lazy.force dft_atom) a_to_coq in - CoqInterface.mkArray (Lazy.force catom, t) + CoqTerms.mkArray (Lazy.force catom, t) (** Producing a Coq term corresponding to the interpretation of an atom *) diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index c610129..923874e 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -156,7 +156,7 @@ let interp_tbl reify = | _ -> Some bt in Hashtbl.filter_map_inplace set reify.tbl; - CoqInterface.mkArray (Lazy.force ctyp_compdec, t) + CoqTerms.mkArray (Lazy.force ctyp_compdec, t) let to_list reify = diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index e655a9d..82dd46f 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -18,65 +18,57 @@ open SmtTrace open SmtCertif -let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ] -let certif_ops args = CoqTerms.make_certif_ops euf_checker_modules args -let cCertif = gen_constant euf_checker_modules "Certif" -let ccertif = gen_constant euf_checker_modules "certif" -let cchecker = gen_constant euf_checker_modules "checker" -let cchecker_correct = gen_constant euf_checker_modules "checker_correct" -let cchecker_b_correct = - gen_constant euf_checker_modules "checker_b_correct" -let cchecker_b = gen_constant euf_checker_modules "checker_b" -let cchecker_eq_correct = - gen_constant euf_checker_modules "checker_eq_correct" -let cchecker_eq = gen_constant euf_checker_modules "checker_eq" -(* let csetup_checker_step_debug = - * gen_constant euf_checker_modules "setup_checker_step_debug" *) -(* let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug" *) -(* let cstep = gen_constant euf_checker_modules "step" *) -let cchecker_debug = gen_constant euf_checker_modules "checker_debug" - -let cname_step = gen_constant euf_checker_modules "name_step" - -let cName_Res = gen_constant euf_checker_modules "Name_Res" -let cName_Weaken= gen_constant euf_checker_modules "Name_Weaken" -let cName_ImmFlatten= gen_constant euf_checker_modules "Name_ImmFlatten" -let cName_CTrue= gen_constant euf_checker_modules "Name_CTrue" -let cName_CFalse = gen_constant euf_checker_modules "Name_CFalse" -let cName_BuildDef= gen_constant euf_checker_modules "Name_BuildDef" -let cName_BuildDef2= gen_constant euf_checker_modules "Name_BuildDef2" -let cName_BuildProj = gen_constant euf_checker_modules "Name_BuildProj" -let cName_ImmBuildDef= gen_constant euf_checker_modules "Name_ImmBuildDef" -let cName_ImmBuildDef2= gen_constant euf_checker_modules "Name_ImmBuildDef2" -let cName_ImmBuildProj = gen_constant euf_checker_modules "Name_ImmBuildProj" -let cName_EqTr = gen_constant euf_checker_modules "Name_EqTr" -let cName_EqCgr = gen_constant euf_checker_modules "Name_EqCgr" -let cName_EqCgrP= gen_constant euf_checker_modules "Name_EqCgrP" -let cName_LiaMicromega = gen_constant euf_checker_modules "Name_LiaMicromega" -let cName_LiaDiseq= gen_constant euf_checker_modules "Name_LiaDiseq" -let cName_SplArith= gen_constant euf_checker_modules "Name_SplArith" -let cName_SplDistinctElim = gen_constant euf_checker_modules "Name_SplDistinctElim" -let cName_BBVar= gen_constant euf_checker_modules "Name_BBVar" -let cName_BBConst= gen_constant euf_checker_modules "Name_BBConst" -let cName_BBOp= gen_constant euf_checker_modules "Name_BBOp" -let cName_BBNot= gen_constant euf_checker_modules "Name_BBNot" -let cName_BBNeg= gen_constant euf_checker_modules "Name_BBNeg" -let cName_BBAdd= gen_constant euf_checker_modules "Name_BBAdd" -let cName_BBConcat= gen_constant euf_checker_modules "Name_BBConcat" -let cName_BBMul= gen_constant euf_checker_modules "Name_BBMul" -let cName_BBUlt= gen_constant euf_checker_modules "Name_BBUlt" -let cName_BBSlt= gen_constant euf_checker_modules "Name_BBSlt" -let cName_BBEq= gen_constant euf_checker_modules "Name_BBEq" -let cName_BBDiseq= gen_constant euf_checker_modules "Name_BBDiseq" -let cName_BBExtract= gen_constant euf_checker_modules "Name_BBExtract" -let cName_BBZextend= gen_constant euf_checker_modules "Name_BBZextend" -let cName_BBSextend= gen_constant euf_checker_modules "Name_BBSextend" -let cName_BBShl= gen_constant euf_checker_modules "Name_BBShl" -let cName_BBShr= gen_constant euf_checker_modules "Name_BBShr" -let cName_RowEq= gen_constant euf_checker_modules "Name_RowEq" -let cName_RowNeq= gen_constant euf_checker_modules "Name_RowNeq" -let cName_Ext= gen_constant euf_checker_modules "Name_Ext" -let cName_Hole= gen_constant euf_checker_modules "Name_Hole" +let certif_ops = CoqTerms.ceuf_checker_certif_ops +let cCertif = CoqTerms.ceuf_checker_Certif +let ccertif = CoqTerms.ceuf_checker_certif +let cchecker = CoqTerms.ceuf_checker_checker +let cchecker_correct = CoqTerms.ceuf_checker_checker_correct +let cchecker_b_correct = CoqTerms.ceuf_checker_checker_b_correct +let cchecker_b = CoqTerms.ceuf_checker_checker_b +let cchecker_eq_correct = CoqTerms.ceuf_checker_checker_eq_correct +let cchecker_eq = CoqTerms.ceuf_checker_checker_eq +let cchecker_debug = CoqTerms.ceuf_checker_checker_debug +let cname_step = CoqTerms.ceuf_checker_name_step +let cName_Res = CoqTerms.ceuf_checker_Name_Res +let cName_Weaken = CoqTerms.ceuf_checker_Name_Weaken +let cName_ImmFlatten = CoqTerms.ceuf_checker_Name_ImmFlatten +let cName_CTrue = CoqTerms.ceuf_checker_Name_CTrue +let cName_CFalse = CoqTerms.ceuf_checker_Name_CFalse +let cName_BuildDef = CoqTerms.ceuf_checker_Name_BuildDef +let cName_BuildDef2 = CoqTerms.ceuf_checker_Name_BuildDef2 +let cName_BuildProj = CoqTerms.ceuf_checker_Name_BuildProj +let cName_ImmBuildDef = CoqTerms.ceuf_checker_Name_ImmBuildDef +let cName_ImmBuildDef2 = CoqTerms.ceuf_checker_Name_ImmBuildDef2 +let cName_ImmBuildProj = CoqTerms.ceuf_checker_Name_ImmBuildProj +let cName_EqTr = CoqTerms.ceuf_checker_Name_EqTr +let cName_EqCgr = CoqTerms.ceuf_checker_Name_EqCgr +let cName_EqCgrP = CoqTerms.ceuf_checker_Name_EqCgrP +let cName_LiaMicromega = CoqTerms.ceuf_checker_Name_LiaMicromega +let cName_LiaDiseq = CoqTerms.ceuf_checker_Name_LiaDiseq +let cName_SplArith = CoqTerms.ceuf_checker_Name_SplArith +let cName_SplDistinctElim = CoqTerms.ceuf_checker_Name_SplDistinctElim +let cName_BBVar = CoqTerms.ceuf_checker_Name_BBVar +let cName_BBConst = CoqTerms.ceuf_checker_Name_BBConst +let cName_BBOp = CoqTerms.ceuf_checker_Name_BBOp +let cName_BBNot = CoqTerms.ceuf_checker_Name_BBNot +let cName_BBNeg = CoqTerms.ceuf_checker_Name_BBNeg +let cName_BBAdd = CoqTerms.ceuf_checker_Name_BBAdd +let cName_BBConcat = CoqTerms.ceuf_checker_Name_BBConcat +let cName_BBMul = CoqTerms.ceuf_checker_Name_BBMul +let cName_BBUlt = CoqTerms.ceuf_checker_Name_BBUlt +let cName_BBSlt = CoqTerms.ceuf_checker_Name_BBSlt +let cName_BBEq = CoqTerms.ceuf_checker_Name_BBEq +let cName_BBDiseq = CoqTerms.ceuf_checker_Name_BBDiseq +let cName_BBExtract = CoqTerms.ceuf_checker_Name_BBExtract +let cName_BBZextend = CoqTerms.ceuf_checker_Name_BBZextend +let cName_BBSextend = CoqTerms.ceuf_checker_Name_BBSextend +let cName_BBShl = CoqTerms.ceuf_checker_Name_BBShl +let cName_BBShr = CoqTerms.ceuf_checker_Name_BBShr +let cName_RowEq = CoqTerms.ceuf_checker_Name_RowEq +let cName_RowNeq = CoqTerms.ceuf_checker_Name_RowNeq +let cName_Ext = CoqTerms.ceuf_checker_Name_Ext +let cName_Hole = CoqTerms.ceuf_checker_Name_Hole + (* Given an SMT-LIB2 file and a certif, build the corresponding objects *) @@ -155,13 +147,13 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - CoqInterface.mkArray (Lazy.force cint, res) in + CoqTerms.mkArray (Lazy.force cint, res) in let used_roots = let l = List.length used_roots in let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in let ce3 = CoqInterface.mkUConst roots in let _ = CoqInterface.declare_constant root ce3 in let ce3' = CoqInterface.mkUConst used_roots in @@ -217,12 +209,12 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) = let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - CoqInterface.mkArray (Lazy.force cint, res) in + CoqTerms.mkArray (Lazy.force cint, res) in let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in let theorem_proof_cast = @@ -294,12 +286,12 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) = let res = Array.make (l + 1) (mkInt 0) in let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; - mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in + mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - CoqInterface.mkArray (Lazy.force cint, res) in + CoqTerms.mkArray (Lazy.force cint, res) in let tm = CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], @@ -364,12 +356,12 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; mklApp cSome [|mklApp carray [|Lazy.force cint|]; - CoqInterface.mkArray (Lazy.force cint, res)|] in + CoqTerms.mkArray (Lazy.force cint, res)|] in let rootsCstr = let res = Array.make (List.length roots + 1) (mkInt 0) in let i = ref 0 in List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - CoqInterface.mkArray (Lazy.force cint, res) in + CoqTerms.mkArray (Lazy.force cint, res) in let tm = CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], @@ -492,14 +484,14 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * let res = Array.make (List.length roots + 1) (mkInt 0) in * let i = ref 0 in * List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots; - * CoqInterface.mkArray (Lazy.force cint, res) in + * CoqTerms.mkArray (Lazy.force cint, res) in * let cused_roots = * let l = List.length used_roots in * let res = Array.make (l + 1) (mkInt 0) in * let i = ref (l-1) in * List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; * mklApp cSome [|mklApp carray [|Lazy.force cint|]; - * CoqInterface.mkArray (Lazy.force cint, res)|] in + * CoqTerms.mkArray (Lazy.force cint, res)|] in * let ce3 = CoqInterface.mkUConst croots in * let _ = CoqInterface.declare_constant root ce3 in * let ce3' = CoqInterface.mkUConst cused_roots in diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 0a7d859..0a5f693 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -546,7 +546,7 @@ module Make (Atom:ATOM) = 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; - CoqInterface.mkArray (Lazy.force cint, cargs) + CoqTerms.mkArray (Lazy.force cint, cargs) let pf_to_coq = function | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|] @@ -586,7 +586,7 @@ module Make (Atom:ATOM) = let interp_tbl reify = let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in - (mkInt i, CoqInterface.mkArray (Lazy.force cform, t)) + (mkInt i, CoqTerms.mkArray (Lazy.force cform, t)) let nvars reify = reify.count (* Producing a Coq term corresponding to the interpretation of a formula *) diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index 7b68a26..470742a 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -383,7 +383,7 @@ let to_coq to_lit interp (cstep, l := tl | _ -> assert false done; - mklApp cRes [|mkInt (get_pos c); CoqInterface.mkArray (Lazy.force cint, args)|] + mklApp cRes [|mkInt (get_pos c); CoqTerms.mkArray (Lazy.force cint, args)|] | Other other -> begin match other with | Weaken (c',l') -> @@ -412,12 +412,12 @@ let to_coq to_lit interp (cstep, 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 CoqInterface.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force CoqInterface.micromega_coq_proofTerm|]) in + let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqTerms.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force CoqTerms.micromega_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 CoqInterface.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force CoqInterface.micromega_coq_proofTerm|]) in + let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqTerms.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force CoqTerms.micromega_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|] | BBVar res -> mklApp cBBVar [|out_c c; out_f res|] @@ -483,7 +483,7 @@ let to_coq to_lit interp (cstep, | _ -> assert false in let step = Lazy.force cstep in let def_step = - mklApp cRes [|mkInt 0; CoqInterface.mkArray (Lazy.force cint, [|mkInt 0|]) |] in + mklApp cRes [|mkInt 0; CoqTerms.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; -- cgit From 04964c70f5afd95d66fc76945e62dce773a3b3bc Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 16 Feb 2022 10:38:15 +0100 Subject: Add debugging information for uninterpreted functions --- src/trace/satAtom.ml | 2 +- src/trace/satAtom.mli | 2 +- src/trace/smtAtom.ml | 14 ++++++++------ src/trace/smtAtom.mli | 2 +- src/trace/smtForm.ml | 20 ++++++++++---------- src/trace/smtForm.mli | 2 +- 6 files changed, 22 insertions(+), 20 deletions(-) (limited to 'src/trace') diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml index ff648a9..bc59943 100644 --- a/src/trace/satAtom.ml +++ b/src/trace/satAtom.ml @@ -55,7 +55,7 @@ module Atom = let logic _ = SL.empty - let to_smt = Format.pp_print_int + let to_smt ?(debug=false) = Format.pp_print_int end diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli index 311b147..875e1ad 100644 --- a/src/trace/satAtom.mli +++ b/src/trace/satAtom.mli @@ -18,7 +18,7 @@ module Atom : sig val is_bool_type : t -> bool val is_bv_type : t -> bool - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit val logic : t -> SmtMisc.logic type reify_tbl = { diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 6447ae7..23c56e7 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -707,12 +707,12 @@ module Atom = | [] -> () - let to_smt_named ?pi:(pi=false) (fmt:Format.formatter) h = + let to_smt_named ?(debug=false) ?pi:(pi=false) (fmt:Format.formatter) h = let rec to_smt fmt h = if pi then Format.fprintf fmt "%d:" (index h); - to_smt_atom (atom h) + to_smt_atom ~debug:debug (atom h) - and to_smt_atom = function + and to_smt_atom ?(debug=false) = function | Acop (CO_BV bv) -> if List.length bv = 0 then CoqInterface.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv | Acop _ as a -> to_smt_int fmt (compute_int a) | Auop (op,h) -> to_smt_uop op h @@ -722,7 +722,9 @@ module Atom = | Aapp ((i,op),a) -> let op_smt () = (match i with - | Index index -> Format.fprintf fmt "op_%i" index + | Index index -> + (Format.fprintf fmt "op_%i" index; + if debug then Format.fprintf fmt " (aka %s)" (Pp.string_of_ppcmds (CoqInterface.pr_constr op.op_val));) | Rel_name name -> Format.fprintf fmt "%s" name); if pi then to_smt_op op in @@ -805,7 +807,7 @@ module Atom = in to_smt fmt h - let to_smt (fmt:Format.formatter) h = to_smt_named fmt h + let to_smt ?(debug=false) (fmt:Format.formatter) h = to_smt_named ~debug:debug fmt h type reify_tbl = @@ -855,7 +857,7 @@ module Atom = else ( Format.eprintf "Incorrect type: wanted %a, got %a@." SmtBtype.to_smt t SmtBtype.to_smt th; - failwith (Format.asprintf "Atom %a is not of the expected type" to_smt h) + failwith (Format.asprintf "Atom %a is not of the expected type" (to_smt ~debug:true) h) ) in diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index 27737ff..05d4042 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -119,7 +119,7 @@ module Atom : val type_of : t -> btype - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit type reify_tbl diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 0a5f693..8019f3b 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -25,7 +25,7 @@ module type ATOM = val is_bool_type : t -> bool val is_bv_type : t -> bool - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit val logic : t -> logic end @@ -173,12 +173,12 @@ module Make (Atom:ATOM) = to_smt_pform fmt hp.hval; Format.fprintf fmt ")" - and to_smt_pform fmt = function - | Fatom a -> Atom.to_smt fmt a + and to_smt_pform ?(debug=false) fmt = function + | Fatom a -> Atom.to_smt ~debug:debug fmt a | Fapp (op,args) -> to_smt_op fmt op args (* This is an intermediate object of proofs, it correspond to nothing in SMT *) | FbbT (a, l) -> - Format.fprintf fmt "(bbT %a [" Atom.to_smt a; + Format.fprintf fmt "(bbT %a [" (Atom.to_smt ~debug:debug) a; let fi = ref true in List.iter (fun f -> Format.fprintf fmt "%s%a" (if !fi then "" else "; ") @@ -296,34 +296,34 @@ module Make (Atom:ATOM) = let check pf = match pf with | Fatom ha -> if not (Atom.is_bool_type ha) then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fapp (op, args) -> (match op with | Ftrue | Ffalse -> if Array.length args <> 0 then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fnot2 _ -> if Array.length args <> 1 then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fand | For -> () | Fxor | Fimp | Fiff -> if Array.length args <> 2 then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fite -> if Array.length args <> 3 then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) | Fforall l -> () ) | FbbT (ha, l) -> if not (Atom.is_bv_type ha) then - raise (Format.eprintf "nwt: %a" to_smt_pform pf; + raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf; NotWellTyped pf) let declare reify pf = diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index 47b4123..560b9e4 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -22,7 +22,7 @@ module type ATOM = val is_bool_type : t -> bool val is_bv_type : t -> bool - val to_smt : Format.formatter -> t -> unit + val to_smt : ?debug:bool -> Format.formatter -> t -> unit val logic : t -> logic end -- cgit From 2fdaf566e83897ed46127791d731f5788c22907c Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 16 Feb 2022 17:35:44 +0100 Subject: Update copyright --- src/trace/coqTerms.ml | 2 +- src/trace/coqTerms.mli | 2 +- src/trace/satAtom.ml | 2 +- src/trace/satAtom.mli | 2 +- src/trace/smtAtom.ml | 2 +- src/trace/smtAtom.mli | 2 +- src/trace/smtBtype.ml | 2 +- src/trace/smtBtype.mli | 2 +- src/trace/smtCertif.ml | 2 +- src/trace/smtCertif.mli | 2 +- src/trace/smtCnf.ml | 2 +- src/trace/smtCnf.mli | 2 +- src/trace/smtCommands.ml | 2 +- src/trace/smtCommands.mli | 2 +- src/trace/smtForm.ml | 2 +- src/trace/smtForm.mli | 2 +- src/trace/smtMaps.ml | 2 +- src/trace/smtMaps.mli | 2 +- src/trace/smtMisc.ml | 2 +- src/trace/smtMisc.mli | 2 +- src/trace/smtTrace.ml | 2 +- src/trace/smtTrace.mli | 2 +- 22 files changed, 22 insertions(+), 22 deletions(-) (limited to 'src/trace') diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 65995b5..dcacd4b 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index 282f8f6..f62f01a 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml index 6ffd752..4a3a62d 100644 --- a/src/trace/satAtom.ml +++ b/src/trace/satAtom.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli index b6a8dea..1e14cbb 100644 --- a/src/trace/satAtom.mli +++ b/src/trace/satAtom.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 06e1472..1befbf7 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index 645a638..b430d6f 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 7c08157..71f7c14 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index ec73d21..05a8486 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index 2ea4ca8..33437bf 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli index 7da3097..ef25b1f 100644 --- a/src/trace/smtCertif.mli +++ b/src/trace/smtCertif.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml index c7601d5..ffd2c45 100644 --- a/src/trace/smtCnf.ml +++ b/src/trace/smtCnf.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCnf.mli b/src/trace/smtCnf.mli index ba9be04..b15eef7 100644 --- a/src/trace/smtCnf.mli +++ b/src/trace/smtCnf.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 9cfc7c4..d15ae68 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli index b643594..eddf576 100644 --- a/src/trace/smtCommands.mli +++ b/src/trace/smtCommands.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index a86fe8a..6f26f24 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index e3c3859..9678b4c 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtMaps.ml b/src/trace/smtMaps.ml index 8b1bc9f..df87579 100644 --- a/src/trace/smtMaps.ml +++ b/src/trace/smtMaps.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtMaps.mli b/src/trace/smtMaps.mli index 220b22a..ebbdc64 100644 --- a/src/trace/smtMaps.mli +++ b/src/trace/smtMaps.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index e4747dd..227f2ff 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index 6378627..149e377 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index 876e420..e637b5c 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli index 2c70bbc..06dc6a3 100644 --- a/src/trace/smtTrace.mli +++ b/src/trace/smtTrace.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) -- cgit