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/verit/veritSyntax.mli | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/verit/veritSyntax.mli')
| -rw-r--r-- | src/verit/veritSyntax.mli | 34 |
1 files changed, 31 insertions, 3 deletions
diff --git a/src/verit/veritSyntax.mli b/src/verit/veritSyntax.mli index c7bf659..27a7ee3 100644 --- a/src/verit/veritSyntax.mli +++ b/src/verit/veritSyntax.mli @@ -21,15 +21,30 @@ type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 val get_clause : int -> SmtAtom.Form.t SmtCertif.clause val add_clause : int -> SmtAtom.Form.t SmtCertif.clause -> unit +val add_ref : int -> int -> unit +val get_ref : int -> int +val to_add : (int * SmtAtom.Form.t list) list ref + val mk_clause : SmtCertif.clause_id * typ * SmtAtom.Form.t list * SmtCertif.clause_id list -> SmtCertif.clause_id type atom_form_lit = | Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.pform | Lit of SmtAtom.Form.t -val lit_of_atom_form_lit : SmtAtom.Form.reify -> atom_form_lit -> SmtAtom.Form.t -val get_solver : int -> atom_form_lit -val add_solver : int -> atom_form_lit -> unit +val lit_of_atom_form_lit : SmtAtom.Form.reify -> bool * atom_form_lit -> SmtAtom.Form.t + +val apply_dec_atom : (bool -> SmtAtom.hatom -> SmtAtom.hatom) -> + bool * atom_form_lit -> bool * atom_form_lit +val apply_bdec_atom : + (bool -> SmtAtom.Atom.t -> SmtAtom.Atom.t -> SmtAtom.Atom.t) -> + bool * atom_form_lit -> bool * atom_form_lit -> bool * atom_form_lit + +val apply_dec : ('a -> 'b) -> bool * 'a -> bool * 'b +val list_dec : (bool * 'a) list -> bool * 'a list + + +val get_solver : int -> bool * atom_form_lit +val add_solver : int -> bool * atom_form_lit -> unit val get_btype : string -> SmtBtype.btype val add_btype : string -> SmtBtype.btype -> unit @@ -37,8 +52,21 @@ val add_btype : string -> SmtBtype.btype -> unit val get_fun : string -> SmtAtom.indexed_op val add_fun : string -> SmtAtom.indexed_op -> unit +val find_opt_qvar : string -> SmtBtype.btype option +val add_qvar : string -> SmtBtype.btype -> unit +val clear_qvar : unit -> unit + +val string_hform : SmtAtom.Form.t -> string + +val init_index : SmtAtom.Form.t list -> (SmtAtom.Form.t -> SmtAtom.Form.t) -> + SmtAtom.Form.t -> int + +val qf_to_add : SmtAtom.Form.t SmtCertif.clause list -> (SmtAtom.Form.t SmtCertif.clause_kind * SmtAtom.Form.t list option * SmtAtom.Form.t SmtCertif.clause) list + val ra : SmtAtom.Atom.reify_tbl val rf : SmtAtom.Form.reify +val ra' : SmtAtom.Atom.reify_tbl +val rf' : SmtAtom.Form.reify val hlets : (string, atom_form_lit) Hashtbl.t |