z3-src 503.3.0

/*++
Copyright (c) 2026 Romain Soulat

Module Name:

    ff_solver.cpp

Abstract:

    Frontend-independent finite-field reasoning tests. These exercise the
    reusable interface directly, without a smt::context or SAT solver.

--*/
#include "ast/ff/ff_solver.h"
#include "ast/ff/ff_evidence.h"
#include "ast/proofs/proof_checker.h"
#include "ast/reg_decl_plugins.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "util/debug.h"
#include "util/z3_exception.h"
#include "tactic/ff/ff_solve_tactic.h"
#include "tactic/tactic.h"
#include "solver/solver.h"
#include "solver/simplifier_solver.h"
#include "ast/simplifiers/ff_simplify.h"

namespace {
    void recording_contract() {
        ast_manager m(PGM_ENABLED);
        reg_decl_plugins(m);
        ff_util ff(m);
        sort_ref field(ff.mk_sort(rational(7)), m);
        expr_ref x(m.mk_const("proof.x", field), m);
        expr_ref zero(ff.mk_numeral(rational(0), field), m);
        expr_ref one(ff.mk_numeral(rational(1), field), m);
        params_ref params;
        ff::solver unsat(m, field, params);
        unsat.add(x, zero, true);
        unsat.add(x, one, true);
        ENSURE(unsat.check(true) == l_false);
        ENSURE(unsat.evidence());
        ENSURE(ff::check_refutation(m, unsat.evidence()));
        ENSURE(unsat.conflict().size() == 2);
        // A recorded conflict must contain exactly the assumptions used by
        // its PAC DAG. Irrelevant premises otherwise make theory clauses much
        // wider and can prevent SAT search from reusing the contradiction.
        expr_ref y(m.mk_const("proof.y", field), m);
        ff::solver sparse(m, field, params);
        sparse.add(x, zero, true);
        sparse.add(x, one, true);
        sparse.add(y, zero, true);
        ENSURE(sparse.check(true) == l_false);
        ENSURE(ff::check_refutation(m, sparse.evidence()));
        ENSURE(sparse.conflict() == std::set<unsigned>({0, 1}));
        ENSURE(ff::refutation_clause(m, sparse.evidence()).size() == 2);
        app *evidence = sparse.evidence();
        expr *forged_args[] = {evidence->get_arg(0), evidence->get_arg(1),
                               m.mk_app(symbol("ff-support"), 0, nullptr, m.mk_proof_sort())};
        app_ref forged(m.mk_app(symbol("ff-pac"), 3, forged_args, m.mk_proof_sort()), m);
        ENSURE(!ff::check_refutation(m, forged));
        arith_util arith(m);
        expr *all_indices[] = {arith.mk_int(0), arith.mk_int(1), arith.mk_int(2)};
        forged_args[2] = m.mk_app(symbol("ff-support"), 3, all_indices, m.mk_proof_sort());
        forged = m.mk_app(symbol("ff-pac"), 3, forged_args, m.mk_proof_sort());
        ENSURE(!ff::check_refutation(m, forged));
        ff::solver sat(m, field, params);
        sat.add(x, one, true);
        ENSURE(sat.check(true) == l_true);
        ENSURE(sat.value(x) == rational(1));
        ENSURE(!sat.evidence());

        // A proof returned by ordinary SMT solving must retain its field
        // evidence after the solver and its assignment trail are destroyed.
        proof_ref retained(m);
        {
            scoped_ptr<solver> ordinary = mk_smt2_solver(m, params, symbol("QF_FF"));
            expr_ref three(ff.mk_numeral(rational(3), field), m);
            ordinary->assert_expr(m.mk_eq(ff.mk_mul(x, x), three));
            ENSURE(ordinary->check_sat() == l_false);
            retained = ordinary->get_proof();
        }
        ENSURE(retained && m.is_false(m.get_fact(retained)));
        proof_checker checker(m);
        expr_ref_vector side_conditions(m);
        ENSURE(checker.check(retained, side_conditions));
        th_rewriter rw(m);
        for (expr *condition : side_conditions) {
            expr_ref simplified(m);
            rw(condition, simplified);
            ENSURE(m.is_true(simplified) || ff::check_polynomial_rewrite(m, condition));
        }
        bool found_field_lemma = false;
        ptr_vector<expr> pending;
        expr_mark seen;
        pending.push_back(retained);
        while (!pending.empty()) {
            expr *current = pending.back(); pending.pop_back();
            if (seen.is_marked(current)) continue;
            seen.mark(current, true);
            if (!is_app(current)) continue;
            auto *step = to_app(current);
            if (step->get_family_id() == m.get_basic_family_id() && step->get_decl_kind() == PR_TH_LEMMA &&
                step->get_decl()->get_parameter(0).get_symbol() == symbol("ff")) {
                ENSURE(ff::check_refutation_lemma(m, step));
                found_field_lemma = true;
            }
            for (expr *child : *step) pending.push_back(child);
        }
        ENSURE(found_field_lemma);

        for (bool incremental_simplifier : {false, true}) {
            scoped_ptr<solver> ordinary = mk_smt2_solver(m, params, symbol("QF_FF"));
            if (incremental_simplifier) {
                simplifier_factory factory = [](ast_manager &manager, params_ref const &p,
                                                dependent_expr_state &state) {
                    return alloc(ff_basic_simplifier, manager, p, state);
                };
                ordinary = mk_simplifier_solver(ordinary.detach(), &factory);
            }
            ordinary->assert_expr(m.mk_eq(x, one));
            ordinary->push();
            expr_ref three(ff.mk_numeral(rational(3), field), m);
            ordinary->assert_expr(m.mk_eq(x, three));
            ENSURE(ordinary->check_sat() == l_false);
            expr_ref_vector obligations(m);
            ENSURE(checker.check(ordinary->get_proof(), obligations));
            ordinary->pop(1);
            ENSURE(ordinary->check_sat() == l_true);
            expr *assumptions[] = {m.mk_eq(x, three)};
            ENSURE(ordinary->check_sat(1, assumptions) == l_false);
            obligations.reset();
            ENSURE(checker.check(ordinary->get_proof(), obligations));
            ENSURE(ordinary->check_sat() == l_true);
        }
    }

