Crate mago_algebra 

Modules

assertion_set

clause

Structs

AlgebraThresholds

Configuration thresholds for CNF formula operations.

Constants

DEFAULT_CONSENSUS_LIMIT

Default upper limit for consensus optimization.

DEFAULT_DISJUNCTION_COMPLEXITY

Default maximum clauses per side in disjunction operations.

DEFAULT_NEGATION_COMPLEXITY

Default maximum cumulative complexity during negation.

DEFAULT_SATURATION_COMPLEXITY

Default maximum clauses during CNF saturation.

Functions

disjoin_clauses

Performs a logical OR (disjunction) on two sets of CNF clauses.

find_satisfying_assignments

Extracts simple assertions from a set of clauses and identifies which are “active”.

negate_formula

Computes the logical negation of a formula in Conjunctive Normal Form (CNF).

saturate_clauses

Reduces a set of CNF clauses by exhaustively applying logical simplification rules.

Type Aliases

ActiveTruths

SatisfyingAssignments