[solver] On model-refutation, block the assignment and continue instead of Unknown #40

Summary

When a theory-accepted trail fails concrete evaluation (model_refutes_assertions), v0.3.2 returns Unknown immediately. Main’s fc810843 instead learns a blocking clause over the current decision assignment and continues searching (bounded).

Main behaviour (fc810843 perf(lia): fold define-fun reps and block refuted models)

// sketch of main's check loop
if self.model_refutes_assertions(manager) {
    if model_block_rounds < 256 && self.block_current_model() {
        model_block_rounds += 1;
        // backtrack to root, reset theories, continue CDCL(T)
        continue;
    }
    return SolverResult::Unknown;
}

block_current_model negates every true Reason::Decision literal on the trail into one clause and sat.add_clauses it — so that exact decision assignment is never revisited.

Measured on main for large discrete LIA after equality-ite table fold: dfem ~31–50s sat (was hang); qi_1_h1 with model ~14s sat.

0.3.2 behaviour

oxiz-solver/src/solver/check_core.rs (ground sat path):

if self.model_refutes_assertions(manager) {
    ...
    return SolverResult::Unknown;
}

Same pattern on several quantified / MBQI exit paths. Array-lemma refinement does continue after instantiating lemmas — but plain model-eval refutation does not block-and-continue.

Why it matters

Incomplete theories (and table-folded LIA) can accept trails that concrete eval rejects. Giving up with Unknown throws away all search progress; blocking the spurious model is the cheap way to keep completeness pressure on the Boolean core.

Suggested direction

Add a bounded block_current_model + continue path on the ground model_refutes_assertions failure (cap rounds, reset theory state the same way array-lemma refinement already does). Keep Unknown when nothing is blockable (level 0 / no decisions) or the cap is hit.