mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
refactor tests from nla_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
c9e989ae85
commit
48fcd66bb9
|
|
@ -1,6 +1,6 @@
|
|||
add_executable(lp_tst
|
||||
EXCLUDE_FROM_ALL
|
||||
lp_main.cpp lp.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:polynomial> $<TARGET_OBJECTS:nlsat> $<TARGET_OBJECTS:lp> )
|
||||
lp_main.cpp lp.cpp nla_solver_test.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:polynomial> $<TARGET_OBJECTS:nlsat> $<TARGET_OBJECTS:lp> )
|
||||
target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
|
||||
target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
|
||||
target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
|
||||
|
|
|
|||
|
|
@ -55,6 +55,18 @@
|
|||
#include "util/lp/general_matrix.h"
|
||||
#include "util/lp/bound_propagator.h"
|
||||
#include "util/lp/nla_solver.h"
|
||||
namespace nla {
|
||||
void test_factorization();
|
||||
void test_order_lemma();
|
||||
void test_monotone_lemma();
|
||||
void test_basic_sign_lemma();
|
||||
void test_tangent_lemma();
|
||||
void test_basic_lemma_for_mon_zero_from_monomial_to_factors();
|
||||
void test_basic_lemma_for_mon_zero_from_factors_to_monomial();
|
||||
void test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
|
||||
void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
|
||||
}
|
||||
|
||||
namespace lp {
|
||||
unsigned seed = 1;
|
||||
|
||||
|
|
@ -3557,11 +3569,11 @@ void test_gomory_cut() {
|
|||
}
|
||||
|
||||
void test_nla_factorization() {
|
||||
nla::solver::test_factorization();
|
||||
nla::test_factorization();
|
||||
}
|
||||
|
||||
void test_nla_order_lemma() {
|
||||
nla::solver::test_order_lemma();
|
||||
nla::test_order_lemma();
|
||||
}
|
||||
|
||||
void test_lp_local(int argn, char**argv) {
|
||||
|
|
@ -3597,49 +3609,49 @@ void test_lp_local(int argn, char**argv) {
|
|||
|
||||
if (args_parser.option_is_used("-nla_monot")) {
|
||||
#ifdef Z3DEBUG
|
||||
nla::solver::test_monotone_lemma();
|
||||
nla::test_monotone_lemma();
|
||||
#endif
|
||||
return finalize(0);
|
||||
}
|
||||
|
||||
if (args_parser.option_is_used("-nla_bsl")) {
|
||||
#ifdef Z3DEBUG
|
||||
nla::solver::test_basic_sign_lemma();
|
||||
nla::test_basic_sign_lemma();
|
||||
#endif
|
||||
return finalize(0);
|
||||
}
|
||||
|
||||
if (args_parser.option_is_used("-nla_tan")) {
|
||||
#ifdef Z3DEBUG
|
||||
nla::solver::test_tangent_lemma();
|
||||
nla::test_tangent_lemma();
|
||||
#endif
|
||||
return finalize(0);
|
||||
}
|
||||
|
||||
if (args_parser.option_is_used("-nla_blfmz_mf")) {
|
||||
#ifdef Z3DEBUG
|
||||
nla::solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors();
|
||||
nla::test_basic_lemma_for_mon_zero_from_monomial_to_factors();
|
||||
#endif
|
||||
return finalize(0);
|
||||
}
|
||||
|
||||
if (args_parser.option_is_used("-nla_blfmz_fm")) {
|
||||
#ifdef Z3DEBUG
|
||||
nla::solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial();
|
||||
nla::test_basic_lemma_for_mon_zero_from_factors_to_monomial();
|
||||
#endif
|
||||
return finalize(0);
|
||||
}
|
||||
|
||||
if (args_parser.option_is_used("-nla_blnt_mf")) {
|
||||
#ifdef Z3DEBUG
|
||||
nla::solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
|
||||
nla::test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
|
||||
#endif
|
||||
return finalize(0);
|
||||
}
|
||||
|
||||
if (args_parser.option_is_used("-nla_blnt_fm")) {
|
||||
#ifdef Z3DEBUG
|
||||
nla::solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
|
||||
nla::test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
|
||||
#endif
|
||||
return finalize(0);
|
||||
}
|
||||
|
|
|
|||
815
src/test/lp/nla_solver_test.cpp
Normal file
815
src/test/lp/nla_solver_test.cpp
Normal file
|
|
@ -0,0 +1,815 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
Nikolaj Bjorner (nbjorner)
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
#include "util/lp/nla_solver.h"
|
||||
namespace nla {
|
||||
void create_abcde(solver & nla,
|
||||
unsigned lp_a,
|
||||
unsigned lp_b,
|
||||
unsigned lp_c,
|
||||
unsigned lp_d,
|
||||
unsigned lp_e,
|
||||
unsigned lp_abcde,
|
||||
unsigned lp_ac,
|
||||
unsigned lp_bde,
|
||||
unsigned lp_acd,
|
||||
unsigned lp_be) {
|
||||
// create monomial abcde
|
||||
vector<unsigned> vec;
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_b);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
vec.push_back(lp_e);
|
||||
|
||||
nla.add_monomial(lp_abcde, vec.size(), vec.begin());
|
||||
|
||||
// create monomial ac
|
||||
vec.clear();
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_c);
|
||||
nla.add_monomial(lp_ac, vec.size(), vec.begin());
|
||||
|
||||
// create monomial bde
|
||||
vec.clear();
|
||||
vec.push_back(lp_b);
|
||||
vec.push_back(lp_d);
|
||||
vec.push_back(lp_e);
|
||||
nla.add_monomial(lp_bde, vec.size(), vec.begin());
|
||||
|
||||
// create monomial acd
|
||||
vec.clear();
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
nla.add_monomial(lp_acd, vec.size(), vec.begin());
|
||||
|
||||
// create monomial be
|
||||
vec.clear();
|
||||
vec.push_back(lp_b);
|
||||
vec.push_back(lp_e);
|
||||
nla.add_monomial(lp_be, vec.size(), vec.begin());
|
||||
}
|
||||
|
||||
void test_factorization() {
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
|
||||
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_abcde = s.add_named_var(abcde, true, "abcde");
|
||||
lpvar lp_ac = s.add_named_var(ac, true, "ac");
|
||||
lpvar lp_bde = s.add_named_var(bde, true, "bde");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
lpvar lp_be = s.add_named_var(be, true, "be");
|
||||
|
||||
solver nla(s);
|
||||
|
||||
create_abcde(nla,
|
||||
lp_a,
|
||||
lp_b,
|
||||
lp_c,
|
||||
lp_d,
|
||||
lp_e,
|
||||
lp_abcde,
|
||||
lp_ac,
|
||||
lp_bde,
|
||||
lp_acd,
|
||||
lp_be);
|
||||
nla.get_core()->register_monomials_in_tables();
|
||||
nla.get_core()->print_monomials(std::cout);
|
||||
nla.get_core()->test_factorization(1, // 0 is the index of monomial abcde
|
||||
1); // 3 is the number of expected factorizations
|
||||
nla.get_core()->test_factorization(0, // 0 is the index of monomial abcde
|
||||
3); // 3 is the number of expected factorizations
|
||||
|
||||
|
||||
}
|
||||
|
||||
void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
|
||||
std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0\n";
|
||||
enable_trace("nla_solver");
|
||||
TRACE("nla_solver",);
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
abcde = 5, ac = 6, bde = 7;
|
||||
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_abcde = s.add_named_var(abcde, true, "abcde");
|
||||
lpvar lp_ac = s.add_named_var(ac, true, "ac");
|
||||
lpvar lp_bde = s.add_named_var(bde, true, "bde");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
|
||||
nla.add_monomial(lp_bde, v.size(), v.begin());
|
||||
v.clear();
|
||||
v.push_back(lp_a);v.push_back(lp_b);v.push_back(lp_c);v.push_back(lp_d);v.push_back(lp_e);
|
||||
nla.add_monomial(lp_abcde, v.size(), v.begin());
|
||||
v.clear();
|
||||
v.push_back(lp_a);v.push_back(lp_c);
|
||||
nla.add_monomial(lp_ac, v.size(), v.begin());
|
||||
|
||||
vector<lemma> lv;
|
||||
|
||||
// set abcde = ac * bde
|
||||
// ac = 1 then abcde = bde, but we have abcde < bde
|
||||
s.set_column_value(lp_a, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_b, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_c, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_d, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_e, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_abcde, lp::impq(rational(15)));
|
||||
s.set_column_value(lp_ac, lp::impq(rational(1)));
|
||||
s.set_column_value(lp_bde, lp::impq(rational(16)));
|
||||
|
||||
|
||||
SASSERT(nla.get_core()->test_check(lv) == l_false);
|
||||
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_ac);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_bde);
|
||||
i1.m_term.add_coeff_var(-rational(1), lp_abcde);
|
||||
ineq i2(llc::EQ, lp::lar_term(), rational(0));
|
||||
i2.m_term.add_var(lp_abcde);
|
||||
i2.m_term.add_coeff_var(-rational(1), lp_bde);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
for (const auto& k : lv[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
} else if (k == i2) {
|
||||
found2 = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found0 && (found1 || found2));
|
||||
|
||||
|
||||
}
|
||||
|
||||
void s_set_column_value(lp::lar_solver&s, lpvar j, const rational & v) {
|
||||
s.set_column_value(j, lp::impq(v));
|
||||
}
|
||||
|
||||
void s_set_column_value(lp::lar_solver&s, lpvar j, const lp::impq & v) {
|
||||
s.set_column_value(j, v);
|
||||
}
|
||||
|
||||
void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
|
||||
std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1\n";
|
||||
TRACE("nla_solver",);
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
bde = 7;
|
||||
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_bde = s.add_var(bde, true);
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
|
||||
nla.add_monomial(lp_bde, v.size(), v.begin());
|
||||
|
||||
vector<lemma> lemma;
|
||||
|
||||
s_set_column_value(s, lp_a, rational(1));
|
||||
s_set_column_value(s, lp_b, rational(1));
|
||||
s_set_column_value(s, lp_c, rational(1));
|
||||
s_set_column_value(s, lp_d, rational(1));
|
||||
s_set_column_value(s, lp_e, rational(1));
|
||||
s_set_column_value(s, lp_bde, rational(3));
|
||||
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
SASSERT(lemma[0].size() == 4);
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_b);
|
||||
ineq i1(llc::NE, lp::lar_term(), rational(1));
|
||||
i1.m_term.add_var(lp_d);
|
||||
ineq i2(llc::NE, lp::lar_term(), rational(1));
|
||||
i2.m_term.add_var(lp_e);
|
||||
ineq i3(llc::EQ, lp::lar_term(), rational(1));
|
||||
i3.m_term.add_var(lp_bde);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
bool found3 = false;
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
} else if (k == i2) {
|
||||
found2 = true;
|
||||
} else if (k == i3) {
|
||||
found3 = true;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
SASSERT(found0 && found1 && found2 && found3);
|
||||
|
||||
}
|
||||
void test_basic_lemma_for_mon_neutral_from_factors_to_monomial() {
|
||||
test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0();
|
||||
test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1();
|
||||
}
|
||||
|
||||
|
||||
void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
|
||||
std::cout << "test_basic_lemma_for_mon_zero_from_factors_to_monomial\n";
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
|
||||
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_abcde = s.add_named_var(abcde, true, "abcde");
|
||||
lpvar lp_ac = s.add_named_var(ac, true, "ac");
|
||||
lpvar lp_bde = s.add_named_var(bde, true, "bde");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
lpvar lp_be = s.add_named_var(be, true, "be");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
|
||||
create_abcde(nla,
|
||||
lp_a,
|
||||
lp_b,
|
||||
lp_c,
|
||||
lp_d,
|
||||
lp_e,
|
||||
lp_abcde,
|
||||
lp_ac,
|
||||
lp_bde,
|
||||
lp_acd,
|
||||
lp_be);
|
||||
vector<lemma> lemma;
|
||||
|
||||
// set vars
|
||||
s_set_column_value(s, lp_a, rational(1));
|
||||
s_set_column_value(s, lp_b, rational(0));
|
||||
s_set_column_value(s, lp_c, rational(1));
|
||||
s_set_column_value(s, lp_d, rational(1));
|
||||
s_set_column_value(s, lp_e, rational(1));
|
||||
s_set_column_value(s, lp_abcde, rational(0));
|
||||
s_set_column_value(s, lp_ac, rational(1));
|
||||
s_set_column_value(s, lp_bde, rational(0));
|
||||
s_set_column_value(s, lp_acd, rational(1));
|
||||
s_set_column_value(s, lp_be, rational(1));
|
||||
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(0));
|
||||
i0.m_term.add_var(lp_b);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_be);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found0 && found1);
|
||||
}
|
||||
|
||||
void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
|
||||
std::cout << "test_basic_lemma_for_mon_zero_from_monomial_to_factors\n";
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, c = 2, d = 3, acd = 8;
|
||||
lpvar lp_a = s.add_named_var(a, true, "a");
|
||||
lpvar lp_c = s.add_named_var(c, true, "c");
|
||||
lpvar lp_d = s.add_named_var(d, true, "d");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
|
||||
// create monomial acd
|
||||
unsigned_vector vec;
|
||||
vec.clear();
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
nla.add_monomial(lp_acd, vec.size(), vec.begin());
|
||||
|
||||
vector<lemma> lemma;
|
||||
s_set_column_value(s, lp_a, rational(1));
|
||||
s_set_column_value(s, lp_c, rational(1));
|
||||
s_set_column_value(s, lp_d, rational(1));
|
||||
s_set_column_value(s, lp_acd, rational(0));
|
||||
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::EQ, lp::lar_term(), rational(0));
|
||||
i0.m_term.add_var(lp_a);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_c);
|
||||
ineq i2(llc::EQ, lp::lar_term(), rational(0));
|
||||
i2.m_term.add_var(lp_d);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
} else if (k == i2){
|
||||
found2 = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found0 && found1 && found2);
|
||||
|
||||
}
|
||||
|
||||
void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
|
||||
std::cout << "test_basic_lemma_for_mon_neutral_from_monomial_to_factors\n";
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
|
||||
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_abcde = s.add_named_var(abcde, true, "abcde");
|
||||
lpvar lp_ac = s.add_named_var(ac, true, "ac");
|
||||
lpvar lp_bde = s.add_named_var(bde, true, "bde");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
lpvar lp_be = s.add_named_var(be, true, "be");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
|
||||
create_abcde(nla,
|
||||
lp_a,
|
||||
lp_b,
|
||||
lp_c,
|
||||
lp_d,
|
||||
lp_e,
|
||||
lp_abcde,
|
||||
lp_ac,
|
||||
lp_bde,
|
||||
lp_acd,
|
||||
lp_be);
|
||||
vector<lemma> lemma;
|
||||
|
||||
// set all vars to 1
|
||||
s_set_column_value(s, lp_a, rational(1));
|
||||
s_set_column_value(s, lp_b, rational(1));
|
||||
s_set_column_value(s, lp_c, rational(1));
|
||||
s_set_column_value(s, lp_d, rational(1));
|
||||
s_set_column_value(s, lp_e, rational(1));
|
||||
s_set_column_value(s, lp_abcde, rational(1));
|
||||
s_set_column_value(s, lp_ac, rational(1));
|
||||
s_set_column_value(s, lp_bde, rational(1));
|
||||
s_set_column_value(s, lp_acd, rational(1));
|
||||
s_set_column_value(s, lp_be, rational(1));
|
||||
|
||||
// set bde to 2, b to minus 2
|
||||
s_set_column_value(s, lp_bde, rational(2));
|
||||
s_set_column_value(s, lp_b, - rational(2));
|
||||
// we have bde = -b, therefore d = +-1 and e = +-1
|
||||
s_set_column_value(s, lp_d, rational(3));
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
|
||||
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
ineq i0(llc::EQ, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_d);
|
||||
ineq i1(llc::EQ, lp::lar_term(), -rational(1));
|
||||
i1.m_term.add_var(lp_d);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found0 && found1);
|
||||
}
|
||||
|
||||
void test_basic_sign_lemma() {
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
bde = 7, acd = 8;
|
||||
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_bde = s.add_named_var(bde, true, "bde");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
// create monomial bde
|
||||
vector<unsigned> vec;
|
||||
|
||||
vec.push_back(lp_b);
|
||||
vec.push_back(lp_d);
|
||||
vec.push_back(lp_e);
|
||||
|
||||
nla.add_monomial(lp_bde, vec.size(), vec.begin());
|
||||
vec.clear();
|
||||
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
|
||||
nla.add_monomial(lp_acd, vec.size(), vec.begin());
|
||||
|
||||
// set the values of the factors so it should be bde = -acd according to the model
|
||||
|
||||
// b = -a
|
||||
s_set_column_value(s, lp_a, rational(7));
|
||||
s_set_column_value(s, lp_b, rational(-7));
|
||||
|
||||
// e - c = 0
|
||||
s_set_column_value(s, lp_e, rational(4));
|
||||
s_set_column_value(s, lp_c, rational(4));
|
||||
|
||||
s_set_column_value(s, lp_d, rational(6));
|
||||
|
||||
// make bde != -acd according to the model
|
||||
s_set_column_value(s, lp_bde, rational(5));
|
||||
s_set_column_value(s, lp_acd, rational(3));
|
||||
|
||||
vector<lemma> lemma;
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
|
||||
lp::lar_term t;
|
||||
t.add_var(lp_bde);
|
||||
t.add_var(lp_acd);
|
||||
ineq q(llc::EQ, t, rational(0));
|
||||
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
SASSERT(q == lemma[0].ineqs().back());
|
||||
ineq i0(llc::EQ, lp::lar_term(), rational(0));
|
||||
i0.m_term.add_var(lp_bde);
|
||||
i0.m_term.add_var(lp_acd);
|
||||
bool found = false;
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found);
|
||||
}
|
||||
|
||||
void test_order_lemma_params(bool var_equiv, int sign) {
|
||||
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,
|
||||
k = 18;
|
||||
|
||||
|
||||
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_k = s.add_named_var(k, true, "k");
|
||||
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");
|
||||
lpvar lp_cdij = s.add_named_var(cdij, true, "cdij");
|
||||
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
s_set_column_value(s, j, rational(j + 2));
|
||||
}
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
// 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);
|
||||
int mon_ef = nla.add_monomial(lp_ef, vec.size(), vec.begin());
|
||||
// create monomial ij
|
||||
vec.clear();
|
||||
vec.push_back(lp_i);
|
||||
if (var_equiv)
|
||||
vec.push_back(lp_k);
|
||||
else
|
||||
vec.push_back(lp_j);
|
||||
int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin());
|
||||
|
||||
if (var_equiv) { // make k equivalent to j
|
||||
lp::lar_term t;
|
||||
t.add_var(lp_k);
|
||||
t.add_coeff_var(-rational(1), lp_j);
|
||||
lpvar kj = s.add_term(t.coeffs_as_vector(), -1);
|
||||
s.add_var_bound(kj, llc::LE, rational(0));
|
||||
s.add_var_bound(kj, llc::GE, rational(0));
|
||||
}
|
||||
|
||||
//create monomial (ab)(ef)
|
||||
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());
|
||||
|
||||
//create monomial (cd)(ij)
|
||||
vec.clear();
|
||||
vec.push_back(lp_i);
|
||||
vec.push_back(lp_j);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
auto mon_cdij = nla.add_monomial(lp_cdij, vec.size(), vec.begin());
|
||||
|
||||
// set i == e
|
||||
s_set_column_value(s, lp_e, s.get_column_value(lp_i));
|
||||
// set f == sign*j
|
||||
s_set_column_value(s, lp_f, rational(sign) * s.get_column_value(lp_j));
|
||||
if (var_equiv) {
|
||||
s_set_column_value(s, lp_k, s.get_column_value(lp_j));
|
||||
}
|
||||
// set the values of ab, ef, cd, and ij correctly
|
||||
s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab));
|
||||
s_set_column_value(s, lp_ef, nla.get_core()->mon_value_by_vars(mon_ef));
|
||||
s_set_column_value(s, lp_cd, nla.get_core()->mon_value_by_vars(mon_cd));
|
||||
s_set_column_value(s, lp_ij, nla.get_core()->mon_value_by_vars(mon_ij));
|
||||
|
||||
// set abef = cdij, while it has to be abef < cdij
|
||||
if (sign > 0) {
|
||||
SASSERT(s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
|
||||
// we have ab < cd
|
||||
|
||||
// we need to have ab*ef < cd*ij, so let us make ab*ef > cd*ij
|
||||
s_set_column_value(s, lp_cdij, nla.get_core()->mon_value_by_vars(mon_cdij));
|
||||
s_set_column_value(s, lp_abef, nla.get_core()->mon_value_by_vars(mon_cdij)
|
||||
+ rational(1));
|
||||
|
||||
}
|
||||
else {
|
||||
SASSERT(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
|
||||
// we need to have abef < cdij, so let us make abef < cdij
|
||||
s_set_column_value(s, lp_cdij, nla.get_core()->mon_value_by_vars(mon_cdij));
|
||||
s_set_column_value(s, lp_abef, nla.get_core()->mon_value_by_vars(mon_cdij)
|
||||
+ rational(1));
|
||||
}
|
||||
vector<lemma> lemma;
|
||||
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
// lp::lar_term t;
|
||||
// t.add_coeff_var(lp_bde);
|
||||
// t.add_coeff_var(lp_acd);
|
||||
// ineq q(llc::EQ, t, rational(0));
|
||||
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
// SASSERT(q == lemma.back());
|
||||
// ineq i0(llc::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);
|
||||
}
|
||||
|
||||
void 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");
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
s_set_column_value(s, j, rational((j + 2)*(j + 2)));
|
||||
}
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
// 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(s, lp_e, s.get_column_value(lp_i) + lp::impq(rational(1)));
|
||||
// set f == j + 1
|
||||
s_set_column_value(s, lp_f, s.get_column_value(lp_j) +lp::impq( rational(1)));
|
||||
// set the values of ab, ef, cd, and ij correctly
|
||||
|
||||
s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab));
|
||||
s_set_column_value(s, lp_cd, nla.get_core()->mon_value_by_vars(mon_cd));
|
||||
s_set_column_value(s, lp_ij, nla.get_core()->mon_value_by_vars(mon_ij));
|
||||
|
||||
// set ef = ij while it has to be ef > ij
|
||||
s_set_column_value(s, lp_ef, s.get_column_value(lp_ij));
|
||||
|
||||
vector<lemma> lemma;
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
}
|
||||
|
||||
void test_tangent_lemma_reg() {
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, ab = 10;
|
||||
|
||||
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");
|
||||
int sign = 1;
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
sign *= -1;
|
||||
s_set_column_value(s, j, sign * rational((j + 2) * (j + 2)));
|
||||
}
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
// 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());
|
||||
|
||||
s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
|
||||
vector<lemma> lemma;
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
}
|
||||
|
||||
void test_tangent_lemma_equiv() {
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, k = 2, ab = 10;
|
||||
|
||||
lpvar lp_a = s.add_named_var(a, true, "a");
|
||||
lpvar lp_k = s.add_named_var(k, true, "k");
|
||||
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");
|
||||
int sign = 1;
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
sign *= -1;
|
||||
s_set_column_value(s, j, sign * rational((j + 2) * (j + 2)));
|
||||
}
|
||||
|
||||
// make k == -a
|
||||
lp::lar_term t;
|
||||
t.add_var(lp_k);
|
||||
t.add_var(lp_a);
|
||||
lpvar kj = s.add_term(t.coeffs_as_vector(), -1);
|
||||
s.add_var_bound(kj, llc::LE, rational(0));
|
||||
s.add_var_bound(kj, llc::GE, rational(0));
|
||||
s_set_column_value(s, lp_a, - s.get_column_value(lp_k));
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s);
|
||||
// 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());
|
||||
|
||||
s_set_column_value(s, lp_ab, nla.get_core()->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
|
||||
vector<lemma> lemma;
|
||||
|
||||
SASSERT(nla.get_core()->test_check(lemma) == l_false);
|
||||
nla.get_core()->print_lemma(std::cout);
|
||||
}
|
||||
|
||||
|
||||
void test_tangent_lemma() {
|
||||
test_tangent_lemma_reg();
|
||||
test_tangent_lemma_equiv();
|
||||
}
|
||||
|
||||
void test_order_lemma() {
|
||||
test_order_lemma_params(false, 1);
|
||||
test_order_lemma_params(false, -1);
|
||||
test_order_lemma_params(true, 1);
|
||||
test_order_lemma_params(true, -1);
|
||||
}
|
||||
|
||||
|
||||
} // end of namespace nla
|
||||
|
|
@ -54,797 +54,4 @@ solver::~solver() {
|
|||
dealloc(m_core);
|
||||
}
|
||||
|
||||
void create_abcde(solver & nla,
|
||||
unsigned lp_a,
|
||||
unsigned lp_b,
|
||||
unsigned lp_c,
|
||||
unsigned lp_d,
|
||||
unsigned lp_e,
|
||||
unsigned lp_abcde,
|
||||
unsigned lp_ac,
|
||||
unsigned lp_bde,
|
||||
unsigned lp_acd,
|
||||
unsigned lp_be) {
|
||||
// create monomial abcde
|
||||
vector<unsigned> vec;
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_b);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
vec.push_back(lp_e);
|
||||
|
||||
nla.add_monomial(lp_abcde, vec.size(), vec.begin());
|
||||
|
||||
// create monomial ac
|
||||
vec.clear();
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_c);
|
||||
nla.add_monomial(lp_ac, vec.size(), vec.begin());
|
||||
|
||||
// create monomial bde
|
||||
vec.clear();
|
||||
vec.push_back(lp_b);
|
||||
vec.push_back(lp_d);
|
||||
vec.push_back(lp_e);
|
||||
nla.add_monomial(lp_bde, vec.size(), vec.begin());
|
||||
|
||||
// create monomial acd
|
||||
vec.clear();
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
nla.add_monomial(lp_acd, vec.size(), vec.begin());
|
||||
|
||||
// create monomial be
|
||||
vec.clear();
|
||||
vec.push_back(lp_b);
|
||||
vec.push_back(lp_e);
|
||||
nla.add_monomial(lp_be, vec.size(), vec.begin());
|
||||
}
|
||||
|
||||
void solver::test_factorization() {
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
|
||||
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_abcde = s.add_named_var(abcde, true, "abcde");
|
||||
lpvar lp_ac = s.add_named_var(ac, true, "ac");
|
||||
lpvar lp_bde = s.add_named_var(bde, true, "bde");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
lpvar lp_be = s.add_named_var(be, true, "be");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s, l, p);
|
||||
|
||||
create_abcde(nla,
|
||||
lp_a,
|
||||
lp_b,
|
||||
lp_c,
|
||||
lp_d,
|
||||
lp_e,
|
||||
lp_abcde,
|
||||
lp_ac,
|
||||
lp_bde,
|
||||
lp_acd,
|
||||
lp_be);
|
||||
nla.m_core->register_monomials_in_tables();
|
||||
nla.m_core->print_monomials(std::cout);
|
||||
nla.m_core->test_factorization(1, // 0 is the index of monomial abcde
|
||||
1); // 3 is the number of expected factorizations
|
||||
nla.m_core->test_factorization(0, // 0 is the index of monomial abcde
|
||||
3); // 3 is the number of expected factorizations
|
||||
|
||||
|
||||
}
|
||||
|
||||
void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial() {
|
||||
test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0();
|
||||
test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1();
|
||||
}
|
||||
|
||||
void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
|
||||
std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0\n";
|
||||
enable_trace("nla_solver");
|
||||
TRACE("nla_solver",);
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
abcde = 5, ac = 6, bde = 7;
|
||||
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_abcde = s.add_named_var(abcde, true, "abcde");
|
||||
lpvar lp_ac = s.add_named_var(ac, true, "ac");
|
||||
lpvar lp_bde = s.add_named_var(bde, true, "bde");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s, l, p);
|
||||
svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
|
||||
nla.add_monomial(lp_bde, v.size(), v.begin());
|
||||
v.clear();
|
||||
v.push_back(lp_a);v.push_back(lp_b);v.push_back(lp_c);v.push_back(lp_d);v.push_back(lp_e);
|
||||
nla.add_monomial(lp_abcde, v.size(), v.begin());
|
||||
v.clear();
|
||||
v.push_back(lp_a);v.push_back(lp_c);
|
||||
nla.add_monomial(lp_ac, v.size(), v.begin());
|
||||
|
||||
vector<lemma> lv;
|
||||
|
||||
// set abcde = ac * bde
|
||||
// ac = 1 then abcde = bde, but we have abcde < bde
|
||||
s.set_column_value(lp_a, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_b, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_c, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_d, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_e, lp::impq(rational(4)));
|
||||
s.set_column_value(lp_abcde, lp::impq(rational(15)));
|
||||
s.set_column_value(lp_ac, lp::impq(rational(1)));
|
||||
s.set_column_value(lp_bde, lp::impq(rational(16)));
|
||||
|
||||
|
||||
SASSERT(nla.m_core->test_check(lv) == l_false);
|
||||
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_ac);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_bde);
|
||||
i1.m_term.add_coeff_var(-rational(1), lp_abcde);
|
||||
ineq i2(llc::EQ, lp::lar_term(), rational(0));
|
||||
i2.m_term.add_var(lp_abcde);
|
||||
i2.m_term.add_coeff_var(-rational(1), lp_bde);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
for (const auto& k : lv[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
} else if (k == i2) {
|
||||
found2 = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found0 && (found1 || found2));
|
||||
|
||||
|
||||
}
|
||||
|
||||
void solver::s_set_column_value(lp::lar_solver&s, lpvar j, const rational & v) {
|
||||
s.set_column_value(j, lp::impq(v));
|
||||
}
|
||||
|
||||
void solver::s_set_column_value(lp::lar_solver&s, lpvar j, const lp::impq & v) {
|
||||
s.set_column_value(j, v);
|
||||
}
|
||||
|
||||
void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
|
||||
std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1\n";
|
||||
TRACE("nla_solver",);
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
bde = 7;
|
||||
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_bde = s.add_var(bde, true);
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s, l, p);
|
||||
svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
|
||||
nla.add_monomial(lp_bde, v.size(), v.begin());
|
||||
|
||||
vector<lemma> lemma;
|
||||
|
||||
s_set_column_value(s, lp_a, rational(1));
|
||||
s_set_column_value(s, lp_b, rational(1));
|
||||
s_set_column_value(s, lp_c, rational(1));
|
||||
s_set_column_value(s, lp_d, rational(1));
|
||||
s_set_column_value(s, lp_e, rational(1));
|
||||
s_set_column_value(s, lp_bde, rational(3));
|
||||
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
SASSERT(lemma[0].size() == 4);
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_b);
|
||||
ineq i1(llc::NE, lp::lar_term(), rational(1));
|
||||
i1.m_term.add_var(lp_d);
|
||||
ineq i2(llc::NE, lp::lar_term(), rational(1));
|
||||
i2.m_term.add_var(lp_e);
|
||||
ineq i3(llc::EQ, lp::lar_term(), rational(1));
|
||||
i3.m_term.add_var(lp_bde);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
bool found3 = false;
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
} else if (k == i2) {
|
||||
found2 = true;
|
||||
} else if (k == i3) {
|
||||
found3 = true;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
SASSERT(found0 && found1 && found2 && found3);
|
||||
|
||||
}
|
||||
|
||||
void solver::test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
|
||||
std::cout << "test_basic_lemma_for_mon_zero_from_factors_to_monomial\n";
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
|
||||
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_abcde = s.add_named_var(abcde, true, "abcde");
|
||||
lpvar lp_ac = s.add_named_var(ac, true, "ac");
|
||||
lpvar lp_bde = s.add_named_var(bde, true, "bde");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
lpvar lp_be = s.add_named_var(be, true, "be");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s, l, p);
|
||||
|
||||
create_abcde(nla,
|
||||
lp_a,
|
||||
lp_b,
|
||||
lp_c,
|
||||
lp_d,
|
||||
lp_e,
|
||||
lp_abcde,
|
||||
lp_ac,
|
||||
lp_bde,
|
||||
lp_acd,
|
||||
lp_be);
|
||||
vector<lemma> lemma;
|
||||
|
||||
// set vars
|
||||
s_set_column_value(s, lp_a, rational(1));
|
||||
s_set_column_value(s, lp_b, rational(0));
|
||||
s_set_column_value(s, lp_c, rational(1));
|
||||
s_set_column_value(s, lp_d, rational(1));
|
||||
s_set_column_value(s, lp_e, rational(1));
|
||||
s_set_column_value(s, lp_abcde, rational(0));
|
||||
s_set_column_value(s, lp_ac, rational(1));
|
||||
s_set_column_value(s, lp_bde, rational(0));
|
||||
s_set_column_value(s, lp_acd, rational(1));
|
||||
s_set_column_value(s, lp_be, rational(1));
|
||||
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
|
||||
ineq i0(llc::NE, lp::lar_term(), rational(0));
|
||||
i0.m_term.add_var(lp_b);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_be);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found0 && found1);
|
||||
}
|
||||
|
||||
void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
|
||||
std::cout << "test_basic_lemma_for_mon_zero_from_monomial_to_factors\n";
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, c = 2, d = 3, acd = 8;
|
||||
lpvar lp_a = s.add_named_var(a, true, "a");
|
||||
lpvar lp_c = s.add_named_var(c, true, "c");
|
||||
lpvar lp_d = s.add_named_var(d, true, "d");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s, l, p);
|
||||
|
||||
// create monomial acd
|
||||
unsigned_vector vec;
|
||||
vec.clear();
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
nla.add_monomial(lp_acd, vec.size(), vec.begin());
|
||||
|
||||
vector<lemma> lemma;
|
||||
s_set_column_value(s, lp_a, rational(1));
|
||||
s_set_column_value(s, lp_c, rational(1));
|
||||
s_set_column_value(s, lp_d, rational(1));
|
||||
s_set_column_value(s, lp_acd, rational(0));
|
||||
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
|
||||
ineq i0(llc::EQ, lp::lar_term(), rational(0));
|
||||
i0.m_term.add_var(lp_a);
|
||||
ineq i1(llc::EQ, lp::lar_term(), rational(0));
|
||||
i1.m_term.add_var(lp_c);
|
||||
ineq i2(llc::EQ, lp::lar_term(), rational(0));
|
||||
i2.m_term.add_var(lp_d);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
bool found2 = false;
|
||||
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
} else if (k == i2){
|
||||
found2 = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found0 && found1 && found2);
|
||||
|
||||
}
|
||||
|
||||
void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
|
||||
std::cout << "test_basic_lemma_for_mon_neutral_from_monomial_to_factors\n";
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
abcde = 5, ac = 6, bde = 7, acd = 8, be = 9;
|
||||
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_abcde = s.add_named_var(abcde, true, "abcde");
|
||||
lpvar lp_ac = s.add_named_var(ac, true, "ac");
|
||||
lpvar lp_bde = s.add_named_var(bde, true, "bde");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
lpvar lp_be = s.add_named_var(be, true, "be");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s, l, p);
|
||||
|
||||
create_abcde(nla,
|
||||
lp_a,
|
||||
lp_b,
|
||||
lp_c,
|
||||
lp_d,
|
||||
lp_e,
|
||||
lp_abcde,
|
||||
lp_ac,
|
||||
lp_bde,
|
||||
lp_acd,
|
||||
lp_be);
|
||||
vector<lemma> lemma;
|
||||
|
||||
// set all vars to 1
|
||||
s_set_column_value(s, lp_a, rational(1));
|
||||
s_set_column_value(s, lp_b, rational(1));
|
||||
s_set_column_value(s, lp_c, rational(1));
|
||||
s_set_column_value(s, lp_d, rational(1));
|
||||
s_set_column_value(s, lp_e, rational(1));
|
||||
s_set_column_value(s, lp_abcde, rational(1));
|
||||
s_set_column_value(s, lp_ac, rational(1));
|
||||
s_set_column_value(s, lp_bde, rational(1));
|
||||
s_set_column_value(s, lp_acd, rational(1));
|
||||
s_set_column_value(s, lp_be, rational(1));
|
||||
|
||||
// set bde to 2, b to minus 2
|
||||
s_set_column_value(s, lp_bde, rational(2));
|
||||
s_set_column_value(s, lp_b, - rational(2));
|
||||
// we have bde = -b, therefore d = +-1 and e = +-1
|
||||
s_set_column_value(s, lp_d, rational(3));
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
|
||||
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
ineq i0(llc::EQ, lp::lar_term(), rational(1));
|
||||
i0.m_term.add_var(lp_d);
|
||||
ineq i1(llc::EQ, lp::lar_term(), -rational(1));
|
||||
i1.m_term.add_var(lp_d);
|
||||
bool found0 = false;
|
||||
bool found1 = false;
|
||||
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found0 = true;
|
||||
} else if (k == i1) {
|
||||
found1 = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found0 && found1);
|
||||
}
|
||||
|
||||
void solver::test_basic_sign_lemma() {
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, c = 2, d = 3, e = 4,
|
||||
bde = 7, acd = 8;
|
||||
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_bde = s.add_named_var(bde, true, "bde");
|
||||
lpvar lp_acd = s.add_named_var(acd, true, "acd");
|
||||
|
||||
reslimit l;
|
||||
params_ref p;
|
||||
solver nla(s, l, p);
|
||||
// create monomial bde
|
||||
vector<unsigned> vec;
|
||||
|
||||
vec.push_back(lp_b);
|
||||
vec.push_back(lp_d);
|
||||
vec.push_back(lp_e);
|
||||
|
||||
nla.add_monomial(lp_bde, vec.size(), vec.begin());
|
||||
vec.clear();
|
||||
|
||||
vec.push_back(lp_a);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
|
||||
nla.add_monomial(lp_acd, vec.size(), vec.begin());
|
||||
|
||||
// set the values of the factors so it should be bde = -acd according to the model
|
||||
|
||||
// b = -a
|
||||
s_set_column_value(s, lp_a, rational(7));
|
||||
s_set_column_value(s, lp_b, rational(-7));
|
||||
|
||||
// e - c = 0
|
||||
s_set_column_value(s, lp_e, rational(4));
|
||||
s_set_column_value(s, lp_c, rational(4));
|
||||
|
||||
s_set_column_value(s, lp_d, rational(6));
|
||||
|
||||
// make bde != -acd according to the model
|
||||
s_set_column_value(s, lp_bde, rational(5));
|
||||
s_set_column_value(s, lp_acd, rational(3));
|
||||
|
||||
vector<lemma> lemma;
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
|
||||
lp::lar_term t;
|
||||
t.add_var(lp_bde);
|
||||
t.add_var(lp_acd);
|
||||
ineq q(llc::EQ, t, rational(0));
|
||||
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
SASSERT(q == lemma[0].ineqs().back());
|
||||
ineq i0(llc::EQ, lp::lar_term(), rational(0));
|
||||
i0.m_term.add_var(lp_bde);
|
||||
i0.m_term.add_var(lp_acd);
|
||||
bool found = false;
|
||||
for (const auto& k : lemma[0].ineqs()){
|
||||
if (k == i0) {
|
||||
found = true;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(found);
|
||||
}
|
||||
|
||||
void solver::test_order_lemma_params(bool var_equiv, int sign) {
|
||||
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,
|
||||
k = 18;
|
||||
|
||||
|
||||
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_k = s.add_named_var(k, true, "k");
|
||||
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");
|
||||
lpvar lp_cdij = s.add_named_var(cdij, true, "cdij");
|
||||
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
s_set_column_value(s, j, rational(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);
|
||||
int mon_ef = nla.add_monomial(lp_ef, vec.size(), vec.begin());
|
||||
// create monomial ij
|
||||
vec.clear();
|
||||
vec.push_back(lp_i);
|
||||
if (var_equiv)
|
||||
vec.push_back(lp_k);
|
||||
else
|
||||
vec.push_back(lp_j);
|
||||
int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin());
|
||||
|
||||
if (var_equiv) { // make k equivalent to j
|
||||
lp::lar_term t;
|
||||
t.add_var(lp_k);
|
||||
t.add_coeff_var(-rational(1), lp_j);
|
||||
lpvar kj = s.add_term(t.coeffs_as_vector(), -1);
|
||||
s.add_var_bound(kj, llc::LE, rational(0));
|
||||
s.add_var_bound(kj, llc::GE, rational(0));
|
||||
}
|
||||
|
||||
//create monomial (ab)(ef)
|
||||
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());
|
||||
|
||||
//create monomial (cd)(ij)
|
||||
vec.clear();
|
||||
vec.push_back(lp_i);
|
||||
vec.push_back(lp_j);
|
||||
vec.push_back(lp_c);
|
||||
vec.push_back(lp_d);
|
||||
auto mon_cdij = nla.add_monomial(lp_cdij, vec.size(), vec.begin());
|
||||
|
||||
// set i == e
|
||||
s_set_column_value(s, lp_e, s.get_column_value(lp_i));
|
||||
// set f == sign*j
|
||||
s_set_column_value(s, lp_f, rational(sign) * s.get_column_value(lp_j));
|
||||
if (var_equiv) {
|
||||
s_set_column_value(s, lp_k, s.get_column_value(lp_j));
|
||||
}
|
||||
// set the values of ab, ef, cd, and ij correctly
|
||||
s_set_column_value(s, lp_ab, nla.m_core->mon_value_by_vars(mon_ab));
|
||||
s_set_column_value(s, lp_ef, nla.m_core->mon_value_by_vars(mon_ef));
|
||||
s_set_column_value(s, lp_cd, nla.m_core->mon_value_by_vars(mon_cd));
|
||||
s_set_column_value(s, lp_ij, nla.m_core->mon_value_by_vars(mon_ij));
|
||||
|
||||
// set abef = cdij, while it has to be abef < cdij
|
||||
if (sign > 0) {
|
||||
SASSERT(s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
|
||||
// we have ab < cd
|
||||
|
||||
// we need to have ab*ef < cd*ij, so let us make ab*ef > cd*ij
|
||||
s_set_column_value(s, lp_cdij, nla.m_core->mon_value_by_vars(mon_cdij));
|
||||
s_set_column_value(s, lp_abef, nla.m_core->mon_value_by_vars(mon_cdij)
|
||||
+ rational(1));
|
||||
|
||||
}
|
||||
else {
|
||||
SASSERT(-s.get_column_value(lp_ab) < s.get_column_value(lp_cd));
|
||||
// we need to have abef < cdij, so let us make abef < cdij
|
||||
s_set_column_value(s, lp_cdij, nla.m_core->mon_value_by_vars(mon_cdij));
|
||||
s_set_column_value(s, lp_abef, nla.m_core->mon_value_by_vars(mon_cdij)
|
||||
+ rational(1));
|
||||
}
|
||||
vector<lemma> lemma;
|
||||
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
// lp::lar_term t;
|
||||
// t.add_coeff_var(lp_bde);
|
||||
// t.add_coeff_var(lp_acd);
|
||||
// ineq q(llc::EQ, t, rational(0));
|
||||
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
// SASSERT(q == lemma.back());
|
||||
// ineq i0(llc::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);
|
||||
}
|
||||
|
||||
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");
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
s_set_column_value(s, 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(s, lp_e, s.get_column_value(lp_i) + lp::impq(rational(1)));
|
||||
// set f == j + 1
|
||||
s_set_column_value(s, lp_f, s.get_column_value(lp_j) +lp::impq( rational(1)));
|
||||
// set the values of ab, ef, cd, and ij correctly
|
||||
|
||||
s_set_column_value(s, lp_ab, nla.m_core->mon_value_by_vars(mon_ab));
|
||||
s_set_column_value(s, lp_cd, nla.m_core->mon_value_by_vars(mon_cd));
|
||||
s_set_column_value(s, lp_ij, nla.m_core->mon_value_by_vars(mon_ij));
|
||||
|
||||
// set ef = ij while it has to be ef > ij
|
||||
s_set_column_value(s, lp_ef, s.get_column_value(lp_ij));
|
||||
|
||||
vector<lemma> lemma;
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
}
|
||||
|
||||
void solver::test_tangent_lemma_reg() {
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, ab = 10;
|
||||
|
||||
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");
|
||||
int sign = 1;
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
sign *= -1;
|
||||
s_set_column_value(s, j, sign * 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());
|
||||
|
||||
s_set_column_value(s, lp_ab, nla.m_core->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
|
||||
vector<lemma> lemma;
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
}
|
||||
|
||||
void solver::test_tangent_lemma_equiv() {
|
||||
enable_trace("nla_solver");
|
||||
lp::lar_solver s;
|
||||
unsigned a = 0, b = 1, k = 2, ab = 10;
|
||||
|
||||
lpvar lp_a = s.add_named_var(a, true, "a");
|
||||
lpvar lp_k = s.add_named_var(k, true, "k");
|
||||
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");
|
||||
int sign = 1;
|
||||
for (unsigned j = 0; j < s.number_of_vars(); j++) {
|
||||
sign *= -1;
|
||||
s_set_column_value(s, j, sign * rational((j + 2) * (j + 2)));
|
||||
}
|
||||
|
||||
// make k == -a
|
||||
lp::lar_term t;
|
||||
t.add_var(lp_k);
|
||||
t.add_var(lp_a);
|
||||
lpvar kj = s.add_term(t.coeffs_as_vector(), -1);
|
||||
s.add_var_bound(kj, llc::LE, rational(0));
|
||||
s.add_var_bound(kj, llc::GE, rational(0));
|
||||
s_set_column_value(s, lp_a, - s.get_column_value(lp_k));
|
||||
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());
|
||||
|
||||
s_set_column_value(s, lp_ab, nla.m_core->mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
|
||||
vector<lemma> lemma;
|
||||
|
||||
SASSERT(nla.m_core->test_check(lemma) == l_false);
|
||||
nla.m_core->print_lemma(std::cout);
|
||||
}
|
||||
|
||||
|
||||
void solver::test_tangent_lemma() {
|
||||
test_tangent_lemma_reg();
|
||||
test_tangent_lemma_equiv();
|
||||
}
|
||||
|
||||
void solver::test_order_lemma() {
|
||||
test_order_lemma_params(false, 1);
|
||||
test_order_lemma_params(false, -1);
|
||||
test_order_lemma_params(true, 1);
|
||||
test_order_lemma_params(true, -1);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -37,25 +37,10 @@ public:
|
|||
|
||||
solver(lp::lar_solver& s, reslimit& lim, params_ref const& p);
|
||||
~solver();
|
||||
inline core * get_core() { return m_core; }
|
||||
void push();
|
||||
void pop(unsigned scopes);
|
||||
bool need_check();
|
||||
lbool check(vector<lemma>&);
|
||||
static void test_factorization();
|
||||
static void test_basic_sign_lemma();
|
||||
static void test_basic_lemma_for_mon_zero_from_monomial_to_factors();
|
||||
static void test_basic_lemma_for_mon_zero_from_factors_to_monomial();
|
||||
static void test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
|
||||
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_1();
|
||||
static void test_order_lemma();
|
||||
static void test_order_lemma_params(bool, int sign);
|
||||
static void test_monotone_lemma();
|
||||
static void test_tangent_lemma();
|
||||
static void test_tangent_lemma_reg();
|
||||
static void test_tangent_lemma_equiv();
|
||||
static void s_set_column_value(lp::lar_solver&, unsigned, const rational &);
|
||||
static void s_set_column_value(lp::lar_solver&, unsigned, const lp::impq &);
|
||||
};
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue