opt: enumerate Pareto fronts of pure NRA problems over an nlsat-backed solver (#10736)

Follow-up to the "Limitations and follow-up" section of #10725: this
implements the exact treatment promised there.

## The gap

#10725 made the Pareto GIA loop sound for irrational objective values,
but only up to a 12-decimal-digit bracket: the dominance and blocking
atoms compare against rounded endpoints of the value's isolating
interval, because the smt core cannot internalize an irrational
algebraic numeral. Two front points whose coordinates differ by less
than the bracket can each "dominate" the other under rounding:

```smt2
(set-option :opt.priority pareto)
(declare-const x Real) (declare-const w Real)
(declare-const r2 Real) (declare-const r3 Real)
(assert (= (* r2 r2) 2)) (assert (> r2 0))
(assert (= (* r3 r3) 3)) (assert (> r3 0))
(assert (or (and (= x r2) (= w (- r3 (/ 1 100000000000000))))
            (and (= x (- r2 (/ 1 100000000000000))) (= w r3))))
(maximize x) (maximize w)
(check-sat) (check-sat) (check-sat)
```

The two points (sqrt(2), sqrt(3) - 10^-14) and (sqrt(2) - 10^-14,
sqrt(3)) are incomparable, so the answer must be sat/sat/unsat. With
rounded dominance each point blocks the other: the front collapses to
one point and the loop answers sat/unsat/sat, contradicting its own
unsat.

## The fix

nlsat decides atoms over algebraic numerals natively, so on the fragment
it handles the loop now runs there and compares exactly:

- `mk_pareto_solver`: when every objective is a real min/max term, the
hard constraints pass `in_nra_fragment` (exported from `opt_nlsat`;
Boolean structure over polynomial atoms, uninterpreted constants only),
and no assumptions are in play, the GIA loop gets a
`tactic2solver(qfnra-nlsat)` loaded with the hard constraints instead of
the smt solver.
- `mk_cmp`: with the nlsat-backed solver active, an irrational algebraic
model value goes into the comparison atom as-is; the isolating-interval
endpoint substitution is skipped.
- `opt.pareto_nlsat` (default true) restores the previous behavior when
disabled; anything outside the fragment falls back to the smt solver
unchanged.
- The reported intervals remain 12-digit brackets: `update_bound` feeds
the `inf_eps` display bookkeeping only, which cannot carry algebraic
values. Printing the root-obj value is a separate follow-up.

Known cost: `tactic2solver` re-solves from scratch at each check, so
long fronts pay per point; an incremental nlsat integration (persisting
learned clauses across checks) is planned separately.

## Validation

- new unit test `test-z3 opt_pareto`: the sqrt(2) front with
algebraic-numeral model values, the nearly tied front above, the
uninterpreted-function fallback; `test-z3 -a` 104/104
- z3test `regressions/smt2`: all pass (companion PR regenerates
`opt_algebraic_pareto_front.expected.out` - nlsat enumerates the same
front in the opposite order - and adds `opt_algebraic_pareto_slack`)
- OMT benchmark set: verdicts unchanged; the nearly-tied-front instance
passes in 0.02s

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

src/opt/opt_context.cpp

@@ -45,8 +45,11 @@ Notes:
 #include "ackermannization/ackermannize_bv_tactic.h"
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "params/sat_params.hpp"
+#include "solver/tactic2solver.h"
+#include "nlsat/tactic/qfnra_nlsat_tactic.h"
 #include "opt/opt_context.h"
 #include "opt/opt_solver.h"
+#include "opt/opt_nlsat.h"
 #include "opt/opt_params.hpp"
 
 
@@ -353,6 +356,7 @@ namespace opt {
         import_scoped_state(); 
         expr_ref_vector asms(_asms);
         asms.append(m_scoped_state.m_asms);
+        m_has_assumptions = !asms.empty();
         normalize(asms);
         if (m_hard_constraints.size() == 1 && m.is_false(m_hard_constraints.get(0))) {
             return l_false;
@@ -677,6 +681,13 @@ namespace opt {
             Z3_fallthrough;
         case O_MAXIMIZE:
             val = (*mdl)(obj.m_term);
+            if (m_pareto_exact_comparison && m_arith.is_irrational_algebraic_numeral(val)) {
+                // The nlsat-backed Pareto solver (mk_pareto_solver) decides
+                // atoms over algebraic numerals, so compare the objective
+                // against its exact model value.
+                result = is_ge ? mk_ge(obj.m_term, val) : mk_ge(val, obj.m_term);
+                break;
+            }
             // The model may pin the objective to an irrational algebraic
             // value v. The smt backend does not internalize an irrational
             // algebraic numeral (it reports the term unsupported and answers
@@ -747,7 +758,7 @@ namespace opt {
         return result;
     }
 
-    void context::yield() {
+    void context::publish_pareto_result() {
         SASSERT (m_pareto);
         m_pareto->get_model(m_model, m_labels);
         update_bound(true);
@@ -755,16 +766,44 @@ namespace opt {
         TRACE(opt, model_smt2_pp(tout, m, *m_model.get(), 0););
     }
 
-    lbool context::execute_pareto() {        
+    // Pick the solver the GIA loop runs on. On a pure NRA problem the
+    // dominance and blocking constraints go to an nlsat-backed solver:
+    // nlsat decides atoms over irrational algebraic numerals, which the
+    // smt core reports unsupported at internalization, so mk_cmp can
+    // compare an objective against its exact model value instead of a
+    // rounded isolating-interval endpoint (opt.pareto_nlsat to disable).
+    solver* context::mk_pareto_solver() {
+        opt_params optp(m_params);
+        m_pareto_exact_comparison = false;
+        if (!optp.pareto_nlsat() || m_has_assumptions)
+            return m_solver.get();
+        for (objective const& obj : m_objectives) {
+            if (obj.m_type != O_MAXIMIZE && obj.m_type != O_MINIMIZE)
+                return m_solver.get();
+            if (!m_arith.is_real(obj.m_term))
+                return m_solver.get();
+            if (!in_nra_fragment(m, m_arith, m_hard_constraints, obj.m_term))
+                return m_solver.get();
+        }
+        tactic_ref t = mk_qfnra_nlsat_tactic(m, m_params);
+        solver* s = mk_tactic2solver(m, t.get(), m_params);
+        for (expr* f : m_hard_constraints)
+            s->assert_expr(f);
+        m_pareto_exact_comparison = true;
+        IF_VERBOSE(2, verbose_stream() << "(opt.pareto :solver qfnra-nlsat)\n");
+        return s;
+    }
+
+    lbool context::execute_pareto() {
         if (!m_pareto) {
-            set_pareto(alloc(gia_pareto, m, *this, m_solver.get(), m_params));
+            set_pareto(alloc(gia_pareto, m, *this, mk_pareto_solver(), m_params));
         }
         lbool is_sat = (*(m_pareto.get()))();
         if (is_sat != l_true) {
             set_pareto(nullptr);
         }
         if (is_sat == l_true) {
-            yield();
+            publish_pareto_result();
         }
         return is_sat;
     }

src/opt/opt_context.h

@@ -177,6 +177,8 @@ namespace opt {
         ref<solver>         m_sat_solver;
         scoped_ptr<pareto_base>  m_pareto;
         bool                 m_pareto1;
+        bool                 m_pareto_exact_comparison = false;
+        bool                 m_has_assumptions = false;
         sref_vector<model>  m_box_models;
         unsigned            m_box_index;
         params_ref          m_params;
@@ -305,6 +307,7 @@ namespace opt {
         lbool execute_lex();
         lbool execute_box();
         lbool execute_pareto();
+        solver* mk_pareto_solver();
         lbool adjust_unknown(lbool r);
         bool scoped_lex();
         bool contains_quantifiers() const;
@@ -373,7 +376,7 @@ namespace opt {
         void display_benchmark();
 
         // pareto
-        void yield();
+        void publish_pareto_result();
         expr_ref mk_ge(expr* t, expr* s);
         expr_ref mk_cmp(bool is_ge, model_ref& mdl, objective const& obj);
 

src/opt/opt_nlsat.cpp

@@ -79,7 +79,7 @@ namespace opt {
         }
     };
 
-    static bool in_nra_fragment(ast_manager& m, arith_util& a, expr_ref_vector const& hard, expr* obj) {
+    bool in_nra_fragment(ast_manager& m, arith_util& a, expr_ref_vector const& hard, expr* obj) {
         nra_fragment_check chk(m, a);
         expr_fast_mark1 visited;
         for (expr* f : hard) {

src/opt/opt_nlsat.h

@@ -40,6 +40,13 @@ class model_converter;
 
 namespace opt {
 
+    /**
+       \brief True when the hard constraints and obj lie in the fragment
+       nlsat decides: Boolean structure over polynomial arithmetic atoms,
+       with uninterpreted constants as the only free symbols.
+    */
+    bool in_nra_fragment(ast_manager& m, arith_util& a, expr_ref_vector const& hard, expr* obj);
+
     class nlsat_opt {
         ast_manager&  m;
         params_ref    m_params;

src/opt/opt_params.pyg

@@ -4,6 +4,7 @@ def_module_params('opt',
                   params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'symba'"),
                           ('optsmt_bisect_rounds', UINT, 64, 'maximal number of solver calls spent bisecting the interval between the best model value and the refuted arithmetic bound of a real-valued objective (e.g. under nonlinear constraints); when exhausted the objective is reported as unknown with that interval'),
                           ('optsmt_nlsat', BOOL, True, 'optimize real objectives under nonlinear constraints exactly over nlsat cells (algebraic optima print as root-obj; unboundedness proven by nlqsat queries under an escalating rlimit budget)'),
+                          ('pareto_nlsat', BOOL, True, 'enumerate Pareto fronts of pure NRA problems over an nlsat-backed solver, comparing objectives against exact algebraic model values instead of rounded isolating-interval endpoints'),
                           ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'maxresw', 'pd-maxres', 'maxres-bin', 'rc2'"),
                           ('priority', SYMBOL, 'lex', "select how to prioritize objectives: 'lex' (lexicographic), 'pareto', 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),

src/test/CMakeLists.txt

@@ -106,6 +106,7 @@ add_executable(test-z3
   object_allocator.cpp
   old_interval.cpp
   opt_nlsat.cpp
+  opt_pareto.cpp
   optional.cpp
   parray.cpp
   pb2bv.cpp

src/test/main.cpp

@@ -147,6 +147,7 @@
     X(permutation) \
     X(nlsat) \
     X(opt_nlsat) \
+    X(opt_pareto) \
     X(13) \
     X(zstring)
 

src/test/opt_pareto.cpp

@@ -0,0 +1,129 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    opt_pareto.cpp
+
+Abstract:
+
+    Tests for Pareto enumeration in opt::context over the nlsat-backed
+    solver (opt.pareto_nlsat). Covers what the SMT-LIB regressions cannot
+    assert directly: the model values of the front points are irrational
+    algebraic numerals, front points closer than the 12-digit display
+    bracket are still told apart, and problems outside the NRA fragment
+    fall back to the smt solver and enumerate their front there.
+
+Author:
+
+    Lev Nachmanson 2026-09-04
+
+--*/
+#include "opt/opt_context.h"
+#include "ast/reg_decl_plugins.h"
+
+static void set_pareto_priority(opt::context& ctx) {
+    params_ref p;
+    p.set_sym("priority", symbol("pareto"));
+    ctx.updt_params(p);
+}
+
+// maximize x, maximize y s.t. x^2 = 2, y = -x: the front is the two
+// incomparable points (sqrt(2), -sqrt(2)) and (-sqrt(2), sqrt(2)); the
+// third round is unsat and the model values are algebraic numerals.
+static void tst_irrational_front() {
+    std::cout << "opt_pareto: irrational front\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    arith_util a(m);
+    opt::context ctx(m);
+    set_pareto_priority(ctx);
+    expr_ref x(m.mk_const(symbol("x"), a.mk_real()), m);
+    expr_ref y(m.mk_const(symbol("y"), a.mk_real()), m);
+    expr_ref two(a.mk_numeral(rational(2), false), m);
+    ctx.add_hard_constraint(m.mk_eq(a.mk_mul(x, x), two));
+    ctx.add_hard_constraint(m.mk_eq(y, a.mk_uminus(x)));
+    ctx.add_objective(to_app(x.get()), true);
+    ctx.add_objective(to_app(y.get()), true);
+    expr_ref_vector asms(m);
+    model_ref mdl;
+    ENSURE(ctx.optimize(asms) == l_true);
+    ctx.get_model(mdl);
+    expr_ref x1 = (*mdl)(x);
+    ENSURE(a.is_irrational_algebraic_numeral(x1));
+    ENSURE(ctx.optimize(asms) == l_true);
+    ctx.get_model(mdl);
+    expr_ref x2 = (*mdl)(x);
+    ENSURE(a.is_irrational_algebraic_numeral(x2));
+    ENSURE(x1 != x2);
+    ENSURE(ctx.optimize(asms) == l_false);
+}
+
+// two incomparable points whose coordinates differ by 10^-14, below the
+// 12-digit bracket of the rounded comparison: (sqrt(2), sqrt(3) - 10^-14)
+// and (sqrt(2) - 10^-14, sqrt(3)). The exact dominance constraints tell
+// them apart, so both are enumerated before the front is exhausted.
+static void tst_nearly_tied_front() {
+    std::cout << "opt_pareto: nearly tied front\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    arith_util a(m);
+    opt::context ctx(m);
+    set_pareto_priority(ctx);
+    sort* real = a.mk_real();
+    expr_ref x(m.mk_const(symbol("x"), real), m);
+    expr_ref w(m.mk_const(symbol("w"), real), m);
+    expr_ref r2(m.mk_const(symbol("r2"), real), m);
+    expr_ref r3(m.mk_const(symbol("r3"), real), m);
+    expr_ref two(a.mk_numeral(rational(2), false), m);
+    expr_ref three(a.mk_numeral(rational(3), false), m);
+    expr_ref zero(a.mk_numeral(rational(0), false), m);
+    expr_ref eps(a.mk_numeral(rational(1, 100000000000000ull), false), m);
+    ctx.add_hard_constraint(m.mk_eq(a.mk_mul(r2, r2), two));
+    ctx.add_hard_constraint(a.mk_gt(r2, zero));
+    ctx.add_hard_constraint(m.mk_eq(a.mk_mul(r3, r3), three));
+    ctx.add_hard_constraint(a.mk_gt(r3, zero));
+    expr_ref pt1(m.mk_and(m.mk_eq(x, r2), m.mk_eq(w, a.mk_sub(r3, eps))), m);
+    expr_ref pt2(m.mk_and(m.mk_eq(x, a.mk_sub(r2, eps)), m.mk_eq(w, r3)), m);
+    ctx.add_hard_constraint(m.mk_or(pt1, pt2));
+    ctx.add_objective(to_app(x.get()), true);
+    ctx.add_objective(to_app(w.get()), true);
+    expr_ref_vector asms(m);
+    ENSURE(ctx.optimize(asms) == l_true);
+    ENSURE(ctx.optimize(asms) == l_true);
+    ENSURE(ctx.optimize(asms) == l_false);
+}
+
+// an uninterpreted function puts the problem outside the NRA fragment: the
+// loop falls back to the smt solver and still enumerates the (rational)
+// two-point front.
+static void tst_uf_fallback() {
+    std::cout << "opt_pareto: uf fallback\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    arith_util a(m);
+    opt::context ctx(m);
+    set_pareto_priority(ctx);
+    sort* real = a.mk_real();
+    expr_ref x(m.mk_const(symbol("x"), real), m);
+    expr_ref w(m.mk_const(symbol("w"), real), m);
+    func_decl_ref f(m.mk_func_decl(symbol("f"), real, real), m);
+    expr_ref zero(a.mk_numeral(rational(0), false), m);
+    expr_ref one(a.mk_numeral(rational(1), false), m);
+    expr_ref pt1(m.mk_and(m.mk_eq(x, one), m.mk_eq(w, zero)), m);
+    expr_ref pt2(m.mk_and(m.mk_eq(x, zero), m.mk_eq(w, one)), m);
+    ctx.add_hard_constraint(m.mk_or(pt1, pt2));
+    ctx.add_hard_constraint(a.mk_ge(m.mk_app(f, x.get()), zero));
+    ctx.add_objective(to_app(x.get()), true);
+    ctx.add_objective(to_app(w.get()), true);
+    expr_ref_vector asms(m);
+    ENSURE(ctx.optimize(asms) == l_true);
+    ENSURE(ctx.optimize(asms) == l_true);
+    ENSURE(ctx.optimize(asms) == l_false);
+}
+
+void tst_opt_pareto() {
+    tst_irrational_front();
+    tst_nearly_tied_front();
+    tst_uf_fallback();
+}