    bool holds(ast_manager &m, expr *formula, expr *x, expr *y, unsigned a, unsigned b) {
        ff_util ff(m);
        expr_safe_replace subst(m);
        expr_ref ax(ff.mk_numeral(rational(a), x->get_sort()), m);
        expr_ref by(ff.mk_numeral(rational(b), y->get_sort()), m);
        subst.insert(x, ax);
        subst.insert(y, by);
        expr_ref value(formula, m);
        subst(value);
        th_rewriter rw(m);
        rw(value);
        ENSURE(m.is_true(value) || m.is_false(value));
        return m.is_true(value);
    }

    void exhaustive_problems() {
        ast_manager m;
        reg_decl_plugins(m);
        ff_util ff(m);
        unsigned checked = 0;
        for (unsigned prime : {2u, 3u, 7u}) {
            sort_ref field(ff.mk_sort(rational(prime)), m);
            expr_ref x(m.mk_const("x", field), m), y(m.mk_const("y", field), m);
            expr_ref product(ff.mk_mul(x, y), m), sum(ff.mk_add(x, y), m);
            ff::ff_encoding_cache cache(m, field);
            ff::basis_cache basis;
            // Reuse pure encodings while changing all input equations. Test
            // compact encodings too: their fresh definitions must stay local.
            for (bool preprocess : {false, true})
              for (bool compact : {false, true})
                for (unsigned a = 0; a < prime; ++a)
                    for (unsigned b = 0; b < prime; ++b) {
                        params_ref params;
                        params.set_bool("ff.compact_encoding", compact);
                        params.set_bool("solve_eqs", preprocess);
                        ff::solver core(m, field, params, &cache, &basis);
                        expr_ref ca(ff.mk_numeral(rational(a), field), m);
                        expr_ref cb(ff.mk_numeral(rational(b), field), m);
                        core.add(product, ca, true);
                        core.add(sum, cb, true);
                        core.add(x, cb, false);
                        bool exists = false;
                        for (unsigned u = 0; u < prime; ++u)
                            for (unsigned v = 0; v < prime; ++v)
                                exists |= u*v % prime == a && (u+v) % prime == b && u != b;
                        lbool result = core.check();
                        ENSURE(result == (exists ? l_true : l_false));
                        if (exists) {
                            rational u = core.value(x), v = core.value(y);
                            ENSURE(mod(u*v, rational(prime)) == rational(a));
                            ENSURE(mod(u+v, rational(prime)) == rational(b));
                            ENSURE(u != rational(b));
                        }
                        else {
                            // Check only the reported supporting premises by
                            // exhaustive enumeration, independently of algebra.
                            for (unsigned u = 0; u < prime; ++u)
                                for (unsigned v = 0; v < prime; ++v) {
                                    bool witness = true;
                                    for (unsigned index : core.conflict()) {
                                        ENSURE(index < 3);
                                        witness &= holds(m, core.premise(index), x, y, u, v);
                                    }
                                    ENSURE(!witness);
                                }
                        }
                        ++checked;
                    }
            ENSURE(cache.size() > 0);
            cache.reset();
            ENSURE(cache.size() == 0);
        }
        ENSURE(checked == 248);
    }

