mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add missing fixed propagations on negated integer inequalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
ae5a713e81
commit
21a31fcd26
|
|
@ -46,9 +46,6 @@ Revision History:
|
|||
|
||||
namespace lp {
|
||||
|
||||
typedef unsigned lpvar;
|
||||
const lpvar null_lpvar = UINT_MAX;
|
||||
const constraint_index null_ci = UINT_MAX;
|
||||
|
||||
class lar_solver : public column_namer {
|
||||
struct term_hasher {
|
||||
|
|
@ -123,9 +120,7 @@ public:
|
|||
static_matrix<double, double> & A_d();
|
||||
static_matrix<double, double > const & A_d() const;
|
||||
|
||||
static bool valid_index(unsigned j){ return static_cast<int>(j) >= 0;}
|
||||
|
||||
bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); }
|
||||
static bool valid_index(unsigned j) { return static_cast<int>(j) >= 0;}
|
||||
|
||||
bool column_is_int(unsigned j) const;
|
||||
bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); }
|
||||
|
|
@ -136,7 +131,8 @@ public:
|
|||
}
|
||||
|
||||
unsigned external_to_column_index(unsigned) const;
|
||||
|
||||
|
||||
// NSB code review: function seems misnamed. 'j' can be a term index. Columns are not term indices.
|
||||
const mpq& get_column_value_rational(unsigned j) const {
|
||||
if (tv::is_term(j)) {
|
||||
j = m_var_register.external_to_local(j);
|
||||
|
|
@ -147,8 +143,6 @@ public:
|
|||
bool column_is_fixed(unsigned j) const;
|
||||
bool column_is_free(unsigned j) const;
|
||||
|
||||
bool well_formed(lar_term const& t) const;
|
||||
|
||||
const lar_term & get_term(unsigned j) const;
|
||||
|
||||
public:
|
||||
|
|
@ -203,6 +197,14 @@ public:
|
|||
|
||||
bool compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs);
|
||||
|
||||
// columns
|
||||
|
||||
bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); }
|
||||
column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
|
||||
bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
|
||||
const impq& get_value(column_index const& j) const { return get_column_value(j); }
|
||||
|
||||
|
||||
void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
|
||||
void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
|
||||
void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
|
||||
|
|
@ -280,14 +282,13 @@ public:
|
|||
|
||||
var_index external_to_local(unsigned j) const {
|
||||
var_index local_j;
|
||||
if (
|
||||
m_var_register.external_is_used(j, local_j) ||
|
||||
m_term_register.external_is_used(j, local_j))
|
||||
{
|
||||
return local_j;
|
||||
}
|
||||
else
|
||||
if (m_var_register.external_is_used(j, local_j) ||
|
||||
m_term_register.external_is_used(j, local_j)) {
|
||||
return local_j;
|
||||
}
|
||||
else {
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
|
||||
bool column_has_upper_bound(unsigned j) const {
|
||||
|
|
@ -298,11 +299,11 @@ public:
|
|||
return m_mpq_lar_core_solver.m_r_solver.column_has_lower_bound(j);
|
||||
}
|
||||
|
||||
const impq& get_upper_bound(unsigned j) const {
|
||||
const impq& get_upper_bound(column_index j) const {
|
||||
return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j];
|
||||
}
|
||||
|
||||
const impq& get_lower_bound(unsigned j) const {
|
||||
const impq& get_lower_bound(column_index j) const {
|
||||
return m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j];
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -27,10 +27,14 @@ namespace nla {
|
|||
}
|
||||
|
||||
namespace lp {
|
||||
|
||||
typedef unsigned var_index;
|
||||
typedef unsigned constraint_index;
|
||||
typedef unsigned row_index;
|
||||
enum lconstraint_kind { LE = -2, LT = -1 , GE = 2, GT = 1, EQ = 0, NE = 3 };
|
||||
typedef unsigned lpvar;
|
||||
const lpvar null_lpvar = UINT_MAX;
|
||||
const constraint_index null_ci = UINT_MAX;
|
||||
|
||||
|
||||
// index that comes from term or variable.
|
||||
|
|
@ -79,6 +83,7 @@ class column_index {
|
|||
public:
|
||||
column_index(unsigned j): m_index(j) {}
|
||||
unsigned index() const { return m_index; }
|
||||
bool is_null() const { return m_index == null_lpvar; }
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1371,19 +1371,19 @@ void core::update_to_refine_of_var(lpvar j) {
|
|||
}
|
||||
|
||||
bool core::patch_blocker(lpvar u, const monic& m) const {
|
||||
SASSERT(m_to_refine.contains(m.var()));
|
||||
if (var_is_used_in_a_correct_monic(u)) {
|
||||
TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool ret = u == m.var() || m.contains_var(u);
|
||||
|
||||
TRACE("nla_solver", tout << "u = " << u << ", m = "; print_monic(m, tout) <<
|
||||
"ret = " << ret << "\n";);
|
||||
|
||||
return ret;
|
||||
SASSERT(m_to_refine.contains(m.var()));
|
||||
if (var_is_used_in_a_correct_monic(u)) {
|
||||
TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool ret = u == m.var() || m.contains_var(u);
|
||||
|
||||
TRACE("nla_solver", tout << "u = " << u << ", m = "; print_monic(m, tout) <<
|
||||
"ret = " << ret << "\n";);
|
||||
|
||||
return ret;
|
||||
}
|
||||
|
||||
bool core::try_to_patch(lpvar k, const rational& v, const monic & m) {
|
||||
return m_lar_solver.try_to_patch(k, v,
|
||||
|
|
|
|||
|
|
@ -750,9 +750,7 @@ namespace qe {
|
|||
expr_ref tmp1(m), tmp2(m);
|
||||
expr *a0, *a1;
|
||||
eqs.reset();
|
||||
conj_enum::iterator it = conjs.begin(), end = conjs.end();
|
||||
for (; it != end; ++it) {
|
||||
expr* e = *it;
|
||||
for (expr* e : conjs) {
|
||||
bool is_leq = false;
|
||||
|
||||
if (m.is_eq(e, a0, a1) && is_arith(a0)) {
|
||||
|
|
@ -1548,10 +1546,8 @@ public:
|
|||
{}
|
||||
|
||||
~arith_plugin() override {
|
||||
bounds_cache::iterator it = m_bounds_cache.begin(), end = m_bounds_cache.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->get_value());
|
||||
}
|
||||
for (auto & kv : m_bounds_cache)
|
||||
dealloc(kv.get_value());
|
||||
}
|
||||
|
||||
void assign(contains_app& contains_x, expr* fml, rational const& vl) override {
|
||||
|
|
@ -2397,9 +2393,7 @@ public:
|
|||
bool update_bounds(bounds_proc& bounds, contains_app& contains_x, expr* fml, atom_set const& tbl, bool is_pos)
|
||||
{
|
||||
app_ref tmp(m);
|
||||
atom_set::iterator it = tbl.begin(), end = tbl.end();
|
||||
for (; it != end; ++it) {
|
||||
app* e = *it;
|
||||
for (app* e : tbl) {
|
||||
if (!contains_x(e)) {
|
||||
continue;
|
||||
}
|
||||
|
|
@ -2468,14 +2462,10 @@ public:
|
|||
}
|
||||
|
||||
~nlarith_plugin() override {
|
||||
bcs_t::iterator it = m_cache.begin(), end = m_cache.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->get_value());
|
||||
}
|
||||
weights_t::iterator it2 = m_weights.begin(), e2 = m_weights.end();
|
||||
for (; it2 != e2; ++it2) {
|
||||
dealloc(it2->get_value());
|
||||
}
|
||||
for (auto & kv : m_cache)
|
||||
dealloc(kv.get_value());
|
||||
for (auto& kv : m_weights)
|
||||
dealloc(kv.get_value());
|
||||
}
|
||||
|
||||
bool simplify(expr_ref& fml) override {
|
||||
|
|
@ -2605,9 +2595,7 @@ public:
|
|||
}
|
||||
|
||||
void update_bounds(expr_ref_vector& lits, atom_set const& tbl, bool is_pos) {
|
||||
atom_set::iterator it = tbl.begin(), end = tbl.end();
|
||||
for (; it != end; ++it) {
|
||||
app* e = *it;
|
||||
for (app* e : tbl) {
|
||||
lits.push_back(is_pos?e:m.mk_not(e));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -974,9 +974,6 @@ namespace {
|
|||
}
|
||||
|
||||
void assign_lit_eh(literal l) override {
|
||||
// if (m_current_generation > stop_gen)
|
||||
// m_current_generation--;
|
||||
|
||||
expr * e = m_context.bool_var2expr(l.var());
|
||||
if (e == m_current_goal)
|
||||
return;
|
||||
|
|
@ -1096,7 +1093,6 @@ namespace {
|
|||
|
||||
void set_goal(expr * e)
|
||||
{
|
||||
|
||||
if (e == m_current_goal) return;
|
||||
|
||||
GOAL_START();
|
||||
|
|
|
|||
|
|
@ -468,7 +468,7 @@ namespace smt {
|
|||
SASSERT(upper || new_bound->get_bound_kind() == B_LOWER);
|
||||
theory_var v = new_bound->get_var();
|
||||
set_bound_core(v, new_bound, upper);
|
||||
if ((propagate_eqs() || propagate_diseqs()) && is_fixed(v))
|
||||
if ((propagate_eqs() || propagate_diseqs()) && is_fixed(v))
|
||||
fixed_var_eh(v);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -84,7 +84,7 @@ public:
|
|||
}
|
||||
virtual ~bound() {}
|
||||
smt::theory_var get_var() const { return m_var; }
|
||||
lpvar lp_solver_var() const { return m_vi; }
|
||||
lp::tv tv() const { return lp::tv::raw(m_vi); }
|
||||
smt::bool_var get_bv() const { return m_bv; }
|
||||
bound_kind get_bound_kind() const { return m_bound_kind; }
|
||||
bool is_int() const { return m_is_int; }
|
||||
|
|
@ -114,7 +114,6 @@ std::ostream& operator<<(std::ostream& out, bound const& b) {
|
|||
struct stats {
|
||||
unsigned m_assert_lower;
|
||||
unsigned m_assert_upper;
|
||||
unsigned m_add_rows;
|
||||
unsigned m_bounds_propagations;
|
||||
unsigned m_num_iterations;
|
||||
unsigned m_num_iterations_with_no_progress;
|
||||
|
|
@ -842,26 +841,21 @@ class theory_lra::imp {
|
|||
void add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2) {
|
||||
m_constraint_sources.setx(index, equality_source, null_source);
|
||||
m_equalities.setx(index, enode_pair(n1, n2), enode_pair(0, 0));
|
||||
++m_stats.m_add_rows;
|
||||
}
|
||||
|
||||
void add_ineq_constraint(lp::constraint_index index, literal lit) {
|
||||
m_constraint_sources.setx(index, inequality_source, null_source);
|
||||
m_inequalities.setx(index, lit, null_literal);
|
||||
++m_stats.m_add_rows;
|
||||
TRACE("arith", lp().constraints().display(tout, index) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";);
|
||||
}
|
||||
|
||||
void add_def_constraint(lp::constraint_index index) {
|
||||
m_constraint_sources.setx(index, definition_source, null_source);
|
||||
m_definitions.setx(index, null_theory_var, null_theory_var);
|
||||
++m_stats.m_add_rows;
|
||||
}
|
||||
|
||||
void add_def_constraint(lp::constraint_index index, theory_var v) {
|
||||
m_constraint_sources.setx(index, definition_source, null_source);
|
||||
m_definitions.setx(index, v, null_theory_var);
|
||||
++m_stats.m_add_rows;
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -1609,8 +1603,8 @@ public:
|
|||
if (!th.is_relevant_and_shared(n1)) {
|
||||
continue;
|
||||
}
|
||||
lpvar vj = lp().external_to_column_index(v);
|
||||
if (vj == lp::null_lpvar)
|
||||
lp::column_index vj = lp().to_column_index(v);
|
||||
if (vj.is_null())
|
||||
continue;
|
||||
theory_var other = m_model_eqs.insert_if_not_there(v);
|
||||
if (other == v) {
|
||||
|
|
@ -1619,14 +1613,14 @@ public:
|
|||
enode * n2 = get_enode(other);
|
||||
if (n1->get_root() == n2->get_root())
|
||||
continue;
|
||||
if (!lp().column_is_fixed(vj)) {
|
||||
vars.push_back(vj);
|
||||
if (!lp().is_fixed(vj)) {
|
||||
vars.push_back(vj.index());
|
||||
}
|
||||
else if (!m_tmp_var_set.contains(other) ) {
|
||||
unsigned other_j = lp().external_to_column_index(other);
|
||||
if (!lp().column_is_fixed(other_j)) {
|
||||
lp::column_index other_j = lp().to_column_index(other);
|
||||
if (!lp().is_fixed(other_j)) {
|
||||
m_tmp_var_set.insert(other);
|
||||
vars.push_back(other_j);
|
||||
vars.push_back(other_j.index());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -2447,6 +2441,7 @@ public:
|
|||
});
|
||||
++m_stats.m_bound_propagations1;
|
||||
assign(lit, m_core, m_eqs, m_params);
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -2999,6 +2994,8 @@ public:
|
|||
|
||||
void assert_bound(bool_var bv, bool is_true, lp_api::bound& b) {
|
||||
lp::constraint_index ci = b.get_constraint(is_true);
|
||||
lp::column_index j = lp().to_column_index(b.get_var());
|
||||
bool was_fixed = lp().is_fixed(j);
|
||||
m_solver->activate(ci);
|
||||
if (is_infeasible()) {
|
||||
return;
|
||||
|
|
@ -3010,7 +3007,10 @@ public:
|
|||
else {
|
||||
++m_stats.m_assert_upper;
|
||||
}
|
||||
propagate_eqs(b.lp_solver_var(), ci, k, b);
|
||||
inf_rational const& value = b.get_value(is_true);
|
||||
if (value.is_rational()) {
|
||||
propagate_eqs(b.tv(), ci, k, b, value.get_rational());
|
||||
}
|
||||
}
|
||||
|
||||
lp_api::bound* mk_var_bound(bool_var bv, theory_var v, lp_api::bound_kind bk, rational const& bound) {
|
||||
|
|
@ -3054,22 +3054,30 @@ public:
|
|||
typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
|
||||
value2var m_fixed_var_table;
|
||||
|
||||
void propagate_eqs(lpvar vi, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b) {
|
||||
if (propagate_eqs()) {
|
||||
rational const& value = b.get_value();
|
||||
void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b, rational const& value) {
|
||||
bool best_bound = false;
|
||||
if (k == lp::GE) {
|
||||
best_bound = set_lower_bound(t, ci, value);
|
||||
}
|
||||
else if (k == lp::LE) {
|
||||
best_bound = set_upper_bound(t, ci, value);
|
||||
}
|
||||
|
||||
if (propagate_eqs() && best_bound) {
|
||||
if (k == lp::GE) {
|
||||
if (set_lower_bound(vi, ci, value) && has_upper_bound(vi, ci, value)) {
|
||||
if (has_upper_bound(t.index(), ci, value)) {
|
||||
fixed_var_eh(b.get_var(), value);
|
||||
}
|
||||
}
|
||||
else if (k == lp::LE) {
|
||||
if (set_upper_bound(vi, ci, value) && has_lower_bound(vi, ci, value)) {
|
||||
if (has_lower_bound(t.index(), ci, value)) {
|
||||
fixed_var_eh(b.get_var(), value);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool dump_lemmas() const { return m_arith_params.m_arith_dump_lemmas; }
|
||||
|
||||
bool propagate_eqs() const { return m_arith_params.m_arith_propagate_eqs && m_num_conflicts < m_arith_params.m_arith_propagation_threshold; }
|
||||
|
|
@ -3080,9 +3088,9 @@ public:
|
|||
|
||||
bool proofs_enabled() const { return m.proofs_enabled(); }
|
||||
|
||||
bool set_upper_bound(lpvar vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, false); }
|
||||
bool set_upper_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); }
|
||||
|
||||
bool set_lower_bound(lpvar vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, true); }
|
||||
bool set_lower_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); }
|
||||
|
||||
vector<constraint_bound> m_history;
|
||||
template<typename Ctx, typename T, bool CallDestructors=true>
|
||||
|
|
@ -3106,17 +3114,16 @@ public:
|
|||
};
|
||||
|
||||
|
||||
bool set_bound(lpvar vi, lp::constraint_index ci, rational const& v, bool is_lower) {
|
||||
|
||||
if (lp::tv::is_term(vi)) {
|
||||
lpvar ti = lp::tv::unmask_term(vi);
|
||||
bool set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower) {
|
||||
if (tv.is_term()) {
|
||||
lpvar ti = tv.id();
|
||||
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
|
||||
if (vec.size() <= ti) {
|
||||
vec.resize(ti + 1, constraint_bound(UINT_MAX, rational()));
|
||||
}
|
||||
constraint_bound& b = vec[ti];
|
||||
if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) {
|
||||
TRACE("arith", tout << "tighter bound " << lp().get_variable_name(vi) << "\n";);
|
||||
TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";);
|
||||
m_history.push_back(vec[ti]);
|
||||
ctx().push_trail(history_trail<context, constraint_bound>(vec, ti, m_history));
|
||||
b.first = ci;
|
||||
|
|
@ -3125,17 +3132,16 @@ public:
|
|||
return true;
|
||||
}
|
||||
else {
|
||||
TRACE("arith", tout << "not a term " << vi << "\n";);
|
||||
TRACE("arith", tout << "not a term " << tv.to_string() << "\n";);
|
||||
// m_solver already tracks bounds on proper variables, but not on terms.
|
||||
bool is_strict = false;
|
||||
rational b;
|
||||
if (is_lower) {
|
||||
return lp().has_lower_bound(vi, ci, b, is_strict) && !is_strict && b == v;
|
||||
return lp().has_lower_bound(tv.id(), ci, b, is_strict) && !is_strict && b == v;
|
||||
}
|
||||
else {
|
||||
return lp().has_upper_bound(vi, ci, b, is_strict) && !is_strict && b == v;
|
||||
}
|
||||
|
||||
return lp().has_upper_bound(tv.id(), ci, b, is_strict) && !is_strict && b == v;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -3188,11 +3194,13 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
bool is_equal(theory_var x, theory_var y) const { return get_enode(x)->get_root() == get_enode(y)->get_root(); }
|
||||
|
||||
bool is_equal(theory_var x, theory_var y) const {
|
||||
return get_enode(x)->get_root() == get_enode(y)->get_root();
|
||||
}
|
||||
|
||||
void fixed_var_eh(theory_var v1, rational const& bound) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "fix " << mk_bounded_pp(get_owner(v1), m) << " " << bound << "\n");
|
||||
|
||||
theory_var v2;
|
||||
value_sort_pair key(bound, is_int(v1));
|
||||
if (m_fixed_var_table.find(key, v2)) {
|
||||
|
|
@ -3888,7 +3896,6 @@ public:
|
|||
m_arith_eq_adapter.collect_statistics(st);
|
||||
st.update("arith-lower", m_stats.m_assert_lower);
|
||||
st.update("arith-upper", m_stats.m_assert_upper);
|
||||
st.update("arith-add-rows", m_stats.m_add_rows);
|
||||
st.update("arith-propagations", m_stats.m_bounds_propagations);
|
||||
st.update("arith-iterations", m_stats.m_num_iterations);
|
||||
st.update("arith-factorizations", lp().settings().stats().m_num_factorizations);
|
||||
|
|
|
|||
|
|
@ -631,6 +631,7 @@ namespace smt {
|
|||
cex = expr_ref(m_autil.mk_ge(mk_strlen(term), mk_int(0)), m);
|
||||
return false;
|
||||
}
|
||||
SASSERT(varLen_value.is_unsigned() && "actually arithmetic solver can assign it a very large number");
|
||||
TRACE("str_fl", tout << "creating character terms for variable " << mk_pp(term, m) << ", length = " << varLen_value << std::endl;);
|
||||
ptr_vector<expr> new_chars;
|
||||
for (unsigned i = 0; i < varLen_value.get_unsigned(); ++i) {
|
||||
|
|
|
|||
|
|
@ -313,7 +313,7 @@ class parallel_tactic : public tactic {
|
|||
unsigned mult = static_cast<unsigned>(pow(exp, m_depth - 1));
|
||||
p.set_uint("inprocess.max", pp.simplify_inprocess_max() * mult);
|
||||
p.set_uint("restart.max", pp.simplify_restart_max() * mult);
|
||||
p.set_bool("lookahead_simplify", true);
|
||||
p.set_bool("lookahead_simplify", m_depth > 2);
|
||||
p.set_bool("retain_blocked_clauses", retain_blocked);
|
||||
p.set_uint("max_conflicts", pp.simplify_max_conflicts());
|
||||
if (m_depth > 1) p.set_uint("bce_delay", 0);
|
||||
|
|
@ -475,8 +475,8 @@ private:
|
|||
|
||||
simplify_again:
|
||||
++num_simplifications;
|
||||
s.inc_depth(1);
|
||||
// simplify
|
||||
s.inc_depth(1);
|
||||
if (canceled(s)) return;
|
||||
switch (s.simplify()) {
|
||||
case l_undef: break;
|
||||
|
|
|
|||
Loading…
Reference in a new issue