🥮 mooncakes.io

    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