    void interface_and_scope_contract() {
        ast_manager m;
        reg_decl_plugins(m);
        ff_util ff(m);
        sort_ref field(ff.mk_sort(rational(7)), m), other(ff.mk_sort(rational(11)), m);
        expr_ref x(m.mk_const("x", field), m), y(m.mk_const("y", field), m);
        expr_ref z(m.mk_const("z", field), m);
        expr_ref zero(ff.mk_numeral(rational(0), field), m), one(ff.mk_numeral(rational(1), field), m);
        expr_ref square(ff.mk_mul(x, x), m);
        ff::ff_encoding_cache cache(m, field);
        ff::basis_cache basis;
        params_ref params;
        {
            ff::solver core(m, field, params, &cache, &basis);
            core.add(y, square, true);
            core.add(z, ff.mk_add(y, one), true);
            core.add(x, zero, true);
            core.add(z, one, false);
            ENSURE(core.check() == l_false);
            // All four premises are necessary in F7; no scope-local definition
            // may disappear from the explanation of the contradiction.
            ENSURE(core.conflict().size() == 4);
        }
        {
            ff::solver core(m, field, params, &cache, &basis);
            core.add(z, zero, true);
            ENSURE(core.check() == l_true && core.value(z).is_zero());
            bool rejected = false;
            try { core.add(z, one, true); }
            catch (default_exception const &) { rejected = true; }
            ENSURE(rejected);
        }
        bool rejected = false;
        try { ff::solver wrong(m, other, params, &cache); }
        catch (default_exception const &) { rejected = true; }
        ENSURE(rejected);
        // Foreign terms are opaque field leaves, including non-field arguments.
        // A mock frontend supplies their congruence equality as an explicit fact.
        sort* domain[] = {m.mk_bool_sort()};
        func_decl_ref f(m.mk_func_decl(symbol("f"), 1, domain, field), m);
        expr_ref a(m.mk_app(f, m.mk_true()), m), b(m.mk_app(f, m.mk_false()), m);
        {
            ff::solver core(m, field, params, &cache);
            core.add(a, zero, true); core.add(b, one, true);
            ENSURE(core.check() == l_true);
            ENSURE(core.value(a).is_zero() && core.value(b).is_one());
        }
        {
            ff::solver core(m, field, params, &cache);
            core.add(a, zero, true); core.add(b, one, true); core.add(a, b, true);
            ENSURE(core.check() == l_false);
            ENSURE(core.conflict().size() == 3);
        }
        // A canceled check exposes no candidate; a fresh problem can reuse the
        // pure cache after cancellation is reset, without any stale assertions.
        {
            ff::solver core(m, field, params, &cache);
            core.add(x, zero, true);
            m.limit().inc_cancel();
            try { core.check(); } catch (ff::exhausted const &) {}
            m.limit().dec_cancel();
            bool unavailable = false;
            try { core.value(x); } catch (default_exception const &) { unavailable = true; }
            ENSURE(unavailable);
        }
        ff::solver recovered(m, field, params, &cache);
        recovered.add(x, one, true);
        ENSURE(recovered.check() == l_true && recovered.value(x).is_one());
    }

