mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix the build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-22 13:01:20 -07:00
parent b01fc9816f
commit dfb862db7c
3 changed files with 50 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -84,33 +84,33 @@ void test_cn() {
);
enable_trace("nla_cn");
enable_trace("nla_cn_details");
nex_var* a = cn.mk_var(0);
nex_var* b = cn.mk_var(1);
nex_var* c = cn.mk_var(2);
nex_var* d = cn.mk_var(3);
nex_var* e = cn.mk_var(4);
nex_var* g = cn.mk_var(6);
nex* min_1 = cn.mk_scalar(rational(-1));
nex_var* a = cn.get_nex_creator().mk_var(0);
nex_var* b = cn.get_nex_creator().mk_var(1);
nex_var* c = cn.get_nex_creator().mk_var(2);
nex_var* d = cn.get_nex_creator().mk_var(3);
nex_var* e = cn.get_nex_creator().mk_var(4);
nex_var* g = cn.get_nex_creator().mk_var(6);
nex* min_1 = cn.get_nex_creator().mk_scalar(rational(-1));
// test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c);
nex* bcd = cn.mk_mul(b, c, d);
nex_mul* bcg = cn.mk_mul(b, c, g);
nex* bcd = cn.get_nex_creator().mk_mul(b, c, d);
nex_mul* bcg = cn.get_nex_creator().mk_mul(b, c, g);
bcg->add_child(min_1);
nex_sum* t = cn.mk_sum(bcd, bcg);
nex_sum* t = cn.get_nex_creator().mk_sum(bcd, bcg);
test_cn_on_expr(t, cn);
nex* aad = cn.mk_mul(a, a, d);
nex* abcd = cn.mk_mul(a, b, c, d);
nex* aaccd = cn.mk_mul(a, a, c, c, d);
nex* add = cn.mk_mul(a, d, d);
nex* eae = cn.mk_mul(e, a, e);
nex* eac = cn.mk_mul(e, a, c);
nex* ed = cn.mk_mul(e, d);
nex* _6aad = cn.mk_mul(cn.mk_scalar(rational(6)), a, a, d);
nex* aad = cn.get_nex_creator().mk_mul(a, a, d);
nex* abcd = cn.get_nex_creator().mk_mul(a, b, c, d);
nex* aaccd = cn.get_nex_creator().mk_mul(a, a, c, c, d);
nex* add = cn.get_nex_creator().mk_mul(a, d, d);
nex* eae = cn.get_nex_creator().mk_mul(e, a, e);
nex* eac = cn.get_nex_creator().mk_mul(e, a, c);
nex* ed = cn.get_nex_creator().mk_mul(e, d);
nex* _6aad = cn.get_nex_creator().mk_mul(cn.get_nex_creator().mk_scalar(rational(6)), a, a, d);
#ifdef Z3DEBUG
nex * clone = cn.clone(cn.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed));
nex * clone = cn.clone(cn.get_nex_creator().mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed));
TRACE("nla_cn", tout << "clone = " << *clone << "\n";);
#endif
// test_cn_on_expr(cn.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn);
test_cn_on_expr(cn.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed), cn);
// test_cn_on_expr(cn.get_nex_creator().mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn);
test_cn_on_expr(cn.get_nex_creator().mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed), cn);
// TRACE("nla_cn", tout << "done\n";);
// test_cn_on_expr(a*b*d + a*b*c + c*b*d + a*c*d);
// TRACE("nla_cn", tout << "done\n";);

56
src/test/lp/nla_solver_test.cpp
View file

@ -38,33 +38,33 @@ void create_abcde(solver & nla,
vec.push_back(lp_d);
vec.push_back(lp_e);
nla.add_monomial(lp_abcde, vec.size(), vec.begin());
nla.add_monic(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());
nla.add_monic(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());
nla.add_monic(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());
nla.add_monic(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());
nla.add_monic(lp_be, vec.size(), vec.begin());
}
@ -88,13 +88,13 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
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());
nla.add_monic(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());
nla.add_monic(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());
nla.add_monic(lp_ac, v.size(), v.begin());
vector<lemma> lv;
@ -165,7 +165,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
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());
nla.add_monic(lp_bde, v.size(), v.begin());
vector<lemma> lemma;
@ -301,7 +301,7 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
vec.push_back(lp_a);
vec.push_back(lp_c);
vec.push_back(lp_d);
nla.add_monomial(lp_acd, vec.size(), vec.begin());
nla.add_monic(lp_acd, vec.size(), vec.begin());
vector<lemma> lemma;
s_set_column_value(s, lp_a, rational(1));
@ -436,19 +436,19 @@ void test_horner() {
solver nla(s);
vector<lpvar> v;
v.push_back(a); v.push_back(b);
nla.add_monomial(lp_ab, v.size(), v.begin());
nla.add_monic(lp_ab, v.size(), v.begin());
v.clear();
v.push_back(c); v.push_back(e);
nla.add_monomial(lp_ce, v.size(), v.begin());
nla.add_monic(lp_ce, v.size(), v.begin());
v.clear();
v.push_back(b); v.push_back(d);
nla.add_monomial(lp_bd, v.size(), v.begin());
nla.add_monic(lp_bd, v.size(), v.begin());
v.clear();
v.push_back(a); v.push_back(c);
nla.add_monomial(lp_ac, v.size(), v.begin());
nla.add_monic(lp_ac, v.size(), v.begin());
v.clear();
*/
@ -478,14 +478,14 @@ void test_basic_sign_lemma() {
vec.push_back(lp_d);
vec.push_back(lp_e);
nla.add_monomial(lp_bde, vec.size(), vec.begin());
nla.add_monic(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());
nla.add_monic(lp_acd, vec.size(), vec.begin());
// set the values of the factors so it should be bde = -acd according to the model
@ -550,17 +550,17 @@ void test_order_lemma_params(bool var_equiv, int sign) {
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());
int mon_ab = nla.add_monic(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());
int mon_cd = nla.add_monic(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());
int mon_ef = nla.add_monic(lp_ef, vec.size(), vec.begin());
// create monomial ij
vec.clear();
vec.push_back(lp_i);
@ -568,7 +568,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
vec.push_back(lp_k);
else
vec.push_back(lp_j);
int mon_ij = nla.add_monomial(lp_ij, vec.size(), vec.begin());
int mon_ij = nla.add_monic(lp_ij, vec.size(), vec.begin());
if (var_equiv) { // make k equivalent to j
lp::lar_term t;
@ -585,7 +585,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
vec.push_back(lp_a);
vec.push_back(lp_b);
vec.push_back(lp_f);
nla.add_monomial(lp_abef, vec.size(), vec.begin());
nla.add_monic(lp_abef, vec.size(), vec.begin());
//create monomial (cd)(ij)
vec.clear();
@ -593,7 +593,7 @@ void test_order_lemma_params(bool var_equiv, int sign) {
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());
auto mon_cdij = nla.add_monic(lp_cdij, vec.size(), vec.begin());
// set i == e
s_set_column_value(s, lp_e, s.get_column_value(lp_i));
@ -681,22 +681,22 @@ void test_monotone_lemma() {
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());
int mon_ab = nla.add_monic(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());
int mon_cd = nla.add_monic(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());
nla.add_monic(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());
int mon_ij = nla.add_monic(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)));
@ -745,7 +745,7 @@ void test_tangent_lemma_reg() {
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());
int mon_ab = nla.add_monic(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;
@ -791,7 +791,7 @@ void test_tangent_lemma_equiv() {
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());
int mon_ab = nla.add_monic(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;