mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove experimental option. Fix #4806
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ac1b3fc6f2
commit
1269776777
|
@ -1056,7 +1056,6 @@ namespace arith {
|
|||
// SAT core assigns a value to
|
||||
lia_check = l_false;
|
||||
++m_stats.m_branch;
|
||||
add_variable_bound(t, offset);
|
||||
break;
|
||||
}
|
||||
case lp::lia_move::cut: {
|
||||
|
@ -1167,27 +1166,6 @@ namespace arith {
|
|||
}
|
||||
}
|
||||
|
||||
void solver::add_variable_bound(expr* t, rational const& offset) {
|
||||
if (!use_bounded_expansion())
|
||||
return;
|
||||
if (m_bounded_range_lit == sat::null_literal)
|
||||
return;
|
||||
// if term is not already bounded, add a range and assert max_bound => range
|
||||
bound_info bi(offset, init_range());
|
||||
if (m_term2bound_info.find(t, bi))
|
||||
return;
|
||||
expr_ref hi(a.mk_le(t, a.mk_int(offset + bi.m_range)), m);
|
||||
expr_ref lo(a.mk_ge(t, a.mk_int(offset - bi.m_range)), m);
|
||||
add_clause(~m_bounded_range_lit, mk_literal(hi));
|
||||
add_clause(~m_bounded_range_lit, mk_literal(lo));
|
||||
m_bound_terms.push_back(lo);
|
||||
m_bound_terms.push_back(hi);
|
||||
m_bound_terms.push_back(t);
|
||||
m_predicate2term.insert(lo, t);
|
||||
m_predicate2term.insert(hi, t);
|
||||
m_term2bound_info.insert(t, bi);
|
||||
}
|
||||
|
||||
void solver::reset_evidence() {
|
||||
m_core.reset();
|
||||
m_eqs.reset();
|
||||
|
@ -1204,6 +1182,7 @@ namespace arith {
|
|||
app_ref s(a.mk_numeral(offset, isint), m);
|
||||
return eq_internalize(t, s);
|
||||
}
|
||||
|
||||
// create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false
|
||||
app_ref solver::mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) {
|
||||
rational offset;
|
||||
|
|
|
@ -346,7 +346,6 @@ namespace arith {
|
|||
lbool make_feasible();
|
||||
lbool check_lia();
|
||||
lbool check_nla();
|
||||
void add_variable_bound(expr* t, rational const& offset);
|
||||
bool is_infeasible() const;
|
||||
|
||||
nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const;
|
||||
|
@ -375,7 +374,6 @@ namespace arith {
|
|||
obj_map<expr, bound_info> m_term2bound_info;
|
||||
bool m_model_is_initialized{ false };
|
||||
|
||||
bool use_bounded_expansion() const { return get_config().m_arith_bounded_expansion; }
|
||||
unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; }
|
||||
bool propagate_eqs() const { return get_config().m_arith_propagate_eqs && m_num_conflicts < get_config().m_arith_propagation_threshold; }
|
||||
bool should_propagate() const { return bound_prop_mode::BP_NONE != propagation_mode(); }
|
||||
|
|
|
@ -83,7 +83,6 @@ def_module_params(module_name='smt',
|
|||
('arith.auto_config_simplex', BOOL, False, 'force simplex solver in auto_config'),
|
||||
('arith.rep_freq', UINT, 0, 'the report frequency, in how many iterations print the cost and other info'),
|
||||
('arith.min', BOOL, False, 'minimize cost'),
|
||||
('arith.bounded_expansion', BOOL, False, 'box variables used in branch and bound into bound assumptions'),
|
||||
('arith.print_stats', BOOL, False, 'print statistic'),
|
||||
('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'),
|
||||
('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'),
|
||||
|
|
|
@ -38,7 +38,6 @@ void theory_arith_params::updt_params(params_ref const & _p) {
|
|||
m_arith_reflect = p.arith_reflect();
|
||||
m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
|
||||
m_arith_auto_config_simplex = p.arith_auto_config_simplex();
|
||||
m_arith_bounded_expansion = p.arith_bounded_expansion();
|
||||
|
||||
arith_rewriter_params ap(_p);
|
||||
m_arith_eq2ineq = ap.eq2ineq();
|
||||
|
@ -79,7 +78,6 @@ void theory_arith_params::display(std::ostream & out) const {
|
|||
DISPLAY_PARAM(m_arith_adaptive_gcd);
|
||||
DISPLAY_PARAM(m_arith_propagation_threshold);
|
||||
DISPLAY_PARAM(m_arith_pivot_strategy);
|
||||
DISPLAY_PARAM(m_arith_bounded_expansion);
|
||||
DISPLAY_PARAM(m_arith_add_binary_bounds);
|
||||
DISPLAY_PARAM((unsigned)m_arith_propagation_strategy);
|
||||
DISPLAY_PARAM(m_arith_eq_bounds);
|
||||
|
|
|
@ -83,8 +83,6 @@ struct theory_arith_params {
|
|||
bool m_arith_adaptive_gcd;
|
||||
unsigned m_arith_propagation_threshold;
|
||||
|
||||
bool m_arith_bounded_expansion;
|
||||
|
||||
arith_pivot_strategy m_arith_pivot_strategy;
|
||||
|
||||
// used in diff-logic
|
||||
|
@ -142,7 +140,6 @@ struct theory_arith_params {
|
|||
m_arith_eager_gcd(false),
|
||||
m_arith_adaptive_gcd(false),
|
||||
m_arith_propagation_threshold(UINT_MAX),
|
||||
m_arith_bounded_expansion(false),
|
||||
m_arith_pivot_strategy(arith_pivot_strategy::ARITH_PIVOT_SMALLEST),
|
||||
m_arith_add_binary_bounds(false),
|
||||
m_arith_propagation_strategy(arith_prop_strategy::ARITH_PROP_PROPORTIONAL),
|
||||
|
|
|
@ -1926,7 +1926,6 @@ public:
|
|||
// SAT core assigns a value to
|
||||
lia_check = l_false;
|
||||
++m_stats.m_branch;
|
||||
add_variable_bound(t, offset);
|
||||
break;
|
||||
}
|
||||
case lp::lia_move::cut: {
|
||||
|
@ -3733,86 +3732,9 @@ public:
|
|||
obj_map<expr, expr*> m_predicate2term;
|
||||
obj_map<expr, bound_info> m_term2bound_info;
|
||||
|
||||
bool use_bounded_expansion() const {
|
||||
return ctx().get_fparams().m_arith_bounded_expansion;
|
||||
}
|
||||
|
||||
unsigned init_range() const { return 5; }
|
||||
unsigned max_range() const { return 20; }
|
||||
|
||||
void add_theory_assumptions(expr_ref_vector& assumptions) {
|
||||
if (!use_bounded_expansion())
|
||||
return;
|
||||
ctx().push_trail(value_trail<context, literal>(m_bounded_range_lit));
|
||||
if (!m_bound_predicate || !m_term2bound_info.empty())
|
||||
m_bound_predicate = m.mk_fresh_const("arith.bound", m.mk_bool_sort());
|
||||
m_bounded_range_lit = mk_literal(m_bound_predicate);
|
||||
// add max-unfolding literal
|
||||
// add variable bounds
|
||||
assumptions.push_back(m_bound_predicate);
|
||||
for (auto const& kv : m_term2bound_info) {
|
||||
bound_info const& bi = kv.m_value;
|
||||
expr* t = kv.m_key;
|
||||
expr_ref hi(a.mk_le(t, a.mk_int(bi.m_offset + bi.m_range)), m);
|
||||
expr_ref lo(a.mk_ge(t, a.mk_int(bi.m_offset - bi.m_range)), m);
|
||||
assumptions.push_back(lo);
|
||||
assumptions.push_back(hi);
|
||||
m_predicate2term.insert(lo, t);
|
||||
m_predicate2term.insert(hi, t);
|
||||
IF_VERBOSE(10, verbose_stream() << lo << "\n" << hi << "\n");
|
||||
}
|
||||
}
|
||||
|
||||
bool should_research(expr_ref_vector& unsat_core) {
|
||||
if (!use_bounded_expansion())
|
||||
return false;
|
||||
bool found = false;
|
||||
expr* t = nullptr;
|
||||
for (auto & e : unsat_core) {
|
||||
if (e == m_bound_predicate) {
|
||||
found = true;
|
||||
for (auto & kv : m_term2bound_info)
|
||||
if (kv.m_value.m_range == init_range())
|
||||
kv.m_value.m_range *= 2;
|
||||
}
|
||||
else if (m_predicate2term.find(e, t)) {
|
||||
found = true;
|
||||
bound_info bi;
|
||||
if (!m_term2bound_info.find(t, bi)) {
|
||||
TRACE("arith", tout << "bound information for term " << mk_pp(t, m) << " not found\n";);
|
||||
}
|
||||
else if (bi.m_range >= max_range()) {
|
||||
m_term2bound_info.erase(t);
|
||||
}
|
||||
else {
|
||||
bi.m_range *= 2;
|
||||
m_term2bound_info.insert(t, bi);
|
||||
}
|
||||
}
|
||||
}
|
||||
return found;
|
||||
}
|
||||
|
||||
void add_variable_bound(expr* t, rational const& offset) {
|
||||
if (!use_bounded_expansion())
|
||||
return;
|
||||
if (m_bounded_range_lit == null_literal)
|
||||
return;
|
||||
// if term is not already bounded, add a range and assert max_bound => range
|
||||
bound_info bi(offset, init_range());
|
||||
if (m_term2bound_info.find(t, bi))
|
||||
return;
|
||||
expr_ref hi(a.mk_le(t, a.mk_int(offset + bi.m_range)), m);
|
||||
expr_ref lo(a.mk_ge(t, a.mk_int(offset - bi.m_range)), m);
|
||||
mk_axiom(~m_bounded_range_lit, mk_literal(hi));
|
||||
mk_axiom(~m_bounded_range_lit, mk_literal(lo));
|
||||
m_bound_terms.push_back(lo);
|
||||
m_bound_terms.push_back(hi);
|
||||
m_bound_terms.push_back(t);
|
||||
m_predicate2term.insert(lo, t);
|
||||
m_predicate2term.insert(hi, t);
|
||||
m_term2bound_info.insert(t, bi);
|
||||
}
|
||||
|
||||
void setup() {
|
||||
m_bounded_range_lit = null_literal;
|
||||
|
@ -3945,12 +3867,7 @@ theory_var theory_lra::add_objective(app* term) {
|
|||
expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) {
|
||||
return m_imp->mk_ge(fm, v, val);
|
||||
}
|
||||
void theory_lra::add_theory_assumptions(expr_ref_vector& assumptions) {
|
||||
m_imp->add_theory_assumptions(assumptions);
|
||||
}
|
||||
bool theory_lra::should_research(expr_ref_vector& unsat_core) {
|
||||
return m_imp->should_research(unsat_core);
|
||||
}
|
||||
|
||||
void theory_lra::setup() {
|
||||
m_imp->setup();
|
||||
}
|
||||
|
|
|
@ -97,10 +97,6 @@ namespace smt {
|
|||
|
||||
void setup() override;
|
||||
|
||||
void add_theory_assumptions(expr_ref_vector& assumptions) override;
|
||||
|
||||
bool should_research(expr_ref_vector& unsat_core) override;
|
||||
|
||||
// optimization
|
||||
expr_ref mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val);
|
||||
inf_eps value(theory_var) override;
|
||||
|
|
Loading…
Reference in a new issue