mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

Merge branch 'master' into unit_prop_on_monomials

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-09-26 20:14:06 -07:00 committed by GitHub
parent 368fe80b3d ec2937e2de
commit e8fcc876c9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
9 changed files with 31 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/nla_core.cpp
View file

@ -1855,6 +1855,7 @@ bool core::is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed)
}
}
return n_of_non_fixed <= 1;
}
void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep) {

3
src/math/lp/nla_core.h
View file

@ -399,8 +399,6 @@ public:
bool no_lemmas_hold() const;
// void propagate();
lbool test_check();
lpvar map_to_root(lpvar) const;
std::ostream& print_terms(std::ostream&) const;
@ -435,6 +433,7 @@ public:
void set_use_nra_model(bool m);
bool use_nra_model() const { return m_use_nra_model; }
void collect_statistics(::statistics&);
bool is_linear(const svector<lpvar>& m, lpvar& zero_var, lpvar& non_fixed);
void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var);
void propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k);

3
src/smt/params/smt_params_helper.pyg
View file

@ -81,6 +81,9 @@ def_module_params(module_name='smt',
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),

6
src/smt/params/theory_arith_params.cpp
View file

@ -36,6 +36,9 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
m_arith_eager_eq_axioms = p.arith_eager_eq_axioms();
m_arith_auto_config_simplex = p.arith_auto_config_simplex();
m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials();
m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds();
m_nl_arith_cross_nested = p.arith_nl_cross_nested();
arith_rewriter_params ap(_p);
m_arith_eq2ineq = ap.eq2ineq();
@ -89,4 +92,7 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_nl_arith_max_degree);
DISPLAY_PARAM(m_nl_arith_branching);
DISPLAY_PARAM(m_nl_arith_rounds);
DISPLAY_PARAM(m_nl_arith_propagate_linear_monomials);
DISPLAY_PARAM(m_nl_arith_optimize_bounds);
DISPLAY_PARAM(m_nl_arith_cross_nested);
}

3
src/smt/params/theory_arith_params.h
View file

@ -105,6 +105,9 @@ struct theory_arith_params {
unsigned m_nl_arith_max_degree = 6;
bool m_nl_arith_branching = true;
unsigned m_nl_arith_rounds = 1024;
bool m_nl_arith_propagate_linear_monomials = true;
bool m_nl_arith_optimize_bounds = true;
bool m_nl_arith_cross_nested = true;
theory_arith_params(params_ref const & p = params_ref()) {

4
src/smt/smt_context.h
View file

@ -134,7 +134,6 @@ namespace smt {
enode * m_lhs;
enode * m_rhs;
eq_justification m_justification;
new_eq() {}
new_eq(enode * lhs, enode * rhs, eq_justification const & js):
m_lhs(lhs), m_rhs(rhs), m_justification(js) {}
};
@ -143,7 +142,6 @@ namespace smt {
theory_id m_th_id;
theory_var m_lhs;
theory_var m_rhs;
new_th_eq():m_th_id(null_theory_id), m_lhs(null_theory_var), m_rhs(null_theory_var) {}
new_th_eq(theory_id id, theory_var l, theory_var r):m_th_id(id), m_lhs(l), m_rhs(r) {}
};
svector<new_th_eq> m_th_eq_propagation_queue;
@ -215,7 +213,7 @@ namespace smt {
// -----------------------------------
proto_model_ref m_proto_model;
model_ref m_model;
std::string m_unknown;
const char * m_unknown;
void mk_proto_model();
void reset_model() { m_model = nullptr; m_proto_model = nullptr; }

2
src/smt/smt_context_pp.cpp
View file

@ -66,6 +66,7 @@ namespace smt {
std::string context::last_failure_as_string() const {
std::string r;
switch(m_last_search_failure) {
case UNKNOWN:
case OK: r = m_unknown; break;
case MEMOUT: r = "memout"; break;
case CANCELED: r = "canceled"; break;
@ -82,7 +83,6 @@ namespace smt {
case RESOURCE_LIMIT: r = "(resource limits reached)"; break;
case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
case LAMBDAS: r = "(incomplete lambdas)"; break;
case UNKNOWN: r = m_unknown; break;
}
return r;
}

6
src/smt/theory_arith_nl.h
View file

@ -902,6 +902,8 @@ bool theory_arith<Ext>::propagate_linear_monomial(theory_var v) {
*/
template<typename Ext>
bool theory_arith<Ext>::propagate_linear_monomials() {
if (!m_params.m_nl_arith_propagate_linear_monomials)
return false;
if (!reflection_enabled())
return false;
TRACE("non_linear", tout << "propagating linear monomials...\n";);
@ -2278,6 +2280,8 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
*/
template<typename Ext>
bool theory_arith<Ext>::max_min_nl_vars() {
if (!m_params.m_nl_arith_optimize_bounds)
return true;
var_set already_found;
svector<theory_var> vars;
for (theory_var v : m_nl_monomials) {
@ -2360,7 +2364,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
}
break;
case 1:
if (!is_cross_nested_consistent(vars))
if (m_params.m_nl_arith_cross_nested && !is_cross_nested_consistent(vars))
progress = true;
break;
case 2:

18
src/test/lp/nla_solver_test.cpp
View file

@ -197,6 +197,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
auto const& lemmas = nla.get_core().lemmas();
nla.get_core().print_lemma(lemmas.back(), std::cout);
ineq i0(lp_ac, llc::NE, 1);
lp::lar_term t1, t2;
t1.add_var(lp_bde);
@ -477,7 +478,6 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
nla.get_core().print_lemma(lemma.back(), std::cout);
ineq i0(lp_d, llc::EQ, 1);
ineq i1(lp_d, llc::EQ, -1);
@ -714,9 +714,9 @@ void test_order_lemma_params(bool var_equiv, int sign) {
s_set_column_value_test(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij)
+ rational(1));
}
vector<lemma> lemma;
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
// lp::lar_term t;
// t.add_monomial(lp_bde);
// t.add_monomial(lp_acd);
@ -800,8 +800,8 @@ void test_monotone_lemma() {
// set ef = ij while it has to be ef > ij
s_set_column_value_test(s, lp_ef, s.get_column_value(lp_ij));
vector<lemma> lemma;
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
nla.get_core().print_lemma(lemma.back(), std::cout);
*/
}
@ -859,8 +859,7 @@ void test_tangent_lemma_reg() {
nla.add_monic(lp_ab, vec.size(), vec.begin());
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
nla.get_core().print_lemma(lemma.back(), std::cout);
nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout);
}
void test_tangent_lemma_equiv() {
@ -904,10 +903,9 @@ void test_tangent_lemma_equiv() {
int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
s_set_column_value_test(s, lp_ab, nla.get_core().mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
vector<lemma> lemma;
VERIFY(nla.get_core().test_check(lemma) == l_false);
nla.get_core().print_lemma(lemma.back(), std::cout);
VERIFY(nla.get_core().test_check() == l_false);
nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout);
*/
}