🥮 mooncakes.io

moonbdd

Canonical ROBDDs and bounded symbolic state-space analysis for MoonBit

bdd
robdd
boolean-functions
symbolic-analysis
model-checking
moon add oyjh0381/moonbdd@0.1.0
Download zip
Author
Version
0.1.0
License
Apache-2.0
Repository
Last updated
12 hours ago
Downloads
3

Dependencies

README

#MoonBDD

Canonical ROBDDs and bounded symbolic finite-state reachability for MoonBit.

///|
let manager = @moonbdd.Manager::new(
  ["a", "b"],
  @moonbdd.ResourceBudget::default(),
).unwrap()

///|
let value = manager.compile("a -> b").unwrap()

///|
let count = manager.sat_count_decimal(value).unwrap()

The core is portable across Wasm, Wasm-GC, JavaScript, and Native. All BDD Handles are owned by one explicit Manager and explosive entry points use Resource Budgets. See the repository README for the full contract.

#
Bdd

source
pub struct Bdd {
  owner : Manager
  root : Int
}

A Manager-owned reference to one canonical Boolean Function.

#
Bdd::same

source
fn Bdd::same(self : Bdd, other : Bdd) -> Bool

#
BddError

source
pub(all) enum BddError {
  InvalidBudget(String, Int)
  EmptyVariable
  InvalidVariableName(String)
  DuplicateVariable(String)
  UnknownVariable(String)
  ForeignHandle
  NodeBudgetExceeded(Int)
  WorkBudgetExceeded(Int)
  InputBudgetExceeded(Int)
  DepthBudgetExceeded(Int)
  ModelBudgetExceeded(Int)
  ConstraintBudgetExceeded(Int)
  AnalysisBudgetExceeded(Int)
  OutputBudgetExceeded(Int)
  IterationBudgetExceeded(Int)
  ArithmeticOverflow
  InvalidArgument(String)
  InvalidArtifact(String)
  UnsupportedVersion(Int)
} derive(Eq, 
Debug)

Stable public error categories. Errors never encode private node-table layout and are suitable for mapping to CLI exit categories.

#
BddStatistics

source
pub(all) struct BddStatistics {
  declared_variables : Int
  support_variables : Int
  reachable_nodes : Int
  retained_nodes : Int
  model_count_decimal : String
} derive(Eq, 
Debug)

Deterministic public statistics for one BDD Handle.

#
ConstraintError

source
pub(all) enum ConstraintError {
  EmptyConstraintName
  DuplicateConstraintName(String)
  ConstraintCompileFailure(String, ExpressionError)
  ConstraintAnalysisFailure(BddError)
} derive(Eq, 
Debug)

Stable failures specific to compiling and diagnosing named Constraint Sets.

#
ConstraintReport

source
pub struct ConstraintReport {
  combined : Bdd
  satisfiable : Bool
  witness : Model?
  minimal_conflict : Array[String]
  redundant : Array[String]
}

Deterministic Constraint Set diagnosis. Satisfiable sets provide a witness and constraints removable without changing the conjunction. Unsatisfiable sets provide a deletion-minimal conflict in input order.

#
Cube

source
pub(all) struct Cube {
  values : Array[(String, Bool)]
} derive(Eq, 
Debug)

One partial assignment that guarantees the represented function is true. Variables absent from values are don't-care dimensions.

#
CubeEnumeration

source
pub(all) struct CubeEnumeration {
  cubes : Array[Cube]
  complete : Bool
} derive(Eq, 
Debug)

Bounded deterministic enumeration of pairwise-disjoint satisfying Cubes.

#
DecisionNode

source
type DecisionNode derive(Eq, 
Debug)

#
ExpressionError

source
pub(all) enum ExpressionError {
  ParseFailure(ParseDiagnostic)
  CompileFailure(BddError)
} derive(Eq, 
Debug)

#
Manager

source
pub struct Manager {
  variables : Array[String]
  variable_index : 
HashMap[String, Int]
  budget : ResourceBudget
  // private fields
}

Owner of one Variable Order and one canonical ROBDD node universe.

#
Manager::and_bdd

source
fn Manager::and_bdd(self : Manager, left : Bdd, right : Bdd) -> Result[Bdd, BddError]

#
Manager::backbone

source
fn Manager::backbone(self : Manager, value : Bdd) -> Result[Array[(String, Bool)], BddError]

Return assignments forced in every satisfying Model, in Variable Order.

#
Manager::canonical_expression

source
fn Manager::canonical_expression(self : Manager, value : Bdd) -> Result[String, BddError]

Produce a deterministic parser-compatible Shannon expansion. Equivalent BDD Handles in one Manager produce byte-identical text.

#
Manager::check_disjoint

source
fn Manager::check_disjoint(self : Manager, left : Bdd, right : Bdd) -> Result[RelationCheck, BddError]

Check that two Boolean Functions have no common Model.

#
Manager::check_entailment

source
fn Manager::check_entailment(self : Manager, premise : Bdd, conclusion : Bdd) -> Result[RelationCheck, BddError]

Check whether every Model of premise is also a Model of conclusion.

#
Manager::check_equivalence

