Z3 encoder and seven core satisfiability checks (decidability Step 2)#63

Merged

rmichaelthomas merged 7 commits into

mainfrom

feat/z3-encoder-and-core-checks

Jul 20, 2026

Commits on Jul 20, 2026

Add Z3 checker packaging: check extra, lazy import, CheckerUnavailable

rmichaelthomas
and
claude
committed
Add Z3 encoder sort model and constant allocation

rmichaelthomas
and
claude
committed
Add Z3 condition encoder: operators, within, includes, predicates

rmichaelthomas
and
claude
committed
Add arithmetic encoding, name inlining, and nonlinearity detection

rmichaelthomas
and
claude
committed
Add deontic statement effect formulas

rmichaelthomas
and
claude
committed
Add the seven core satisfiability checks

rmichaelthomas
and
claude
committed
Add check_agreement public API

rmichaelthomas
and
claude
committed