Module solver 

Some symbolic computation utilities based on the Poly abstraction.

All operations are exact. Coefficients are stored as i128s and panic on overflow.

Modules

count

Polynomial summation.

poly

A multivariable polynomial ring with integer coefficients.

t0

Try to prove a goal given only a non-negative variable list.

t1

Linearized systems of constraints and a pipe to Z3 for QF_LIA solving.

t2

Bounded-degree positivity certificates for non-linear goals.

Structs

Constraint

Format for facts and goals, e.g. X > 2*Y.

Solver

A consolidated t0 -> t1 -> t2 solving pipeline.

Enums

Cmp

Obligation vocabulary.

Verdict

Solver response. t0 refutations provide a trivial !goal given non-negative variables; t1 refutations provide a counterexample point; t2 is best-effort and cannot refute.

Type Aliases

Point