From ca3ce964ce27d4e24abdfd6eaa144e2a1d358970 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 18 Sep 2018 13:34:05 -0700 Subject: [PATCH 01/41] work on Gomory cut Signed-off-by: Lev --- src/smt/smt_arith_value.h | 2 +- src/util/lp/column_namer.h | 23 ------ src/util/lp/gomory.cpp | 141 ++++++++++++++++++++++++++++++++++--- src/util/lp/int_solver.h | 8 --- src/util/lp/lar_solver.cpp | 2 +- src/util/lp/lp_utils.h | 31 ++++++-- 6 files changed, 160 insertions(+), 47 deletions(-) diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h index 9b0f833ac..4e22b44f8 100644 --- a/src/smt/smt_arith_value.h +++ b/src/smt/smt_arith_value.h @@ -17,7 +17,7 @@ Author: Revision History: --*/ -#pragma once; +#pragma once #include "ast/arith_decl_plugin.h" #include "smt/smt_context.h" diff --git a/src/util/lp/column_namer.h b/src/util/lp/column_namer.h index e6e8e53a2..51baf445f 100644 --- a/src/util/lp/column_namer.h +++ b/src/util/lp/column_namer.h @@ -33,29 +33,6 @@ public: print_linear_combination_of_column_indices(coeff, out); } - template - void print_linear_combination_of_column_indices_only(const vector> & coeffs, std::ostream & out) const { - bool first = true; - for (const auto & it : coeffs) { - auto val = it.first; - if (first) { - first = false; - } else { - if (numeric_traits::is_pos(val)) { - out << " + "; - } else { - out << " - "; - val = -val; - } - } - if (val == -numeric_traits::one()) - out << " - "; - else if (val != numeric_traits::one()) - out << T_to_string(val); - - out << "v" << it.second; - } - } template diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 55098dccf..f936397d4 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -23,6 +23,16 @@ namespace lp { class gomory::imp { + inline static bool is_rational(const impq & n) { return is_zero(n.y); } + + inline static mpq fractional_part(const impq & n) { + lp_assert(is_rational(n)); + return n.x - floor(n.x); + } + inline static mpq fractional_part(const mpq & n) { + return n - floor(n); + } + lar_term & m_t; // the term to return in the cut mpq & m_k; // the right side of the cut explanation& m_ex; // the conflict explanation @@ -43,32 +53,31 @@ class gomory::imp { void int_case_in_gomory_cut(const mpq & a, unsigned j, mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) { lp_assert(is_int(j) && !a.is_int()); - mpq fj = int_solver::fractional_part(a); - lp_assert(fj.is_pos()); + mpq fj = fractional_part(a); TRACE("gomory_cut_detail", tout << a << " j=" << j << " k = " << m_k; tout << ", fj: " << fj << ", "; - tout << "f0: " << f0 << ", "; - tout << "1 - f0: " << 1 - f0 << ", "; + tout << "a - fj = " << a - fj << ", "; tout << (at_lower(j)?"at_lower":"at_upper")<< std::endl; ); + lp_assert(fj.is_pos() && (a - fj).is_int()); mpq new_a; mpq one_minus_fj = 1 - fj; if (at_lower(j)) { - new_a = fj < one_minus_f0? fj / one_minus_f0 : one_minus_fj / f0; + new_a = fj < one_minus_f0? fj / one_minus_f0 : (- one_minus_fj / f0); m_k.addmul(new_a, lower_bound(j).x); m_ex.push_justification(column_lower_bound_constraint(j), new_a); } else { lp_assert(at_upper(j)); // the upper terms are inverted: therefore we have the minus - new_a = - (fj < f0? fj / f0 : one_minus_fj / one_minus_f0); + new_a = - (fj < f0? fj / f0 : (- one_minus_fj / one_minus_f0)); m_k.addmul(new_a, upper_bound(j).x); m_ex.push_justification(column_upper_bound_constraint(j), new_a); } - TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << m_k << "\n";); m_t.add_monomial(new_a, j); lcm_den = lcm(lcm_den, denominator(new_a)); + TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";); } void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) { @@ -150,10 +159,117 @@ class gomory::imp { TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;); lp_assert(m_k.is_int()); } + + std::string var_name(unsigned j) const { + return std::string("x") + std::to_string(j); + } + + void dump_coeff_val(std::ostream & out, const mpq & a) const { + if (a.is_int()) { + if ( a >= zero_of_type()) + out << a; + else { + out << "( - " << - a << ") "; + } + } else { + if ( a >= zero_of_type()) + out << "(div " << numerator(a) << " " << denominator(a) << ")"; + else { + out << "(- ( div " << numerator(-a) << " " << denominator(-a) << "))"; + } + + } + } + + template + void dump_coeff(std::ostream & out, const T& c) const { + out << "( * "; + dump_coeff_val(out, c.coeff()); + out << " " << var_name(c.var()) << ")"; + } + + void dump_row_coefficients(std::ostream & out) const { + for (const auto& p : m_row) { + dump_coeff(out, p); + } + } + + void dump_the_row(std::ostream& out) const { + out << "; the row\n"; + out << "(assert ( = ( + "; + dump_row_coefficients(out); + out << ") 0))\n"; + } + + void dump_declarations(std::ostream& out) const { + // for a column j the var name is vj + for (const auto & p : m_row) { + out << "(declare-fun " << var_name(p.var()) << " () " + << (is_int(p.var())? "Int" : "Real") << ")\n"; + } + } + + void dump_lower_bound_expl(std::ostream & out, unsigned j) const { + out << "(assert ( >= " << var_name(j) << " " << lower_bound(j).x << "))\n"; + } + void dump_upper_bound_expl(std::ostream & out, unsigned j) const { + out << "(assert ( <= " << var_name(j) << " " << upper_bound(j).x << "))\n"; + } + + void dump_explanations(std::ostream& out) const { + for (const auto & p : m_row) { + unsigned j = p.var(); + if (j == m_inf_col) { + continue; + } + + if (column_is_fixed(j)) { + dump_lower_bound_expl(out, j); + dump_upper_bound_expl(out, j); + continue; + } + + if (at_lower(j)) { + dump_lower_bound_expl(out, j); + } else { + dump_upper_bound_expl(out, j); + } + } + } + + void dump_terms_coefficients(std::ostream & out) const { + for (const auto& p : m_t) { + dump_coeff(out, p); + } + } + + void dump_term_sum(std::ostream & out) const { + out << "( + "; + dump_terms_coefficients(out); + out << ")"; + } + + void dump_term_le_k(std::ostream & out) const { + out << "( <= "; + dump_term_sum(out); + out << m_k << ")"; + } + void dump_the_cut_assert(std::ostream & out) const { + out <<"(assert (not "; + dump_term_le_k(out); + out << "))\n"; + } + void dump_cut_and_constraints_as_smt_lemma(std::ostream& out) const { + dump_declarations(out); + dump_the_row(out); + dump_explanations(out); + dump_the_cut_assert(out); + out << "(check-sat)\n"; + } public: lia_move create_cut() { TRACE("gomory_cut", - tout << "applying cut at:\n"; m_int_solver.m_lar_solver->print_row(m_row, tout); tout << std::endl; + tout << "applying cut at:\n"; print_linear_combination_of_column_indices_only(m_row, tout); tout << std::endl; for (auto & p : m_row) { m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), tout); } @@ -164,7 +280,11 @@ public: m_k = 1; mpq lcm_den(1); bool some_int_columns = false; - mpq f0 = int_solver::fractional_part(get_value(m_inf_col)); + mpq f0 = fractional_part(get_value(m_inf_col)); + TRACE("gomory_cut_detail", tout << "f0: " << f0 << ", "; + tout << "1 - f0: " << 1 - f0 << ", get_value(m_inf_col).x - f0 = " << get_value(m_inf_col).x - f0;); + lp_assert(f0.is_pos() && (get_value(m_inf_col).x - f0).is_int()); + mpq one_min_f0 = 1 - f0; for (const auto & p : m_row) { unsigned j = p.var(); @@ -194,7 +314,8 @@ public: adjust_term_and_k_for_some_ints_case_gomory(lcm_den); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); - TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout); tout << " <= " << m_k << std::endl;); + TRACE("gomory_cut", tout<<"gomory cut:"; print_linear_combination_of_column_indices_only(m_t, tout); tout << " <= " << m_k << std::endl;); + TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); return lia_move::cut; } imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index dfe51711c..013f53ce0 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -113,17 +113,9 @@ private: bool has_low(unsigned j) const; bool has_upper(unsigned j) const; unsigned row_of_basic_column(unsigned j) const; - inline static bool is_rational(const impq & n) { - return is_zero(n.y); - } public: void display_column(std::ostream & out, unsigned j) const; - inline static - mpq fractional_part(const impq & n) { - lp_assert(is_rational(n)); - return n.x - floor(n.x); - } constraint_index column_upper_bound_constraint(unsigned j) const; constraint_index column_lower_bound_constraint(unsigned j) const; bool current_solution_is_inf_on_cut() const; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 09c3bd5b9..56a61177c 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1273,7 +1273,7 @@ std::ostream& lar_solver::print_term_as_indices(lar_term const& term, std::ostre if (!numeric_traits::is_zero(term.m_v)) { out << term.m_v << " + "; } - print_linear_combination_of_column_indices_only(term.coeffs_as_vector(), out); + print_linear_combination_of_column_indices_only(term, out); return out; } diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h index e776092a2..573fc319c 100644 --- a/src/util/lp/lp_utils.h +++ b/src/util/lp/lp_utils.h @@ -50,11 +50,34 @@ bool contains(const std::unordered_map & map, const A& key) { namespace lp { - - inline void throw_exception(std::string && str) { - throw default_exception(std::move(str)); +template +void print_linear_combination_of_column_indices_only(const T & coeffs, std::ostream & out) { + bool first = true; + for (const auto & it : coeffs) { + auto val = it.coeff(); + if (first) { + first = false; + } else { + if (val.is_pos()) { + out << " + "; + } else { + out << " - "; + val = -val; + } + } + if (val == 1) + out << " "; + else + out << T_to_string(val); + + out << "x" << it.var(); } - typedef z3_exception exception; +} + +inline void throw_exception(std::string && str) { + throw default_exception(std::move(str)); +} +typedef z3_exception exception; #define lp_assert(_x_) { SASSERT(_x_); } inline void lp_unreachable() { lp_assert(false); } From b940b7873bbac7b2420aa0cb6bcc04e0a79a8d3f Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 18 Sep 2018 13:47:18 -0700 Subject: [PATCH 02/41] work on Gomory cut Signed-off-by: Lev --- src/util/lp/gomory.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index f936397d4..e1e6fc0ea 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -190,12 +190,13 @@ class gomory::imp { void dump_row_coefficients(std::ostream & out) const { for (const auto& p : m_row) { - dump_coeff(out, p); + if (!column_is_fixed(p.var())) + dump_coeff(out, p); } } void dump_the_row(std::ostream& out) const { - out << "; the row\n"; + out << "; the row, excluding fixed vars\n"; out << "(assert ( = ( + "; dump_row_coefficients(out); out << ") 0))\n"; @@ -204,6 +205,7 @@ class gomory::imp { void dump_declarations(std::ostream& out) const { // for a column j the var name is vj for (const auto & p : m_row) { + if (column_is_fixed(p.var())) continue; out << "(declare-fun " << var_name(p.var()) << " () " << (is_int(p.var())? "Int" : "Real") << ")\n"; } @@ -217,8 +219,9 @@ class gomory::imp { } void dump_explanations(std::ostream& out) const { - for (const auto & p : m_row) { + for (const auto & p : m_row) { unsigned j = p.var(); + if (column_is_fixed(j)) continue; if (j == m_inf_col) { continue; } From 041458f97ae81d52884e4993c042b594c0297552 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 18 Sep 2018 14:42:32 -0700 Subject: [PATCH 03/41] fixes the +- bug in gomory cut Signed-off-by: Lev --- src/util/lp/gomory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index e1e6fc0ea..377c6125c 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -71,7 +71,7 @@ class gomory::imp { else { lp_assert(at_upper(j)); // the upper terms are inverted: therefore we have the minus - new_a = - (fj < f0? fj / f0 : (- one_minus_fj / one_minus_f0)); + new_a = fj < f0? (- fj / f0 ) : (one_minus_fj / one_minus_f0); m_k.addmul(new_a, upper_bound(j).x); m_ex.push_justification(column_upper_bound_constraint(j), new_a); } From b90d571d9a4c35cb38bcc91bea1f696e9ff25132 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 18 Sep 2018 15:36:01 -0700 Subject: [PATCH 04/41] fixing the build Signed-off-by: Lev Nachmanson --- src/test/lp/gomory_test.h | 5 +++-- src/util/lp/gomory.cpp | 11 +---------- src/util/lp/lp_settings.h | 8 ++++++++ 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 03ad5b187..501ad9e1a 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -1,4 +1,5 @@ namespace lp { +#include "util/lp/lp_utils.h" struct gomory_test { gomory_test( std::function name_function_p, @@ -88,7 +89,7 @@ struct gomory_test { lp_assert(is_int(x_j)); lp_assert(!a.is_int()); lp_assert(f_0 > zero_of_type() && f_0 < one_of_type()); - mpq f_j = int_solver::fractional_part(a); + mpq f_j = fractional_part(a); TRACE("gomory_cut_detail", tout << a << " x_j = " << x_j << ", k = " << k << "\n"; tout << "f_j: " << f_j << "\n"; @@ -206,7 +207,7 @@ struct gomory_test { unsigned x_j; mpq a; bool some_int_columns = false; - mpq f_0 = int_solver::fractional_part(get_value(inf_col)); + mpq f_0 = fractional_part(get_value(inf_col)); mpq one_min_f_0 = 1 - f_0; for ( auto pp : row) { a = pp.first; diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 377c6125c..f0bbd2348 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -20,19 +20,10 @@ #include "util/lp/gomory.h" #include "util/lp/int_solver.h" #include "util/lp/lar_solver.h" +#include "util/lp/lp_utils.h" namespace lp { class gomory::imp { - inline static bool is_rational(const impq & n) { return is_zero(n.y); } - - inline static mpq fractional_part(const impq & n) { - lp_assert(is_rational(n)); - return n.x - floor(n.x); - } - inline static mpq fractional_part(const mpq & n) { - return n - floor(n); - } - lar_term & m_t; // the term to return in the cut mpq & m_k; // the right side of the cut explanation& m_ex; // the conflict explanation diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 71be7258a..1bbefd154 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -433,7 +433,15 @@ inline void ensure_increasing(vector & v) { } } +inline static bool is_rational(const impq & n) { return is_zero(n.y); } +inline static mpq fractional_part(const impq & n) { + lp_assert(is_rational(n)); + return n.x - floor(n.x); +} +inline static mpq fractional_part(const mpq & n) { + return n - floor(n); +} #if Z3DEBUG bool D(); From ed19af4c4e7fc2d4387650c7c0087ccbfa5a7d63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Sep 2018 09:02:37 -0700 Subject: [PATCH 05/41] merge Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 1 + src/util/lp/gomory.cpp | 4 +++- src/util/lp/lp_core_solver_base.h | 6 +++--- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index fd2dc0da2..f096d1dd5 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1629,6 +1629,7 @@ public: expr_ref term2expr(lp::lar_term const& term) { expr_ref t(m); expr_ref_vector ts(m); + ts.push_back(a.mk_numeral(term.m_v, true)); for (auto const& p : term) { lp::var_index wi = p.var(); if (m_solver->is_term(wi)) { diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 55098dccf..9974eda7f 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -168,11 +168,13 @@ public: mpq one_min_f0 = 1 - f0; for (const auto & p : m_row) { unsigned j = p.var(); +#if 1 if (column_is_fixed(j)) { m_ex.push_justification(column_lower_bound_constraint(j)); m_ex.push_justification(column_upper_bound_constraint(j)); continue; } +#endif if (j == m_inf_col) { lp_assert(p.coeff() == one_of_type()); TRACE("gomory_cut_detail", tout << "seeing basic var";); @@ -194,7 +196,7 @@ public: adjust_term_and_k_for_some_ints_case_gomory(lcm_den); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); - TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout); tout << " <= " << m_k << std::endl;); + TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout) << " <= " << m_k << std::endl;); return lia_move::cut; } imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h index 41b6fe31d..9a6549917 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -577,7 +577,7 @@ public: } void print_column_info(unsigned j, std::ostream & out) const { - out << "j = " << j << ", name = "<< column_name(j); + out << "j = " << j << ",\tname = "<< column_name(j) << "\t"; switch (m_column_types[j]) { case column_type::fixed: case column_type::boxed: @@ -596,11 +596,11 @@ public: lp_assert(false); } // out << "basis heading = " << m_basis_heading[j] << std::endl; - out << " x = " << m_x[j]; + out << "\tx = " << m_x[j]; if (m_basis_heading[j] >= 0) out << " base\n"; else - out << " nbas\n"; + out << " \n"; } bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; } From a99ebed907e3a620a751a0d63b6ed7ce62e49dcd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 19 Sep 2018 10:17:27 -0700 Subject: [PATCH 06/41] keep the coefficients of 'at lower' variables positive, and the rest negative for Gomory cuts Signed-off-by: Lev Nachmanson --- src/util/lp/gomory.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index f0bbd2348..53e12c7ec 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -55,14 +55,14 @@ class gomory::imp { mpq new_a; mpq one_minus_fj = 1 - fj; if (at_lower(j)) { - new_a = fj < one_minus_f0? fj / one_minus_f0 : (- one_minus_fj / f0); + new_a = fj < one_minus_f0? fj / one_minus_f0 : one_minus_fj / f0; m_k.addmul(new_a, lower_bound(j).x); m_ex.push_justification(column_lower_bound_constraint(j), new_a); } else { lp_assert(at_upper(j)); // the upper terms are inverted: therefore we have the minus - new_a = fj < f0? (- fj / f0 ) : (one_minus_fj / one_minus_f0); + new_a = - (fj < f0? fj / f0 : one_minus_fj / one_minus_f0); m_k.addmul(new_a, upper_bound(j).x); m_ex.push_justification(column_upper_bound_constraint(j), new_a); } From dcda39e76e68fd2264e681c42fb3ae25e10e3ade Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Sep 2018 17:12:32 -0700 Subject: [PATCH 07/41] merge Signed-off-by: Nikolaj Bjorner --- src/util/lp/gomory.cpp | 15 ++++++++++++--- src/util/lp/lar_solver.h | 4 +--- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 2dd349354..2136f5f3e 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -197,12 +197,21 @@ class gomory::imp { out << "(assert ( = ( +"; dump_row_coefficients(out) << ") 0))\n"; } + + void dump_declaration(std::ostream& out, unsigned v) const { + out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n"; + } void dump_declarations(std::ostream& out) const { // for a column j the var name is vj for (const auto & p : m_row) { - out << "(declare-const " << var_name(p.var()) - << (is_int(p.var())? " Int" : " Real") << ")\n"; + dump_declaration(out, p.var()); + } + for (const auto& p : m_t) { + unsigned v = p.var(); + if (m_int_solver.m_lar_solver->is_term(v)) { + dump_declaration(out, v); + } } } @@ -298,7 +307,7 @@ public: lp_assert(m_int_solver.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); - // TBD: validate result of subs_term_columns + TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 3c0ed4fbf..9e9edacc8 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -239,8 +239,7 @@ public: void analyze_new_bounds_on_row_tableau( unsigned row_index, - bound_propagator & bp - ); + bound_propagator & bp); void substitute_basis_var_in_terms_for_row(unsigned i); @@ -549,7 +548,6 @@ public: mpq v = it->second; t.m_coeffs.erase(it); t.m_coeffs[p.second] = v; - if (lt.m_v.is_zero()) continue; rs -= v * lt.m_v; } } From d75b6fd9c1536b9c8f98392ad292be7859e0ce63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 11:06:05 -0700 Subject: [PATCH 08/41] remove offsets from terms Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 128 +++++++++++++++++++------------ src/util/lp/bound_propagator.cpp | 4 - src/util/lp/gomory.cpp | 16 ++-- src/util/lp/int_solver.cpp | 51 ++++++------ src/util/lp/int_solver.h | 16 ++-- src/util/lp/lar_constraints.h | 2 +- src/util/lp/lar_solver.cpp | 69 ++++++----------- src/util/lp/lar_solver.h | 14 ++-- src/util/lp/lar_term.h | 12 ++- 9 files changed, 159 insertions(+), 153 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f096d1dd5..ca59a2c27 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -55,7 +55,7 @@ std::ostream& operator<<(std::ostream& out, bound_kind const& k) { } class bound { - smt::bool_var m_bv; + smt::bool_var m_bv; smt::theory_var m_var; bool m_is_int; rational m_value; @@ -165,13 +165,13 @@ class theory_lra::imp { expr_ref_vector m_terms; vector m_coeffs; svector m_vars; - rational m_coeff; + rational m_offset; ptr_vector m_terms_to_internalize; internalize_state(ast_manager& m): m_terms(m) {} void reset() { m_terms.reset(); m_coeffs.reset(); - m_coeff.reset(); + m_offset.reset(); m_vars.reset(); m_terms_to_internalize.reset(); } @@ -197,7 +197,7 @@ class theory_lra::imp { expr_ref_vector& terms() { return m_st.m_terms; } vector& coeffs() { return m_st.m_coeffs; } svector& vars() { return m_st.m_vars; } - rational& coeff() { return m_st.m_coeff; } + rational& offset() { return m_st.m_offset; } ptr_vector& terms_to_internalize() { return m_st.m_terms_to_internalize; } void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); } void set_back(unsigned i) { @@ -216,6 +216,8 @@ class theory_lra::imp { svector m_term_index2theory_var; // reverse map from lp_solver variables to theory variables var_coeffs m_left_side; // constraint left side mutable std::unordered_map m_variable_values; // current model + lp::var_index m_one_var; + lp::var_index m_zero_var; enum constraint_source { inequality_source, @@ -331,6 +333,32 @@ class theory_lra::imp { } } + void add_const(int c, lp::var_index& var) { + if (var != UINT_MAX) { + return; + } + app_ref cnst(a.mk_int(c), m); + TRACE("arith", tout << "add " << cnst << "\n";); + enode* e = mk_enode(cnst); + theory_var v = mk_var(cnst); + var = m_solver->add_var(v, true); + m_theory_var2var_index.setx(v, var, UINT_MAX); + m_var_index2theory_var.setx(var, v, UINT_MAX); + m_var_trail.push_back(v); + add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c))); + add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c))); + } + + lp::var_index get_one() { + add_const(1, m_one_var); + return m_one_var; + } + + lp::var_index get_zero() { + add_const(0, m_zero_var); + return m_zero_var; + } + void found_not_handled(expr* n) { m_not_handled = n; @@ -375,7 +403,7 @@ class theory_lra::imp { expr_ref_vector & terms = st.terms(); svector& vars = st.vars(); vector& coeffs = st.coeffs(); - rational& coeff = st.coeff(); + rational& offset = st.offset(); rational r; expr* n1, *n2; unsigned index = 0; @@ -415,7 +443,7 @@ class theory_lra::imp { ++index; } else if (a.is_numeral(n, r)) { - coeff += coeffs[index]*r; + offset += coeffs[index]*r; ++index; } else if (a.is_uminus(n, n1)) { @@ -427,7 +455,6 @@ class theory_lra::imp { app* t = to_app(n); internalize_args(t); mk_enode(t); - theory_var v = mk_var(n); coeffs[vars.size()] = coeffs[index]; vars.push_back(v); @@ -738,7 +765,15 @@ class theory_lra::imp { } bool is_unit_var(scoped_internalize_state& st) { - return st.coeff().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one(); + return st.offset().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one(); + } + + bool is_one(scoped_internalize_state& st) { + return st.offset().is_one() && st.vars().empty(); + } + + bool is_zero(scoped_internalize_state& st) { + return st.offset().is_zero() && st.vars().empty(); } theory_var internalize_def(app* term, scoped_internalize_state& st) { @@ -771,13 +806,24 @@ class theory_lra::imp { if (is_unit_var(st)) { return st.vars()[0]; } + else if (is_one(st)) { + return get_one(); + } + else if (is_zero(st)) { + return get_zero(); + } else { init_left_side(st); theory_var v = mk_var(term); lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX); - TRACE("arith", tout << mk_pp(term, m) << " " << v << " " << vi << "\n";); + TRACE("arith", tout << mk_pp(term, m) << " v" << v << "\n";); if (vi == UINT_MAX) { - vi = m_solver->add_term(m_left_side, st.coeff()); + rational const& offset = st.offset(); + if (!offset.is_zero()) { + m_left_side.push_back(std::make_pair(offset, get_one())); + } + SASSERT(!m_left_side.empty()); + vi = m_solver->add_term(m_left_side); m_theory_var2var_index.setx(v, vi, UINT_MAX); if (m_solver->is_term(vi)) { m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX); @@ -806,6 +852,8 @@ public: m_has_int(false), m_arith_eq_adapter(th, ap, a), m_internalize_head(0), + m_one_var(UINT_MAX), + m_zero_var(UINT_MAX), m_not_handled(nullptr), m_asserted_qhead(0), m_assume_eq_head(0), @@ -879,7 +927,7 @@ public: } void internalize_eq_eh(app * atom, bool_var) { - expr* lhs = 0, *rhs = 0; + expr* lhs = nullptr, *rhs = nullptr; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); @@ -1197,7 +1245,6 @@ public: m_todo_terms.pop_back(); if (m_solver->is_term(vi)) { const lp::lar_term& term = m_solver->get_term(vi); - result += term.m_v * coeff; for (const auto & i: term) { m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff())); } @@ -1234,7 +1281,6 @@ public: m_todo_terms.pop_back(); if (m_solver->is_term(wi)) { const lp::lar_term& term = m_solver->get_term(wi); - result += term.m_v * coeff; for (const auto & i : term) { if (m_variable_values.count(i.var()) > 0) { result += m_variable_values[i.var()] * coeff * i.coeff(); @@ -1481,8 +1527,8 @@ public: bool all_bounded = true; for (unsigned v = 0; v < nv; ++v) { lp::var_index vi = m_theory_var2var_index[v]; - if (vi == UINT_MAX) - continue; + if (vi == UINT_MAX) + continue; if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { lp::lar_term term; term.add_monomial(rational::one(), vi); @@ -1516,23 +1562,10 @@ public: theory_var v = mk_var(n); theory_var v1 = mk_var(p); theory_var v2 = mk_var(q); - rational r = get_value(v); rational r1 = get_value(v1); - rational r2 = get_value(v2); - rational r3; - if (r2.is_zero()) { - continue; - } - if (r1.is_int() && r2.is_int() && r == div(r1, r2)) { - continue; - } - if (r2.is_neg() || r1.is_neg()) { - // TBD - continue; - } + rational r2; - if (!r1.is_int() || !r2.is_int()) { - // std::cout << r1 << " " << r2 << " " << r << " " << expr_ref(n, m) << "\n"; + if (!r1.is_int() || r1.is_neg()) { // TBD // r1 = 223/4, r2 = 2, r = 219/8 // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0 @@ -1542,16 +1575,18 @@ public: continue; } - if (a.is_numeral(q, r3)) { + if (a.is_numeral(q, r2) && r2.is_pos()) { + if (get_value(v) == div(r1, r2)) continue; - SASSERT(r3 == r2 && r2.is_int()); - SASSERT(r1.is_int() && r3.is_int()); rational div_r = div(r1, r2); // p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2) // p >= q * div(r1, q) => div(r1, q) <= div(p, q) rational mul(1); rational hi = r2 * div_r + r2 - 1; rational lo = r2 * div_r; + + // used to normalize inequalities so they + // don't appear as 8*x >= 15, but x >= 2 expr *n1 = nullptr, *n2 = nullptr; if (a.is_mul(p, n1, n2) && is_numeral(n1, mul) && mul.is_pos()) { p = n2; @@ -1568,7 +1603,7 @@ public: all_divs_valid = false; TRACE("arith", - tout << r1 << " div " << r2 << " = " << r3 << "\n"; + tout << r1 << " div " << r2 << "\n"; literal_vector lits; lits.push_back(~p_le_r1); lits.push_back(n_le_div); @@ -1578,8 +1613,10 @@ public: ctx().display_literals_verbose(tout, lits) << "\n";); continue; } +#if 0 - + // TBD similar for non-linear division. + // better to deal with in nla_solver: all_divs_valid = false; @@ -1610,6 +1647,7 @@ public: lits[0] = pq_rhs; lits[1] = n_ge_div; ctx().display_literals_verbose(tout, lits) << "\n";); +#endif } return all_divs_valid; @@ -1629,7 +1667,6 @@ public: expr_ref term2expr(lp::lar_term const& term) { expr_ref t(m); expr_ref_vector ts(m); - ts.push_back(a.mk_numeral(term.m_v, true)); for (auto const& p : term) { lp::var_index wi = p.var(); if (m_solver->is_term(wi)) { @@ -1709,17 +1746,13 @@ public: TRACE("arith", tout << "idiv bounds check\n";); return l_false; } - lp::lar_term term; - lp::mpq k; - lp::explanation ex; // TBD, this should be streamlined accross different explanations - bool upper; m_explanation.reset(); - switch(m_lia->check(term, k, ex, upper)) { + switch (m_lia->check()) { case lp::lia_move::sat: return l_true; case lp::lia_move::branch: { TRACE("arith", tout << "branch\n";); - app_ref b = mk_bound(term, k, !upper); + app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";); // branch on term >= k + 1 // branch on term <= k @@ -1732,13 +1765,13 @@ public: TRACE("arith", tout << "cut\n";); ++m_stats.m_gomory_cuts; // m_explanation implies term <= k - app_ref b = mk_bound(term, k, !upper); + app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n"); - TRACE("arith", dump_cut_lemma(tout, term, k, ex, upper);); + TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper());); m_eqs.reset(); m_core.reset(); m_params.reset(); - for (auto const& ev : ex.m_explanation) { + for (auto const& ev : m_lia->get_explanation().m_explanation) { if (!ev.first.is_zero()) { set_evidence(ev.second); } @@ -1753,7 +1786,7 @@ public: case lp::lia_move::conflict: TRACE("arith", tout << "conflict\n";); // ex contains unsat core - m_explanation = ex.m_explanation; + m_explanation = m_lia->get_explanation().m_explanation; set_conflict1(); return l_false; case lp::lia_move::undef: @@ -2922,7 +2955,7 @@ public: lp::lar_term const& term = m_solver->get_term(vi); TRACE("arith", m_solver->print_term(term, tout) << "\n";); scoped_anum r1(m_nra->am()); - rational c1 = term.m_v * wcoeff; + rational c1(0); m_nra->am().set(r1, c1.to_mpq()); m_nra->am().add(r, r1, r); for (auto const & arg : term) { @@ -3197,7 +3230,6 @@ public: coeffs.find(w, c0); coeffs.insert(w, c0 + ti.coeff() * coeff); } - offset += coeff * term.m_v; } app_ref coeffs2app(u_map const& coeffs, rational const& offset, bool is_int) { diff --git a/src/util/lp/bound_propagator.cpp b/src/util/lp/bound_propagator.cpp index c4fa2aefa..a5c7c976a 100644 --- a/src/util/lp/bound_propagator.cpp +++ b/src/util/lp/bound_propagator.cpp @@ -17,10 +17,6 @@ const impq & bound_propagator::get_upper_bound(unsigned j) const { } void bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { j = m_lar_solver.adjust_column_index_to_term_index(j); - if (m_lar_solver.is_term(j)) { - // lp treats terms as not having a free coefficient, restoring it below for the outside consumption - v += m_lar_solver.get_term(j).m_v; - } lconstraint_kind kind = is_low? GE : LE; if (strict) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 2136f5f3e..96b3ab395 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -45,7 +45,7 @@ class gomory::imp { void int_case_in_gomory_cut(const mpq & a, unsigned j, mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) { lp_assert(is_int(j) && !a.is_int()); - mpq fj = fractional_part(a); + mpq fj = fractional_part(a); TRACE("gomory_cut_detail", tout << a << " j=" << j << " k = " << m_k; tout << ", fj: " << fj << ", "; @@ -56,10 +56,9 @@ class gomory::imp { mpq new_a; if (at_lower(j)) { new_a = fj <= one_minus_f0 ? fj / one_minus_f0 : ((1 - fj) / f0); - m_k.addmul(new_a, lower_bound(j).x); - // m_k += (new_a * lower_bound(j).x); lp_assert(new_a.is_pos()); - m_ex.push_justification(column_lower_bound_constraint(j), new_a); + m_k.addmul(new_a, lower_bound(j).x); + m_ex.push_justification(column_lower_bound_constraint(j), new_a); } else { lp_assert(at_upper(j)); @@ -67,7 +66,6 @@ class gomory::imp { new_a = - (fj <= f0 ? fj / f0 : ((1 - fj) / one_minus_f0)); lp_assert(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); - // m_k += (new_a * upper_bound(j).x); m_ex.push_justification(column_upper_bound_constraint(j), new_a); } m_t.add_monomial(new_a, j); @@ -251,9 +249,12 @@ class gomory::imp { std::ostream& dump_term_le_k(std::ostream & out) const { return dump_term_sum(out << "(<= ") << " " << m_k << ")"; } + void dump_the_cut_assert(std::ostream & out) const { dump_term_le_k(out << "(assert (not ") << "))\n"; } + + void dump_cut_and_constraints_as_smt_lemma(std::ostream& out) const { dump_declarations(out); dump_the_row(out); @@ -284,7 +285,6 @@ public: mpq one_min_f0 = 1 - f0; for (const auto & p : m_row) { unsigned j = p.var(); - if (j == m_inf_col) { lp_assert(p.coeff() == one_of_type()); TRACE("gomory_cut_detail", tout << "seeing basic var";); @@ -306,11 +306,11 @@ public: adjust_term_and_k_for_some_ints_case_gomory(lcm_den); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); - m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); - TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); + m_int_solver.m_lar_solver->subs_term_columns(m_t); TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } + imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : m_t(t), m_k(k), diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index cd3a88669..83fbe3961 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -125,19 +125,19 @@ constraint_index int_solver::column_lower_bound_constraint(unsigned j) const { bool int_solver::current_solution_is_inf_on_cut() const { const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x; - impq v = m_t->apply(x); - mpq sign = *m_upper ? one_of_type() : -one_of_type(); - CTRACE("current_solution_is_inf_on_cut", v * sign <= (*m_k) * sign, - tout << "m_upper = " << *m_upper << std::endl; - tout << "v = " << v << ", k = " << (*m_k) << std::endl; + impq v = m_t.apply(x); + mpq sign = m_upper ? one_of_type() : -one_of_type(); + CTRACE("current_solution_is_inf_on_cut", v * sign <= m_k * sign, + tout << "m_upper = " << m_upper << std::endl; + tout << "v = " << v << ", k = " << m_k << std::endl; ); - return v * sign > (*m_k) * sign; + return v * sign > m_k * sign; } lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip & row) { lp_assert(column_is_int_inf(inf_col)); - gomory gc(*m_t, *m_k, *m_ex, inf_col, row, *this); + gomory gc(m_t, m_k, m_ex, inf_col, row, *this); return gc.create_cut(); } @@ -147,7 +147,7 @@ lia_move int_solver::proceed_with_gomory_cut(unsigned j) { if (!is_gomory_cut_target(row)) return create_branch_on_column(j); - *m_upper = true; + m_upper = true; return mk_gomory_cut(j, row); } @@ -373,21 +373,21 @@ lia_move int_solver::make_hnf_cut() { #else vector x0; #endif - lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0); + lia_move r = m_hnf_cutter.create_cut(m_t, m_k, m_ex, m_upper, x0); if (r == lia_move::cut) { TRACE("hnf_cut", - m_lar_solver->print_term(*m_t, tout << "cut:"); - tout << " <= " << *m_k << std::endl; + m_lar_solver->print_term(m_t, tout << "cut:"); + tout << " <= " << m_k << std::endl; for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { m_lar_solver->print_constraint(i, tout); } ); lp_assert(current_solution_is_inf_on_cut()); settings().st().m_hnf_cuts++; - m_ex->clear(); + m_ex.clear(); for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { - m_ex->push_justification(i); + m_ex.push_justification(i); } } return r; @@ -403,10 +403,13 @@ lia_move int_solver::hnf_cut() { return lia_move::undef; } -lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) { +lia_move int_solver::check() { if (!has_inf_int()) return lia_move::sat; - m_t = &t; m_k = &k; m_ex = &ex; m_upper = &upper; + m_t.clear(); + m_k.reset(); + m_ex.clear(); + m_upper = false; lia_move r = run_gcd_test(); if (r != lia_move::undef) return r; @@ -646,8 +649,8 @@ bool int_solver::gcd_test_for_row(static_matrix> & A, uns void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) { constraint_index lc, uc; m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc); - m_ex->m_explanation.push_back(std::make_pair(mpq(1), lc)); - m_ex->m_explanation.push_back(std::make_pair(mpq(1), uc)); + m_ex.m_explanation.push_back(std::make_pair(mpq(1), lc)); + m_ex.m_explanation.push_back(std::make_pair(mpq(1), uc)); } void int_solver::fill_explanation_from_fixed_columns(const row_strip & row) { for (const auto & c : row) { @@ -1042,20 +1045,20 @@ const impq& int_solver::lower_bound(unsigned j) const { lia_move int_solver::create_branch_on_column(int j) { TRACE("check_main_int", tout << "branching" << std::endl;); - lp_assert(m_t->is_empty()); + lp_assert(m_t.is_empty()); lp_assert(j != -1); - m_t->add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j)); + m_t.add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j)); if (is_free(j)) { - *m_upper = true; - *m_k = mpq(0); + m_upper = true; + m_k = mpq(0); } else { - *m_upper = left_branch_is_more_narrow_than_right(j); - *m_k = *m_upper? floor(get_value(j)) : ceil(get_value(j)); + m_upper = left_branch_is_more_narrow_than_right(j); + m_k = m_upper? floor(get_value(j)) : ceil(get_value(j)); } TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n"; display_column(tout, j); - tout << "k = " << *m_k << std::endl; + tout << "k = " << m_k << std::endl; ); return lia_move::branch; diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index 013f53ce0..17ce20481 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -39,19 +39,23 @@ public: // fields lar_solver *m_lar_solver; 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 - explanation *m_ex; // the conflict explanation - bool *m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise + lar_term m_t; // the term to return in the cut + mpq m_k; // the right side of the cut + explanation m_ex; // the conflict explanation + bool m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise hnf_cutter m_hnf_cutter; // methods int_solver(lar_solver* lp); // main function to check that the solution provided by lar_solver is valid for integral values, // or provide a way of how it can be adjusted. - lia_move check(lar_term& t, mpq& k, explanation& ex, bool & upper); + lia_move check(); + lar_term const& get_term() const { return m_t; } + mpq const& get_offset() const { return m_k; } + explanation const& get_explanation() const { return m_ex; } + bool is_upper() const { return m_upper; } + bool move_non_basic_column_to_bounds(unsigned j); - lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex); bool is_base(unsigned j) const; bool is_real(unsigned j) const; const impq & lower_bound(unsigned j) const; diff --git a/src/util/lp/lar_constraints.h b/src/util/lp/lar_constraints.h index ac15028bb..6305089b4 100644 --- a/src/util/lp/lar_constraints.h +++ b/src/util/lp/lar_constraints.h @@ -75,7 +75,7 @@ struct lar_term_constraint: public lar_base_constraint { } unsigned size() const override { return m_term->size();} lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { } - mpq get_free_coeff_of_left_side() const override { return m_term->m_v;} + // mpq get_free_coeff_of_left_side() const override { return m_term->m_v;} }; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 56a61177c..30494aa1c 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -137,7 +137,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, kind = static_cast(-kind); } rs_of_evidence /= ratio; - rs_of_evidence += t->m_v * ratio; + // rs_of_evidence += t->m_v * ratio; } return kind == be.kind() && rs_of_evidence == be.m_bound; @@ -602,7 +602,7 @@ void lar_solver::register_monoid_in_map(std::unordered_map & coe void lar_solver::substitute_terms_in_linear_expression(const vector>& left_side_with_terms, - vector> &left_side, mpq & free_coeff) const { + vector> &left_side) const { std::unordered_map coeffs; for (auto & t : left_side_with_terms) { unsigned j = t.second; @@ -613,7 +613,6 @@ void lar_solver::substitute_terms_in_linear_expression(const vector= constr.m_right_side; - case GT: return left_side_val > constr.m_right_side; + case GT: return left_side_val > constr.m_right_side; case EQ: return left_side_val == constr.m_right_side; default: lp_unreachable(); @@ -976,8 +975,10 @@ bool lar_solver::the_relations_are_of_same_type(const vectorm_kind); if (kind == GT || kind == LT) strict = true; - if (kind == GE || kind == GT) n_of_G++; - else if (kind == LE || kind == LT) n_of_L++; + if (kind == GE || kind == GT) + n_of_G++; + else if (kind == LE || kind == LT) + n_of_L++; } the_kind_of_sum = n_of_G ? GE : (n_of_L ? LE : EQ); if (strict) @@ -1117,7 +1118,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value bool lar_solver::has_value(var_index var, mpq& value) const { if (is_term(var)) { lar_term const& t = get_term(var); - value = t.m_v; + value = 0; for (auto const& cv : t) { impq const& r = get_column_value(cv.var()); if (!numeric_traits::is_zero(r.y)) return false; @@ -1229,8 +1230,7 @@ std::ostream& lar_solver::print_constraints(std::ostream& out) const { std::ostream& lar_solver::print_terms(std::ostream& out) const { for (auto it : m_terms) { - print_term(*it, out); - out << "\n"; + print_term(*it, out) << "\n"; } return out; } @@ -1244,9 +1244,6 @@ std::ostream& lar_solver::print_left_side_of_constraint(const lar_base_constrain } std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) const { - if (!numeric_traits::is_zero(term.m_v)) { - out << term.m_v << " + "; - } bool first = true; for (const auto p : term) { mpq val = p.coeff(); @@ -1270,9 +1267,6 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c } std::ostream& lar_solver::print_term_as_indices(lar_term const& term, std::ostream & out) const { - if (!numeric_traits::is_zero(term.m_v)) { - out << term.m_v << " + "; - } print_linear_combination_of_column_indices_only(term, out); return out; } @@ -1497,7 +1491,7 @@ bool lar_solver::term_is_int(const lar_term * t) const { for (auto const & p : t->m_coeffs) if (! (column_is_int(p.first) && p.second.is_int())) return false; - return t->m_v.is_int(); + return true; } bool lar_solver::var_is_int(var_index v) const { @@ -1598,17 +1592,13 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) { } -var_index lar_solver::add_term_undecided(const vector> & coeffs, - const mpq &m_v) { - push_and_register_term(new lar_term(coeffs, m_v)); +var_index lar_solver::add_term_undecided(const vector> & coeffs) { + push_and_register_term(new lar_term(coeffs)); return m_terms_start_index + m_terms.size() - 1; } #if Z3DEBUG_CHECK_UNIQUE_TERMS -bool lar_solver::term_coeffs_are_ok(const vector> & coeffs, const mpq& v) { - if (coeffs.empty()) { - return is_zero(v); - } +bool lar_solver::term_coeffs_are_ok(const vector> & coeffs) { for (const auto & p : coeffs) { if (column_is_real(p.second)) @@ -1643,12 +1633,11 @@ void lar_solver::push_and_register_term(lar_term* t) { } // terms -var_index lar_solver::add_term(const vector> & coeffs, - const mpq &m_v) { +var_index lar_solver::add_term(const vector> & coeffs) { if (strategy_is_undecided()) - return add_term_undecided(coeffs, m_v); + return add_term_undecided(coeffs); - push_and_register_term(new lar_term(coeffs, m_v)); + push_and_register_term(new lar_term(coeffs)); unsigned adjusted_term_index = m_terms.size() - 1; var_index ret = m_terms_start_index + adjusted_term_index; if (use_tableau() && !coeffs.empty()) { @@ -1656,13 +1645,12 @@ var_index lar_solver::add_term(const vector> & coeffs, if (m_settings.bound_propagation()) m_rows_with_changed_bounds.insert(A_r().row_count() - 1); } - CTRACE("add_term_lar_solver", !m_v.is_zero(), print_term(*m_terms.back(), tout);); lp_assert(m_var_register.size() == A_r().column_count()); return ret; } void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) { - TRACE("dump_terms", print_term(*term, tout); tout << std::endl;); + TRACE("dump_terms", print_term(*term, tout) << std::endl;); register_new_ext_var_index(term_ext_index, term_is_int(term)); // j will be a new variable unsigned j = A_r().column_count(); @@ -1744,9 +1732,8 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); unsigned term_j; if (m_var_register.external_is_used(j, term_j)) { - mpq rs = right_side - m_terms[adjusted_term_index]->m_v; m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side)); - update_column_type_and_bound(term_j, kind, rs, ci); + update_column_type_and_bound(term_j, kind, right_side, ci); } else { add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side); @@ -1755,11 +1742,10 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k constraint_index lar_solver::add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) { vector> left_side; - mpq rs = -right_side_parm; - substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs); - unsigned term_index = add_term(left_side, zero_of_type()); + substitute_terms_in_linear_expression(left_side_with_terms, left_side); + unsigned term_index = add_term(left_side); constraint_index ci = m_constraints.size(); - add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci); + add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci); return ci; } @@ -1768,7 +1754,7 @@ void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned ter add_row_from_term_no_constraint(term, term_j); unsigned j = A_r().column_count() - 1; - update_column_type_and_bound(j, kind, right_side - term->m_v, m_constraints.size()); + update_column_type_and_bound(j, kind, right_side, m_constraints.size()); m_constraints.push_back(new lar_term_constraint(term, kind, right_side)); lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); } @@ -2266,15 +2252,6 @@ void lar_solver::set_cut_strategy(unsigned cut_frequency) { } } -void lar_solver::adjust_cut_for_terms(const lar_term& t, mpq & rs) { - for (const auto& p : t) { - if (!is_term(p.var())) continue; - const lar_term & p_term = get_term(p.var()); - if (p_term.m_v.is_zero()) continue; - rs -= p.coeff() * p_term.m_v; - } -} - } // namespace lp diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 9e9edacc8..f3aa4f23b 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -164,13 +164,11 @@ public: // terms - var_index add_term(const vector> & coeffs, - const mpq &m_v); + var_index add_term(const vector> & coeffs); - var_index add_term_undecided(const vector> & coeffs, - const mpq &m_v); + var_index add_term_undecided(const vector> & coeffs); - bool term_coeffs_are_ok(const vector> & coeffs, const mpq& v); + bool term_coeffs_are_ok(const vector> & coeffs); void push_and_register_term(lar_term* t); void add_row_for_term(const lar_term * term, unsigned term_ext_index); @@ -331,7 +329,7 @@ public: void substitute_terms_in_linear_expression( const vector>& left_side_with_terms, - vector> &left_side, mpq & free_coeff) const; + vector> &left_side) const; void detect_rows_of_bound_change_column_for_nbasic_column(unsigned j); @@ -534,7 +532,7 @@ public: return m_columns_to_ul_pairs()[j].lower_bound_witness(); } - void subs_term_columns(lar_term& t, mpq & rs) { + void subs_term_columns(lar_term& t) { vector> columns_to_subs; for (const auto & m : t.m_coeffs) { unsigned tj = adjust_column_index_to_term_index(m.first); @@ -548,7 +546,6 @@ public: mpq v = it->second; t.m_coeffs.erase(it); t.m_coeffs[p.second] = v; - rs -= v * lt.m_v; } } @@ -585,6 +582,5 @@ public: lar_term get_term_to_maximize(unsigned ext_j) const; void set_cut_strategy(unsigned cut_frequency); bool sum_first_coords(const lar_term& t, mpq & val) const; - void adjust_cut_for_terms(const lar_term& t, mpq & rs); }; } diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 519847848..e9259b8c0 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -21,9 +21,9 @@ #include "util/lp/indexed_vector.h" namespace lp { struct lar_term { - // the term evaluates to sum of m_coeffs + m_v + // the term evaluates to sum of m_coeffs std::unordered_map m_coeffs; - mpq m_v; + // mpq m_v; lar_term() {} void add_monomial(const mpq& c, unsigned j) { auto it = m_coeffs.find(j); @@ -37,7 +37,7 @@ struct lar_term { } bool is_empty() const { - return m_coeffs.size() == 0 && is_zero(m_v); + return m_coeffs.size() == 0; // && is_zero(m_v); } unsigned size() const { return static_cast(m_coeffs.size()); } @@ -46,8 +46,7 @@ struct lar_term { return m_coeffs; } - lar_term(const vector>& coeffs, - const mpq & v) : m_v(v) { + lar_term(const vector>& coeffs) { for (const auto & p : coeffs) { add_monomial(p.first, p.second); } @@ -87,7 +86,7 @@ struct lar_term { template T apply(const vector& x) const { - T ret = T(m_v); + T ret(0); for (const auto & t : m_coeffs) { ret += t.second * x[t.first]; } @@ -96,7 +95,6 @@ struct lar_term { void clear() { m_coeffs.clear(); - m_v = zero_of_type(); } struct ival { From 91dbcbc36f1fe3ba51d6804e774ee70dd7b880cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 18:57:47 -0700 Subject: [PATCH 09/41] fix test build Signed-off-by: Nikolaj Bjorner --- src/test/lp/gomory_test.h | 1 - src/test/lp/lp.cpp | 20 +++++++++++++------- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 501ad9e1a..972466dc3 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -185,7 +185,6 @@ struct gomory_test { } void print_term(lar_term & t, std::ostream & out) { - lp_assert(is_zero(t.m_v)); vector> row; for (auto p : t.m_coeffs) row.push_back(std::make_pair(p.second, p.first)); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 6e418fe68..ff9de0e58 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -2667,13 +2667,20 @@ void test_term() { lar_solver solver; unsigned _x = 0; unsigned _y = 1; + unsigned _one = 2; var_index x = solver.add_var(_x, false); var_index y = solver.add_var(_y, false); + var_index one = solver.add_var(_one, false); + + vector> term_one; + term_one.push_back(std::make_pair((int)1, one)); + solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0)); vector> term_ls; term_ls.push_back(std::pair((int)1, x)); term_ls.push_back(std::pair((int)1, y)); - var_index z = solver.add_term(term_ls, mpq(3)); + term_ls.push_back(std::make_pair((int)3, one)); + var_index z = solver.add_term(term_ls); vector> ls; ls.push_back(std::pair((int)1, x)); @@ -2743,10 +2750,10 @@ void test_bound_propagation_one_small_sample1() { vector> coeffs; coeffs.push_back(std::pair(1, a)); coeffs.push_back(std::pair(-1, c)); - ls.add_term(coeffs, zero_of_type()); + ls.add_term(coeffs); coeffs.pop_back(); coeffs.push_back(std::pair(-1, b)); - ls.add_term(coeffs, zero_of_type()); + ls.add_term(coeffs); coeffs.clear(); coeffs.push_back(std::pair(1, a)); coeffs.push_back(std::pair(-1, b)); @@ -3485,12 +3492,12 @@ void test_maximize_term() { vector> term_ls; term_ls.push_back(std::pair((int)1, x)); term_ls.push_back(std::pair((int)-1, y)); - unsigned term_x_min_y = solver.add_term(term_ls, mpq(0)); + unsigned term_x_min_y = solver.add_term(term_ls); term_ls.clear(); term_ls.push_back(std::pair((int)2, x)); term_ls.push_back(std::pair((int)2, y)); - unsigned term_2x_pl_2y = solver.add_term(term_ls, mpq(0)); + unsigned term_2x_pl_2y = solver.add_term(term_ls); solver.add_var_bound(term_x_min_y, LE, zero_of_type()); solver.add_var_bound(term_2x_pl_2y, LE, mpq((int)5)); solver.find_feasible_solution(); @@ -3502,8 +3509,7 @@ void test_maximize_term() { std::cout<< "v[" << p.first << "] = " << p.second << std::endl; } std::cout << "calling int_solver\n"; - lar_term t; mpq k; explanation ex; bool upper; - lia_move lm = i_solver.check(t, k, ex, upper); + lia_move lm = i_solver.check(); VERIFY(lm == lia_move::sat); impq term_max; lp_status st = solver.maximize_term(term_2x_pl_2y, term_max); From 382bce4bb79c4823af0605bd94c7cc824c641b4d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 19:19:40 -0700 Subject: [PATCH 10/41] fix #1836 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 25b437bc4..d7d8aeddc 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1816,7 +1816,7 @@ struct let get_model x = let q = Z3native.solver_get_model (gc x) x in - if Z3native.is_null_model q then None else Some q + try if Z3native.is_null_model q then None else Some q with | _ -> None let get_proof x = let q = Z3native.solver_get_proof (gc x) x in From d6a1d17d695648e6e6b713323122a55a26283184 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 20 Sep 2018 16:28:45 -0700 Subject: [PATCH 11/41] extend(src/api/c++/z3++.h): support units() for solver class --- src/api/c++/z3++.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e1f263e17..a65d6e4d8 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2038,6 +2038,7 @@ namespace z3 { stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); } expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } + expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, solver const & s); From 39ed27101ed9f465504f4e12e2bd2f676ea66fda Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 19:56:55 -0700 Subject: [PATCH 12/41] include version.h in install include directory for cmake build #1833 Signed-off-by: Nikolaj Bjorner --- src/CMakeLists.txt | 2 ++ src/util/CMakeLists.txt | 1 + 2 files changed, 3 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 826f87e8c..c2d7d84a3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -166,6 +166,8 @@ foreach (header ${libz3_public_headers}) set_property(TARGET libz3 APPEND PROPERTY PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}") endforeach() +set_property(TARGET libz3 APPEND PROPERTY + PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/version.h") install(TARGETS libz3 EXPORT Z3_EXPORTED_TARGETS diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 85b6f955c..a84cc1f00 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -7,6 +7,7 @@ endif() set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"") configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h) + z3_add_component(util SOURCES approx_nat.cpp From c59a957737bdb04319df105cdd61130b228f23c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Sep 2018 20:37:14 -0700 Subject: [PATCH 13/41] add non-units method Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 15 +++++++++++++++ src/api/c++/z3++.h | 1 + src/api/z3_api.h | 8 ++++++++ src/solver/solver.cpp | 29 +++++++++++++++++++++++++++++ src/solver/solver.h | 2 ++ 5 files changed, 55 insertions(+) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index fc42acbb9..5a4537a4a 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -372,6 +372,21 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s) { + Z3_TRY; + LOG_Z3_solver_get_non_units(c, s); + RESET_ERROR_CODE(); + init_solver(c, s); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + expr_ref_vector fmls = to_solver_ref(s)->get_non_units(mk_c(c)->m()); + for (expr* f : fmls) { + v->m_ast_vector.push_back(f); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) { for (unsigned i = 0; i < num_assumptions; i++) { if (!is_expr(to_ast(assumptions[i]))) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e1f263e17..378819682 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2038,6 +2038,7 @@ namespace z3 { stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); } expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } + expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, solver const & s); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2657e558d..03bce5d5e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6121,6 +6121,14 @@ extern "C" { */ Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s); + + /** + \brief Return the set of non units in the solver state. + + def_API('Z3_solver_get_non_units', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) + */ + Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s); + /** \brief Check whether the assertions in a given solver are consistent or not. diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 4044c4a85..149fe0d65 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -256,3 +256,32 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } + +expr_ref_vector solver::get_non_units(ast_manager& m) { + expr_ref_vector result(m), fmls(m); + get_assertions(fmls); + family_id bfid = m.get_basic_family_id(); + expr_mark marked; + for (unsigned i = 0; i < fmls.size(); ++i) { + expr* f = fmls.get(i); + if (marked.is_marked(f)) continue; + marked.mark(f); + if (!is_app(f)) { + result.push_back(f); + continue; + } + app* _f = to_app(f); + if (_f->get_family_id() == bfid) { + if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { + fmls.append(_f->get_num_args(), _f->get_args()); + } + else if (m.is_eq(f) || m.is_distinct(f)) { + result.push_back(f); + } + } + else { + result.push_back(f); + } + } + return result; +} diff --git a/src/solver/solver.h b/src/solver/solver.h index c371be284..5329161cd 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -236,6 +236,8 @@ public: */ expr_ref_vector get_units(ast_manager& m); + expr_ref_vector get_non_units(ast_manager& m); + class scoped_push { solver& s; bool m_nopop; From 0b7918c52eaadee049e28056b134e4621035d85f Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 21 Sep 2018 09:37:36 +0100 Subject: [PATCH 14/41] remove spurious pragma --- src/smt/smt_arith_value.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp index ce4c0d9a9..41679851a 100644 --- a/src/smt/smt_arith_value.cpp +++ b/src/smt/smt_arith_value.cpp @@ -1,4 +1,3 @@ - /*++ Copyright (c) 2018 Microsoft Corporation @@ -17,7 +16,6 @@ Author: Revision History: --*/ -#pragma once; #include "smt/smt_arith_value.h" #include "smt/theory_lra.h" From 0c4754d94bdfaf07077120f5cbff780d8fb0971d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 20:13:58 -0700 Subject: [PATCH 15/41] rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833 Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- scripts/mk_util.py | 4 ++-- src/CMakeLists.txt | 2 +- src/shell/main.cpp | 2 +- src/solver/solver.cpp | 3 ++- src/util/CMakeLists.txt | 6 +++--- src/util/{version.h.cmake.in => z3_version.h.cmake.in} | 0 src/util/{version.h.in => z3_version.h.in} | 0 8 files changed, 10 insertions(+), 9 deletions(-) rename src/util/{version.h.cmake.in => z3_version.h.cmake.in} (100%) rename src/util/{version.h.in => z3_version.h.in} (100%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index ca62f5c5f..1ec5f05b5 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -10,7 +10,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): set_version(4, 8, 0, 0) - add_lib('util', []) + add_lib('util', [], includes2install = ['z3_version.h']) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) add_lib('nlsat', ['polynomial', 'sat']) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 770e118ee..ebe017739 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2805,8 +2805,8 @@ def get_full_version_string(major, minor, build, revision): # Update files with the version number def mk_version_dot_h(major, minor, build, revision): c = get_component(UTIL_COMPONENT) - version_template = os.path.join(c.src_dir, 'version.h.in') - version_header_output = os.path.join(c.src_dir, 'version.h') + version_template = os.path.join(c.src_dir, 'z3_version.h.in') + version_header_output = os.path.join(c.src_dir, 'z3_version.h') # Note the substitution names are what is used by the CMake # builds system. If you change these you should change them # in the CMake build too diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c2d7d84a3..c497c19ee 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -167,7 +167,7 @@ foreach (header ${libz3_public_headers}) PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}") endforeach() set_property(TARGET libz3 APPEND PROPERTY - PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/version.h") + PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/z3_version.h") install(TARGETS libz3 EXPORT Z3_EXPORTED_TARGETS diff --git a/src/shell/main.cpp b/src/shell/main.cpp index bb1c19b47..1c8b6908d 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -26,7 +26,7 @@ Revision History: #include "shell/smtlib_frontend.h" #include "shell/z3_log_frontend.h" #include "util/warning.h" -#include "util/version.h" +#include "util/z3_version.h" #include "shell/dimacs_frontend.h" #include "shell/datalog_frontend.h" #include "shell/opt_frontend.h" diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index e4fe09adf..a7c1372b3 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -273,7 +273,8 @@ expr_ref_vector solver::get_non_units(ast_manager& m) { } app* _f = to_app(f); if (_f->get_family_id() == bfid) { - // basic objects are true/false/and/or/not/=/distinct and proof objects (that are not Boolean) + // basic objects are true/false/and/or/not/=/distinct + // and proof objects (that are not Boolean). if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { fmls.append(_f->get_num_args(), _f->get_args()); } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index a84cc1f00..b6abb785f 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,11 +1,11 @@ -if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h") - message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\"" +if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/z3_version.h") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/z3_version.h\"" ${z3_polluted_tree_msg} ) endif() set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"") -configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h) +configure_file(z3_version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/z3_version.h) z3_add_component(util diff --git a/src/util/version.h.cmake.in b/src/util/z3_version.h.cmake.in similarity index 100% rename from src/util/version.h.cmake.in rename to src/util/z3_version.h.cmake.in diff --git a/src/util/version.h.in b/src/util/z3_version.h.in similarity index 100% rename from src/util/version.h.in rename to src/util/z3_version.h.in From e391416855aa5298c1ce880109e1b4fbfc2b7a49 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 20:30:50 -0700 Subject: [PATCH 16/41] fix include path for z3_version.h Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index e65eb1b32..ea5994ece 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "util/gparams.h" #include "util/env_params.h" -#include "util/version.h" +#include "util/z3_version.h" #include "ast/ast_smt_pp.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp_dot.h" From 8e0eebf507307b8a3ddc59f305a6486d78a5f4c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 20:37:13 -0700 Subject: [PATCH 17/41] fix include path for z3_version.h Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index cc2a13aed..4b3b85399 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -19,7 +19,7 @@ Revision History: --*/ #include #include "api/api_context.h" -#include "util/version.h" +#include "util/z3_version.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "api/api_log_macros.h" From 984e74428aedbc36ea5930ba78c9890594524444 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 20:41:26 -0700 Subject: [PATCH 18/41] fix include path for z3_version.h Signed-off-by: Nikolaj Bjorner --- src/api/api_log.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index 1bdbb8735..0f531b98e 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -19,7 +19,7 @@ Revision History: #include "api/z3.h" #include "api/api_log_macros.h" #include "util/util.h" -#include "util/version.h" +#include "util/z3_version.h" std::ostream * g_z3_log = nullptr; bool g_z3_log_enabled = false; From f349d3d0137c0ad09cf6881a4291743110b87630 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 21:15:28 -0700 Subject: [PATCH 19/41] fix extraction of non-units Signed-off-by: Nikolaj Bjorner --- src/solver/solver.cpp | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index a7c1372b3..66fedb36f 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -257,6 +257,15 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } +static bool is_atom(ast_manager& m, expr* f) { + if (!is_app(f)) return true; + app* _f = to_app(f); + family_id bfid = m.get_basic_family_id(); + if (_f->get_family_id() != bfid) return true; + if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; + return m.is_eq(f) || m.is_distinct(f); +} + expr_ref_vector solver::get_non_units(ast_manager& m) { expr_ref_vector result(m), fmls(m); get_assertions(fmls); @@ -275,13 +284,17 @@ expr_ref_vector solver::get_non_units(ast_manager& m) { if (_f->get_family_id() == bfid) { // basic objects are true/false/and/or/not/=/distinct // and proof objects (that are not Boolean). - if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { + if (i < sz0 && m.is_not(f) && is_atom(m, _f->get_arg(0))) { + marked.mark(_f->get_arg(0)); + } + else if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { fmls.append(_f->get_num_args(), _f->get_args()); } - else if (m.is_eq(f) || m.is_distinct(f)) { - if (i >= sz0) result.push_back(f); + else if (i >= sz0 && is_atom(m, f)) { + result.push_back(f); } } + else { if (i >= sz0) result.push_back(f); } From 3113901c8fecf70ce0284bce0797ab2f7013ee67 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Sep 2018 23:15:57 -0700 Subject: [PATCH 20/41] rename is_atom Signed-off-by: Nikolaj Bjorner --- src/solver/solver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 66fedb36f..1f0dac0ce 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -257,7 +257,7 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } -static bool is_atom(ast_manager& m, expr* f) { +static bool is_m_atom(ast_manager& m, expr* f) { if (!is_app(f)) return true; app* _f = to_app(f); family_id bfid = m.get_basic_family_id(); @@ -284,13 +284,13 @@ expr_ref_vector solver::get_non_units(ast_manager& m) { if (_f->get_family_id() == bfid) { // basic objects are true/false/and/or/not/=/distinct // and proof objects (that are not Boolean). - if (i < sz0 && m.is_not(f) && is_atom(m, _f->get_arg(0))) { + if (i < sz0 && m.is_not(f) && is_m_atom(m, _f->get_arg(0))) { marked.mark(_f->get_arg(0)); } else if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { fmls.append(_f->get_num_args(), _f->get_args()); } - else if (i >= sz0 && is_atom(m, f)) { + else if (i >= sz0 && is_m_atom(m, f)) { result.push_back(f); } } From 43f89dc2ccfbb24f2f13f394595abfd3e29b50bd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 22 Sep 2018 12:01:24 -0700 Subject: [PATCH 21/41] changes in column_info of lar_solver Signed-off-by: Lev Nachmanson --- src/util/lp/column_info.h | 10 ---------- src/util/lp/lar_solver.cpp | 9 ++------- src/util/lp/lar_solver.h | 2 +- src/util/lp/lp_primal_core_solver_def.h | 1 + src/util/lp/lp_solver_def.h | 2 +- 5 files changed, 5 insertions(+), 19 deletions(-) diff --git a/src/util/lp/column_info.h b/src/util/lp/column_info.h index 407f40dfc..2a38900c1 100644 --- a/src/util/lp/column_info.h +++ b/src/util/lp/column_info.h @@ -69,16 +69,6 @@ public: m_column_index(static_cast(-1)) {} - column_info(unsigned column_index) : - m_lower_bound_is_set(false), - m_lower_bound_is_strict(false), - m_upper_bound_is_set (false), - m_upper_bound_is_strict (false), - m_is_fixed(false), - m_cost(numeric_traits::zero()), - m_column_index(column_index) { - } - column_info(const column_info & ci) { m_name = ci.m_name; m_lower_bound_is_set = ci.m_lower_bound_is_set; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 30494aa1c..c83268602 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -909,13 +909,8 @@ bool lar_solver::try_to_set_fixed(column_info & ci) { return false; } -column_type lar_solver::get_column_type(const column_info & ci) { - auto ret = ci.get_column_type_no_flipping(); - if (ret == column_type::boxed) { // changing boxed to fixed because of the no span - if (ci.get_lower_bound() == ci.get_upper_bound()) - ret = column_type::fixed; - } - return ret; +column_type lar_solver::get_column_type(unsigned j) const{ + return m_mpq_lar_core_solver.m_column_types[j]; } std::string lar_solver::get_column_name(unsigned j) const { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index f3aa4f23b..cfe581ba3 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -395,7 +395,7 @@ public: bool try_to_set_fixed(column_info & ci); - column_type get_column_type(const column_info & ci); + column_type get_column_type(unsigned j) const; std::string get_column_name(unsigned j) const; diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h index 1e9edbd31..872922f60 100644 --- a/src/util/lp/lp_primal_core_solver_def.h +++ b/src/util/lp/lp_primal_core_solver_def.h @@ -1238,6 +1238,7 @@ template void lp_primal_core_solver::print_column break; case column_type::free_column: out << "( _" << this->m_x[j] << "_)" << std::endl; + break; default: lp_unreachable(); } diff --git a/src/util/lp/lp_solver_def.h b/src/util/lp/lp_solver_def.h index 10c7a6feb..9b385dee6 100644 --- a/src/util/lp/lp_solver_def.h +++ b/src/util/lp/lp_solver_def.h @@ -24,7 +24,7 @@ Revision History: namespace lp { template column_info * lp_solver::get_or_create_column_info(unsigned column) { auto it = m_map_from_var_index_to_column_info.find(column); - return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info(static_cast(-1))) : it->second; + return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info()) : it->second; } template From 7b3b1b6e9f70231d29981def70522913bc96ec20 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Sep 2018 14:04:15 -0700 Subject: [PATCH 22/41] pop to base before incremental internalization to ensure that units are not lost Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 3 ++- src/solver/solver.cpp | 21 +++++++++++---------- 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ff55598c2..097d3f0fa 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -259,7 +259,7 @@ public: return m_num_scopes; } - void assert_expr_core2(expr * t, expr * a) override { + void assert_expr_core2(expr * t, expr * a) override { if (a) { m_asmsf.push_back(a); assert_expr_core(m.mk_implies(a, t)); @@ -473,6 +473,7 @@ public: } void convert_internalized() { + m_solver.pop_to_base_level(); if (!is_internalized() && m_fmls_head > 0) { internalize_formulas(); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 1f0dac0ce..0e2128990 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -178,10 +178,19 @@ lbool solver::preferred_sat(expr_ref_vector const& asms, vector return check_sat(0, nullptr); } -bool solver::is_literal(ast_manager& m, expr* e) { - return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); + +static bool is_m_atom(ast_manager& m, expr* f) { + if (!is_app(f)) return true; + app* _f = to_app(f); + family_id bfid = m.get_basic_family_id(); + if (_f->get_family_id() != bfid) return true; + if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; + return m.is_eq(f) || m.is_distinct(f); } +bool solver::is_literal(ast_manager& m, expr* e) { + return is_m_atom(m, e) || (m.is_not(e, e) && is_m_atom(m, e)); +} void solver::assert_expr(expr* f) { expr_ref fml(f, get_manager()); @@ -257,14 +266,6 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } -static bool is_m_atom(ast_manager& m, expr* f) { - if (!is_app(f)) return true; - app* _f = to_app(f); - family_id bfid = m.get_basic_family_id(); - if (_f->get_family_id() != bfid) return true; - if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; - return m.is_eq(f) || m.is_distinct(f); -} expr_ref_vector solver::get_non_units(ast_manager& m) { expr_ref_vector result(m), fmls(m); From 9a09689dfab27059332092bf329db0c4abc258b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Sep 2018 19:19:05 -0700 Subject: [PATCH 23/41] add documentation on the cuber Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 11 ++++++++++- src/sat/sat_lookahead.cpp | 2 ++ src/sat/sat_params.pyg | 28 +++++++++++++++++++++++++--- 3 files changed, 37 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b9e15d329..a6b05904c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6605,7 +6605,12 @@ class Solver(Z3PPObject): _handle_parse_error(e, self.ctx) def cube(self, vars = None): - """Get set of cubes""" + """Get set of cubes + The method takes an optional set of variables that restrict which + variables may be used as a starting point for cubing. + If vars is not None, then the first case split is based on a variable in + this set. + """ self.cube_vs = AstVector(None, self.ctx) if vars is not None: for v in vars: @@ -6621,6 +6626,10 @@ class Solver(Z3PPObject): return def cube_vars(self): + """Access the set of variables that were touched by the most recently generated cube. + This set of variables can be used as a starting point for additional cubes. + The idea is that variables that appear in clauses that are reduced by the most recent + cube are likely more useful to cube on.""" return self.cube_vs def proof(self): diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 3833e2a52..4ca2c5f84 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -16,6 +16,8 @@ Author: Notes: + + --*/ #include diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 89776c479..113a8133e 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -50,17 +50,39 @@ def_module_params('sat', ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'), ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'), ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth. + # So if the value is 10, at most 1024 cubes will be generated of length 10. + # - freevars: cutoff based on a variable fraction of lookahead.cube.freevars. + # Cut if the number of current unassigned variables drops below a fraction of number of initial variables. + # - psat: Let psat_heur := (Sum_{clause C} (psat.clause_base ^ {-|C|+1})) / |freevars|^psat.var_exp + # Cut if the value of psat_heur exceeds psat.trigger + # - adaptive_freevars: Cut if the number of current unassigned variables drops below a fraction of free variables + # at the time of the last conflict. The fraction is increased every time the a cutoff is created. + # - adative_psat: Cut based on psat_heur in an adaptive way. ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), ('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), - ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), + ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free variable fraction. Used when lookahead.cube.cutoff is freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), - ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), - ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))) + ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')) + # reward function used to determine which literal to cube on. + # - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March. + # - heule_schur: reward function based on "Schur Number 5", Heule, AAAI 2018 + # The score of a literal lit is: + # Sum_{C in Clauses | lit in C} 2 ^ (- |C|+1) + # * Sum_{lit' in C | lit' != lit} lit_occs(~lit') + # / | C | + # where lit_occs(lit) is the number of clauses containing lit. + # - heuleu: The score of a literal lit is: Sum_{C in Clauses | lit in C} 2 ^ (-|C| + 1) + # - unit: heule_schur + also counts number of unit clauses. + # - march_cu: default reward function used in a version of March + # Each reward function also comes with its own variant of "mix_diff", which + # is the function for combining reward metrics for the positive and negative variant of a literal. + ) From 066b5334ad5882dff635abd354928f14b9a3c4d2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 22 Sep 2018 20:57:59 -0700 Subject: [PATCH 24/41] refactor some parameters into fields in Gomory cuts Signed-off-by: Lev Nachmanson --- src/util/lp/gomory.cpp | 119 +++++++++++++++++++++-------------------- 1 file changed, 62 insertions(+), 57 deletions(-) diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 96b3ab395..ad1c02625 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -27,11 +27,15 @@ class gomory::imp { lar_term & m_t; // the term to return in the cut mpq & m_k; // the right side of the cut explanation& m_ex; // the conflict explanation - unsigned m_inf_col; // a basis column which has to be an integer but has a not integral value + unsigned m_inf_col; // a basis column which has to be an integer but has a non integral value const row_strip& m_row; - const int_solver& m_int_solver; - - + const int_solver& m_int_solver; + mpq m_lcm_den; + mpq m_f; + mpq m_one_minus_f; + mpq m_fj; + mpq m_one_minus_fj; + const impq & get_value(unsigned j) const { return m_int_solver.get_value(j); } bool is_real(unsigned j) const { return m_int_solver.is_real(j); } bool at_lower(unsigned j) const { return m_int_solver.at_lower(j); } @@ -42,66 +46,60 @@ class gomory::imp { constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); } bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); } - void int_case_in_gomory_cut(const mpq & a, unsigned j, - mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) { - lp_assert(is_int(j) && !a.is_int()); - mpq fj = fractional_part(a); + void int_case_in_gomory_cut(unsigned j) { + lp_assert(is_int(j) && m_fj.is_pos()); TRACE("gomory_cut_detail", - tout << a << " j=" << j << " k = " << m_k; - tout << ", fj: " << fj << ", "; - tout << "a - fj = " << a - fj << ", "; + tout << " k = " << m_k; + tout << ", fj: " << m_fj << ", "; tout << (at_lower(j)?"at_lower":"at_upper")<< std::endl; ); - lp_assert(fj.is_pos() && (a - fj).is_int()); mpq new_a; if (at_lower(j)) { - new_a = fj <= one_minus_f0 ? fj / one_minus_f0 : ((1 - fj) / f0); + new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f); lp_assert(new_a.is_pos()); m_k.addmul(new_a, lower_bound(j).x); - m_ex.push_justification(column_lower_bound_constraint(j), new_a); + m_ex.push_justification(column_lower_bound_constraint(j)); } else { lp_assert(at_upper(j)); // the upper terms are inverted: therefore we have the minus - new_a = - (fj <= f0 ? fj / f0 : ((1 - fj) / one_minus_f0)); + new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f)); lp_assert(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); - m_ex.push_justification(column_upper_bound_constraint(j), new_a); + m_ex.push_justification(column_upper_bound_constraint(j)); } m_t.add_monomial(new_a, j); - lcm_den = lcm(lcm_den, denominator(new_a)); - TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";); + m_lcm_den = lcm(m_lcm_den, denominator(new_a)); + TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", m_lcm_den = " << m_lcm_den << "\n";); } - void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) { + void real_case_in_gomory_cut(const mpq & a, unsigned j) { TRACE("gomory_cut_detail_real", tout << "real\n";); mpq new_a; - if (at_lower(x_j)) { + if (at_lower(j)) { if (a.is_pos()) { - new_a = a / one_minus_f0; + new_a = a / m_one_minus_f; } else { - new_a = a / f0; - new_a.neg(); + new_a = - a / m_f; } - m_k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than - // k += lower_bound(x_j).x * new_a; - m_ex.push_justification(column_lower_bound_constraint(x_j), new_a); + m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than + // k += lower_bound(j).x * new_a; + m_ex.push_justification(column_lower_bound_constraint(j)); } else { - lp_assert(at_upper(x_j)); + lp_assert(at_upper(j)); if (a.is_pos()) { - new_a = a / f0; - new_a.neg(); // the upper terms are inverted. + new_a = - a / m_f; } else { - new_a = a / one_minus_f0; + new_a = a / m_one_minus_f; } - m_k.addmul(new_a, upper_bound(x_j).x); // k += upper_bound(x_j).x * new_a; - m_ex.push_justification(column_upper_bound_constraint(x_j), new_a); + m_k.addmul(new_a, upper_bound(j).x); // k += upper_bound(j).x * new_a; + m_ex.push_justification(column_upper_bound_constraint(j)); } - TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << m_k << "\n";); - m_t.add_monomial(new_a, x_j); + TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";); + m_t.add_monomial(new_a, j); } lia_move report_conflict_from_gomory_cut() { @@ -111,7 +109,7 @@ class gomory::imp { return lia_move::conflict; } - void adjust_term_and_k_for_some_ints_case_gomory(mpq &lcm_den) { + void adjust_term_and_k_for_some_ints_case_gomory() { lp_assert(!m_t.is_empty()); // k = 1 + sum of m_t at bounds auto pol = m_t.coeffs_as_vector(); @@ -134,16 +132,16 @@ class gomory::imp { m_t.add_monomial(mpq(1), v); } } else { - lcm_den = lcm(lcm_den, denominator(m_k)); - lp_assert(lcm_den.is_pos()); - TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << lcm_den << std::endl;); - if (!lcm_den.is_one()) { + m_lcm_den = lcm(m_lcm_den, denominator(m_k)); + lp_assert(m_lcm_den.is_pos()); + TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << m_lcm_den << std::endl;); + if (!m_lcm_den.is_one()) { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { - pi.first *= lcm_den; + pi.first *= m_lcm_den; SASSERT(!is_int(pi.second) || pi.first.is_int()); } - m_k *= lcm_den; + m_k *= m_lcm_den; } // negate everything to return -pol <= -m_k for (const auto & pi: pol) { @@ -275,14 +273,14 @@ public: // gomory will be t <= k and the current solution has a property t > k m_k = 1; m_t.clear(); - mpq lcm_den(1); + mpq m_lcm_den(1); bool some_int_columns = false; - mpq f0 = fractional_part(get_value(m_inf_col)); - TRACE("gomory_cut_detail", tout << "f0: " << f0 << ", "; - tout << "1 - f0: " << 1 - f0 << ", get_value(m_inf_col).x - f0 = " << get_value(m_inf_col).x - f0;); - lp_assert(f0.is_pos() && (get_value(m_inf_col).x - f0).is_int()); + mpq m_f = fractional_part(get_value(m_inf_col)); + TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; + tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f;); + lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); - mpq one_min_f0 = 1 - f0; + mpq one_min_m_f = 1 - m_f; for (const auto & p : m_row) { unsigned j = p.var(); if (j == m_inf_col) { @@ -290,20 +288,26 @@ public: TRACE("gomory_cut_detail", tout << "seeing basic var";); continue; } - // make the format compatible with the format used in: Integrating Simplex with DPLL(T) - mpq a = - p.coeff(); - if (is_real(j)) - real_case_in_gomory_cut(a, j, f0, one_min_f0); - else if (!a.is_int()) { // fj will be zero and no monomial will be added + + // use -p.coeff() to make the format compatible with the format used in: Integrating Simplex with DPLL(T) + if (is_real(j)) { + real_case_in_gomory_cut(- p.coeff(), j); + } else { + if (p.coeff().is_int()) { + // m_fj will be zero and no monomial will be added + continue; + } some_int_columns = true; - int_case_in_gomory_cut(a, j, lcm_den, f0, one_min_f0); + m_fj = fractional_part(-p.coeff()); + m_one_minus_fj = 1 - m_fj; + int_case_in_gomory_cut(j); } } if (m_t.is_empty()) return report_conflict_from_gomory_cut(); if (some_int_columns) - adjust_term_and_k_for_some_ints_case_gomory(lcm_den); + adjust_term_and_k_for_some_ints_case_gomory(); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); m_int_solver.m_lar_solver->subs_term_columns(m_t); @@ -317,9 +321,10 @@ public: m_ex(ex), m_inf_col(basic_inf_int_j), m_row(row), - m_int_solver(int_slv) - { - } + m_int_solver(int_slv), + m_lcm_den(1), + m_f(fractional_part(get_value(basic_inf_int_j).x)), + m_one_minus_f(1 - m_f) {} }; From 80d0c5cf8217e344e1a18de7dadda53298927074 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Sep 2018 16:52:25 -0700 Subject: [PATCH 25/41] fix #1836 again Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 12 ++++++++---- src/sat/sat_solver/inc_sat_solver.cpp | 4 ++++ 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index d7d8aeddc..231587729 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1815,8 +1815,10 @@ struct | _ -> UNKNOWN let get_model x = - let q = Z3native.solver_get_model (gc x) x in - try if Z3native.is_null_model q then None else Some q with | _ -> None + try + let q = Z3native.solver_get_model (gc x) x in + if Z3native.is_null_model q then None else Some q + with | _ -> None let get_proof x = let q = Z3native.solver_get_proof (gc x) x in @@ -1952,8 +1954,10 @@ struct | _ -> Solver.UNKNOWN let get_model (x:optimize) = - let q = Z3native.optimize_get_model (gc x) x in - if Z3native.is_null_model q then None else Some q + try + let q = Z3native.optimize_get_model (gc x) x in + if Z3native.is_null_model q then None else Some q + with | _ -> None let get_lower (x:handle) = Z3native.optimize_get_lower (gc x.opt) x.opt x.h let get_upper (x:handle) = Z3native.optimize_get_upper (gc x.opt) x.opt x.h diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 097d3f0fa..f0fe44160 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -113,6 +113,7 @@ public: if (m_num_scopes > 0) { throw default_exception("Cannot translate sat solver at non-base level"); } + std::cout << "translate\n"; std::cout.flush(); ast_translation tr(m, dst_m); m_solver.pop_to_base_level(); inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, is_incremental()); @@ -167,6 +168,7 @@ public: lbool check_sat(unsigned sz, expr * const * assumptions) override { m_solver.pop_to_base_level(); m_core.reset(); + std::cout << "#inconsistent: " << m_solver.inconsistent() << "\n"; if (m_solver.inconsistent()) return l_false; expr_ref_vector _assumptions(m); obj_map asm2fml; @@ -777,6 +779,8 @@ private: } m_core.push_back(e); } + std::cout << "core " << core << "\n"; + std::cout.flush(); } void check_assumptions(dep2asm_t& dep2asm) { From 7335b3bf565a0c6a50bd98c21fab67bee0ff810b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Sep 2018 16:53:15 -0700 Subject: [PATCH 26/41] remove debug Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index f0fe44160..097d3f0fa 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -113,7 +113,6 @@ public: if (m_num_scopes > 0) { throw default_exception("Cannot translate sat solver at non-base level"); } - std::cout << "translate\n"; std::cout.flush(); ast_translation tr(m, dst_m); m_solver.pop_to_base_level(); inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p, is_incremental()); @@ -168,7 +167,6 @@ public: lbool check_sat(unsigned sz, expr * const * assumptions) override { m_solver.pop_to_base_level(); m_core.reset(); - std::cout << "#inconsistent: " << m_solver.inconsistent() << "\n"; if (m_solver.inconsistent()) return l_false; expr_ref_vector _assumptions(m); obj_map asm2fml; @@ -779,8 +777,6 @@ private: } m_core.push_back(e); } - std::cout << "core " << core << "\n"; - std::cout.flush(); } void check_assumptions(dep2asm_t& dep2asm) { From af41255a9d01e50e328900dbbaeb48959e5d779c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Sep 2018 10:00:13 -0700 Subject: [PATCH 27/41] fix regression in model generation for UFLRA Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 41 +++++++++++++++++++++++++---------------- 1 file changed, 25 insertions(+), 16 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ca59a2c27..5b1de851e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -218,6 +218,8 @@ class theory_lra::imp { mutable std::unordered_map m_variable_values; // current model lp::var_index m_one_var; lp::var_index m_zero_var; + lp::var_index m_rone_var; + lp::var_index m_rzero_var; enum constraint_source { inequality_source, @@ -333,11 +335,11 @@ class theory_lra::imp { } } - void add_const(int c, lp::var_index& var) { + lp::var_index add_const(int c, lp::var_index& var, bool is_int) { if (var != UINT_MAX) { - return; + return var; } - app_ref cnst(a.mk_int(c), m); + app_ref cnst(a.mk_numeral(rational(c), is_int), m); TRACE("arith", tout << "add " << cnst << "\n";); enode* e = mk_enode(cnst); theory_var v = mk_var(cnst); @@ -347,16 +349,15 @@ class theory_lra::imp { m_var_trail.push_back(v); add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c))); add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c))); + return var; } - lp::var_index get_one() { - add_const(1, m_one_var); - return m_one_var; + lp::var_index get_one(bool is_int) { + return add_const(1, is_int ? m_one_var : m_rone_var, is_int); } - lp::var_index get_zero() { - add_const(0, m_zero_var); - return m_zero_var; + lp::var_index get_zero(bool is_int) { + return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int); } @@ -577,6 +578,7 @@ class theory_lra::imp { } enode * mk_enode(app * n) { + TRACE("arith", tout << expr_ref(n, m) << "\n";); if (ctx().e_internalized(n)) { return get_enode(n); } @@ -777,6 +779,7 @@ class theory_lra::imp { } theory_var internalize_def(app* term, scoped_internalize_state& st) { + TRACE("arith", tout << expr_ref(term, m) << "\n";); if (ctx().e_internalized(term)) { IF_VERBOSE(0, verbose_stream() << "repeated term\n";); return mk_var(term, false); @@ -807,10 +810,10 @@ class theory_lra::imp { return st.vars()[0]; } else if (is_one(st)) { - return get_one(); + return get_one(a.is_int(term)); } else if (is_zero(st)) { - return get_zero(); + return get_zero(a.is_int(term)); } else { init_left_side(st); @@ -820,7 +823,7 @@ class theory_lra::imp { if (vi == UINT_MAX) { rational const& offset = st.offset(); if (!offset.is_zero()) { - m_left_side.push_back(std::make_pair(offset, get_one())); + m_left_side.push_back(std::make_pair(offset, get_one(a.is_int(term)))); } SASSERT(!m_left_side.empty()); vi = m_solver->add_term(m_left_side); @@ -854,6 +857,8 @@ public: m_internalize_head(0), m_one_var(UINT_MAX), m_zero_var(UINT_MAX), + m_rone_var(UINT_MAX), + m_rzero_var(UINT_MAX), m_not_handled(nullptr), m_asserted_qhead(0), m_assume_eq_head(0), @@ -925,16 +930,18 @@ public: } return true; } + + bool is_arith(enode* n) { + return n && n->get_th_var(get_id()) != null_theory_var; + } void internalize_eq_eh(app * atom, bool_var) { + TRACE("arith_verbose", tout << mk_pp(atom, m) << "\n";); expr* lhs = nullptr, *rhs = nullptr; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); - if (n1->get_th_var(get_id()) != null_theory_var && - n2->get_th_var(get_id()) != null_theory_var && - n1 != n2) { - TRACE("arith_verbose", tout << mk_pp(atom, m) << "\n";); + if (is_arith(n1) && is_arith(n2) && n1 != n2) { m_arith_eq_adapter.mk_axioms(n1, n2); } } @@ -1301,6 +1308,7 @@ public: void init_variable_values() { reset_variable_values(); if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) { + TRACE("arith", tout << "update variable values\n";); m_solver->get_model(m_variable_values); } } @@ -3002,6 +3010,7 @@ public: if (!can_get_bound(v)) return false; lp::var_index vi = m_theory_var2var_index[v]; if (m_solver->has_value(vi, val)) { + TRACE("arith", tout << expr_ref(n->get_owner(), m) << " := " << val << "\n";); if (is_int(n) && !val.is_int()) return false; return true; } From 0b2b6b13061c1fccf4dac1c295d73813d169c522 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 25 Sep 2018 13:33:30 -0700 Subject: [PATCH 28/41] assert all_constraints_hold() rarely Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 56a61177c..a9bdf19d1 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -782,7 +782,7 @@ void lar_solver::solve_with_core_solver() { update_x_and_inf_costs_for_columns_with_changed_bounds(); m_mpq_lar_core_solver.solve(); set_status(m_mpq_lar_core_solver.m_r_solver.get_status()); - lp_assert(m_status != lp_status::OPTIMAL || all_constraints_hold()); + lp_assert((m_settings.random_next() % 100) != 0 || m_status != lp_status::OPTIMAL || all_constraints_hold()); } From 26d40865faddb888dfd72afc55b85777c34e2c1c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Sep 2018 23:54:48 -0700 Subject: [PATCH 29/41] add verbose output to capture cases for empty cube Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 097d3f0fa..5de64b496 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -311,7 +311,10 @@ public: expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override { if (!is_internalized()) { lbool r = internalize_formulas(); - if (r != l_true) return expr_ref_vector(m); + if (r != l_true) { + IF_VERBOSE(0, verbose_stream() << "internalize produced " << r << "\n"); + return expr_ref_vector(m); + } } convert_internalized(); obj_hashtable _vs; @@ -329,6 +332,7 @@ public: return result; } if (result == l_true) { + IF_VERBOSE(1, verbose_stream() << "formulas are SAT\n"); return expr_ref_vector(m); } expr_ref_vector fmls(m); @@ -345,6 +349,7 @@ public: vs.push_back(x); } } + if (fmls.empty()) { IF_VERBOSE(0, verbose_stream() << "no literals were produced in cube\n"); } return fmls; } From e0490450f3ae0811ee9650ab9e8ce685184ecfe5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Sep 2018 13:23:28 -0700 Subject: [PATCH 30/41] add capabilities to python API, fix model extraction for qsat Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 28 ++++++++++++++++++++++------ src/qe/qsat.cpp | 4 ++-- 2 files changed, 24 insertions(+), 8 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a6b05904c..253541a91 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1258,6 +1258,11 @@ def Consts(names, sort): names = names.split(" ") return [Const(name, sort) for name in names] +def FreshConst(sort, prefix='c'): + """Create a fresh constant of a specified sort""" + ctx = _get_ctx(sort.ctx) + return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx) + def Var(idx, s): """Create a Z3 free variable. Free variables are used to create quantified formulas. @@ -4280,7 +4285,7 @@ def get_map_func(a): _z3_assert(is_map(a), "Z3 array map expression expected.") return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx) -def ArraySort(d, r): +def ArraySort(*sig): """Return the Z3 array sort with the given domain and range sorts. >>> A = ArraySort(IntSort(), BoolSort()) @@ -4294,12 +4299,23 @@ def ArraySort(d, r): >>> AA Array(Int, Array(Int, Bool)) """ + sig = _get_args(sig) if __debug__: - _z3_assert(is_sort(d), "Z3 sort expected") - _z3_assert(is_sort(r), "Z3 sort expected") - _z3_assert(d.ctx == r.ctx, "Context mismatch") + z3_assert(len(sig) > 1, "At least two arguments expected") + arity = len(sig) - 1 + r = sig[arity] + d = sig[0] + if __debug__: + for s in sig: + _z3_assert(is_sort(s), "Z3 sort expected") + _z3_assert(s.ctx == r.ctx, "Context mismatch") ctx = d.ctx - return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx) + if len(sig) == 2: + return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx) + dom = (Sort * arity)() + for i in range(arity): + dom[i] = sig[i].ast + return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx) def Array(name, dom, rng): """Return an array constant named `name` with the given domain and range sorts. @@ -8048,7 +8064,7 @@ def substitute(t, *m): """ if isinstance(m, tuple): m1 = _get_args(m) - if isinstance(m1, list): + if isinstance(m1, list) and all(isinstance(p, tuple) for p in m1): m = m1 if __debug__: _z3_assert(is_expr(t), "Z3 expression expected") diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index c87b1c2eb..2ad5b9b96 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1266,9 +1266,9 @@ namespace qe { in->reset(); in->inc_depth(); result.push_back(in.get()); - if (in->models_enabled()) { + if (in->models_enabled()) { model_converter_ref mc; - mc = model2model_converter(m_model.get()); + mc = model2model_converter(m_model_save.get()); mc = concat(m_pred_abs.fmc(), mc.get()); in->add(mc.get()); } From 6dcec4ce79bf4b63606b67cb45c934ae2abd8ea9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Sep 2018 16:38:43 -0700 Subject: [PATCH 31/41] z3_assert -> _z3_assert Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 253541a91..8b37fb802 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4301,7 +4301,7 @@ def ArraySort(*sig): """ sig = _get_args(sig) if __debug__: - z3_assert(len(sig) > 1, "At least two arguments expected") + _z3_assert(len(sig) > 1, "At least two arguments expected") arity = len(sig) - 1 r = sig[arity] d = sig[0] From 5d586c8fd1817ce56f96c9cd594fce8bc1c22160 Mon Sep 17 00:00:00 2001 From: Lev Date: Fri, 28 Sep 2018 14:14:25 -0700 Subject: [PATCH 32/41] set lar_solver.m_status = UNKNOWN in the constructor Signed-off-by: Lev --- src/util/lp/int_solver.cpp | 4 ---- src/util/lp/lar_solver.cpp | 3 ++- src/util/lp/lar_solver.h | 1 - 3 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index 83fbe3961..0967c6cc6 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -187,10 +187,6 @@ struct check_return_helper { ~check_return_helper() { TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;); m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows); - if (m_r == lia_move::cut || m_r == lia_move::branch) { - int_solver * s = m_lar_solver->get_int_solver(); - // m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k)); - } } }; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 436e6ab04..5b3028a98 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -27,7 +27,7 @@ void clear() {lp_assert(false); // not implemented } -lar_solver::lar_solver() : m_status(lp_status::OPTIMAL), +lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), m_infeasible_column_index(-1), m_terms_start_index(1000000), m_mpq_lar_core_solver(m_settings, *this), @@ -1174,6 +1174,7 @@ void lar_solver::get_model(std::unordered_map & variable_values) std::unordered_set set_of_different_pairs; std::unordered_set set_of_different_singles; delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta); + TRACE("get_model", tout << "delta=" << delta << "size = " << m_mpq_lar_core_solver.m_r_x.size() << std::endl;); for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) { const numeric_pair & rp = m_mpq_lar_core_solver.m_r_x[i]; set_of_different_pairs.insert(rp); diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index cfe581ba3..4189bad4e 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -542,7 +542,6 @@ public: for (const auto & p : columns_to_subs) { auto it = t.m_coeffs.find(p.first); lp_assert(it != t.m_coeffs.end()); - const lar_term& lt = get_term(p.second); mpq v = it->second; t.m_coeffs.erase(it); t.m_coeffs[p.second] = v; From a5762a78e94dea0d02ba101692b68b847fa72195 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Sep 2018 17:39:18 -0700 Subject: [PATCH 33/41] change to ast-vector Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 5 +++-- src/api/ml/z3.mli | 4 ++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 25b437bc4..7415fc507 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1815,8 +1815,9 @@ struct | _ -> UNKNOWN let get_model x = - let q = Z3native.solver_get_model (gc x) x in - if Z3native.is_null_model q then None else Some q + let q = Z3native.solver_get_model (gc x) x in + try if Z3native.is_null_model q then None else Some q with | _ -> None + let get_proof x = let q = Z3native.solver_get_proof (gc x) x in diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index f67966a0f..18ade29bf 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3407,10 +3407,10 @@ sig (** Parse the given string using the SMT-LIB2 parser. @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *) - val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr + val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector (** Parse the given file using the SMT-LIB2 parser. *) - val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr + val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector end From 90fca8b378b493b4213711fa91edfe29a6a3031d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Sep 2018 17:44:28 -0700 Subject: [PATCH 34/41] add psat to available tactics Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/CMakeLists.txt | 2 ++ src/sat/sat_solver/inc_sat_solver.h | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/sat/sat_solver/CMakeLists.txt b/src/sat/sat_solver/CMakeLists.txt index 14eb4ac25..45a673367 100644 --- a/src/sat/sat_solver/CMakeLists.txt +++ b/src/sat/sat_solver/CMakeLists.txt @@ -8,4 +8,6 @@ z3_add_component(sat_solver core_tactics sat_tactic solver + TACTIC_HEADERS + inc_sat_solver.h ) diff --git a/src/sat/sat_solver/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h index 71ec48b99..b1cf7ad37 100644 --- a/src/sat/sat_solver/inc_sat_solver.h +++ b/src/sat/sat_solver/inc_sat_solver.h @@ -28,6 +28,9 @@ solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_ tactic* mk_psat_tactic(ast_manager& m, params_ref const& p); +/* + ADD_TACTIC('psat', '(try to) solve goal using a parallel SAT solver.', 'mk_psat_tactic(m, p)') +*/ void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights); From f0e74b7f2a75ae105418b9f5bb462a29bb7e6343 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 12:11:42 +0100 Subject: [PATCH 35/41] Fix for module name clash (and thus linking error) in the Visual Studio solution. --- src/util/lp/{bound_propagator.cpp => lp_bound_propagator.cpp} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/util/lp/{bound_propagator.cpp => lp_bound_propagator.cpp} (100%) diff --git a/src/util/lp/bound_propagator.cpp b/src/util/lp/lp_bound_propagator.cpp similarity index 100% rename from src/util/lp/bound_propagator.cpp rename to src/util/lp/lp_bound_propagator.cpp From 35bf63d563b682d794067c66f018a0fb06bf7ce2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 12:29:14 +0100 Subject: [PATCH 36/41] Fixed filename in CMakeLists.txt --- src/util/lp/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/CMakeLists.txt b/src/util/lp/CMakeLists.txt index 539c68712..edb73fdab 100644 --- a/src/util/lp/CMakeLists.txt +++ b/src/util/lp/CMakeLists.txt @@ -2,7 +2,7 @@ z3_add_component(lp SOURCES binary_heap_priority_queue.cpp binary_heap_upair_queue.cpp - bound_propagator.cpp + lp_bound_propagator.cpp core_solver_pretty_printer.cpp dense_matrix.cpp eta_matrix.cpp From 2a92de0aee7a77fee650f22f8b5acb3f16f57cf2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 15:20:00 +0100 Subject: [PATCH 37/41] Fixed side conditions for UFs translated from FP to BV. Fixes #1825. --- src/ast/fpa/fpa2bv_converter.cpp | 39 ++++++++++++++++++++++++++++++-- src/ast/fpa/fpa2bv_converter.h | 2 ++ src/ast/fpa/fpa2bv_rewriter.cpp | 11 +++++++++ 3 files changed, 50 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index dd3f35a2a..055f751c1 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -21,6 +21,8 @@ Notes: #include "ast/ast_smt2_pp.h" #include "ast/well_sorted.h" #include "ast/rewriter/th_rewriter.h" +#include "ast/used_vars.h" +#include "ast/rewriter/var_subst.h" #include "ast/fpa/fpa2bv_converter.h" #include "ast/rewriter/fpa_rewriter.h" @@ -230,6 +232,39 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result) result = m_util.mk_fp(sgn, e, s); } +expr_ref fpa2bv_converter::extra_quantify(expr * e) +{ + used_vars uv; + unsigned nv; + + ptr_buffer new_decl_sorts; + sbuffer new_decl_names; + expr_ref_buffer subst_map(m); + + uv(e); + nv = uv.get_num_vars(); + subst_map.resize(uv.get_max_found_var_idx_plus_1()); + + for (unsigned i = 0; i < nv; i++) + { + if (uv.contains(i)) { + TRACE("fpa2bv", tout << "uv[" << i << "] = " << mk_ismt2_pp(uv.get(i), m) << std::endl; ); + sort * s = uv.get(i); + var * v = m.mk_var(i, s); + new_decl_sorts.push_back(s); + new_decl_names.push_back(symbol(i)); + subst_map.set(i, v); + } + } + + expr_ref res(m); + var_subst vsubst(m); + res = vsubst.operator()(e, nv, subst_map.c_ptr()); + TRACE("fpa2bv", tout << "subst'd = " << mk_ismt2_pp(res, m) << std::endl; ); + res = m.mk_forall(nv, new_decl_sorts.c_ptr(), new_decl_names.c_ptr(), res); + return res; +} + void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; ); @@ -252,7 +287,7 @@ void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, e m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app), m_bv_util.mk_extract(sbits-2, 0, bv_app)); new_eq = m.mk_eq(fapp, flt_app); - m_extra_assertions.push_back(new_eq); + m_extra_assertions.push_back(extra_quantify(new_eq)); result = flt_app; } else if (m_util.is_rm(rng)) { @@ -263,7 +298,7 @@ void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, e bv_app = m.mk_app(bv_f, num, args); flt_app = m_util.mk_bv2rm(bv_app); new_eq = m.mk_eq(fapp, flt_app); - m_extra_assertions.push_back(new_eq); + m_extra_assertions.push_back(extra_quantify(new_eq)); result = flt_app; } else diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 7637317b0..812c24155 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -220,6 +220,8 @@ private: func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range); expr_ref nan_wrap(expr * n); + + expr_ref extra_quantify(expr * e); }; #endif diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index cc25905f0..b2614e27d 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -215,6 +215,12 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q, new_decl_names.push_back(symbol(name_buffer.c_str())); new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits)); } + else if (m_conv.is_rm(s)) { + name_buffer.reset(); + name_buffer << n << ".bv"; + new_decl_names.push_back(symbol(name_buffer.c_str())); + new_decl_sorts.push_back(m_conv.bu().mk_sort(3)); + } else { new_decl_sorts.push_back(s); new_decl_names.push_back(n); @@ -248,6 +254,11 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res m_conv.bu().mk_extract(ebits - 1, 0, new_var), m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var)); } + else if (m_conv.is_rm(s)) { + expr_ref new_var(m()); + new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(3)); + new_exp = m_conv.fu().mk_bv2rm(new_var); + } else new_exp = m().mk_var(t->get_idx(), s); From aaba1b9b15b787b020288dadc7c7298475a3007d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Oct 2018 09:18:40 -0700 Subject: [PATCH 38/41] fix sort retrieval for lambdas Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 +++- src/smt/theory_array_full.cpp | 15 ++++++++++++--- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 8b37fb802..cefe8bbbb 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1749,7 +1749,9 @@ class QuantifierRef(BoolRef): return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) def sort(self): - """Return the Boolean sort.""" + """Return the Boolean sort or sort of Lambda.""" + if self.is_lambda(): + return _sort(self.ctx, self.as_ast()) return BoolSort(self.ctx) def is_forall(self): diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index d872997c4..03cd3e1b2 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -339,6 +339,7 @@ namespace smt { SASSERT(v != null_theory_var); v = find(v); var_data* d = m_var_data[v]; + TRACE("array", tout << "v" << v << "\n";); for (enode * store : d->m_stores) { SASSERT(is_store(store)); instantiate_default_store_axiom(store); @@ -383,13 +384,21 @@ namespace smt { void theory_array_full::relevant_eh(app* n) { TRACE("array", tout << mk_pp(n, get_manager()) << "\n";); theory_array::relevant_eh(n); - if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)) { + if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n) && !is_store(n)) { return; } context & ctx = get_context(); enode* node = ctx.get_enode(n); - - if (is_select(n)) { + if (is_store(n)) { + enode * arg = ctx.get_enode(n->get_arg(0)); + if (is_const(arg)) { + TRACE("array", tout << expr_ref(arg->get_owner(), get_manager()) << " " << is_const(arg) << "\n";); + theory_var v = arg->get_th_var(get_id()); + set_prop_upward(v); + add_parent_default(v); + } + } + else if (is_select(n)) { enode * arg = ctx.get_enode(n->get_arg(0)); theory_var v = arg->get_th_var(get_id()); SASSERT(v != null_theory_var); From 48ec7c1175af91f8e43ab51153f8cc289b9e96dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 17:25:02 +0100 Subject: [PATCH 39/41] Follow-up fix for fpa2bv_converter. --- src/ast/fpa/fpa2bv_converter.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 055f751c1..1dc13ff9e 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -245,6 +245,9 @@ expr_ref fpa2bv_converter::extra_quantify(expr * e) nv = uv.get_num_vars(); subst_map.resize(uv.get_max_found_var_idx_plus_1()); + if (nv == 0) + return expr_ref(e, m); + for (unsigned i = 0; i < nv; i++) { if (uv.contains(i)) { From f145873603ca8b83a5a84e299528b7dfad7c845b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 20:22:20 +0100 Subject: [PATCH 40/41] CI Test From aaae3118de5d3faadffcdc9344089f377b6ecae6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 20:26:05 +0100 Subject: [PATCH 41/41] CI Test