source
fn Manager::check_equivalence(self : Manager, left : Bdd, right : Bdd) -> Result[RelationCheck, BddError]

Check semantic equivalence and return a Model of the exclusive-or on failure.

#
Manager::compile

source
fn Manager::compile(self : Manager, source : String) -> Result[Bdd, ExpressionError]

#
Manager::compose

source
fn Manager::compose(self : Manager, value : Bdd, variable_name : String, replacement : Bdd) -> Result[Bdd, BddError]

#
Manager::cube_to_bdd

source
fn Manager::cube_to_bdd(self : Manager, cube : Cube) -> Result[Bdd, BddError]

Convert a partial assignment into its conjunction. Input order is ignored; the resulting BDD always follows Manager Variable Order.

#
Manager::decode_json

source
fn Manager::decode_json(text : String, budget : ResourceBudget) -> Result[(Manager, Bdd), BddError]

Decode a strict deterministic JSON Schema v1 artifact into a fresh Manager.

#
Manager::diagnose_constraints

source
fn Manager::diagnose_constraints(self : Manager, constraints : Array[NamedConstraint]) -> Result[ConstraintReport, ConstraintError]

Compile and diagnose a deterministic set of named constraints. Redundancy elimination scans from the end so earlier policy declarations win.

#
Manager::encode_json

source
fn Manager::encode_json(self : Manager, value : Bdd) -> Result[String, BddError]

Encode one BDD Handle as deterministic JSON Schema v1. Artifact node IDs are compact and independent from unreachable Manager-retained nodes.

#
Manager::enumerate_cubes

source
fn Manager::enumerate_cubes(self : Manager, value : Bdd, maximum_cubes : Int) -> Result[CubeEnumeration, BddError]

Enumerate true-terminal paths as disjoint partial assignments. Cubes are returned in low-before-high Variable Order and may omit don't-care names.

#
Manager::enumerate_models

source
fn Manager::enumerate_models(self : Manager, value : Bdd, maximum : Int) -> Result[ModelEnumeration, BddError]

#
Manager::equivalent

source
fn Manager::equivalent(self : Manager, left : Bdd, right : Bdd) -> Result[Bdd, BddError]

#
Manager::evaluate

source
fn Manager::evaluate(self : Manager, value : Bdd, assignment : Array[(String, Bool)]) -> Result[Bool, BddError]

#
Manager::evaluate_partial

source
fn Manager::evaluate_partial(self : Manager, value : Bdd, assignment : Array[(String, Bool)]) -> Result[PartialValue, BddError]

#
Manager::exists

source
fn Manager::exists(self : Manager, value : Bdd, variables : Array[String]) -> Result[Bdd, BddError]

#
Manager::false_bdd

source
fn Manager::false_bdd(self : Manager) -> Bdd

#
Manager::forall

source
fn Manager::forall(self : Manager, value : Bdd, variables : Array[String]) -> Result[Bdd, BddError]

#
Manager::implies

source
fn Manager::implies(self : Manager, premise : Bdd, conclusion : Bdd) -> Result[Bdd, BddError]

#
Manager::is_false

source
fn Manager::is_false(self : Manager, value : Bdd) -> Bool

#
Manager::is_terminal

source
fn Manager::is_terminal(self : Manager, value : Bdd) -> Bool

#
Manager::is_true

source
fn Manager::is_true(self : Manager, value : Bdd) -> Bool

#
Manager::ite

source
fn Manager::ite(self : Manager, condition : Bdd, then_value : Bdd, else_value : Bdd) -> Result[Bdd, BddError]

#
Manager::new

source
fn Manager::new(variable_names : Array[String], budget : ResourceBudget) -> Result[Manager, BddError]

#
Manager::not_bdd

source
fn Manager::not_bdd(self : Manager, value : Bdd) -> Result[Bdd, BddError]

#
Manager::optimize_order

source
fn Manager::optimize_order(self : Manager, value : Bdd) -> Result[ReorderResult, BddError]

Deterministically accept adjacent swaps that strictly reduce reachable Decision Nodes. The source Manager and BDD Handle are never modified.

#
Manager::or_bdd

source
fn Manager::or_bdd(self : Manager, left : Bdd, right : Bdd) -> Result[Bdd, BddError]

#
Manager::reach

source
fn Manager::reach(self : Manager, initial : Bdd, transition : Bdd, encoding : StateEncoding, invariant : Bdd?) -> Result[ReachabilityResult, BddError]

Compute the least finite Reachability Fixed Point. The Transition Relation is interpreted over the paired current and next Variables in encoding.

#
Manager::reachable_node_count

source
fn Manager::reachable_node_count(self : Manager, value : Bdd) -> Result[Int, BddError]

#
Manager::reorder

source
fn Manager::reorder(self : Manager, value : Bdd, order : Array[String]) -> Result[ReorderResult, BddError]

#
Manager::restrict

source
fn Manager::restrict(self : Manager, value : Bdd, assignments : Array[(String, Bool)]) -> Result[Bdd, BddError]

#
Manager::retained_node_count

source
fn Manager::retained_node_count(self : Manager) -> Int

