package mc2

  1. Overview
  2. Docs

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

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