diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /src/trace/smtAtom.mli | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/trace/smtAtom.mli')
| -rw-r--r-- | src/trace/smtAtom.mli | 45 |
1 files changed, 31 insertions, 14 deletions
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index 8e69265..47734fb 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -43,7 +43,10 @@ type nop = type indexed_op -val dummy_indexed_op: int -> btype array -> btype -> indexed_op +type index = Index of int + | Rel_name of string + +val dummy_indexed_op: index -> btype array -> btype -> indexed_op val indexed_op_index : indexed_op -> int module Op : @@ -53,7 +56,8 @@ module Op : val create : unit -> reify_tbl - val declare : reify_tbl -> Term.constr -> btype array -> btype -> indexed_op + val declare : reify_tbl -> Term.constr -> btype array -> + btype -> string option -> indexed_op val of_coq : reify_tbl -> Term.constr -> indexed_op @@ -92,6 +96,8 @@ module Atom : val type_of : hatom -> btype + val to_string : ?pi:bool -> hatom -> string + val to_smt : Format.formatter -> t -> unit exception NotWellTyped of atom @@ -102,10 +108,22 @@ module Atom : val clear : reify_tbl -> unit - val get : reify_tbl -> atom -> hatom + val get : ?declare:bool -> reify_tbl -> atom -> hatom + + val mk_eq : reify_tbl -> bool -> btype -> hatom -> hatom -> hatom + + val mk_neg : reify_tbl -> hatom -> hatom + + val hash_hatom : reify_tbl -> hatom -> hatom + + (** for debugging purposes **) + val copy : reify_tbl -> reify_tbl + + val print_atoms : reify_tbl -> string -> unit + (** Given a coq term, build the corresponding atom *) - val of_coq : SmtBtype.reify_tbl -> Op.reify_tbl -> + val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl -> reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t val to_coq : hatom -> Term.constr @@ -121,16 +139,15 @@ module Atom : val hatom_Z_of_int : reify_tbl -> int -> hatom val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> hatom - val mk_eq : reify_tbl -> btype -> hatom -> hatom -> hatom - val mk_lt : reify_tbl -> hatom -> hatom -> hatom - val mk_le : reify_tbl -> hatom -> hatom -> hatom - val mk_gt : reify_tbl -> hatom -> hatom -> hatom - val mk_ge : reify_tbl -> hatom -> hatom -> hatom - val mk_plus : reify_tbl -> hatom -> hatom -> hatom - val mk_minus : reify_tbl -> hatom -> hatom -> hatom - val mk_mult : reify_tbl -> hatom -> hatom -> hatom - val mk_opp : reify_tbl -> hatom -> hatom - val mk_distinct : reify_tbl -> btype -> hatom array -> hatom + val mk_lt : reify_tbl -> bool -> hatom -> hatom -> hatom + val mk_le : reify_tbl -> bool -> hatom -> hatom -> hatom + val mk_gt : reify_tbl -> bool -> hatom -> hatom -> hatom + val mk_ge : reify_tbl -> bool -> hatom -> hatom -> hatom + val mk_plus : reify_tbl -> bool -> hatom -> hatom -> hatom + val mk_minus : reify_tbl -> bool -> hatom -> hatom -> hatom + val mk_mult : reify_tbl -> bool -> hatom -> hatom -> hatom + val mk_opp : reify_tbl -> ?declare:bool -> hatom -> hatom + val mk_distinct : reify_tbl -> btype -> ?declare:bool -> hatom array -> hatom end |