Module Mc2_core.Term
Modular Term Structure
type view
= Mc2_core__.Solver_types.term_view
=
..
type t
= Mc2_core__.Solver_types.term
type tc
= Mc2_core__.Solver_types.tc_term
Basics
val id : t -> int
Globally unique ID of this term
ID Management
val plugin_id_width : int
Number of bits dedicated to plugin IDs. There can be at most
2 ** plugin_id_width
plugins in a solver.
val plugin_id : t -> Mc2_core__.Solver_types.plugin_id
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 -> Mc2_core__.Solver_types.level
decision/assignment level of the term
val level_for : t -> Mc2_core__.Solver_types.value -> Mc2_core__.Solver_types.level
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 ty : t -> Type.t
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 -> Mc2_core__.Solver_types.level
maximum level of subterms, or -1 if some subterm is not assigned
val level_sub : t -> Mc2_core__.Solver_types.level
maximum level of subterms, ignoring unassigned subterms
val max_level : Mc2_core__.Solver_types.level -> Mc2_core__.Solver_types.level -> Mc2_core__.Solver_types.level
maximum of the levels, or
-1
if either is-1
val iter_subterms : t -> t Iter.t
Iteration over subterms. When incrementing activity, adding new terms, etc. we want to be able to iterate over all subterms of a formula.
val subterms : t -> t list
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 mk_eq : t -> t -> t
Use the term's type to make two terms equal
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
Bool terms
module Bool : sig ... end
1-term Watch Scheme
module Watch1 : sig ... end
2-terms Watch Scheme
module Watch2 : sig ... end
Assignment view
val assigned : t -> bool
val assignment : t -> Mc2_core__.Solver_types.assignment_view option
Current assignment of this term
Low Level constructors. Use at your own risks.
module TC : sig ... end
Hashconsing of terms belonging to a Plugin
module type TERM_ALLOC_OPS = sig ... end
module type TERM_ALLOC = sig ... end
module Term_allocator : functor (T : TERM_ALLOC_OPS) -> TERM_ALLOC
Containers
module Tbl : CCHashtbl.S with type Tbl.key = Mc2_core__.Solver_types.term
module Map : CCMap.S with type Map.key = Mc2_core__.Solver_types.term
module Set : CCSet.S with type Set.elt = Mc2_core__.Solver_types.term