From faaa2848c37444f8f37ac432c25f9f813e1df39b Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Sat, 27 Oct 2018 20:08:44 +0200
Subject: Adding support for lemmas in the command verit

---
 src/trace/smtForm.mli | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'src/trace/smtForm.mli')

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
 
-- 
cgit