Module `Mc2_core.Term`Source

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 pp : t CCFormat.printer

Sourceval debug : t CCFormat.printer

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

Sourcemodule Term_allocator (T : TERM_ALLOC_OPS) : TERM_ALLOC

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mc2.core/Mc2_core/Term/index.html

Module `Mc2_core.Term`Source

Modular Term Structure

Basics

ID Management

Bool terms

1-term Watch Scheme

2-terms Watch Scheme

Assignment view

Low Level constructors. Use at your own risks.

Hashconsing of terms belonging to a Plugin

Containers

package mc2

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mc2.core/Mc2_core/Term/index.html

Module Mc2_core.TermSource

Modular Term Structure

Basics

ID Management

Bool terms

1-term Watch Scheme

2-terms Watch Scheme

Assignment view

Low Level constructors. Use at your own risks.

Hashconsing of terms belonging to a Plugin

Containers

Module `Mc2_core.Term`Source