mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

re-enable feature that lets Z3 solver mixed integer/real constraints with additional information tha texpressions with sort real can only take integer values. Fixes regression on epsilon.smt2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-12 12:42:18 -08:00
parent e2d54940b4
commit 9a6fe93e6c
3 changed files with 12 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_arith.h
View file

@ -547,6 +547,7 @@ namespace smt {
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
bool is_int_expr(expr* e); bool is_int_expr(expr* e);
bool is_int(theory_var v) const { return m_data[v].m_is_int; } bool is_int(theory_var v) const { return m_data[v].m_is_int; }
bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); }
bool is_real(theory_var v) const { return !is_int(v); } bool is_real(theory_var v) const { return !is_int(v); }
bool get_implied_old_value(theory_var v, inf_numeral & r) const; bool get_implied_old_value(theory_var v, inf_numeral & r) const;
inf_numeral const & get_implied_value(theory_var v) const; inf_numeral const & get_implied_value(theory_var v) const;

8
src/smt/theory_arith_core.h
View file

@ -66,9 +66,9 @@ namespace smt {
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::is_int_expr(expr* e) { bool theory_arith<Ext>::is_int_expr(expr* e) {
return m_util.is_int(e);
#if 0 #if 0
Disable refined integer until equality propagation is fixed. return m_util.is_int(e);
#else
if (m_util.is_int(e)) return true; if (m_util.is_int(e)) return true;
if (is_uninterp(e)) return false; if (is_uninterp(e)) return false;
m_todo.reset(); m_todo.reset();
@ -3077,7 +3077,7 @@ namespace smt {
theory_var num = get_num_vars(); theory_var num = get_num_vars();
bool refine = false; bool refine = false;
for (theory_var v = 0; v < num; v++) { for (theory_var v = 0; v < num; v++) {
if (is_int(v)) if (is_int_src(v))
continue; continue;
if (!get_context().is_shared(get_enode(v))) if (!get_context().is_shared(get_enode(v)))
continue; continue;
@ -3088,7 +3088,7 @@ namespace smt {
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;
if (mapping.find(value, v2)) { if (mapping.find(value, v2)) {
SASSERT(!is_int(v2)); SASSERT(!is_int_src(v2));
if (get_value(v) != get_value(v2)) { if (get_value(v) != get_value(v2)) {
// v and v2 are not known to be equal. // v and v2 are not known to be equal.
// The choice of m_epsilon is making them equal. // The choice of m_epsilon is making them equal.

15
src/smt/theory_arith_eq.h
View file

@ -43,7 +43,7 @@ namespace smt {
CTRACE("arith_bug", !lower_bound(v).is_rational(), display_var(tout, v);); CTRACE("arith_bug", !lower_bound(v).is_rational(), display_var(tout, v););
SASSERT(lower_bound(v).is_rational()); SASSERT(lower_bound(v).is_rational());
numeral const & val = lower_bound(v).get_rational(); numeral const & val = lower_bound(v).get_rational();
value_sort_pair key(val, is_int(v)); value_sort_pair key(val, is_int_src(v));
theory_var v2; theory_var v2;
if (m_fixed_var_table.find(key, v2)) { if (m_fixed_var_table.find(key, v2)) {
if (v2 < static_cast<int>(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) { if (v2 < static_cast<int>(get_num_vars()) && is_fixed(v2) && lower_bound(v2).get_rational() == val) {
@ -51,7 +51,7 @@ namespace smt {
// The table m_fixed_var_table is not restored during backtrack. So, it may // The table m_fixed_var_table is not restored during backtrack. So, it may
// contain invalid (key -> value) pairs. So, we must check whether v2 is really equal to val (previous test) AND it has // contain invalid (key -> value) pairs. So, we must check whether v2 is really equal to val (previous test) AND it has
// the same sort of v. The following test was missing in a previous version of Z3. // the same sort of v. The following test was missing in a previous version of Z3.
if (!is_equal(v, v2) && is_int(v) == is_int(v2)) { if (!is_equal(v, v2) && is_int_src(v) == is_int_src(v2)) {
antecedents ante(*this); antecedents ante(*this);
// //
@ -226,7 +226,7 @@ namespace smt {
if (y == null_theory_var) { if (y == null_theory_var) {
// x is an implied fixed var at k. // x is an implied fixed var at k.
value_sort_pair key(k, is_int(x)); value_sort_pair key(k, is_int_src(x));
theory_var x2; theory_var x2;
if (m_fixed_var_table.find(key, x2) && if (m_fixed_var_table.find(key, x2) &&
x2 < static_cast<int>(get_num_vars()) && x2 < static_cast<int>(get_num_vars()) &&
@ -238,7 +238,7 @@ namespace smt {
// So, we must check whether x2 is really equal to k (previous test) // So, we must check whether x2 is really equal to k (previous test)
// AND has the same sort of x. // AND has the same sort of x.
// The following test was missing in a previous version of Z3. // The following test was missing in a previous version of Z3.
is_int(x) == is_int(x2) && is_int_src(x) == is_int_src(x2) &&
!is_equal(x, x2)) { !is_equal(x, x2)) {
antecedents ante(*this); antecedents ante(*this);
@ -254,7 +254,7 @@ namespace smt {
} }
} }
if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int(x) == is_int(y)) { if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int_src(x) == is_int_src(y)) {
// found equality x = y // found equality x = y
antecedents ante(*this); antecedents ante(*this);
collect_fixed_var_justifications(r, ante); collect_fixed_var_justifications(r, ante);
@ -294,7 +294,7 @@ namespace smt {
} }
if (new_eq) { if (new_eq) {
if (!is_equal(x, x2) && is_int(x) == is_int(x2)) { if (!is_equal(x, x2) && is_int_src(x) == is_int_src(x2)) {
SASSERT(y == y2 && k == k2); SASSERT(y == y2 && k == k2);
antecedents ante(*this); antecedents ante(*this);
collect_fixed_var_justifications(r, ante); collect_fixed_var_justifications(r, ante);
@ -323,11 +323,10 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) { void theory_arith<Ext>::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) {
// I doesn't make sense to propagate an equality (to the core) of variables of different sort.
SASSERT(is_int(x) == is_int(y));
// Ignore equality if variables are already known to be equal. // Ignore equality if variables are already known to be equal.
if (is_equal(x, y)) if (is_equal(x, y))
return; return;
// I doesn't make sense to propagate an equality (to the core) of variables of different sort.
if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) { if (get_manager().get_sort(var2expr(x)) != get_manager().get_sort(var2expr(y))) {
TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";); TRACE("arith", tout << mk_pp(var2expr(x), get_manager()) << " = " << mk_pp(var2expr(y), get_manager()) << "\n";);
return; return;