CAD and sign constraints¶
Use poly.cad to express real polynomial sign conditions, find witnesses, and decompose space from sparse coefficient arrays over integers, rationals, or AA.
Every computational operation has a shared Budget overload and a convenience
overload with max_steps=. Borrowed evidence is immutable. Decomposition and
full-covering evidence now uses CADFinalCertificate; copies share immutable
storage. Call its metadata methods instead of reading the old .projection,
.cells or .stacks fields. cad.cells explicitly materializes absolute
geometry, and cad.sample materializes only the requested satisfying path.
Both costs are charged to their caller. For AA, decomposition and solving
follow only the supplied coefficient values. The borrowed tree retains rational
projection and local stack evidence, with one selected section per coefficient
axis. Use cad.check or cad.checker to verify that restricted claim and its
binding to the original coefficients; ordinary full-space core checkers have a
different coverage requirement. The
workflow tutorial explains the raw stream
format and auxiliary axes.
Decomposition and full covering default to Brown–McCallum projection reductions
with Lazard lifting and the verified compact backend. lazard=True requests
plain Lazard on that backend;
lazard=False and restricted coordinate prefixes use checked legacy evidence.
solve and the streaming API retain their existing implementations.
Pass fixed=[(axis, value), ...] to restrict decomposition or solving to exact
coordinate values. decompose, solve, cover, decompose_to, and checker
accept homogeneous iterables or mixed tuples of axis/value pairs. Fixed axes
lead the traversal; samples retain every original axis and signs omit synthetic
binding polynomials. cad.check verifies coverage on that slice, including
its exact root choices. Use the same fixed= and axes= for a stream producer
and checker. Checked archives retain these bindings.
Constraint¶
@fieldwise_init
struct Constraint[P: Copyable & Deinitable](Copyable, Movable)
A sparse exact-real polynomial and the signs allowed for its value.
Construct constraints with negative, zero, positive, nonpositive, nonnegative, or nonzero. Every constraint compares the polynomial to zero.
Parameters.
P: The polynomial's sparse power shape.
Defined in src/poly/cad.mojo.
negative¶
def negative[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](values: I, mut budget: Budget) raises PolyError -> Constraint[P] where _Element[I] == Tuple[P, C]
Require a polynomial value to be less than zero.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.
Arguments.
values: An integer, rational, or real-algebraic sparse term iterable or prepared array.budget: The shared work allowance for preparation and computation.
Returns. A reusable constraint for solve; inputs remain unchanged.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
zero¶
def zero[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](values: I, mut budget: Budget) raises PolyError -> Constraint[P] where _Element[I] == Tuple[P, C]
Require a polynomial value to be equal to zero.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.
Arguments.
values: An integer, rational, or real-algebraic sparse term iterable or prepared array.budget: The shared work allowance for preparation and computation.
Returns. A reusable constraint for solve; inputs remain unchanged.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
positive¶
def positive[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](values: I, mut budget: Budget) raises PolyError -> Constraint[P] where _Element[I] == Tuple[P, C]
Require a polynomial value to be greater than zero.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.
Arguments.
values: An integer, rational, or real-algebraic sparse term iterable or prepared array.budget: The shared work allowance for preparation and computation.
Returns. A reusable constraint for solve; inputs remain unchanged.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
nonpositive¶
def nonpositive[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](values: I, mut budget: Budget) raises PolyError -> Constraint[P] where _Element[I] == Tuple[P, C]
Require a polynomial value to be less than or equal to zero.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.
Arguments.
values: An integer, rational, or real-algebraic sparse term iterable or prepared array.budget: The shared work allowance for preparation and computation.
Returns. A reusable constraint for solve; inputs remain unchanged.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
nonnegative¶
def nonnegative[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](values: I, mut budget: Budget) raises PolyError -> Constraint[P] where _Element[I] == Tuple[P, C]
Require a polynomial value to be greater than or equal to zero.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.
Arguments.
values: An integer, rational, or real-algebraic sparse term iterable or prepared array.budget: The shared work allowance for preparation and computation.
Returns. A reusable constraint for solve; inputs remain unchanged.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
nonzero¶
def nonzero[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](values: I, mut budget: Budget) raises PolyError -> Constraint[P] where _Element[I] == Tuple[P, C]
Require a polynomial value to be different from zero.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.
Arguments.
values: An integer, rational, or real-algebraic sparse term iterable or prepared array.budget: The shared work allowance for preparation and computation.
Returns. A reusable constraint for solve; inputs remain unchanged.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
Decomposition¶
@fieldwise_init
struct Decomposition[P: Copyable & Deinitable](_Archive, Copyable, Movable)
A sign-invariant decomposition at the supplied coefficients and fixed coordinates.
Parameters.
P: The input polynomials' power shape.
Defined in src/poly/cad.mojo.
Decomposition.evidence¶
def evidence(self) -> ref[ImmOrigin(origin_of(self._data[].proof))] CADFinalCertificate
Borrow the decomposition and its proof on the selected coordinate slice.
Returns. Immutable compact final evidence; use cad.check to verify its scope and cad.cells to request absolute geometry.
Solution¶
@fieldwise_init
struct Solution[P: Copyable & Deinitable](_Archive, Copyable, Movable)
A witness or a proof that a conjunction has no solution on the selected slice.
Parameters.
P: The constraints' shared sparse power shape.
Defined in src/poly/cad.mojo.
Solution.satisfiable¶
def satisfiable(self) -> Bool
Report whether the search found a point satisfying every constraint.
Returns. True for a witness, False for a covering proof of failure.
Solution.evidence¶
def evidence(self) -> ref[ImmOrigin(origin_of(self._data[].proof))] CADCoveringsCertificate
Borrow the coverings certificate: a satisfying point or a covering tree.
Returns. Immutable evidence for this conjunction, not a full decomposition.
decompose¶
def decompose[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](polynomials: I, mut budget: Budget, *, axes: List[Int] = List[Int](), lazard: Optional[Bool] = None) raises PolyError -> Decomposition[P] where _Element[_Nested[I]] == Tuple[P, C]
Decompose real space into cells where every input has a constant sign.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.
Arguments.
polynomials: A finite iterable of integer, rational, or real-algebraic sparse polynomials.budget: The shared work allowance for preparation and computation.axes: All axes in base-to-top order; defaults to increasing axis order.lazard: None selects Revision 15 with interval lifting and complete final verification; True requests plain Lazard, False uses the checked legacy McCallum backend.
Returns. The computed result, with its evidence retained.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
solve¶
def solve[I: Iterable, P: Copyable & Deinitable](constraints: I, mut budget: Budget, *, axes: List[Int] = List[Int](), lazard: Bool = True) raises PolyError -> Solution[P] where _Element[I] == Constraint[P]
Find a point satisfying every sign constraint, or prove none exists.
The constraints form a conjunction. Budget exhaustion raises and never masquerades as an unsatisfiable result.
Parameters.
I: The inferred input type.P: The inferred power shape.
Arguments.
constraints: A finite iterable of constraints sharing one power shape.budget: The shared work allowance for preparation and computation.axes: All axes in base-to-top order; defaults to increasing axis order.lazard: Use Lazard projection; False selects McCallum projection.
Returns. The computed result, with its evidence retained.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
check¶
def check[P: Copyable & Deinitable](result: Decomposition[P], mut budget: Budget) raises PolyError -> Bool
Verify the retained geometric claim independently.
Parameters.
P: The inferred power shape.
Arguments.
result: The original result with its input and certificate.budget: The shared work allowance for preparation and computation.
Returns. Whether the complete certificate supports the stated result.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
sample¶
def sample[P: Copyable & Deinitable](result: Solution[P], mut budget: Budget) raises PolyError -> Optional[List[Real]]
Extract a satisfying point in polynomial axis order.
Parameters.
P: The inferred power shape.
Arguments.
result: A selective sign-solving result.budget: The shared work allowance for preparation and computation.
Returns. Exact real coordinates, or None when the conjunction is unsatisfiable.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
Cell¶
@fieldwise_init
struct Cell(Copyable, Movable)
A terminal cell's dimension, exact sample point, and input signs.
Defined in src/poly/cad.mojo.
| Field | Type | |
|---|---|---|
index |
Int |
The corresponding cell index in the full decomposition certificate. |
dimension |
Int |
The number of sector choices along this cell's path. |
sample |
List[Real] |
An exact sample point in polynomial axis order. |
signs |
List[Int] |
Minus one, zero, or one in original input polynomial order. |
cells¶
def cells[P: Copyable & Deinitable](result: Decomposition[P], mut budget: Budget) raises PolyError -> List[Cell]
Describe every terminal cell using its dimension, sample, and signs.
Parameters.
P: The inferred power shape.
Arguments.
result: A full decomposition.budget: The shared work allowance for preparation and computation.
Returns. Cells in certificate order. Samples name cells; the full certificate proves their geometry.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
fixed_coordinates¶
def fixed_coordinates[P: Copyable & Deinitable](result: Decomposition[P], mut budget: Budget) raises PolyError -> List[Tuple[Int, Real]]
Copy the user-fixed axes and exact values in traversal order.
Parameters.
P: The inferred polynomial power shape.
Arguments.
result: The retained CAD result.budget: The shared work allowance, including output storage.
Returns. Independent axis/value pairs; empty when no user coordinates were fixed.
Raises.
PolyError: LIMIT or CAPACITY when resource limits are reached.
Defined in src/poly/cad.mojo.
decompose_to¶
def decompose_to[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable, S: CADSink](polynomials: I, mut sink: S, mut budget: Budget, *, axes: List[Int] = List[Int](), lazard: Bool = True) raises PolyError -> CADStreamReceipt where _Element[_Nested[I]] == Tuple[P, C]
Stream projection and cell witnesses without retaining their full history.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.S: The inferred input type.
Arguments.
polynomials: The integer, rational, or real-algebraic sparse polynomial inputs.sink: The consumer of projection and depth-first witness events.budget: The shared work allowance for preparation and computation.axes: All axes in base-to-top order.lazard: Use Lazard projection by default.
Returns. A completion receipt. Events written before an error do not prove a complete decomposition.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
checker¶
def checker[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](polynomials: I, mut budget: Budget) raises PolyError -> _Checker[_Kind[C]] where _Element[_Nested[I]] == Tuple[P, C]
Prepare independent incremental checking of a decomposition stream.
Parameters.
I: The inferred input type.P: The inferred power shape.C: The inferred input type.
Arguments.
polynomials: The original input polynomials.budget: The shared work allowance for preparation and computation.
Returns. A checker accepting streamed events; finish(receipt, budget) verifies complete traversal.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
Projection, selected cells, and lifting¶
The specialized workflows tutorial explains axis order and how to consume lifting coefficients.
Projection¶
@fieldwise_init
struct Projection[P: Copyable & Deinitable, k: Int = 1](_Archive, Copyable, Movable)
A retained CAD projection closure in an explicit axis order.
Parameters.
P: The original sparse power shape.k: The inferred real coefficient field; normally left implicit.
Defined in src/poly/cad.mojo.
Projection.evidence¶
def evidence(self) -> ref[ImmOrigin(origin_of(self._data[].proof))] CADProjectionCertificate
Borrow the retained core evidence.
Returns. An immutable certificate bound to the original inputs.
CellAt¶
@fieldwise_init
struct CellAt[P: Copyable & Deinitable](_Archive, Copyable, Movable)
A certified sign-invariant cell containing the supplied exact point.
Parameters.
P: The original sparse power shape.
Defined in src/poly/cad.mojo.
CellAt.evidence¶
def evidence(self) -> ref[ImmOrigin(origin_of(self._data[].proof))] CADCellCertificate
Borrow the retained core evidence.
Returns. An immutable certificate bound to the original inputs.
Lazard¶
@fieldwise_init
struct Lazard[P: Copyable & Deinitable](_Archive, Copyable, Movable)
A lifting polynomial with certified vanishing orders.
Parameters.
P: The original sparse power shape.
Defined in src/poly/cad.mojo.
Lazard.evidence¶
def evidence(self) -> ref[ImmOrigin(origin_of(self._data[].proof))] LazardEvaluationCertificate
Borrow the retained core evidence.
Returns. An immutable certificate bound to the original inputs.
Covering¶
@fieldwise_init
struct Covering[P: Copyable & Deinitable](_Archive, Copyable, Movable)
A full-decomposition feasibility witness or conflict covering.
Parameters.
P: The original sparse power shape.
Defined in src/poly/cad.mojo.
Covering.evidence¶
def evidence(self) -> ref[ImmOrigin(origin_of(self._data[].proof))] CADFinalCertificate
Borrow the retained core evidence.
Returns. An immutable certificate bound to the original inputs.
Covering.satisfiable¶
def satisfiable(self) -> Bool
Report whether the covering contains a satisfying witness cell.
Returns. True for a witness; verify the claim with cad.check.
project¶
def project[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable](polynomials: I, mut budget: Budget, *, axes: List[Int] = List[Int](), lazard: Bool = True) raises PolyError -> Projection[P, _FieldKind[_Kind[C]]] where _Element[_Nested[I]] == Tuple[P, C]
Compute a CAD projection closure without constructing lifted cells.
Parameters.
I: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.C: Inferred from the input types unless explicitly supplied.
Arguments.
polynomials: A finite iterable of integer, rational, or real-algebraic sparse polynomials.budget: The shared work allowance, including preparation and output storage.axes: All axes in base-to-top cylindrical order; empty uses increasing order.lazard: Use Lazard projection; False selects McCallum projection.
Returns. A projection result with independently checkable closure and basis evidence.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
cell_at¶
def cell_at[I: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable, A: Iterable](polynomials: I, point: A, mut budget: Budget, *, axes: List[Int] = List[Int](), lazard: Bool = True) raises PolyError -> CellAt[P] where _Element[_Nested[I]] == Tuple[P, C]
Construct only the CAD cell path containing an exact query point.
Coordinates use original polynomial axis order, even when axes changes the CAD traversal order.
Parameters.
I: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.C: Inferred from the input types unless explicitly supplied.A: Inferred from the input types unless explicitly supplied.
Arguments.
polynomials: A finite iterable of integer, rational, or real-algebraic sparse polynomials.point: The scalar argument or coordinates in original axis order.budget: The shared work allowance, including preparation and output storage.axes: All axes in base-to-top cylindrical order; empty uses increasing order.lazard: Use Lazard projection; False selects McCallum projection.
Returns. A cell result retaining query-point containment and constant-sign evidence.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
lazard_evaluate¶
def lazard_evaluate[I: Iterable, A: Iterable, P: Copyable & Deinitable, C: Copyable & Deinitable, X: Copyable & Deinitable](values: I, assignments: A, mut budget: Budget, *, axis: Int = 0) raises PolyError -> Lazard[P] where _Element[I] == Tuple[P, C] and _Element[A] == Tuple[Int, X]
Remove vanishing factors before ordered algebraic substitutions.
Assignments follow base-to-top cylindrical order and must leave the lifting axis unassigned.
Parameters.
I: Inferred from the input types unless explicitly supplied.A: Inferred from the input types unless explicitly supplied.P: Inferred from the input types unless explicitly supplied.C: Inferred from the input types unless explicitly supplied.X: Inferred from the input types unless explicitly supplied.
Arguments.
values: Input coefficients, sparse terms, or a prepared array.assignments: Distinct axis and exact-value pairs in the required order.budget: The shared work allowance, including preparation and output storage.axis: The zero-based polynomial axis.
Returns. Certified vanishing orders and a nonzero lifting polynomial up to positive factorials.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
cover¶
def cover[I: Iterable, P: Copyable & Deinitable](constraints: I, mut budget: Budget, *, axes: List[Int] = List[Int](), lazard: Optional[Bool] = None) raises PolyError -> Covering[P] where _Element[I] == Constraint[P]
Decide sign constraints using a complete CAD decomposition.
The result retains the full decomposition and a witness or conflict covering. Use solve when a selective search is sufficient.
Parameters.
I: The inferred input type.P: The inferred power shape.
Arguments.
constraints: A finite iterable of constraints sharing one power shape.budget: The shared work allowance for preparation and computation.axes: All axes in base-to-top order; defaults to increasing axis order.lazard: None selects Revision 15 with interval lifting and complete final verification; True requests plain Lazard, False uses the checked legacy McCallum backend.
Returns. The computed result, with its evidence retained.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable operation, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
projection_polynomials¶
def projection_polynomials[P: Copyable & Deinitable, k: Int](result: Projection[P, k], mut budget: Budget, *, axis: Int = -1) raises PolyError -> List[sparse.Array[P, k]]
Copy projection basis polynomials for one axis or the complete closure.
Parameters.
P: Inferred from the input types unless explicitly supplied.k: The inferred real coefficient field.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.axis: The original polynomial axis; -1 collects every level in CAD order.
Returns. Independent sparse arrays retaining all original axes.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
signs¶
def signs[P: Copyable & Deinitable](result: CellAt[P], mut budget: Budget) raises PolyError -> List[Int]
Return the constant input-polynomial signs on the selected cell.
Parameters.
P: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. Minus one, zero or one for each input polynomial in input order.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
vanishing_orders¶
def vanishing_orders[P: Copyable & Deinitable](result: Lazard[P], mut budget: Budget) raises PolyError -> List[Tuple[Int, Int]]
Copy the minimal vanishing order for each assigned variable.
Parameters.
P: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. Axis and vanishing-order pairs in the original assignment order.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.
lifting_coefficients¶
def lifting_coefficients[P: Copyable & Deinitable](result: Lazard[P], mut budget: Budget) raises PolyError -> List[Real]
Copy ascending exact-real coefficients of the Lazard lifting polynomial.
Parameters.
P: Inferred from the input types unless explicitly supplied.
Arguments.
result: The result retaining its original inputs and evidence.budget: The shared work allowance, including preparation and output storage.
Returns. Exact coefficients usable directly with dense.real_roots; verify the Lazard result with cad.check.
Raises.
PolyError: DOMAIN for incompatible input, UNSUPPORTED for an unavailable coefficient domain, or LIMIT/CAPACITY on resource limits.
Defined in src/poly/cad.mojo.