mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
work on test for order lemma
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
parent
54f447d118
commit
0470547842
|
@ -1898,7 +1898,8 @@ void test_replace_column() {
|
||||||
void setup_args_parser(argument_parser & parser) {
|
void setup_args_parser(argument_parser & parser) {
|
||||||
parser.add_option_with_help_string("-nla_blfmz_mf", "test_basic_lemma_for_mon_zero_from_factor_to_monomial");
|
parser.add_option_with_help_string("-nla_blfmz_mf", "test_basic_lemma_for_mon_zero_from_factor_to_monomial");
|
||||||
parser.add_option_with_help_string("-nla_blfmz_fm", "test_basic_lemma_for_mon_zero_from_monomials_to_factor");
|
parser.add_option_with_help_string("-nla_blfmz_fm", "test_basic_lemma_for_mon_zero_from_monomials_to_factor");
|
||||||
parser.add_option_with_help_string("-nla_fact", "test nla_solver");
|
parser.add_option_with_help_string("-nla_fact", "test nla_solver factorization");
|
||||||
|
parser.add_option_with_help_string("-nla_order", "test nla_solver order lemma");
|
||||||
parser.add_option_with_help_string("-nla_bsl", "test_basic_sign_lemma");
|
parser.add_option_with_help_string("-nla_bsl", "test_basic_sign_lemma");
|
||||||
parser.add_option_with_help_string("-nla_blnt_mf", "test_basic_lemma_for_mon_neutral_from_monomial_to_factors");
|
parser.add_option_with_help_string("-nla_blnt_mf", "test_basic_lemma_for_mon_neutral_from_monomial_to_factors");
|
||||||
parser.add_option_with_help_string("-nla_blnt_fm", "test_basic_lemma_for_mon_neutral_from_factors_to_monomial");
|
parser.add_option_with_help_string("-nla_blnt_fm", "test_basic_lemma_for_mon_neutral_from_factors_to_monomial");
|
||||||
|
@ -3561,6 +3562,10 @@ void test_nla_factorization() {
|
||||||
nla::solver::test_factorization();
|
nla::solver::test_factorization();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void test_nla_order_lemma() {
|
||||||
|
nla::solver::test_order_lemma();
|
||||||
|
}
|
||||||
|
|
||||||
void test_lp_local(int argn, char**argv) {
|
void test_lp_local(int argn, char**argv) {
|
||||||
|
|
||||||
// initialize_util_module();
|
// initialize_util_module();
|
||||||
|
@ -3584,6 +3589,14 @@ void test_lp_local(int argn, char**argv) {
|
||||||
return finalize(0);
|
return finalize(0);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (args_parser.option_is_used("-nla_order")) {
|
||||||
|
#ifdef Z3DEBUG
|
||||||
|
test_nla_order_lemma();
|
||||||
|
#endif
|
||||||
|
return finalize(0);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
if (args_parser.option_is_used("-nla_bsl")) {
|
if (args_parser.option_is_used("-nla_bsl")) {
|
||||||
#ifdef Z3DEBUG
|
#ifdef Z3DEBUG
|
||||||
nla::solver::test_basic_sign_lemma();
|
nla::solver::test_basic_sign_lemma();
|
||||||
|
|
|
@ -91,7 +91,7 @@ class lar_solver : public column_namer {
|
||||||
lp_settings m_settings;
|
lp_settings m_settings;
|
||||||
lp_status m_status;
|
lp_status m_status;
|
||||||
stacked_value<simplex_strategy_enum> m_simplex_strategy;
|
stacked_value<simplex_strategy_enum> m_simplex_strategy;
|
||||||
var_register m_var_register;
|
var_register m_var_register;
|
||||||
stacked_vector<ul_pair> m_columns_to_ul_pairs;
|
stacked_vector<ul_pair> m_columns_to_ul_pairs;
|
||||||
vector<lar_base_constraint*> m_constraints;
|
vector<lar_base_constraint*> m_constraints;
|
||||||
stacked_value<unsigned> m_constraint_count;
|
stacked_value<unsigned> m_constraint_count;
|
||||||
|
@ -271,6 +271,8 @@ public:
|
||||||
|
|
||||||
var_index local2external(var_index idx) const { return m_var_register.local_to_external(idx); }
|
var_index local2external(var_index idx) const { return m_var_register.local_to_external(idx); }
|
||||||
|
|
||||||
|
unsigned number_of_vars() const { return m_var_register.size(); }
|
||||||
|
|
||||||
var_index external2local(unsigned j) const {
|
var_index external2local(unsigned j) const {
|
||||||
var_index local_j;
|
var_index local_j;
|
||||||
lp_assert(m_var_register.external_is_used(j, local_j));
|
lp_assert(m_var_register.external_is_used(j, local_j));
|
||||||
|
|
|
@ -235,7 +235,7 @@ struct solver::imp {
|
||||||
);
|
);
|
||||||
SASSERT(m_lemma->size() == 0);
|
SASSERT(m_lemma->size() == 0);
|
||||||
mk_ineq(rational(1), a.var(), -sign, b.var(), lp::lconstraint_kind::EQ, rational::zero());
|
mk_ineq(rational(1), a.var(), -sign, b.var(), lp::lconstraint_kind::EQ, rational::zero());
|
||||||
TRACE("nla_solver", print_explanation_and_lemma(tout););
|
TRACE("nla_solver", print_lemma(tout););
|
||||||
}
|
}
|
||||||
|
|
||||||
// Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus.
|
// Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus.
|
||||||
|
@ -327,7 +327,7 @@ struct solver::imp {
|
||||||
}
|
}
|
||||||
|
|
||||||
mk_ineq(m_monomials[i].var(), -sign, m_monomials[k].var(), lp::lconstraint_kind::EQ);
|
mk_ineq(m_monomials[i].var(), -sign, m_monomials[k].var(), lp::lconstraint_kind::EQ);
|
||||||
TRACE("nla_solver", print_explanation_and_lemma(tout););
|
TRACE("nla_solver", print_lemma(tout););
|
||||||
}
|
}
|
||||||
|
|
||||||
bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const vector<index_with_sign>& list){
|
bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector<rational>& abs_vals, const vector<index_with_sign>& list){
|
||||||
|
@ -391,8 +391,9 @@ struct solver::imp {
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
std::ostream & print_lemma(std::ostream & out) const {
|
||||||
std::ostream & print_lemma(lemma& l, std::ostream & out) const {
|
auto &l = *m_lemma;
|
||||||
|
out << "lemma: ";
|
||||||
for (unsigned i = 0; i < l.size(); i++) {
|
for (unsigned i = 0; i < l.size(); i++) {
|
||||||
print_ineq(l[i], out);
|
print_ineq(l[i], out);
|
||||||
if (i + 1 < l.size()) out << " or ";
|
if (i + 1 < l.size()) out << " or ";
|
||||||
|
@ -406,13 +407,6 @@ struct solver::imp {
|
||||||
for (lpvar j : vars) {
|
for (lpvar j : vars) {
|
||||||
print_var(j, out);
|
print_var(j, out);
|
||||||
}
|
}
|
||||||
return out;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::ostream & print_explanation_and_lemma(std::ostream & out) const {
|
|
||||||
out << "explanation:\n";
|
|
||||||
print_explanation(out) << "lemma: ";
|
|
||||||
print_lemma(*m_lemma, out);
|
|
||||||
out << "\n";
|
out << "\n";
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
@ -488,7 +482,7 @@ struct solver::imp {
|
||||||
}
|
}
|
||||||
expl_set e;
|
expl_set e;
|
||||||
add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
|
add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
|
||||||
TRACE("nla_solver", print_explanation_and_lemma(tout););
|
TRACE("nla_solver", print_lemma(tout););
|
||||||
|
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
@ -537,7 +531,7 @@ struct solver::imp {
|
||||||
|
|
||||||
expl_set e;
|
expl_set e;
|
||||||
add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
|
add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
|
||||||
TRACE("nla_solver", print_explanation_and_lemma(tout););
|
TRACE("nla_solver", print_lemma(tout););
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -599,7 +593,7 @@ struct solver::imp {
|
||||||
mk_ineq(not_one_j, lp::lconstraint_kind::EQ, -rational(1));
|
mk_ineq(not_one_j, lp::lconstraint_kind::EQ, -rational(1));
|
||||||
expl_set e;
|
expl_set e;
|
||||||
add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
|
add_explanation_of_factorization_and_set_explanation(i_mon, f, e);
|
||||||
TRACE("nla_solver", print_explanation_and_lemma(tout); );
|
TRACE("nla_solver", print_lemma(tout); );
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -640,7 +634,7 @@ struct solver::imp {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
mk_ineq(m_monomials[i_mon].var(), lp::lconstraint_kind::EQ, rational(sign));
|
mk_ineq(m_monomials[i_mon].var(), lp::lconstraint_kind::EQ, rational(sign));
|
||||||
TRACE("nla_solver", print_explanation_and_lemma(tout););
|
TRACE("nla_solver", print_lemma(tout););
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -652,7 +646,7 @@ struct solver::imp {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
mk_ineq(m_monomials[i_mon].var(), -rational(sign), not_one_j,lp::lconstraint_kind::EQ);
|
mk_ineq(m_monomials[i_mon].var(), -rational(sign), not_one_j,lp::lconstraint_kind::EQ);
|
||||||
TRACE("nla_solver", print_explanation_and_lemma(tout););
|
TRACE("nla_solver", print_lemma(tout););
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1188,7 +1182,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
|
||||||
|
|
||||||
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
||||||
|
|
||||||
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
|
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
|
||||||
|
|
||||||
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(1));
|
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(1));
|
||||||
i0.m_term.add_coeff_var(lp_ac);
|
i0.m_term.add_coeff_var(lp_ac);
|
||||||
|
@ -1247,7 +1241,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
|
||||||
|
|
||||||
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
||||||
SASSERT(lemma.size() == 4);
|
SASSERT(lemma.size() == 4);
|
||||||
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
|
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
|
||||||
|
|
||||||
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(1));
|
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(1));
|
||||||
i0.m_term.add_coeff_var(lp_b);
|
i0.m_term.add_coeff_var(lp_b);
|
||||||
|
@ -1326,7 +1320,7 @@ void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
|
||||||
s.set_column_value(lp_be, rational(1));
|
s.set_column_value(lp_be, rational(1));
|
||||||
|
|
||||||
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
||||||
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
|
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
|
||||||
SASSERT(lemma.size() == 2);
|
SASSERT(lemma.size() == 2);
|
||||||
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(0));
|
ineq i0(lp::lconstraint_kind::NE, lp::lar_term(), rational(0));
|
||||||
i0.m_term.add_coeff_var(lp_b);
|
i0.m_term.add_coeff_var(lp_b);
|
||||||
|
@ -1390,7 +1384,7 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
|
||||||
|
|
||||||
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
||||||
|
|
||||||
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
|
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
|
||||||
|
|
||||||
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
|
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
|
||||||
i0.m_term.add_coeff_var(lp_b);
|
i0.m_term.add_coeff_var(lp_b);
|
||||||
|
@ -1468,7 +1462,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
|
||||||
// we have bde = -b, therefore d = +-1 and e = +-1
|
// we have bde = -b, therefore d = +-1 and e = +-1
|
||||||
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
||||||
|
|
||||||
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
|
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
|
||||||
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(1));
|
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(1));
|
||||||
i0.m_term.add_coeff_var(lp_b);
|
i0.m_term.add_coeff_var(lp_b);
|
||||||
ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), -rational(1));
|
ineq i1(lp::lconstraint_kind::EQ, lp::lar_term(), -rational(1));
|
||||||
|
@ -1544,7 +1538,7 @@ void solver::test_basic_sign_lemma() {
|
||||||
t.add_coeff_var(lp_acd);
|
t.add_coeff_var(lp_acd);
|
||||||
ineq q(lp::lconstraint_kind::EQ, t, rational(0));
|
ineq q(lp::lconstraint_kind::EQ, t, rational(0));
|
||||||
|
|
||||||
nla.m_imp->print_explanation_and_lemma(std::cout << "expl & lemma: ");
|
nla.m_imp->print_lemma(std::cout << "expl & lemma: ");
|
||||||
SASSERT(q == lemma.back());
|
SASSERT(q == lemma.back());
|
||||||
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
|
ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
|
||||||
i0.m_term.add_coeff_var(lp_bde);
|
i0.m_term.add_coeff_var(lp_bde);
|
||||||
|
@ -1558,4 +1552,114 @@ void solver::test_basic_sign_lemma() {
|
||||||
|
|
||||||
SASSERT(found);
|
SASSERT(found);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void solver::test_order_lemma() {
|
||||||
|
enable_trace("nla_solver");
|
||||||
|
lp::lar_solver s;
|
||||||
|
unsigned a = 0, b = 1, c = 2, d = 3, e = 4, f = 5,
|
||||||
|
i = 8, j = 9,
|
||||||
|
ab = 10, cd = 11, ef = 12, abef = 13, cdij = 16, ij = 17;
|
||||||
|
|
||||||
|
lpvar lp_a = s.add_var(a, true);
|
||||||
|
lpvar lp_b = s.add_var(b, true);
|
||||||
|
lpvar lp_c = s.add_var(c, true);
|
||||||
|
lpvar lp_d = s.add_var(d, true);
|
||||||
|
lpvar lp_e = s.add_var(e, true);
|
||||||
|
lpvar lp_f = s.add_var(f, true);
|
||||||
|
lpvar lp_i = s.add_var(i, true);
|
||||||
|
lpvar lp_j = s.add_var(j, true);
|
||||||
|
lpvar lp_ab = s.add_var(ab, true);
|
||||||
|
lpvar lp_cd = s.add_var(cd, true);
|
||||||
|
lpvar lp_ef = s.add_var(ef, true);
|
||||||
|
lpvar lp_ij = s.add_var(ij, true);
|
||||||
|
lpvar lp_abef = s.add_var(abef, true);
|
||||||
|
lpvar lp_cdij = s.add_var(cdij, true);
|
||||||
|
|
||||||
|
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||||
|
s.set_column_value(j, rational(3));
|
||||||
|
}
|
||||||
|
|
||||||
|
reslimit l;
|
||||||
|
params_ref p;
|
||||||
|
solver nla(s, l, p);
|
||||||
|
// create monomial ab
|
||||||
|
vector<unsigned> vec;
|
||||||
|
vec.push_back(lp_a);
|
||||||
|
vec.push_back(lp_b);
|
||||||
|
nla.add_monomial(lp_ab, vec.size(), vec.begin());
|
||||||
|
// create monomial cd
|
||||||
|
vec.clear();
|
||||||
|
vec.push_back(lp_c);
|
||||||
|
vec.push_back(lp_d);
|
||||||
|
nla.add_monomial(lp_cd, vec.size(), vec.begin());
|
||||||
|
// create monomial ef
|
||||||
|
vec.clear();
|
||||||
|
vec.push_back(lp_e);
|
||||||
|
vec.push_back(lp_f);
|
||||||
|
nla.add_monomial(lp_ef, vec.size(), vec.begin());
|
||||||
|
// create monomial ij
|
||||||
|
vec.clear();
|
||||||
|
vec.push_back(lp_i);
|
||||||
|
vec.push_back(lp_j);
|
||||||
|
nla.add_monomial(lp_ij, vec.size(), vec.begin());
|
||||||
|
|
||||||
|
// make ab < cd it the model
|
||||||
|
s.set_column_value(lp_ab, rational(7));
|
||||||
|
s.set_column_value(lp_cd, rational(8));
|
||||||
|
|
||||||
|
s.set_column_value(lp_a, rational(4));
|
||||||
|
s.set_column_value(lp_b, rational(4));
|
||||||
|
s.set_column_value(lp_c, rational(2));
|
||||||
|
s.set_column_value(lp_d, rational(3));
|
||||||
|
//create monomial abef
|
||||||
|
vec.clear();
|
||||||
|
vec.push_back(lp_e);
|
||||||
|
vec.push_back(lp_a);
|
||||||
|
vec.push_back(lp_b);
|
||||||
|
vec.push_back(lp_f);
|
||||||
|
nla.add_monomial(lp_abef, vec.size(), vec.begin());
|
||||||
|
|
||||||
|
s.set_column_value(lp_e, rational(9));
|
||||||
|
s.set_column_value(lp_f, rational(11));
|
||||||
|
|
||||||
|
//create monomial cdij
|
||||||
|
vec.clear();
|
||||||
|
vec.push_back(lp_i);
|
||||||
|
vec.push_back(lp_j);
|
||||||
|
vec.push_back(lp_c);
|
||||||
|
vec.push_back(lp_d);
|
||||||
|
nla.add_monomial(lp_cdij, vec.size(), vec.begin());
|
||||||
|
|
||||||
|
// set ij == ef in the model
|
||||||
|
s.set_column_value(lp_ij, rational(17));
|
||||||
|
s.set_column_value(lp_ef, rational(17));
|
||||||
|
|
||||||
|
// set abef = cdij, while it has to be abef < cdij
|
||||||
|
s.set_column_value(lp_abef, rational(18));
|
||||||
|
s.set_column_value(lp_cdij, rational(18));
|
||||||
|
|
||||||
|
vector<ineq> lemma;
|
||||||
|
lp::explanation exp;
|
||||||
|
|
||||||
|
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
|
||||||
|
|
||||||
|
// lp::lar_term t;
|
||||||
|
// t.add_coeff_var(lp_bde);
|
||||||
|
// t.add_coeff_var(lp_acd);
|
||||||
|
// ineq q(lp::lconstraint_kind::EQ, t, rational(0));
|
||||||
|
|
||||||
|
nla.m_imp->print_lemma(std::cout << "lemma: ");
|
||||||
|
// SASSERT(q == lemma.back());
|
||||||
|
// ineq i0(lp::lconstraint_kind::EQ, lp::lar_term(), rational(0));
|
||||||
|
// i0.m_term.add_coeff_var(lp_bde);
|
||||||
|
// i0.m_term.add_coeff_var(rational(1), lp_acd);
|
||||||
|
// bool found = false;
|
||||||
|
// for (const auto& k : lemma){
|
||||||
|
// if (k == i0) {
|
||||||
|
// found = true;
|
||||||
|
// }
|
||||||
|
// }
|
||||||
|
|
||||||
|
// SASSERT(found);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -59,5 +59,6 @@ public:
|
||||||
static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
|
static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
|
||||||
static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0();
|
static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0();
|
||||||
static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1();
|
static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1();
|
||||||
|
static void test_order_lemma();
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue