mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix model generation for non-linear expressions, reported by Martin Suda and Giles Reger
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
3a0e9e8f53
commit
b42973152f
|
@ -946,6 +946,7 @@ namespace smt {
|
|||
//
|
||||
// -----------------------------------
|
||||
typedef int_hashtable<int_hash, default_eq<int> > row_set;
|
||||
bool m_model_depends_on_computed_epsilon;
|
||||
unsigned m_nl_rounds;
|
||||
bool m_nl_gb_exhausted;
|
||||
unsigned m_nl_strategy_idx; // for fairness
|
||||
|
|
|
@ -1405,6 +1405,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
final_check_status theory_arith<Ext>::final_check_core() {
|
||||
m_model_depends_on_computed_epsilon = false;
|
||||
unsigned old_idx = m_final_check_idx;
|
||||
final_check_status result = FC_DONE;
|
||||
final_check_status ok;
|
||||
|
@ -1669,6 +1670,7 @@ namespace smt {
|
|||
m_liberal_final_check(true),
|
||||
m_changed_assignment(false),
|
||||
m_assume_eq_head(0),
|
||||
m_model_depends_on_computed_epsilon(false),
|
||||
m_nl_rounds(0),
|
||||
m_nl_gb_exhausted(false),
|
||||
m_nl_new_exprs(m),
|
||||
|
@ -3220,7 +3222,9 @@ namespace smt {
|
|||
m_factory = alloc(arith_factory, get_manager());
|
||||
m.register_factory(m_factory);
|
||||
compute_epsilon();
|
||||
refine_epsilon();
|
||||
if (!m_model_depends_on_computed_epsilon) {
|
||||
refine_epsilon();
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
|
|
|
@ -638,6 +638,7 @@ namespace smt {
|
|||
if (!val.get_infinitesimal().is_zero() && !computed_epsilon) {
|
||||
compute_epsilon();
|
||||
computed_epsilon = true;
|
||||
m_model_depends_on_computed_epsilon = true;
|
||||
}
|
||||
return val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
|
||||
}
|
||||
|
@ -652,14 +653,18 @@ namespace smt {
|
|||
bool theory_arith<Ext>::check_monomial_assignment(theory_var v, bool & computed_epsilon) {
|
||||
SASSERT(is_pure_monomial(var2expr(v)));
|
||||
expr * m = var2expr(v);
|
||||
rational val(1);
|
||||
rational val(1), v_val;
|
||||
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
|
||||
expr * arg = to_app(m)->get_arg(i);
|
||||
theory_var curr = expr2var(arg);
|
||||
SASSERT(curr != null_theory_var);
|
||||
val *= get_value(curr, computed_epsilon);
|
||||
v_val = get_value(curr, computed_epsilon);
|
||||
TRACE("non_linear", tout << mk_pp(arg, get_manager()) << " = " << v_val << "\n";);
|
||||
val *= v_val;
|
||||
}
|
||||
return get_value(v, computed_epsilon) == val;
|
||||
v_val = get_value(v, computed_epsilon);
|
||||
TRACE("non_linear", tout << "v" << v << " := " << v_val << " == " << val << "\n";);
|
||||
return v_val == val;
|
||||
}
|
||||
|
||||
|
||||
|
@ -2356,6 +2361,7 @@ namespace smt {
|
|||
*/
|
||||
template<typename Ext>
|
||||
final_check_status theory_arith<Ext>::process_non_linear() {
|
||||
m_model_depends_on_computed_epsilon = false;
|
||||
if (m_nl_monomials.empty())
|
||||
return FC_DONE;
|
||||
|
||||
|
|
Loading…
Reference in a new issue