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/smtForm.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/smtForm.mli')
-rw-r--r-- | src/trace/smtForm.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index c372bf5..4ee86e2 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -37,6 +37,7 @@ type fop = | Fiff | Fite | Fnot2 of int + | Fforall of (string * SmtBtype.btype) list type ('a,'f) gen_pform = | Fatom of 'a @@ -61,18 +62,21 @@ module type FORM = val is_pos : t -> bool val is_neg : t -> bool - val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit + val to_string : ?pi:bool -> (hatom -> string) -> t -> string + val to_smt : (hatom -> string) -> Format.formatter -> t -> unit (* Building formula from positive formula *) exception NotWellTyped of pform type reify val create : unit -> reify val clear : reify -> unit - val get : reify -> pform -> t + val get : ?declare:bool -> reify -> pform -> t (** Given a coq term, build the corresponding formula *) val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t + val hash_hform : (hatom -> hatom) -> reify -> t -> t + (** Flattening of [Fand] and [For], removing of [Fnot2] *) val flatten : reify -> t -> t |