mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix #2962

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-10 11:43:13 -08:00
parent 26eb23c05b
commit f1abc71c35
11 changed files with 71 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/math/lp/hnf_cutter.cpp
View file

@ -127,16 +127,7 @@ namespace lp {
t += H[l][k]*row[l];
}
row[k] = -t / H[k][k];
}
// // test region
// vector<mpq> ei(H.row_count(), zero_of_type<mpq>());
// ei[i] = one_of_type<mpq>();
// vector<mpq> pr = row * H;
// pr.shrink(ei.size());
// lp_assert(ei == pr);
// // end test region
}
}
void hnf_cutter::fill_term(const vector<mpq> & row, lar_term& t) {
@ -220,7 +211,6 @@ namespace lp {
}
}
bool hnf_cutter::hnf_has_var_with_non_integral_value() const {
for (unsigned j : vars())
if (!lia.get_value(j).is_int())

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

@ -17,6 +17,7 @@ namespace lp {
int_solver::int_solver(lar_solver& lar_slv) :
lra(lar_slv),
lrac(lra.m_mpq_lar_core_solver),
m_number_of_calls(0),
m_hnf_cutter(*this),
m_hnf_cut_period(settings().hnf_cut_period()) {
@ -26,15 +27,17 @@ int_solver::int_solver(lar_solver& lar_slv) :
// this will allow to enable and disable tracking of the pivot rows
struct check_return_helper {
lar_solver& lra;
lar_core_solver& lrac;
bool m_track_pivoted_rows;
check_return_helper(lar_solver& ls) :
lra(ls),
lrac(ls.m_mpq_lar_core_solver),
m_track_pivoted_rows(lra.get_track_pivoted_rows()) {
TRACE("pivoted_rows", tout << "pivoted rows = " << lra.m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
TRACE("pivoted_rows", tout << "pivoted rows = " << lrac.m_r_solver.m_pivoted_rows->size() << std::endl;);
lra.set_track_pivoted_rows(false);
}
~check_return_helper() {
TRACE("pivoted_rows", tout << "pivoted rows = " << lra.m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
TRACE("pivoted_rows", tout << "pivoted rows = " << lrac.m_r_solver.m_pivoted_rows->size() << std::endl;);
lra.set_track_pivoted_rows(m_track_pivoted_rows);
}
};
@ -82,7 +85,7 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
num = 0;
for (unsigned i = 0; i < lra.A_r().row_count(); i++) {
unsigned j = lra.m_mpq_lar_core_solver.m_r_basis[i];
unsigned j = lrac.m_r_basis[i];
if (column_is_int_inf(j)) {
num++;
lra.print_row(lra.A_r().m_rows[i], out);
@ -94,7 +97,7 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
}
bool int_solver::current_solution_is_inf_on_cut() const {
const auto & x = lra.m_mpq_lar_core_solver.m_r_x;
const auto & x = lrac.m_r_x;
impq v = m_t.apply(x);
mpq sign = m_upper ? one_of_type<mpq>() : -one_of_type<mpq>();
CTRACE("current_solution_is_inf_on_cut", v * sign <= impq(m_k) * sign,
@ -141,7 +144,7 @@ bool int_solver::value_is_int(unsigned j) const {
}
unsigned int_solver::random() {
return lra.get_core_solver().settings().random_next();
return settings().random_next();
}
const impq& int_solver::upper_bound(unsigned j) const {
@ -189,7 +192,7 @@ lia_move int_solver::hnf_cut() {
void int_solver::set_value_for_nbasic_column_ignore_old_values(unsigned j, const impq & new_val) {
lp_assert(!is_base(j));
auto & x = lra.m_mpq_lar_core_solver.m_r_x[j];
auto & x = lrac.m_r_x[j];
auto delta = new_val - x;
x = new_val;
TRACE("int_solver", tout << "x[" << j << "] = " << x << "\n";);
@ -197,8 +200,7 @@ void int_solver::set_value_for_nbasic_column_ignore_old_values(unsigned j, const
}
void int_solver::patch_nbasic_column(unsigned j) {
auto & lcs = lra.m_mpq_lar_core_solver;
impq & val = lcs.m_r_x[j];
impq & val = lrac.m_r_x[j];
bool inf_l, inf_u;
impq l, u;
mpq m;
@ -243,7 +245,7 @@ void int_solver::patch_nbasic_column(unsigned j) {
lia_move int_solver::patch_nbasic_columns() {
settings().stats().m_patches++;
lp_assert(is_feasible());
for (unsigned j : lra.m_mpq_lar_core_solver.m_r_nbasis) {
for (unsigned j : lrac.m_r_nbasis) {
patch_nbasic_column(j);
}
lp_assert(is_feasible());
@ -256,7 +258,7 @@ lia_move int_solver::patch_nbasic_columns() {
bool int_solver::has_lower(unsigned j) const {
switch (lra.m_mpq_lar_core_solver.m_column_types()[j]) {
switch (lrac.m_column_types()[j]) {
case column_type::fixed:
case column_type::boxed:
case column_type::lower_bound:
@ -267,7 +269,7 @@ bool int_solver::has_lower(unsigned j) const {
}
bool int_solver::has_upper(unsigned j) const {
switch (lra.m_mpq_lar_core_solver.m_column_types()[j]) {
switch (lrac.m_column_types()[j]) {
case column_type::fixed:
case column_type::boxed:
case column_type::upper_bound:
@ -292,8 +294,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
}
bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
auto & lcs = lra.m_mpq_lar_core_solver;
if (lcs.m_r_heading[j] >= 0) // the basic var
if (lrac.m_r_heading[j] >= 0) // the basic var
return false;
TRACE("random_update", display_column(tout, j) << ", is_int = " << column_is_int(j) << "\n";);
@ -318,7 +319,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
for (const auto &c : A.column(j)) {
row_index = c.var();
const mpq & a = c.coeff();
unsigned i = lcs.m_r_basis[row_index];
unsigned i = lrac.m_r_basis[row_index];
TRACE("random_update", tout << "i = " << i << ", a = " << a << "\n";);
if (column_is_int(i) && !a.is_int())
m = lcm(m, denominator(a));
@ -329,7 +330,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
if (!inf_l && !inf_u && l >= u) break;
row_index = c.var();
const mpq & a = c.coeff();
unsigned i = lcs.m_r_basis[row_index];
unsigned i = lrac.m_r_basis[row_index];
impq const & xi = get_value(i);
#define SET_BOUND(_fn_, a, b, x, y, z) \
@ -345,18 +346,18 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
if (a.is_neg()) {
if (has_lower(i)) {
SET_BOUND(set_lower, l, inf_l, a, xi, lcs.m_r_lower_bounds()[i]);
SET_BOUND(set_lower, l, inf_l, a, xi, lrac.m_r_lower_bounds()[i]);
}
if (has_upper(i)) {
SET_BOUND(set_upper, u, inf_u, a, xi, lcs.m_r_upper_bounds()[i]);
SET_BOUND(set_upper, u, inf_u, a, xi, lrac.m_r_upper_bounds()[i]);
}
}
else {
if (has_upper(i)) {
SET_BOUND(set_lower, l, inf_l, a, xi, lcs.m_r_upper_bounds()[i]);
SET_BOUND(set_lower, l, inf_l, a, xi, lrac.m_r_upper_bounds()[i]);
}
if (has_lower(i)) {
SET_BOUND(set_upper, u, inf_u, a, xi, lcs.m_r_lower_bounds()[i]);
SET_BOUND(set_upper, u, inf_u, a, xi, lrac.m_r_lower_bounds()[i]);
}
}
++rounds;
@ -381,18 +382,18 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
bool int_solver::is_feasible() const {
auto & lcs = lra.m_mpq_lar_core_solver;
lp_assert(
lcs.m_r_solver.calc_current_x_is_feasible_include_non_basis() ==
lcs.m_r_solver.current_x_is_feasible());
return lcs.m_r_solver.current_x_is_feasible();
lrac.m_r_solver.calc_current_x_is_feasible_include_non_basis() ==
lrac.m_r_solver.current_x_is_feasible());
return lrac.m_r_solver.current_x_is_feasible();
}
const impq & int_solver::get_value(unsigned j) const {
return lra.m_mpq_lar_core_solver.m_r_x[j];
return lrac.m_r_x[j];
}
std::ostream& int_solver::display_column(std::ostream & out, unsigned j) const {
return lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
return lrac.m_r_solver.print_column_info(j, out);
return out;
}
@ -401,23 +402,23 @@ bool int_solver::column_is_int_inf(unsigned j) const {
}
bool int_solver::is_base(unsigned j) const {
return lra.m_mpq_lar_core_solver.m_r_heading[j] >= 0;
return lrac.m_r_heading[j] >= 0;
}
bool int_solver::is_boxed(unsigned j) const {
return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed;
return lrac.m_column_types[j] == column_type::boxed;
}
bool int_solver::is_fixed(unsigned j) const {
return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed;
return lrac.m_column_types[j] == column_type::fixed;
}
bool int_solver::is_free(unsigned j) const {
return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::free_column;
return lrac.m_column_types[j] == column_type::free_column;
}
bool int_solver::at_bound(unsigned j) const {
auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
auto & mpq_solver = lrac.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
case column_type::boxed:
@ -434,7 +435,7 @@ bool int_solver::at_bound(unsigned j) const {
}
bool int_solver::at_lower(unsigned j) const {
auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
auto & mpq_solver = lrac.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
case column_type::boxed:
@ -446,7 +447,7 @@ bool int_solver::at_lower(unsigned j) const {
}
bool int_solver::at_upper(unsigned j) const {
auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
auto & mpq_solver = lrac.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
case column_type::boxed:
@ -458,7 +459,7 @@ bool int_solver::at_upper(unsigned j) const {
}
void int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
auto & rslv = lra.m_mpq_lar_core_solver.m_r_solver;
auto & rslv = lrac.m_r_solver;
for (const auto &c: rslv.m_A.m_rows[row_index]) {
if (numeric_traits<mpq>::is_pos(c.coeff()))
out << "+";
@ -524,20 +525,19 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
}
bool int_solver::non_basic_columns_are_at_bounds() const {
auto & lcs = lra.m_mpq_lar_core_solver;
for (unsigned j :lcs.m_r_nbasis) {
auto & val = lcs.m_r_x[j];
switch (lcs.m_column_types()[j]) {
for (unsigned j : lrac.m_r_nbasis) {
auto & val = lrac.m_r_x[j];
switch (lrac.m_column_types()[j]) {
case column_type::boxed:
if (val != lcs.m_r_lower_bounds()[j] && val != lcs.m_r_upper_bounds()[j])
if (val != lrac.m_r_lower_bounds()[j] && val != lrac.m_r_upper_bounds()[j])
return false;
break;
case column_type::lower_bound:
if (val != lcs.m_r_lower_bounds()[j])
if (val != lrac.m_r_lower_bounds()[j])
return false;
break;
case column_type::upper_bound:
if (val != lcs.m_r_upper_bounds()[j])
if (val != lrac.m_r_upper_bounds()[j])
return false;
break;
default:

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

@ -29,6 +29,7 @@ Revision History:
namespace lp {
class lar_solver;
class lar_core_solver;
class int_solver {
friend class create_cut;
@ -39,6 +40,7 @@ class int_solver {
friend class hnf_cutter;
lar_solver& lra;
lar_core_solver& lrac;
unsigned m_number_of_calls;
lar_term m_t; // the term to return in the cut
mpq m_k; // the right side of the cut

4
src/sat/sat_aig_cuts.cpp
View file

@ -29,7 +29,7 @@ namespace sat {
}
vector<cut_set> const& aig_cuts::operator()() {
if (true || m_config.m_full) flush_roots();
if (m_config.m_full) flush_roots();
unsigned_vector node_ids = filter_valid_nodes();
TRACE("aig_simplifier", display(tout););
augment(node_ids);
@ -412,7 +412,7 @@ namespace sat {
}
bool aig_cuts::insert_aux(unsigned v, node const& n) {
if (false && !m_config.m_full) return false;
if (!m_config.m_full) return false;
unsigned num_gt = 0, num_eq = 0;
for (node const& n2 : m_aig[v]) {
if (eq(n, n2)) return false;

2
src/sat/sat_aig_cuts.h
View file

@ -63,7 +63,7 @@ namespace sat {
unsigned m_max_aux;
unsigned m_max_insertions;
bool m_full;
config(): m_max_cutset_size(20), m_max_aux(5), m_max_insertions(20), m_full(false) {}
config(): m_max_cutset_size(20), m_max_aux(5), m_max_insertions(20), m_full(true) {}
};
private:

21
src/sat/sat_aig_simplifier.cpp
View file

@ -228,17 +228,18 @@ namespace sat {
xf.set(on_xor);
xf(clauses);
if (m_config.m_enable_lut) {
std::function<void(uint64_t, bool_var_vector const&, bool_var)> on_lut =
[&,this](uint64_t lut, bool_var_vector const& vars, bool_var v) {
m_stats.m_xluts++;
m_aig_cuts.add_cut(v, lut, vars);
};
lut_finder lf(s);
lf.set(on_lut);
lf(clauses);
}
#if 0
std::function<void(uint64_t, bool_var_vector const&, bool_var)> on_lut =
[&,this](uint64_t lut, bool_var_vector const& vars, bool_var v) {
m_stats.m_xluts++;
m_aig_cuts.add_cut(v, lut, vars);
};
lut_finder lf(s);
lf.set(on_lut);
lf(clauses);
statistics st;
collect_statistics(st);
st.display(std::cout);

4
src/sat/sat_aig_simplifier.h
View file

@ -36,6 +36,7 @@ namespace sat {
struct config {
bool m_enable_units; // enable learning units
bool m_enable_dont_cares; // enable applying don't cares to LUTs
bool m_enable_lut; // enable lut finding
bool m_learn_implies; // learn binary clauses
bool m_learned2aig; // add learned clauses to AIGs used by cut-set enumeration
bool m_validate_cuts; // enable direct validation of generated cuts
@ -44,11 +45,12 @@ namespace sat {
config():
m_enable_units(true),
m_enable_dont_cares(true),
m_enable_lut(false),
m_learn_implies(false),
m_learned2aig(true),
m_validate_cuts(false),
m_validate_lemmas(false),
m_simulate_eqs(true) {}
m_simulate_eqs(false) {}
};
private:
struct report;

2
src/sat/sat_solver.cpp
View file

@ -1930,7 +1930,7 @@ namespace sat {
anf.collect_statistics(m_aux_stats);
// TBD: throttle anf_delay based on yield
}
if (m_aig_simplifier && m_simplifications > m_config.m_aig_delay && !inconsistent()) {
(*m_aig_simplifier)();
}

2
src/smt/smt_theory.cpp
View file

@ -105,7 +105,7 @@ namespace smt {
out << ")";
}
else {
out << "#" << n->get_id();
out << mk_bounded_pp(n, get_manager(), 1);
}
return out;
}

2
src/smt/theory_arith_core.h
View file

@ -1369,7 +1369,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::internalize_eq_eh(app * atom, bool_var v) {
expr* _lhs, *_rhs;
expr* _lhs = nullptr, *_rhs = nullptr;
if (m_params.m_arith_eager_eq_axioms && get_manager().is_eq(atom, _lhs, _rhs) && is_app(_lhs) && is_app(_rhs)) {
context & ctx = get_context();
app * lhs = to_app(_lhs);

8
src/smt/theory_lra.cpp
View file

@ -1088,6 +1088,13 @@ public:
if (is_arith(n1) && is_arith(n2) && n1 != n2) {
m_arith_eq_adapter.mk_axioms(n1, n2);
}
// internalization of ite expressions produces equalities of the form
// (= x (ite c x y)) and (= y (ite c x y))
// this step ensures that a shared enode is attached
// with the ite expression.
else if (m.is_ite(lhs) || m.is_ite(rhs)) {
m_arith_eq_adapter.mk_axioms(n1, n2);
}
}
void assign_eh(bool_var v, bool is_true) {
@ -1134,6 +1141,7 @@ public:
}
void apply_sort_cnstr(enode* n, sort*) {
TRACE("arith", tout << "sort constraint: " << mk_pp(n->get_owner(), m) << "\n";);
if (!th.is_attached_to_var(n)) {
theory_var v = mk_var(n->get_owner(), false);
register_theory_var_in_lar_solver(v);