module Istate: sig end
Global state.
Global state.
type t = {
|
mutable current : Context.t; |
|
mutable symtab : Symtab.t; |
|
mutable inchannel : Pervasives.in_channel; |
|
mutable outchannel : Format.formatter; |
|
mutable eot : string; |
|
mutable counter : int; |
}
val init : unit -> t
val s : t
Initialize.
val initialize : bool -> string -> Pervasives.in_channel -> Format.formatter -> unit
| Parameters: |
|
pp |
: |
bool
|
|
eot |
: |
string
|
|
inch |
: |
Pervasives.in_channel
|
|
outch |
: |
Format.formatter
|
|
Accessors to components of global state.
val current : unit -> Context.t
val symtab : unit -> Symtab.t
val eot : unit -> string
val inchannel : unit -> Pervasives.in_channel
val outchannel : unit -> Format.formatter
Adding to symbol table
val def : Name.t -> Symtab.defn -> unit
val sgn : Name.t -> int -> unit
val typ : Name.t list -> Dom.t -> unit
val entry_of : Name.t -> Symtab.entry option
Type from the symbol table.
val type_of : Name.t -> Dom.t option
Get context for name in symbol table
val context_of : Name.t -> Context.t
Getting the width of bitvector terms from the signature.
val width_of : Term.t -> int option
Resetting all of the global state.
val reset : unit -> unit
Getting either current context or explicitly specified context.
val get_context : Name.t option -> Context.t
Set input and output channels.
val set_inchannel : Pervasives.in_channel -> unit
| Parameters: |
|
ch |
: |
Pervasives.in_channel
|
|
val set_outchannel : Format.formatter -> unit
val flush : unit -> unit
val nl : unit -> unit
Context.
val ctxt_of : Name.t option -> Atom.Set.t
Canonization w.r.t current state.
val can : Term.t -> Term.t
val sigma : Sym.t -> Term.t list -> Term.t
Create a fresh name for a state.
val fresh_state_name : unit -> Name.t
Change current state.
val save : Name.t option -> Name.t
val restore : Name.t -> unit
val remove : Name.t -> unit
val forget : unit -> unit
Adding a new fact
val process : Name.t option -> Atom.t -> Name.t Context.Status.t
val valid : Name.t option -> Atom.t -> bool
val unsat : Name.t option -> Atom.t -> bool
val model : Name.t option -> Term.t list -> (Term.Map.key * Term.t) list
Accessors.
val diseq : Name.t option -> Term.t -> Term.Set.t
val sign : Name.t option -> Term.t -> Sign.t option
val dom : Name.t option -> Term.t -> Dom.t option
Applying maps.
val find : Name.t option -> Th.t -> Term.t -> Term.t
val inv : Name.t option -> Th.t -> Term.t -> Term.t
val use : Name.t option -> Th.t -> Term.t -> Term.Set.t
Solution sets.
val solution : Name.t option -> Th.t -> (Term.t * Term.t) list
Solver.
val solve : Th.t -> Term.t * Term.t -> (Term.t * Term.t) list
Equality/disequality test.
val is_equal : Term.t -> Term.t -> Three.t
Sat solver
val sat : Prop.t -> (Prop.Assignment.t * Name.t) option
Splitting.
val split : unit -> Atom.Set.t