    void preprocessing_contract() {
        ast_manager m;
        reg_decl_plugins(m);
        ff_util ff(m);
        sort_ref field(ff.mk_sort(rational(7)), m);
        expr_ref x(m.mk_const("px", field), m), y(m.mk_const("py", field), m);
        expr_ref z(m.mk_const("pz", field), m);
        expr_ref zero(ff.mk_numeral(rational(0), field), m);
        expr_ref one(ff.mk_numeral(rational(1), field), m);
        expr_ref two(ff.mk_numeral(rational(2), field), m);
        ff::ff_encoding_cache cache(m, field);
        params_ref params, no_algebra;
        no_algebra.set_uint("ff.max_steps", 0);
        {
            // Generic solve-eqs must discharge this without invoking algebra.
            // Using the input formulas themselves as dependency labels freezes
            // x and y and prevents the required substitutions.
            ff::solver core(m, field, no_algebra, &cache);
            core.add(x, zero, true);
            core.add(y, ff.mk_add(x, one), true);
            core.add(y, one, false);
            core.add(z, two, true);
            ENSURE(core.check() == l_false);
            ENSURE(core.conflict() == std::set<unsigned>({0, 1, 2}));
        }
        expr_ref c(m.mk_const("pc", m.mk_bool_sort()), m);
        expr_ref leaf(m.mk_ite(c, x, zero), m);
        for (unsigned value = 0; value < 7; ++value) {
            // Only pure encodings survive. New assignments reconstruct fresh
            // values for eliminated variables and the same opaque ITE leaf.
            ff::solver core(m, field, params, &cache);
            expr_ref n(ff.mk_numeral(rational(value), field), m);
            core.add(x, n, true);
            core.add(y, ff.mk_add(ff.mk_mul(x, x), one), true);
            core.add(leaf, y, true);
            ENSURE(core.check() == l_true);
            ENSURE(core.value(x) == rational(value));
            ENSURE(core.value(y) == rational((value * value + 1) % 7));
            ENSURE(core.value(leaf) == core.value(y));
        }
        {
            // The field solver treats a foreign term as opaque; it must not
            // substitute inside the ITE and silently change its identity.
            ff::solver core(m, field, params, &cache);
            core.add(x, zero, true);
            core.add(leaf, one, true);
            ENSURE(core.check() == l_true && core.value(leaf).is_one());
            // The frontend's selected-branch equality rules out this candidate.
            ff::solver combined(m, field, params, &cache);
            combined.add(x, zero, true);
            combined.add(leaf, one, true);
            combined.add(leaf, x, true);
            ENSURE(combined.check() == l_false);
            ENSURE(combined.conflict().size() == 3);
        }
        {
            // Inconsistent cyclic definitions cannot be eliminated together.
            ff::solver core(m, field, params, &cache);
            core.add(x, ff.mk_add(y, one), true);
            core.add(y, ff.mk_add(x, one), true);
            ENSURE(core.check() == l_false);
            ENSURE(core.conflict().size() == 2);
        }
    }

