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/Misc.v | 23 ++ src/SMT_terms.v | 73 +++++ src/State.v | 5 + src/Trace.v | 121 ++++++++ src/array/FArray.v | 8 + src/bva/BVList.v | 23 ++ src/classes/SMT_classes.v | 9 + src/classes/SMT_classes_instances.v | 9 + 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 +- src/zchaff/zchaff.ml | 42 ++- 19 files changed, 983 insertions(+), 585 deletions(-) diff --git a/src/Misc.v b/src/Misc.v index ff2366a..31a7086 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -1418,6 +1418,29 @@ Lemma is_true_iff e : e = true <-> is_true e. Proof. now unfold is_true. Qed. +(* Register constants for OCaml access *) +Register distinct as SMTCoq.Misc.distinct. + +Register Int63.eqb as num.int63.eqb. +Register PArray.array as array.array.type. +Register PArray.make as array.array.make. +Register PArray.set as array.array.set. +Register Coq.Init.Datatypes.is_true as core.is_true.is_true. +Register Coq.PArith.BinPosDef.Pos.eqb as num.pos.eqb. +Register Coq.NArith.BinNat.N.of_nat as num.N.of_nat. +Register Coq.ZArith.BinInt.Z.ltb as num.Z.ltb. +Register Coq.ZArith.BinInt.Z.leb as num.Z.leb. +Register Coq.ZArith.BinInt.Z.gtb as num.Z.gtb. +Register Coq.ZArith.BinInt.Z.geb as num.Z.geb. +Register Coq.ZArith.BinInt.Z.eqb as num.Z.eqb. +Register Coq.Init.Datatypes.implb as core.bool.implb. +Register Coq.Bool.Bool.eqb as core.bool.eqb. +Register Coq.Bool.Bool.ifb as core.bool.ifb. +Register Coq.Bool.Bool.reflect as core.bool.reflect. +Register Coq.Init.Datatypes.length as core.list.length. +Register Coq.micromega.ZMicromega.ZArithProof as micromega.ZMicromega.ZArithProof. + + (* Local Variables: coq-load-path: ((rec "." "SMTCoq")) diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 585a1cc..3e6f930 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -2608,6 +2608,79 @@ End PredefinedArrays. *) +(* Register constants for OCaml access *) +Register Typ.type as SMTCoq.SMT_terms.Typ.type. +Register Typ.TFArray as SMTCoq.SMT_terms.Typ.TFArray. +Register Typ.Tindex as SMTCoq.SMT_terms.Typ.Tindex. +Register Typ.TZ as SMTCoq.SMT_terms.Typ.TZ. +Register Typ.Tbool as SMTCoq.SMT_terms.Typ.Tbool. +Register Typ.Tpositive as SMTCoq.SMT_terms.Typ.Tpositive. +Register Typ.TBV as SMTCoq.SMT_terms.Typ.TBV. +Register Typ.interp as SMTCoq.SMT_terms.Typ.interp. +Register Typ.dec_interp as SMTCoq.SMT_terms.Typ.dec_interp. +Register Typ.ord_interp as SMTCoq.SMT_terms.Typ.ord_interp. +Register Typ.comp_interp as SMTCoq.SMT_terms.Typ.comp_interp. +Register Typ.inh_interp as SMTCoq.SMT_terms.Typ.inh_interp. +Register Typ.i_eqb as SMTCoq.SMT_terms.Typ.i_eqb. +Register Atom.tval as SMTCoq.SMT_terms.Atom.tval. +Register Atom.Tval as SMTCoq.SMT_terms.Atom.Tval. +Register Atom.CO_xH as SMTCoq.SMT_terms.Atom.CO_xH. +Register Atom.CO_Z0 as SMTCoq.SMT_terms.Atom.CO_Z0. +Register Atom.CO_BV as SMTCoq.SMT_terms.Atom.CO_BV. +Register Atom.UO_xO as SMTCoq.SMT_terms.Atom.UO_xO. +Register Atom.UO_xI as SMTCoq.SMT_terms.Atom.UO_xI. +Register Atom.UO_Zpos as SMTCoq.SMT_terms.Atom.UO_Zpos. +Register Atom.UO_Zneg as SMTCoq.SMT_terms.Atom.UO_Zneg. +Register Atom.UO_Zopp as SMTCoq.SMT_terms.Atom.UO_Zopp. +Register Atom.UO_BVbitOf as SMTCoq.SMT_terms.Atom.UO_BVbitOf. +Register Atom.UO_BVnot as SMTCoq.SMT_terms.Atom.UO_BVnot. +Register Atom.UO_BVneg as SMTCoq.SMT_terms.Atom.UO_BVneg. +Register Atom.UO_BVextr as SMTCoq.SMT_terms.Atom.UO_BVextr. +Register Atom.UO_BVzextn as SMTCoq.SMT_terms.Atom.UO_BVzextn. +Register Atom.UO_BVsextn as SMTCoq.SMT_terms.Atom.UO_BVsextn. +Register Atom.BO_Zplus as SMTCoq.SMT_terms.Atom.BO_Zplus. +Register Atom.BO_Zminus as SMTCoq.SMT_terms.Atom.BO_Zminus. +Register Atom.BO_Zmult as SMTCoq.SMT_terms.Atom.BO_Zmult. +Register Atom.BO_Zlt as SMTCoq.SMT_terms.Atom.BO_Zlt. +Register Atom.BO_Zle as SMTCoq.SMT_terms.Atom.BO_Zle. +Register Atom.BO_Zge as SMTCoq.SMT_terms.Atom.BO_Zge. +Register Atom.BO_Zgt as SMTCoq.SMT_terms.Atom.BO_Zgt. +Register Atom.BO_eq as SMTCoq.SMT_terms.Atom.BO_eq. +Register Atom.BO_BVand as SMTCoq.SMT_terms.Atom.BO_BVand. +Register Atom.BO_BVor as SMTCoq.SMT_terms.Atom.BO_BVor. +Register Atom.BO_BVxor as SMTCoq.SMT_terms.Atom.BO_BVxor. +Register Atom.BO_BVadd as SMTCoq.SMT_terms.Atom.BO_BVadd. +Register Atom.BO_BVmult as SMTCoq.SMT_terms.Atom.BO_BVmult. +Register Atom.BO_BVult as SMTCoq.SMT_terms.Atom.BO_BVult. +Register Atom.BO_BVslt as SMTCoq.SMT_terms.Atom.BO_BVslt. +Register Atom.BO_BVconcat as SMTCoq.SMT_terms.Atom.BO_BVconcat. +Register Atom.BO_BVshl as SMTCoq.SMT_terms.Atom.BO_BVshl. +Register Atom.BO_BVshr as SMTCoq.SMT_terms.Atom.BO_BVshr. +Register Atom.BO_select as SMTCoq.SMT_terms.Atom.BO_select. +Register Atom.BO_diffarray as SMTCoq.SMT_terms.Atom.BO_diffarray. +Register Atom.TO_store as SMTCoq.SMT_terms.Atom.TO_store. +Register Atom.NO_distinct as SMTCoq.SMT_terms.Atom.NO_distinct. +Register Atom.atom as SMTCoq.SMT_terms.Atom.atom. +Register Atom.Acop as SMTCoq.SMT_terms.Atom.Acop. +Register Atom.Auop as SMTCoq.SMT_terms.Atom.Auop. +Register Atom.Abop as SMTCoq.SMT_terms.Atom.Abop. +Register Atom.Atop as SMTCoq.SMT_terms.Atom.Atop. +Register Atom.Anop as SMTCoq.SMT_terms.Atom.Anop. +Register Atom.Aapp as SMTCoq.SMT_terms.Atom.Aapp. +Register Form.form as SMTCoq.SMT_terms.Form.form. +Register Form.Fatom as SMTCoq.SMT_terms.Form.Fatom. +Register Form.Ftrue as SMTCoq.SMT_terms.Form.Ftrue. +Register Form.Ffalse as SMTCoq.SMT_terms.Form.Ffalse. +Register Form.Fnot2 as SMTCoq.SMT_terms.Form.Fnot2. +Register Form.Fand as SMTCoq.SMT_terms.Form.Fand. +Register Form.For as SMTCoq.SMT_terms.Form.For. +Register Form.Fxor as SMTCoq.SMT_terms.Form.Fxor. +Register Form.Fimp as SMTCoq.SMT_terms.Form.Fimp. +Register Form.Fiff as SMTCoq.SMT_terms.Form.Fiff. +Register Form.Fite as SMTCoq.SMT_terms.Form.Fite. +Register Form.FbbT as SMTCoq.SMT_terms.Form.FbbT. + + (* Local Variables: coq-load-path: ((rec "." "SMTCoq")) diff --git a/src/State.v b/src/State.v index dca62e3..baa175e 100644 --- a/src/State.v +++ b/src/State.v @@ -737,3 +737,8 @@ Module S. End S. + + +(* Register constants for OCaml access *) +Register C.t as SMTCoq.State.C.t. +Register S.t as SMTCoq.State.S.t. diff --git a/src/Trace.v b/src/Trace.v index 3f61dc7..85671f9 100644 --- a/src/Trace.v +++ b/src/Trace.v @@ -778,6 +778,127 @@ End Euf_Checker. Unset Implicit Arguments. +(* Register constants for OCaml access *) +Register Sat_Checker.valid as SMTCoq.Trace.Sat_Checker.valid. +Register Sat_Checker.interp_var as SMTCoq.Trace.Sat_Checker.interp_var. +Register Sat_Checker.Certif as SMTCoq.Trace.Sat_Checker.Certif. +Register Sat_Checker.step as SMTCoq.Trace.Sat_Checker.step. +Register Sat_Checker.Res as SMTCoq.Trace.Sat_Checker.Res. +Register Sat_Checker.dimacs as SMTCoq.Trace.Sat_Checker.dimacs. +Register Sat_Checker.certif as SMTCoq.Trace.Sat_Checker.certif. +Register Sat_Checker.theorem_checker as SMTCoq.Trace.Sat_Checker.theorem_checker. +Register Sat_Checker.checker as SMTCoq.Trace.Sat_Checker.checker. + +Register Cnf_Checker.certif as SMTCoq.Trace.Cnf_Checker.certif. +Register Cnf_Checker.Certif as SMTCoq.Trace.Cnf_Checker.Certif. +Register Cnf_Checker.checker_b_correct as SMTCoq.Trace.Cnf_Checker.checker_b_correct. +Register Cnf_Checker.checker_b as SMTCoq.Trace.Cnf_Checker.checker_b. +Register Cnf_Checker.checker_eq_correct as SMTCoq.Trace.Cnf_Checker.checker_eq_correct. +Register Cnf_Checker.checker_eq as SMTCoq.Trace.Cnf_Checker.checker_eq. +Register Cnf_Checker.step as SMTCoq.Trace.Cnf_Checker.step. +Register Cnf_Checker.Res as SMTCoq.Trace.Cnf_Checker.Res. +Register Cnf_Checker.ImmFlatten as SMTCoq.Trace.Cnf_Checker.ImmFlatten. +Register Cnf_Checker.CTrue as SMTCoq.Trace.Cnf_Checker.CTrue. +Register Cnf_Checker.CFalse as SMTCoq.Trace.Cnf_Checker.CFalse. +Register Cnf_Checker.BuildDef as SMTCoq.Trace.Cnf_Checker.BuildDef. +Register Cnf_Checker.BuildDef2 as SMTCoq.Trace.Cnf_Checker.BuildDef2. +Register Cnf_Checker.BuildProj as SMTCoq.Trace.Cnf_Checker.BuildProj. +Register Cnf_Checker.ImmBuildDef as SMTCoq.Trace.Cnf_Checker.ImmBuildDef. +Register Cnf_Checker.ImmBuildDef2 as SMTCoq.Trace.Cnf_Checker.ImmBuildDef2. +Register Cnf_Checker.ImmBuildProj as SMTCoq.Trace.Cnf_Checker.ImmBuildProj. + +Register Euf_Checker.Certif as SMTCoq.Trace.Euf_Checker.Certif. +Register Euf_Checker.certif as SMTCoq.Trace.Euf_Checker.certif. +Register Euf_Checker.checker as SMTCoq.Trace.Euf_Checker.checker. +Register Euf_Checker.checker_correct as SMTCoq.Trace.Euf_Checker.checker_correct. +Register Euf_Checker.checker_b_correct as SMTCoq.Trace.Euf_Checker.checker_b_correct. +Register Euf_Checker.checker_b as SMTCoq.Trace.Euf_Checker.checker_b. +Register Euf_Checker.checker_eq_correct as SMTCoq.Trace.Euf_Checker.checker_eq_correct. +Register Euf_Checker.checker_eq as SMTCoq.Trace.Euf_Checker.checker_eq. +Register Euf_Checker.checker_debug as SMTCoq.Trace.Euf_Checker.checker_debug. +Register Euf_Checker.name_step as SMTCoq.Trace.Euf_Checker.name_step. +Register Euf_Checker.Name_Res as SMTCoq.Trace.Euf_Checker.Name_Res. +Register Euf_Checker.Name_Weaken as SMTCoq.Trace.Euf_Checker.Name_Weaken. +Register Euf_Checker.Name_ImmFlatten as SMTCoq.Trace.Euf_Checker.Name_ImmFlatten. +Register Euf_Checker.Name_CTrue as SMTCoq.Trace.Euf_Checker.Name_CTrue. +Register Euf_Checker.Name_CFalse as SMTCoq.Trace.Euf_Checker.Name_CFalse. +Register Euf_Checker.Name_BuildDef as SMTCoq.Trace.Euf_Checker.Name_BuildDef. +Register Euf_Checker.Name_BuildDef2 as SMTCoq.Trace.Euf_Checker.Name_BuildDef2. +Register Euf_Checker.Name_BuildProj as SMTCoq.Trace.Euf_Checker.Name_BuildProj. +Register Euf_Checker.Name_ImmBuildDef as SMTCoq.Trace.Euf_Checker.Name_ImmBuildDef. +Register Euf_Checker.Name_ImmBuildDef2 as SMTCoq.Trace.Euf_Checker.Name_ImmBuildDef2. +Register Euf_Checker.Name_ImmBuildProj as SMTCoq.Trace.Euf_Checker.Name_ImmBuildProj. +Register Euf_Checker.Name_EqTr as SMTCoq.Trace.Euf_Checker.Name_EqTr. +Register Euf_Checker.Name_EqCgr as SMTCoq.Trace.Euf_Checker.Name_EqCgr. +Register Euf_Checker.Name_EqCgrP as SMTCoq.Trace.Euf_Checker.Name_EqCgrP. +Register Euf_Checker.Name_LiaMicromega as SMTCoq.Trace.Euf_Checker.Name_LiaMicromega. +Register Euf_Checker.Name_LiaDiseq as SMTCoq.Trace.Euf_Checker.Name_LiaDiseq. +Register Euf_Checker.Name_SplArith as SMTCoq.Trace.Euf_Checker.Name_SplArith. +Register Euf_Checker.Name_SplDistinctElim as SMTCoq.Trace.Euf_Checker.Name_SplDistinctElim. +Register Euf_Checker.Name_BBVar as SMTCoq.Trace.Euf_Checker.Name_BBVar. +Register Euf_Checker.Name_BBConst as SMTCoq.Trace.Euf_Checker.Name_BBConst. +Register Euf_Checker.Name_BBOp as SMTCoq.Trace.Euf_Checker.Name_BBOp. +Register Euf_Checker.Name_BBNot as SMTCoq.Trace.Euf_Checker.Name_BBNot. +Register Euf_Checker.Name_BBNeg as SMTCoq.Trace.Euf_Checker.Name_BBNeg. +Register Euf_Checker.Name_BBAdd as SMTCoq.Trace.Euf_Checker.Name_BBAdd. +Register Euf_Checker.Name_BBConcat as SMTCoq.Trace.Euf_Checker.Name_BBConcat. +Register Euf_Checker.Name_BBMul as SMTCoq.Trace.Euf_Checker.Name_BBMul. +Register Euf_Checker.Name_BBUlt as SMTCoq.Trace.Euf_Checker.Name_BBUlt. +Register Euf_Checker.Name_BBSlt as SMTCoq.Trace.Euf_Checker.Name_BBSlt. +Register Euf_Checker.Name_BBEq as SMTCoq.Trace.Euf_Checker.Name_BBEq. +Register Euf_Checker.Name_BBDiseq as SMTCoq.Trace.Euf_Checker.Name_BBDiseq. +Register Euf_Checker.Name_BBExtract as SMTCoq.Trace.Euf_Checker.Name_BBExtract. +Register Euf_Checker.Name_BBZextend as SMTCoq.Trace.Euf_Checker.Name_BBZextend. +Register Euf_Checker.Name_BBSextend as SMTCoq.Trace.Euf_Checker.Name_BBSextend. +Register Euf_Checker.Name_BBShl as SMTCoq.Trace.Euf_Checker.Name_BBShl. +Register Euf_Checker.Name_BBShr as SMTCoq.Trace.Euf_Checker.Name_BBShr. +Register Euf_Checker.Name_RowEq as SMTCoq.Trace.Euf_Checker.Name_RowEq. +Register Euf_Checker.Name_RowNeq as SMTCoq.Trace.Euf_Checker.Name_RowNeq. +Register Euf_Checker.Name_Ext as SMTCoq.Trace.Euf_Checker.Name_Ext. +Register Euf_Checker.Name_Hole as SMTCoq.Trace.Euf_Checker.Name_Hole. +Register Euf_Checker.step as SMTCoq.Trace.Euf_Checker.step. +Register Euf_Checker.Res as SMTCoq.Trace.Euf_Checker.Res. +Register Euf_Checker.Weaken as SMTCoq.Trace.Euf_Checker.Weaken. +Register Euf_Checker.ImmFlatten as SMTCoq.Trace.Euf_Checker.ImmFlatten. +Register Euf_Checker.CTrue as SMTCoq.Trace.Euf_Checker.CTrue. +Register Euf_Checker.CFalse as SMTCoq.Trace.Euf_Checker.CFalse. +Register Euf_Checker.BuildDef as SMTCoq.Trace.Euf_Checker.BuildDef. +Register Euf_Checker.BuildDef2 as SMTCoq.Trace.Euf_Checker.BuildDef2. +Register Euf_Checker.BuildProj as SMTCoq.Trace.Euf_Checker.BuildProj. +Register Euf_Checker.ImmBuildProj as SMTCoq.Trace.Euf_Checker.ImmBuildProj. +Register Euf_Checker.ImmBuildDef as SMTCoq.Trace.Euf_Checker.ImmBuildDef. +Register Euf_Checker.ImmBuildDef2 as SMTCoq.Trace.Euf_Checker.ImmBuildDef2. +Register Euf_Checker.EqTr as SMTCoq.Trace.Euf_Checker.EqTr. +Register Euf_Checker.EqCgr as SMTCoq.Trace.Euf_Checker.EqCgr. +Register Euf_Checker.EqCgrP as SMTCoq.Trace.Euf_Checker.EqCgrP. +Register Euf_Checker.LiaMicromega as SMTCoq.Trace.Euf_Checker.LiaMicromega. +Register Euf_Checker.LiaDiseq as SMTCoq.Trace.Euf_Checker.LiaDiseq. +Register Euf_Checker.SplArith as SMTCoq.Trace.Euf_Checker.SplArith. +Register Euf_Checker.SplDistinctElim as SMTCoq.Trace.Euf_Checker.SplDistinctElim. +Register Euf_Checker.BBVar as SMTCoq.Trace.Euf_Checker.BBVar. +Register Euf_Checker.BBConst as SMTCoq.Trace.Euf_Checker.BBConst. +Register Euf_Checker.BBOp as SMTCoq.Trace.Euf_Checker.BBOp. +Register Euf_Checker.BBNot as SMTCoq.Trace.Euf_Checker.BBNot. +Register Euf_Checker.BBEq as SMTCoq.Trace.Euf_Checker.BBEq. +Register Euf_Checker.BBDiseq as SMTCoq.Trace.Euf_Checker.BBDiseq. +Register Euf_Checker.BBNeg as SMTCoq.Trace.Euf_Checker.BBNeg. +Register Euf_Checker.BBAdd as SMTCoq.Trace.Euf_Checker.BBAdd. +Register Euf_Checker.BBMul as SMTCoq.Trace.Euf_Checker.BBMul. +Register Euf_Checker.BBUlt as SMTCoq.Trace.Euf_Checker.BBUlt. +Register Euf_Checker.BBSlt as SMTCoq.Trace.Euf_Checker.BBSlt. +Register Euf_Checker.BBConcat as SMTCoq.Trace.Euf_Checker.BBConcat. +Register Euf_Checker.BBExtract as SMTCoq.Trace.Euf_Checker.BBExtract. +Register Euf_Checker.BBZextend as SMTCoq.Trace.Euf_Checker.BBZextend. +Register Euf_Checker.BBSextend as SMTCoq.Trace.Euf_Checker.BBSextend. +Register Euf_Checker.BBShl as SMTCoq.Trace.Euf_Checker.BBShl. +Register Euf_Checker.BBShr as SMTCoq.Trace.Euf_Checker.BBShr. +Register Euf_Checker.RowEq as SMTCoq.Trace.Euf_Checker.RowEq. +Register Euf_Checker.RowNeq as SMTCoq.Trace.Euf_Checker.RowNeq. +Register Euf_Checker.Ext as SMTCoq.Trace.Euf_Checker.Ext. +Register Euf_Checker.Hole as SMTCoq.Trace.Euf_Checker.Hole. +Register Euf_Checker.ForallInst as SMTCoq.Trace.Euf_Checker.ForallInst. + + (* Local Variables: coq-load-path: ((rec "." "SMTCoq")) diff --git a/src/array/FArray.v b/src/array/FArray.v index 69e56f9..dfff5e8 100644 --- a/src/array/FArray.v +++ b/src/array/FArray.v @@ -1861,6 +1861,14 @@ Notation "a '[' i '<-' v ']'" := (store a i v) (at level 1, format "a [ i <- v ]") : farray_scope. +(* Register constants for OCaml access *) +Register FArray.farray as SMTCoq.array.FArray.farray. +Register select as SMTCoq.array.FArray.select. +Register store as SMTCoq.array.FArray.store. +Register diff as SMTCoq.array.FArray.diff. +Register FArray.equal as SMTCoq.array.FArray.equal. + + (* Local Variables: diff --git a/src/bva/BVList.v b/src/bva/BVList.v index f0ba8ef..d8632bb 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -2541,6 +2541,29 @@ Module BITVECTOR_LIST <: BITVECTOR. End BITVECTOR_LIST. + +(* Register constants for OCaml access *) +Register BITVECTOR_LIST.bitvector as SMTCoq.bva.BVList.BITVECTOR_LIST.bitvector. +Register BITVECTOR_LIST.of_bits as SMTCoq.bva.BVList.BITVECTOR_LIST.of_bits. +Register BITVECTOR_LIST.bitOf as SMTCoq.bva.BVList.BITVECTOR_LIST.bitOf. +Register BITVECTOR_LIST.bv_eq as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_eq. +Register BITVECTOR_LIST.bv_not as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_not. +Register BITVECTOR_LIST.bv_neg as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_neg. +Register BITVECTOR_LIST.bv_and as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_and. +Register BITVECTOR_LIST.bv_or as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_or. +Register BITVECTOR_LIST.bv_xor as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_xor. +Register BITVECTOR_LIST.bv_add as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_add. +Register BITVECTOR_LIST.bv_mult as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_mult. +Register BITVECTOR_LIST.bv_ult as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_ult. +Register BITVECTOR_LIST.bv_slt as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_slt. +Register BITVECTOR_LIST.bv_concat as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_concat. +Register BITVECTOR_LIST.bv_extr as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_extr. +Register BITVECTOR_LIST.bv_zextn as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_zextn. +Register BITVECTOR_LIST.bv_sextn as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_sextn. +Register BITVECTOR_LIST.bv_shl as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_shl. +Register BITVECTOR_LIST.bv_shr as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_shr. + + (* Local Variables: coq-load-path: ((rec ".." "SMTCoq")) diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v index 9ee394b..e1fd8e9 100644 --- a/src/classes/SMT_classes.v +++ b/src/classes/SMT_classes.v @@ -217,3 +217,12 @@ Section CompDec_from. Typ_compdec T CompDec_from. End CompDec_from. + + +(* Register constants for OCaml access *) +Register typ_compdec as SMTCoq.classes.SMT_classes.typ_compdec. +Register Typ_compdec as SMTCoq.classes.SMT_classes.Typ_compdec. +Register te_carrier as SMTCoq.classes.SMT_classes.te_carrier. +Register te_compdec as SMTCoq.classes.SMT_classes.te_compdec. +Register eqb_of_compdec as SMTCoq.classes.SMT_classes.eqb_of_compdec. +Register CompDec as SMTCoq.classes.SMT_classes.CompDec. diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index 1c8b2f6..0e51366 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -747,3 +747,12 @@ Section prod. |}. End prod. + + +(* Register constants for OCaml access *) +Register unit_typ_compdec as SMTCoq.classes.SMT_classes_instances.unit_typ_compdec. +Register bool_compdec as SMTCoq.classes.SMT_classes_instances.bool_compdec. +Register Z_compdec as SMTCoq.classes.SMT_classes_instances.Z_compdec. +Register Positive_compdec as SMTCoq.classes.SMT_classes_instances.Positive_compdec. +Register BV_compdec as SMTCoq.classes.SMT_classes_instances.BV_compdec. +Register FArray_compdec as SMTCoq.classes.SMT_classes_instances.FArray_compdec. 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; diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 1f5110b..89dd13e 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -133,7 +133,7 @@ let import_cnf_trace reloc filename first last = let make_roots first last = let cint = Lazy.force cint in - let roots = Array.make (last.id + 2) (CoqInterface.mkArray (cint, Array.make 1 (mkInt 0))) in + let roots = Array.make (last.id + 2) (CoqTerms.mkArray (cint, Array.make 1 (mkInt 0))) in let mk_elem l = let x = match Form.pform l with | Fatom x -> x + 2 @@ -144,15 +144,15 @@ let make_roots first last = let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; - roots.(!r.id) <- CoqInterface.mkArray (cint, croot); + roots.(!r.id) <- CoqTerms.mkArray (cint, croot); r := next !r done; let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; - roots.(!r.id) <- CoqInterface.mkArray (cint, croot); + roots.(!r.id) <- CoqTerms.mkArray (cint, croot); - CoqInterface.mkArray (mklApp carray [|cint|], roots) + CoqTerms.mkArray (mklApp carray [|cint|], roots) let interp_roots first last = let tbl = Hashtbl.create 17 in @@ -185,10 +185,8 @@ let interp_roots first last = end; !res -let sat_checker_modules = [ ["SMTCoq";"Trace";"Sat_Checker"] ] - -let certif_ops = CoqTerms.make_certif_ops sat_checker_modules None -let cCertif = gen_constant sat_checker_modules "Certif" +let certif_ops = CoqTerms.csat_checker_certif_ops +let cCertif = CoqTerms.csat_checker_Certif let parse_certif dimacs trace fdimacs ftrace = SmtTrace.clear (); @@ -205,10 +203,10 @@ let parse_certif dimacs trace fdimacs ftrace = let _ = CoqInterface.declare_constant trace ce2 in () -let cdimacs = gen_constant sat_checker_modules "dimacs" -let ccertif = gen_constant sat_checker_modules "certif" -let ctheorem_checker = gen_constant sat_checker_modules "theorem_checker" -let cchecker = gen_constant sat_checker_modules "checker" +let cdimacs = CoqTerms.csat_checker_dimacs +let ccertif = CoqTerms.csat_checker_certif +let ctheorem_checker = CoqTerms.csat_checker_theorem_checker +let cchecker = CoqTerms.csat_checker_checker let theorems interp name fdimacs ftrace = SmtTrace.clear (); @@ -251,7 +249,7 @@ let theorems interp name fdimacs ftrace = let theorem = theorems (fun _ -> interp_roots) let theorem_abs = - theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|CoqInterface.mkRel 1(*v*)|]; d|]) + theorems (fun d _ _ -> mklApp csat_checker_valid [|mklApp csat_checker_interp_var [|CoqInterface.mkRel 1(*v*)|]; d|]) let checker fdimacs ftrace = @@ -345,17 +343,13 @@ let call_zchaff nvars root = (* Build the problem that it may be understoof by zchaff *) -let cnf_checker_modules = [ ["SMTCoq";"Trace";"Cnf_Checker"] ] - -let certif_ops = CoqTerms.make_certif_ops cnf_checker_modules None -let ccertif = gen_constant cnf_checker_modules "certif" -let cCertif = gen_constant cnf_checker_modules "Certif" -let cchecker_b_correct = - gen_constant cnf_checker_modules "checker_b_correct" -let cchecker_b = gen_constant cnf_checker_modules "checker_b" -let cchecker_eq_correct = - gen_constant cnf_checker_modules "checker_eq_correct" -let cchecker_eq = gen_constant cnf_checker_modules "checker_eq" +let certif_ops = CoqTerms.ccnf_checker_certif_ops +let ccertif = CoqTerms.ccnf_checker_certif +let cCertif = CoqTerms.ccnf_checker_Certif +let cchecker_b_correct = CoqTerms.ccnf_checker_checker_b_correct +let cchecker_b = CoqTerms.ccnf_checker_checker_b +let cchecker_eq_correct = CoqTerms.ccnf_checker_checker_eq_correct +let cchecker_eq = CoqTerms.ccnf_checker_checker_eq let build_body reify_atom reify_form l b (max_id, confl) vm_cast = let ntvar = CoqInterface.mkName "t_var" in -- cgit