package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type
type term = Term.t
type location = ParseLocation.t
type inductive = {
  1. id : Id.t;
  2. vars : term list;
  3. cstrs : (Id.t * term list) list;
  4. loc : location option;
}
type descr =
  1. | Pack of t list
  2. | Pop of int
  3. | Push of int
  4. | Prove
  5. | Antecedent of term
  6. | Consequent of term
  7. | Include of string
  8. | Set_logic of string
  9. | Get_info of string
  10. | Set_info of string * term option
  11. | Get_option of string
  12. | Set_option of string * term option
  13. | Def of Id.t * term
  14. | Decl of Id.t * term
  15. | Inductive of inductive
  16. | Get_proof
  17. | Get_unsat_core
  18. | Get_value of term list
  19. | Get_assignment
  20. | Get_assertions
  21. | Exit
and t = {
  1. id : Id.t;
  2. descr : descr;
  3. attr : term option;
  4. loc : location option;
}
val annot : ?loc:location -> term -> term list -> term
val include_ : ?loc:location -> string -> Id.t list -> t
val p_cnf : ?loc:location -> int -> int -> t
val clause : ?loc:location -> term list -> t
val assumption : ?loc:location -> term list -> t
val pop : ?loc:location -> int -> t
val push : ?loc:location -> int -> t
val assert_ : ?loc:location -> term -> t
val check_sat : ?loc:location -> unit -> t
val set_logic : ?loc:location -> string -> t
val get_info : ?loc:location -> string -> t
val set_info : ?loc:location -> (string * term option) -> t
val get_option : ?loc:location -> string -> t
val set_option : ?loc:location -> (string * term option) -> t
val type_decl : ?loc:location -> Id.t -> int -> t
val type_def : ?loc:location -> Id.t -> Id.t list -> term -> t
val fun_decl : ?loc:location -> Id.t -> term list -> term -> t
val fun_def : ?loc:location -> Id.t -> term list -> term -> term -> t
val get_proof : ?loc:location -> unit -> t
val get_unsat_core : ?loc:location -> unit -> t
val get_value : ?loc:location -> term list -> t
val get_assignment : ?loc:location -> unit -> t
val get_assertions : ?loc:location -> unit -> t
val exit : ?loc:location -> unit -> t
val tpi : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val thf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val tff : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val fof : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val cnf : ?loc:location -> ?annot:term -> Id.t -> string -> term -> t
val inductive : ?loc:location -> Id.t -> term list -> (Id.t * term list) list -> t
val data : ?loc:location -> t list -> t
val decl : ?loc:location -> Id.t -> term -> t
val definition : ?loc:location -> Id.t -> term -> term -> t
val goal : ?loc:location -> ?attr:term -> term -> t
val assume : ?loc:location -> ?attr:term -> term -> t
val rewrite : ?loc:location -> ?attr:term -> term -> t
val pp : Buffer.t -> t -> unit
val print : Format.formatter -> t -> unit