Skip to main content

Module t1

Module t1 

Source
Expand description

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

Structsยง

Linearized
A linearized representation of a system of constraints. Non-linear atoms get fresh Vars and names like X*Y or Z^2.
Z3
A cached Z3 pipe, using either the command line or a JavaScript callback.