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

fix #2898

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-28 10:29:05 -08:00
parent d3a4b7c44b
commit f161bdaf8f
4 changed files with 34 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3/z3.py
View file

@ -4452,8 +4452,8 @@ def Update(a, i, v):
""" """
if z3_debug(): if z3_debug():
_z3_assert(is_array_sort(a), "First argument must be a Z3 array expression") _z3_assert(is_array_sort(a), "First argument must be a Z3 array expression")
i = a.domain().cast(i) i = a.sort().domain().cast(i)
v = a.range().cast(v) v = a.sort().range().cast(v)
ctx = a.ctx ctx = a.ctx
return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx) return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)

2
src/smt/theory_arith.h
View file

@ -1063,6 +1063,8 @@ namespace smt {
void setup() override; void setup() override;
lbool get_phase(bool_var v) override;
char const * get_name() const override { return "arithmetic"; } char const * get_name() const override { return "arithmetic"; }
// ----------------------------------- // -----------------------------------

15
src/smt/theory_arith_core.h
View file

@ -2233,6 +2233,21 @@ namespace smt {
return result < max ? result : null_theory_var; return result < max ? result : null_theory_var;
} }
template<typename Ext>
lbool theory_arith<Ext>::get_phase(bool_var bv) {
atom* a = get_bv2a(bv);
theory_var v = a->get_var();
auto const& k = a->get_k();
switch (a->get_bound_kind()) {
case B_LOWER:
return get_value(v) >= k ? l_true : l_false;
case B_UPPER:
return get_value(v) <= k ? l_true : l_false;
default:
return l_undef;
}
}
/** /**
\brief Wrapper for select_blands_pivot_core and select_pivot_core \brief Wrapper for select_blands_pivot_core and select_pivot_core
*/ */

26
src/smt/theory_lra.cpp
View file

@ -120,6 +120,7 @@ struct stats {
unsigned m_gomory_cuts; unsigned m_gomory_cuts;
unsigned m_nla_explanations; unsigned m_nla_explanations;
unsigned m_nla_lemmas; unsigned m_nla_lemmas;
unsigned m_assume_eqs;
stats() { reset(); } stats() { reset(); }
void reset() { void reset() {
memset(this, 0, sizeof(*this)); memset(this, 0, sizeof(*this));
@ -1627,6 +1628,7 @@ public:
ctx().push_trail(value_trail<context, unsigned>(m_assume_eq_head)); ctx().push_trail(value_trail<context, unsigned>(m_assume_eq_head));
while (m_assume_eq_head < m_assume_eq_candidates.size()) { while (m_assume_eq_head < m_assume_eq_candidates.size()) {
++m_stats.m_assume_eqs;
std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head]; std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
theory_var v1 = p.first; theory_var v1 = p.first;
theory_var v2 = p.second; theory_var v2 = p.second;
@ -3805,20 +3807,22 @@ public:
st.update("arith-make-feasible", lp().settings().stats().m_make_feasible); st.update("arith-make-feasible", lp().settings().stats().m_make_feasible);
st.update("arith-max-columns", lp().settings().stats().m_max_cols); st.update("arith-max-columns", lp().settings().stats().m_max_cols);
st.update("arith-max-rows", lp().settings().stats().m_max_rows); st.update("arith-max-rows", lp().settings().stats().m_max_rows);
st.update("gcd-calls", lp().settings().stats().m_gcd_calls); st.update("arith-gcd-calls", lp().settings().stats().m_gcd_calls);
st.update("gcd-conflict", lp().settings().stats().m_gcd_conflicts); st.update("arith-gcd-conflict", lp().settings().stats().m_gcd_conflicts);
st.update("cube-calls", lp().settings().stats().m_cube_calls); st.update("arith-cube-calls", lp().settings().stats().m_cube_calls);
st.update("cube-success", lp().settings().stats().m_cube_success); st.update("arith-cube-success", lp().settings().stats().m_cube_success);
st.update("arith-patches", lp().settings().stats().m_patches); st.update("arith-patches", lp().settings().stats().m_patches);
st.update("arith-patches-success", lp().settings().stats().m_patches_success); st.update("arith-patches-success", lp().settings().stats().m_patches_success);
st.update("arith-hnf-calls", lp().settings().stats().m_hnf_cutter_calls); st.update("arith-hnf-calls", lp().settings().stats().m_hnf_cutter_calls);
st.update("horner-calls", lp().settings().stats().m_horner_calls); st.update("arith-horner-calls", lp().settings().stats().m_horner_calls);
st.update("horner-conflicts", lp().settings().stats().m_horner_conflicts); st.update("arith-horner-conflicts", lp().settings().stats().m_horner_conflicts);
st.update("horner-cross-nested-forms", lp().settings().stats().m_cross_nested_forms); st.update("arith-horner-cross-nested-forms", lp().settings().stats().m_cross_nested_forms);
st.update("grobner-calls", lp().settings().stats().m_grobner_calls); st.update("arith-grobner-calls", lp().settings().stats().m_grobner_calls);
st.update("grobner-conflicts", lp().settings().stats().m_grobner_conflicts); st.update("arith-grobner-conflicts", lp().settings().stats().m_grobner_conflicts);
st.update("nla-explanations", m_stats.m_nla_explanations); st.update("arith-nla-explanations", m_stats.m_nla_explanations);
st.update("nla-lemmas", m_stats.m_nla_lemmas); st.update("arith-nla-lemmas", m_stats.m_nla_lemmas);
st.update("arith-gomory-cuts", m_stats.m_gomory_cuts);
st.update("arith-assume-eqs", m_stats.m_assume_eqs);
} }
}; };