mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 16:55:47 +00:00
Code Activity

arith updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-05-14 15:53:58 -07:00
parent 62e1ec0698
commit e5231c040d
20 changed files with 526 additions and 165 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/lp/explanation.h
View file

@ -48,6 +48,15 @@ public:
SASSERT(m_vector.empty());
m_set.insert(j);
}
void remove(constraint_index j) {
m_set.remove(j);
unsigned i = 0;
for (auto& p : m_vector)
if (p.first != j)
m_vector[i++] = p;
m_vector.shrink(i);
}
void add_expl(const explanation& e) {
if (e.m_vector.empty()) {

83
src/math/lp/int_solver.cpp
View file

@ -17,51 +17,29 @@ namespace lp {
int_solver::patcher::patcher(int_solver& lia):
lia(lia),
lra(lia.lra),
lrac(lia.lrac),
m_num_nbasic_patches(0),
m_patch_cost(0),
m_next_patch(0),
m_delay(0)
lrac(lia.lrac)
{}
bool int_solver::patcher::should_apply() {
#if 1
return true;
#else
if (m_delay == 0) {
return true;
}
--m_delay;
return false;
#endif
}
lia_move int_solver::patcher::operator()() {
return patch_nbasic_columns();
}
lia_move int_solver::patcher::patch_nbasic_columns() {
lia.settings().stats().m_patches++;
lp_assert(lia.is_feasible());
m_num_nbasic_patches = 0;
m_patch_cost = 0;
for (unsigned j : lia.lrac.m_r_nbasis) {
patch_nbasic_column(j);
m_patch_success = 0;
m_patch_fail = 0;
unsigned num = lra.A_r().column_count();
for (unsigned v = 0; v < num; v++) {
if (lia.is_base(v))
continue;
patch_nbasic_column(v);
}
// for (unsigned j : lia.lrac.m_r_nbasis)
// patch_nbasic_column(j);
lp_assert(lia.is_feasible());
verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << "\n";
if (!lia.has_inf_int()) {
lia.settings().stats().m_patches_success++;
m_delay = 0;
m_next_patch = 0;
return lia_move::sat;
}
if (m_patch_cost > 0 && m_num_nbasic_patches * 10 < m_patch_cost) {
m_delay = std::min(20u, m_next_patch++);
}
else {
m_delay = 0;
m_next_patch = 0;
}
return lia_move::undef;
}
@ -71,10 +49,8 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
impq l, u;
mpq m;
bool has_free = lia.get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);
m_patch_cost += lra.A_r().number_of_non_zeroes_in_column(j);
if (!has_free) {
if (!has_free)
return;
}
bool m_is_one = m.is_one();
bool val_is_int = lia.value_is_int(j);
@ -82,6 +58,7 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
if (val_is_int && (m_is_one || (val.x / m).is_int())) {
return;
}
TRACE("patch_int",
tout << "TARGET j" << j << " -> [";
if (inf_l) tout << "-oo"; else tout << l;
@ -89,9 +66,24 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
if (inf_u) tout << "oo"; else tout << u;
tout << "]";
tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";);
#if 0
verbose_stream() << "path " << m << " ";
if (!inf_l) verbose_stream() << "infl " << l.x << " ";
if (!inf_u) verbose_stream() << "infu " << u.x << " ";
verbose_stream() << "\n";
if (m.is_big() || (!inf_l && l.x.is_big()) || (!inf_u && u.x.is_big())) {
return;
}
#endif
verbose_stream() << "TARGET v" << j << " -> [";
if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x);
verbose_stream() << ", ";
if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x);
verbose_stream() << "]";
verbose_stream() << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";
if (!inf_l) {
l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
if (inf_u || l <= u) {
@ -99,7 +91,8 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
lra.set_value_for_nbasic_column(j, l);
}
else {
--m_num_nbasic_patches;
--m_patch_success;
++m_patch_fail;
TRACE("patch_int", tout << "not patching " << l << "\n";);
}
}
@ -112,7 +105,7 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
lra.set_value_for_nbasic_column(j, impq(0));
TRACE("patch_int", tout << "patching with 0\n";);
}
++m_num_nbasic_patches;
++m_patch_success;
}
int_solver::int_solver(lar_solver& lar_slv) :
@ -554,6 +547,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
return false;
const impq & x = get_value(j);
// x, the value of j column, might be shifted on a multiple of m
if (inf_l && inf_u) {
impq new_val = m * impq(random() % (range + 1)) + x;
lra.set_value_for_nbasic_column(j, new_val);
@ -570,6 +564,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
if (!inf_l && !inf_u && l >= u)
return false;
if (inf_u) {
SASSERT(!inf_l);
impq new_val = x + m * impq(random() % (range + 1));
@ -640,9 +635,6 @@ int int_solver::select_int_infeasible_var() {
unsigned n = 0;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
unsigned prev_usage = 0; // to quiet down the compile
unsigned k = 0;
unsigned usage;
unsigned j;
enum state { small_box, is_small_value, any_value, not_found };
state st = not_found;
@ -650,11 +642,10 @@ int int_solver::select_int_infeasible_var() {
// 1. small box
// 2. small value
// 3. any value
for (; k < lra.r_basis().size(); k++) {
j = lra.r_basis()[k];
for (unsigned j : lra.r_basis()) {
if (!column_is_int_inf(j))
continue;
usage = lra.usage_in_terms(j);
unsigned usage = lra.usage_in_terms(j);
if (is_boxed(j) && (new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
SASSERT(!is_fixed(j));
if (st != small_box) {
@ -688,12 +679,12 @@ int int_solver::select_int_infeasible_var() {
continue;
SASSERT(st == not_found || st == any_value);
st = any_value;
if (n == 0 /*|| usage > prev_usage*/) {
if (n == 0 || usage > prev_usage) {
result = j;
prev_usage = usage;
n = 1;
}
else if (usage > 0 && /*usage == prev_usage && */ (random() % (++n) == 0))
else if (usage > 0 && usage == prev_usage && (random() % (++n) == 0))
result = j;
}

10
src/math/lp/int_solver.h
View file

@ -44,14 +44,12 @@ class int_solver {
int_solver& lia;
lar_solver& lra;
lar_core_solver& lrac;
unsigned m_num_nbasic_patches;
unsigned m_patch_cost;
unsigned m_next_patch;
unsigned m_delay;
unsigned m_patch_success = 0;
unsigned m_patch_fail = 0;
public:
patcher(int_solver& lia);
bool should_apply();
lia_move operator()();
bool should_apply() const { return true; }
lia_move operator()() { return patch_nbasic_columns(); }
void patch_nbasic_column(unsigned j);
private:
lia_move patch_nbasic_columns();

12
src/math/lp/lar_core_solver_def.h
View file

@ -86,12 +86,12 @@ void lar_core_solver::solve() {
TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
lp_assert(m_r_solver.inf_set_is_correct());
TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.inf_set_size() << ", int_infs = " << get_number_of_non_ints() << std::endl;);
if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) {
m_r_solver.set_status(lp_status::OPTIMAL);
TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
return;
}
TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.inf_set_size() << ", int_infs = " << get_number_of_non_ints() << std::endl;);
if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) {
m_r_solver.set_status(lp_status::OPTIMAL);
TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
return;
}
++settings().stats().m_need_to_solve_inf;
lp_assert( r_basis_is_OK());

76
src/math/lp/lar_solver.cpp
View file

@ -41,7 +41,6 @@ namespace lp {
for (auto t : m_terms)
delete t;
}
bool lar_solver::sizes_are_correct() const {
lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size());
@ -50,7 +49,6 @@ namespace lp {
return true;
}
std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostream& out) const {
out << "implied bound\n";
unsigned v = be.m_j;
@ -1350,8 +1348,8 @@ namespace lp {
}
bool lar_solver::term_is_int(const vector<std::pair<mpq, unsigned int>>& coeffs) const {
for (auto const& p : coeffs)
if (!(column_is_int(p.second) && p.first.is_int()))
for (auto const& [coeff, v] : coeffs)
if (!(column_is_int(v) && coeff.is_int()))
return false;
return true;
}
@ -1382,7 +1380,7 @@ namespace lp {
// the lower/upper bound is not strict.
// the LP obtained by making the bound strict is infeasible
// -> the column has to be fixed
bool lar_solver::is_fixed_at_bound(column_index const& j) {
bool lar_solver::is_fixed_at_bound(column_index const& j, vector<std::tuple<explanation, column_index, bool, mpq>>& bounds) {
if (column_is_fixed(j))
return false;
mpq val;
@ -1391,50 +1389,56 @@ namespace lp {
lp::lconstraint_kind k;
if (column_has_upper_bound(j) &&
get_upper_bound(j).x == val) {
verbose_stream() << "check upper " << j << "\n";
push();
if (column_is_int(j))
k = LE, val -= 1;
else
k = LT;
auto ci = mk_var_bound(j, k, val);
update_column_type_and_bound(j, k, val, ci);
push();
k = column_is_int(j) ? LE : LT;
auto ci = mk_var_bound(j, k, column_is_int(j) ? val - 1 : val);
update_column_type_and_bound(j, k, column_is_int(j) ? val - 1 : val, ci);
auto st = find_feasible_solution();
bool infeasible = st == lp_status::INFEASIBLE;
if (infeasible) {
explanation exp;
get_infeasibility_explanation(exp);
unsigned_vector cis;
exp.remove(ci);
verbose_stream() << "tight upper bound " << j << " " << val << "\n";
bounds.push_back({exp, j, true, val});
}
pop(1);
return st == lp_status::INFEASIBLE;
return infeasible;
}
if (column_has_lower_bound(j) &&
get_lower_bound(j).x == val) {
verbose_stream() << "check lower " << j << "\n";
push();
if (column_is_int(j))
k = GE, val += 1;
else
k = GT;
auto ci = mk_var_bound(j, k, val);
update_column_type_and_bound(j, k, val, ci);
k = column_is_int(j) ? GE : GT;
auto ci = mk_var_bound(j, k, column_is_int(j) ? val + 1 : val);
update_column_type_and_bound(j, k, column_is_int(j) ? val + 1 : val, ci);
auto st = find_feasible_solution();
bool infeasible = st == lp_status::INFEASIBLE;
if (infeasible) {
explanation exp;
get_infeasibility_explanation(exp);
exp.remove(ci);
verbose_stream() << "tight lower bound " << j << " " << val << "\n";
bounds.push_back({exp, j, false, val});
}
pop(1);
return st == lp_status::INFEASIBLE;
return infeasible;
}
return false;
}
bool lar_solver::has_fixed_at_bound() {
bool lar_solver::has_fixed_at_bound(vector<std::tuple<explanation, column_index, bool, mpq>>& bounds) {
verbose_stream() << "has-fixed-at-bound\n";
unsigned num_fixed = 0;
for (unsigned j = 0; j < A_r().m_columns.size(); ++j) {
auto ci = column_index(j);
if (is_fixed_at_bound(ci)) {
++num_fixed;
if (is_fixed_at_bound(ci, bounds))
verbose_stream() << "fixed " << j << "\n";
}
}
verbose_stream() << "num fixed " << num_fixed << "\n";
if (num_fixed > 0)
verbose_stream() << "num fixed " << bounds.size() << "\n";
if (!bounds.empty())
find_feasible_solution();
return num_fixed > 0;
return !bounds.empty();
}
@ -1613,6 +1617,18 @@ namespace lp {
return ret;
}
/**
* \brief ensure there is a column index corresponding to vi
* If vi is already a column, just return vi
* If vi is for a term, then create a row that uses the term.
*/
var_index lar_solver::ensure_column(var_index vi) {
if (lp::tv::is_term(vi))
return to_column(vi);
else
return vi;
}
void lar_solver::add_row_from_term_no_constraint(const lar_term* term, unsigned term_ext_index) {
TRACE("dump_terms", print_term(*term, tout) << std::endl;);

5
src/math/lp/lar_solver.h
View file

@ -366,8 +366,8 @@ public:
}
}
bool is_fixed_at_bound(column_index const& j);
bool has_fixed_at_bound();
bool is_fixed_at_bound(column_index const& j, vector<std::tuple<explanation, column_index, bool, mpq>>& bounds);
bool has_fixed_at_bound(vector<std::tuple<explanation, column_index, bool, mpq>>& bounds);
bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
@ -376,6 +376,7 @@ public:
bool compare_values(var_index j, lconstraint_kind kind, const mpq & right_side);
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i);
void register_existing_terms();
var_index ensure_column(var_index vi);
constraint_index add_var_bound(var_index, lconstraint_kind, const mpq &);
constraint_index add_var_bound_check_on_equal(var_index, lconstraint_kind, const mpq &, var_index&);

32
src/math/lp/lp_api.h
View file

@ -103,6 +103,7 @@ namespace lp_api {
unsigned m_conflicts;
unsigned m_bound_propagations1;
unsigned m_bound_propagations2;
unsigned m_bound_axioms;
unsigned m_assert_diseq;
unsigned m_assert_eq;
unsigned m_gomory_cuts;
@ -113,21 +114,22 @@ namespace lp_api {
memset(this, 0, sizeof(*this));
}
void collect_statistics(statistics& st) const {
st.update("arith-lower", m_assert_lower);
st.update("arith-upper", m_assert_upper);
st.update("arith-propagations", m_bounds_propagations);
st.update("arith-iterations", m_num_iterations);
st.update("arith-pivots", m_need_to_solve_inf);
st.update("arith-plateau-iterations", m_num_iterations_with_no_progress);
st.update("arith-fixed-eqs", m_fixed_eqs);
st.update("arith-conflicts", m_conflicts);
st.update("arith-bound-propagations-lp", m_bound_propagations1);
st.update("arith-bound-propagations-cheap", m_bound_propagations2);
st.update("arith-diseq", m_assert_diseq);
st.update("arith-eq", m_assert_eq);
st.update("arith-gomory-cuts", m_gomory_cuts);
st.update("arith-assume-eqs", m_assume_eqs);
st.update("arith-branch", m_branch);
st.update("arith assert lower", m_assert_lower);
st.update("arith assert upper", m_assert_upper);
st.update("arith propagations", m_bounds_propagations);
st.update("arith iterations", m_num_iterations);
st.update("arith pivots", m_need_to_solve_inf);
st.update("arith plateau iterations", m_num_iterations_with_no_progress);
st.update("arith fixed eqs", m_fixed_eqs);
st.update("arith conflicts", m_conflicts);
st.update("arith bound propagations lp", m_bound_propagations1);
st.update("arith bound propagations cheap", m_bound_propagations2);
st.update("arith bound axioms", m_bound_axioms);
st.update("arith diseq", m_assert_diseq);
st.update("arith eq", m_assert_eq);
st.update("arith gomory cuts", m_gomory_cuts);
st.update("arith assume eqs", m_assume_eqs);
st.update("arith branch", m_branch);
}
};

29
src/math/lp/lp_core_solver_base_def.h
View file

@ -117,10 +117,10 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::
add_delta_to_entering(unsigned entering, const X& delta) {
m_x[entering] += delta;
for (const auto & c : m_A.m_columns[entering]) {
unsigned i = c.var();
m_x[m_basis[i]] -= delta * m_A.get_val(c);
}
for (const auto & c : m_A.m_columns[entering]) {
unsigned i = c.var();
m_x[m_basis[i]] -= delta * m_A.get_val(c);
}
}
@ -295,7 +295,7 @@ divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col) {
}
template <typename T, typename X> bool lp_core_solver_base<T, X>::
pivot_column_tableau(unsigned j, unsigned piv_row_index) {
if (!divide_row_by_pivot(piv_row_index, j))
if (!divide_row_by_pivot(piv_row_index, j))
return false;
auto &column = m_A.m_columns[j];
int pivot_col_cell_index = -1;
@ -406,15 +406,16 @@ template <typename T, typename X> void lp_core_solver_base<T, X>::transpose_row
}
// j is the new basic column, j_basic - the leaving column
template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w) {
lp_assert(m_basis_heading[j] < 0);
lp_assert(m_basis_heading[j_basic] >= 0);
unsigned row_index = m_basis_heading[j_basic];
// the tableau case
if (pivot_column_tableau(j, row_index))
change_basis(j, j_basic);
else return false;
return true;
lp_assert(m_basis_heading[j] < 0);
lp_assert(m_basis_heading[j_basic] >= 0);
unsigned row_index = m_basis_heading[j_basic];
// the tableau case
if (pivot_column_tableau(j, row_index))
change_basis(j, j_basic);
else
return false;
return true;
}

4
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -59,6 +59,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
}
unsigned j_nz = this->m_m() + 1; // this number is greater than the max column size
std::list<unsigned>::iterator entering_iter = m_non_basis_list.end();
unsigned n = 0;
for (auto non_basis_iter = m_non_basis_list.begin(); number_of_benefitial_columns_to_go_over && non_basis_iter != m_non_basis_list.end(); ++non_basis_iter) {
unsigned j = *non_basis_iter;
if (!column_is_benefitial_for_entering_basis(j))
@ -71,8 +72,9 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
entering_iter = non_basis_iter;
if (number_of_benefitial_columns_to_go_over)
number_of_benefitial_columns_to_go_over--;
n = 1;
}
else if (t == j_nz && this->m_settings.random_next() % 2 == 0) {
else if (t == j_nz && this->m_settings.random_next() % (++n) == 0) {
entering_iter = non_basis_iter;
}
}// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);

4
src/smt/params/smt_params.cpp
View file

@ -246,7 +246,7 @@ void smt_params::setup_QF_LRA(static_features const& st) {
m_phase_selection = PS_THEORY;
if (!st.m_cnf) {
m_restart_strategy = RS_GEOMETRIC;
m_arith_stronger_lemmas = false;
m_arith_relax_bounds = false;
m_restart_adaptive = false;
}
m_arith_small_lemma_size = 32;
@ -288,7 +288,7 @@ void smt_params::setup_QF_LIA(static_features const& st) {
}
if (st.m_num_bin_clauses + st.m_num_units == st.m_num_clauses && st.m_cnf && st.m_arith_k_sum > rational(100000)) {
m_arith_bound_prop = bound_prop_mode::BP_NONE;
m_arith_stronger_lemmas = false;
m_arith_relax_bounds = false;
}
}

2
src/smt/params/theory_arith_params.cpp
View file

@ -52,7 +52,7 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_blands_rule_threshold);
DISPLAY_PARAM(m_arith_propagate_eqs);
DISPLAY_PARAM((unsigned)m_arith_bound_prop);
DISPLAY_PARAM(m_arith_stronger_lemmas);
DISPLAY_PARAM(m_arith_relax_bounds);
DISPLAY_PARAM(m_arith_skip_rows_with_big_coeffs);
DISPLAY_PARAM(m_arith_max_lemma_size);
DISPLAY_PARAM(m_arith_small_lemma_size);

2
src/smt/params/theory_arith_params.h
View file

@ -58,7 +58,7 @@ struct theory_arith_params {
unsigned m_arith_blands_rule_threshold = 1000;
bool m_arith_propagate_eqs = true;
bound_prop_mode m_arith_bound_prop = bound_prop_mode::BP_REFINE;
bool m_arith_stronger_lemmas = true;
bool m_arith_relax_bounds = true;
bool m_arith_skip_rows_with_big_coeffs = true;
unsigned m_arith_max_lemma_size = 128;
unsigned m_arith_small_lemma_size = 16;

4
src/smt/theory_arith.h
View file

@ -43,7 +43,7 @@ namespace smt {
struct theory_arith_stats {
unsigned m_conflicts, m_add_rows, m_pivots, m_diseq_cs, m_gomory_cuts, m_branches, m_gcd_tests, m_gcd_conflicts, m_patches, m_patches_succ;
unsigned m_assert_lower, m_assert_upper, m_assert_diseq, m_core2th_eqs, m_core2th_diseqs;
unsigned m_th2core_eqs, m_th2core_diseqs, m_bound_props, m_offset_eqs, m_fixed_eqs, m_offline_eqs;
unsigned m_th2core_eqs, m_th2core_diseqs, m_bound_props, m_bound_axioms, m_offset_eqs, m_fixed_eqs, m_offline_eqs;
unsigned m_max_min;
unsigned m_assume_eqs;
unsigned m_gb_simplify, m_gb_superpose, m_gb_compute_basis, m_gb_num_processed;
@ -541,7 +541,7 @@ namespace smt {
double adaptive_assertion_threshold() const { return m_params.m_arith_adaptive_assertion_threshold; }
unsigned max_lemma_size() const { return m_params.m_arith_max_lemma_size; }
unsigned small_lemma_size() const { return m_params.m_arith_small_lemma_size; }
bool relax_bounds() const { return m_params.m_arith_stronger_lemmas; }
bool relax_bounds() const { return m_params.m_arith_relax_bounds; }
bool skip_big_coeffs() const { return m_params.m_arith_skip_rows_with_big_coeffs; }
bool process_atoms() const;
unsigned get_num_conflicts() const { return m_num_conflicts; }

2
src/smt/theory_arith_aux.h
View file

@ -2141,6 +2141,8 @@ namespace smt {
if (candidates.empty())
return;
verbose_stream() << "candidates " << candidates.size() << "\n";
m_tmp_var_set.reset();
m_tmp_var_set2.reset();
for (theory_var v : candidates) {

18
src/smt/theory_arith_core.h
View file

@ -1148,6 +1148,7 @@ namespace smt {
mk_clause(~l1, l2, 3, coeffs);
}
}
++m_stats.m_bound_axioms;
}
template<typename Ext>
@ -1489,6 +1490,19 @@ namespace smt {
unsigned old_idx = m_final_check_idx;
final_check_status result = FC_DONE;
final_check_status ok;
//display(verbose_stream());
//exit(0);
if (false)
{
verbose_stream() << "final\n";
::statistics stats;
collect_statistics(stats);
stats.display(verbose_stream());
}
do {
if (ctx.get_cancel_flag()) {
return FC_GIVEUP;
@ -2812,10 +2826,11 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::explain_bound(row const & r, int idx, bool is_lower, inf_numeral & delta, antecedents& ante) {
SASSERT(delta >= inf_numeral::zero());
TRACE("arith_conflict", tout << "relax: " << relax_bounds() << " lits: " << ante.lits().size() << " eqs: " << ante.eqs().size() << " idx: " << idx << "\n";);
if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty())) {
return;
}
row_entry const & entry = r[idx];
numeral coeff = entry.m_coeff;
if (relax_bounds()) {
@ -2835,6 +2850,7 @@ namespace smt {
if (!b->has_justification()) {
continue;
}
if (!relax_bounds() || delta.is_zero()) {
TRACE("propagate_bounds", tout << "push justification: v" << it->m_var << "\n";);
b->push_justification(ante, it->m_coeff, coeffs_enabled());

22
src/smt/theory_arith_int.h
View file

@ -219,7 +219,7 @@ namespace smt {
{
std::function<expr*(void)> fn = [&]() { return m.mk_or(bound, m.mk_not(bound)); };
scoped_trace_stream _sts(*this, fn);
IF_VERBOSE(10, verbose_stream() << "branch " << bound << "\n");
IF_VERBOSE(4, verbose_stream() << "branch " << bound << "\n");
TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";);
ctx.internalize(bound, true);
ctx.mark_as_relevant(bound.get());
@ -670,13 +670,14 @@ namespace smt {
TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout););
literal l = null_literal;
context & ctx = get_context();
ctx.get_rewriter()(bound);
{
std::function<expr*(void)> fn = [&]() { return bound; };
scoped_trace_stream _sts(*this, fn);
ctx.internalize(bound, true);
}
l = ctx.get_literal(bound);
IF_VERBOSE(10, verbose_stream() << "cut " << bound << "\n");
IF_VERBOSE(4, verbose_stream() << "cut " << bound << "\n");
ctx.mark_as_relevant(l);
auto js = ctx.mk_justification(
gomory_cut_justification(
@ -906,6 +907,7 @@ namespace smt {
bool inf_l, inf_u;
inf_numeral l, u;
numeral m;
unsigned num_patched = 0, num_not_patched = 0;
for (theory_var v = 0; v < num; v++) {
if (!is_non_base(v))
continue;
@ -915,6 +917,7 @@ namespace smt {
// check whether value of v is already a multiple of m.
if ((get_value(v).get_rational() / m).is_int())
continue;
TRACE("patch_int",
tout << "TARGET v" << v << " -> [";
if (inf_l) tout << "-oo"; else tout << ceil(l);
@ -922,6 +925,15 @@ namespace smt {
if (inf_u) tout << "oo"; else tout << floor(u);
tout << "]";
tout << ", m: " << m << ", val: " << get_value(v) << ", is_int: " << is_int(v) << "\n";);
verbose_stream() << "TARGET v" << v << " -> [";
if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l);
verbose_stream() << ", ";
if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u);
verbose_stream() << "]";
verbose_stream() << ", m: " << m << ", val: " << get_value(v) << ", is_int: " << is_int(v) << "\n";
if (!inf_l)
l = ceil(l);
if (!inf_u)
@ -932,8 +944,11 @@ namespace smt {
if (!inf_u)
u = m*floor(u/m);
}
if (!inf_l && !inf_u && l > u)
if (!inf_l && !inf_u && l > u) {
++num_not_patched;
continue; // cannot patch
}
++num_patched;
if (!inf_l)
set_value(v, l);
else if (!inf_u)
@ -942,6 +957,7 @@ namespace smt {
set_value(v, inf_numeral(0));
}
SASSERT(m_to_patch.empty());
verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << "\n";
}
/**

3
src/smt/theory_arith_pp.h
View file

@ -33,13 +33,14 @@ namespace smt {
st.update("arith assert upper", m_stats.m_assert_upper);
st.update("arith assert diseq", m_stats.m_assert_diseq);
st.update("arith bound prop", m_stats.m_bound_props);
st.update("arith bound axioms", m_stats.m_bound_axioms);
st.update("arith fixed eqs", m_stats.m_fixed_eqs);
st.update("arith assume eqs", m_stats.m_assume_eqs);
st.update("arith offset eqs", m_stats.m_offset_eqs);
st.update("arith gcd tests", m_stats.m_gcd_tests);
st.update("arith gcd conflicts", m_stats.m_gcd_conflicts);
st.update("arith ineq splits", m_stats.m_branches);
st.update("arith gomory cuts", m_stats.m_gomory_cuts);
st.update("arith branch", m_stats.m_branches);
st.update("arith branch int", m_stats.m_branch_infeasible_int);
st.update("arith branch var", m_stats.m_branch_infeasible_var);
st.update("arith patches", m_stats.m_patches);

2
src/smt/theory_diff_logic_def.h
View file

@ -695,7 +695,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
template<typename Ext>
void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
m_nc_functor.reset();
m_graph.traverse_neg_cycle2(m_params.m_arith_stronger_lemmas, m_nc_functor);
m_graph.traverse_neg_cycle2(m_params.m_arith_relax_bounds, m_nc_functor);
inc_conflicts();
literal_vector const& lits = m_nc_functor.get_lits();
TRACE("arith_conflict",

370
src/smt/theory_lra.cpp
View file

@ -127,6 +127,7 @@ class theory_lra::imp {
ptr_vector<expr>& to_ensure_enode() { return m_st.m_to_ensure_enode; }
ptr_vector<expr>& to_ensure_var() { return m_st.m_to_ensure_var; }
void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); }
void add(theory_var v, rational const& c) { vars().push_back(v); coeffs().push_back(c); }
void set_back(unsigned i) {
if (terms().size() == i + 1) return;
terms()[i] = terms().back();
@ -335,17 +336,204 @@ class theory_lra::imp {
}
bool internalize_term2(app* term) {
TRACE("arith_internalize", tout << "internalising term:\n" << mk_pp(term, m) << "\n";);
theory_var v = internalize_term_core(term);
TRACE("arith_internalize", tout << "theory_var: " << v << "\n";);
return v != null_theory_var;
}
theory_var internalize_add(app* n) {
TRACE("add_bug", tout << "n: " << mk_pp(n, m) << "\n";);
CTRACE("internalize_add_bug", n->get_num_args() == 2 && n->get_arg(0) == n->get_arg(1), tout << "n: " << mk_pp(n, m) << "\n";);
SASSERT(a.is_add(n));
scoped_internalize_state st(*this);
for (expr* arg : *n)
internalize_internal_monomial(to_app(arg), st);
enode* e = mk_enode(n);
theory_var v = e->get_th_var(get_id());
if (v == null_theory_var)
v = internalize_linearized_def(n, st);
return v;
}
void internalize_internal_monomial(app* arg, scoped_internalize_state& st) {
expr* arg1, * arg2;
rational val, val2;
if (ctx().e_internalized(arg)) {
enode* e = ctx().get_enode(arg);
if (th.is_attached_to_var(e)) {
// there is already a theory variable (i.e., name) for arg.
st.add(e->get_th_var(get_id()), rational::one());
return;
}
}
if (a.is_extended_numeral(arg, val))
st.add(internalize_numeral(arg, val), rational::one());
else if (a.is_mul(arg, arg1, arg2)) {
if (a.is_extended_numeral(arg2, val))
std::swap(arg1, arg2);
if (a.is_extended_numeral(arg1, val)) {
st.add(internalize_term_core(to_app(arg2)), val);
if (reflect(arg)) {
internalize_term_core(to_app(arg1));
mk_enode(arg);
}
return;
}
}
st.add(internalize_term_core(arg), rational::one());
}
theory_var internalize_numeral(app* n, rational const& val) {
if (ctx().e_internalized(n))
return mk_var(n);
enode* e = mk_enode(n);
theory_var v = mk_var(n);
lpvar vi = get_lpvar(v);
if (vi == UINT_MAX) {
vi = lp().add_var(v, a.is_int(n));
add_def_constraint_and_equality(vi, lp::GE, val);
add_def_constraint_and_equality(vi, lp::LE, val);
register_fixed_var(v, val);
}
return v;
}
/**
\brief Internalize the terms of the form (* c (* t1 ... tn)) and (* t1 ... tn).
Return an alias for the term.
*/
theory_var internalize_mul1(app* arg) {
rational val;
TRACE("arith", tout << arg->get_num_args() << " " << mk_pp(arg, m) << "\n";);
SASSERT(a.is_mul(arg));
expr* arg0 = arg->get_arg(0);
expr* arg1 = arg->get_arg(1);
if (a.is_numeral(arg1))
std::swap(arg0, arg1);
if (a.is_numeral(arg0, val) && !a.is_numeral(arg1) && arg->get_num_args() == 2) {
if (val.is_zero())
return internalize_numeral(arg, val);
scoped_internalize_state st(*this);
if (reflect(arg))
internalize_term_core(to_app(arg0));
st.add(internalize_mul_core(to_app(arg1)), val);
mk_enode(arg);
return internalize_linearized_def(arg, st);
}
else
return internalize_mul_core(arg);
}
theory_var internalize_mul_core(app* t) {
TRACE("internalize_mul_core", tout << "internalizing...\n" << mk_pp(t, m) << "\n";);
if (!a.is_mul(t))
return internalize_term_core(t);
for (expr* arg : *t) {
theory_var v = internalize_term_core(to_app(arg));
if (v == null_theory_var)
mk_var(to_app(arg));
}
enode* e = mk_enode(t);
theory_var v = e->get_th_var(get_id());
if (v == null_theory_var)
v = mk_var(t);
return v;
}
/**
* \brief Internalize the given term and return an alias for it.
* Return null_theory_var if the term was not implemented by the theory yet.
*/
theory_var internalize_term_core(app* n) {
TRACE("arith_internalize_detail", tout << "internalize_term_core:\n" << mk_pp(n, m) << "\n";);
if (ctx().e_internalized(n)) {
enode* e = ctx().get_enode(n);
if (th.is_attached_to_var(e))
return e->get_th_var(get_id());
}
SASSERT(!a.is_uminus(n));
rational val;
if (a.is_add(n))
return internalize_add(n);
else if (a.is_extended_numeral(n, val))
return internalize_numeral(n, val);
else if (a.is_mul(n))
return internalize_mul1(n);
else if (a.is_arith_expr(n))
NOT_IMPLEMENTED_YET();
#if 0
else if (a.is_div(n))
return internalize_div(n);
else if (a.is_idiv(n))
return internalize_idiv(n);
else if (a.is_mod(n))
return internalize_mod(n);
else if (a.is_rem(n))
return internalize_rem(n);
else if (a.is_to_real(n))
return internalize_to_real(n);
else if (a.is_to_int(n))
return internalize_to_int(n);
else if (a.is_sub(n))
return internalize_sub(n);
if (a.is_power(n)) {
// unsupported
found_unsupported_op(n);
return mk_binary_op(n);
}
if (a.is_irrational_algebraic_numeral(n)) {
// unsupported
found_unsupported_op(n);
enode* e = mk_enode(n);
return mk_var(e);
}
if (a.get_family_id() == n->get_family_id()) {
if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n))
found_unsupported_op(n);
if (ctx().e_internalized(n))
return expr2var(n);
for (expr* arg : *n)
ctx().internalize(arg, false);
return mk_var(mk_enode(n));
}
#endif
TRACE("arith_internalize_detail", tout << "before:\n" << mk_pp(n, m) << "\n";);
if (!ctx().e_internalized(n))
ctx().internalize(n, false);
TRACE("arith_internalize_detail", tout << "after:\n" << mk_pp(n, m) << "\n";);
enode* e = ctx().get_enode(n);
if (!th.is_attached_to_var(e))
return mk_var(n);
else
return e->get_th_var(get_id());
}
void linearize_term(expr* term, scoped_internalize_state& st) {
st.push(term, rational::one());
linearize(st);
}
void linearize_ineq(expr* lhs, expr* rhs, scoped_internalize_state& st) {
st.push(lhs, rational::one());
st.push(rhs, rational::minus_one());
linearize(st);
}
void linearize(scoped_internalize_state& st) {
expr_ref_vector & terms = st.terms();
svector<theory_var>& vars = st.vars();
@ -371,6 +559,7 @@ class theory_lra::imp {
st.push(to_app(n)->get_arg(i), -coeffs[index]);
}
}
#if 1
else if (a.is_mul(n, n1, n2) && a.is_extended_numeral(n1, r)) {
coeffs[index] *= r;
terms[index] = n2;
@ -381,6 +570,29 @@ class theory_lra::imp {
terms[index] = n1;
st.to_ensure_enode().push_back(n2);
}
#else
else if (a.is_mul(n, n1, n2) && a.is_extended_numeral(n1, r)) {
internalize_args(n2);
VERIFY(internalize_term(to_app(n2)));
theory_var v = mk_var(n2);
coeffs[vars.size()] = r * coeffs[index];
vars.push_back(v);
get_lpvar(v);
verbose_stream() << v << "\n";
st.to_ensure_enode().push_back(n1);
++index;
}
else if (a.is_mul(n, n1, n2) && a.is_extended_numeral(n2, r)) {
VERIFY(internalize_term(to_app(n1)));
theory_var v = mk_var(n1);
coeffs[vars.size()] = r * coeffs[index];
vars.push_back(v);
get_lpvar(v);
verbose_stream() << v << "\n";
st.to_ensure_enode().push_back(n2);
++index;
}
#endif
else if (a.is_mul(n)) {
theory_var v = internalize_mul(to_app(n));
coeffs[vars.size()] = coeffs[index];
@ -663,8 +875,10 @@ class theory_lra::imp {
for (unsigned i = 0; i < vars.size(); ++i) {
theory_var var = vars[i];
rational const& r = m_columns[var];
if (!r.is_zero()) {
m_left_side.push_back(std::make_pair(r, register_theory_var_in_lar_solver(var)));
if (!r.is_zero()) {
auto vi = register_theory_var_in_lar_solver(var);
vi = lp().ensure_column(vi);
m_left_side.push_back({ r, vi });
m_columns[var].reset();
}
}
@ -672,12 +886,7 @@ class theory_lra::imp {
}
bool all_zeros(vector<rational> const& v) const {
for (rational const& r : v) {
if (!r.is_zero()) {
return false;
}
}
return true;
return all_of(v, [](rational const& r) { return r.is_zero(); });
}
void add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2) {
@ -850,8 +1059,9 @@ class theory_lra::imp {
else if (is_zero(st) && a.is_numeral(term)) {
return lp().local_to_external(get_zero(a.is_int(term)));
}
else {
else {
init_left_side(st);
lpvar vi = get_lpvar(v);
if (vi == UINT_MAX) {
if (m_left_side.empty()) {
@ -862,8 +1072,10 @@ class theory_lra::imp {
return v;
}
if (!st.offset().is_zero()) {
m_left_side.push_back(std::make_pair(st.offset(), get_one(a.is_int(term))));
verbose_stream() << "Offset row " << st.offset() << "\n";
m_left_side.push_back({ st.offset(), get_one(a.is_int(term)) });
}
if (m_left_side.empty()) {
vi = lp().add_var(v, a.is_int(term));
add_def_constraint_and_equality(vi, lp::GE, rational(0));
@ -872,7 +1084,7 @@ class theory_lra::imp {
else {
vi = lp().add_term(m_left_side, v);
SASSERT(lp::tv::is_term(vi));
TRACE("arith_verbose",
TRACE("arith_init",
tout << "v" << v << " := " << mk_pp(term, m)
<< " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
lp().print_term(lp().get_term(lp::tv::raw(vi)), tout) << "\n";);
@ -963,19 +1175,19 @@ public:
m_bool_var2bound.erase(bv);
ctx().set_var_theory(bv, get_id());
if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n2, r) && is_app(n1)) {
v = internalize_def(to_app(n1));
v = internalize_term_core(to_app(n1));
k = lp_api::upper_t;
}
else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n2, r) && is_app(n1)) {
v = internalize_def(to_app(n1));
v = internalize_term_core(to_app(n1));
k = lp_api::lower_t;
}
else if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n1, r) && is_app(n2)) {
v = internalize_def(to_app(n2));
v = internalize_term_core(to_app(n2));
k = lp_api::lower_t;
}
else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n1, r) && is_app(n2)) {
v = internalize_def(to_app(n2));
v = internalize_term_core(to_app(n2));
k = lp_api::upper_t;
}
else if (a.is_is_int(atom)) {
@ -1007,7 +1219,8 @@ public:
// skip
}
else {
internalize_def(term);
internalize_term2(term);
// internalize_def(term);
}
return true;
}
@ -1098,6 +1311,8 @@ public:
if (num_scopes == 0) {
return;
}
m_has_popped = true;
unsigned old_size = m_scopes.size() - num_scopes;
del_bounds(m_scopes[old_size].m_bounds_lim);
m_asserted_atoms.shrink(m_scopes[old_size].m_asserted_atoms_lim);
@ -1499,6 +1714,8 @@ public:
void random_update() {
if (m_nla && m_nla->need_check())
return;
if (!m_liberal_final_check)
return;
m_tmp_var_set.clear();
m_tmp_var_set.resize(th.get_num_vars());
m_model_eqs.reset();
@ -1536,7 +1753,9 @@ public:
tout << "v" << v << " ";
tout << "\n"; );
if (!vars.empty()) {
verbose_stream() << "random update " << vars.size() << "\n";
lp().random_update(vars.size(), vars.data());
m_changed_assignment = true;
}
}
@ -1552,8 +1771,9 @@ public:
unsigned old_sz = m_assume_eq_candidates.size();
unsigned num_candidates = 0;
int start = ctx().get_random_value();
for (theory_var i = 0; i < sz; ++i) {
for (int i = 0; i < sz; ++i) {
theory_var v = (i + start) % sz;
enode* n1 = get_enode(v);
if (!th.is_relevant_and_shared(n1)) {
continue;
@ -1646,10 +1866,84 @@ public:
return FC_GIVEUP;
}
bool m_has_propagated_fixed = false;
bool m_has_popped = false;
bool propagate_fixed() {
m_has_propagated_fixed = false;
vector<std::tuple<lp::explanation, lp::column_index, bool, lp::mpq>> bounds;
if (!lp().has_fixed_at_bound(bounds))
return false;
// verbose_stream() << "scope " << ctx().get_scope_level() << "\n";
for (auto const& [exp, j, lower, b] : bounds) {
auto t = lp().column2tv(j);
expr_ref trm(m);
if (t.is_term())
trm = term2expr(lp().get_term(t));
else
trm = var2expr(t.id());
expr* v = a.mk_numeral(b, a.is_int(trm));
expr* bound = lower ? a.mk_ge(trm, v) : a.mk_le(trm, v);
literal lit = mk_literal(bound);
reset_evidence();
for (auto ev : exp)
set_evidence(ev.ci(), m_core, m_eqs);
//verbose_stream() << "assign " << lit << " " << mk_pp(bound, m) << " " << ctx().get_assignment(lit) << "\n";
ctx().mark_as_relevant(bound);
//ctx().display(verbose_stream());
assign(lit, m_core, m_eqs, m_params);
/// verbose_stream() << "propagate " << lit << "\n";
//exit(0);
}
m_has_propagated_fixed = true;
m_has_popped = false;
return true;
}
unsigned m_final_check_idx = 0;
distribution m_dist { 0 };
bool m_liberal_final_check = false;
bool m_changed_assignment = false;
final_check_status final_check_eh() {
TRACE("arith_eq_adapter_info", m_arith_eq_adapter.display_already_processed(tout););
TRACE("arith", display(tout););
if (propagate_core())
return FC_CONTINUE;
if (delayed_assume_eqs())
return FC_CONTINUE;
m_liberal_final_check = true;
m_changed_assignment = false;
ctx().push_trail(value_trail<unsigned>(m_final_check_idx));
final_check_status result = final_check_core();
if (result != FC_DONE)
return result;
if (!m_changed_assignment)
return FC_DONE;
m_liberal_final_check = false;
m_changed_assignment = false;
result = final_check_core();
TRACE("arith", tout << "result: " << result << "\n";);
return result;
}
final_check_status final_check_core() {
if (false)
{
verbose_stream() << "final\n";
::statistics stats;
collect_statistics(stats);
stats.display(verbose_stream());
}
#if 0
if (!m_has_propagated_fixed && propagate_fixed())
return FC_CONTINUE;
#endif
if (propagate_core())
return FC_CONTINUE;
m_model_is_initialized = false;
@ -1661,13 +1955,11 @@ public:
}
bool giveup = false;
final_check_status st = FC_DONE;
m_final_check_idx = 0; // remove to experiment.
unsigned old_idx = m_final_check_idx;
switch (is_sat) {
case l_true:
TRACE("arith", display(tout));
// if (lp().has_fixed_at_bound()) // explain and propagate.
#if 0
m_dist.reset();
@ -1691,6 +1983,7 @@ public:
st = check_lia();
break;
default:
verbose_stream() << idx << "\n";
UNREACHABLE();
break;
}
@ -1713,11 +2006,11 @@ public:
switch (m_final_check_idx) {
case 0:
if (assume_eqs())
st = FC_CONTINUE;
st = check_lia();
break;
case 1:
st = check_lia();
if (assume_eqs())
st = FC_CONTINUE;
break;
case 2:
st = check_nla();
@ -2171,7 +2464,7 @@ public:
}
bool can_propagate_core() {
return m_asserted_atoms.size() > m_asserted_qhead || m_new_def;
return m_asserted_atoms.size() > m_asserted_qhead || m_new_def || (m_has_propagated_fixed && m_has_popped);
}
bool propagate() {
@ -2181,8 +2474,9 @@ public:
bool propagate_core() {
m_model_is_initialized = false;
flush_bound_axioms();
if (!can_propagate_core())
if (!can_propagate_core())
return false;
m_new_def = false;
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
@ -2196,6 +2490,10 @@ public:
assert_bound(bv, is_true, *b);
++m_asserted_qhead;
}
if (false && m_has_propagated_fixed && m_has_popped && propagate_fixed())
return true;
if (ctx().inconsistent()) {
m_bv_to_propagate.reset();
return true;
@ -2603,6 +2901,7 @@ public:
mk_clause(~l1, l2, 3, coeffs);
}
}
++m_stats.m_bound_axioms;
}
typedef lp_bounds::iterator iterator;
@ -3305,6 +3604,13 @@ public:
tout << "\n";
display_evidence(tout, m_explanation);
display(tout << "is-conflict: " << is_conflict << "\n"););
TRACE("arith_conflict",
display_evidence(tout, m_explanation);
for (auto lit : m_core)
ctx().display_literal_verbose(tout, lit);
);
for (auto ev : m_explanation)
set_evidence(ev.ci(), m_core, m_eqs);

2
src/smt/theory_utvpi_def.h
View file

@ -507,7 +507,7 @@ namespace smt {
TRACE("utvpi", a.display(*this, tout); tout << "\n";);
int edge_id = a.get_asserted_edge();
if (!enable_edge(edge_id)) {
m_graph.traverse_neg_cycle2(m_params.m_arith_stronger_lemmas, m_nc_functor);
m_graph.traverse_neg_cycle2(m_params.m_arith_relax_bounds, m_nc_functor);
set_conflict();
return false;
}