Up  Next

Module Encoding

module Encoding: sig .. end

Encoding of clauses


type 'a printer = Format.formatter -> 'a -> unit

Base definitions


type 'a lit =
| Eq of 'a * 'a * bool
| Prop of 'a * bool
| Bool of bool 
val fmap_lit : ('a -> 'b) -> 'a lit -> 'b lit
type 'a clause = 'a lit list 
val fmap_clause : ('a -> 'b) -> 'a clause -> 'b clause
type foterm = Libzipperposition.FOTerm.t 
type hoterm = Libzipperposition.TypedSTerm.t 
type foclause = foterm clause 
type hoclause = hoterm clause 
val foclause_of_clause : Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list ->
       foclause
Raises Invalid_argument if the argument is not a proper clause
val clause_of_foclause : foclause ->
       Libzipperposition.FOTerm.t Libzipperposition.SLiteral.t list
Convert back to a list of formulas
Since 0.8
val pp_clause : 'a printer -> 'a clause printer
Printer of clauses

Encoding abstraction

class type [['a, 'b]] t = object .. end
val id : ('a, 'a) t
Identity encoding
val compose : ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t
Compose two encodings together
val (>>>) : ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t
Infix notation for composition

Currying

val currying : (foterm clause, hoterm clause) t

Clause encoding

Encode the whole clause into a Reasoner.Property.t, ie a higher-order term that represents a meta-level property.

module EncodedClause: sig .. end
val clause_prop : (hoclause, EncodedClause.t) t