    void bit_domain_preservation() {
        ast_manager m;
        reg_decl_plugins(m);
        ff_util ff(m);
        sort_ref field(ff.mk_sort(rational(257)), m);
        expr_ref zero(ff.mk_numeral(rational(0), field), m);
        expr_ref one(ff.mk_numeral(rational(1), field), m);
        params_ref params;
        params.set_uint("ff.max_steps", 1000);
        for (bool factored : {false, true}) {
            ff::solver core(m, field, params);
            expr_ref_vector xs(m), ys(m), left(m), right(m);
            for (unsigned i = 0; i < 4; ++i) {
                expr_ref x(m.mk_fresh_const("bit.x", field), m);
                expr_ref y(m.mk_fresh_const("bit.y", field), m);
                xs.push_back(x); ys.push_back(y);
                for (expr *v : {x.get(), y.get()}) {
                    if (factored)
                        core.add(ff.mk_mul(v, ff.mk_add(v, ff.mk_neg(one))), zero, true);
                    else
                        core.add(ff.mk_mul(v, v), v, true);
                }
                expr_ref weight(ff.mk_numeral(rational(1u << i), field), m);
                left.push_back(ff.mk_mul(weight, x));
                right.push_back(ff.mk_mul(weight, y));
            }
            // Equal four-bit packs over F257 have identical bits: both integer
            // sums lie in [0,15], below the modulus. Eliminating a bit through
            // the pack equation obscures its domain and defeats bit propagation.
            core.add(ff.mk_add(left), ff.mk_add(right), true);
            core.add(xs.get(0), ys.get(0), false);
            ENSURE(core.check() == l_false);
        }
        {
            // The domain detector may match a polynomial identity. Preservation
            // must never turn that heuristic match into a Boolean assumption.
            ff::solver core(m, field, params);
            expr_ref x(m.mk_const("not.a.bit", field), m);
            expr_ref square(ff.mk_mul(x, x), m);
            expr_ref two(ff.mk_numeral(rational(2), field), m);
            core.add(square, square, true);
            core.add(x, two, true);
            ENSURE(core.check() == l_true && core.value(x) == rational(2));
        }
    }

    void tactic_dependencies() {
        ast_manager m;
        reg_decl_plugins(m);
        ff_util ff(m);
        sort_ref field(ff.mk_sort(rational(7)), m);
        expr_ref x(m.mk_const("tx", field), m), y(m.mk_const("ty", field), m);
        expr_ref z(m.mk_const("tz", field), m);
        expr_ref zero(ff.mk_numeral(rational(0), field), m);
        expr_ref one(ff.mk_numeral(rational(1), field), m);
        expr_ref two(ff.mk_numeral(rational(2), field), m);
        expr_ref_vector formulas(m), labels(m);
        formulas.push_back(m.mk_eq(x, zero));
        formulas.push_back(m.mk_eq(y, ff.mk_add(x, one)));
        formulas.push_back(m.mk_not(m.mk_eq(y, one)));
        formulas.push_back(m.mk_eq(z, two));
        goal_ref g = alloc(goal, m, true, false, true);
        for (expr *f : formulas) {
            labels.push_back(m.mk_fresh_const("support", m.mk_bool_sort()));
            g->assert_expr(f, nullptr, m.mk_leaf(labels.back()));
        }
        params_ref params;
        params.set_uint("ff.enum_bits", 0);
        tactic_ref solve = mk_ff_solve_tactic(m, params);
        goal_ref_buffer result;
        (*solve)(g, result);
        ENSURE(result.size() == 1 && result[0]->inconsistent());
        ptr_vector<expr> support;
        m.linearize(result[0]->dep(0), support);
        ENSURE(support.size() == 3);
        for (unsigned i = 0; i < 3; ++i)
            ENSURE(support.contains(labels.get(i)));
        ENSURE(!support.contains(labels.get(3)));
    }

}

void tst_ff_solver() {
    recording_contract();
    exhaustive_problems();
    interface_and_scope_contract();
    preprocessing_contract();
    bit_domain_preservation();
    tactic_dependencies();
}