sig
type t
type id
type term
type location
val annot :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.term -> Stmt_intf.Logic.term list -> Stmt_intf.Logic.term
val include_ :
?loc:Stmt_intf.Logic.location ->
string -> Stmt_intf.Logic.id list -> Stmt_intf.Logic.t
val clause :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.term list -> Stmt_intf.Logic.t
val pop : ?loc:Stmt_intf.Logic.location -> int -> Stmt_intf.Logic.t
val push : ?loc:Stmt_intf.Logic.location -> int -> Stmt_intf.Logic.t
val assert_ :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val check_sat : ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
val set_logic :
?loc:Stmt_intf.Logic.location -> string -> Stmt_intf.Logic.t
val get_info : ?loc:Stmt_intf.Logic.location -> string -> Stmt_intf.Logic.t
val set_info :
?loc:Stmt_intf.Logic.location ->
string * Stmt_intf.Logic.term option -> Stmt_intf.Logic.t
val get_option :
?loc:Stmt_intf.Logic.location -> string -> Stmt_intf.Logic.t
val set_option :
?loc:Stmt_intf.Logic.location ->
string * Stmt_intf.Logic.term option -> Stmt_intf.Logic.t
val type_decl :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.id -> int -> Stmt_intf.Logic.t
val type_def :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.id ->
Stmt_intf.Logic.id list -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val fun_decl :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.id ->
Stmt_intf.Logic.term list -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val fun_def :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.id ->
Stmt_intf.Logic.term list ->
Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val get_proof : ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
val get_unsat_core :
?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
val get_value :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.term list -> Stmt_intf.Logic.t
val get_assignment :
?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
val get_assertions :
?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
val exit : ?loc:Stmt_intf.Logic.location -> unit -> Stmt_intf.Logic.t
val tpi :
?loc:Stmt_intf.Logic.location ->
?annot:Stmt_intf.Logic.term ->
Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val thf :
?loc:Stmt_intf.Logic.location ->
?annot:Stmt_intf.Logic.term ->
Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val tff :
?loc:Stmt_intf.Logic.location ->
?annot:Stmt_intf.Logic.term ->
Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val fof :
?loc:Stmt_intf.Logic.location ->
?annot:Stmt_intf.Logic.term ->
Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val cnf :
?loc:Stmt_intf.Logic.location ->
?annot:Stmt_intf.Logic.term ->
Stmt_intf.Logic.id -> string -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val inductive :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.id ->
Stmt_intf.Logic.term list ->
(Stmt_intf.Logic.id * Stmt_intf.Logic.term list) list ->
Stmt_intf.Logic.t
val data :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.t list -> Stmt_intf.Logic.t
val decl :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.id -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val definition :
?loc:Stmt_intf.Logic.location ->
Stmt_intf.Logic.id ->
Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val goal :
?loc:Stmt_intf.Logic.location ->
?attr:Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val assume :
?loc:Stmt_intf.Logic.location ->
?attr:Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
val rewrite :
?loc:Stmt_intf.Logic.location ->
?attr:Stmt_intf.Logic.term -> Stmt_intf.Logic.term -> Stmt_intf.Logic.t
end