diff options
-rw-r--r-- | src/extraction/Makefile | 11 | ||||
-rw-r--r-- | src/extraction/smtcoq.mli | 5 | ||||
-rw-r--r-- | src/extraction/test.mli | 1 | ||||
-rw-r--r-- | src/extraction/verit_checker.mli | 45 | ||||
-rw-r--r-- | src/extraction/zchaff_checker.mli | 13 | ||||
-rw-r--r-- | src/lia/lia.mli | 59 | ||||
-rw-r--r-- | src/smtlib2/smtlib2_ast.mli | 79 | ||||
-rw-r--r-- | src/smtlib2/smtlib2_genConstr.mli | 34 | ||||
-rw-r--r-- | src/smtlib2/smtlib2_util.mli | 8 | ||||
-rw-r--r-- | src/trace/coqTerms.mli | 112 | ||||
-rw-r--r-- | src/trace/satAtom.mli | 112 | ||||
-rw-r--r-- | src/trace/smtCertif.mli | 42 | ||||
-rw-r--r-- | src/trace/smtCnf.mli | 25 | ||||
-rw-r--r-- | src/trace/smtCommands.mli | 92 | ||||
-rw-r--r-- | src/trace/smtMisc.mli | 7 | ||||
-rw-r--r-- | src/trace/smtTrace.mli | 81 | ||||
-rw-r--r-- | src/verit/verit.mli | 31 | ||||
-rw-r--r-- | src/versions/native/Make | 21 | ||||
-rw-r--r-- | src/versions/native/Makefile | 25 | ||||
-rw-r--r-- | src/versions/native/structures.mli | 40 | ||||
-rw-r--r-- | src/zchaff/cnfParser.mli | 13 | ||||
-rw-r--r-- | src/zchaff/satParser.mli | 33 | ||||
-rw-r--r-- | src/zchaff/zchaff.mli | 88 | ||||
-rw-r--r-- | src/zchaff/zchaffParser.mli | 36 |
24 files changed, 1007 insertions, 6 deletions
diff --git a/src/extraction/Makefile b/src/extraction/Makefile index 043afa1..73b0ae4 100644 --- a/src/extraction/Makefile +++ b/src/extraction/Makefile @@ -1,6 +1,6 @@ # List of user's files and name of the final program (edit this part) -USERFILES=smtcoq.ml +USERFILES=smtcoq.ml smtcoq.mli PROGRAM=smtcoq # USERFILES=test.ml # PROGRAM=test @@ -19,9 +19,12 @@ SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../ COQLIB=-I ${COQTOP}kernel -I ${COQTOP}lib -I ${COQTOP}library -I ${COQTOP}parsing -I ${COQTOP}pretyping -I ${COQTOP}interp -I ${COQTOP}proofs -I ${COQTOP}tactics -I ${COQTOP}toplevel -I ${COQTOP}plugins/btauto -I ${COQTOP}plugins/cc -I ${COQTOP}plugins/decl_mode -I ${COQTOP}plugins/extraction -I ${COQTOP}plugins/field -I ${COQTOP}plugins/firstorder -I ${COQTOP}plugins/fourier -I ${COQTOP}plugins/funind -I ${COQTOP}plugins/micromega -I ${COQTOP}plugins/nsatz -I ${COQTOP}plugins/omega -I ${COQTOP}plugins/quote -I ${COQTOP}plugins/ring -I ${COQTOP}plugins/romega -I ${COQTOP}plugins/rtauto -I ${COQTOP}plugins/setoid_ring -I ${COQTOP}plugins/syntax -I ${COQTOP}plugins/xml -I /usr/lib/ocaml/camlp5 CMXA=nums.cmxa str.cmxa unix.cmxa gramlib.cmxa dynlink.cmxa ${COQTOP}kernel/byterun/coq_fix_code.o ${COQTOP}kernel/byterun/coq_interp.o ${COQTOP}kernel/byterun/coq_memory.o ${COQTOP}kernel/byterun/coq_values.o clib.cmxa lib.cmxa kernel.cmxa library.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa tactics.cmxa toplevel.cmxa micromega_plugin.cmxa smtcoq.cmxa -CMI=extrNative.cmi sat_checker.cmi smt_checker.cmi +CMI=extrNative.cmi sat_checker.cmi zchaff_checker.cmi smt_checker.cmi verit_checker.cmi CMX=extrNative.cmx sat_checker.cmx zchaff_checker.cmx smt_checker.cmx verit_checker.cmx -USERCMX=$(USERFILES:.ml=.cmx) +USERML=$(filter %.ml,$(USERFILES)) +USERCMX=$(USERML:%.ml=%.cmx) +USERMLI=$(filter %.mli,$(USERFILES)) +USERCMI=$(USERMLI:%.mli=%.cmi) OCAMLC=ocamlc OCAMLOPT=ocamlopt @@ -35,7 +38,7 @@ all: $(PROGRAM) %.cmx: %.ml $(OCAMLOPT) -c $(FLAGS) $(SMTLIB) $(COQLIB) $< -$(PROGRAM): $(CMI) $(CMX) $(USERCMX) +$(PROGRAM): $(CMI) $(CMX) $(USERCMI) $(USERCMX) $(OCAMLOPT) $(FLAGS) $(SMTLIB) $(COQLIB) -o $@ $(COMPILEFLAGS) $(CMXA) $(CMX) $(USERCMX) diff --git a/src/extraction/smtcoq.mli b/src/extraction/smtcoq.mli new file mode 100644 index 0000000..7b33e0f --- /dev/null +++ b/src/extraction/smtcoq.mli @@ -0,0 +1,5 @@ +type solver = Zchaff | Verit +val usage : string +val string_of_solver : solver -> string +val verifier_of_solver : solver -> string -> string -> bool +val run : solver -> string -> string -> unit diff --git a/src/extraction/test.mli b/src/extraction/test.mli new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/src/extraction/test.mli @@ -0,0 +1 @@ + diff --git a/src/extraction/verit_checker.mli b/src/extraction/verit_checker.mli new file mode 100644 index 0000000..3c43d22 --- /dev/null +++ b/src/extraction/verit_checker.mli @@ -0,0 +1,45 @@ +module Mc = Structures.Micromega_plugin_Certificate.Mc +val mkInt : int -> ExtrNative.uint +val mkArray : 'a array -> 'a ExtrNative.parray +val dump_nat : Mc.nat -> Smt_checker.nat +val dump_positive : Mc.positive -> Smt_checker.positive +val dump_z : Mc.z -> Smt_checker.z +val dump_pol : Mc.z Mc.pol -> Smt_checker.z Smt_checker.pol +val dump_psatz : Mc.z Mc.psatz -> Smt_checker.z Smt_checker.psatz +val dump_list : ('a -> 'b) -> 'a list -> 'b Smt_checker.list +val dump_proof_term : Micromega.zArithProof -> Smt_checker.zArithProof +val to_coq : + ('a -> Smt_checker.int) -> + 'a SmtCertif.clause -> + Smt_checker.Euf_Checker.step ExtrNative.parray ExtrNative.parray * + 'a SmtCertif.clause +val btype_to_coq : SmtAtom.btype -> Smt_checker.Typ.coq_type +val c_to_coq : SmtAtom.cop -> Smt_checker.Atom.cop +val u_to_coq : SmtAtom.uop -> Smt_checker.Atom.unop +val b_to_coq : SmtAtom.bop -> Smt_checker.Atom.binop +val n_to_coq : SmtAtom.nop -> Smt_checker.Typ.coq_type +val i_to_coq : SmtAtom.indexed_op -> ExtrNative.uint +val a_to_coq : SmtAtom.atom -> Smt_checker.Atom.atom +val atom_interp_tbl : + SmtAtom.Atom.reify_tbl -> Smt_checker.Atom.atom ExtrNative.parray +val form_to_coq : SmtAtom.Form.t -> ExtrNative.uint +val args_to_coq : SmtAtom.Form.t array -> ExtrNative.uint ExtrNative.parray +val pf_to_coq : + (SmtAtom.hatom, SmtAtom.Form.t) SmtForm.gen_pform -> Smt_checker.Form.form +val form_interp_tbl : + SmtAtom.Form.reify -> Smt_checker.Form.form ExtrNative.parray +val count_btype : int ref +val count_op : int ref +val declare_sort : Smtlib2_ast.symbol -> SmtAtom.btype +val declare_fun : + Smtlib2_ast.symbol -> + Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op +val declare_commands : + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> + SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list +val import_smtlib2 : + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> string -> SmtAtom.Form.t list +val this_clear_all : unit -> unit +val checker : string -> string -> bool diff --git a/src/extraction/zchaff_checker.mli b/src/extraction/zchaff_checker.mli new file mode 100644 index 0000000..d24a1e3 --- /dev/null +++ b/src/extraction/zchaff_checker.mli @@ -0,0 +1,13 @@ +val mkInt : int -> ExtrNative.uint +val mkArray : 'a array -> 'a ExtrNative.parray +val make_roots : + SatAtom.Form.t SmtCertif.clause -> + 'a SmtCertif.clause -> ExtrNative.uint ExtrNative.parray ExtrNative.parray +val to_coq : + 'a -> + 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n * 'o * 'p * + 'q * 'r * 's * 't -> + 'u SmtCertif.clause -> + Sat_checker.Sat_Checker.step ExtrNative.parray ExtrNative.parray * + 'u SmtCertif.clause +val checker : string -> string -> bool diff --git a/src/lia/lia.mli b/src/lia/lia.mli new file mode 100644 index 0000000..bb5587f --- /dev/null +++ b/src/lia/lia.mli @@ -0,0 +1,59 @@ +val pos_of_int : int -> Structures.Micromega_plugin_Micromega.positive +val z_of_int : int -> Structures.Micromega_plugin_Micromega.z +type my_tbl = { tbl : (SmtAtom.hatom, int) Hashtbl.t; mutable count : int; } +val get_atom_var : my_tbl -> SmtAtom.hatom -> int +val create_tbl : int -> my_tbl +val smt_Atom_to_micromega_pos : + SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.positive +val smt_Atom_to_micromega_Z : + SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.z +val smt_Atom_to_micromega_pExpr : + my_tbl -> + SmtAtom.hatom -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Micromega.pExpr +val smt_binop_to_micromega_formula : + my_tbl -> + SmtAtom.bop -> + SmtAtom.hatom -> + SmtAtom.hatom -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Micromega.formula +val smt_Atom_to_micromega_formula : + my_tbl -> + SmtAtom.hatom -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Micromega.formula +val default_constr : Term.constr +val default_tag : Structures.Micromega_plugin_Mutils.Tag.t +val binop_array : + ('a -> 'b -> 'c) -> 'a -> ('c -> 'c -> 'c) -> 'c -> 'b array -> 'c +val smt_Form_to_coq_micromega_formula : + my_tbl -> + SmtAtom.Form.t -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Coq_micromega.formula +val binop_list : + my_tbl -> + (Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Coq_micromega.formula -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Coq_micromega.formula -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Coq_micromega.formula) -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Coq_micromega.formula -> + SmtAtom.Form.t list -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Coq_micromega.formula +val smt_clause_to_coq_micromega_formula : + my_tbl -> + SmtAtom.Form.t list -> + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Coq_micromega.formula +val build_lia_certif : + SmtAtom.Form.t list -> + my_tbl * + Structures.Micromega_plugin_Micromega.z + Structures.Micromega_plugin_Coq_micromega.formula * + Certificate.Mc.zArithProof list option diff --git a/src/smtlib2/smtlib2_ast.mli b/src/smtlib2/smtlib2_ast.mli new file mode 100644 index 0000000..4fb1280 --- /dev/null +++ b/src/smtlib2/smtlib2_ast.mli @@ -0,0 +1,79 @@ +type loc = Lexing.position * Lexing.position +type specconstant = + SpecConstsDec of loc * string + | SpecConstNum of loc * string + | SpecConstString of loc * string + | SpecConstsHex of loc * string + | SpecConstsBinary of loc * string +type symbol = Symbol of loc * string | SymbolWithOr of loc * string +type sexpr = + SexprSpecConst of loc * specconstant + | SexprSymbol of loc * symbol + | SexprKeyword of loc * string + | SexprInParen of loc * (loc * sexpr list) +type attributevalue = + AttributeValSpecConst of loc * specconstant + | AttributeValSymbol of loc * symbol + | AttributeValSexpr of loc * (loc * sexpr list) +type attribute = + AttributeKeyword of loc * string + | AttributeKeywordValue of loc * string * attributevalue +type an_option = AnOptionAttribute of loc * attribute +type infoflag = InfoFlagKeyword of loc * string +type identifier = + IdSymbol of loc * symbol + | IdUnderscoreSymNum of loc * symbol * (loc * string list) +type sort = + SortIdentifier of loc * identifier + | SortIdSortMulti of loc * identifier * (loc * sort list) +type qualidentifier = + QualIdentifierId of loc * identifier + | QualIdentifierAs of loc * identifier * sort +type sortedvar = SortedVarSymSort of loc * symbol * sort +type varbinding = VarBindingSymTerm of loc * symbol * term +and term = + TermSpecConst of loc * specconstant + | TermQualIdentifier of loc * qualidentifier + | TermQualIdTerm of loc * qualidentifier * (loc * term list) + | TermLetTerm of loc * (loc * varbinding list) * term + | TermForAllTerm of loc * (loc * sortedvar list) * term + | TermExistsTerm of loc * (loc * sortedvar list) * term + | TermExclimationPt of loc * term * (loc * attribute list) +type command = + CSetLogic of loc * symbol + | CSetOption of loc * an_option + | CSetInfo of loc * attribute + | CDeclareSort of loc * symbol * string + | CDefineSort of loc * symbol * (loc * symbol list) * sort + | CDeclareFun of loc * symbol * (loc * sort list) * sort + | CDefineFun of loc * symbol * (loc * sortedvar list) * sort * term + | CPush of loc * string + | CPop of loc * string + | CAssert of loc * term + | CCheckSat of loc + | CGetAssert of loc + | CGetProof of loc + | CGetUnsatCore of loc + | CGetValue of loc * (loc * term list) + | CGetAssign of loc + | CGetOption of loc * string + | CGetInfo of loc * infoflag + | CExit of loc +type commands = Commands of loc * (loc * command list) +val loc_an_option : an_option -> loc +val loc_attribute : attribute -> loc +val loc_attributevalue : attributevalue -> loc +val loc_command : command -> loc +val loc_commands : commands -> loc +val loc_identifier : identifier -> loc +val loc_infoflag : infoflag -> loc +val loc_qualidentifier : qualidentifier -> loc +val loc_sexpr : sexpr -> loc +val loc_sort : sort -> loc +val loc_sortedvar : sortedvar -> loc +val loc_specconstant : specconstant -> loc +val loc_symbol : symbol -> loc +val loc_term : term -> loc +val loc_varbinding : varbinding -> loc +val loc_couple : 'a * 'b -> 'a +val loc_of : commands -> loc diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli new file mode 100644 index 0000000..ba69741 --- /dev/null +++ b/src/smtlib2/smtlib2_genConstr.mli @@ -0,0 +1,34 @@ +val pp_symbol : Smtlib2_ast.symbol -> string +val string_of_symbol : Smtlib2_ast.symbol -> string +val identifier_of_qualidentifier : + Smtlib2_ast.qualidentifier -> Smtlib2_ast.identifier +val string_type : string -> SmtAtom.btype +val sort_of_string : string -> SmtAtom.btype * 'a list +val sort_of_symbol : Smtlib2_ast.symbol -> SmtAtom.btype * 'a list +val string_of_identifier : Smtlib2_ast.identifier -> string +val string_of_qualidentifier : Smtlib2_ast.qualidentifier -> string +val sort_of_sort : Smtlib2_ast.sort -> (SmtAtom.btype * 'a list as 'a) +val declare_sort : + SmtAtom.Btype.reify_tbl -> Smtlib2_ast.symbol -> SmtAtom.btype +val declare_fun : + SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + Smtlib2_ast.symbol -> + Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op +val make_root_specconstant : + SmtAtom.Atom.reify_tbl -> Smtlib2_ast.specconstant -> SmtAtom.hatom +type atom_form = Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t +val make_root : + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> Smtlib2_ast.term -> SmtAtom.Form.t +val declare_commands : + SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> + SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list +val import_smtlib2 : + SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> string -> SmtAtom.Form.t list diff --git a/src/smtlib2/smtlib2_util.mli b/src/smtlib2/smtlib2_util.mli new file mode 100644 index 0000000..8afbce3 --- /dev/null +++ b/src/smtlib2/smtlib2_util.mli @@ -0,0 +1,8 @@ +type extradata = unit +val initial_data : unit -> unit +val file : string ref +val line : int ref +type pos = int +val string_of_pos : int -> string +val cur_pd : unit -> int * unit +type pd = pos * extradata diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli new file mode 100644 index 0000000..8fd166e --- /dev/null +++ b/src/trace/coqTerms.mli @@ -0,0 +1,112 @@ +val gen_constant : string list list -> string -> Term.constr lazy_t +val cint : Term.constr lazy_t +val ceq63 : Term.constr lazy_t +val carray : Term.constr lazy_t +val positive_modules : string list list +val cpositive : Term.constr lazy_t +val cxI : Term.constr lazy_t +val cxO : Term.constr lazy_t +val cxH : Term.constr lazy_t +val ceqbP : Term.constr lazy_t +val z_modules : string list list +val cZ : Term.constr lazy_t +val cZ0 : Term.constr lazy_t +val cZpos : Term.constr lazy_t +val cZneg : Term.constr lazy_t +val copp : Term.constr lazy_t +val cadd : Term.constr lazy_t +val csub : Term.constr lazy_t +val cmul : Term.constr lazy_t +val cltb : Term.constr lazy_t +val cleb : Term.constr lazy_t +val cgeb : Term.constr lazy_t +val cgtb : Term.constr lazy_t +val ceqbZ : Term.constr lazy_t +val bool_modules : string list list +val cbool : Term.constr lazy_t +val ctrue : Term.constr lazy_t +val cfalse : Term.constr lazy_t +val candb : Term.constr lazy_t +val corb : Term.constr lazy_t +val cxorb : Term.constr lazy_t +val cnegb : Term.constr lazy_t +val cimplb : Term.constr lazy_t +val ceqb : Term.constr lazy_t +val cifb : Term.constr lazy_t +val creflect : Term.constr lazy_t +val clist : Term.constr lazy_t +val cnil : Term.constr lazy_t +val ccons : Term.constr lazy_t +val coption : Term.constr lazy_t +val cSome : Term.constr lazy_t +val cNone : Term.constr lazy_t +val cpair : Term.constr lazy_t +val csigT : Term.constr lazy_t +val cnot : Term.constr lazy_t +val ceq : Term.constr lazy_t +val crefl_equal : Term.constr lazy_t +val smt_modules : string list list +val cState_C_t : Term.constr lazy_t +val cdistinct : Term.constr lazy_t +val ctype : Term.constr lazy_t +val cTZ : Term.constr lazy_t +val cTbool : Term.constr lazy_t +val cTpositive : Term.constr lazy_t +val cTindex : Term.constr lazy_t +val ctyp_eqb : Term.constr lazy_t +val cTyp_eqb : Term.constr lazy_t +val cte_carrier : Term.constr lazy_t +val cte_eqb : Term.constr lazy_t +val ctyp_eqb_of_typ_eqb_param : Term.constr lazy_t +val cunit_typ_eqb : Term.constr lazy_t +val ctval : Term.constr lazy_t +val cTval : Term.constr lazy_t +val cCO_xH : Term.constr lazy_t +val cCO_Z0 : Term.constr lazy_t +val cUO_xO : Term.constr lazy_t +val cUO_xI : Term.constr lazy_t +val cUO_Zpos : Term.constr lazy_t +val cUO_Zneg : Term.constr lazy_t +val cUO_Zopp : Term.constr lazy_t +val cBO_Zplus : Term.constr lazy_t +val cBO_Zminus : Term.constr lazy_t +val cBO_Zmult : Term.constr lazy_t +val cBO_Zlt : Term.constr lazy_t +val cBO_Zle : Term.constr lazy_t +val cBO_Zge : Term.constr lazy_t +val cBO_Zgt : Term.constr lazy_t +val cBO_eq : Term.constr lazy_t +val cNO_distinct : Term.constr lazy_t +val catom : Term.constr lazy_t +val cAcop : Term.constr lazy_t +val cAuop : Term.constr lazy_t +val cAbop : Term.constr lazy_t +val cAnop : Term.constr lazy_t +val cAapp : Term.constr lazy_t +val cform : Term.constr lazy_t +val cFatom : Term.constr lazy_t +val cFtrue : Term.constr lazy_t +val cFfalse : Term.constr lazy_t +val cFnot2 : Term.constr lazy_t +val cFand : Term.constr lazy_t +val cFor : Term.constr lazy_t +val cFxor : Term.constr lazy_t +val cFimp : Term.constr lazy_t +val cFiff : Term.constr lazy_t +val cFite : Term.constr lazy_t +val cis_true : Term.constr lazy_t +val cvalid_sat_checker : Term.constr lazy_t +val cinterp_var_sat_checker : Term.constr lazy_t +val make_certif_ops : + string list list -> + Term.constr array option -> + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t +val ceq_refl_true : Term.constr lazy_t +val eq_refl_true : unit -> Term.constr +val vm_cast_true : Term.constr -> Term.constr diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli new file mode 100644 index 0000000..5d4201b --- /dev/null +++ b/src/trace/satAtom.mli @@ -0,0 +1,112 @@ +module Atom : + sig + type t = int + val index : 'a -> 'a + val equal : 'a -> 'a -> bool + val is_bool_type : 'a -> bool + type reify_tbl = { + mutable count : int; + tbl : (Term.constr, int) Hashtbl.t; + } + val create : unit -> reify_tbl + val declare : reify_tbl -> Term.constr -> int + val get : reify_tbl -> Term.constr -> int + val atom_tbl : reify_tbl -> Term.constr array + val interp_tbl : reify_tbl -> Term.constr + end +module Form : + sig + type hatom = Atom.t + type t = SmtForm.Make(Atom).t + type pform = (hatom, t) SmtForm.gen_pform + val pform_true : pform + val pform_false : pform + val equal : t -> t -> bool + val to_lit : t -> int + val index : t -> int + val pform : t -> pform + val neg : t -> t + val is_pos : t -> bool + val is_neg : t -> bool + val to_smt : + (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit + exception NotWellTyped of pform + type reify = SmtForm.Make(Atom).reify + val create : unit -> reify + val clear : reify -> unit + val get : reify -> pform -> t + val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t + val flatten : reify -> t -> t + val to_coq : t -> Term.constr + val pform_tbl : reify -> pform array + val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array + val interp_tbl : reify -> Term.constr * Term.constr + val nvars : reify -> int + val interp_to_coq : + (hatom -> Term.constr) -> + (int, Term.constr) Hashtbl.t -> t -> Term.constr + end +module Trace : + sig + val share_value : Form.t SmtCertif.clause -> unit + module HashedHeadRes : + sig + type t = Form.t SmtCertif.resolution + val equal : + 'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool + val hash : 'a SmtCertif.resolution -> int + end + module HRtbl : + sig + type key = HashedHeadRes.t + type 'a t = 'a Hashtbl.Make(HashedHeadRes).t + val create : int -> 'a t + val clear : 'a t -> unit + val reset : 'a t -> unit + val copy : 'a t -> 'a t + val add : 'a t -> key -> 'a -> unit + val remove : 'a t -> key -> unit + val find : 'a t -> key -> 'a + val find_all : 'a t -> key -> 'a list + val replace : 'a t -> key -> 'a -> unit + val mem : 'a t -> key -> bool + val iter : (key -> 'a -> unit) -> 'a t -> unit + val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + val length : 'a t -> int + val stats : 'a t -> Hashtbl.statistics + end + val common_head : + 'a SmtCertif.clause list -> + 'b SmtCertif.clause list -> + 'a SmtCertif.clause list * 'a SmtCertif.clause list * + 'b SmtCertif.clause list + val share_prefix : Form.t SmtCertif.clause -> int -> unit + end +module Cnf : + sig + type form_info = + SmtCnf.MakeCnf(Form).form_info = + Immediate of bool + | Done + | Todo + val info : (int, form_info) Hashtbl.t + val init_last : Form.t SmtCertif.clause + val last : Form.t SmtCertif.clause ref + val cnf_todo : Form.t array list ref + val clear : unit -> unit + val push_cnf : Form.t array -> unit + val get_info : Form.t -> form_info + val set_done : Form.t -> unit + val set_immediate : Form.t -> unit + val test_immediate : Form.t -> bool + val check_trivial : Form.t list -> bool + val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit + val both_lit : Form.t -> Form.t * Form.t + val or_of_imp : Form.t array -> Form.t array + val cnf : Form.t -> unit + exception Cnf_done + val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit + val imm_cnf : Form.t SmtCertif.clause -> unit + val make_cnf : + Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause + end diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli new file mode 100644 index 0000000..dee465c --- /dev/null +++ b/src/trace/smtCertif.mli @@ -0,0 +1,42 @@ +type used = int +type clause_id = int +type 'hform rule = + ImmFlatten of 'hform clause * 'hform + | True + | False + | BuildDef of 'hform + | BuildDef2 of 'hform + | BuildProj of 'hform * int + | ImmBuildDef of 'hform clause + | ImmBuildDef2 of 'hform clause + | ImmBuildProj of 'hform clause * int + | EqTr of 'hform * 'hform list + | EqCgr of 'hform * 'hform option list + | EqCgrP of 'hform * 'hform * 'hform option list + | LiaMicromega of 'hform list * + Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | LiaDiseq of 'hform + | SplArith of 'hform clause * 'hform * + Structures.Micromega_plugin_Certificate.Mc.zArithProof list + | SplDistinctElim of 'hform clause * 'hform + | Hole of 'hform clause list * 'hform list +and 'hform clause = { + id : clause_id; + mutable kind : 'hform clause_kind; + mutable pos : int option; + mutable used : used; + mutable prev : 'hform clause option; + mutable next : 'hform clause option; + value : 'hform list option; +} +and 'hform clause_kind = + Root + | Same of 'hform clause + | Res of 'hform resolution + | Other of 'hform rule +and 'hform resolution = { + mutable rc1 : 'hform clause; + mutable rc2 : 'hform clause; + mutable rtail : 'hform clause list; +} +val used_clauses : 'a rule -> 'a clause list diff --git a/src/trace/smtCnf.mli b/src/trace/smtCnf.mli new file mode 100644 index 0000000..47fbd8c --- /dev/null +++ b/src/trace/smtCnf.mli @@ -0,0 +1,25 @@ +module MakeCnf : + functor (Form : SmtForm.FORM) -> + sig + type form_info = Immediate of bool | Done | Todo + val info : (int, form_info) Hashtbl.t + val init_last : Form.t SmtCertif.clause + val last : Form.t SmtCertif.clause ref + val cnf_todo : Form.t array list ref + val clear : unit -> unit + val push_cnf : Form.t array -> unit + val get_info : Form.t -> form_info + val set_done : Form.t -> unit + val set_immediate : Form.t -> unit + val test_immediate : Form.t -> bool + val check_trivial : Form.t list -> bool + val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit + val both_lit : Form.t -> Form.t * Form.t + val or_of_imp : Form.t array -> Form.t array + val cnf : Form.t -> unit + exception Cnf_done + val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit + val imm_cnf : Form.t SmtCertif.clause -> unit + val make_cnf : + Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause + end diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli new file mode 100644 index 0000000..b90e3ff --- /dev/null +++ b/src/trace/smtCommands.mli @@ -0,0 +1,92 @@ +val euf_checker_modules : string list list +val certif_ops : + Term.constr array option -> + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t +val cCertif : Term.constr lazy_t +val ccertif : Term.constr lazy_t +val cchecker : Term.constr lazy_t +val cchecker_correct : Term.constr lazy_t +val cchecker_b_correct : Term.constr lazy_t +val cchecker_b : Term.constr lazy_t +val cchecker_eq_correct : Term.constr lazy_t +val cchecker_eq : Term.constr lazy_t +val compute_roots : + SmtAtom.Form.t list -> SmtAtom.Form.t SmtCertif.clause -> int list +val interp_uf : + (int, Term.constr) Hashtbl.t -> + (int, Term.constr) Hashtbl.t -> SmtAtom.Form.t list -> Term.constr +val interp_conseq_uf : + SmtAtom.Form.t list list * SmtAtom.Form.t list -> Term.types +val print_assm : Term.constr -> unit +val parse_certif : + Names.identifier -> + Names.identifier -> + Names.identifier -> + Names.identifier -> + Names.identifier -> + Names.identifier -> + Names.identifier -> + SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * + SmtAtom.Form.reify * SmtAtom.Form.t list * int * + SmtAtom.Form.t SmtCertif.clause -> unit +val interp_roots : SmtAtom.Form.t list -> Term.constr +val theorem : + Names.identifier -> + SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * + SmtAtom.Form.reify * SmtAtom.Form.t list * int * + SmtAtom.Form.t SmtCertif.clause -> unit +val checker : + SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * + SmtAtom.Form.reify * SmtAtom.Form.t list * int * + SmtAtom.Form.t SmtCertif.clause -> unit +val build_body : + SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> + Term.constr -> + Term.constr -> + int * SmtAtom.Form.t SmtCertif.clause -> + Term.constr * Term.constr * (Names.identifier * Term.types) list +val build_body_eq : + SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> + Term.constr -> + Term.constr -> + Term.constr -> + int * SmtAtom.Form.t SmtCertif.clause -> + Term.constr * Term.constr * (Names.identifier * Term.types) list +val get_arguments : Term.constr -> Term.constr * Term.constr +val make_proof : + ('a -> + 'b -> + SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) -> + 'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c +val core_tactic : + (SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Form.t -> + SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> + int * SmtAtom.Form.t SmtCertif.clause) -> + SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> + Environ.env -> Evd.evar_map -> Term.constr -> Proof_type.tactic +val tactic : + (SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Form.t -> + SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> + int * SmtAtom.Form.t SmtCertif.clause) -> + SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Proof_type.tactic diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli new file mode 100644 index 0000000..d6aa792 --- /dev/null +++ b/src/trace/smtMisc.mli @@ -0,0 +1,7 @@ +val cInt_tbl : (int, Term.constr) Hashtbl.t +val mkInt : int -> Term.constr +type 'a gen_hashed = { index : int; hval : 'a; } +val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr +val declare_new_type : Names.variable -> Term.constr +val declare_new_variable : Names.variable -> Term.types -> Term.constr +val mkName : string -> Names.name diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli new file mode 100644 index 0000000..533725b --- /dev/null +++ b/src/trace/smtTrace.mli @@ -0,0 +1,81 @@ +val notUsed : int +val clear : unit -> unit +val next_id : unit -> SmtCertif.clause_id +val mk_scertif : + 'a SmtCertif.clause_kind -> 'a list option -> 'a SmtCertif.clause +val mkRootGen : 'a list option -> 'a SmtCertif.clause +val mkRootV : 'a list -> 'a SmtCertif.clause +val isRoot : 'a SmtCertif.clause_kind -> bool +val mkRes : + 'a SmtCertif.clause -> + 'a SmtCertif.clause -> 'a SmtCertif.clause list -> 'a SmtCertif.clause +val isRes : 'a SmtCertif.clause_kind -> bool +val mkOther : 'a SmtCertif.rule -> 'a list option -> 'a SmtCertif.clause +val next : 'a SmtCertif.clause -> 'a SmtCertif.clause +val has_prev : 'a SmtCertif.clause -> bool +val prev : 'a SmtCertif.clause -> 'a SmtCertif.clause +val link : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit +val clear_links : 'a SmtCertif.clause -> unit +val skip : 'a SmtCertif.clause -> unit +val insert_before : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit +val get_res : 'a SmtCertif.clause -> string -> 'a SmtCertif.resolution +val get_other : 'a SmtCertif.clause -> string -> 'a SmtCertif.rule +val get_val : 'a SmtCertif.clause -> 'a list +val repr : 'a SmtCertif.clause -> 'a SmtCertif.clause +val set_same : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit +val get_pos : 'a SmtCertif.clause -> int +val eq_clause : 'a SmtCertif.clause -> 'b SmtCertif.clause -> bool +val select : 'a SmtCertif.clause -> unit +val occur : 'a SmtCertif.clause -> unit +val alloc : 'a SmtCertif.clause -> int +val naive_alloc : 'a SmtCertif.clause -> int +val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int +val to_coq : + ('a -> Term.constr) -> + ('a list list * 'a list -> 'b) -> + Term.types Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * + Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * + Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * + Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * + Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * + Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * + Term.constr Lazy.t -> + 'a SmtCertif.clause -> + Term.constr * 'a SmtCertif.clause * (Names.identifier * 'b) list +module MakeOpt : + functor (Form : SmtForm.FORM) -> + sig + val share_value : Form.t SmtCertif.clause -> unit + module HashedHeadRes : + sig + type t = Form.t SmtCertif.resolution + val equal : + 'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool + val hash : 'a SmtCertif.resolution -> int + end + module HRtbl : + sig + type key = HashedHeadRes.t + type 'a t = 'a Hashtbl.Make(HashedHeadRes).t + val create : int -> 'a t + val clear : 'a t -> unit + val reset : 'a t -> unit + val copy : 'a t -> 'a t + val add : 'a t -> key -> 'a -> unit + val remove : 'a t -> key -> unit + val find : 'a t -> key -> 'a + val find_all : 'a t -> key -> 'a list + val replace : 'a t -> key -> 'a -> unit + val mem : 'a t -> key -> bool + val iter : (key -> 'a -> unit) -> 'a t -> unit + val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + val length : 'a t -> int + val stats : 'a t -> Hashtbl.statistics + end + val common_head : + 'a SmtCertif.clause list -> + 'b SmtCertif.clause list -> + 'a SmtCertif.clause list * 'a SmtCertif.clause list * + 'b SmtCertif.clause list + val share_prefix : Form.t SmtCertif.clause -> int -> unit + end diff --git a/src/verit/verit.mli b/src/verit/verit.mli new file mode 100644 index 0000000..2ec830c --- /dev/null +++ b/src/verit/verit.mli @@ -0,0 +1,31 @@ +val debug : bool +val import_trace : + string -> + (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option -> + int * SmtAtom.Form.t SmtCertif.clause +val clear_all : unit -> unit +val import_all : + string -> + string -> + SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * + SmtAtom.Form.reify * SmtAtom.Form.t list * int * + SmtAtom.Form.t SmtCertif.clause +val parse_certif : + Names.identifier -> + Names.identifier -> + Names.identifier -> + Names.identifier -> + Names.identifier -> + Names.identifier -> Names.identifier -> string -> string -> unit +val theorem : Names.identifier -> string -> string -> unit +val checker : string -> string -> unit +val export : + out_channel -> + SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> unit +val call_verit : + SmtAtom.Btype.reify_tbl -> + SmtAtom.Op.reify_tbl -> + SmtAtom.Form.t -> + SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> + int * SmtAtom.Form.t SmtCertif.clause +val tactic : unit -> Proof_type.tactic diff --git a/src/versions/native/Make b/src/versions/native/Make index 07ff232..406ebb9 100644 --- a/src/versions/native/Make +++ b/src/versions/native/Make @@ -48,41 +48,62 @@ CAMLYACC = $(CAMLBIN)ocamlyacc versions/native/Structures.v versions/native/structures.ml +versions/native/structures.mli trace/coqTerms.ml +trace/coqTerms.mli trace/satAtom.ml +trace/satAtom.mli trace/smtAtom.ml trace/smtAtom.mli trace/smtCertif.ml +trace/smtCertif.mli trace/smtCnf.ml +trace/smtCnf.mli trace/smtCommands.ml +trace/smtCommands.mli trace/smtForm.ml trace/smtForm.mli trace/smtMisc.ml +trace/smtMisc.mli trace/smtTrace.ml +trace/smtTrace.mli smtlib2/smtlib2_parse.ml +smtlib2/smtlib2_parse.mli smtlib2/smtlib2_lex.ml +smtlib2/smtlib2_lex.mli smtlib2/smtlib2_ast.ml +smtlib2/smtlib2_ast.mli smtlib2/smtlib2_genConstr.ml +smtlib2/smtlib2_genConstr.mli smtlib2/smtlib2_util.ml +smtlib2/smtlib2_util.mli verit/veritParser.ml +verit/veritParser.mli verit/veritLexer.ml +verit/veritLexer.mli verit/verit.ml +verit/verit.mli verit/veritSyntax.ml verit/veritSyntax.mli zchaff/cnfParser.ml +zchaff/cnfParser.mli zchaff/satParser.ml +zchaff/satParser.mli zchaff/zchaff.ml +zchaff/zchaff.mli zchaff/zchaffParser.ml +zchaff/zchaffParser.mli cnf/Cnf.v euf/Euf.v lia/lia.ml +lia/lia.mli lia/Lia.v spl/Assumptions.v diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile index bbeb95a..540b7ce 100644 --- a/src/versions/native/Makefile +++ b/src/versions/native/Makefile @@ -192,9 +192,30 @@ MLFILES:=lia/lia.ml\ -include $(addsuffix .d,$(MLFILES)) .SECONDARY: $(addsuffix .d,$(MLFILES)) -MLIFILES:=verit/veritSyntax.mli\ +MLIFILES:=lia/lia.mli\ + zchaff/zchaffParser.mli\ + zchaff/zchaff.mli\ + zchaff/satParser.mli\ + zchaff/cnfParser.mli\ + verit/veritSyntax.mli\ + verit/verit.mli\ + verit/veritLexer.mli\ + verit/veritParser.mli\ + smtlib2/smtlib2_util.mli\ + smtlib2/smtlib2_genConstr.mli\ + smtlib2/smtlib2_ast.mli\ + smtlib2/smtlib2_lex.mli\ + smtlib2/smtlib2_parse.mli\ + trace/smtTrace.mli\ + trace/smtMisc.mli\ trace/smtForm.mli\ - trace/smtAtom.mli + trace/smtCommands.mli\ + trace/smtCnf.mli\ + trace/smtCertif.mli\ + trace/smtAtom.mli\ + trace/satAtom.mli\ + trace/coqTerms.mli\ + versions/native/structures.mli -include $(addsuffix .d,$(MLIFILES)) .SECONDARY: $(addsuffix .d,$(MLIFILES)) diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli new file mode 100644 index 0000000..057625c --- /dev/null +++ b/src/versions/native/structures.mli @@ -0,0 +1,40 @@ +val gen_constant : string list list -> string -> Term.constr lazy_t +val int63_modules : string list list +val mkInt : int -> Term.constr +val cint : Term.constr lazy_t +val parray_modules : string list list +val max_array_size : int +val mkArray : Term.types * Term.constr array -> Term.constr +val mkTrace : + ('a -> Term.constr) -> + ('a -> 'a) -> + Term.constr Lazy.t -> + 'b -> + 'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr +type names_id_t = Names.identifier +val dummy_loc : Pp.loc +val mkUConst : Term.constr -> Entries.definition_entry +val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry +val error : string -> 'a +val coqtype : Term.types lazy_t +val declare_new_type : Names.variable -> Term.constr +val declare_new_variable : Names.variable -> Term.types -> Term.constr +val extern_constr : Term.constr -> Topconstr.constr_expr +val vernacentries_interp : Topconstr.constr_expr -> unit +val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds +val lift : int -> Term.constr -> Term.constr +val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic +val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic +val assert_before : Names.name -> Term.types -> Proof_type.tactic +val vm_cast_no_check : Term.constr -> Proof_type.tactic +val mk_tactic : + (Environ.env -> + Evd.evar_map -> Term.types -> Proof_type.goal Tacmach.sigma -> 'a) -> + Proof_type.goal Tacmach.sigma -> 'a +val set_evars_tac : 'a -> Proof_type.tactic +val ppconstr_lsimpleconstr : Ppconstr.precedence +val constrextern_extern_constr : Term.constr -> Topconstr.constr_expr +module Micromega_plugin_Certificate = Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega +module Micromega_plugin_Micromega = Micromega +module Micromega_plugin_Mutils = Mutils diff --git a/src/zchaff/cnfParser.mli b/src/zchaff/cnfParser.mli new file mode 100644 index 0000000..4e2e079 --- /dev/null +++ b/src/zchaff/cnfParser.mli @@ -0,0 +1,13 @@ +val skip_comment : SatParser.lex_buff -> unit +val parse_p_cnf : SatParser.lex_buff -> int +val mklit : int -> SatAtom.Form.reify -> int -> SatAtom.Form.t +val parse_clause : + int -> SatAtom.Form.reify -> SatParser.lex_buff -> SatAtom.Form.t list +val parse_clauses : + int -> + SatAtom.Form.reify -> + SatParser.lex_buff -> + SatAtom.Form.t SmtCertif.clause -> SatAtom.Form.t SmtCertif.clause +val parse_cnf : + string -> + int * SatAtom.Form.t SmtCertif.clause * SatAtom.Form.t SmtCertif.clause diff --git a/src/zchaff/satParser.mli b/src/zchaff/satParser.mli new file mode 100644 index 0000000..ad5385b --- /dev/null +++ b/src/zchaff/satParser.mli @@ -0,0 +1,33 @@ +type lex_buff = { + buff : string; + mutable curr_char : int; + mutable buff_end : int; + in_ch : in_channel; +} +val buff_length : int +val open_file : string -> string -> lex_buff +val close : lex_buff -> unit +val eof : lex_buff -> bool +val curr_char : lex_buff -> char +val refill : lex_buff -> unit +val is_space : char -> bool +val is_space_ret : char -> bool +val skip : (char -> bool) -> lex_buff -> unit +val skip_space : lex_buff -> unit +val skip_blank : lex_buff -> unit +val skip_string : lex_buff -> string -> bool +val match_string : lex_buff -> string -> unit +val aux_buff : bytes +val aux_be : int ref +val aux_pi : int ref +val aux_cc : int ref +val save_lb : lex_buff -> unit +val restore_lb : lex_buff -> unit +val check_string : lex_buff -> string -> bool +val blank_check_string : lex_buff -> string -> bool +val blank_match_string : lex_buff -> string -> unit +val is_digit : char -> bool +val is_start_int : lex_buff -> bool +val input_int : lex_buff -> int +val input_blank_int : lex_buff -> int +val skip_line : lex_buff -> unit diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli new file mode 100644 index 0000000..ff0fe51 --- /dev/null +++ b/src/zchaff/zchaff.mli @@ -0,0 +1,88 @@ +val is_trivial : SatAtom.Form.t list -> bool +val string_of_op : SmtForm.fop -> string +val pp_form : Format.formatter -> SatAtom.Form.t -> unit +val pp_sign : Format.formatter -> SatAtom.Form.t -> unit +val pp_pform : Format.formatter -> SatAtom.Form.pform -> unit +val pp_value : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit +val pp_kind : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit +val pp_trace : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit +val import_cnf : + string -> + int * SatAtom.Form.t SmtCertif.clause * SatAtom.Form.t SmtCertif.clause * + (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t +val import_cnf_trace : + (int, 'a SmtCertif.clause) Hashtbl.t -> + string -> + SatAtom.Form.t SmtCertif.clause -> + 'a SmtCertif.clause -> int * 'a SmtCertif.clause +val make_roots : + SatAtom.Form.t SmtCertif.clause -> 'a SmtCertif.clause -> Term.constr +val interp_roots : + SatAtom.Form.t SmtCertif.clause -> 'a SmtCertif.clause -> Term.constr +val sat_checker_modules : string list list +val parse_certif : + Names.identifier -> Names.identifier -> string -> string -> unit +val cdimacs : Term.constr lazy_t +val ctheorem_checker : Term.constr lazy_t +val cchecker : Term.constr lazy_t +val theorems : + (Term.constr -> + SatAtom.Form.t SmtCertif.clause -> + SatAtom.Form.t SmtCertif.clause -> Term.constr) -> + Names.identifier -> string -> string -> unit +val theorem : Names.identifier -> string -> string -> unit +val theorem_abs : Names.identifier -> string -> string -> unit +val checker : string -> string -> unit +val export_clause : Format.formatter -> SatAtom.Form.t list -> unit +val export : + out_channel -> + int -> + SatAtom.Form.t SmtCertif.clause -> + (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t * + SatAtom.Form.t SmtCertif.clause +val call_zchaff : + int -> + SatAtom.Form.t SmtCertif.clause -> + (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t * string * string * + SatAtom.Form.t SmtCertif.clause +val cnf_checker_modules : string list list +val certif_ops : + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * + Term.constr lazy_t +val ccertif : Term.constr lazy_t +val cCertif : Term.constr lazy_t +val cchecker_b_correct : Term.constr lazy_t +val cchecker_b : Term.constr lazy_t +val cchecker_eq_correct : Term.constr lazy_t +val cchecker_eq : Term.constr lazy_t +val build_body : + SatAtom.Atom.reify_tbl -> + SatAtom.Form.reify -> + Term.constr -> + Term.constr -> + int * SatAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr +val build_body_eq : + SatAtom.Atom.reify_tbl -> + SatAtom.Form.reify -> + Term.constr -> + Term.constr -> + Term.constr -> + int * SatAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr +val get_arguments : Term.constr -> Term.constr * Term.constr +exception Sat of int list +exception Finished +val input_int : in_channel -> int +val check_unsat : string -> unit +val make_proof : + (int, 'a) SmtForm.gen_pform array -> + Term.constr array -> + Environ.env -> + SatAtom.Form.reify -> + SatAtom.Form.t -> int * SatAtom.Form.t SmtCertif.clause +val core_tactic : Environ.env -> 'a -> Term.types -> Proof_type.tactic +val tactic : unit -> Proof_type.tactic diff --git a/src/zchaff/zchaffParser.mli b/src/zchaff/zchaffParser.mli new file mode 100644 index 0000000..a512f48 --- /dev/null +++ b/src/zchaff/zchaffParser.mli @@ -0,0 +1,36 @@ +val _CL : string +val _INF : string +val _VAR : string +val _L : string +val _V : string +val _A : string +val _LITS : string +val _CONF : string +val _EQ : string +val alloc_res : + 'a SmtCertif.clause -> + 'a SmtCertif.clause -> + 'a SmtCertif.clause -> 'a SmtCertif.clause list -> 'a SmtCertif.clause +val parse_tailres : (int, 'a) Hashtbl.t -> SatParser.lex_buff -> 'a list +val parse_resolution : + (int, 'a SmtCertif.clause) Hashtbl.t -> + SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause +val parse_CL : + (int, 'a SmtCertif.clause) Hashtbl.t -> + SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause +type var_key = Var of int | Level of int +type 'hform var_decl = { + var : int; + ante : 'hform SmtCertif.clause; + ante_val : int list; + mutable vclause : 'hform SmtCertif.clause option; +} +type 'hform parse_var_info = (var_key, 'hform var_decl) Hashtbl.t +val var_of_lit : int -> int +val parse_zclause : SatParser.lex_buff -> int list +val parse_VAR_CONF : + (int, 'a SmtCertif.clause) Hashtbl.t -> + SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause +val parse_proof : + (int, 'a SmtCertif.clause) Hashtbl.t -> + string -> 'a SmtCertif.clause -> 'a SmtCertif.clause |