mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

create a test for order lemma

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-22 10:21:37 -08:00 committed by Lev Nachmanson
parent 54edea4f37
commit ea02231ef8
3 changed files with 77 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/test/lp/lp.cpp
View file

@ -1900,6 +1900,7 @@ void setup_args_parser(argument_parser & parser) {
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 factorization");
parser.add_option_with_help_string("-nla_order", "test nla_solver order lemma");
parser.add_option_with_help_string("-nla_monot", "test nla_solver order 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_fm", "test_basic_lemma_for_mon_neutral_from_factors_to_monomial");
@ -3597,6 +3598,13 @@ void test_lp_local(int argn, char**argv) {
}
if (args_parser.option_is_used("-nla_monot")) {
#ifdef Z3DEBUG
nla::solver::test_monotone_lemma();
#endif
return finalize(0);
}
if (args_parser.option_is_used("-nla_bsl")) {
#ifdef Z3DEBUG
nla::solver::test_basic_sign_lemma();

68
src/util/lp/nla_solver.cpp
View file

@ -2257,6 +2257,74 @@ void solver::test_order_lemma_params(bool var_equiv, int sign) {
// SASSERT(found);
}
void solver::test_monotone_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, ij = 17;
lpvar lp_a = s.add_named_var(a, true, "a");
lpvar lp_b = s.add_named_var(b, true, "b");
lpvar lp_c = s.add_named_var(c, true, "c");
lpvar lp_d = s.add_named_var(d, true, "d");
lpvar lp_e = s.add_named_var(e, true, "e");
lpvar lp_f = s.add_named_var(f, true, "f");
lpvar lp_i = s.add_named_var(i, true, "i");
lpvar lp_j = s.add_named_var(j, true, "j");
lpvar lp_ab = s.add_named_var(ab, true, "ab");
lpvar lp_cd = s.add_named_var(cd, true, "cd");
lpvar lp_ef = s.add_named_var(ef, true, "ef");
lpvar lp_ij = s.add_named_var(ij, true, "ij");
// lpvar lp_abef = s.add_named_var(abef, true, "abef");
for (unsigned j = 0; j < s.number_of_vars(); j++) {
s.set_column_value(j, rational((j + 2)*(j + 2)));
}
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);
int mon_ab = nla.add_monomial(lp_ab, vec.size(), vec.begin());
// create monomial cd
vec.clear();
vec.push_back(lp_c);
vec.push_back(lp_d);
int mon_cd = 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);
int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin());
// set e == i + 1
s.set_column_value(lp_e, s.get_column_value(lp_i) + rational(1));
// set f == j + 1
s.set_column_value(lp_f, s.get_column_value(lp_j) + rational(1));
// set the values of ab, ef, cd, and ij correctly
s.set_column_value(lp_ab, nla.m_imp->mon_value_by_vars(mon_ab));
s.set_column_value(lp_cd, nla.m_imp->mon_value_by_vars(mon_cd));
s.set_column_value(lp_ij, nla.m_imp->mon_value_by_vars(mon_ij));
// set ef = ij while it has to be ef > ij
s.set_column_value(lp_ef, s.get_column_value(lp_ij));
vector<ineq> lemma;
lp::explanation exp;
SASSERT(nla.m_imp->test_check(lemma, exp) == l_false);
nla.m_imp->print_lemma(std::cout << "lemma: ");
}
void solver::test_order_lemma() {
test_order_lemma_params(false, 1);
test_order_lemma_params(false, -1);

1
src/util/lp/nla_solver.h
View file

@ -73,5 +73,6 @@ public:
static void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1();
static void test_order_lemma();
static void test_order_lemma_params(bool, int sign);
static void test_monotone_lemma();
};
}