From 1a59123819fa9da1e5ff61385a1107948c6ed1a3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 28 Jun 2017 12:49:10 +0100 Subject: [PATCH 01/36] Fixed x86/x64 issues in theory_str --- src/smt/theory_str.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 523e087f2..0671c319c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -21,14 +21,13 @@ #include"ast_pp.h" #include"ast_ll_pp.h" #include -#include #include #include"theory_seq_empty.h" #include"theory_arith.h" #include"ast_util.h" namespace smt { - + theory_str::theory_str(ast_manager & m, theory_str_params const & params): theory(m.mk_family_id("seq")), m_params(params), @@ -99,7 +98,7 @@ namespace smt { if (defaultCharset) { // valid C strings can't contain the null byte ('\0') charSetSize = 255; - char_set.resize(256, 0); + char_set.resize(256, 0); int idx = 0; // small letters for (int i = 97; i < 123; i++) { @@ -9217,8 +9216,8 @@ namespace smt { coverAll = get_next_val_encode(val_range_map[lastestValIndi], base); } - long long l = (tries) * distance; - long long h = l; + size_t l = (tries) * distance; + size_t h = l; for (int i = 0; i < distance; i++) { if (coverAll) break; @@ -9239,10 +9238,10 @@ namespace smt { ); // ---------------------------------------------------------------------------------------- - + expr_ref_vector orList(m), andList(m); - for (long long i = l; i < h; i++) { + for (size_t i = l; i < h; i++) { orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); if (m_params.m_AggressiveValueTesting) { literal lit = mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()), false); From 1f29cebd4df633a4fea50a29b80aa756ecd0e8e7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 28 Jun 2017 14:44:41 +0000 Subject: [PATCH 02/36] Fixed backwards compatibility problem in maxsat example --- examples/maxsat/maxsat.c | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c index 45325311e..a312e79ad 100644 --- a/examples/maxsat/maxsat.c +++ b/examples/maxsat/maxsat.c @@ -348,7 +348,15 @@ void assert_at_most_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits, un */ void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits) { - assert_at_most_k(ctx, s, n, lits, 1); + assert_at_most_k(ctx, s, n, lits, 1); +} + + +Z3_solver mk_solver(Z3_context ctx) +{ + Z3_solver r = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, r); + return r; } /** @@ -357,8 +365,7 @@ void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits) void tst_at_most_one() { Z3_context ctx = mk_context(); - Z3_solver s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); + Z3_solver s = mk_solver(ctx); Z3_ast k1 = mk_bool_var(ctx, "k1"); Z3_ast k2 = mk_bool_var(ctx, "k2"); Z3_ast k3 = mk_bool_var(ctx, "k3"); @@ -460,7 +467,7 @@ int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast * printf("unsat\n"); return num_soft_cnstrs - k - 1; } - m = Z3_solver_get_model(ctx, s); + m = Z3_solver_get_model(ctx, s); Z3_model_inc_ref(ctx, m); num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars); Z3_model_dec_ref(ctx, m); @@ -523,7 +530,7 @@ int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs, unsigned j; // check whether assumption[i] is in the core or not for (j = 0; j < core_size; j++) { - if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) + if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) break; } if (j < core_size) { @@ -607,8 +614,7 @@ int smtlib_maxsat(char * file_name, int approach) Z3_ast * hard_cnstrs, * soft_cnstrs; unsigned result = 0; ctx = mk_context(); - s = Z3_mk_solver(ctx); - Z3_solver_inc_ref(ctx, s); + s = mk_solver(ctx); Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0); hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs); soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs); From c44c8284bd21472d66dc04c56cc99b83bb10e88e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Jun 2017 18:10:36 -0700 Subject: [PATCH 03/36] use worklist algorithm to avoid stack overflow #1125 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 116 ++++++++++++++++++++++++++++------------- src/smt/theory_seq.h | 3 ++ 2 files changed, 83 insertions(+), 36 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4dfff21c2..1c293ad8d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2863,77 +2863,121 @@ bool theory_seq::canonize(expr_ref_vector const& es, expr_ref_vector& result, de return change; } - -expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { +expr_ref theory_seq::expand(expr* e, dependency*& eqs) { + unsigned sz = m_expand_todo.size(); + m_expand_todo.push_back(e); + expr_ref result(m); + while (m_expand_todo.size() != sz) { + expr* e = m_expand_todo.back(); + result = expand1(e, eqs); + if (result.get()) m_expand_todo.pop_back(); + } + return result; +} + +expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ expr_ref result(m); - dependency* deps = 0; expr_dep ed; - if (m_rep.find_cache(e0, ed)) { + if (m_rep.find_cache(e, ed)) { eqs = m_dm.mk_join(eqs, ed.second); result = ed.first; - return result; } + else { + m_expand_todo.push_back(e); + } + return result; +} +expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { + expr_ref result(m); + dependency* deps = 0; + result = try_expand(e0, deps); + if (result) return result; expr* e = m_rep.find(e0, deps); expr* e1, *e2, *e3; + expr_ref arg1(m), arg2(m); context& ctx = get_context(); if (m_util.str.is_concat(e, e1, e2)) { - result = mk_concat(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = mk_concat(arg1, arg2); } else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { result = e; } else if (m_util.str.is_prefix(e, e1, e2)) { - result = m_util.str.mk_prefix(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_prefix(arg1, arg2); } else if (m_util.str.is_suffix(e, e1, e2)) { - result = m_util.str.mk_suffix(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_suffix(arg1, arg2); } else if (m_util.str.is_contains(e, e1, e2)) { - result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_contains(arg1, arg2); } else if (m_util.str.is_unit(e, e1)) { - result = m_util.str.mk_unit(expand(e1, deps)); + arg1 = try_expand(e1, deps); + if (!arg1) return result; + result = m_util.str.mk_unit(arg1); } else if (m_util.str.is_index(e, e1, e2)) { - result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), m_autil.mk_int(0)); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_index(arg1, arg2, m_autil.mk_int(0)); } else if (m_util.str.is_index(e, e1, e2, e3)) { - result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), e3); + arg1 = try_expand(e1, deps); + arg2 = try_expand(e2, deps); + if (!arg1 || !arg2) return result; + result = m_util.str.mk_index(arg1, arg2, e3); } else if (m.is_ite(e, e1, e2, e3)) { if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e2)->get_root()) { - result = expand(e2, deps); + result = try_expand(e2, deps); + if (!result) return result; add_dependency(deps, ctx.get_enode(e), ctx.get_enode(e2)); } else if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e3)->get_root()) { - result = expand(e3, deps); + result = try_expand(e3, deps); + if (!result) return result; add_dependency(deps, ctx.get_enode(e), ctx.get_enode(e3)); } else { - literal lit(mk_literal(e1)); + literal lit(mk_literal(e1)); #if 0 - expr_ref sk_ite = mk_sk_ite(e1, e2, e3); - add_axiom(~lit, mk_eq(e2, sk_ite, false)); - add_axiom( lit, mk_eq(e3, sk_ite, false)); - result = sk_ite; - + expr_ref sk_ite = mk_sk_ite(e1, e2, e3); + add_axiom(~lit, mk_eq(e2, sk_ite, false)); + add_axiom( lit, mk_eq(e3, sk_ite, false)); + result = sk_ite; + #else - switch (ctx.get_assignment(lit)) { - case l_true: - deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); - result = expand(e2, deps); - break; - case l_false: - deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit))); - result = expand(e3, deps); - break; - case l_undef: - result = e; - m_reset_cache = true; - TRACE("seq", tout << "undef: " << result << "\n"; - tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); - break; - } + switch (ctx.get_assignment(lit)) { + case l_true: + deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); + result = try_expand(e2, deps); + if (!result) return result; + break; + case l_false: + deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit))); + result = try_expand(e3, deps); + if (!result) return result; + break; + case l_undef: + result = e; + m_reset_cache = true; + TRACE("seq", tout << "undef: " << result << "\n"; + tout << lit << "@ level: " << ctx.get_scope_level() << "\n";); + break; + } #endif } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 5fd31e2ca..f7212e608 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -462,7 +462,10 @@ namespace smt { expr_ref canonize(expr* e, dependency*& eqs); bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs); bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs); + ptr_vector m_expand_todo; expr_ref expand(expr* e, dependency*& eqs); + expr_ref expand1(expr* e, dependency*& eqs); + expr_ref try_expand(expr* e, dependency*& eqs); void add_dependency(dependency*& dep, enode* a, enode* b); void get_concat(expr* e, ptr_vector& concats); From be4b0ffe69282f52faaf23cf4ed1a239c25d1118 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Jun 2017 19:36:38 -0700 Subject: [PATCH 04/36] fix unsoundness bug instroduced when fixing #1125 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 1c293ad8d..ea53f1342 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2879,7 +2879,9 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ expr_ref result(m); expr_dep ed; if (m_rep.find_cache(e, ed)) { - eqs = m_dm.mk_join(eqs, ed.second); + if (e != ed.first) { + eqs = m_dm.mk_join(eqs, ed.second); + } result = ed.first; } else { @@ -2889,9 +2891,9 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ } expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) { expr_ref result(m); - dependency* deps = 0; - result = try_expand(e0, deps); + result = try_expand(e0, eqs); if (result) return result; + dependency* deps = 0; expr* e = m_rep.find(e0, deps); expr* e1, *e2, *e3; expr_ref arg1(m), arg2(m); From 8310fed528622a3a91f65d223e2165b6a46dc234 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 25 Jun 2017 22:36:03 +0100 Subject: [PATCH 05/36] [TravisCI] Implement TravisCI build and testing infrastructure for Linux The Linux builds rely on Docker (using Ubuntu 16.04LTS and Ubuntu 14.04LTS) to build and test Z3 so that builds are easily reproducible. A build status button has been added to `README.md` so that it is easy to see the current build status. More documentation can be found in `contrib/ci/README.md`. This implementation currently tests 13 different configurations. If build times become too long we can remove some of them. Although it would be nice to test macOS builds that requires significantly more work so I have left this as future work. --- .dockerignore | 4 + .travis.yml | 68 ++++++ README.md | 6 +- .../z3_base_ubuntu32_16.04.Dockerfile | 50 +++++ .../z3_base_ubuntu_14.04.Dockerfile | 35 +++ .../z3_base_ubuntu_16.04.Dockerfile | 38 ++++ contrib/ci/Dockerfiles/z3_build.Dockerfile | 109 +++++++++ contrib/ci/README.md | 113 ++++++++++ contrib/ci/maintainers.txt | 3 + contrib/ci/scripts/build_z3_cmake.sh | 128 +++++++++++ contrib/ci/scripts/run_quiet.sh | 41 ++++ contrib/ci/scripts/set_compiler_flags.sh | 46 ++++ contrib/ci/scripts/set_generator_args.sh | 20 ++ contrib/ci/scripts/test_z3_docs.sh | 24 ++ contrib/ci/scripts/test_z3_examples_cmake.sh | 87 ++++++++ contrib/ci/scripts/test_z3_install_cmake.sh | 24 ++ contrib/ci/scripts/test_z3_system_tests.sh | 54 +++++ .../ci/scripts/test_z3_unit_tests_cmake.sh | 24 ++ contrib/ci/scripts/travis_ci_entry_point.sh | 18 ++ .../ci/scripts/travis_ci_linux_entry_point.sh | 208 ++++++++++++++++++ .../ci/scripts/travis_ci_osx_entry_point.sh | 10 + 21 files changed, 1107 insertions(+), 3 deletions(-) create mode 100644 .dockerignore create mode 100644 .travis.yml create mode 100644 contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile create mode 100644 contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile create mode 100644 contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile create mode 100644 contrib/ci/Dockerfiles/z3_build.Dockerfile create mode 100644 contrib/ci/README.md create mode 100644 contrib/ci/maintainers.txt create mode 100755 contrib/ci/scripts/build_z3_cmake.sh create mode 100644 contrib/ci/scripts/run_quiet.sh create mode 100644 contrib/ci/scripts/set_compiler_flags.sh create mode 100644 contrib/ci/scripts/set_generator_args.sh create mode 100755 contrib/ci/scripts/test_z3_docs.sh create mode 100755 contrib/ci/scripts/test_z3_examples_cmake.sh create mode 100755 contrib/ci/scripts/test_z3_install_cmake.sh create mode 100755 contrib/ci/scripts/test_z3_system_tests.sh create mode 100755 contrib/ci/scripts/test_z3_unit_tests_cmake.sh create mode 100755 contrib/ci/scripts/travis_ci_entry_point.sh create mode 100755 contrib/ci/scripts/travis_ci_linux_entry_point.sh create mode 100755 contrib/ci/scripts/travis_ci_osx_entry_point.sh diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 000000000..e85dae524 --- /dev/null +++ b/.dockerignore @@ -0,0 +1,4 @@ +**/*.swp +**/*.pyc +.git +**/*.Dockerfile diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 000000000..e8e207466 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,68 @@ +cache: + # This persistent cache is used to cache the building of + # docker base images. + directories: + - $DOCKER_TRAVIS_CI_CACHE_DIR +sudo: required +language: cpp +services: + - docker +env: + global: + # This environment variable tells the `travis_ci_linux_entry_point.sh` + # script to look for a cached Docker image. + - DOCKER_TRAVIS_CI_CACHE_DIR=$HOME/.cache/docker + # Configurations + matrix: +############################################################################### +# Ubuntu 16.04 LTS +############################################################################### + # 64-bit GCC 5.4 RelWithDebInfo + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo + # 64-bit Clang 3.9 RelWithDebInfo + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo + + # 64-bit GCC 5.4 Debug + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug + # 64-bit Clang Debug + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/clang-3.9 CXX_COMPILER=/usr/bin/clang++-3.9 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug + + # 32-bit GCC 5.4 RelWithDebInfo + - LINUX_BASE=ubuntu32_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=i686 Z3_BUILD_TYPE=RelWithDebInfo + + # Both of the two configurations below build the docs because the current + # implementation uses python as part of the building process. + # TODO: Teach one of the configurations to upload built docs somewhere. + # Test with Python 3 and API docs + - LINUX_BASE=ubuntu_16.04 PYTHON_EXECUTABLE=/usr/bin/python3 BUILD_DOCS=1 + # Test with LibGMP and API docs + - LINUX_BASE=ubuntu_16.04 TARGET_ARCH=x86_64 USE_LIBGMP=1 BUILD_DOCS=1 PYTHON_EXECUTABLE=/usr/bin/python2.7 + + # Test without OpenMP + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 + + # Unix Makefile generator build + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_CMAKE_GENERATOR="Unix Makefiles" + + # LTO build + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 USE_LTO=1 + + # Static build. Note we have disable building the bindings because they won't work with a static libz3 + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_STATIC_BUILD=1 DOTNET_BINDINGS=0 JAVA_BINDINGS=0 PYTHON_BINDINGS=0 + +############################################################################### +# Ubuntu 14.04 LTS +############################################################################### + # GCC 4.8 + # 64-bit GCC 4.8 RelWithDebInfo + - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo + # 64-bit GCC 4.8 Debug + - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug + +# TODO: OSX support +#matrix: +# include: +# - os: osx +# osx_image: xcode 8.2 +script: + - contrib/ci/scripts/travis_ci_entry_point.sh diff --git a/README.md b/README.md index f92a5389a..465348dbd 100644 --- a/README.md +++ b/README.md @@ -12,9 +12,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z ## Build status -| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | -| ----------- | ----------- | ---------- | ---------- | ---------- | --- | -![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) +| Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI | +| ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- | +![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile new file mode 100644 index 000000000..d8a32edea --- /dev/null +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu32_16.04.Dockerfile @@ -0,0 +1,50 @@ +# This base image is not officially supported by Docker it +# is generated by running +# ``` +# ./update.sh xenial +# ``` +# from git@github.com:daald/docker-brew-ubuntu-core-32bit.git +# at commit 34ea593b40b423755b7d46b6c8c89fc8162ea74b +# +# We could actually store the image generated by this Dockerfile +# rather than just the bare image. However given we have a TravisCI +# cache I'm not sure if it faster to use the TravisCI cache or to +# download from DockerHub everytime. +FROM z3prover/ubuntu32:16.04 + +RUN apt-get update && \ + apt-get -y --no-install-recommends install \ + binutils \ + clang \ + clang-3.9 \ + cmake \ + doxygen \ + default-jdk \ + gcc \ + gcc-5 \ + git \ + graphviz \ + g++ \ + g++ \ + libgmp-dev \ + libgomp1 \ + libomp5 \ + libomp-dev \ + make \ + mono-devel \ + ninja-build \ + python3 \ + python3-setuptools \ + python2.7 \ + python-setuptools \ + sudo + +# Create `user` user for container with password `user`. and give it +# password-less sudo access +RUN useradd -m user && \ + echo user:user | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers +USER user +WORKDIR /home/user + diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile new file mode 100644 index 000000000..c28e59e97 --- /dev/null +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_14.04.Dockerfile @@ -0,0 +1,35 @@ +FROM ubuntu:14.04 + +RUN apt-get update && \ + apt-get -y --no-install-recommends install \ + binutils \ + clang-3.9 \ + cmake \ + doxygen \ + default-jdk \ + gcc-multilib \ + gcc-4.8-multilib \ + git \ + graphviz \ + g++-multilib \ + g++-4.8-multilib \ + libgmp-dev \ + libgomp1 \ + lib32gomp1 \ + make \ + mono-devel \ + ninja-build \ + python3 \ + python3-setuptools \ + python2.7 \ + python-setuptools + +# Create `user` user for container with password `user`. and give it +# password-less sudo access +RUN useradd -m user && \ + echo user:user | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers +USER user +WORKDIR /home/user + diff --git a/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile new file mode 100644 index 000000000..98a5a3e09 --- /dev/null +++ b/contrib/ci/Dockerfiles/z3_base_ubuntu_16.04.Dockerfile @@ -0,0 +1,38 @@ +FROM ubuntu:16.04 + +RUN apt-get update && \ + apt-get -y --no-install-recommends install \ + binutils \ + clang \ + clang-3.9 \ + cmake \ + doxygen \ + default-jdk \ + gcc-multilib \ + gcc-5-multilib \ + git \ + graphviz \ + g++-multilib \ + g++-5-multilib \ + libgmp-dev \ + libgomp1 \ + libomp5 \ + libomp-dev \ + make \ + mono-devel \ + ninja-build \ + python3 \ + python3-setuptools \ + python2.7 \ + python-setuptools \ + sudo + +# Create `user` user for container with password `user`. and give it +# password-less sudo access +RUN useradd -m user && \ + echo user:user | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers +USER user +WORKDIR /home/user + diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile new file mode 100644 index 000000000..8b922edff --- /dev/null +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -0,0 +1,109 @@ +ARG DOCKER_IMAGE_BASE +FROM ${DOCKER_IMAGE_BASE} + + +# Specify defaults. This can be changed when invoking +# `docker build`. +ARG ASAN_BUILD=0 +ARG BUILD_DOCS=0 +ARG CC=gcc +ARG CXX=g++ +ARG DOTNET_BINDINGS=1 +ARG JAVA_BINDINGS=1 +ARG NO_SUPPRESS_OUTPUT=0 +ARG PYTHON_BINDINGS=1 +ARG PYTHON_EXECUTABLE=/usr/bin/python2.7 +ARG RUN_SYSTEM_TESTS=1 +ARG RUN_UNIT_TESTS=1 +ARG TARGET_ARCH=x86_64 +ARG TEST_INSTALL=1 +ARG UBSAN_BUILD=0 +ARG USE_LIBGMP=0 +ARG USE_LTO=0 +ARG USE_OPENMP=1 +ARG Z3_SRC_DIR=/home/user/z3_src +ARG Z3_BUILD_TYPE=RelWithDebInfo +ARG Z3_CMAKE_GENERATOR=Ninja +ARG Z3_INSTALL_PREFIX=/usr +ARG Z3_STATIC_BUILD=0 +# Blank default indicates use latest. +ARG Z3_SYSTEM_TEST_GIT_REVISION +ARG Z3_VERBOSE_BUILD_OUTPUT=0 + +ENV \ + ASAN_BUILD=${ASAN_BUILD} \ + BUILD_DOCS=${BUILD_DOCS} \ + CC=${CC} \ + CXX=${CXX} \ + DOTNET_BINDINGS=${DOTNET_BINDINGS} \ + JAVA_BINDINGS=${JAVA_BINDINGS} \ + NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT} \ + PYTHON_BINDINGS=${PYTHON_BINDINGS} \ + PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ + RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS} \ + RUN_UNIT_TESTS=${RUN_UNIT_TESTS} \ + TARGET_ARCH=${TARGET_ARCH} \ + TEST_INSTALL=${TEST_INSTALL} \ + UBSAN_BUILD=${UBSAN_BUILD} \ + USE_LIBGMP=${USE_LIBGMP} \ + USE_LTO=${USE_LTO} \ + USE_OPENMP=${USE_OPENMP} \ + Z3_SRC_DIR=${Z3_SRC_DIR} \ + Z3_BUILD_DIR=/home/user/z3_build \ + Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR} \ + Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT} \ + Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \ + Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \ + Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \ + Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} + +# We add context across incrementally to maximal cache reuse + +# Build Z3 +RUN mkdir -p "${Z3_SRC_DIR}" && \ + mkdir -p "${Z3_SRC_DIR}/contrib/ci/scripts" +# Deliberately leave out `contrib` +ADD /cmake ${Z3_SRC_DIR}/cmake/ +ADD /doc ${Z3_SRC_DIR}/doc/ +ADD /examples ${Z3_SRC_DIR}/examples/ +ADD /scripts ${Z3_SRC_DIR}/scripts/ +ADD /src ${Z3_SRC_DIR}/src/ +ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/ + +ADD \ + /contrib/ci/scripts/build_z3_cmake.sh \ + /contrib/ci/scripts/set_compiler_flags.sh \ + /contrib/ci/scripts/set_generator_args.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/build_z3_cmake.sh + +# Test building docs +ADD \ + /contrib/ci/scripts/test_z3_docs.sh \ + /contrib/ci/scripts/run_quiet.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_docs.sh + +# Test examples +ADD \ + /contrib/ci/scripts/test_z3_examples_cmake.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_examples_cmake.sh + +# Run unit tests +ADD \ + /contrib/ci/scripts/test_z3_unit_tests_cmake.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_unit_tests_cmake.sh + +# Run system tests +ADD \ + /contrib/ci/scripts/test_z3_system_tests.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_system_tests.sh + +# Test install +ADD \ + /contrib/ci/scripts/test_z3_install_cmake.sh \ + ${Z3_SRC_DIR}/contrib/ci/scripts/ +RUN ${Z3_SRC_DIR}/contrib/ci/scripts/test_z3_install_cmake.sh diff --git a/contrib/ci/README.md b/contrib/ci/README.md new file mode 100644 index 000000000..31bb504b6 --- /dev/null +++ b/contrib/ci/README.md @@ -0,0 +1,113 @@ +# Continous integration scripts + +## TravisCI + +For testing on Linux and macOS we use [TravisCI](https://travis-ci.org/) + +TravisCI consumes the `.travis.yml` file in the root of the repository +to tell it how to build and test Z3. + +However the logic for building and test Z3 is kept out of this file +and instead in a set of scripts in `scripts/`. This avoids +coupling the build to TravisCI tightly so we can migrate to another +service if required in the future. + +The scripts rely on a set of environment variables to control the configuration +of the build. The `.travis.yml` declares a list of configuration with each +configuration setting different environment variables. + +Note that the build scripts currently only support Z3 built with CMake. Support +for building Z3 using the older Python/Makefile build system might be added in +the future. + +### Configuration variables + +* `ASAN_BUILD` - Do [AddressSanitizer](https://github.com/google/sanitizers/wiki/AddressSanitizer) build (`0` or `1`) +* `BUILD_DOCS` - Build API documentation (`0` or `1`) +* `C_COMPILER` - Path to C Compiler +* `CXX_COMPILER` - Path to C++ Compiler +* `DOTNET_BINDINGS` - Build and test .NET API bindings (`0` or `1`) +* `JAVA_BINDINGS` - Build and test Java API bindings (`0` or `1`) +* `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`) +* `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`) +* `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`) +* `RUN_UNIT_TESTS` - Run unit tests (`0` or `1`) +* `TARGET_ARCH` - Target architecture (`x86_64` or `i686`) +* `TEST_INSTALL` - Test running `install` target (`0` or `1`) +* `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`) +* `USE_LIBGMP` - Use [GNU multiple precision library](https://gmplib.org/) (`0` or `1`) +* `USE_LTO` - Link binaries using link time optimization (`0` or `1`) +* `USE_OPENMP` - Use OpenMP (`0` or `1`) +* `Z3_BUILD_TYPE` - CMake build type (`RelWithDebInfo`, `Release`, `Debug`, or `MinSizeRel`) +* `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`) +* `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`) +* `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`) +* `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used. + +### Linux + +For Linux we use Docker to perform the build so that it easily reproducible +on a local machine and so that we can avoid depending on TravisCI's environment +and instead use a Linux distribution of our choice. + +The `scripts/travis_ci_linux_entry_point.sh` script + +1. Creates a base image containing all the dependencies needed to build and test Z3 +2. Builds and tests Z3 using the base image propagating configuration environment + variables (if set) into the build using the `--build-arg` argument of the `docker run` + command. + +If an environemnt variable is not set a defaults value is used which can be +found in `Dockerfiles/z3_build.Dockerfile`. + +#### Linux specific configuration variables + +* `LINUX_BASE` - The base docker image identifier to use (`ubuntu_16.04`, `ubuntu32_16.04`, or `ubuntu_14.04`). + +#### Reproducing a build locally + +A build can be reproduced locally by using the `scripts/travis_ci_linux_entry_point.sh` +script and setting the appropriate environment variable. + +For example lets say we wanted to reproduce the build below. + +```yaml + + - LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo +``` + +This can be done by running the command + +```bash +LINUX_BASE=ubuntu_16.04 C_COMPILER=/usr/bin/gcc-5 CXX_COMPILER=/usr/bin/g++-5 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=RelWithDebInfo scripts/travis_ci_linux_entry_point.sh +``` + +The `docker build` command which we use internally supports caching. What this +means in practice is that re-running the above command will re-use successfully +completed stages of the build provided they haven't changed. This requires that +the `Dockerfiles/z3_build.Dockerfile` is carefully crafted to avoid invalidating +the cache when unrelated files sent to the build context change. + +#### TravisCI docker image cache + +To improve build times the Z3 base docker images are cached using +[TravisCI's cache directory feature](https://docs.travis-ci.com/user/caching). +If the `DOCKER_TRAVIS_CI_CACHE_DIR` environment variable is set (see `.travis.yml`) +then the directory pointed to by the environment variable is used as a cache +for Docker images. + +The logic for this can be found in `scripts/travis_ci_linux_entry_point.sh`. +The build time improvements are rather modest (~ 2 minutes) and the cache is +rather large due to TravisCI giving each configuration its own cache. So this +feature might be removed in the future. + +It may be better to just build the base image once (outside of TravisCI), upload +it to [DockerHub](https://hub.docker.com/) and have the build pull down the pre-built +image everytime. + +An [organization](https://hub.docker.com/u/z3prover/) has been created on +DockerHub for this. + +### macOS + +Not yet implemented. diff --git a/contrib/ci/maintainers.txt b/contrib/ci/maintainers.txt new file mode 100644 index 000000000..caa6798c6 --- /dev/null +++ b/contrib/ci/maintainers.txt @@ -0,0 +1,3 @@ +# Maintainers + +- Dan Liew (@delcypher) diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh new file mode 100755 index 000000000..98a9724c7 --- /dev/null +++ b/contrib/ci/scripts/build_z3_cmake.sh @@ -0,0 +1,128 @@ +#!/bin/bash +# This script builds Z3 + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"} +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"} +: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"} +: ${Z3_STATIC_BUILD?"Z3_STATIC_BUILD must be specified"} +: ${USE_OPENMP?"USE_OPENMP must be specified"} +: ${USE_LIBGMP?"USE_LIBGMP must be specified"} +: ${BUILD_DOCS?"BUILD_DOCS must be specified"} +: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} +: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} +: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} +: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} +: ${USE_LTO?"USE_LTO must be specified"} +: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX"} + +ADDITIONAL_Z3_OPTS=() + +# Static or dynamic libz3 +if [ "X${Z3_STATIC_BUILD}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=('-DBUILD_LIBZ3_SHARED=OFF') +else + ADDITIONAL_Z3_OPTS+=('-DBUILD_LIBZ3_SHARED=ON') +fi + +# Use OpenMP? +if [ "X${USE_OPENMP}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=('-DUSE_OPENMP=ON') +else + ADDITIONAL_Z3_OPTS+=('-DUSE_OPENMP=OFF') +fi + +# Use LibGMP? +if [ "X${USE_LIBGMP}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=('-DUSE_LIB_GMP=ON') +else + ADDITIONAL_Z3_OPTS+=('-DUSE_LIB_GMP=OFF') +fi + +# Use link time optimziation? +if [ "X${USE_LTO}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=('-DLINK_TIME_OPTIMIZATION=ON') +else + ADDITIONAL_Z3_OPTS+=('-DLINK_TIME_OPTIMIZATION=OFF') +fi + +# Build API docs? +if [ "X${BUILD_DOCS}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_DOCUMENTATION=ON' \ + '-DALWAYS_BUILD_DOCS=OFF' \ + ) +else + ADDITIONAL_Z3_OPTS+=('-DBUILD_DOCUMENTATION=OFF') +fi + +# Python bindings? +if [ "X${PYTHON_BINDINGS}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_PYTHON_BINDINGS=ON' \ + '-DINSTALL_PYTHON_BINDINGS=ON' \ + ) +else + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_PYTHON_BINDINGS=OFF' \ + '-DINSTALL_PYTHON_BINDINGS=OFF' \ + ) +fi + +# .NET bindings? +if [ "X${DOTNET_BINDINGS}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_DOTNET_BINDINGS=ON' \ + '-DINSTALL_DOTNET_BINDINGS=ON' \ + ) +else + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_DOTNET_BINDINGS=OFF' \ + '-DINSTALL_DOTNET_BINDINGS=OFF' \ + ) +fi + +# Java bindings? +if [ "X${JAVA_BINDINGS}" = "X1" ]; then + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_JAVA_BINDINGS=ON' \ + '-DINSTALL_JAVA_BINDINGS=ON' \ + ) +else + ADDITIONAL_Z3_OPTS+=( \ + '-DBUILD_JAVA_BINDINGS=OFF' \ + '-DINSTALL_JAVA_BINDINGS=OFF' \ + ) +fi + +# Set compiler flags +source ${SCRIPT_DIR}/set_compiler_flags.sh + +# Sanity check +if [ ! -e "${Z3_SRC_DIR}/CMakeLists.txt" ]; then + echo "Z3_SRC_DIR is invalid" + exit 1 +fi + +# Make build tree +mkdir -p "${Z3_BUILD_DIR}" +cd "${Z3_BUILD_DIR}" + +# Configure +cmake \ + -G "${Z3_CMAKE_GENERATOR}" \ + -DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \ + -DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ + -DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \ + "${ADDITIONAL_Z3_OPTS[@]}" \ + "${Z3_SRC_DIR}" + +# Build +source ${SCRIPT_DIR}/set_generator_args.sh +cmake --build $(pwd) "${GENERATOR_ARGS[@]}" diff --git a/contrib/ci/scripts/run_quiet.sh b/contrib/ci/scripts/run_quiet.sh new file mode 100644 index 000000000..5abc910e8 --- /dev/null +++ b/contrib/ci/scripts/run_quiet.sh @@ -0,0 +1,41 @@ +# Simple wrapper function that runs a command suppressing +# it's output. However it's output will be shown in the +# case that `NO_SUPPRESS_OUTPUT` is set to `1` or the command +# fails. +# +# The use case for this trying to avoid large logs on TravisCI +function run_quiet() { + if [ "X${NO_SUPPRESS_OUTPUT}" = "X1" ]; then + "${@}" + else + OLD_SETTINGS="$-" + set +x + set +e + TMP_DIR="${TMP_DIR:-/tmp/}" + STDOUT="${TMP_DIR}/$$.stdout" + STDERR="${TMP_DIR}/$$.stderr" + "${@}" > "${STDOUT}" 2> "${STDERR}" + EXIT_STATUS="$?" + if [ "${EXIT_STATUS}" -ne 0 ]; then + echo "Command \"$@\" failed" + echo "EXIT CODE: ${EXIT_STATUS}" + echo "STDOUT" + echo "" + echo "\`\`\`" + cat ${STDOUT} + echo "\`\`\`" + echo "" + echo "STDERR" + echo "" + echo "\`\`\`" + cat ${STDERR} + echo "\`\`\`" + echo "" + fi + # Clean up + rm "${STDOUT}" "${STDERR}" + [ $( echo "${OLD_SETTINGS}" | grep -c 'e') -ne 0 ] && set -e + [ $( echo "${OLD_SETTINGS}" | grep -c 'x') -ne 0 ] && set -x + return ${EXIT_STATUS} + fi +} diff --git a/contrib/ci/scripts/set_compiler_flags.sh b/contrib/ci/scripts/set_compiler_flags.sh new file mode 100644 index 000000000..7efdecdac --- /dev/null +++ b/contrib/ci/scripts/set_compiler_flags.sh @@ -0,0 +1,46 @@ +# This script should is intended to be included by other +# scripts and should not be executed directly + +: ${TARGET_ARCH?"TARGET_ARCH must be specified"} +: ${ASAN_BUILD?"ASAN_BUILD must be specified"} +: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} +: ${CC?"CC must be specified"} +: ${CXX?"CXX must be specified"} + +case ${TARGET_ARCH} in + x86_64) + CXXFLAGS="${CXXFLAGS} -m64" + CFLAGS="${CFLAGS} -m64" + ;; + i686) + CXXFLAGS="${CXXFLAGS} -m32" + CFLAGS="${CFLAGS} -m32" + ;; + *) + echo "Unknown arch \"${TARGET_ARCH}\"" + exit 1 +esac + +if [ "X${ASAN_BUILD}" = "X1" ]; then + CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" + CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer" +fi + +if [ "X${UBSAN_BUILD}" = "X1" ]; then + CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" + CFLAGS="${CFLAGS} -fsanitize=undefined" +fi + +# Report flags +echo "CXXFLAGS: ${CXXFLAGS}" +echo "CFLAGS: ${CFLAGS}" + +# Report compiler +echo "CC: ${CC}" +${CC} --version +echo "CXX: ${CXX}" +${CXX} --version + +# Export the values +export CFLAGS +export CXXFLAGS diff --git a/contrib/ci/scripts/set_generator_args.sh b/contrib/ci/scripts/set_generator_args.sh new file mode 100644 index 000000000..0ef7b76aa --- /dev/null +++ b/contrib/ci/scripts/set_generator_args.sh @@ -0,0 +1,20 @@ +# This script should is intended to be included by other +# scripts and should not be executed directly + +: ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"} +: ${Z3_VERBOSE_BUILD_OUTPUT?"Z3_VERBOSE_BUILD_OUTPUT must be specified"} + +GENERATOR_ARGS=('--') +if [ "${Z3_CMAKE_GENERATOR}" = "Unix Makefiles" ]; then + GENERATOR_ARGS+=("-j$(nproc)") + if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then + GENERATOR_ARGS+=("VERBOSE=1") + fi +elif [ "${Z3_CMAKE_GENERATOR}" = "Ninja" ]; then + if [ "X${Z3_VERBOSE_BUILD_OUTPUT}" = "X1" ]; then + GENERATOR_ARGS+=("-v") + fi +else + echo "Unknown CMake generator \"${Z3_CMAKE_GENERATOR}\"" + exit 1 +fi diff --git a/contrib/ci/scripts/test_z3_docs.sh b/contrib/ci/scripts/test_z3_docs.sh new file mode 100755 index 000000000..6a65ffedd --- /dev/null +++ b/contrib/ci/scripts/test_z3_docs.sh @@ -0,0 +1,24 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" +. ${SCRIPT_DIR}/run_quiet.sh + +set -x +set -e +set -o pipefail + +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${BUILD_DOCS?"BUILD_DOCS must be specified"} + +# Set CMake generator args +source ${SCRIPT_DIR}/set_generator_args.sh + +cd "${Z3_BUILD_DIR}" + +# Generate documentation +if [ "X${BUILD_DOCS}" = "X1" ]; then + # TODO: Make quiet once we've fixed the build + run_quiet cmake --build $(pwd) --target api_docs "${GENERATOR_ARGS[@]}" +fi + +# TODO: Test or perhaps deploy the built docs? diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh new file mode 100755 index 000000000..2eda3de7b --- /dev/null +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -0,0 +1,87 @@ +#!/bin/bash + +# This script tests Z3 + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" +. ${SCRIPT_DIR}/run_quiet.sh + +set -x +set -e +set -o pipefail +: ${Z3_SRC_DIR?"Z3_SRC_DIR must be specified"} +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} +: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} +: ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} +: ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} + +# Set compiler flags +source ${SCRIPT_DIR}/set_compiler_flags.sh + +# Set CMake generator args +source ${SCRIPT_DIR}/set_generator_args.sh + +cd "${Z3_BUILD_DIR}" + +# Build and run C example +cmake --build $(pwd) --target c_example "${GENERATOR_ARGS[@]}" +run_quiet examples/c_example_build_dir/c_example + +# Build and run C++ example +cmake --build $(pwd) --target cpp_example "${GENERATOR_ARGS[@]}" +run_quiet examples/cpp_example_build_dir/cpp_example + +# Build and run tptp5 example +cmake --build $(pwd) --target z3_tptp5 "${GENERATOR_ARGS[@]}" +# FIXME: Do something more useful with example +run_quiet examples/tptp_build_dir/z3_tptp5 -help + +# Build an run c_maxsat_example +cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}" +run_quiet \ + examples/c_maxsat_example_build_dir/c_maxsat_example \ + ${Z3_SRC_DIR}/examples/maxsat/ex.smt + + +if [ "X${PYTHON_BINDINGS}" = "X1" ]; then + # Run python examples + # `all_interval_series.py` produces a lot of output so just throw + # away output. + # TODO: This example is slow should we remove it from testing? + run_quiet ${PYTHON_EXECUTABLE} python/all_interval_series.py + run_quiet ${PYTHON_EXECUTABLE} python/complex.py + run_quiet ${PYTHON_EXECUTABLE} python/example.py + # FIXME: `hamiltonian.py` example is disabled because its too slow. + #${PYTHON_EXECUTABLE} python/hamiltonian.py + run_quiet ${PYTHON_EXECUTABLE} python/marco.py + run_quiet ${PYTHON_EXECUTABLE} python/mss.py + run_quiet ${PYTHON_EXECUTABLE} python/socrates.py + run_quiet ${PYTHON_EXECUTABLE} python/visitor.py + run_quiet ${PYTHON_EXECUTABLE} python/z3test.py +fi + +if [ "X${DOTNET_BINDINGS}" = "X1" ]; then + # Build .NET example + # FIXME: Move compliation step into CMake target + mcs ${Z3_SRC_DIR}/examples/dotnet/Program.cs /target:exe /out:dotnet_test.exe /reference:Microsoft.Z3.dll /r:System.Numerics.dll + # Run .NET example + run_quiet mono ./dotnet_test.exe +fi + +if [ "X${JAVA_BINDINGS}" = "X1" ]; then + # Build Java example + # FIXME: Move compilation step into CMake target + mkdir -p examples/java + cp ${Z3_SRC_DIR}/examples/java/JavaExample.java examples/java/ + javac examples/java/JavaExample.java -classpath com.microsoft.z3.jar + # Run Java example + if [ "$(uname)" = "Darwin" ]; then + # macOS + export DYLD_LIBRARY_PATH=$(pwd):${DYLD_LIBRARY_PATH} + else + # Assume Linux for now + export LD_LIBRARY_PATH=$(pwd):${LD_LIBRARY_PATH} + fi + run_quiet java -cp .:examples/java:com.microsoft.z3.jar JavaExample +fi + diff --git a/contrib/ci/scripts/test_z3_install_cmake.sh b/contrib/ci/scripts/test_z3_install_cmake.sh new file mode 100755 index 000000000..804158f6f --- /dev/null +++ b/contrib/ci/scripts/test_z3_install_cmake.sh @@ -0,0 +1,24 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +: ${TEST_INSTALL?"TEST_INSTALL must be specified"} +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} + +if [ "X${TEST_INSTALL}" != "X1" ]; then + echo "Skipping install" + exit 0 +fi + +# Set CMake generator args +source ${SCRIPT_DIR}/set_generator_args.sh + +cd "${Z3_BUILD_DIR}" + +sudo cmake --build $(pwd) --target install "${GENERATOR_ARGS[@]}" + +# TODO: Test the installed version in some way diff --git a/contrib/ci/scripts/test_z3_system_tests.sh b/contrib/ci/scripts/test_z3_system_tests.sh new file mode 100755 index 000000000..dfb1084a4 --- /dev/null +++ b/contrib/ci/scripts/test_z3_system_tests.sh @@ -0,0 +1,54 @@ +#!/bin/bash + +set -x +set -e +set -o pipefail + +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${Z3_BUILD_TYPE?"Z3_BUILD_TYPE must be specified"} +: ${RUN_SYSTEM_TESTS?"RUN_SYSTEM_TESTS must be speicifed"} +: ${PYTHON_BINDINGS?"PYTHON_BINDINGS must be specified"} +: ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} +: ${Z3_SYSTEM_TEST_DIR?"Z3_SYSTEM_TEST_DIR must be specified"} + +if [ "X${RUN_SYSTEM_TESTS}" != "X1" ]; then + echo "Skipping system tests" + exit 0 +fi + +Z3_EXE="${Z3_BUILD_DIR}/z3" +Z3_LIB_DIR="${Z3_BUILD_DIR}" + +# Set value if not already defined externally +Z3_SYSTEM_TEST_GIT_URL="${Z3_GIT_URL:-https://github.com/Z3Prover/z3test.git}" + +# Clone repo to destination +mkdir -p "${Z3_SYSTEM_TEST_GIT_URL}" +git clone "${Z3_SYSTEM_TEST_GIT_URL}" "${Z3_SYSTEM_TEST_DIR}" +cd "${Z3_SYSTEM_TEST_DIR}" + +if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then + # If a particular revision is requested then check it out. + # This is useful for reproducible builds + git checkout "${Z3_SYSTEM_TEST_GIT_REVISION}" +fi + +############################################################################### +# Run system tests +############################################################################### + +# SMTLIBv2 tests +${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2 + +${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-extra + +if [ "X${Z3_BUILD_TYPE}" = "XDebug" ]; then + ${PYTHON_EXECUTABLE} scripts/test_benchmarks.py "${Z3_EXE}" regressions/smt2-debug +fi + +if [ "X${PYTHON_BINDINGS}" = "X1" ]; then + # Run python binding tests + ${PYTHON_EXECUTABLE} scripts/test_pyscripts.py "${Z3_LIB_DIR}" regressions/python/ +fi + +# FIXME: Run `scripts/test_cs.py` once it has been modified to support mono diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh new file mode 100755 index 000000000..0d8e59b0f --- /dev/null +++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh @@ -0,0 +1,24 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"} +: ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"} + +if [ "X${RUN_UNIT_TESTS}" != "X1" ]; then + echo "Skipping unit tests" + exit 0 +fi + +# Set CMake generator args +source ${SCRIPT_DIR}/set_generator_args.sh + +cd "${Z3_BUILD_DIR}" + +# Build and run internal tests +cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}" +./test-z3 diff --git a/contrib/ci/scripts/travis_ci_entry_point.sh b/contrib/ci/scripts/travis_ci_entry_point.sh new file mode 100755 index 000000000..41bde7230 --- /dev/null +++ b/contrib/ci/scripts/travis_ci_entry_point.sh @@ -0,0 +1,18 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +: ${TRAVIS_OS_NAME?"TRAVIS_OS_NAME should be set"} + +if [ "${TRAVIS_OS_NAME}" = "osx" ]; then + ${SCRIPT_DIR}/travis_ci_osx_entry_point.sh +elif [ "${TRAVIS_OS_NAME}" = "linux" ]; then + ${SCRIPT_DIR}/travis_ci_linux_entry_point.sh +else + echo "Unsupported OS \"${TRAVIS_OS_NAME}\"" + exit 1 +fi diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh new file mode 100755 index 000000000..21b97788f --- /dev/null +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -0,0 +1,208 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +DOCKER_FILE_DIR="$(cd ${SCRIPT_DIR}/../Dockerfiles; echo $PWD)" + +: ${LINUX_BASE?"LINUX_BASE must be specified"} + + + +# Sanity check. Current working directory should be repo root +if [ ! -f "./README.md" ]; then + echo "Current working directory should be repo root" + exit 1 +fi + +BUILD_OPTS=() +# Override options if they have been provided. +# Otherwise the defaults in the Docker file will be used +if [ -n "${Z3_CMAKE_GENERATOR}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}") +fi + +if [ -n "${USE_OPENMP}" ]; then + BUILD_OPTS+=("--build-arg" "USE_OPENMP=${USE_OPENMP}") +fi + +if [ -n "${USE_LIBGMP}" ]; then + BUILD_OPTS+=("--build-arg" "USE_LIBGMP=${USE_LIBGMP}") +fi + +if [ -n "${BUILD_DOCS}" ]; then + BUILD_OPTS+=("--build-arg" "BUILD_DOCS=${BUILD_DOCS}") +fi + +if [ -n "${PYTHON_EXECUTABLE}" ]; then + BUILD_OPTS+=("--build-arg" "PYTHON_EXECUTABLE=${PYTHON_EXECUTABLE}") +fi + +if [ -n "${PYTHON_BINDINGS}" ]; then + BUILD_OPTS+=("--build-arg" "PYTHON_BINDINGS=${PYTHON_BINDINGS}") +fi + +if [ -n "${DOTNET_BINDINGS}" ]; then + BUILD_OPTS+=("--build-arg" "DOTNET_BINDINGS=${DOTNET_BINDINGS}") +fi + +if [ -n "${JAVA_BINDINGS}" ]; then + BUILD_OPTS+=("--build-arg" "JAVA_BINDINGS=${JAVA_BINDINGS}") +fi + +if [ -n "${USE_LTO}" ]; then + BUILD_OPTS+=("--build-arg" "USE_LTO=${USE_LTO}") +fi + +if [ -n "${Z3_INSTALL_PREFIX}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX}") +fi + +# TravisCI reserves CC for itself so use a different name +if [ -n "${C_COMPILER}" ]; then + BUILD_OPTS+=("--build-arg" "CC=${C_COMPILER}") +fi + +# TravisCI reserves CXX for itself so use a different name +if [ -n "${CXX_COMPILER}" ]; then + BUILD_OPTS+=("--build-arg" "CXX=${CXX_COMPILER}") +fi + +if [ -n "${TARGET_ARCH}" ]; then + BUILD_OPTS+=("--build-arg" "TARGET_ARCH=${TARGET_ARCH}") +fi + +if [ -n "${ASAN_BUILD}" ]; then + BUILD_OPTS+=("--build-arg" "ASAN_BUILD=${ASAN_BUILD}") +fi + +if [ -n "${UBSAN_BUILD}" ]; then + BUILD_OPTS+=("--build-arg" "UBSAN_BUILD=${UBSAN_BUILD}") +fi + +if [ -n "${TEST_INSTALL}" ]; then + BUILD_OPTS+=("--build-arg" "TEST_INSTALL=${TEST_INSTALL}") +fi + +if [ -n "${RUN_SYSTEM_TESTS}" ]; then + BUILD_OPTS+=("--build-arg" "RUN_SYSTEM_TESTS=${RUN_SYSTEM_TESTS}") +fi + +if [ -n "${Z3_SYSTEM_TEST_GIT_REVISION}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION}" \ + ) +fi + +if [ -n "${RUN_UNIT_TESTS}" ]; then + BUILD_OPTS+=("--build-arg" "RUN_UNIT_TESTS=${RUN_UNIT_TESTS}") +fi + +if [ -n "${Z3_VERBOSE_BUILD_OUTPUT}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "Z3_VERBOSE_BUILD_OUTPUT=${Z3_VERBOSE_BUILD_OUTPUT}" \ + ) +fi + +if [ -n "${Z3_STATIC_BUILD}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_STATIC_BUILD=${Z3_STATIC_BUILD}") +fi + +if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "NO_SUPPRESS_OUTPUT=${NO_SUPPRESS_OUTPUT}" \ + ) +fi + +case ${LINUX_BASE} in + ubuntu_14.04) + BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_14.04.Dockerfile" + BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:14.04" + ;; + ubuntu_16.04) + BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_16.04.Dockerfile" + BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu:16.04" + ;; + ubuntu32_16.04) + BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu32_16.04.Dockerfile" + BASE_DOCKER_IMAGE_NAME="z3_base_ubuntu32:16.04" + ;; + *) + echo "Unknown Linux base ${LINUX_BASE}" + exit 1 + ;; +esac + +# Initially assume that we need to build the base Docker image +MUST_BUILD=1 + +# Travis CI persistent cache. +# +# This inspired by http://rundef.com/fast-travis-ci-docker-build . +# The idea is to cache the built image for subsequent builds to +# reduce build time. +if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then + CHECKSUM_FILE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.chksum" + CACHED_DOCKER_IMAGE="${DOCKER_TRAVIS_CI_CACHE_DIR}/${BASE_DOCKER_IMAGE_NAME}.gz" + if [ -f "${CACHED_DOCKER_IMAGE}" ]; then + # There's a cached image to use. Check the checksums of the Dockerfile + # match. If they don't that implies we need to build a fresh image. + if [ -f "${CHECKSUM_FILE}" ]; then + CURRENT_DOCKERFILE_CHECKSUM=$(sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }') + CACHED_DOCKERFILE_CHECKSUM=$(cat "${CHECKSUM_FILE}") + if [ "X${CURRENT_DOCKERFILE_CHECKSUM}" = "X${CACHED_DOCKERFILE_CHECKSUM}" ]; then + # Load the cached image + MUST_BUILD=0 + gunzip --stdout "${CACHED_DOCKER_IMAGE}" | docker load + fi + fi + fi +fi + +if [ "${MUST_BUILD}" -eq 1 ]; then + # The base image contains all the dependencies we want to build + # Z3. + docker build -t "${BASE_DOCKER_IMAGE_NAME}" - < "${BASE_DOCKER_FILE}" + + if [ -n "${DOCKER_TRAVIS_CI_CACHE_DIR}" ]; then + # Write image and checksum to cache + docker save "${BASE_DOCKER_IMAGE_NAME}" | \ + gzip > "${CACHED_DOCKER_IMAGE}" + sha256sum "${BASE_DOCKER_FILE}" | awk '{ print $1 }' > \ + "${CHECKSUM_FILE}" + fi +fi + + +DOCKER_MAJOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\1/') +DOCKER_MINOR_VERSION=$(docker info --format '{{.ServerVersion}}' | sed 's/^\([0-9]\+\)\.\([0-9]\+\).*$/\2/') +DOCKER_BUILD_FILE="${DOCKER_FILE_DIR}/z3_build.Dockerfile" + +if [ "${DOCKER_MAJOR_VERSION}${DOCKER_MINOR_VERSION}" -lt 1705 ]; then + # Workaround limitation in older Docker versions where the FROM + # command cannot be parameterized with an ARG. + sed \ + -e '/^ARG DOCKER_IMAGE_BASE/d' \ + -e 's/${DOCKER_IMAGE_BASE}/'"${BASE_DOCKER_IMAGE_NAME}/" \ + "${DOCKER_BUILD_FILE}" > "${DOCKER_BUILD_FILE}.patched" + DOCKER_BUILD_FILE="${DOCKER_BUILD_FILE}.patched" +else + # This feature landed in Docker 17.05 + # See https://github.com/moby/moby/pull/31352 + BUILD_OPTS+=( \ + "--build-arg" \ + "DOCKER_IMAGE_BASE=${BASE_DOCKER_IMAGE_NAME}" \ + ) +fi + +# Now build Z3 and test it using the created base image +docker build \ + -f "${DOCKER_BUILD_FILE}" \ + "${BUILD_OPTS[@]}" \ + . diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh new file mode 100755 index 000000000..03be81647 --- /dev/null +++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" + +set -x +set -e +set -o pipefail + +echo "Not implemented" +exit 1 From 08524a2d90e4402e72a7735dfa022b909cbe629e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Jul 2017 11:47:17 -0700 Subject: [PATCH 06/36] cleanup for warning message Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/muz/base/dl_rule_set.cpp | 2 +- src/muz/rel/dl_relation_manager.cpp | 2 +- src/opt/wmax.cpp | 2 +- src/qe/qe_arith_plugin.cpp | 2 +- src/smt/smt_consequences.cpp | 1 + src/smt/theory_lra.cpp | 8 +++-- src/smt/theory_seq.cpp | 34 +++++++++---------- .../portfolio/bounded_int2bv_solver.cpp | 4 +-- src/tactic/portfolio/enum2bv_solver.cpp | 4 +-- 10 files changed, 32 insertions(+), 29 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 2b2087e3b..258c28369 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -985,7 +985,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { numeral a; - expr* x; + expr* x = 0; if (m_util.is_numeral(arg, a)) { result = m_util.mk_numeral(floor(a), true); return BR_DONE; diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index e9b383b56..229db4d27 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -668,7 +668,7 @@ namespace datalog { T * el = it->m_key; item_set * out_edges = it->m_value; - unsigned el_comp; + unsigned el_comp = 0; VERIFY( m_component_nums.find(el, el_comp) ); item_set::iterator eit = out_edges->begin(); diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 74206a1f6..9e02a764f 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -294,7 +294,7 @@ namespace datalog { } table_relation_plugin & relation_manager::get_table_relation_plugin(table_plugin & tp) { - table_relation_plugin * res; + table_relation_plugin * res = 0; VERIFY( m_table_relation_plugins.find(&tp, res) ); return *res; } diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 58d319a63..15b723c8c 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -216,7 +216,7 @@ namespace opt { rational remove_negations(smt::theory_wmaxsat& th, expr_ref_vector const& core, ptr_vector& keys, vector& weights) { rational min_weight(-1); for (unsigned i = 0; i < core.size(); ++i) { - expr* e; + expr* e = 0; VERIFY(m.is_not(core[i], e)); keys.push_back(m_keys[e]); rational weight = m_weights[e]; diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 4281ec909..d8ae75256 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -2503,7 +2503,7 @@ public: } virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) { - nlarith::branch_conditions *brs; + nlarith::branch_conditions *brs = 0; VERIFY (m_cache.find(x.x(), fml, brs)); SASSERT(vl.is_unsigned()); SASSERT(vl.get_unsigned() < brs->size()); diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 65272207e..20813602e 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -103,6 +103,7 @@ namespace smt { void context::justify(literal lit, index_set& s) { ast_manager& m = m_manager; + (void)m; b_justification js = get_justification(lit.var()); switch (js.get_kind()) { case b_justification::CLAUSE: { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 76e721faa..2bd4844e8 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -765,7 +765,7 @@ namespace smt { } void internalize_eq_eh(app * atom, bool_var) { - expr* lhs, *rhs; + expr* lhs = 0, *rhs = 0; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); @@ -892,7 +892,7 @@ namespace smt { // to_int (to_real x) = x // to_real(to_int(x)) <= x < to_real(to_int(x)) + 1 void mk_to_int_axiom(app* n) { - expr* x, *y; + expr* x = 0, *y = 0; VERIFY (a.is_to_int(n, x)); if (a.is_to_real(x, y)) { mk_axiom(th.mk_eq(y, n, false)); @@ -908,7 +908,7 @@ namespace smt { // is_int(x) <=> to_real(to_int(x)) = x void mk_is_int_axiom(app* n) { - expr* x; + expr* x = 0; VERIFY(a.is_is_int(n, x)); literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false); literal is_int = ctx().get_literal(n); @@ -1299,12 +1299,14 @@ namespace smt { return; } int num_of_p = m_solver->settings().st().m_num_of_implied_bounds; + (void)num_of_p; local_bound_propagator bp(*this); m_solver->propagate_bounds_for_touched_rows(bp); if (m.canceled()) { return; } int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds; + (void)new_num_of_p; CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";); if (m_solver->get_status() == lean::lp_status::INFEASIBLE) { set_conflict(); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ea53f1342..dfb535f51 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1074,7 +1074,7 @@ expr_ref theory_seq::mk_first(expr* s) { void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) { - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; zstring s; if (m_util.str.is_empty(e)) { head = m_util.str.mk_unit(mk_nth(e, m_autil.mk_int(0))); @@ -1401,7 +1401,7 @@ bool theory_seq::occurs(expr* a, expr* b) { // true if a occurs under an interpreted function or under left/right selector. SASSERT(is_var(a)); SASSERT(m_todo.empty()); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; m_todo.push_back(b); while (!m_todo.empty()) { b = m_todo.back(); @@ -1990,7 +1990,7 @@ bool theory_seq::solve_nc(unsigned idx) { return true; } - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; if (m.is_eq(c, e1, e2)) { literal eq = mk_eq(e1, e2, false); propagate_lit(deps, 0, 0, ~eq); @@ -2316,7 +2316,7 @@ bool theory_seq::check_int_string() { bool theory_seq::add_stoi_axiom(expr* e) { context& ctx = get_context(); - expr* n; + expr* n = 0; rational val; TRACE("seq", tout << mk_pp(e, m) << "\n";); VERIFY(m_util.str.is_stoi(e, n)); @@ -2398,7 +2398,7 @@ expr_ref theory_seq::digit2int(expr* ch) { bool theory_seq::add_itos_axiom(expr* e) { context& ctx = get_context(); rational val; - expr* n; + expr* n = 0; TRACE("seq", tout << mk_pp(e, m) << "\n";); VERIFY(m_util.str.is_itos(e, n)); if (get_num_value(n, val)) { @@ -3197,7 +3197,7 @@ void theory_seq::add_indexof_axiom(expr* i) { */ void theory_seq::add_replace_axiom(expr* r) { - expr* a, *s, *t; + expr* a = 0, *s = 0, *t = 0; VERIFY(m_util.str.is_replace(r, a, s, t)); expr_ref x = mk_skolem(m_indexof_left, a, s); expr_ref y = mk_skolem(m_indexof_right, a, s); @@ -3330,7 +3330,7 @@ void theory_seq::add_itos_length_axiom(expr* len) { void theory_seq::propagate_in_re(expr* n, bool is_true) { TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; VERIFY(m_util.str.is_in_re(n, e1, e2)); expr_ref tmp(n, m); @@ -3462,7 +3462,7 @@ bool theory_seq::get_length(expr* e, rational& val) const { if (!tha) return false; rational val1; expr_ref len(m), len_val(m); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; ptr_vector todo; todo.push_back(e); val.reset(); @@ -3522,7 +3522,7 @@ bool theory_seq::get_length(expr* e, rational& val) const { */ void theory_seq::add_extract_axiom(expr* e) { - expr* s, *i, *l; + expr* s = 0, *i = 0, *l = 0; VERIFY(m_util.str.is_extract(e, s, i, l)); if (is_tail(s, i, l)) { add_tail_axiom(e, s); @@ -3682,7 +3682,7 @@ void theory_seq::add_at_axiom(expr* e) { */ void theory_seq::propagate_step(literal lit, expr* step) { SASSERT(get_context().get_assignment(lit) == l_true); - expr* re, *acc, *s, *idx, *i, *j; + expr* re = 0, *acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0; VERIFY(is_step(step, s, idx, re, i, j, acc)); TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";); propagate_lit(0, 1, &lit, mk_literal(acc)); @@ -3843,7 +3843,7 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp void theory_seq::assign_eh(bool_var v, bool is_true) { context & ctx = get_context(); expr* e = ctx.bool_var2expr(v); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; expr_ref f(m); bool change = false; literal lit(v, !is_true); @@ -4191,7 +4191,7 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned rej(s, idx, re, i) -> len(s) > idx if i is final */ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) { - expr *s, * idx, *re; + expr *s = 0, *idx = 0, *re = 0; unsigned src; eautomaton* aut = 0; bool is_acc; @@ -4220,7 +4220,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) { TRACE("seq", tout << mk_pp(acc, m) << "\n";); SASSERT(ctx.get_assignment(acc) == l_true); - expr *e, * idx, *re; + expr *e = 0, *idx = 0, *re = 0; expr_ref step(m); unsigned src; eautomaton* aut = 0; @@ -4299,7 +4299,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) { bool theory_seq::add_step2accept(expr* step, bool& change) { context& ctx = get_context(); SASSERT(ctx.get_assignment(step) == l_true); - expr* re, *_acc, *s, *idx, *i, *j; + expr* re = 0, *_acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0; VERIFY(is_step(step, s, idx, re, i, j, _acc)); literal acc1 = mk_accept(s, idx, re, i); switch (ctx.get_assignment(acc1)) { @@ -4348,7 +4348,7 @@ Recall we also have: bool theory_seq::add_reject2reject(expr* rej, bool& change) { context& ctx = get_context(); SASSERT(ctx.get_assignment(rej) == l_true); - expr* s, *idx, *re; + expr* s = 0, *idx = 0, *re = 0; unsigned src; rational r; eautomaton* aut = 0; @@ -4410,7 +4410,7 @@ bool theory_seq::add_reject2reject(expr* rej, bool& change) { void theory_seq::propagate_not_prefix(expr* e) { context& ctx = get_context(); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; VERIFY(m_util.str.is_prefix(e, e1, e2)); literal lit = ctx.get_literal(e); SASSERT(ctx.get_assignment(lit) == l_false); @@ -4439,7 +4439,7 @@ void theory_seq::propagate_not_prefix(expr* e) { void theory_seq::propagate_not_prefix2(expr* e) { context& ctx = get_context(); - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; VERIFY(m_util.str.is_prefix(e, e1, e2)); literal lit = ctx.get_literal(e); SASSERT(ctx.get_assignment(lit) == l_false); diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 83693abba..e293ade17 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -168,7 +168,7 @@ public: // translate bit-vector consequences back to integer values for (unsigned i = 0; i < consequences.size(); ++i) { - expr* a, *b, *u, *v; + expr* a = 0, *b = 0, *u = 0, *v = 0; func_decl* f; rational num; unsigned bvsize; @@ -228,7 +228,7 @@ private: for (; it != end; ++it) { expr* e = *it; rational lo, hi; - bool s1, s2; + bool s1 = false, s2 = false; SASSERT(is_uninterp_const(e)); func_decl* f = to_app(e)->get_decl(); diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 35601f374..8c9ff122d 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -116,7 +116,7 @@ public: // translate enumeration constants to bit-vectors. for (unsigned i = 0; i < vars.size(); ++i) { - func_decl* f; + func_decl* f = 0; if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { bvars.push_back(m.mk_const(f)); } @@ -128,7 +128,7 @@ public: // translate bit-vector consequences back to enumeration types for (unsigned i = 0; i < consequences.size(); ++i) { - expr* a, *b, *u, *v; + expr* a = 0, *b = 0, *u = 0, *v = 0; func_decl* f; rational num; unsigned bvsize; From 031d7e1b5992b50f30c4871031d695be48dff169 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Jul 2017 16:58:40 -0700 Subject: [PATCH 07/36] use iterators, update build icon for osx Signed-off-by: Nikolaj Bjorner --- README.md | 2 +- src/smt/theory_seq.cpp | 15 +++++---------- src/util/scoped_vector.h | 25 +++++++++++++++++++++++++ 3 files changed, 31 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index 465348dbd..0df1979a8 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z | Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI | | ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- | -![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) +![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index dfb535f51..832995994 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2246,10 +2246,7 @@ bool theory_seq::internalize_term(app* term) { return true; } TRACE("seq_verbose", tout << mk_pp(term, m) << "\n";); - unsigned num_args = term->get_num_args(); - expr* arg; - for (unsigned i = 0; i < num_args; i++) { - arg = term->get_arg(i); + for (expr* arg : *term) { mk_var(ensure_enode(arg)); } if (m.is_bool(term)) { @@ -2602,9 +2599,9 @@ void theory_seq::collect_statistics(::statistics & st) const { void theory_seq::init_model(expr_ref_vector const& es) { expr_ref new_s(m); - for (unsigned i = 0; i < es.size(); ++i) { + for (expr* e : es) { dependency* eqs = 0; - expr_ref s = canonize(es[i], eqs); + expr_ref s = canonize(e, eqs); if (is_var(s)) { new_s = m_factory->get_fresh_value(m.get_sort(s)); m_rep.update(s, new_s, eqs); @@ -2615,13 +2612,11 @@ void theory_seq::init_model(expr_ref_vector const& es) { void theory_seq::init_model(model_generator & mg) { m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); mg.register_factory(m_factory); - for (unsigned j = 0; j < m_nqs.size(); ++j) { - ne const& n = m_nqs[j]; + for (ne const& n : m_nqs) { m_factory->register_value(n.l()); m_factory->register_value(n.r()); } - for (unsigned j = 0; j < m_nqs.size(); ++j) { - ne const& n = m_nqs[j]; + for (ne const& n : m_nqs) { for (unsigned i = 0; i < n.ls().size(); ++i) { init_model(n.ls(i)); init_model(n.rs(i)); diff --git a/src/util/scoped_vector.h b/src/util/scoped_vector.h index bacfbac89..f62fbc8a6 100644 --- a/src/util/scoped_vector.h +++ b/src/util/scoped_vector.h @@ -91,6 +91,31 @@ public: SASSERT(invariant()); } + class iterator { + scoped_vector const& m_vec; + unsigned m_index; + public: + iterator(scoped_vector const& v, unsigned idx): m_vec(v), m_index(idx) {} + + bool operator==(iterator const& other) const { return &other.m_vec == &m_vec && other.m_index == m_index; } + bool operator!=(iterator const& other) const { return &other.m_vec != &m_vec || other.m_index != m_index; } + T const& operator*() { return m_vec[m_index]; } + + iterator & operator++() { + ++m_index; + return *this; + } + + iterator operator++(int) { + iterator r = *this; + ++m_index; + return r; + } + }; + + iterator begin() { return iterator(*this, 0); } + iterator end() { return iterator(*this, m_size); } + void push_back(T const& t) { set_index(m_size, m_elems.size()); m_elems.push_back(t); From 934dd0db4af848dbe37c7af0f4df007978a247f1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Jul 2017 17:00:48 -0700 Subject: [PATCH 08/36] revert icon update Signed-off-by: Nikolaj Bjorner --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 0df1979a8..465348dbd 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z | Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI | | ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- | -![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) +![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang From 416d955cfbd36a5f4aa4f42c29a927180da41367 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Jul 2017 17:03:41 -0700 Subject: [PATCH 09/36] icon update, take 2 Signed-off-by: Nikolaj Bjorner --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 465348dbd..fa39f5a43 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z | Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI | | ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- | -![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | ![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) +![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang From cc4cc8e4fb3f7923b1c4f894126e70011a5b6cf0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Jul 2017 17:05:31 -0700 Subject: [PATCH 10/36] icon update, take 3 Signed-off-by: Nikolaj Bjorner --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index fa39f5a43..4f8889caa 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z | Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI | | ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- | -![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge) | ![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge) | ![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge) | ![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge) | ![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) +[![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)]((https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)]((https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=6) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)]((https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang From 47f194e4c981e6b438056f929d944d1191195cb3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Jul 2017 17:06:38 -0700 Subject: [PATCH 11/36] icon update, take 4 Signed-off-by: Nikolaj Bjorner --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 4f8889caa..197928877 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z | Windows x86 | Windows x64 | Ubuntu x64 | Ubuntu x86 | Debian x64 | OSX | TravisCI | | ----------- | ----------- | ---------- | ---------- | ---------- | --- | -------- | -[![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)]((https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)]((https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=6) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)]((https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) +[![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![ubuntu-x86-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/6/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=6) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang From 03fe3d74f88c14aba999703463e1d58f864f54a0 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 4 Jul 2017 13:28:18 -0400 Subject: [PATCH 12/36] clean up warnings in theory_str --- src/smt/theory_str.cpp | 112 +++++++++++++---------------------------- 1 file changed, 34 insertions(+), 78 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0671c319c..d8d130212 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -232,11 +232,11 @@ namespace smt { for (unsigned i = 0; i < num_args; ++i) { enode * arg = e->get_arg(i); theory_var v_arg = mk_var(arg); - TRACE("str", tout << "arg has theory var #" << v_arg << std::endl;); + TRACE("str", tout << "arg has theory var #" << v_arg << std::endl;); (void)v_arg; } theory_var v = mk_var(e); - TRACE("str", tout << "term has theory var #" << v << std::endl;); + TRACE("str", tout << "term has theory var #" << v << std::endl;); (void)v; if (opt_EagerStringConstantLengthAssertions && u.str.is_string(term)) { TRACE("str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;); @@ -257,7 +257,7 @@ namespace smt { void theory_str::refresh_theory_var(expr * e) { enode * en = ensure_enode(e); - theory_var v = mk_var(en); + theory_var v = mk_var(en); (void)v; TRACE("str", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;); m_basicstr_axiom_todo.push_back(en); } @@ -487,7 +487,6 @@ namespace smt { app * theory_str::mk_str_var(std::string name) { context & ctx = get_context(); - ast_manager & m = get_manager(); TRACE("str", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;); @@ -505,7 +504,7 @@ namespace smt { // this might help?? mk_var(ctx.get_enode(a)); m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); - TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); + TRACE("str", tout << "add " << mk_pp(a, get_manager()) << " to m_basicstr_axiom_todo" << std::endl;); variable_set.insert(a); internal_variable_set.insert(a); @@ -516,7 +515,6 @@ namespace smt { app * theory_str::mk_regex_rep_var() { context & ctx = get_context(); - ast_manager & m = get_manager(); sort * string_sort = u.str.mk_string_sort(); app * a = mk_fresh_const("regex", string_sort); @@ -527,7 +525,7 @@ namespace smt { SASSERT(ctx.e_internalized(a)); mk_var(ctx.get_enode(a)); m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); - TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); + TRACE("str", tout << "add " << mk_pp(a, get_manager()) << " to m_basicstr_axiom_todo" << std::endl;); variable_set.insert(a); //internal_variable_set.insert(a); @@ -933,8 +931,7 @@ namespace smt { SASSERT(len_xy); // build RHS: start by extracting x and y from Concat(x, y) - unsigned nArgs = a_cat->get_num_args(); - SASSERT(nArgs == 2); + SASSERT(a_cat->get_num_args() == 2); app * a_x = to_app(a_cat->get_arg(0)); app * a_y = to_app(a_cat->get_arg(1)); @@ -2054,7 +2051,7 @@ namespace smt { << "* |parent| = " << rational_to_string_if_exists(parentLen, parentLen_exists) << std::endl << "* |arg0| = " << rational_to_string_if_exists(arg0Len, arg0Len_exists) << std::endl << "* |arg1| = " << rational_to_string_if_exists(arg1Len, arg1Len_exists) << std::endl; - ); + ); (void)arg0Len_exists; if (parentLen_exists && !arg1Len_exists) { TRACE("str", tout << "make up len for arg1" << std::endl;); @@ -2125,7 +2122,8 @@ namespace smt { << "* |parent| = " << rational_to_string_if_exists(parentLen, parentLen_exists) << std::endl << "* |arg0| = " << rational_to_string_if_exists(arg0Len, arg0Len_exists) << std::endl << "* |arg1| = " << rational_to_string_if_exists(arg1Len, arg1Len_exists) << std::endl; - ); + ); (void)arg1Len_exists; + if (parentLen_exists && !arg0Len_exists) { TRACE("str", tout << "make up len for arg0" << std::endl;); expr_ref implyL11(m.mk_and(ctx.mk_eq_atom(mk_strlen(a_parent), mk_int(parentLen)), @@ -4496,8 +4494,6 @@ namespace smt { } void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) { - ast_manager & m = get_manager(); - if (!u.re.is_unroll(to_app(unrollFunc))) { return; } @@ -4509,8 +4505,8 @@ namespace smt { zstring strValue; u.str.is_string(constStr, strValue); - TRACE("str", tout << "unrollFunc: " << mk_pp(unrollFunc, m) << std::endl - << "constStr: " << mk_pp(constStr, m) << std::endl;); + TRACE("str", tout << "unrollFunc: " << mk_pp(unrollFunc, get_manager()) << std::endl + << "constStr: " << mk_pp(constStr, get_manager()) << std::endl;); if (strValue == "") { return; @@ -4807,17 +4803,16 @@ namespace smt { bool theory_str::in_same_eqc(expr * n1, expr * n2) { if (n1 == n2) return true; context & ctx = get_context(); - ast_manager & m = get_manager(); // similar to get_eqc_value(), make absolutely sure // that we've set this up properly for the context if (!ctx.e_internalized(n1)) { - TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n1, m) << " was not internalized" << std::endl;); + TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n1, get_manager()) << " was not internalized" << std::endl;); ctx.internalize(n1, false); } if (!ctx.e_internalized(n2)) { - TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n2, m) << " was not internalized" << std::endl;); + TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n2, get_manager()) << " was not internalized" << std::endl;); ctx.internalize(n2, false); } @@ -4876,7 +4871,7 @@ namespace smt { expr * strAst = itor1->first; expr * substrAst = itor1->second; - expr * boolVar; + expr * boolVar = NULL; if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) { TRACE("str", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;); } @@ -5013,7 +5008,7 @@ namespace smt { expr * strAst = itor1->first; expr * substrAst = itor1->second; - expr * boolVar; + expr * boolVar = NULL; if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) { TRACE("str", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;); } @@ -5624,7 +5619,6 @@ namespace smt { } void theory_str::print_grounded_concat(expr * node, std::map, std::set > > & groundedMap) { - ast_manager & m = get_manager(); TRACE("str", tout << mk_pp(node, m) << std::endl;); if (groundedMap.find(node) != groundedMap.end()) { std::map, std::set >::iterator itor = groundedMap[node].begin(); @@ -5633,13 +5627,13 @@ namespace smt { tout << "\t[grounded] "; std::vector::const_iterator vIt = itor->first.begin(); for (; vIt != itor->first.end(); ++vIt) { - tout << mk_pp(*vIt, m) << ", "; + tout << mk_pp(*vIt, get_manager()) << ", "; } tout << std::endl; tout << "\t[condition] "; std::set::iterator sIt = itor->second.begin(); for (; sIt != itor->second.end(); sIt++) { - tout << mk_pp(*sIt, m) << ", "; + tout << mk_pp(*sIt, get_manager()) << ", "; } tout << std::endl; ); @@ -6935,7 +6929,7 @@ namespace smt { } void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) { - ast_manager & m = get_manager(); + ast_manager & m = get_manager(); (void)m; expr * fVar = valueTester_fvar_map[valTester]; if (m_params.m_UseBinarySearch) { @@ -6990,17 +6984,16 @@ namespace smt { } bool theory_str::free_var_attempt(expr * nn1, expr * nn2) { - ast_manager & m = get_manager(); zstring nn2_str; if (internal_lenTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { - TRACE("str", tout << "acting on equivalence between length tester var " << mk_ismt2_pp(nn1, m) - << " and constant " << mk_ismt2_pp(nn2, m) << std::endl;); + TRACE("str", tout << "acting on equivalence between length tester var " << mk_pp(nn1, get_manager()) + << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); more_len_tests(nn1, nn2_str); return true; } else if (internal_valTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { if (nn2_str == "more") { - TRACE("str", tout << "acting on equivalence between value var " << mk_ismt2_pp(nn1, m) - << " and constant " << mk_ismt2_pp(nn2, m) << std::endl;); + TRACE("str", tout << "acting on equivalence between value var " << mk_pp(nn1, get_manager()) + << " and constant " << mk_pp(nn2, get_manager()) << std::endl;); more_value_tests(nn1, nn2_str); } return true; @@ -7301,6 +7294,7 @@ namespace smt { // this might help?? theory_var v = mk_var(n); TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;); + (void)v; } } } else if (ex_sort == bool_sort && !is_quantifier(ex)) { @@ -7387,7 +7381,6 @@ namespace smt { } void theory_str::init_search_eh() { - ast_manager & m = get_manager(); context & ctx = get_context(); TRACE("str", @@ -7395,7 +7388,7 @@ namespace smt { unsigned nFormulas = ctx.get_num_asserted_formulas(); for (unsigned i = 0; i < nFormulas; ++i) { expr * ex = ctx.get_asserted_formula(i); - tout << mk_ismt2_pp(ex, m) << (ctx.is_relevant(ex) ? " (rel)" : " (NOT REL)") << std::endl; + tout << mk_pp(ex, get_manager()) << (ctx.is_relevant(ex) ? " (rel)" : " (NOT REL)") << std::endl; } ); /* @@ -7410,36 +7403,6 @@ namespace smt { set_up_axioms(ex); } - /* - * Similar recursive descent, except over all initially assigned terms. - * This is done to find equalities between terms, etc. that we otherwise - * might not get a chance to see. - */ - - /* - expr_ref_vector assignments(m); - ctx.get_assignments(assignments); - for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) { - expr * ex = *i; - if (m.is_eq(ex)) { - TRACE("str", tout << "processing assignment " << mk_ismt2_pp(ex, m) << - ": expr is equality" << std::endl;); - app * eq = (app*)ex; - SASSERT(eq->get_num_args() == 2); - expr * lhs = eq->get_arg(0); - expr * rhs = eq->get_arg(1); - - enode * e_lhs = ctx.get_enode(lhs); - enode * e_rhs = ctx.get_enode(rhs); - std::pair eq_pair(e_lhs, e_rhs); - m_str_eq_todo.push_back(eq_pair); - } else { - TRACE("str", tout << "processing assignment " << mk_ismt2_pp(ex, m) - << ": expr ignored" << std::endl;); - } - } - */ - // this might be cheating but we need to make sure that certain maps are populated // before the first call to new_eq_eh() propagate(); @@ -7475,8 +7438,7 @@ namespace smt { } void theory_str::assign_eh(bool_var v, bool is_true) { - context & ctx = get_context(); - TRACE("str", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;); + TRACE("str", tout << "assert: v" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;); } void theory_str::push_scope_eh() { @@ -7543,7 +7505,6 @@ namespace smt { void theory_str::pop_scope_eh(unsigned num_scopes) { sLevel -= num_scopes; TRACE("str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;); - ast_manager & m = get_manager(); TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); }); @@ -7552,10 +7513,9 @@ namespace smt { obj_map >::iterator varItor = cut_var_map.begin(); while (varItor != cut_var_map.end()) { - expr * e = varItor->m_key; std::stack & val = cut_var_map[varItor->m_key]; while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) { - TRACE("str", tout << "remove cut info for " << mk_pp(e, m) << std::endl; print_cut_var(e, tout);); + TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout);); // T_cut * aCut = val.top(); val.pop(); // dealloc(aCut); @@ -7577,8 +7537,7 @@ namespace smt { ptr_vector new_m_basicstr; for (ptr_vector::iterator it = m_basicstr_axiom_todo.begin(); it != m_basicstr_axiom_todo.end(); ++it) { enode * e = *it; - app * a = e->get_owner(); - TRACE("str", tout << "consider deleting " << mk_pp(a, get_manager()) + TRACE("str", tout << "consider deleting " << mk_pp(e->get_owner(), get_manager()) << ", enode scope level is " << e->get_iscope_lvl() << std::endl;); if (e->get_iscope_lvl() <= (unsigned)sLevel) { @@ -8861,7 +8820,7 @@ namespace smt { continue; } bool hasEqcValue = false; - expr * eqcString = get_eqc_value(itor->first, hasEqcValue); + get_eqc_value(itor->first, hasEqcValue); if (!hasEqcValue) { TRACE("str", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;); needToAssignFreeVars = true; @@ -9104,7 +9063,6 @@ namespace smt { } void theory_str::print_value_tester_list(svector > & testerList) { - ast_manager & m = get_manager(); TRACE("str", int ss = testerList.size(); tout << "valueTesterList = {"; @@ -9113,7 +9071,7 @@ namespace smt { tout << std::endl; } tout << "(" << testerList[i].first << ", "; - tout << mk_ismt2_pp(testerList[i].second, m); + tout << mk_pp(testerList[i].second, get_manager()); tout << "), "; } tout << std::endl << "}" << std::endl; @@ -9345,8 +9303,7 @@ namespace smt { } bool anEqcHasValue = false; - // Z3_ast anEqc = get_eqc_value(t, aTester, anEqcHasValue); - expr * aTester_eqc_value = get_eqc_value(aTester, anEqcHasValue); + get_eqc_value(aTester, anEqcHasValue); if (!anEqcHasValue) { TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) << " doesn't have an equivalence class value." << std::endl;); @@ -9513,8 +9470,8 @@ namespace smt { items.reset(); rational low, high; - bool low_exists = lower_bound(cntInUnr, low); - bool high_exists = upper_bound(cntInUnr, high); + bool low_exists = lower_bound(cntInUnr, low); (void)low_exists; + bool high_exists = upper_bound(cntInUnr, high); (void)high_exists; TRACE("str", tout << "unroll " << mk_pp(unrFunc, mgr) << std::endl; @@ -10265,7 +10222,7 @@ namespace smt { } else { tout << "no eqc string constant"; } - tout << std::endl;); + tout << std::endl;); (void)effectiveInScope; if (effectiveLenInd == lenTesterInCbEq) { effectiveLenIndiStr = lenTesterValue; } else { @@ -10350,7 +10307,6 @@ namespace smt { void theory_str::process_free_var(std::map & freeVar_map) { context & ctx = get_context(); - ast_manager & m = get_manager(); std::set eqcRepSet; std::set leafVarSet; @@ -10377,7 +10333,7 @@ namespace smt { } } if (duplicated && dupVar != NULL) { - TRACE("str", tout << "Duplicated free variable found:" << mk_ismt2_pp(freeVar, m) + TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager()) << " = " << mk_ismt2_pp(dupVar, m) << " (SKIP)" << std::endl;); continue; } else { From 253870c6d7bb13c508188c51d81002f048c70b51 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jul 2017 13:08:23 -0700 Subject: [PATCH 13/36] fix compiler warnings Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_relation_manager.cpp | 50 +++++++------------ .../dl_mk_interp_tail_simplifier.cpp | 13 +++-- src/test/old_interval.cpp | 6 +-- src/test/small_object_allocator.cpp | 9 ++++ src/test/sorting_network.cpp | 10 ++-- src/test/substitution.cpp | 2 + src/util/total_order.h | 7 +-- src/util/uint_map.h | 5 ++ 8 files changed, 46 insertions(+), 56 deletions(-) diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 9e02a764f..5bb47c5c3 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -36,13 +36,10 @@ namespace datalog { void relation_manager::reset_relations() { - relation_map::iterator it=m_relations.begin(); - relation_map::iterator end=m_relations.end(); - for(;it!=end;++it) { - func_decl * pred = it->m_key; + for (auto const& kv : m_relations) { + func_decl * pred = kv.m_key; get_context().get_manager().dec_ref(pred); //inc_ref in get_relation - relation_base * r=(*it).m_value; - r->deallocate(); + kv.m_value->deallocate(); } m_relations.reset(); } @@ -119,35 +116,25 @@ namespace datalog { } void relation_manager::collect_non_empty_predicates(decl_set & res) const { - relation_map::iterator it = m_relations.begin(); - relation_map::iterator end = m_relations.end(); - for(; it!=end; ++it) { - if(!it->m_value->fast_empty()) { - res.insert(it->m_key); + for (auto const& kv : m_relations) { + if (!kv.m_value->fast_empty()) { + res.insert(kv.m_key); } } } void relation_manager::restrict_predicates(const decl_set & preds) { - typedef ptr_vector fd_vector; - fd_vector to_remove; + ptr_vector to_remove; - relation_map::iterator rit = m_relations.begin(); - relation_map::iterator rend = m_relations.end(); - for(; rit!=rend; ++rit) { - func_decl * pred = rit->m_key; + for (auto const& kv : m_relations) { + func_decl* pred = kv.m_key; if (!preds.contains(pred)) { to_remove.insert(pred); } } - fd_vector::iterator pit = to_remove.begin(); - fd_vector::iterator pend = to_remove.end(); - for(; pit!=pend; ++pit) { - func_decl * pred = *pit; - relation_base * rel; - VERIFY( m_relations.find(pred, rel) ); - rel->deallocate(); + for (func_decl* pred : to_remove) { + m_relations.find(pred)->deallocate(); m_relations.remove(pred); get_context().get_manager().dec_ref(pred); } @@ -283,11 +270,9 @@ namespace datalog { } table_plugin * relation_manager::get_table_plugin(symbol const& k) { - table_plugin_vector::iterator tpit = m_table_plugins.begin(); - table_plugin_vector::iterator tpend = m_table_plugins.end(); - for(; tpit!=tpend; ++tpit) { - if((*tpit)->get_name()==k) { - return *tpit; + for (table_plugin * tp : m_table_plugins) { + if (tp->get_name()==k) { + return tp; } } return 0; @@ -341,10 +326,9 @@ namespace datalog { return res; } - for (unsigned i = 0; i < m_relation_plugins.size(); ++i) { - p = m_relation_plugins[i]; - if (p->can_handle_signature(s)) { - return p->mk_empty(s); + for (relation_plugin* p1 : m_relation_plugins) { + if (p1->can_handle_signature(s)) { + return p1->mk_empty(s); } } diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 3c1d1b924..1ed847e89 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -250,7 +250,7 @@ namespace datalog { bool detect_equivalences(expr_ref_vector& v, bool inside_disjunction) { bool have_pair = false; - unsigned prev_pair_idx; + unsigned prev_pair_idx = 0; arg_pair ap; unsigned read_idx = 0; @@ -296,21 +296,20 @@ namespace datalog { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - if (m.is_not(f) && (m.is_and(args[0]) || m.is_or(args[0]))) { - SASSERT(num==1); + SASSERT(num == 1); expr_ref tmp(m); app* a = to_app(args[0]); m_app_args.reset(); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - m_brwr.mk_not(a->get_arg(i), tmp); + for (expr* arg : *a) { + m_brwr.mk_not(arg, tmp); m_app_args.push_back(tmp); } if (m.is_and(args[0])) { - result = m.mk_or(m_app_args.size(), m_app_args.c_ptr()); + result = mk_or(m_app_args); } else { - result = m.mk_and(m_app_args.size(), m_app_args.c_ptr()); + result = mk_and(m_app_args); } return BR_REWRITE2; } diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp index 92064c03e..12a45555d 100644 --- a/src/test/old_interval.cpp +++ b/src/test/old_interval.cpp @@ -120,9 +120,9 @@ class interval_tester { interval singleton(int i) { return interval(m, rational(i)); } interval all() { return interval(m); } - interval l(int i, bool o = false, int idx = 0) { return interval(m, rational(i), o, true, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx))); } - interval r(int i, bool o = false, int idx = 0) { return interval(m, rational(i), o, false, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx))); } - interval b(int l, int u, bool lo = false, bool uo = false, int idx_l = 0, int idx_u = 0) { + interval l(int i, bool o = false, size_t idx = 0) { return interval(m, rational(i), o, true, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx))); } + interval r(int i, bool o = false, size_t idx = 0) { return interval(m, rational(i), o, false, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx))); } + interval b(int l, int u, bool lo = false, bool uo = false, size_t idx_l = 0, size_t idx_u = 0) { return interval(m, rational(l), lo, idx_l == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx_l)), rational(u), uo, idx_u == 0 ? 0 : m.mk_leaf(reinterpret_cast(idx_u))); } diff --git a/src/test/small_object_allocator.cpp b/src/test/small_object_allocator.cpp index 1ecf865dd..5ae2836d0 100644 --- a/src/test/small_object_allocator.cpp +++ b/src/test/small_object_allocator.cpp @@ -36,5 +36,14 @@ void tst_small_object_allocator() { r3 = new (soa) char[1]; TRACE("small_object_allocator", tout << "r1: " << (void*)r1 << " r2: " << (void*)r2 << " r3: " << (void*)r3 << " r4: " << (void*)r4 << "\n";); + (void)r1; + (void)r2; + (void)r3; + (void)r4; + (void)q1; + + (void)p1; + (void)p2; + (void)p3; } diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index 81340651a..87cc05375 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -364,15 +364,13 @@ void test_at_most_1(unsigned n, bool full) { for (unsigned i = 0; i < ext.m_clauses.size(); ++i) { solver.assert_expr(ext.m_clauses[i].get()); } - lbool res; if (full) { solver.push(); solver.assert_expr(m.mk_not(m.mk_eq(result1, result2))); std::cout << result1 << "\n"; - res = solver.check(); - SASSERT(res == l_false); + VERIFY(l_false == solver.check()); solver.pop(1); } @@ -390,8 +388,7 @@ void test_at_most_1(unsigned n, bool full) { std::cout << atom << "\n"; if (is_true) ++k; } - res = solver.check(); - SASSERT(res == l_true); + VERIFY(l_false == solver.check()); if (k > 1) { solver.assert_expr(result1); } @@ -402,8 +399,7 @@ void test_at_most_1(unsigned n, bool full) { else { solver.assert_expr(m.mk_not(result1)); } - res = solver.check(); - SASSERT(res == l_false); + VERIFY(l_false == solver.check()); solver.pop(1); } } diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp index cdc7f2080..5609225c6 100644 --- a/src/test/substitution.cpp +++ b/src/test/substitution.cpp @@ -35,6 +35,8 @@ void tst_substitution() bool ok1 = unif(v1.get(), v2.get(), subst, false); bool ok2 = unif(v2.get(), v1.get(), subst, false); + (void)ok1; + (void)ok2; expr_ref res(m); diff --git a/src/util/total_order.h b/src/util/total_order.h index 7238a5ef9..6fda88110 100644 --- a/src/util/total_order.h +++ b/src/util/total_order.h @@ -79,12 +79,7 @@ class total_order { } cell * to_cell(T const & a) const { - void * r; -#ifdef Z3DEBUG - bool ok = -#endif - m_map.find(a, r); - SASSERT(ok); + void * r = m_map.find(a); return reinterpret_cast(r); } diff --git a/src/util/uint_map.h b/src/util/uint_map.h index 13e0a9db3..0344de322 100644 --- a/src/util/uint_map.h +++ b/src/util/uint_map.h @@ -38,6 +38,11 @@ public: return v != 0; } } + + T * find(unsigned k) const { + SASSERT(k < m_map.size() && m_map[k] != 0); + return m_map[k]; + } void insert(unsigned k, T * v) { m_map.reserve(k+1); From a1306eaab6497f1a321b97e8fc1d6463edcf7890 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jul 2017 13:17:37 -0700 Subject: [PATCH 14/36] fix compiler warnings Signed-off-by: Nikolaj Bjorner --- src/test/ext_numeral.cpp | 3 +-- src/test/heap.cpp | 5 +++-- src/test/karr.cpp | 4 ++-- src/test/model_based_opt.cpp | 4 +++- src/test/model_evaluator.cpp | 1 - src/test/mpz.cpp | 2 ++ src/test/object_allocator.cpp | 1 + src/test/qe_arith.cpp | 4 ++-- 8 files changed, 14 insertions(+), 10 deletions(-) diff --git a/src/test/ext_numeral.cpp b/src/test/ext_numeral.cpp index 0e2b691c9..6f92b1372 100644 --- a/src/test/ext_numeral.cpp +++ b/src/test/ext_numeral.cpp @@ -158,8 +158,7 @@ static void FUN_NAME(int a, ext_numeral_kind ak, int b, ext_numeral_kind bk, boo scoped_mpq _a(m), _b(m); \ m.set(_a, a); \ m.set(_b, b); \ - bool r = OP_NAME(m, _a, ak, _b, bk); \ - SASSERT(r == expected); \ + VERIFY(expected == OP_NAME(m, _a, ak, _b, bk)); \ } #define MK_TST_REL(NAME) MK_TST_REL_CORE(tst_ ## NAME, NAME) diff --git a/src/test/heap.cpp b/src/test/heap.cpp index e745463ff..3d5c5308a 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -47,12 +47,13 @@ static void tst1() { for (; it != end; ++it) { SASSERT(h.contains(*it)); } - int last = -1; while (!h.empty()) { int m1 = h.min_value(); int m2 = h.erase_min(); + (void)m1; + (void)m2; SASSERT(m1 == m2); - SASSERT(last < m2); + SASSERT(-1 < m2); } } diff --git a/src/test/karr.cpp b/src/test/karr.cpp index c5581cc66..c69932e22 100644 --- a/src/test/karr.cpp +++ b/src/test/karr.cpp @@ -58,7 +58,7 @@ namespace karr { } lbool is_sat = hb.saturate(); hb.display(std::cout); - SASSERT(is_sat == l_true); + VERIFY(is_sat == l_true); dst.reset(); unsigned basis_size = hb.get_basis_size(); for (unsigned i = 0; i < basis_size; ++i) { @@ -85,7 +85,7 @@ namespace karr { } lbool is_sat = hb.saturate(); hb.display(std::cout); - SASSERT(is_sat == l_true); + VERIFY(is_sat == l_true); dst.reset(); unsigned basis_size = hb.get_basis_size(); bool first_initial = true; diff --git a/src/test/model_based_opt.cpp b/src/test/model_based_opt.cpp index 64b2df285..5ee671a4a 100644 --- a/src/test/model_based_opt.cpp +++ b/src/test/model_based_opt.cpp @@ -20,6 +20,7 @@ static void add_ineq(opt::model_based_opt& mbo, mbo.add_constraint(vars, rational(k), rel); } +#if 0 static void add_ineq(opt::model_based_opt& mbo, unsigned x, int a, unsigned y, int b, @@ -31,6 +32,7 @@ static void add_ineq(opt::model_based_opt& mbo, vars.push_back(var(z, rational(c))); mbo.add_constraint(vars, rational(k), rel); } +#endif static void add_random_ineq(opt::model_based_opt& mbo, random_gen& r, @@ -295,7 +297,7 @@ static void test8() { unsigned z = mbo.add_var(rational(4)); unsigned u = mbo.add_var(rational(5)); unsigned v = mbo.add_var(rational(6)); - unsigned w = mbo.add_var(rational(6)); + // unsigned w = mbo.add_var(rational(6)); add_ineq(mbo, x0, 1, y, -1, 0, opt::t_le); add_ineq(mbo, x, 1, y, -1, 0, opt::t_lt); diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp index 0b509fba6..00048b230 100644 --- a/src/test/model_evaluator.cpp +++ b/src/test/model_evaluator.cpp @@ -28,7 +28,6 @@ void tst_model_evaluator() { expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m); expr* vI0p = vI0.get(); expr* vI1p = vI1.get(); - expr* vB0p = vB0.get(); expr* vB1p = vB1.get(); expr* vB2p = vB2.get(); diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp index ee7cf39f1..02627e842 100644 --- a/src/test/mpz.cpp +++ b/src/test/mpz.cpp @@ -147,6 +147,7 @@ void tst_div2k(synch_mpz_manager & m, mpz const & v, unsigned k) { m.power(two, k, pw); m.machine_div(v, pw, y); bool is_eq = m.eq(x, y); + (void)is_eq; CTRACE("mpz_2k", !is_eq, tout << "div: " << m.to_string(v) << ", k: " << k << " r: " << m.to_string(x) << ", expected: " << m.to_string(y) << "\n";); SASSERT(is_eq); m.del(x); @@ -174,6 +175,7 @@ void tst_mul2k(synch_mpz_manager & m, mpz const & v, unsigned k) { m.power(two, k, pw); m.mul(v, pw, y); bool is_eq = m.eq(x, y); + (void)is_eq; CTRACE("mpz_2k", !is_eq, tout << "mul: " << m.to_string(v) << ", k: " << k << " r: " << m.to_string(x) << ", expected: " << m.to_string(y) << "\n";); SASSERT(is_eq); m.del(x); diff --git a/src/test/object_allocator.cpp b/src/test/object_allocator.cpp index 16b9331e2..cca42cf6f 100644 --- a/src/test/object_allocator.cpp +++ b/src/test/object_allocator.cpp @@ -61,6 +61,7 @@ static void tst1() { m.recycle(c1); cell * c3 = m.allocate(); + (void)c3; SASSERT(c3->m_coeff.is_zero()); } diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index a73f7ed38..a52c02ecb 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -163,7 +163,7 @@ static app_ref generate_ineqs(ast_manager& m, sort* s, vector& app* x = vars[0].get(); app* y = vars[1].get(); - app* z = vars[2].get(); + // app* z = vars[2].get(); // // ax <= by, ax < by, not (ax >= by), not (ax > by) // @@ -247,7 +247,7 @@ static void test2(char const *ex) { ctx.push(); ctx.assert_expr(fml); lbool result = ctx.check(); - SASSERT(result == l_true); + VERIFY(result == l_true); ref md; ctx.get_model(md); ctx.pop(1); From d66db280a875f5f646b61a0ee0f41f8bf2877d97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jul 2017 13:43:32 -0700 Subject: [PATCH 15/36] fix compiler warnings Signed-off-by: Nikolaj Bjorner --- src/ast/substitution/substitution.cpp | 4 ++-- src/tactic/arith/elim01_tactic.cpp | 2 +- src/tactic/arith/lia2card_tactic.cpp | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index eea1938a6..f741d3fd4 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -85,7 +85,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e m_state = APPLY; unsigned j; - expr * e; + expr * e = 0; unsigned off; expr_offset n1; bool visited; @@ -214,7 +214,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e } } SASSERT(m_apply_cache.contains(n)); - m_apply_cache.find(n, e); + VERIFY(m_apply_cache.find(n, e)); m_new_exprs.push_back(e); result = e; diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index 1aef52d78..e00b1e9c0 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -169,7 +169,7 @@ public: for (; bit != bend; ++bit) { if (!is_app(*bit)) continue; app* x = to_app(*bit); - bool s1, s2; + bool s1 = false, s2 = false; rational lo, hi; if (a.is_int(x) && bounds.has_lower(x, lo, s1) && !s1 && zero <= lo && diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 4c2e0dead..8f37a8d5e 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -176,7 +176,7 @@ public: bound_manager::iterator bit = bounds.begin(), bend = bounds.end(); for (; bit != bend; ++bit) { expr* x = *bit; - bool s1, s2; + bool s1 = false, s2 = false; rational lo, hi; if (a.is_int(x) && bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() && From bd92797663eb29f92163249e92f4f80fe15bc5f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jul 2017 15:25:59 -0700 Subject: [PATCH 16/36] fix compiler warnings Signed-off-by: Nikolaj Bjorner --- src/test/bit_vector.cpp | 2 +- src/test/bv_simplifier_plugin.cpp | 58 +++++++++++++++---------------- src/test/check_assumptions.cpp | 2 +- src/test/dl_context.cpp | 54 +++++++++++++++------------- src/test/dl_query.cpp | 2 +- src/test/heap.cpp | 1 + src/test/hwf.cpp | 6 ++-- src/test/list.cpp | 1 + src/test/mpff.cpp | 2 +- src/test/nlsat.cpp | 3 +- src/test/pb2bv.cpp | 8 ++--- src/test/polynorm.cpp | 1 + src/test/proof_checker.cpp | 4 +-- src/test/rational.cpp | 2 +- src/test/sat_user_scope.cpp | 1 + src/test/simple_parser.cpp | 1 + src/test/upolynomial.cpp | 12 +++---- 17 files changed, 83 insertions(+), 77 deletions(-) diff --git a/src/test/bit_vector.cpp b/src/test/bit_vector.cpp index 7d3f96ae4..6f83bb328 100644 --- a/src/test/bit_vector.cpp +++ b/src/test/bit_vector.cpp @@ -48,7 +48,7 @@ static void tst1() { SASSERT(v1.size() == v2.size()); if (v1.size() > 0) { unsigned idx = rand()%v1.size(); - SASSERT(v1.get(idx) == v2[idx]); + VERIFY(v1.get(idx) == v2[idx]); } } else if (op <= 5) { diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp index dc930bb82..69b97a9cc 100644 --- a/src/test/bv_simplifier_plugin.cpp +++ b/src/test/bv_simplifier_plugin.cpp @@ -133,7 +133,7 @@ public: params[0] = parameter(2); ar = m_manager.mk_app(m_fid, OP_REPEAT, 1, params, 1, es); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((a64 << 32) | a64) == u64(e.get())); + VERIFY(((a64 << 32) | a64) == u64(e.get())); ar = m_manager.mk_app(m_fid, OP_BREDOR, e1.get()); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); @@ -163,11 +163,11 @@ public: ar = m_manager.mk_app(m_fid, OP_BIT0); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(!bit2bool(e.get())); + VERIFY(!bit2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_BIT1); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(bit2bool(e.get())); + VERIFY(bit2bool(e.get())); } @@ -187,113 +187,113 @@ public: ar = m_manager.mk_app(m_fid, OP_BADD, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a + b) == u32(e.get())); + VERIFY((a + b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BSUB, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a - b) == u32(e.get())); + VERIFY((a - b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BMUL, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a * b) == u32(e.get())); + VERIFY((a * b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BAND, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a & b) == u32(e.get())); + VERIFY((a & b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a | b) == u32(e.get())); + VERIFY((a | b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BNOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(~(a | b) == u32(e.get())); + VERIFY(~(a | b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BXOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a ^ b) == u32(e.get())); + VERIFY((a ^ b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BXNOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((~(a ^ b)) == u32(e.get())); + VERIFY((~(a ^ b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BNAND, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((~(a & b)) == u32(e.get())); + VERIFY((~(a & b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_ULEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a <= b) == ast2bool(e.get())); + VERIFY((a <= b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_UGEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a >= b) == ast2bool(e.get())); + VERIFY((a >= b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_ULT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a < b) == ast2bool(e.get())); + VERIFY((a < b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_UGT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a > b) == ast2bool(e.get())); + VERIFY((a > b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SLEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa <= sb) == ast2bool(e.get())); + VERIFY((sa <= sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SGEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa >= sb) == ast2bool(e.get())); + VERIFY((sa >= sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SLT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa < sb) == ast2bool(e.get())); + VERIFY((sa < sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SGT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa > sb) == ast2bool(e.get())); + VERIFY((sa > sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_BSHL, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((b>=32)?0:(a << b)) == u32(e.get())); + VERIFY(((b>=32)?0:(a << b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BLSHR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((b>=32)?0:(a >> b)) == u32(e.get())); + VERIFY(((b>=32)?0:(a >> b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BASHR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); std::cout << "compare: " << sa << " >> " << b << " = " << (sa >> b) << " with " << i32(e.get()) << "\n"; - SASSERT(b >= 32 || ((sa >> b) == i32(e.get()))); + VERIFY(b >= 32 || ((sa >> b) == i32(e.get()))); if (b != 0) { ar = m_manager.mk_app(m_fid, OP_BSDIV, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa / sb) == i32(e.get())); + VERIFY((sa / sb) == i32(e.get())); ar = m_manager.mk_app(m_fid, OP_BUDIV, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a / b) == u32(e.get())); + VERIFY((a / b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BSREM, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - //SASSERT((sa % sb) == i32(e.get())); + //VERIFY((sa % sb) == i32(e.get())); ar = m_manager.mk_app(m_fid, OP_BUREM, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a % b) == u32(e.get())); + VERIFY((a % b) == u32(e.get())); // TBD: BSMOD. } ar = m_manager.mk_app(m_fid, OP_CONCAT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((a64 << 32) | b64) == u64(e.get())); + VERIFY(((a64 << 32) | b64) == u64(e.get())); ar = m_manager.mk_app(m_fid, OP_BCOMP, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a == b) == bit2bool(e.get())); + VERIFY((a == b) == bit2bool(e.get())); } void test() { diff --git a/src/test/check_assumptions.cpp b/src/test/check_assumptions.cpp index fa8327cd4..918513ca0 100644 --- a/src/test/check_assumptions.cpp +++ b/src/test/check_assumptions.cpp @@ -38,7 +38,7 @@ void tst_check_assumptions() expr * npE = np.get(); lbool res1 = ctx.check(1, &npE); - SASSERT(res1==l_true); + VERIFY(res1 == l_true); ctx.assert_expr(npE); diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index ac09722ac..99a0480a6 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -14,6 +14,35 @@ Copyright (c) 2015 Microsoft Corporation using namespace datalog; +void tst_dl_context() { + symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") }; + + return; + +#if 0 + const unsigned rel_cnt = sizeof(relations)/sizeof(symbol); + const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog"; + + params_ref params; + for(unsigned rel_index=0; rel_index=0; eager_checking--) { + params.set_bool("eager_emptiness_checking", eager_checking!=0); + + std::cerr << "Testing " << relations[rel_index] << "\n"; + std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n"; + dl_context_simple_query_test(params); + dl_context_saturate_file(params, test_file); + } + } +#endif + +} + + +#if 0 + + static lbool dl_context_eval_unary_predicate(ast_manager & m, context & ctx, char const* problem_text, const char * pred_name) { parser* p = parser::create(ctx,m); @@ -72,29 +101,4 @@ void dl_context_saturate_file(params_ref & params, const char * f) { ctx.get_rel_context()->saturate(); std::cerr << "Done\n"; } - -void tst_dl_context() { - symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") }; - const unsigned rel_cnt = sizeof(relations)/sizeof(symbol); - - return; -#if 0 - const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog"; - - params_ref params; - for(unsigned rel_index=0; rel_index=0; eager_checking--) { - params.set_bool("eager_emptiness_checking", eager_checking!=0); - - std::cerr << "Testing " << relations[rel_index] << "\n"; - std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n"; - dl_context_simple_query_test(params); - dl_context_saturate_file(params, test_file); - } - } #endif -} - - - diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index ae7313e41..e69f1fb13 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -40,7 +40,7 @@ void dl_query_ask_for_last_arg(context & ctx, func_decl * pred, relation_fact & lbool is_sat = ctx.query(query); std::cerr << "@@ last arg query should succeed: " << should_be_successful << "\n"; - SASSERT(is_sat != l_undef); + VERIFY(is_sat != l_undef); relation_fact res_fact(m); res_fact.push_back(f.back()); diff --git a/src/test/heap.cpp b/src/test/heap.cpp index 3d5c5308a..17f9cfaa0 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -77,6 +77,7 @@ static void dump_heap(const int_heap2 & h, std::ostream & out) { } static void tst2() { + (void)dump_heap; int_heap2 h(N); for (int i = 0; i < N * 10; i++) { if (i % 1000 == 0) std::cout << "i: " << i << std::endl; diff --git a/src/test/hwf.cpp b/src/test/hwf.cpp index be32b5400..7a030a452 100644 --- a/src/test/hwf.cpp +++ b/src/test/hwf.cpp @@ -44,19 +44,19 @@ static void bug_to_rational() { unsynch_mpq_manager mq; scoped_mpq r(mq); - double ad, rd; + double ad = 0, rd = 0; m.set(a, 0.0); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + VERIFY(ad == rd); m.set(a, 1.0); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + VERIFY(ad == rd); m.set(a, 1.5); m.to_rational(a, r); diff --git a/src/test/list.cpp b/src/test/list.cpp index 5672f4246..a7ad76972 100644 --- a/src/test/list.cpp +++ b/src/test/list.cpp @@ -35,6 +35,7 @@ static void tst1() { list * l5 = append(r, l4, l2); TRACE("list", display(tout, l5->begin(), l5->end()); tout << "\n";); list * l6 = append(r, l5, l5); + (void) l6; TRACE("list", display(tout, l6->begin(), l6->end()); tout << "\n";); } diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index 44930f2bd..ca2354b8b 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -435,7 +435,7 @@ static void tst_limits(unsigned prec) { bool overflow = false; try { m.inc(a); } catch (mpff_manager::overflow_exception) { overflow = true; } - SASSERT(overflow); + VERIFY(overflow); m.set_max(a); m.dec(a); SASSERT(m.eq(a, b)); diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 27a0aa1da..df25db927 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -391,7 +391,6 @@ static void tst7() { params_ref ps; reslimit rlim; nlsat::solver s(rlim, ps); - anum_manager & am = s.am(); nlsat::pmanager & pm = s.pm(); nlsat::var x0, x1, x2, a, b, c, d; a = s.mk_var(false); @@ -423,7 +422,7 @@ static void tst7() { nlsat::literal_vector litsv(lits.size(), lits.c_ptr()); lbool res = s.check(litsv); - SASSERT(res == l_false); + VERIFY(res == l_false); for (unsigned i = 0; i < litsv.size(); ++i) { s.display(std::cout, litsv[i]); std::cout << " "; diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp index c114997c5..fcc309883 100644 --- a/src/test/pb2bv.cpp +++ b/src/test/pb2bv.cpp @@ -83,10 +83,10 @@ static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vectorcheck_sat(0,0); - SASSERT(res == l_true); + VERIFY(res == l_true); slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get()); res = slv->check_sat(0,0); - SASSERT(res == l_false); + VERIFY(res == l_false); } } diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index a8f4ab861..0bc9dfe3c 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -88,6 +88,7 @@ private: expr_ref_vector& factors = poly.factors(); expr_ref_vector& coefficients = poly.coefficients(); expr_ref& coefficient = poly.coefficient(); + (void) coefficient; m_rw(term); diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp index 7f9827187..035326b26 100644 --- a/src/test/proof_checker.cpp +++ b/src/test/proof_checker.cpp @@ -11,7 +11,6 @@ void tst_checker1() { ast_manager m(PGM_FINE); expr_ref a(m); proof_ref p1(m), p2(m), p3(m), p4(m); - bool result; expr_ref_vector side_conditions(m); a = m.mk_const(symbol("a"), m.mk_bool_sort()); @@ -26,8 +25,7 @@ void tst_checker1() { proof_checker checker(m); p4 = m.mk_lemma(p3.get(), m.mk_or(a.get(), m.mk_not(a.get()))); ast_ll_pp(std::cout, m, p4.get()); - result = checker.check(p4.get(), side_conditions); - SASSERT(result); + VERIFY(checker.check(p4.get(), side_conditions)); } void tst_proof_checker() { diff --git a/src/test/rational.cpp b/src/test/rational.cpp index 834aab92f..ac478af98 100644 --- a/src/test/rational.cpp +++ b/src/test/rational.cpp @@ -196,7 +196,7 @@ static void tst2() { // get_int64, get_uint64 uint64 u1 = uint64_max.get_uint64(); uint64 u2 = UINT64_MAX; - SASSERT(u1 == u2); + VERIFY(u1 == u2); std::cout << "int64_max: " << int64_max << ", INT64_MAX: " << INT64_MAX << ", int64_max.get_int64(): " << int64_max.get_int64() << ", int64_max.get_uint64(): " << int64_max.get_uint64() << "\n"; SASSERT(int64_max.get_int64() == INT64_MAX); SASSERT(int64_min.get_int64() == INT64_MIN); diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp index aa717f371..54de5976a 100644 --- a/src/test/sat_user_scope.cpp +++ b/src/test/sat_user_scope.cpp @@ -35,6 +35,7 @@ static void add_clause(sat::solver& s, random_gen& r, trail_t& t) { } static void display_state(std::ostream& out, sat::solver& s, trail_t& t) { + (void)t; s.display(out); } diff --git a/src/test/simple_parser.cpp b/src/test/simple_parser.cpp index a5d4d8def..934552711 100644 --- a/src/test/simple_parser.cpp +++ b/src/test/simple_parser.cpp @@ -38,6 +38,7 @@ void tst_simple_parser() { TRACE("simple_parser", tout << mk_pp(r, m) << "\n";); p.parse_string("(+ x (* y x) x)", r); float vals[2] = { 2.0f, 3.0f }; + (void)vals; TRACE("simple_parser", tout << mk_pp(r, m) << "\n"; tout << "val: " << eval(r, 2, vals) << "\n";); diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index e7dcf2719..3d9815873 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -129,18 +129,18 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_mana tout << "fourier upper: " << um.sign_variations_at(fseq, uppers[i]) << "\n";); unsigned fsv_lower = um.sign_variations_at(fseq, lowers[i]); unsigned fsv_upper = um.sign_variations_at(fseq, uppers[i]); - SASSERT(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 || - um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 || + VERIFY(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 || + um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 || // fsv_lower - fsv_upper is an upper bound for the number of roots in the interval // fsv_upper - fsv_upper - num_roots is even // Recall that num_roots == 1 in the interval. - (fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0)); - + (fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0)); + // Double checking using Descartes bounds for the interval // Must use square free component. unsigned dab = um.descartes_bound_a_b(q_sqf.size(), q_sqf.c_ptr(), bqm, lowers[i], uppers[i]); TRACE("upolynomial", tout << "Descartes bound: " << dab << "\n";); - SASSERT(dab == 1); + VERIFY(dab == 1); } } std::cout << "\n"; @@ -499,7 +499,7 @@ static void tst_refinable(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a std::cout << "new (" << bqm.to_string(a) << ", " << bqm.to_string(b) << ")\n"; int sign_a = um.eval_sign_at(_p.size(), _p.c_ptr(), a); int sign_b = um.eval_sign_at(_p.size(), _p.c_ptr(), b); - SASSERT(sign_a != 0 && sign_b != 0 && sign_a == -sign_b); + VERIFY(sign_a != 0 && sign_b != 0 && sign_a == -sign_b); } else { std::cout << "new root: " << bqm.to_string(a) << "\n"; From cba9a160d3f4662fdebb75c6d5f4112afc11a216 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jul 2017 19:42:22 -0700 Subject: [PATCH 17/36] deal with warning messages Signed-off-by: Nikolaj Bjorner --- src/test/cnf_backbones.cpp | 2 ++ src/test/dl_context.cpp | 3 ++- src/test/polynorm.cpp | 3 ++- src/test/sat_user_scope.cpp | 5 ----- src/test/upolynomial.cpp | 4 ++-- 5 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index 14fc594b6..3fdf96f87 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -38,6 +38,7 @@ static void STD_CALL on_ctrl_c(int) { raise(SIGINT); } +#if 0 static void display_model(sat::solver const & s) { sat::model const & m = s.get_model(); for (unsigned i = 1; i < m.size(); i++) { @@ -49,6 +50,7 @@ static void display_model(sat::solver const & s) { } std::cout << "\n"; } +#endif static void display_status(lbool r) { switch (r) { diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index 99a0480a6..8a62dcb7d 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -15,11 +15,12 @@ using namespace datalog; void tst_dl_context() { - symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") }; return; #if 0 + symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") }; + const unsigned rel_cnt = sizeof(relations)/sizeof(symbol); const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog"; diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index 0bc9dfe3c..987d8e13b 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -89,6 +89,7 @@ private: expr_ref_vector& coefficients = poly.coefficients(); expr_ref& coefficient = poly.coefficient(); (void) coefficient; + (void) coefficients; m_rw(term); @@ -171,7 +172,7 @@ static expr_ref mk_mul(arith_util& arith, unsigned num_args, expr* const* args) static void nf(expr_ref& term) { ast_manager& m = term.get_manager(); - expr *e1, *e2; + expr *e1 = 0, *e2 = 0; th_rewriter rw(m); arith_util arith(m); diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp index 54de5976a..a271ce6bb 100644 --- a/src/test/sat_user_scope.cpp +++ b/src/test/sat_user_scope.cpp @@ -34,11 +34,6 @@ static void add_clause(sat::solver& s, random_gen& r, trail_t& t) { s.mk_clause(cls.size(), cls.c_ptr()); } -static void display_state(std::ostream& out, sat::solver& s, trail_t& t) { - (void)t; - s.display(out); -} - static void pop_user_scope(sat::solver& s, trail_t& t) { std::cout << "pop\n"; s.user_pop(1); diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index 3d9815873..43aefed99 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -164,7 +164,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m for (unsigned j = 0; j < roots.size(); j++) { if (to_rational(roots[j]) == r) { SASSERT(!visited[j]); - SASSERT(!found); + VERIFY(!found); found = true; visited[j] = true; } @@ -172,7 +172,7 @@ static void check_roots(mpbq_vector const & roots, mpbq_vector const & lowers, m for (unsigned j = 0; j < lowers.size(); j++) { unsigned j_prime = j + roots.size(); if (to_rational(lowers[j]) < r && r < to_rational(uppers[j])) { - SASSERT(!found); + VERIFY(!found); SASSERT(!visited[j_prime]); found = true; visited[j_prime] = true; From 41803ec1cf280ae9634389d17f99bf69a2b597ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jul 2017 19:55:38 -0700 Subject: [PATCH 18/36] fix trace/debug build for unreferenced variables Signed-off-by: Nikolaj Bjorner --- src/smt/theory_str.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index d8d130212..5d46b5349 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -5619,7 +5619,7 @@ namespace smt { } void theory_str::print_grounded_concat(expr * node, std::map, std::set > > & groundedMap) { - TRACE("str", tout << mk_pp(node, m) << std::endl;); + TRACE("str", tout << mk_pp(node, get_manager()) << std::endl;); if (groundedMap.find(node) != groundedMap.end()) { std::map, std::set >::iterator itor = groundedMap[node].begin(); for (; itor != groundedMap[node].end(); ++itor) { @@ -7515,7 +7515,7 @@ namespace smt { while (varItor != cut_var_map.end()) { std::stack & val = cut_var_map[varItor->m_key]; while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) { - TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout);); + // TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout);); // T_cut * aCut = val.top(); val.pop(); // dealloc(aCut); @@ -8828,7 +8828,7 @@ namespace smt { // break; } else { // debug - TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;); + // TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;); } } } @@ -9315,8 +9315,8 @@ namespace smt { << mk_ismt2_pp(makeupAssert, m) << std::endl;); assert_axiom(makeupAssert); } else { - TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) - << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); + // TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) + // << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); } } @@ -10334,7 +10334,7 @@ namespace smt { } if (duplicated && dupVar != NULL) { TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager()) - << " = " << mk_ismt2_pp(dupVar, m) << " (SKIP)" << std::endl;); + << " = " << mk_ismt2_pp(dupVar, get_manager()) << " (SKIP)" << std::endl;); continue; } else { eqcRepSet.insert(freeVar); From b14364a11759d563edd104922b7d38ccb22f20aa Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 5 Jul 2017 11:06:40 -0400 Subject: [PATCH 19/36] fix theory_str warnings: rename get_value() to get_arith_value() --- src/smt/theory_str.cpp | 15 ++++++++------- src/smt/theory_str.h | 4 ++-- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 5d46b5349..2e928af37 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1984,7 +1984,8 @@ namespace smt { return NULL; } - static inline std::string rational_to_string_if_exists(const rational & x, bool x_exists) { + // trace code helper + inline std::string rational_to_string_if_exists(const rational & x, bool x_exists) { if (x_exists) { return x.to_string(); } else { @@ -4651,7 +4652,7 @@ namespace smt { } } - bool theory_str::get_value(expr* e, rational& val) const { + bool theory_str::get_arith_value(expr* e, rational& val) const { if (opt_DisableIntegerTheoryIntegration) { TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;); return false; @@ -4780,7 +4781,7 @@ namespace smt { } }); - if (ctx.e_internalized(len) && get_value(len, val1)) { + if (ctx.e_internalized(len) && get_arith_value(len, val1)) { val += val1; TRACE("str", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has length " << val1 << std::endl;); } @@ -8439,7 +8440,7 @@ namespace smt { // check integer theory rational Ival; - bool Ival_exists = get_value(a, Ival); + bool Ival_exists = get_arith_value(a, Ival); if (Ival_exists) { TRACE("str", tout << "integer theory assigns " << mk_pp(a, m) << " = " << Ival.to_string() << std::endl;); // if that value is not -1, we can assert (str.to-int S) = Ival --> S = "Ival" @@ -8610,7 +8611,7 @@ namespace smt { rational lenValue; expr_ref concatlenExpr (mk_strlen(concat), m) ; bool allLeafResolved = true; - if (! get_value(concatlenExpr, lenValue)) { + if (! get_arith_value(concatlenExpr, lenValue)) { // the length fo concat is unresolved yet if (get_len_value(concat, lenValue)) { // but all leaf nodes have length information @@ -8647,7 +8648,7 @@ namespace smt { expr * var = *it; rational lenValue; expr_ref varlen (mk_strlen(var), m) ; - if (! get_value(varlen, lenValue)) { + if (! get_arith_value(varlen, lenValue)) { if (propagate_length_within_eqc(var)) { axiomAdded = true; } @@ -9479,7 +9480,7 @@ namespace smt { bool unrLenValue_exists = get_len_value(unrFunc, unrLenValue); tout << "unroll length: " << (unrLenValue_exists ? unrLenValue.to_string() : "?") << std::endl; rational cntInUnrValue; - bool cntHasValue = get_value(cntInUnr, cntInUnrValue); + bool cntHasValue = get_arith_value(cntInUnr, cntInUnrValue); tout << "unroll count: " << (cntHasValue ? cntInUnrValue.to_string() : "?") << " low = " << (low_exists ? low.to_string() : "?") diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 0bbc44ab8..7f39efa70 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -219,7 +219,7 @@ protected: /* * If DisableIntegerTheoryIntegration is set to true, * ALL calls to the integer theory integration methods - * (get_value, get_len_value, lower_bound, upper_bound) + * (get_arith_value, get_len_value, lower_bound, upper_bound) * will ignore what the arithmetic solver believes about length terms, * and will return no information. * @@ -464,7 +464,7 @@ protected: bool in_same_eqc(expr * n1, expr * n2); expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet); - bool get_value(expr* e, rational& val) const; + bool get_arith_value(expr* e, rational& val) const; bool get_len_value(expr* e, rational& val); bool lower_bound(expr* _e, rational& lo); bool upper_bound(expr* _e, rational& hi); From 465ed7d068938d5b87cd8ede517f0e93b4ffe67f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jul 2017 10:21:57 -0700 Subject: [PATCH 20/36] adding doc #1132 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 63f1d15ff..386fdd8a2 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -396,6 +396,33 @@ typedef enum The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3) + - Z3_OP_BSMUL_NO_OVFL: a predicate to check that bit-wise signed multiplication does not overflow. + Signed multiplication overflows if the operands have the same sign and the result of multiplication + does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow. + + - Z3_OP_BUMUL_NO_OVFL: check that bit-wise unsigned multiplication does not overflow. + Unsigned multiplication overflows if the result does not fit within the available bits. + \sa Z3_mk_bvmul_no_overflow. + + - Z3_OP_BSMUL_NO_UDFL: check that bit-wise signed multiplication does not underflow. + Signed multiplication underflows if the operands have opposite signs and the result of multiplication + does not fit within the avaialble bits. Z3_mk_bvmul_no_underflow. + + - Z3_OP_BSDIV_I: Binary signed division. + It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero. + + - Z3_OP_BUDIV_I: Binary unsigned division. + It has the same semantics as Z3_OP_BUDIV, but created in a context where the second operand can be assumed to be non-zero. + + - Z3_OP_BSREM_I: Binary signed remainder. + It has the same semantics as Z3_OP_BSREM, but created in a context where the second operand can be assumed to be non-zero. + + - Z3_OP_BUREM_I: Binary unsigned remainder. + It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero. + + - Z3_OP_BSMOD_I: Binary signed modulus. + It has the same semantics as Z3_OP_BSMOND, but created in a context where the second operand can be assumed to be non-zero. + - Z3_OP_PR_UNDEF: Undef/Null proof object. - Z3_OP_PR_TRUE: Proof for the expression 'true'. From d57494395c3929ade7f0fe5454ce249b1357fbc7 Mon Sep 17 00:00:00 2001 From: Daniel Perelman Date: Thu, 6 Jul 2017 16:59:20 -0700 Subject: [PATCH 21/36] Add --guardcf flag to mk_make.py to optionally enable Control Flow Guard. --- scripts/mk_util.py | 31 +++++++++++++++++++++---------- 1 file changed, 21 insertions(+), 10 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 3ce104709..a5f75fd1c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -104,6 +104,8 @@ GIT_DESCRIBE=False SLOW_OPTIMIZE=False USE_OMP=True LOG_SYNC=False +GUARD_CF=False +ALWAYS_DYNAMIC_BASE=False FPMATH="Default" FPMATH_FLAGS="-mfpmath=sse -msse -msse2" @@ -623,13 +625,13 @@ def display_help(exit_code): print(" -d, --debug compile Z3 in debug mode.") print(" -t, --trace enable tracing in release mode.") if IS_WINDOWS: + print(" --guardcf enable Control Flow Guard runtime checks.") print(" -x, --x64 create 64 binary when using Visual Studio.") else: print(" --x86 force 32-bit x86 build on x64 systems.") print(" -m, --makefiles generate only makefiles.") if IS_WINDOWS: print(" -v, --vsproj generate Visual Studio Project Files.") - if IS_WINDOWS: print(" --optimize generate optimized code during linking.") print(" --dotnet generate .NET bindings.") print(" --dotnet-key= sign the .NET assembly using the private key in .") @@ -670,10 +672,11 @@ def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, LOG_SYNC + global GUARD_CF, ALWAYS_DYNAMIC_BASE try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', - ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', + ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin', 'log-sync']) except: @@ -742,6 +745,9 @@ def parse_options(): elif opt in ('--python'): PYTHON_ENABLED = True PYTHON_INSTALL_ENABLED = True + elif opt == '--guardcf': + GUARD_CF = True + ALWAYS_DYNAMIC_BASE = True # /GUARD:CF requires /DYNAMICBASE else: print("ERROR: Invalid command line option '%s'" % opt) display_help(1) @@ -2310,6 +2316,7 @@ def mk_config(): 'SLINK_OUT_FLAG=/Fe\n' 'OS_DEFINES=/D _WINDOWS\n') extra_opt = '' + link_extra_opt = '' HAS_OMP = test_openmp('cl') if HAS_OMP: extra_opt = ' /openmp' @@ -2319,10 +2326,14 @@ def mk_config(): extra_opt = '%s /DZ3_LOG_SYNC' % extra_opt if GIT_HASH: extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) + if GUARD_CF: + extra_opt = ' %s /guard:cf' % extra_opt + link_extra_opt = ' %s /GUARD:CF' % link_extra_opt if STATIC_BIN: static_opt = '/MT' else: static_opt = '/MD' + maybe_disable_dynamic_base = '/DYNAMICBASE' if ALWAYS_DYNAMIC_BASE else '/DYNAMICBASE:NO' if DEBUG_MODE: static_opt = static_opt + 'd' config.write( @@ -2333,8 +2344,8 @@ def mk_config(): config.write( 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) elif VS_ARM: print("ARM on VS is unsupported") exit(1) @@ -2342,8 +2353,8 @@ def mk_config(): config.write( 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') + 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt)) else: # Windows Release mode LTCG=' /LTCG' if SLOW_OPTIMIZE else '' @@ -2358,8 +2369,8 @@ def mk_config(): config.write( 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' - 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG)) + 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 %s\n' + 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt)) elif VS_ARM: print("ARM on VS is unsupported") exit(1) @@ -2367,8 +2378,8 @@ def mk_config(): config.write( 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt)) config.write( - 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' - 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG)) + 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' + 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt)) From 49cf3f800836700add36a25fbe69bd2bf8bad9ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Jul 2017 07:44:55 -0700 Subject: [PATCH 22/36] update documentation according to #1058 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 5 ++++- src/tactic/goal.cpp | 7 ++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 386fdd8a2..505302dc1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5376,7 +5376,10 @@ extern "C" { /** \brief Add a new formula \c a to the given goal. - Conjunctions are split into separate formulas. + The formula is split according to the following procedure that is applied + until a fixed-point: + Conjunctions are split into separate formulas. + Negations are distributed over disjunctions, resulting in separate formulas. If the goal is \c false, adding new formulas is a no-op. If the formula \c a is \c true, then nothing is added. If the formula \c a is \c false, then the entire goal is replaced by the formula \c false. diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index b14d2676c..a3cac9e2e 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -137,7 +137,8 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) { } void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) { - if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) { + expr* g = 0; + if (!m().is_and(f) && !(m().is_not(f, g) && m().is_or(g))) { if (!save_first) { push_back(f, 0, d); } @@ -170,8 +171,8 @@ void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) { todo.push_back(expr_pol(t->get_arg(i), false)); } } - else if (m().is_not(curr)) { - todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol)); + else if (m().is_not(curr, g)) { + todo.push_back(expr_pol(g, !pol)); } else { if (!pol) { From d06e48a36163934c8058a1d7491c55a26c7e0a49 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Jul 2017 08:13:14 -0700 Subject: [PATCH 23/36] detect overlapping signatures #1134 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 26 +++++++++++++++++++++++--- src/cmd_context/cmd_context.h | 1 + 2 files changed, 24 insertions(+), 3 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index d252c3629..6a8b7f79b 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -72,14 +72,34 @@ void func_decls::finalize(ast_manager & m) { m_decls = 0; } +bool func_decls::signatures_collide(func_decl* f, func_decl* g) const { + if (f == g) { + return true; + } + if (f->get_arity() != g->get_arity() || f->get_range() == g->get_range()) { + return false; + } + for (unsigned i = 0; i < f->get_arity(); ++i) { + if (f->get_domain(i) != g->get_domain(i)) + return false; + } + // they have the same type arguments, but different range types. + return true; +} + bool func_decls::contains(func_decl * f) const { if (GET_TAG(m_decls) == 0) { - return UNTAG(func_decl*, m_decls) == f; + func_decl* g = UNTAG(func_decl*, m_decls); + if (!g) return false; + return signatures_collide(f, g); } else { func_decl_set * fs = UNTAG(func_decl_set *, m_decls); - return fs->contains(f); + for (func_decl* g : *fs) { + if (signatures_collide(f, g)) return true; + } } + return false; } bool func_decls::insert(ast_manager & m, func_decl * f) { @@ -661,7 +681,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) { msg += f->get_arity() == 0 ? "constant" : "function"; msg += " '"; msg += s.str(); - msg += "' (with the given signature) already declared"; + msg += "' (with the given signature) already declared with an overlapping signature"; throw cmd_exception(msg.c_str()); } if (s != f->get_name()) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index b231e3c82..74b2f3fbc 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -42,6 +42,7 @@ Notes: class func_decls { func_decl * m_decls; + bool signatures_collide(func_decl* f, func_decl* g) const; public: func_decls():m_decls(0) {} func_decls(ast_manager & m, func_decl * f); From ea331ebfbedf47381df1b3fd2ef296c850de3405 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Jul 2017 08:29:16 -0700 Subject: [PATCH 24/36] revert update to #1134 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 18 +++--------------- 1 file changed, 3 insertions(+), 15 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 6a8b7f79b..a053fc8e6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -73,25 +73,13 @@ void func_decls::finalize(ast_manager & m) { } bool func_decls::signatures_collide(func_decl* f, func_decl* g) const { - if (f == g) { - return true; - } - if (f->get_arity() != g->get_arity() || f->get_range() == g->get_range()) { - return false; - } - for (unsigned i = 0; i < f->get_arity(); ++i) { - if (f->get_domain(i) != g->get_domain(i)) - return false; - } - // they have the same type arguments, but different range types. - return true; + return f == g; } bool func_decls::contains(func_decl * f) const { if (GET_TAG(m_decls) == 0) { func_decl* g = UNTAG(func_decl*, m_decls); - if (!g) return false; - return signatures_collide(f, g); + return g && signatures_collide(f, g); } else { func_decl_set * fs = UNTAG(func_decl_set *, m_decls); @@ -681,7 +669,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) { msg += f->get_arity() == 0 ? "constant" : "function"; msg += " '"; msg += s.str(); - msg += "' (with the given signature) already declared with an overlapping signature"; + msg += "' (with the given signature) already declared"; throw cmd_exception(msg.c_str()); } if (s != f->get_name()) { From 5714f830b03208d8d47717d22963a4a8395d8364 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 8 Jul 2017 13:37:24 -0700 Subject: [PATCH 25/36] fix check for finite sorts #1122 Signed-off-by: Nikolaj Bjorner --- src/muz/base/rule_properties.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 518e848c4..247519d63 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -51,7 +51,8 @@ void rule_properties::collect(rule_set const& rules) { for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) { sort* d = r->get_decl()->get_domain(i); sort_size sz = d->get_num_elements(); - if (!sz.is_finite()) { + if (!sz.is_finite() && !m_dl.is_rule_sort(d)) { + TRACE("dl", tout << "sort " << mk_pp(d, m) << " is not finite " << sz << "\n";); m_inf_sort.push_back(m_rule); } } From 2af08a378d7759fc0a047125dadd80a295737c56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 8 Jul 2017 18:21:47 -0700 Subject: [PATCH 26/36] avoid complaining about division by 0 as unhandled in theory-lra Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.h | 2 ++ src/smt/theory_lra.cpp | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index beb227c33..6d6da9ed5 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -275,7 +275,9 @@ public: bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); } bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); } bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); } + bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); } bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); } + bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); } bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); } bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); } bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 2bd4844e8..9e4f544c1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -292,6 +292,9 @@ namespace smt { } void found_not_handled(expr* n) { + if (a.is_div0(n)) { + return; + } m_not_handled = n; if (is_app(n) && is_underspecified(to_app(n))) { m_underspecified.push_back(to_app(n)); From 2b0106c199a40500bb661c1afdf7818139ccd1d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 Jul 2017 11:26:27 +0200 Subject: [PATCH 27/36] doc fixes Signed-off-by: Nikolaj Bjorner --- doc/website.dox.in | 4 +--- src/api/java/Fixedpoint.java | 2 ++ src/api/python/z3/z3.py | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/website.dox.in b/doc/website.dox.in index 17a8552d1..f8659ec0b 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -4,9 +4,7 @@ Z3 is a high-performance theorem prover being developed at Microsoft Research. - The Z3 website moved to http://github.com/z3prover.. - - The old Z3 websites can be found here and here. + The Z3 website is at http://github.com/z3prover.. This website hosts the automatically generated documentation for the Z3 APIs. diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index ad6d5a658..7bb0fda58 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -88,6 +88,7 @@ public class Fixedpoint extends Z3Object /** * Add rule into the fixedpoint solver. * + * @param rule implication (Horn clause) representing rule * @param name Nullable rule name. * @throws Z3Exception **/ @@ -178,6 +179,7 @@ public class Fixedpoint extends Z3Object /** * Update named rule into in the fixedpoint solver. * + * @param rule implication (Horn clause) representing rule * @param name Nullable rule name. * @throws Z3Exception **/ diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 52cc2e858..9a1ebccf6 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -12,7 +12,7 @@ Several online tutorials for Z3Py are available at: http://rise4fun.com/Z3Py/tutorial/guide -Please send feedback, comments and/or corrections to leonardo@microsoft.com. Your comments are very valuable. +Please send feedback, comments and/or corrections on the Issue tracker for https://github.com/Z3prover/z3.git. Your comments are very valuable. Small example: From 6e2ca69654efae9fcddcad755aa5826448f1a8d2 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 9 Jul 2017 14:21:27 +0100 Subject: [PATCH 28/36] [CMake] Change the `WARNINGS_AS_ERRORS` option from BOOL to STRING to allow a new mode `SERIOUS_ONLY`. Modes: `ON` - All warnings are treated as errors (same as before) `OFF` - Warnings are not treated as errors (same as before) `SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors. Upgrade code is included to upgrade old CMake cache's to use the new type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The user's previous setting is preserved when doing this. Very few warnings are treated as errors for now. Developers can add more later as they see fit. --- README-CMake.md | 12 +++++ cmake/compiler_warnings.cmake | 96 +++++++++++++++++++++++++++++++++-- cmake/z3_add_cxx_flag.cmake | 11 ++-- 3 files changed, 111 insertions(+), 8 deletions(-) diff --git a/README-CMake.md b/README-CMake.md index 7550808fc..715cacad2 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -266,6 +266,8 @@ The following useful options can be passed to CMake whilst configuring. Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target. * ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled. * ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature. +* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` compiler warnings will not be treated as errors. + If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. @@ -381,3 +383,13 @@ It is tempting use file-globbing in ``CMakeLists.txt`` to find a set for files m use them as the sources to build a target. This however is a bad idea because it prevents CMake from knowing when it needs to rerun itself. This is why source file names are explicitly listed in the ``CMakeLists.txt`` so that when changes are made the source files used to build a target automatically triggers a rerun of CMake. Long story short. Don't use file globbing. + +### Serious warning flags + +By default the `WARNINGS_AS_ERRORS` flag is set to `SERIOUS_ONLY` which means +some warnings will be treated as errors. These warnings are controlled by the +relevant `*_WARNINGS_AS_ERRORS` list defined in +`cmake/compiler_warnings.cmake`. + +Additional warnings should only be added here if the warnings has no false +positives. diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index e02b28b2c..183f490dd 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -1,17 +1,61 @@ +################################################################################ +# Compiler warning flags +################################################################################ +# These are passed to relevant compiler provided they are supported set(GCC_AND_CLANG_WARNINGS - "-Wall" + "-Wall" ) set(GCC_ONLY_WARNINGS "") set(CLANG_ONLY_WARNINGS "") set(MSVC_WARNINGS "/W3") +################################################################################ +# Serious warnings +################################################################################ +# This declares the flags that are passed to the compiler when +# `WARNINGS_AS_ERRORS` is set to `SERIOUS_ONLY`. Only flags that are supported +# by the compiler are used. +# +# In effect this a "whitelist" approach where we explicitly tell the compiler +# which warnings we want to be treated as errors. The alternative would be a +# "blacklist" approach where we ask the compiler to treat all warnings are +# treated as errors but then we explicitly list which warnings which should be +# allowed. +# +# The "whitelist" approach seems simpiler because we can incrementally add +# warnings we "think are serious". + +# TODO: Add more warnings that are considered serious enough that we should +# treat them as errors. +set(GCC_AND_CLANG_WARNINGS_AS_ERRORS + # https://clang.llvm.org/docs/DiagnosticsReference.html#wodr + "-Werror=odr" +) +set(GCC_WARNINGS_AS_ERRORS + "" +) +set(CLANG_WARNINGS_AS_ERRORS + # https://clang.llvm.org/docs/DiagnosticsReference.html#wdelete-non-virtual-dtor + "-Werror=delete-non-virtual-dtor" + # https://clang.llvm.org/docs/DiagnosticsReference.html#woverloaded-virtual + "-Werror=overloaded-virtual" +) + +################################################################################ +# Test warning/error flags +################################################################################ set(WARNING_FLAGS_TO_CHECK "") +set(WARNING_AS_ERROR_FLAGS_TO_CHECK "") if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_WARNINGS_AS_ERRORS}) elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS}) + list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS}) # FIXME: Remove "x.." when CMP0054 is set to NEW elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS}) @@ -31,8 +75,40 @@ foreach (flag ${WARNING_FLAGS_TO_CHECK}) z3_add_cxx_flag("${flag}") endforeach() -option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF) -if (WARNINGS_AS_ERRORS) +# TODO: Remove this eventually. +# Detect legacy `WARNINGS_AS_ERRORS` boolean option and covert to new +# to new option type. +get_property( + WARNINGS_AS_ERRORS_CACHE_VAR_TYPE + CACHE + WARNINGS_AS_ERRORS + PROPERTY + TYPE +) +if ("${WARNINGS_AS_ERRORS_CACHE_VAR_TYPE}" STREQUAL "BOOL") + message(WARNING "Detected legacy WARNINGS_AS_ERRORS option. Upgrading") + set(WARNINGS_AS_ERRORS_DEFAULT "${WARNINGS_AS_ERRORS}") + # Delete old entry + unset(WARNINGS_AS_ERRORS CACHE) +else() + set(WARNINGS_AS_ERRORS_DEFAULT "SERIOUS_ONLY") +endif() + +set(WARNINGS_AS_ERRORS + ${WARNINGS_AS_ERRORS_DEFAULT} + CACHE STRING + "Treat warnings as errors. ON, OFF, or SERIOUS_ONLY" +) + # Set GUI options +set_property( + CACHE + WARNINGS_AS_ERRORS + PROPERTY STRINGS + "ON;OFF;SERIOUS_ONLY" +) + +if ("${WARNINGS_AS_ERRORS}" STREQUAL "ON") + message(STATUS "Treating compiler warnings as errors") if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror") # FIXME: Remove "x.." when CMP0054 is set to NEW @@ -41,8 +117,14 @@ if (WARNINGS_AS_ERRORS) else() message(AUTHOR_WARNING "Unknown compiler") endif() - message(STATUS "Treating compiler warnings as errors") -else() +elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "SERIOUS_ONLY") + message(STATUS "Treating only serious compiler warnings as errors") + # Loop through the flags + foreach (flag ${WARNING_AS_ERROR_FLAGS_TO_CHECK}) + # Add globally because some flags need to be passed at link time. + z3_add_cxx_flag("${flag}" GLOBAL) + endforeach() +elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "OFF") message(STATUS "Not treating compiler warnings as errors") # FIXME: Remove "x.." when CMP0054 is set to NEW if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") @@ -51,4 +133,8 @@ else() # build system. list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX-") endif() +else() + message(FATAL_ERROR + "WARNINGS_AS_ERRORS set to unsupported value \"${WARNINGS_AS_ERRORS}\"" + ) endif() diff --git a/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake index 6e756d3b9..d2624d890 100644 --- a/cmake/z3_add_cxx_flag.cmake +++ b/cmake/z3_add_cxx_flag.cmake @@ -2,7 +2,7 @@ include(CheckCXXCompilerFlag) include(CMakeParseArguments) function(z3_add_cxx_flag flag) - CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED" "" "" ${ARGN}) + CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED;GLOBAL" "" "" ${ARGN}) string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") @@ -16,8 +16,13 @@ function(z3_add_cxx_flag flag) endif() if (HAS_${SANITIZED_FLAG_NAME}) message(STATUS "C++ compiler supports ${flag}") - list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}") - set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE) + if (z3_add_flag_GLOBAL) + # Set globally + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag} " PARENT_SCOPE) + else() + list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}") + set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE) + endif() else() message(STATUS "C++ compiler does not support ${flag}") endif() From 630863619b926e1741f195a8ad0b2dd91a4fa4ee Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 9 Jul 2017 14:41:59 +0100 Subject: [PATCH 29/36] [TravisCI] Add `Z3_WARNINGS_AS_ERRORS` environment variable to control the `WARNINGS_AS_ERRORS` CMake option. --- contrib/ci/Dockerfiles/z3_build.Dockerfile | 2 ++ contrib/ci/README.md | 1 + contrib/ci/scripts/build_z3_cmake.sh | 4 +++- contrib/ci/scripts/travis_ci_linux_entry_point.sh | 7 +++++++ 4 files changed, 13 insertions(+), 1 deletion(-) diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 8b922edff..2d16d5394 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -28,6 +28,7 @@ ARG Z3_INSTALL_PREFIX=/usr ARG Z3_STATIC_BUILD=0 # Blank default indicates use latest. ARG Z3_SYSTEM_TEST_GIT_REVISION +ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY ARG Z3_VERBOSE_BUILD_OUTPUT=0 ENV \ @@ -55,6 +56,7 @@ ENV \ Z3_STATIC_BUILD=${Z3_STATIC_BUILD} \ Z3_SYSTEM_TEST_DIR=/home/user/z3_system_test \ Z3_SYSTEM_TEST_GIT_REVISION=${Z3_SYSTEM_TEST_GIT_REVISION} \ + Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \ Z3_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} # We add context across incrementally to maximal cache reuse diff --git a/contrib/ci/README.md b/contrib/ci/README.md index 31bb504b6..2e117c8b1 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -43,6 +43,7 @@ the future. * `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`) * `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`) * `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used. +* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option pased to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`) ### Linux diff --git a/contrib/ci/scripts/build_z3_cmake.sh b/contrib/ci/scripts/build_z3_cmake.sh index 98a9724c7..76fd0fb84 100755 --- a/contrib/ci/scripts/build_z3_cmake.sh +++ b/contrib/ci/scripts/build_z3_cmake.sh @@ -20,7 +20,8 @@ set -o pipefail : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} : ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} : ${USE_LTO?"USE_LTO must be specified"} -: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX"} +: ${Z3_INSTALL_PREFIX?"Z3_INSTALL_PREFIX must be specified"} +: ${Z3_WARNINGS_AS_ERRORS?"Z3_WARNINGS_AS_ERRORS must be specified"} ADDITIONAL_Z3_OPTS=() @@ -120,6 +121,7 @@ cmake \ -DCMAKE_BUILD_TYPE=${Z3_BUILD_TYPE} \ -DPYTHON_EXECUTABLE=${PYTHON_EXECUTABLE} \ -DCMAKE_INSTALL_PREFIX=${Z3_INSTALL_PREFIX} \ + -DWARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS} \ "${ADDITIONAL_Z3_OPTS[@]}" \ "${Z3_SRC_DIR}" diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index 21b97788f..84b2dd400 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -120,6 +120,13 @@ if [ -n "${NO_SUPPRESS_OUTPUT}" ]; then ) fi +if [ -n "${Z3_WARNINGS_AS_ERRORS}" ]; then + BUILD_OPTS+=( \ + "--build-arg" \ + "Z3_WARNINGS_AS_ERRORS=${Z3_WARNINGS_AS_ERRORS}" \ + ) +fi + case ${LINUX_BASE} in ubuntu_14.04) BASE_DOCKER_FILE="${DOCKER_FILE_DIR}/z3_base_ubuntu_14.04.Dockerfile" From 0e45777104e6da51ca717d1950bd8cbb72657857 Mon Sep 17 00:00:00 2001 From: Jack Feser Date: Tue, 11 Jul 2017 14:41:54 -0400 Subject: [PATCH 30/36] add get_num_scopes to python solver api --- src/api/python/z3/z3.py | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 9a1ebccf6..a16c1b92b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6054,6 +6054,24 @@ class Solver(Z3PPObject): """ Z3_solver_pop(self.ctx.ref(), self.solver, num) + def num_scopes(self): + """Return the current number of backtracking points. + + >>> s = Solver() + >>> s.num_scopes() + 0L + >>> s.push() + >>> s.num_scopes() + 1L + >>> s.push() + >>> s.num_scopes() + 2L + >>> s.pop() + >>> s.num_scopes() + 1L + """ + return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver) + def reset(self): """Remove all asserted constraints and backtracking points created using `push()`. From 89c8f1722f33556def93aa54c92c3f2e3141014e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 12 Jul 2017 12:53:10 +0100 Subject: [PATCH 31/36] Fix typo that prevented uses of `bvsmod_i` being parsed. --- src/ast/bv_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 03b4fe637..321943c72 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -732,7 +732,7 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("bvudiv_i", OP_BUDIV_I)); op_names.push_back(builtin_name("bvsrem_i", OP_BSREM_I)); op_names.push_back(builtin_name("bvurem_i", OP_BUREM_I)); - op_names.push_back(builtin_name("bvumod_i", OP_BSMOD_I)); + op_names.push_back(builtin_name("bvsmod_i", OP_BSMOD_I)); op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT)); op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT)); From 5b511f12b3465fa1e2757cee3b500f524f50856a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 12 Jul 2017 13:07:19 +0100 Subject: [PATCH 32/36] Fix minor typo in C API documentation --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 505302dc1..8d53c9255 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -421,7 +421,7 @@ typedef enum It has the same semantics as Z3_OP_BUREM, but created in a context where the second operand can be assumed to be non-zero. - Z3_OP_BSMOD_I: Binary signed modulus. - It has the same semantics as Z3_OP_BSMOND, but created in a context where the second operand can be assumed to be non-zero. + It has the same semantics as Z3_OP_BSMOD, but created in a context where the second operand can be assumed to be non-zero. - Z3_OP_PR_UNDEF: Undef/Null proof object. From da34de340d582784e0068eb6f287faa56b74a243 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 15 Jul 2017 20:25:13 +0100 Subject: [PATCH 33/36] Fixed bug in sat model converter. Fixes #1148. --- src/sat/sat_model_converter.cpp | 27 +++++++++++++++++++++++---- src/sat/sat_model_converter.h | 7 ++++--- src/sat/sat_solver.cpp | 17 +++++++++-------- src/sat/sat_solver/inc_sat_solver.cpp | 18 +++++++++--------- 4 files changed, 45 insertions(+), 24 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 8901c276f..525d084dc 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -32,7 +32,7 @@ namespace sat { void model_converter::reset() { m_entries.finalize(); } - + void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); @@ -46,7 +46,7 @@ namespace sat { literal_vector::const_iterator it2 = it->m_clauses.begin(); literal_vector::const_iterator end2 = it->m_clauses.end(); for (; it2 != end2; ++it2) { - literal l = *it2; + literal l = *it2; if (l == null_literal) { // end of clause if (!sat) { @@ -56,6 +56,7 @@ namespace sat { sat = false; continue; } + if (sat) continue; bool sign = l.sign(); @@ -125,7 +126,7 @@ namespace sat { } return ok; } - + model_converter::entry & model_converter::mk(kind k, bool_var v) { m_entries.push_back(entry(k, v)); entry & e = m_entries.back(); @@ -218,7 +219,7 @@ namespace sat { out << *it2; } out << ")"; - } + } out << ")\n"; } @@ -237,4 +238,22 @@ namespace sat { } } + unsigned model_converter::max_var(unsigned min) const { + unsigned result = min; + vector::const_iterator it = m_entries.begin(); + vector::const_iterator end = m_entries.end(); + for (; it != end; ++it) { + literal_vector::const_iterator lvit = it->m_clauses.begin(); + literal_vector::const_iterator lvend = it->m_clauses.end(); + for (; lvit != lvend; ++lvit) { + literal l = *lvit; + if (l != null_literal) { + if (l.var() > result) + result = l.var(); + } + } + } + return result; + } + }; diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index b89e6e784..eb2237707 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -26,7 +26,7 @@ namespace sat { \brief Stores eliminated variables and Blocked clauses. It uses these clauses to extend/patch the model produced for the simplified CNF formula. - + This information may also be used to support incremental solving. If new clauses are asserted into the SAT engine, then we can restore the state by re-asserting all clauses in the model @@ -50,7 +50,7 @@ namespace sat { m_kind(src.m_kind), m_clauses(src.m_clauses) { } - bool_var var() const { return m_var; } + bool_var var() const { return m_var; } kind get_kind() const { return static_cast(m_kind); } }; private: @@ -74,8 +74,9 @@ namespace sat { void copy(model_converter const & src); void collect_vars(bool_var_set & s) const; + unsigned max_var(unsigned min) const; }; - + }; #endif diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7f2b75830..fbfa0ec6b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2628,7 +2628,7 @@ namespace sat { unsigned j = 0; for (unsigned i = 0; i < clauses.size(); ++i) { clause & c = *(clauses[i]); - if (c.contains(lit)) { + if (c.contains(lit) || c.contains(~lit)) { detach_clause(c); del_clause(c); } @@ -2684,6 +2684,7 @@ namespace sat { w = max_var(m_clauses, w); w = max_var(true, w); w = max_var(false, w); + v = m_mc.max_var(w); for (unsigned i = 0; i < m_trail.size(); ++i) { if (m_trail[i].var() > w) w = m_trail[i].var(); } @@ -3150,9 +3151,9 @@ namespace sat { } } } - + // Algorithm 7: Corebased Algorithm with Chunking - + static void back_remove(sat::literal_vector& lits, sat::literal l) { for (unsigned i = lits.size(); i > 0; ) { --i; @@ -3176,7 +3177,7 @@ namespace sat { } } } - + static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector& conseq, unsigned K) { sat::literal_vector lambda; for (unsigned i = 0; i < vars.size(); i++) { @@ -3375,7 +3376,7 @@ namespace sat { if (check_inconsistent()) return l_false; unsigned num_iterations = 0; - extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); + extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); update_unfixed_literals(unfixed_lits, unfixed_vars); while (!unfixed_lits.empty()) { if (scope_lvl() > 1) { @@ -3390,7 +3391,7 @@ namespace sat { unsigned num_assigned = 0; lbool is_sat = l_true; for (; it != end; ++it) { - literal lit = *it; + literal lit = *it; if (value(lit) != l_undef) { ++num_fixed; if (lvl(lit) <= 1 && value(lit) == l_true) { @@ -3445,8 +3446,8 @@ namespace sat { << " iterations: " << num_iterations << " variables: " << unfixed_lits.size() << " fixed: " << conseq.size() - << " status: " << is_sat - << " pre-assigned: " << num_fixed + << " status: " << is_sat + << " pre-assigned: " << num_fixed << " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size() << ")\n";); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b6904ef02..baac9f37b 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -131,7 +131,7 @@ public: } bool is_literal(expr* e) const { - return + return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); } @@ -153,7 +153,7 @@ public: asm2fml.insert(assumptions[i], assumptions[i]); } } - + TRACE("sat", tout << _assumptions << "\n";); dep2asm_t dep2asm; m_model = 0; @@ -163,7 +163,7 @@ public: if (r != l_true) return r; r = m_solver.check(m_asms.size(), m_asms.c_ptr()); - + switch (r) { case l_true: if (sz > 0) { @@ -280,14 +280,14 @@ public: return r; } - // build map from bound variables to + // build map from bound variables to // the consequences that cover them. u_map bool_var2conseq; for (unsigned i = 0; i < lconseq.size(); ++i) { TRACE("sat", tout << lconseq[i] << "\n";); bool_var2conseq.insert(lconseq[i][0].var(), i); } - + // extract original fixed variables u_map asm2dep; extract_asm2dep(dep2asm, asm2dep); @@ -441,7 +441,7 @@ private: lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) { for (unsigned i = 0; i < vars.size(); ++i) { - internalize_var(vars[i], bvars); + internalize_var(vars[i], bvars); } return l_true; } @@ -453,7 +453,7 @@ private: bool internalized = false; if (is_uninterp_const(v) && m.is_bool(v)) { sat::bool_var b = m_map.to_bool_var(v); - + if (b != sat::null_bool_var) { bvars.push_back(b); internalized = true; @@ -479,7 +479,7 @@ private: else if (is_uninterp_const(v) && bvutil.is_bv(v)) { // variable does not occur in assertions, so is unconstrained. } - CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";); + CTRACE("sat", !internalized, tout << "unhandled variable " << mk_pp(v, m) << "\n";); return internalized; } @@ -506,7 +506,7 @@ private: } expr_ref val(m); expr_ref_vector conj(m); - internalize_value(value, v, val); + internalize_value(value, v, val); while (!premises.empty()) { expr* e = 0; VERIFY(asm2dep.find(premises.pop().index(), e)); From 943dc8118a3df069fb0674ca1c0b739d7f307ce7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 20 Jul 2017 13:44:47 +0100 Subject: [PATCH 34/36] Improved collect-statistics tactic --- src/tactic/core/collect_statistics_tactic.cpp | 40 ++++++++++++------- 1 file changed, 26 insertions(+), 14 deletions(-) diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index 8e8879fef..3b820de7a 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -47,10 +47,10 @@ class collect_statistics_tactic : public tactic { public: collect_statistics_tactic(ast_manager & m, params_ref const & p) : - m(m), + m(m), m_params(p) { - } - + } + virtual ~collect_statistics_tactic() {} virtual tactic * translate(ast_manager & m_) { @@ -60,21 +60,21 @@ public: virtual void updt_params(params_ref const & p) { m_params = p; } - + virtual void collect_param_descrs(param_descrs & r) {} virtual void operator()(goal_ref const & g, goal_ref_buffer & result, - model_converter_ref & mc, proof_converter_ref & pc, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { mc = 0; - tactic_report report("collect-statistics", *g); - + tactic_report report("collect-statistics", *g); + collect_proc cp(m, m_stats); - expr_mark visited; + expr_mark visited; const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) for_each_expr(cp, visited, g->form(i)); - + std::cout << "(" << std::endl; stats_type::iterator it = m_stats.begin(); stats_type::iterator end = m_stats.end(); @@ -84,7 +84,7 @@ public: g->inc_depth(); result.push_back(g.get()); - } + } virtual void cleanup() {} @@ -98,11 +98,12 @@ protected: class collect_proc { public: ast_manager & m; - stats_type & m_stats; + stats_type & m_stats; obj_hashtable m_seen_sorts; obj_hashtable m_seen_func_decls; + unsigned m_qdepth; - collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s) {} + collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s), m_qdepth(0) {} void operator()(var * v) { m_stats["bound-variables"]++; @@ -113,7 +114,18 @@ protected: m_stats["quantifiers"]++; SASSERT(is_app(q->get_expr())); app * body = to_app(q->get_expr()); + if (q->is_forall()) + m_stats["forall-variables"] += q->get_num_decls(); + else + m_stats["exists-variables"] += q->get_num_decls(); + m_stats["patterns"] += q->get_num_patterns(); + m_stats["no-patterns"] += q->get_num_no_patterns(); + m_qdepth++; + if (m_stats.find("max-quantification-depth") == m_stats.end() || + m_stats["max-quantification-depth"] < m_qdepth) + m_stats["max-quantification-depth"] = m_qdepth; this->operator()(body); + m_qdepth--; } void operator()(app * n) { @@ -121,7 +133,7 @@ protected: this->operator()(n->get_decl()); } - void operator()(sort * s) { + void operator()(sort * s) { if (m.is_uninterp(s)) { if (!m_seen_sorts.contains(s)) { m_stats["uninterpreted-sorts"]++; @@ -135,7 +147,7 @@ protected: std::stringstream ss; ss << "(declare-sort " << mk_ismt2_pp(s, m, prms) << ")"; m_stats[ss.str()]++; - + if (s->get_info()->get_num_parameters() > 0) { std::stringstream ssname; ssname << "(declare-sort (_ " << s->get_name() << " *))"; From faa19117e40fa6850318fa777f884e65a68aae1a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 21 Jul 2017 17:42:48 +0100 Subject: [PATCH 35/36] Fixed inconsistent state upon solver interruption. Partially fixes #951. --- src/smt/cached_var_subst.cpp | 25 ++++++++++++++++--------- src/smt/qi_queue.cpp | 36 ++++++++++++++++++------------------ src/smt/smt_quantifier.cpp | 4 ++-- src/smt/smt_quantifier.h | 4 ++-- 4 files changed, 38 insertions(+), 31 deletions(-) diff --git a/src/smt/cached_var_subst.cpp b/src/smt/cached_var_subst.cpp index 1db3aa0a6..c36eb6dd2 100644 --- a/src/smt/cached_var_subst.cpp +++ b/src/smt/cached_var_subst.cpp @@ -23,7 +23,7 @@ bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cache return false; if (k1->m_num_bindings != k2->m_num_bindings) return false; - for (unsigned i = 0; i < k1->m_num_bindings; i++) + for (unsigned i = 0; i < k1->m_num_bindings; i++) if (k1->m_bindings[i] != k2->m_bindings[i]) return false; return true; @@ -49,9 +49,9 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e new_key->m_qa = qa; new_key->m_num_bindings = num_bindings; - for (unsigned i = 0; i < num_bindings; i++) + for (unsigned i = 0; i < num_bindings; i++) new_key->m_bindings[i] = bindings[i]->get_owner(); - + instances::entry * entry = m_instances.insert_if_not_there2(new_key, 0); if (entry->get_data().m_key != new_key) { SASSERT(entry->get_data().m_value != 0); @@ -60,20 +60,27 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e result = entry->get_data().m_value; return; } - - m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result); + + SASSERT(entry->get_data().m_value == 0); + try { + m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result); + } + catch (...) { + // CMW: The var_subst reducer was interrupted and m_instances is + // in an inconsistent state; we need to remove (new_key, 0). + m_instances.remove(new_key); + throw; // Throw on to smt::qi_queue/smt::solver. + } + // cache result entry->get_data().m_value = result; // remove key from cache m_new_keys[num_bindings] = 0; - + // increment reference counters m_refs.push_back(qa); for (unsigned i = 0; i < new_key->m_num_bindings; i++) m_refs.push_back(new_key->m_bindings[i]); m_refs.push_back(result); } - - - diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 530d0ec88..70a3041d2 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -41,7 +41,7 @@ namespace smt { init_parser_vars(); m_vals.resize(15, 0.0f); } - + qi_queue::~qi_queue() { } @@ -50,7 +50,7 @@ namespace smt { if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) { // it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided. // throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str()); - + // using warning message instead warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str()); // Trying again with default function @@ -107,7 +107,7 @@ namespace smt { m_vals[SIZE] = static_cast(stat->get_size()); m_vals[DEPTH] = static_cast(stat->get_depth()); m_vals[GENERATION] = static_cast(generation); - m_vals[QUANT_GENERATION] = static_cast(stat->get_generation()); + m_vals[QUANT_GENERATION] = static_cast(stat->get_generation()); m_vals[WEIGHT] = static_cast(q->get_weight()); m_vals[VARS] = static_cast(q->get_num_decls()); m_vals[PATTERN_WIDTH] = pat ? static_cast(pat->get_num_args()) : 1.0f; @@ -118,7 +118,7 @@ namespace smt { TRACE("qi_queue_detail", for (unsigned i = 0; i < m_vals.size(); i++) { tout << m_vals[i] << " "; } tout << "\n";); return stat; } - + float qi_queue::get_cost(quantifier * q, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) { quantifier_stat * stat = set_values(q, pat, generation, min_top_generation, max_top_generation, 0); float r = m_evaluator(m_cost_function, m_vals.size(), m_vals.c_ptr()); @@ -132,11 +132,11 @@ namespace smt { float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.c_ptr()); return static_cast(r); } - + void qi_queue::insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) { quantifier * q = static_cast(f->get_data()); float cost = get_cost(q, pat, generation, min_top_generation, max_top_generation); - TRACE("qi_queue_detail", + TRACE("qi_queue_detail", tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight() << ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n"; for (unsigned i = 0; i < f->get_num_args(); i++) { @@ -157,7 +157,7 @@ namespace smt { quantifier * qa = static_cast(f->get_data()); if (curr.m_cost <= m_eager_cost_threshold) { - instantiate(curr); + instantiate(curr); } else if (m_params.m_qi_promote_unsat && m_checker.is_unsat(qa->get_expr(), f->get_num_args(), f->get_args())) { // do not delay instances that produce a conflict. @@ -193,7 +193,7 @@ namespace smt { // This nasty side-effect may change the behavior of Z3. m_manager.trace_stream() << " #" << bindings[i]->get_owner_id(); } - + #endif if (m_manager.proofs_enabled()) m_manager.trace_stream() << " #" << proof_id; @@ -233,7 +233,7 @@ namespace smt { if (m_manager.is_true(s_instance)) { TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager);); - if (m_manager.has_trace_stream()) + if (m_manager.has_trace_stream()) m_manager.trace_stream() << "[end-of-instance]\n"; return; @@ -278,7 +278,7 @@ namespace smt { pr1 = m_manager.mk_modus_ponens(qi_pr, rw); } else { - app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance); + app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance); proof * prs[1] = { pr.get() }; proof * cg = m_manager.mk_congruence(bare_lemma, bare_s_lemma, 1, prs); proof * rw = m_manager.mk_rewrite(bare_s_lemma, lemma); @@ -331,13 +331,13 @@ namespace smt { s.m_instances_lim = m_instances.size(); s.m_instantiated_trail_lim = m_instantiated_trail.size(); } - + void qi_queue::pop_scope(unsigned num_scopes) { unsigned new_lvl = m_scopes.size() - num_scopes; scope & s = m_scopes[new_lvl]; unsigned old_sz = s.m_instantiated_trail_lim; unsigned sz = m_instantiated_trail.size(); - for (unsigned i = old_sz; i < sz; i++) + for (unsigned i = old_sz; i < sz; i++) m_delayed_entries[m_instantiated_trail[i]].m_instantiated = false; m_instantiated_trail.shrink(old_sz); m_delayed_entries.shrink(s.m_delayed_entries_lim); @@ -359,7 +359,7 @@ namespace smt { } bool qi_queue::final_check_eh() { - TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold + TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold << ", scope_level: " << m_context.get_scope_level() << "\n";); if (m_params.m_qi_conservative_final_check) { bool init = false; @@ -379,7 +379,7 @@ namespace smt { entry & e = m_delayed_entries[i]; TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= min_cost) { - TRACE("qi_queue", + TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); @@ -389,13 +389,13 @@ namespace smt { } return result; } - + bool result = true; for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { - TRACE("qi_queue", + TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); @@ -443,7 +443,7 @@ namespace smt { quantifier * qa = *it2; delayed_qa_info info; qa2info.find(qa, info); - out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n"; + out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n"; } } @@ -482,6 +482,6 @@ namespace smt { } #endif } - + }; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 10e2df988..1c8f94edf 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -135,7 +135,7 @@ namespace smt { m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_num_instances++; } - TRACE("quantifier", + TRACE("quantifier", tout << mk_pp(q, m()) << " "; for (unsigned i = 0; i < num_bindings; ++i) { tout << mk_pp(bindings[i]->get_owner(), m()) << " "; @@ -372,7 +372,7 @@ namespace smt { quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh(); m_imp->~imp(); m_imp = new (m_imp) imp(*this, ctx, p, plugin); - plugin->set_manager(*this); + plugin->set_manager(*this); } void quantifier_manager::display(std::ostream & out) const { diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 6dcf20583..96af9909a 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -75,7 +75,7 @@ namespace smt { }; bool model_based() const; - bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? + bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? void adjust_model(proto_model * m); check_model_result check_model(proto_model * m, obj_map const & root2value); @@ -167,7 +167,7 @@ namespace smt { virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; - + }; }; From 0f1583309d0813e87d6003fe46cf8bb32899d773 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 21 Jul 2017 21:12:45 +0100 Subject: [PATCH 36/36] Bugfix for fp.fma. One piece of puzzle #872. --- src/ast/fpa/fpa2bv_converter.cpp | 35 ++++++++++++++++++++++++++------ 1 file changed, 29 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 2c0ba1ce1..99b8c5ac8 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1632,8 +1632,6 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, res_exp = e_exp; - // Result could overflow into 4.xxx ... - family_id bvfid = m_bv_util.get_fid(); expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m); @@ -1646,11 +1644,34 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); + // Result could have overflown into 4.xxx. + SASSERT(m_bv_util.get_bv_size(sig_abs) == 2 * sbits + 2); + expr_ref ovfl_into_4(m); + ovfl_into_4 = m.mk_eq(m_bv_util.mk_extract(2 * sbits + 1, 2 * sbits, sig_abs), + m_bv_util.mk_numeral(1, 2)); + dbg_decouple("fpa2bv_fma_ovfl_into_4", ovfl_into_4); if (sbits > 5) { - sticky_raw = m_bv_util.mk_extract(sbits - 5, 0, sig_abs); - sticky = m_bv_util.mk_zero_extend(sbits + 3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get())); - expr * res_or_args[2] = { m_bv_util.mk_extract(2 * sbits - 1, sbits - 4, sig_abs), sticky }; - res_sig = m_bv_util.mk_bv_or(2, res_or_args); + expr_ref sticky_raw(m), sig_upper(m), sticky_redd(m), res_sig_norm(m); + sticky_raw = m_bv_util.mk_extract(sbits - 4, 0, sig_abs); + sig_upper = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs); + SASSERT(m_bv_util.get_bv_size(sig_upper) == sbits + 4); + sticky_redd = m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()); + sticky = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd); + expr * res_or_args[2] = { sig_upper, sticky }; + res_sig_norm = m_bv_util.mk_bv_or(2, res_or_args); + + expr_ref sticky_raw_ovfl(m), sig_upper_ovfl(m), sticky_redd_ovfl(m), sticky_ovfl(m), res_sig_ovfl(m); + sticky_raw_ovfl = m_bv_util.mk_extract(sbits - 4, 0, sig_abs); + sig_upper_ovfl = m_bv_util.mk_extract(2 * sbits, sbits - 3, sig_abs); + SASSERT(m_bv_util.get_bv_size(sig_upper_ovfl) == sbits + 4); + sticky_redd_ovfl = m.mk_app(bvfid, OP_BREDOR, sticky_raw_ovfl.get()); + sticky_ovfl = m_bv_util.mk_zero_extend(sbits + 3, sticky_redd_ovfl); + expr * res_or_args_ovfl[2] = { sig_upper_ovfl, sticky_ovfl }; + res_sig_ovfl = m_bv_util.mk_bv_or(2, res_or_args_ovfl); + + res_sig = m.mk_ite(ovfl_into_4, res_sig_ovfl, res_sig_norm); + res_exp = m.mk_ite(ovfl_into_4, m_bv_util.mk_bv_add(res_exp, m_bv_util.mk_numeral(1, ebits+2)), + res_exp); } else { unsigned too_short = 6 - sbits; @@ -1658,6 +1679,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, res_sig = m_bv_util.mk_extract(sbits + 3, 0, sig_abs); } dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky); + dbg_decouple("fpa2bv_fma_sig_abs", sig_abs); + dbg_decouple("fpa2bv_fma_res_sig", res_sig); SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4); expr_ref is_zero_sig(m), nil_sbits4(m);