diff options
Diffstat (limited to 'src/lfsc/translator_sig.mli')
| -rw-r--r-- | src/lfsc/translator_sig.mli | 159 |
1 files changed, 159 insertions, 0 deletions
diff --git a/src/lfsc/translator_sig.mli b/src/lfsc/translator_sig.mli new file mode 100644 index 0000000..66005f3 --- /dev/null +++ b/src/lfsc/translator_sig.mli @@ -0,0 +1,159 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +(** + Signature to implement to build a converter of LFSC proofs. + See {!Converter.Make}, {!Tosmtcoq} and {!VeritPrinter}. +*) + +open Ast +open Format + + +(** The type of destination rules that are currently supported byt the + converter *) +type rule = + | Reso + | Weak + | Or + | Orp + | Imp + | Impp + | Nand + | Andn + | Nimp1 + | Nimp2 + | Impn1 + | Impn2 + | Nor + | Orn + | And + | Andp + | Equ1 + | Equ2 + | Nequ1 + | Nequ2 + | Equp1 + | Equp2 + | Equn1 + | Equn2 + | Xor1 + | Xor2 + | Xorp1 + | Xorp2 + | Xorn1 + | Xorn2 + | Nxor1 + | Nxor2 + | Itep1 + | Itep2 + | Iten1 + | Iten2 + | Ite1 + | Ite2 + | Nite1 + | Nite2 + | Eqtr + | Eqcp + | Eqco + | Eqre + | Lage + | Flat + | Hole + | True + | Fals + | Bbva + | Bbconst + | Bbeq + | Bbdis + | Bbop + | Bbadd + | Bbmul + | Bbult + | Bbslt + | Bbshl + | Bbshr + | Bbnot + | Bbneg + | Bbconc + | Bbextr + | Bbzext + | Bbsext + | Row1 + | Row2 + | Exte + +(** Signature for translators *) +module type S = sig + + (** The type of literal depends on the chosen tranlation, it is abstract *) + type lit + + (** Clauses are lists of the aforementioned literals *) + type clause = lit list + + (** Transform a term in LFSC to the chosen clause representation. (This + eliminates top-level dijunctions and implications.) *) + val to_clause : term -> clause + + (** Print a clause (for debugging purposes) *) + val print_clause : formatter -> clause -> unit + + (** Manually resgister a clause with an integer identifier *) + val register_clause_id : clause -> int -> unit + + (** Create a new clause as the result of a rule application with a list of + intgeger arguments. These can be either previously defined clause + identifiers or an arbitrary positive integer depending on the rule. It + returns the identifier of the newly created resulting clause. The + optional arguemnt [reuse] ([true] by default) says if we should reuse + clauses that were previously deduced, in this case the rule application + will not be created and it returns the identifier of this pre-existing + clause. *) + val mk_clause : ?reuse:bool -> rule -> clause -> int list -> int + + (** Same as {!mk_clause} but with an hybrid representation for clauses. This + is just used to avoid creating unecessary terms for these clauses when + they are built by hand. *) + val mk_clause_cl : ?reuse:bool -> rule -> term list -> int list -> int + + (** Create an input unit clause. It is given an identifier that is not + returned. *) + val mk_input : Hstring.t -> term -> unit + + val mk_admit_preproc : Hstring.t -> term -> unit + + (** [register_prop_abstr v p] register the term [v] as being a propositional + abstraction of the term [p]. *) + val register_prop_abstr : term -> term -> unit + + (** Returns the identifier of a previously deduced clause. *) + val get_clause_id : clause -> int + + (** Returns the identifier of a unit input clause given its name, as + intoduced by the proprocessor of CVC4 in the LFSC proof. *) + val get_input_id : Hstring.t -> int + + val register_decl : Hstring.t -> term -> unit + + val register_decl_id : Hstring.t -> int -> unit + + (** register an alias name for a term *) + val register_alias : Hstring.t -> term -> unit + + (* (\** register a term as an alias for another term *\) *) + (* val register_termalias : term -> term -> unit *) + + (** Clear and reset global tables and values. *) + val clear : unit -> unit + +end |