Per.DNF (per v5.3.21)

Surface-level OR formula constructor with basic simplifications. Disjunction of conjunctions. Conjunction is a pair of integers {mask, values}. Disjunction is a MapSet of conjunction pairs.

solve(v, val, index \\ nil)

Solves a formula for a given value (1 or 0), returning a disjunction.

to_bits(map, index)

Converts a face map to a bitset representation.

unions(t1, t2)

Computes intersection of two disjunctions (distributes AND over OR).

uniq(t)

Removes redundant conjunctions from a disjunction.

Functions

and_formula(a, b)

Surface-level AND formula constructor with basic simplifications.

contr_and(t)

contr_and(arg, inv_index)

Converts a conjunction back to an AST formula.

contr_atom(arg)

contr_atom(arg, inv_index)

Converts a conjunction element back to an AST formula.

contr_or(t, index \\ nil)

Converts a disjunction back to an AST formula.

eval_and(a, b)

Evaluates AND of two formulas via DNF.

eval_or(a, b)

Evaluates OR of two formulas via DNF.

ext_and(v)

Extracts conjunction (map) from an AND-formula.

ext_and_bits(v, index)

Extracts conjunction (bitset) from an AND-formula.

ext_or(v, index \\ nil)

Extracts disjunction (Set of conjunctions) from a formula.

from_bits(arg, inv_index)

Converts a bitset representation back to a face map.

getFaceV(face)

Converts a face map to an AST formula value.

getFormulaV(map)

Converts a system map to an AST formula value.

logic_eq(v1, v2)

Checks if two formulas are logically equivalent.

meet(f1, f2)

Computes intersection of two conjunctions.

meets(xs, ys)

Intersection of two lists of faces.

neg_conjunction(c, index)

Computes the negation of a conjunction.

neg_disjunction(d, index \\ nil)

Computes the negation of a disjunction.

neg_formula(v, index \\ nil)

Computes the negation of a formula.

or_formula(a, b)