mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

local

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-13 14:30:34 -07:00 • committed by Lev Nachmanson
parent 906d52ca1c
commit 79fefe5fb3
3 changed files with 29 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/nla_solver.cpp
View file

@ -58,4 +58,10 @@ bool solver::influences_nl_var(lpvar j) const {
solver::~solver() { solver::~solver() {
dealloc(m_core); dealloc(m_core);
} }
std::ostream& solver::display(std::ostream& out) const {
m_core->print_monics(out);
return out;
}
} }

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

@ -38,12 +38,13 @@ public:
solver(lp::lar_solver& s); solver(lp::lar_solver& s);
~solver(); ~solver();
inline core * get_core() { return m_core; } core& get_core() { return *m_core; }
void push(); void push();
void pop(unsigned scopes); void pop(unsigned scopes);
bool need_check(); bool need_check();
lbool check(vector<lemma>&); lbool check(vector<lemma>&);
bool is_monic_var(lpvar) const; bool is_monic_var(lpvar) const;
bool influences_nl_var(lpvar) const; bool influences_nl_var(lpvar) const;
std::ostream& display(std::ostream& out) const;
}; };
} }

37
src/smt/theory_lra.cpp
View file

@ -450,21 +450,20 @@ class theory_lra::imp {
m_nla->push(); m_nla->push();
} }
smt_params_helper prms(ctx().get_params()); smt_params_helper prms(ctx().get_params());
m_nla->get_core()->m_nla_settings.run_order() = prms.arith_nl_order(); m_nla->get_core().m_nla_settings.run_order() = prms.arith_nl_order();
m_nla->get_core()->m_nla_settings.run_tangents() = prms.arith_nl_tangents(); m_nla->get_core().m_nla_settings.run_tangents() = prms.arith_nl_tangents();
m_nla->get_core()->m_nla_settings.run_horner() = prms.arith_nl_horner(); m_nla->get_core().m_nla_settings.run_horner() = prms.arith_nl_horner();
m_nla->get_core()->m_nla_settings.horner_subs_fixed() = prms.arith_nl_horner_subs_fixed(); m_nla->get_core().m_nla_settings.horner_subs_fixed() = prms.arith_nl_horner_subs_fixed();
m_nla->get_core().m_nla_settings.horner_frequency() = prms.arith_nl_horner_frequency();
m_nla->get_core()->m_nla_settings.horner_frequency() = prms.arith_nl_horner_frequency(); m_nla->get_core().m_nla_settings.horner_row_length_limit() = prms.arith_nl_horner_row_length_limit();
m_nla->get_core()->m_nla_settings.horner_row_length_limit() = prms.arith_nl_horner_row_length_limit(); m_nla->get_core().m_nla_settings.run_grobner() = prms.arith_nl_grobner();
m_nla->get_core()->m_nla_settings.run_grobner() = prms.arith_nl_grobner(); m_nla->get_core().m_nla_settings.grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed();
m_nla->get_core()->m_nla_settings.grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed(); m_nla->get_core().m_nla_settings.grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth();
m_nla->get_core()->m_nla_settings.grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth(); m_nla->get_core().m_nla_settings.grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth();
m_nla->get_core()->m_nla_settings.grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth(); m_nla->get_core().m_nla_settings.grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth();
m_nla->get_core()->m_nla_settings.grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth(); m_nla->get_core().m_nla_settings.grobner_max_simplified() = prms.arith_nl_grobner_max_simplified();
m_nla->get_core()->m_nla_settings.grobner_max_simplified() = prms.arith_nl_grobner_max_simplified(); m_nla->get_core().m_nla_settings.grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report();
m_nla->get_core()->m_nla_settings.grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); m_nla->get_core().m_grobner_quota = prms.arith_nl_gr_q();
m_nla->get_core()->m_grobner_quota = prms.arith_nl_gr_q();
} }
} }
@ -1396,7 +1395,7 @@ public:
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero))); th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()))); th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()))); th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()))); th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()))); th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
}; };
if_trace_stream _ts(m, log); if_trace_stream _ts(m, log);
@ -3743,6 +3742,12 @@ public:
lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); lp().m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
} }
} }
if (m_nla) {
m_nla->display(out);
}
if (m_nra) {
m_nra->display(out);
}
unsigned nv = th.get_num_vars(); unsigned nv = th.get_num_vars();
for (unsigned v = 0; v < nv; ++v) { for (unsigned v = 0; v < nv; ++v) {
if (!ctx().is_relevant(get_enode(v))) out << "irr: "; if (!ctx().is_relevant(get_enode(v))) out << "irr: ";