From c8a67abdd70550cbab22bafd259a21f68433da7c Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 25 Sep 2017 14:33:20 -0700 Subject: [PATCH 1/4] fixing issue [1269] --- src/interp/iz3mgr.cpp | 29 +++++++++++++++++++++++++++++ src/interp/iz3mgr.h | 6 ++++++ src/interp/iz3proof_itp.cpp | 4 ++-- src/interp/iz3translate.cpp | 5 +++++ 4 files changed, 42 insertions(+), 2 deletions(-) diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 306807f1f..7314403b0 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -33,9 +33,11 @@ #include #include #include +#include #include "ast/expr_abstract.h" #include "util/params.h" +#include "ast/used_vars.h" using namespace stl_ext; @@ -938,3 +940,30 @@ void iz3mgr::get_bound_substitutes(stl_ext::hash_map &memo, const ast } #endif + +unsigned iz3mgr::num_free_variables(const ast &e){ + used_vars uv; + uv(to_expr(e.raw())); + return uv.get_num_vars(); +} + +iz3mgr::ast iz3mgr::close_universally (ast e){ + used_vars uv; + uv(to_expr(e.raw())); + std::vector bvs; + stl_ext::hash_map subst_memo; + for (unsigned i = 0; i < uv.get_max_found_var_idx_plus_1(); i++){ + if (uv.get(i)) { + std::ostringstream os; + os << "%%" << i; + ast c = make_var(os.str(),uv.get(i)); + ast v = cook(m().mk_var(i,uv.get(i))); + subst_memo[v] = c; + bvs.push_back(c); + } + } + e = subst(subst_memo,e); + for (unsigned i = 0; i < bvs.size(); i++) + e = apply_quant(Forall,bvs[i],e); + return e; +} diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index e6e08f84d..6ca8fae34 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -661,6 +661,12 @@ class iz3mgr { ast apply_quant(opr quantifier, ast var, ast e); + // Universally quantify all the free variables in a formula. + // Makes up names for the quntifiers. + + ast close_universally (ast e); + + unsigned num_free_variables(const ast &e); /** For debugging */ void show(ast); diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index eb7f8e325..fc9d0fac6 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2968,9 +2968,9 @@ class iz3proof_itp_impl : public iz3proof_itp { ast interpolate(const node &pf){ // proof of false must be a formula, with quantified symbols #ifndef BOGUS_QUANTS - return add_quants(z3_simplify(pf)); + return close_universally(add_quants(z3_simplify(pf))); #else - return z3_simplify(pf); + return close_universally(z3_simplify(pf)); #endif } diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index ebbee46ca..c59dd0178 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -234,6 +234,11 @@ public: } } + // if(!range_is_empty(rng)){ + // if (num_free_variables(con) > 0) + // rng = range_empty(); + // } + if(res == INT_MAX){ if(range_is_empty(rng)) res = -1; From f07b89df867b29f3dc16633a94f5e204c97fae90 Mon Sep 17 00:00:00 2001 From: Max ulidtko Date: Tue, 26 Sep 2017 17:27:47 +0300 Subject: [PATCH 2/4] fix pydoc part of `make api_docs` --- doc/mk_api_doc.py | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 234dd670c..d7e8e2fb1 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -288,8 +288,21 @@ try: # Put z3py at the beginning of the search path to try to avoid picking up # an installed copy of Z3py. sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) - pydoc.writedoc('z3') - shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) + for modulename in ( + 'z3', + 'z3.z3consts', + 'z3.z3core', + 'z3.z3num', + 'z3.z3poly', + 'z3.z3printer', + 'z3.z3rcf', + 'z3.z3types', + 'z3.z3util', + ): + pydoc.writedoc(modulename) + doc = modulename + '.html' + shutil.move(doc, os.path.join(OUTPUT_DIRECTORY, 'html', doc)) + print("Generated pydoc Z3Py documentation.") if ML_ENABLED: From ce6e26043af3ec3f1e857ab1cfacd6158a472589 Mon Sep 17 00:00:00 2001 From: Max ulidtko Date: Wed, 27 Sep 2017 14:03:38 +0300 Subject: [PATCH 3/4] fix Python API doxygen (`make api_docs`) --- doc/mk_api_doc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index d7e8e2fb1..ab4d32d39 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -188,7 +188,7 @@ try: if Z3PY_ENABLED: print("Z3Py documentation enabled") - doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3.py' + doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3*.py' else: print("Z3Py documentation disabled") doxygen_config_substitutions['PYTHON_API_FILES'] = '' From 9a464dded4a0208d29ff604cb91ccf0fbd9e665b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 27 Sep 2017 14:22:59 +0100 Subject: [PATCH 4/4] Removed -std=c++11 from OCaml stubs build command. Fixes #1263. --- scripts/mk_util.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 24f22d8ee..6f3052f6e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1913,7 +1913,11 @@ class MLComponent(Component): src_dir = self.to_src_dir mk_dir(os.path.join(BUILD_DIR, self.sub_dir)) api_src = get_component(API_COMPONENT).to_src_dir - out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it. + # remove /GL and -std=c++11; the ocaml tools don't like them. + if IS_WINDOWS: + out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') + else: + out.write('CXXFLAGS_OCAML=$(subst -std=c++11,,$(CXXFLAGS))\n') if IS_WINDOWS: prefix_lib = '-L' + os.path.abspath(BUILD_DIR).replace('\\', '\\\\')