mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-10-07 03:35:47 +00:00
Code Activity

use option type

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-08-31 14:32:27 -07:00
parent 66784ec96c
commit 24b02fd7f5
4 changed files with 19 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/opt/opt_nlsat.cpp
View file

@ -95,7 +95,7 @@ namespace opt {
preprocessing refutes the goal, and l_undef if preprocessing fails or
loses T.
*/
lbool nlsat_opt::preprocess(expr_ref_vector const& hard, expr* obj, rational const& lo, bool has_hi, rational const& hi,
lbool nlsat_opt::preprocess(expr_ref_vector const& hard, expr* obj, rational const& lo, std::optional<rational> const& hi,
app_ref& T, goal_ref& pg) {
T = m.mk_fresh_const("opt.nlsat.obj", m_arith.mk_real());
goal_ref g = alloc(goal, m, false, true, false);
@ -103,8 +103,8 @@ namespace opt {
g->assert_expr(f);
g->assert_expr(m.mk_eq(T, obj));
g->assert_expr(m_arith.mk_ge(T, m_arith.mk_numeral(lo, false)));
if (has_hi)
g->assert_expr(m_arith.mk_le(T, m_arith.mk_numeral(hi, false)));
if (hi)
g->assert_expr(m_arith.mk_le(T, m_arith.mk_numeral(*hi, false)));
params_ref simp_p;
simp_p.set_bool("elim_and", true);
@ -272,7 +272,7 @@ namespace opt {
res.m_attained = attained;
}
lbool nlsat_opt::maximize(expr_ref_vector const& hard, expr* obj, rational const& lo, bool has_hi, rational const& hi,
lbool nlsat_opt::maximize(expr_ref_vector const& hard, expr* obj, rational const& lo, std::optional<rational> const& hi,
unsigned max_rounds, result& res) {
res.reset();
if (!in_nra_fragment(m, m_arith, hard, obj)) {
@ -283,7 +283,7 @@ namespace opt {
// 1. hard /\ T = obj /\ lo <= T <= hi, normalized for goal2nlsat.
app_ref T(m);
goal_ref pg;
lbool st = preprocess(hard, obj, lo, has_hi, hi, T, pg);
lbool st = preprocess(hard, obj, lo, hi, T, pg);
if (st != l_true)
return st;
model_converter_ref mc = pg->mc();

7
src/opt/opt_nlsat.h
View file

@ -25,6 +25,7 @@ Author:
--*/
#pragma once
#include <optional>
#include "ast/ast.h"
#include "ast/arith_decl_plugin.h"
#include "model/model.h"
@ -60,18 +61,18 @@ namespace opt {
nlsat_opt(ast_manager& m, params_ref const& p);
/**
\brief Maximize obj subject to the hard constraints and lo <= obj (<= hi when has_hi).
\brief Maximize obj subject to the hard constraints and lo <= obj (<= hi when provided).
Returns l_true when the optimum is proven (r.m_attained),
l_undef when the problem is outside nlsat's fragment or the round
budget is exhausted (r.m_model, if set, is the best model found),
and l_false when hard /\ lo <= obj <= hi has no model.
*/
lbool maximize(expr_ref_vector const& hard, expr* obj, rational const& lo, bool has_hi, rational const& hi,
lbool maximize(expr_ref_vector const& hard, expr* obj, rational const& lo, std::optional<rational> const& hi,
unsigned max_rounds, result& r);
private:
// The steps of maximize, in order.
lbool preprocess(expr_ref_vector const& hard, expr* obj, rational const& lo, bool has_hi, rational const& hi,
lbool preprocess(expr_ref_vector const& hard, expr* obj, rational const& lo, std::optional<rational> const& hi,
app_ref& T, goal_ref& pg);
bool load(goal const& pg, app* T, nlsat::solver& s, nlsat::var& t, expr_ref_vector& x2t, expr_ref_vector& b2a);
model_ref extract_model(nlsat::solver& s, expr_ref_vector const& x2t, expr_ref_vector const& b2a, app* T,

5
src/opt/optsmt.cpp
View file

@ -401,7 +401,10 @@ namespace opt {
nlsat_opt engine(m, p);
nlsat_opt::result res(m);
IF_VERBOSE(2, verbose_stream() << "(optsmt nlsat [" << m_lower[idx] << ", " << hi << "])\n");
lbool r = engine.maximize(hard, m_objs.get(idx), m_lower[idx].get_rational(), hi.is_finite(), hi.get_rational(), m_bisect_rounds, res);
std::optional<rational> upper;
if (hi.is_finite())
upper = hi.get_rational();
lbool r = engine.maximize(hard, m_objs.get(idx), m_lower[idx].get_rational(), upper, m_bisect_rounds, res);
TRACE(opt, tout << "nlsat cells: " << r << " rounds " << res.m_rounds << " value " << res.m_value << "\n";);
if (!res.m_model)
return l_false;

12
src/test/opt_nlsat.cpp
View file

@ -34,7 +34,7 @@ static void tst_attained() {
params_ref p;
opt::nlsat_opt opt(m, p);
opt::nlsat_opt::result res(m);
lbool r = opt.maximize(hard, x, rational(0), true, rational(2), 64, res);
lbool r = opt.maximize(hard, x, rational(0), rational(2), 64, res);
ENSURE(r == l_true);
ENSURE(res.m_attained);
ENSURE(res.m_model);
@ -62,7 +62,7 @@ static void tst_unbounded() {
params_ref p;
opt::nlsat_opt opt(m, p);
opt::nlsat_opt::result res(m);
lbool r = opt.maximize(hard, x, rational(1), false, rational(0), 64, res);
lbool r = opt.maximize(hard, x, rational(1), std::nullopt, 64, res);
ENSURE(r == l_undef);
ENSURE(!res.m_attained);
ENSURE(!res.m_has_sup);
@ -85,7 +85,7 @@ static void tst_open_sup() {
params_ref p;
opt::nlsat_opt opt(m, p);
opt::nlsat_opt::result res(m);
lbool r = opt.maximize(hard, x, rational(0), true, rational(2), 8, res);
lbool r = opt.maximize(hard, x, rational(0), rational(2), 8, res);
ENSURE(r == l_undef);
ENSURE(!res.m_attained);
ENSURE(res.m_model);
@ -111,7 +111,7 @@ static void tst_cubic_roots() {
params_ref p;
opt::nlsat_opt opt(m, p);
opt::nlsat_opt::result res(m);
lbool r = opt.maximize(hard, x, rational(-2), true, rational(2), 64, res);
lbool r = opt.maximize(hard, x, rational(-2), rational(2), 64, res);
ENSURE(r == l_true);
ENSURE(res.m_attained);
ENSURE(res.m_model);
@ -138,7 +138,7 @@ static void tst_outside_fragment() {
params_ref p;
opt::nlsat_opt opt(m, p);
opt::nlsat_opt::result res(m);
lbool r = opt.maximize(hard, x, rational(0), true, rational(2), 64, res);
lbool r = opt.maximize(hard, x, rational(0), rational(2), 64, res);
ENSURE(r == l_undef);
ENSURE(!res.m_model);
ENSURE(!res.m_attained);
@ -157,7 +157,7 @@ static void tst_infeasible() {
params_ref p;
opt::nlsat_opt opt(m, p);
opt::nlsat_opt::result res(m);
lbool r = opt.maximize(hard, x, rational(3), true, rational(4), 64, res);
lbool r = opt.maximize(hard, x, rational(3), rational(4), 64, res);
ENSURE(r == l_false);
ENSURE(!res.m_model);
}