mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 05:09:02 +00:00
Code Activity

evaluate unhandled arithmetic operators based on an initialized model #7876

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-14 06:45:36 -07:00
parent 3c897b450f
commit 0d0dd0315a
2 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/nla_powers.cpp
View file

@ -138,9 +138,10 @@ namespace nla {
bool use_rational = !c.use_nra_model(); bool use_rational = !c.use_nra_model();
rational xval, yval, rval; rational xval, yval, rval;
if (use_rational) { if (use_rational) {
xval = c.val(x);
yval = c.val(y); xval = c.lra.get_value(x);
rval = c.val(r); yval = c.lra.get_value(y);
rval = c.lra.get_value(r);
} }
else { else {
auto& am = c.m_nra.am(); auto& am = c.m_nra.am();

11
src/smt/theory_lra.cpp
View file

@ -186,10 +186,7 @@ class theory_lra::imp {
imp & m_th; imp & m_th;
var_value_eq(imp & th):m_th(th) {} var_value_eq(imp & th):m_th(th) {}
bool operator()(theory_var v1, theory_var v2) const { bool operator()(theory_var v1, theory_var v2) const {
if (m_th.is_int(v1) != m_th.is_int(v2)) { return m_th.is_int(v1) == m_th.is_int(v2) && m_th.is_eq(v1, v2);
return false;
}
return m_th.is_eq(v1, v2);
} }
}; };
@ -270,7 +267,6 @@ class theory_lra::imp {
}; };
m_nla->set_relevant(is_relevant); m_nla->set_relevant(is_relevant);
m_nla->updt_params(ctx().get_params()); m_nla->updt_params(ctx().get_params());
} }
} }
@ -470,7 +466,8 @@ class theory_lra::imp {
st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n1);
st.to_ensure_var().push_back(n2); st.to_ensure_var().push_back(n2);
} }
else if (a.is_power(n, n1, n2)) { else if (a.is_power(n, n1, n2)) {
ensure_nla();
found_unsupported(n); found_unsupported(n);
if (!ctx().relevancy()) mk_power_axiom(n, n1, n2); if (!ctx().relevancy()) mk_power_axiom(n, n1, n2);
st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n1);
@ -1680,6 +1677,8 @@ public:
if (!int_undef && !check_bv_terms()) if (!int_undef && !check_bv_terms())
return FC_CONTINUE; return FC_CONTINUE;
if (!m_not_handled.empty())
init_variable_values();
for (expr* e : m_not_handled) { for (expr* e : m_not_handled) {
if (!ctx().is_relevant(e)) if (!ctx().is_relevant(e))
continue; continue;