From 442d1d28ea5f51d208bb0e39b24fe6b0006f28f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Jul 2021 19:11:16 -0700 Subject: [PATCH 1/4] #5429 --- src/sat/tactic/goal2sat.cpp | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 72b825a09..123eacee5 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -544,6 +544,29 @@ struct goal2sat::imp : public sat::sat_internalizer { } } + void convert_not(app* t, bool root, bool sign) { + SASSERT(t->get_num_args() == 1); + unsigned sz = m_result_stack.size(); + SASSERT(sz >= 1); + sat::literal lit = m_result_stack[sz - 1]; + m_result_stack.shrink(sz - 1); + if (root) { + SASSERT(sz == 1); + mk_root_clause(sign ? lit : ~lit); + } + else { + sat::bool_var k = add_var(false, t); + sat::literal l(k, false); + cache(t, l); + // l <=> ~lit + mk_clause(lit, l); + mk_clause(~lit, ~l); + if (sign) + l.neg(); + m_result_stack.push_back(l); + } + } + void convert_implies(app* t, bool root, bool sign) { SASSERT(t->get_num_args() == 2); unsigned sz = m_result_stack.size(); @@ -702,6 +725,9 @@ struct goal2sat::imp : public sat::sat_internalizer { case OP_IMPLIES: convert_implies(t, root, sign); break; + case OP_NOT: + convert_not(t, root, sign); + break; default: UNREACHABLE(); } @@ -767,7 +793,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_frame_stack.pop_back(); continue; } - if (m.is_not(t)) { + if (m.is_not(t) && !m.is_not(t->get_arg(0))) { m_frame_stack.pop_back(); visit(t->get_arg(0), root, !sign); continue; From 81b8f397b3dfd510aed918c775ca35d5a8923f24 Mon Sep 17 00:00:00 2001 From: Kiwamu Okabe Date: Thu, 29 Jul 2021 08:57:26 +0900 Subject: [PATCH 2/4] Need `-thread` option to compile OCaml example (#5440) I can compile the OCaml example with `-thread` option at Linux. ``` $ ocaml --version The OCaml toplevel, version 4.05.0 ``` --- examples/ml/README | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/ml/README b/examples/ml/README index 9797b85e3..a8d03eaea 100644 --- a/examples/ml/README +++ b/examples/ml/README @@ -14,9 +14,9 @@ for the byte-code version. If Z3 was installed into the ocamlfind package repository (see src/api/ml/README), then we can also compile this example as follows: -ocamlfind ocamlc -o ml_example.byte -package Z3 -linkpkg ml_example.ml +ocamlfind ocamlc -o ml_example.byte -thread -package Z3 -linkpkg ml_example.ml or -ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml +ocamlfind ocamlopt -o ml_example -thread -package Z3 -linkpkg ml_example.ml Note that the resulting binaries depend on the shared z3 library (libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH From 703659a3a88d2b7e2f03b2905ebacf3fb75330e3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Jul 2021 17:15:55 -0700 Subject: [PATCH 3/4] fix #5439 --- src/ast/recfun_decl_plugin.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index bd23e1838..04c5d0545 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -338,7 +338,9 @@ namespace recfun { void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { - expr_ref rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs); + expr_ref rhs1(rhs, m()); + if (!is_macro) + rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs); d.set_definition(subst, is_macro, n_vars, vars, rhs1); } From 72d3074a440b1eaa9eb24bc663d314ab49df9eb5 Mon Sep 17 00:00:00 2001 From: 0152la Date: Thu, 29 Jul 2021 19:29:49 +0100 Subject: [PATCH 4/4] Add Ubuntu CMake Coverage CI step (#5442) Adds an extra step to CI jobs which executes the Z3 test suite with coverage enabled, and additionally executed coverage-enhancing tests added to z3test. --- azure-pipelines.yml | 25 +++++++++++++++++++++++++ scripts/test-regressions-coverage.yaml | 4 ++++ 2 files changed, 29 insertions(+) create mode 100644 scripts/test-regressions-coverage.yaml diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 1735f2337..3db84ce71 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -5,6 +5,7 @@ variables: cmakeNet: '-DZ3_BUILD_DOTNET_BINDINGS=True' cmakePy: '-DZ3_BUILD_PYTHON_BINDINGS=True' cmakeStdArgs: '-DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../' + cmakeCovArgs: '-DCMAKE_INSTALL_PREFIX=./install -G "Ninja" ../' asanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"' ubsanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" CFLAGS="${CFLAGS} -fsanitize=undefined"' msanEnv: 'CC=clang LDFLAGS="-L../libcxx/libcxx_msan/lib -lc++abi -Wl,-rpath=../libcxx/libcxx_msan/lib" CXX=clang++ CXXFLAGS="${CXXFLAGS} -stdlib=libc++ -fsanitize-memory-track-origins -fsanitize=memory -fPIE -fno-omit-frame-pointer -g -O2" CFLAGS="${CFLAGS} -stdlib=libc -fsanitize=memory -fsanitize-memory-track-origins -fno-omit-frame-pointer -g -O2"' @@ -150,6 +151,30 @@ jobs: - ${{if eq(variables['runTests'], 'True')}}: - template: scripts/test-regressions.yml + +- job: "Ubuntu16CMakeCoverage" + displayName: "Ubuntu build - cmake w/ coverage" + pool: + vmImage: "ubuntu-latest" + steps: + - script: sudo apt-get install ninja-build + - script: | + set -e + mkdir build + cd build + CXXFLAGS=--coverage LDFLAGS=-lgcov CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Debug $(cmakeCovArgs) + ninja + ninja test-z3 + ninja install + cd .. + - script: | + cd build + ./test-z3 -a + cd .. + - template: scripts/test-examples-cmake.yml + - template: scripts/test-regressions-coverage.yml + + - job: "WindowsLatest" displayName: "Windows" pool: diff --git a/scripts/test-regressions-coverage.yaml b/scripts/test-regressions-coverage.yaml new file mode 100644 index 000000000..363ea2c19 --- /dev/null +++ b/scripts/test-regressions-coverage.yaml @@ -0,0 +1,4 @@ +steps: +- script: git clone https://github.com/z3prover/z3test z3test +- script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2 +- script: python z3test/scripts/test_coverage_tests.py build/install z3test/coverage/cpp