diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 9e917728b..03bd61ff1 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1705,7 +1705,7 @@ bool lar_solver::all_vars_are_registered(const vector> return true; } -// do not register this term if ext_i == -1 +// do not register this term if ext_i == UINT_MAX var_index lar_solver::add_term(const vector> & coeffs, unsigned ext_i) { TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); m_term_register.add_var(ext_i, term_is_int(coeffs)); @@ -2370,7 +2370,7 @@ std::pair lar_solver::add_equality(lpvar j, vector> coeffs; coeffs.push_back(std::make_pair(mpq(1),j)); coeffs.push_back(std::make_pair(mpq(-1),k)); - unsigned term_index = add_term(coeffs, -1); // -1 is the external null var + unsigned term_index = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var return std::pair( add_var_bound(term_index, lconstraint_kind::LE, mpq(0)), add_var_bound(term_index, lconstraint_kind::GE, mpq(0))); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index fc45f8e7c..dce1ebe0f 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -586,10 +586,14 @@ public: std::ostream& print_column_info(unsigned j, std::ostream& out) const { m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); - if( !column_corresponds_to_term(j)) - return out; - const lar_term& t = * m_terms[m_var_register.local_to_external(j) - m_terms_start_index]; - print_term_as_indices(t, out) << "\n"; + if (is_term(j)) { + const lar_term& t = * m_terms[j - m_terms_start_index]; + print_term_as_indices(t, out) << "\n"; + + } else if(column_corresponds_to_term(j)) { + const lar_term& t = * m_terms[m_var_register.local_to_external(j) - m_terms_start_index]; + print_term_as_indices(t, out) << "\n"; + } return out; } diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h index 66a629465..46c6c3f7b 100644 --- a/src/math/lp/var_eqs.h +++ b/src/math/lp/var_eqs.h @@ -108,6 +108,8 @@ public: \brief merge equivalence classes for v1, v2 with justification j */ void merge(signed_var v1, signed_var v2, eq_justification const& j) { + if (v1 == v2) + return; unsigned max_i = std::max(v1.index(), v2.index()) + 2; m_eqs.reserve(max_i); while (m_uf.get_num_vars() <= max_i) m_uf.mk_var(); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index fabd75598..5ac0121a1 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -58,8 +58,10 @@ #include "math/lp/horner.h" #include "math/lp/cross_nested.h" #include "math/lp/int_cube.h" +#include "math/lp/emonics.h" namespace nla { void test_horner(); +void test_monics(); void test_order_lemma(); void test_monotone_lemma(); void test_basic_sign_lemma(); @@ -2149,6 +2151,7 @@ void test_replace_column() { void setup_args_parser(argument_parser & parser) { + parser.add_option_with_help_string("-monics", "test emonics"); parser.add_option_with_help_string("-nex_order", "test nex order"); parser.add_option_with_help_string("-nla_cn", "test cross nornmal form"); parser.add_option_with_help_string("-nla_sim", "test nex simplify"); @@ -3846,6 +3849,11 @@ void test_lp_local(int argn, char**argv) { } args_parser.print(); + if (args_parser.option_is_used("-monics")) { + nla::test_monics(); + return finalize(0); + } + if (args_parser.option_is_used("-nla_cn")) { #ifdef Z3DEBUG diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index f31793d21..ee12466b1 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -19,6 +19,89 @@ Revision History: --*/ #include "math/lp/nla_solver.h" namespace nla { + +svector get_monic(int monic_size, int var_bound, random_gen& rand) { + svector v; + for (int i = 0; i < monic_size; i++) { + lpvar j = rand() % var_bound; + v.push_back(j); + } + return v; +} + +void add_equality(int n_of_vars, var_eqs & var_eqs, random_gen& rand, bool use_max) { + lpvar a = rand() % n_of_vars; + lpvar b = rand() % n_of_vars; + while (a == b) { + b = rand() % n_of_vars; + } + SASSERT(a != b); + var_eqs.merge_plus(a, b, eq_justification({0})); +} + +void test_monics_on_setup(int n_of_monics , + int n_of_vars , + int max_monic_size, + int min_monic_size, + int number_of_pushes, + int number_of_eqs, + var_eqs & var_eqs, + emonics& ms, random_gen & rand) { + int i; + for ( i = 0; i < n_of_monics; i++) { + int size = min_monic_size + rand() % (max_monic_size - min_monic_size); + ms.add(n_of_vars + i, get_monic(size, n_of_vars, rand)); + } + // add the monomial with the same vars + ms.add(n_of_vars + i, ms[n_of_vars + i - 1].vars()); + int eqs_left = number_of_eqs; + int add_max_var = 4; + for (int i = 0; i < number_of_pushes; i++) { + ms.push(); + if (eqs_left > 0) { + if( i < number_of_pushes - 1) { + eqs_left --; + add_equality(n_of_vars, var_eqs, rand, add_max_var == 0); + add_max_var--;; + } else { + do { + add_equality(n_of_vars, var_eqs, rand, add_max_var == 0); + add_max_var--;; + } while(--eqs_left >= 0); + } + } + ms.pop(1); + } + +} + +void test_monics() { + std::cout << "test monics\n"; + random_gen rand; + + for (int reps = 1000; reps > 0; reps--){ + int m = rand() % 100; + int n_of_monics = 6 * m; + int n_of_vars = 10 * m ; + int max_monic_size = 4 *m; + int min_monic_size = 2* m; + int number_of_pushes = 9*m; + int number_of_eqs = 7*m; + var_eqs var_eqs; + emonics ms(var_eqs); + test_monics_on_setup(n_of_monics, + n_of_vars, + max_monic_size, + min_monic_size, + number_of_pushes, + number_of_eqs, + var_eqs, + ms, + rand) ; + } + +} + void create_abcde(solver & nla, unsigned lp_a, unsigned lp_b,