package libzipperposition

  1. Overview
  2. Docs
On This Page
  1. Boolean Trail
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Libzipperposition.TrailSource

Boolean Trail

Sourcemodule Lit = BBox.Lit
Sourcetype t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval compare : t -> t -> int
Sourcetype bool_lit = Lit.t
Sourceval empty : t
Sourceval singleton : bool_lit -> t
Sourceval mem : bool_lit -> t -> bool
Sourceval add : bool_lit -> t -> t
Sourceval remove : bool_lit -> t -> t
Sourceval map : (bool_lit -> bool_lit) -> t -> t
Sourceval fold : ('a -> bool_lit -> 'a) -> 'a -> t -> 'a
Sourceval length : t -> int
Sourceval for_all : (bool_lit -> bool) -> t -> bool
Sourceval exists : (bool_lit -> bool) -> t -> bool
Sourceval of_list : bool_lit list -> t
Sourceval add_list : t -> bool_lit list -> t
Sourceval to_list : t -> bool_lit list
Sourceval to_seq : t -> bool_lit Iter.t
Sourceval subsumes : t -> t -> bool

subsumes a b is true iff a is a subset of b

Sourceval is_empty : t -> bool

Empty trail?

Sourceval is_trivial : t -> bool

returns true iff the trail contains both i and -i.

Sourceval merge : t -> t -> t

Merge several trails (e.g. from different clauses)

Sourceval merge_l : t list -> t

Merge several trails (e.g. from different clauses)

Sourceval filter : (bool_lit -> bool) -> t -> t

Only keep a subset of boolean literals

Sourcetype valuation = bool_lit -> bool

A boolean valuation

Sourceval is_active : t -> v:valuation -> bool

Trail.is_active t ~v is true iff all boolean literals in t are satisfied in the boolean valuation v.

Sourceval to_s_form : t -> Logtk.TypedSTerm.Form.t
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