Add on-demand zero lemmas for MCSAT-supplement nonlinear relaxation

[ahmed-irfan]

Summary

• Each nonlinear monomial abstracted for simplex (mcsat_relax_pprod) now also gets on-demand "zero lemma" clauses relating the abstraction variable z to its factors (z=0 <-> some factor=0), checked against live simplex values from propagate/final_check:
  • xi=0 while z≠0 → not(xi=0) or (z=0)
  • z=0 while every factor is confirmed nonzero → not(z=0) or (x1=0) or ... or (xk=0)
• Checking is gated by the existing mcsat-supplement-check parameter (both/final-only), same as the expensive nested-MCSAT check it complements — no new config surface.
• Atoms for the lemma are pre-built once, eagerly, at abstraction time (base decision level), since simplex only supports creating new theory atoms there, not mid-search; the on-demand check only ever looks up and combines those cached literals into new clauses. A per-monomial "done" bitmask prevents re-adding the same clause every round, since these literals are typically fresh/unassigned and nothing else forces the search to move past a repeated violation.
• The mid-search checking logic lives in a new file, context_mcsat_relax.c, following the existing context_solver.c/context_simplifier.c pattern of sharing context_t internals via context_utils.h. Only the atom/monomial construction logic (mcsat_relax_pprod and friends) stays in context.c, since it's tightly coupled to the rest of the internalization pass there.

Test plan

• make MODE=debug bin — clean build
• make mcsat-check — 700/700 pass
• make check — 1731/1731 pass
• tests/api/test_cdclt_mcsat_supplement.c — passes
• Manual probes confirming correct SAT/UNSAT results for monomials with factors referenced nowhere else in the problem (e.g. x²y³z), including under mcsat-supplement-check=final-only

[coveralls]

coverage: 69.922% (+0.02%) from 69.901% — mcsat-relax-zero-lemmas into master