mc2 0.1 (latest) · OCaml Package

Modular Term Structure

type view = ..

type t

type tc

Basics

val id : t -> int

Globally unique ID of this term

val view : t -> view

Globally unique ID of this term

val equal : t -> t -> bool

val compare : t -> t -> int

val hash : t -> int

val pp : t CCFormat.printer

val debug : t CCFormat.printer

val debug_no_val : t CCFormat.printer

like debug but does not print val

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 -> 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 marked : t -> bool

Clear the fields of the variable.

Was mark called on this var?

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

val max_level : int -> int -> int

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

val 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

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 (T : TERM_ALLOC_OPS) : TERM_ALLOC

Containers

module Tbl : CCHashtbl.S with type key = Mc2_core__.Solver_types.term

module Map : CCMap.S with type key = Mc2_core__.Solver_types.term

module Set : CCSet.S with type elt = Mc2_core__.Solver_types.term

package mc2