Module Mc2_core.TermSource

Modular Term Structure

Sourcetype view = ..
Sourcetype t
Sourcetype tc

Basics

Sourceval id : t -> int

Globally unique ID of this term

Sourceval view : t -> view

Globally unique ID of this term

Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval hash : t -> int
Sourceval debug_no_val : t CCFormat.printer

like debug but does not print val

ID Management

Sourceval plugin_id_width : int

Number of bits dedicated to plugin IDs. There can be at most 2 ** plugin_id_width plugins in a solver.

Sourceval plugin_id : t -> int

Which plugin owns this term?

Sourceval plugin_specific_id : t -> int

Which plugin owns this term?

ID of the term for the plugin itself

Sourceval mark : t -> unit

Mark the variable

Sourceval unmark : t -> unit

Mark the variable

Clear the fields of the variable.

Sourceval marked : t -> bool

Clear the fields of the variable.

Was mark called on this var?

Sourceval is_deleted : t -> bool
Sourceval is_added : t -> bool
Sourceval level : t -> int

decision/assignment level of the term

Sourceval level_for : t -> Mc2_core__.Solver_types.value -> int

decision/assignment level of the term

level for evaluating into this value

Sourceval var : t -> Mc2_core__.Solver_types.var

level for evaluating into this value

Sourceval ty : t -> Type.t
Sourceval reason : t -> Mc2_core__.Solver_types.reason option
Sourceval reason_exn : t -> Mc2_core__.Solver_types.reason
Sourceval eval : t -> Mc2_core__.Solver_types.eval_res
Sourceval is_bool : t -> bool
Sourceval level_semantic : t -> int

maximum level of subterms, or -1 if some subterm is not assigned

Sourceval level_sub : t -> int

maximum level of subterms, ignoring unassigned subterms

Sourceval max_level : int -> int -> int

maximum of the levels, or -1 if either is -1

Sourceval 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.

Sourceval subterms : t -> t list
Sourceval decide_state_exn : t -> Mc2_core__.Solver_types.decide_state

Obtain decide state, or raises if the variable is not semantic

Sourceval weight : t -> float

Heuristic weight

Sourceval set_weight : t -> float -> unit

Heuristic weight

Sourceval has_some_value : t -> bool
Sourceval has_value : t -> Mc2_core__.Solver_types.value -> bool
Sourceval value : t -> Mc2_core__.Solver_types.value option
Sourceval value_exn : t -> Mc2_core__.Solver_types.value
Sourceval mk_eq : t -> t -> t

Use the term's type to make two terms equal

Sourceval gc_unmark : t -> unit

Unmark just this term

Sourceval gc_marked : t -> bool

Unmark just this term

Sourceval gc_mark : t -> unit

Non recursive

Sourceval field_get : Mc2_core__.Solver_types.Term_fields.field -> t -> bool
Sourceval field_set : Mc2_core__.Solver_types.Term_fields.field -> t -> unit
Sourceval field_clear : Mc2_core__.Solver_types.Term_fields.field -> t -> unit
Sourceval has_var : t -> bool

is there a variable for the term?

Sourceval setup_var : t -> unit

is there a variable for the term?

create a variable for the term

Sourceval add_watch : t -> t -> unit

add_watch t u adds u to the list of watches of t. u will be notified whenever t is assigned

Bool terms

Sourcemodule Bool : sig ... end

1-term Watch Scheme

Sourcemodule Watch1 : sig ... end

2-terms Watch Scheme

Sourcemodule Watch2 : sig ... end

Assignment view

Sourceval assigned : t -> bool
Sourceval assignment : t -> Mc2_core__.Solver_types.assignment_view option

Current assignment of this term

Low Level constructors. Use at your own risks.

Sourcemodule TC : sig ... end

Hashconsing of terms belonging to a Plugin

Sourcemodule type TERM_ALLOC_OPS = sig ... end
Sourcemodule type TERM_ALLOC = sig ... end

Containers

Sourcemodule Tbl : CCHashtbl.S with type key = Mc2_core__.Solver_types.term
Sourcemodule Map : CCMap.S with type key = Mc2_core__.Solver_types.term
Sourcemodule Set : CCSet.S with type elt = Mc2_core__.Solver_types.term