mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix the test build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-03 10:06:35 -07:00
parent f4e7002ea3
commit 6f40ee2f94
2 changed files with 15 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/test/CMakeLists.txt
View file

@ -124,6 +124,7 @@ add_executable(test-z3
var_subst.cpp var_subst.cpp
vector.cpp vector.cpp
lp/lp.cpp lp/lp.cpp
lp/nla_solver_test.cpp
${z3_test_extra_object_files} ${z3_test_extra_object_files}
) )
z3_add_install_tactic_rule(${z3_test_deps}) z3_add_install_tactic_rule(${z3_test_deps})

28
src/test/interval.cpp
View file

@ -211,20 +211,20 @@ char const * get_next_file_name() {
} }
static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term, static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term,
interval const & a, interval const & b, interval const & r, interval_deps const & deps) { interval const & a, interval const & b, interval const & r, interval_deps_combine_rule const & deps) {
{ {
std::ofstream out(get_next_file_name()); std::ofstream out(get_next_file_name());
display_preamble(out); display_preamble(out);
assert_hyp(out, nm, "a", a, dep_in_lower1(deps.m_lower_deps), dep_in_upper1(deps.m_lower_deps)); assert_hyp(out, nm, "a", a, dep_in_lower1(deps.m_lower_combine), dep_in_upper1(deps.m_lower_combine));
assert_hyp(out, nm, "b", b, dep_in_lower2(deps.m_lower_deps), dep_in_upper2(deps.m_lower_deps)); assert_hyp(out, nm, "b", b, dep_in_lower2(deps.m_lower_combine), dep_in_upper2(deps.m_lower_combine));
assert_conj(out, nm, result_term, r, true, false); assert_conj(out, nm, result_term, r, true, false);
out << "(check-sat)\n"; out << "(check-sat)\n";
} }
{ {
std::ofstream out(get_next_file_name()); std::ofstream out(get_next_file_name());
display_preamble(out); display_preamble(out);
assert_hyp(out, nm, "a", a, dep_in_lower1(deps.m_upper_deps), dep_in_upper1(deps.m_upper_deps)); assert_hyp(out, nm, "a", a, dep_in_lower1(deps.m_upper_combine), dep_in_upper1(deps.m_upper_combine));
assert_hyp(out, nm, "b", b, dep_in_lower2(deps.m_upper_deps), dep_in_upper2(deps.m_upper_deps)); assert_hyp(out, nm, "b", b, dep_in_lower2(deps.m_upper_combine), dep_in_upper2(deps.m_upper_combine));
assert_conj(out, nm, result_term, r, false, true); assert_conj(out, nm, result_term, r, false, true);
out << "(check-sat)\n"; out << "(check-sat)\n";
} }
@ -240,7 +240,7 @@ static void tst_ ## NAME(unsigned N, unsigned magnitude) { \
for (unsigned i = 0; i < N; i++) { \ for (unsigned i = 0; i < N; i++) { \
mk_random_interval(im, a, magnitude); \ mk_random_interval(im, a, magnitude); \
mk_random_interval(im, b, magnitude); \ mk_random_interval(im, b, magnitude); \
interval_deps deps; \ interval_deps_combine_rule deps; \
im.NAME(a, b, r, deps); \ im.NAME(a, b, r, deps); \
\ \
display_lemmas(nm, RES_TERM, a, b, r, deps); \ display_lemmas(nm, RES_TERM, a, b, r, deps); \
@ -260,7 +260,7 @@ static void tst_neg(unsigned N, unsigned magnitude) {
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(im, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps_combine_rule deps;
im.neg(a, r, deps); im.neg(a, r, deps);
display_lemmas(nm, "(- a)", a, b, r, deps); display_lemmas(nm, "(- a)", a, b, r, deps);
} }
@ -275,7 +275,7 @@ static void tst_pw_2(unsigned N, unsigned magnitude) {
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(im, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps_combine_rule deps;
im.power(a, 2, r, deps); im.power(a, 2, r, deps);
display_lemmas(nm, "(* a a)", a, b, r, deps); display_lemmas(nm, "(* a a)", a, b, r, deps);
} }
@ -290,7 +290,7 @@ static void tst_pw_3(unsigned N, unsigned magnitude) {
for (unsigned i = 0; i < N; i++) { for (unsigned i = 0; i < N; i++) {
mk_random_interval(im, a, magnitude); mk_random_interval(im, a, magnitude);
interval_deps deps; interval_deps_combine_rule deps;
im.power(a, 3, r, deps); im.power(a, 3, r, deps);
display_lemmas(nm, "(* a a a)", a, b, r, deps); display_lemmas(nm, "(* a a a)", a, b, r, deps);
} }
@ -311,7 +311,7 @@ static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
mk_random_interval(im, a, magnitude); mk_random_interval(im, a, magnitude);
if (!im.lower_is_neg(a)) { if (!im.lower_is_neg(a)) {
i++; i++;
interval_deps deps; interval_deps_combine_rule deps;
im.nth_root(a, 2, p, r, deps); im.nth_root(a, 2, p, r, deps);
display_lemmas(nm, "(^ a (/ 1.0 2.0))", a, b, r, deps); display_lemmas(nm, "(^ a (/ 1.0 2.0))", a, b, r, deps);
} }
@ -332,7 +332,7 @@ static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) {
while (i < N) { while (i < N) {
mk_random_interval(im, a, magnitude); mk_random_interval(im, a, magnitude);
i++; i++;
interval_deps deps; interval_deps_combine_rule deps;
im.nth_root(a, 3, p, r, deps); im.nth_root(a, 3, p, r, deps);
display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, r, deps); display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, r, deps);
} }
@ -351,7 +351,7 @@ static void tst_inv(unsigned N, unsigned magnitude) {
if (!im.contains_zero(a)) if (!im.contains_zero(a))
break; break;
} }
interval_deps deps; interval_deps_combine_rule deps;
im.inv(a, r, deps); im.inv(a, r, deps);
display_lemmas(nm, "(/ 1 a)", a, b, r, deps); display_lemmas(nm, "(/ 1 a)", a, b, r, deps);
} }
@ -371,7 +371,7 @@ static void tst_div(unsigned N, unsigned magnitude) {
if (!im.contains_zero(b)) if (!im.contains_zero(b))
break; break;
} }
interval_deps deps; interval_deps_combine_rule deps;
im.div(a, b, r, deps); im.div(a, b, r, deps);
display_lemmas(nm, "(/ a b)", a, b, r, deps); display_lemmas(nm, "(/ a b)", a, b, r, deps);
} }
@ -406,7 +406,7 @@ static void tst_float() {
std::cout << "\n"; std::cout << "\n";
im.display(std::cout, b); im.display(std::cout, b);
std::cout << "\n"; std::cout << "\n";
interval_deps deps; interval_deps_combine_rule deps;
im.add(a, b, c, deps); im.add(a, b, c, deps);
im.display(std::cout, c); im.display(std::cout, c);
std::cout << "\n"; std::cout << "\n";