#
Manager::sat_count_decimal

source
fn Manager::sat_count_decimal(self : Manager, value : Bdd) -> Result[String, BddError]

#
Manager::sat_count_u64

source
fn Manager::sat_count_u64(self : Manager, value : Bdd) -> Result[UInt64, BddError]

#
Manager::sat_one

source
fn Manager::sat_one(self : Manager, value : Bdd) -> Result[Model?, BddError]

#
Manager::state_encoding

source
fn Manager::state_encoding(self : Manager, current : Array[String], next : Array[String]) -> Result[StateEncoding, BddError]

#
Manager::statistics

source
fn Manager::statistics(self : Manager, value : Bdd) -> Result[BddStatistics, BddError]

#
Manager::support

source
fn Manager::support(self : Manager, value : Bdd) -> Result[Array[String], BddError]

#
Manager::to_dot

source
fn Manager::to_dot(self : Manager, value : Bdd, root_name : String) -> Result[String, BddError]

Export reachable structure as deterministic Graphviz DOT.

#
Manager::true_bdd

source
fn Manager::true_bdd(self : Manager) -> Bdd

#
Manager::truth_table

source
fn Manager::truth_table(self : Manager, value : Bdd, maximum_rows : Int) -> Result[TruthTable, BddError]

#
Manager::validate

source
fn Manager::validate(self : Manager, value : Bdd) -> Result[Unit, BddError]

#
Manager::variable

source
fn Manager::variable(self : Manager, name : String) -> Result[Bdd, BddError]

#
Manager::variable_count

source
fn Manager::variable_count(self : Manager) -> Int

#
Manager::variable_names

source
fn Manager::variable_names(self : Manager) -> Array[String]

#
Manager::xor_bdd

source
fn Manager::xor_bdd(self : Manager, left : Bdd, right : Bdd) -> Result[Bdd, BddError]

#
Model

source
pub(all) struct Model {
  values : Array[(String, Bool)]
} derive(Eq, 
Debug)

One complete assignment in the Manager's Variable Order.

#
ModelEnumeration

source
pub(all) struct ModelEnumeration {
  models : Array[Model]
  complete : Bool
} derive(Eq, 
Debug)

Bounded Model enumeration result. complete is false when more Models exist.

#
NamedConstraint

source
pub(all) struct NamedConstraint {
  name : String
  expression : String
} derive(Eq, 
Debug)

One named Boolean expression in a Constraint Set.

#
NodeKey

source
type NodeKey derive(Eq, Hash)

#
ParseDiagnostic

source
pub(all) struct ParseDiagnostic {
  offset : Int
  message : String
} derive(Eq, 
Debug)

One stable source-positioned expression diagnostic.

#
PartialValue

source
pub(all) enum PartialValue {
  AlwaysFalse
  AlwaysTrue
  Undetermined
} derive(Eq, 
Debug)

Result of evaluating a Boolean Function under a potentially incomplete assignment. Undetermined means both outcomes remain possible.

#
ReachabilityResult

source
pub(all) struct ReachabilityResult {
  reachable : Bdd
  iterations : Int
  fixed_point : Bool
  invariant_holds : Bool
  witness : Model?
}

Result of bounded finite symbolic reachability.

#
RelationCheck

source
pub(all) struct RelationCheck {
  holds : Bool
  witness : Model?
} derive(Eq, 
Debug)

Outcome of a Boolean relation check. When holds is false, witness contains a complete assignment demonstrating the failure.

#
ReorderResult

source
pub(all) struct ReorderResult {
  manager : Manager
  root : Bdd
  before_nodes : Int
  after_nodes : Int
  attempted_orders : Int
}

Result of non-destructive Variable reordering.

#
ResourceBudget

source
pub(all) struct ResourceBudget {
  max_nodes : Int
  max_cache_entries : Int
  max_work : Int
  max_input_bytes : Int
  max_depth : Int
  max_models : Int
  max_constraints : Int
  max_analysis_steps : Int
  max_output_bytes : Int
  max_reorder_attempts : Int
  max_iterations : Int
} derive(Eq, 
Debug)

Explicit limits for operations whose time or retained state can grow exponentially. Every value must be positive.

#
ResourceBudget::default

source

#
StateEncoding

source
pub struct StateEncoding {
  owner : Manager
  current : Array[String]
  next : Array[String]
}

Validated pairing of current-state and next-state Boolean Variables.

#
StateEncoding::current_variables

source
fn StateEncoding::current_variables(self : StateEncoding) -> Array[String]

#
StateEncoding::next_variables

source
fn StateEncoding::next_variables(self : StateEncoding) -> Array[String]

#
TruthRow

source
pub(all) struct TruthRow {
  values : Array[(String, Bool)]
  result : Bool
} derive(Eq, 
Debug)

One complete row in Manager Variable Order.

#
TruthTable

source
pub(all) struct TruthTable {
  rows : Array[TruthRow]
  complete : Bool
} derive(Eq, 
Debug)

Bounded deterministic Truth Table. complete is false when the caller's row limit stopped enumeration before all complete assignments were emitted.

#
artifact_schema_version

source
let artifact_schema_version : Int

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io