🥮 mooncakes.io
README

marianoguerra/wax/cond does not have a README file

#
Atom

source

An atom: one variable against one constant.

The order theory is normalized the way a total-order theory has to be, and the way the reference's Leq does: an atom is always an upper bound, and the lower bounds are its negations. vid > v is not (vid <= v), and vid = v is vid <= v and not (vid < v). That is what keeps the atom set small enough for the search to be trivial.

#
Env

source
pub struct Env {
  bool_vars : Map[String, Int]
  version_vars : Map[String, Int]
  string_vars : Map[String, Int]
  names : Map[Int, String]
  next_var : Int
  var_kind : Map[String, String]
  reported : Map[(Int, Int), Unit]
}

Per-module solver state: variable interning, the kind each name is used at, and deduplication of ill-formed-condition diagnostics.

One Env per module, so nothing leaks between modules processed in the same run.

#
Env::explain

source
fn Env::explain(self : Env, f : T, style? : Style) -> String?

A minimal assumption under which the formula holds -- e.g. $oxcaml and not $debug.

None when the formula is a tautology (always reachable, so there is nothing to assume) or unsatisfiable (no assumption would do).

The reference asks its BDD for a shortest satisfying cube. Here a satisfying assignment is found first and then minimized greedily: a literal whose removal still leaves the remaining conjunction entailing the formula was not carrying its weight. Greedy gives a minimal cube, not necessarily the globally shortest one -- for a handful of atoms the two coincide, and this is diagnostic text rather than a decision.

#
Env::new

source
fn Env::new() -> Env

#
Env::of_cond

source

Translate a condition, interning its variables.

A condition that cannot be modelled is reported (once per source location) and becomes a fresh unconstrained variable, so that exploration proceeds rather than stopping at the first unmodelable branch. location is the enclosing conditional, used when a sub-condition carries no span of its own.

#
Node

source

A boolean formula over atoms.

#
Style

source
pub(all) enum Style {
  Wat
  Wax
} derive(Eq, 
Debug)

Which surface syntax to render in.

The two spell conditions differently: WAT uses $-prefixed variables, dotted versions and <>; Wax uses bare names, version tuples and !=.
pub struct T {
  node : Node
}

A formula over condition variables.

#
Version

source
pub(all) struct Version {
  major : Int
  minor : Int
  patch : Int
} derive(Eq, Hash, 
Debug)

A version triple, ordered lexicographically.
impl Show for Version

#
Version::compare_to

source
fn Version::compare_to(self : Version, other : Version) -> Int

#
and_

source
fn and_(a : T, b : T) -> T

Conjunction, with the constant folding that keeps formulas small.

#
canonical_key

source
fn canonical_key(f : T) -> String

A canonical STRUCTURAL key, for deduplicating formulas in a table.

equal is semantic and hash is therefore a constant, which is correct but useless as a hash key. The exploration driver needs to ask "have I seen this assumption before?" thousands of times, and answering it semantically would be a satisfiability query per comparison.

So this is the weaker question, asked cheaply: two formulas share a key when they are the same up to the commutativity, associativity and idempotence of and and or, which is what actually varies between assumptions built in different branch orders. Equal keys imply equivalence; different keys do not imply inequivalence.

That asymmetry is safe for a dedup set and only there: missing a duplicate costs one more configuration explored, never a wrong answer. It would not be safe for anything that treats "not seen" as "not implied".

#
equal

source
fn equal(a : T, b : T) -> Bool

Are the two formulas equivalent?

Semantic, matching the reference, where equality is BDD identity and BDDs are canonical. Here it is two satisfiability queries instead.

#
false_

source
let false_ : T

#
hash

source
fn hash(_ : T) -> Int

A hash consistent with equal.

Semantically equal formulas must hash alike, and without a canonical form there is nothing cheap to hash that respects that -- so this is a constant. Correct, and degenerate: a hash table keyed on formulas degrades to a list.

The exploration driver does need to dedup assumptions, and asks the weaker structural question instead -- see canonical_key, which is cheap and whose asymmetry is safe for exactly that use.

#
is_satisfiable

source
fn is_satisfiable(f : T) -> Bool

Does the formula have a satisfying assignment?

Theory-aware, so contradictory version bounds are unsatisfiable rather than merely unlikely.

#
logical_implies

source
fn logical_implies(a : T, b : T) -> Bool

Does a entail b?

#
not_

source
fn not_(f : T) -> T

#
or_

source
fn or_(a : T, b : T) -> T

#
true_

source
let true_ : T

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io