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

partial fix to model generation bug for non-linear constraints: avoid epsilon refinment for non-shared variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-07 20:39:20 +09:00
parent e17af8a5de
commit 3d995648ee
3 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_arith.h
View file

@ -85,6 +85,7 @@ namespace smt {
typedef typename Ext::numeral numeral; typedef typename Ext::numeral numeral;
typedef typename Ext::inf_numeral inf_numeral; typedef typename Ext::inf_numeral inf_numeral;
typedef vector<numeral> numeral_vector; typedef vector<numeral> numeral_vector;
typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
static const int dead_row_id = -1; static const int dead_row_id = -1;
protected: protected:

3
src/smt/theory_arith_core.h
View file

@ -2780,7 +2780,6 @@ namespace smt {
*/ */
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::refine_epsilon() { void theory_arith<Ext>::refine_epsilon() {
typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
while (true) { while (true) {
rational2var mapping; rational2var mapping;
theory_var num = get_num_vars(); theory_var num = get_num_vars();
@ -2788,6 +2787,8 @@ namespace smt {
for (theory_var v = 0; v < num; v++) { for (theory_var v = 0; v < num; v++) {
if (is_int(v)) if (is_int(v))
continue; continue;
if (!get_context().is_shared(get_enode(v)))
continue;
inf_numeral const & val = get_value(v); inf_numeral const & val = get_value(v);
rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational(); rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
theory_var v2; theory_var v2;

10
src/smt/theory_arith_nl.h
View file

@ -655,6 +655,7 @@ namespace smt {
return get_value(v, computed_epsilon) == val; return get_value(v, computed_epsilon) == val;
} }
/** /**
\brief Return true if for every monomial x_1 * ... * x_n, \brief Return true if for every monomial x_1 * ... * x_n,
get_value(x_1) * ... * get_value(x_n) = get_value(x_1 * ... * x_n) get_value(x_1) * ... * get_value(x_n) = get_value(x_1 * ... * x_n)
@ -2309,8 +2310,9 @@ namespace smt {
if (m_nl_monomials.empty()) if (m_nl_monomials.empty())
return FC_DONE; return FC_DONE;
if (check_monomial_assignments()) if (check_monomial_assignments()) {
return FC_DONE; return FC_DONE;
}
if (!m_params.m_nl_arith) if (!m_params.m_nl_arith)
return FC_GIVEUP; return FC_GIVEUP;
@ -2338,8 +2340,9 @@ namespace smt {
if (!max_min_nl_vars()) if (!max_min_nl_vars())
return FC_CONTINUE; return FC_CONTINUE;
if (check_monomial_assignments()) if (check_monomial_assignments()) {
return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE; return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
}
svector<theory_var> vars; svector<theory_var> vars;
get_non_linear_cluster(vars); get_non_linear_cluster(vars);
@ -2391,8 +2394,9 @@ namespace smt {
} }
while (m_nl_strategy_idx != old_idx); while (m_nl_strategy_idx != old_idx);
if (check_monomial_assignments()) if (check_monomial_assignments()) {
return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE; return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
}
TRACE("non_linear", display(tout);); TRACE("non_linear", display(tout););