Library
Module
Module type
Parameter
Class
Class type
val id : t -> int
Globally unique ID of this term
val hash : t -> int
val pp : t CCFormat.printer
val debug : t CCFormat.printer
Number of bits dedicated to plugin IDs. There can be at most 2 ** plugin_id_width
plugins in a solver.
val plugin_id : t -> int
Which plugin owns this term?
val plugin_specific_id : t -> int
Which plugin owns this term?
ID of the term for the plugin itself
val mark : t -> unit
Mark the variable
val unmark : t -> unit
Mark the variable
Clear the fields of the variable.
val is_deleted : t -> bool
val is_added : t -> bool
val level : t -> int
decision/assignment level of the term
val level_for : t -> Mc2_core__.Solver_types.value -> int
decision/assignment level of the term
level for evaluating into this value
val var : t -> Mc2_core__.Solver_types.var
level for evaluating into this value
val reason : t -> Mc2_core__.Solver_types.reason option
val reason_exn : t -> Mc2_core__.Solver_types.reason
val eval : t -> Mc2_core__.Solver_types.eval_res
val is_bool : t -> bool
val level_semantic : t -> int
maximum level of subterms, or -1 if some subterm is not assigned
val level_sub : t -> int
maximum level of subterms, ignoring unassigned subterms
Iteration over subterms. When incrementing activity, adding new terms, etc. we want to be able to iterate over all subterms of a formula.
val decide_state_exn : t -> Mc2_core__.Solver_types.decide_state
Obtain decide state, or raises if the variable is not semantic
val weight : t -> float
Heuristic weight
val set_weight : t -> float -> unit
Heuristic weight
val has_some_value : t -> bool
val has_value : t -> Mc2_core__.Solver_types.value -> bool
val value : t -> Mc2_core__.Solver_types.value option
val value_exn : t -> Mc2_core__.Solver_types.value
val gc_unmark : t -> unit
Unmark just this term
val gc_marked : t -> bool
Unmark just this term
val gc_mark : t -> unit
Non recursive
val field_get : Mc2_core__.Solver_types.Term_fields.field -> t -> bool
val field_set : Mc2_core__.Solver_types.Term_fields.field -> t -> unit
val field_clear : Mc2_core__.Solver_types.Term_fields.field -> t -> unit
val has_var : t -> bool
is there a variable for the term?
val setup_var : t -> unit
is there a variable for the term?
create a variable for the term
add_watch t u
adds u
to the list of watches of t
. u
will be notified whenever t
is assigned
module Bool : sig ... end
module Watch1 : sig ... end
module Watch2 : sig ... end
val assigned : t -> bool
val assignment : t -> Mc2_core__.Solver_types.assignment_view option
Current assignment of this term
module TC : sig ... end
module type TERM_ALLOC_OPS = sig ... end
module type TERM_ALLOC = sig ... end
module Term_allocator (T : TERM_ALLOC_OPS) : TERM_ALLOC