package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

Applicative Encoding

module T = Logtk.TypedSTerm
val section : Logtk.Util.Section.t
val enabled_ : bool ref
val (==>) : T.Ty.t list -> T.Ty.t -> T.Ty.t
val decl : Logtk.ID.t -> 'a -> ('b, 'c, 'a) Logtk.Statement.t
val bool_clone_id : Logtk.ID.t
val bool_clone_ty : T.t
val bool_clone_tydecl : (Logtk.Cnf.clause, T.t, T.t) Logtk.Statement.t
val true_clone_id : Logtk.ID.t
val true_term : T.t
val true_clone_tydecl : (Logtk.Cnf.clause, T.t, T.t) Logtk.Statement.t
val false_clone_id : Logtk.ID.t
val false_term : T.t
val false_clone_tydecl : (Logtk.Cnf.clause, T.t, T.t) Logtk.Statement.t
val and_id : Logtk.ID.t
val and_type : T.Ty.t
val and_term : T.t
val and_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val or_id : Logtk.ID.t
val or_type : T.Ty.t
val or_term : T.t
val or_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val not_id : Logtk.ID.t
val not_type : T.Ty.t
val not_term : T.t
val not_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val impl_id : Logtk.ID.t
val impl_type : T.Ty.t
val impl_term : T.t
val impl_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val equiv_id : Logtk.ID.t
val equiv_type : T.Ty.t
val equiv_term : T.t
val equiv_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val xor_id : Logtk.ID.t
val xor_type : T.Ty.t
val xor_term : T.t
val xor_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val eq_id : Logtk.ID.t
val eq_type : T.Ty.t
val eq_term : T.t
val eq_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val neq_id : Logtk.ID.t
val neq_term : T.t
val neq_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val forall_id : Logtk.ID.t
val forall_type : T.Ty.t
val forall_term : T.t
val forall_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val exists_id : Logtk.ID.t
val exists_term : T.t
val exists_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val choice_id : Logtk.ID.t
val choice_type : T.Ty.t
val choice_term : T.t
val choice_clone_tydecl : (Logtk.Cnf.clause, T.t, T.Ty.t) Logtk.Statement.t
val app_bool : T.t -> T.t list -> T.t
val boolean_axioms : T.t Logtk.SLiteral.t list Iter.t
val bool_encode_ty : T.t -> T.t
val bool_encode_term : T.t -> T.t
val bool_encode_lit : T.t Logtk.SLiteral.t -> T.t Logtk.SLiteral.t
val bool_encode_lits : T.t Logtk.SLiteral.t list -> T.t Logtk.SLiteral.t list

Encode a clause

exception E_i of (T.t Logtk.SLiteral.t list, T.t, T.t) Logtk.Statement.t

encode a statement

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct