package mc2

  1. Overview
  2. Docs
package mc2
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct