From 9cd974e3343b83491200071442537d7765f48ad7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Sep 2017 09:40:35 -0700 Subject: [PATCH 01/41] remove display Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 63f1badb7..8782cb462 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -724,8 +724,6 @@ namespace sat { pop_to_base_level(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(scope_lvl() == 0); - SASSERT(m_config.m_dimacs_display); - std::cout << "display dimacs: " << m_config.m_dimacs_display << "\n"; if (m_config.m_dimacs_display) { display_dimacs(std::cout); for (unsigned i = 0; i < num_lits; ++lits) { From f179d49f4f4ac90e9515f42ee690426c5a67fa52 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Sep 2017 10:58:39 -0700 Subject: [PATCH 02/41] check for eof, based on testing garbled repro from #1267 Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2scanner.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index c1cc40b2b..9a9e69b67 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -124,7 +124,7 @@ namespace smt2 { next(); bool is_float = false; - while (true) { + while (!m_at_eof) { char c = curr(); if ('0' <= c && c <= '9') { m_number = rational(10)*m_number + rational(c - '0'); From c8a67abdd70550cbab22bafd259a21f68433da7c Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 25 Sep 2017 14:33:20 -0700 Subject: [PATCH 03/41] 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 6450ee33c58a9dc5e86b7a7b852af46277ce16d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2017 08:25:48 -0700 Subject: [PATCH 04/41] disregard model validation when source expression contains uninterpreted theory functions Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 260d49174..3f34f3128 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1763,7 +1763,7 @@ void cmd_context::validate_model() { continue; } try { - for_each_expr(contains_underspecified, r); + for_each_expr(contains_underspecified, a); } catch (contains_underspecified_op_proc::found) { continue; From 2229a2fc1b07e733bbb69bd3f997cfd259134ca7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2017 08:43:31 -0700 Subject: [PATCH 05/41] model validation update take 2 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3f34f3128..b2a4fc47f 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1764,6 +1764,7 @@ void cmd_context::validate_model() { } try { for_each_expr(contains_underspecified, a); + for_each_expr(contains_underspecified, r); } catch (contains_underspecified_op_proc::found) { continue; From f07b89df867b29f3dc16633a94f5e204c97fae90 Mon Sep 17 00:00:00 2001 From: Max ulidtko Date: Tue, 26 Sep 2017 17:27:47 +0300 Subject: [PATCH 06/41] 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 07/41] 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 08/41] 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('\\', '\\\\') From 8ff8c6433b9c377bae84c5c72084eefa3fbded3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Sep 2017 10:15:27 -0700 Subject: [PATCH 09/41] fix #1277 fix #1278 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 6 ++++++ src/smt/theory_arith_nl.h | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index b2a4fc47f..95c030687 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -870,6 +870,12 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s lhs = m().mk_app(f, binding.size(), binding.c_ptr()); eq = m().mk_eq(lhs, e); if (!ids.empty()) { + if (is_var(e)) { + ptr_vector domain; + for (expr* b : binding) domain.push_back(m().get_sort(b)); + insert_macro(f->get_name(), domain.size(), domain.c_ptr(), e); + return; + } if (!is_app(e)) { throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)"); } diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index a04c34706..230b6de77 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -780,7 +780,7 @@ namespace smt { of a non linear monomial that is not satisfied by the current assignment. if v >= l, then create the case split v >= l+1 else v <= u, then create the case split v <= u-1 - else do nothing and return false. + else create the bound v = 0 and case split on it. */ template bool theory_arith::branch_nl_int_var(theory_var v) { From bec60f763bbe8daf87413088f19a4b7c23ba7e5c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Sep 2017 12:35:36 -0700 Subject: [PATCH 10/41] add diagnostics to DDNF and fix #1268 Signed-off-by: Nikolaj Bjorner --- src/muz/ddnf/ddnf.cpp | 21 ++++++++++++++++----- src/test/ddnf.cpp | 4 ++++ 2 files changed, 20 insertions(+), 5 deletions(-) diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp index 0e2f6b35f..da1f5392b 100644 --- a/src/muz/ddnf/ddnf.cpp +++ b/src/muz/ddnf/ddnf.cpp @@ -192,10 +192,15 @@ namespace datalog { for (unsigned i = 0; i < new_tbvs.size(); ++i) { tbv const& nt = *new_tbvs[i]; IF_VERBOSE(10, m_tbv.display(verbose_stream() << "insert: ", nt); verbose_stream() << "\n";); - if (contains(nt)) continue; - ddnf_node* n = alloc(ddnf_node, *this, m_tbv, nt, m_noderefs.size()); - m_noderefs.push_back(n); - m_nodes.insert(n); + ddnf_node* n; + if (contains(nt)) { + n = find(nt); + } + else { + n = alloc(ddnf_node, *this, m_tbv, nt, m_noderefs.size()); + m_noderefs.push_back(n); + m_nodes.insert(n); + } insert(*m_root, n, new_tbvs); } return find(t); @@ -275,13 +280,17 @@ namespace datalog { void insert(ddnf_node& root, ddnf_node* new_n, ptr_vector& new_intersections) { tbv const& new_tbv = new_n->get_tbv(); + IF_VERBOSE(10, m_tbv.display(verbose_stream() << "root: ", root.get_tbv()); + m_tbv.display(verbose_stream() << " new node ", new_tbv); verbose_stream() << "\n";); SASSERT(m_tbv.contains(root.get_tbv(), new_tbv)); - if (&root == new_n) return; + if (m_eq(&root, new_n)) return; ++m_stats.m_num_inserts; bool inserted = false; for (unsigned i = 0; i < root.num_children(); ++i) { ddnf_node& child = *(root[i]); ++m_stats.m_num_comparisons; + IF_VERBOSE(10, m_tbv.display(verbose_stream() << "child ", child.get_tbv()); + verbose_stream() << " contains: " << m_tbv.contains(child.get_tbv(), new_tbv) << "\n";); if (m_tbv.contains(child.get_tbv(), new_tbv)) { inserted = true; insert(child, new_n, new_intersections); @@ -299,11 +308,13 @@ namespace datalog { // checking for subset if (m_tbv.contains(new_tbv, child.get_tbv())) { subset_children.push_back(&child); + IF_VERBOSE(10, m_tbv.display(verbose_stream() << "contains child", child.get_tbv()); verbose_stream() << "\n";); ++m_stats.m_num_comparisons; } else if (m_tbv.intersect(child.get_tbv(), new_tbv, *intr)) { // this means there is a non-full intersection new_intersections.push_back(intr); + IF_VERBOSE(10, m_tbv.display(verbose_stream() << "intersect child ", child.get_tbv()); verbose_stream() << "\n";); intr = m_tbv.allocate(); m_stats.m_num_comparisons += 2; } diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index 09f1a4cf9..c9eb6aa08 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -214,6 +214,10 @@ void tst_ddnf1() { ddnf.insert(*tX1); ddnf.insert(*t1X); ddnf.display(std::cout); + tbvm.deallocate(tXX); + tbvm.deallocate(t1X); + tbvm.deallocate(tX1); + tbvm.deallocate(t11); } From 05428314be0a3b7bd6b682d0467efa0fe892c9d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Oct 2017 15:13:43 -0700 Subject: [PATCH 11/41] fix #1276 related crashes for re-sumption after cancellation Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/maximize_ac_sharing.cpp | 4 ---- src/smt/asserted_formulas.cpp | 7 ++++--- src/smt/smt_context.cpp | 11 ++++++++++- src/util/rlimit.cpp | 5 +++-- src/util/rlimit.h | 15 ++++++++++++++- 5 files changed, 31 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp index b560132db..d7e8df7a2 100644 --- a/src/ast/rewriter/maximize_ac_sharing.cpp +++ b/src/ast/rewriter/maximize_ac_sharing.cpp @@ -151,11 +151,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) { } void maximize_ac_sharing::reset() { - restore_entries(0); - m_entries.reset(); m_cache.reset(); - m_region.reset(); - m_scopes.reset(); } void maximize_bv_sharing::init_core() { diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index c52ad851c..11cc846b8 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -170,7 +170,7 @@ void asserted_formulas::get_assertions(ptr_vector & result) const { void asserted_formulas::push_scope() { SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled()); - TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";); m_scoped_substitution.push(); m_scopes.push_back(scope()); scope & s = m_scopes.back(); @@ -181,10 +181,11 @@ void asserted_formulas::push_scope() { m_bv_sharing.push_scope(); m_macro_manager.push_scope(); commit(); + TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";); } void asserted_formulas::pop_scope(unsigned num_scopes) { - TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";); m_bv_sharing.pop_scope(num_scopes); m_macro_manager.pop_scope(num_scopes); unsigned new_lvl = m_scopes.size() - num_scopes; @@ -196,7 +197,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) { m_qhead = s.m_formulas_lim; m_scopes.shrink(new_lvl); flush_cache(); - TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n";); } void asserted_formulas::reset() { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 901f4b5ac..ac7b1f44b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -487,6 +487,7 @@ namespace smt { */ void context::add_eq(enode * n1, enode * n2, eq_justification js) { unsigned old_trail_size = m_trail_stack.size(); + scoped_suspend_rlimit _suspend_cancel(m_manager.limit()); try { TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); @@ -541,10 +542,14 @@ namespace smt { mark_as_relevant(r1); } + TRACE("add_eq", tout << "to trail\n";); + push_trail(add_eq_trail(r1, n1, r2->get_num_parents())); + TRACE("add_eq", tout << "qmanager add_eq\n";); m_qmanager->add_eq_eh(r1, r2); + TRACE("add_eq", tout << "merge theory_vars\n";); merge_theory_vars(n2, n1, js); // 'Proof' tree @@ -577,6 +582,7 @@ namespace smt { #endif + TRACE("add_eq", tout << "remove_parents_from_cg_table\n";); remove_parents_from_cg_table(r1); enode * curr = r1; @@ -588,8 +594,10 @@ namespace smt { SASSERT(r1->get_root() == r2); + TRACE("add_eq", tout << "reinsert_parents_into_cg_table\n";); reinsert_parents_into_cg_table(r1, r2, n1, n2, js); + TRACE("add_eq", tout << "propagate_bool_enode_assignment\n";); if (n2->is_bool()) propagate_bool_enode_assignment(r1, r2, n1, n2); @@ -604,6 +612,7 @@ namespace smt { catch (...) { // Restore trail size since procedure was interrupted in the middle. // If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked. + TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m_manager.limit().get_cancel_flag() << "\n";); m_trail_stack.shrink(old_trail_size); throw; } @@ -972,7 +981,7 @@ namespace smt { enode * parent = *it; if (parent->is_cgc_enabled()) { TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";); - CTRACE("add_eq", !parent->is_cgr(), + CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent), tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" << parent->get_owner_id() << ", parents: \n"; for (unsigned i = 0; i < r2->m_parents.size(); i++) { diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index f3f45c654..e625cab95 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -21,6 +21,7 @@ Revision History: reslimit::reslimit(): m_cancel(0), + m_suspend(false), m_count(0), m_limit(0) { } @@ -31,12 +32,12 @@ uint64 reslimit::count() const { bool reslimit::inc() { ++m_count; - return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit); + return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; } bool reslimit::inc(unsigned offset) { m_count += offset; - return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit); + return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; } void reslimit::push(unsigned delta_limit) { diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 3b278d132..0c81f9449 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -23,12 +23,14 @@ Revision History: class reslimit { volatile unsigned m_cancel; + bool m_suspend; uint64 m_count; uint64 m_limit; svector m_limits; ptr_vector m_children; void set_cancel(unsigned f); + friend class scoped_suspend_rlimit; public: reslimit(); @@ -42,7 +44,7 @@ public: uint64 count() const; - bool get_cancel_flag() const { return m_cancel > 0; } + bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; } char const* get_cancel_msg() const; void cancel(); void reset_cancel(); @@ -61,6 +63,17 @@ public: }; +class scoped_suspend_rlimit { + reslimit & m_limit; +public: + scoped_suspend_rlimit(reslimit& r): m_limit(r) { + r.m_suspend = true; + } + ~scoped_suspend_rlimit() { + m_limit.m_suspend = false; + } +}; + struct scoped_limits { reslimit& m_limit; unsigned m_sz; From e0e23975665e4344f853c8f9a51ab34ff50e5f3c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Oct 2017 19:40:30 -0700 Subject: [PATCH 12/41] missing setup datatypes for QF_DT Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_generator.cpp | 18 ++++++++++-------- src/smt/smt_setup.cpp | 1 + 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 5848fac62..df6865f1e 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -54,7 +54,7 @@ namespace smt { ptr_vector::const_iterator it = m_context->begin_theories(); ptr_vector::const_iterator end = m_context->end_theories(); for (; it != end; ++it) { - TRACE("model_generator_bug", tout << "init_model for theory: " << (*it)->get_name() << "\n";); + TRACE("model", tout << "init_model for theory: " << (*it)->get_name() << "\n";); (*it)->init_model(*this); } } @@ -91,7 +91,7 @@ namespace smt { sort * s = m_manager.get_sort(r->get_owner()); model_value_proc * proc = 0; if (m_manager.is_bool(s)) { - CTRACE("func_interp_bug", m_context->get_assignment(r) == l_undef, + CTRACE("model", m_context->get_assignment(r) == l_undef, tout << mk_pp(r->get_owner(), m_manager) << "\n";); SASSERT(m_context->get_assignment(r) != l_undef); if (m_context->get_assignment(r) == l_true) @@ -108,7 +108,7 @@ namespace smt { SASSERT(proc); } else { - TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";); + TRACE("model", tout << "creating fresh value for #" << r->get_owner_id() << "\n";); proc = alloc(fresh_value_proc, mk_extra_fresh_value(m_manager.get_sort(r->get_owner()))); } } @@ -130,7 +130,7 @@ namespace smt { if (!m_manager.is_model_value(n)) { sort * s = m_manager.get_sort(r->get_owner()); n = m_model->get_fresh_value(s); - CTRACE("model_generator_bug", n == 0, + CTRACE("model", n == 0, tout << mk_pp(r->get_owner(), m_manager) << "\nsort:\n" << mk_pp(s, m_manager) << "\n"; tout << "is_finite: " << m_model->is_finite(s) << "\n";); } @@ -406,9 +406,11 @@ namespace smt { */ bool model_generator::include_func_interp(func_decl * f) const { family_id fid = f->get_family_id(); + TRACE("model", tout << f->get_name() << " " << fid << "\n";); if (fid == null_family_id) return !m_hidden_ufs.contains(f); if (fid == m_manager.get_basic_family_id()) return false; theory * th = m_context->get_theory(fid); + TRACE("model", tout << th << "\n";); if (!th) return true; return th->include_func_interp(f); } @@ -443,7 +445,7 @@ namespace smt { SASSERT(m_model->has_interpretation(f)); SASSERT(m_model->get_func_interp(f) == fi); // The entry must be new because n->get_cg() == n - TRACE("func_interp_bug", + TRACE("model", tout << "insert new entry for:\n" << mk_ismt2_pp(n->get_owner(), m_manager) << "\nargs: "; for (unsigned i = 0; i < num_args; i++) { tout << "#" << n->get_arg(i)->get_owner_id() << " "; @@ -507,20 +509,20 @@ namespace smt { void model_generator::register_macros() { unsigned num = m_context->get_num_macros(); - TRACE("register_macros", tout << "num. macros: " << num << "\n";); + TRACE("model", tout << "num. macros: " << num << "\n";); expr_ref v(m_manager); for (unsigned i = 0; i < num; i++) { func_decl * f = m_context->get_macro_interpretation(i, v); func_interp * fi = alloc(func_interp, m_manager, f->get_arity()); fi->set_else(v); - TRACE("register_macros", tout << f->get_name() << "\n" << mk_pp(v, m_manager) << "\n";); + TRACE("model", tout << f->get_name() << "\n" << mk_pp(v, m_manager) << "\n";); m_model->register_decl(f, fi); } } proto_model * model_generator::mk_model() { SASSERT(!m_model); - TRACE("func_interp_bug", m_context->display(tout);); + TRACE("model", m_context->display(tout);); init_model(); register_existing_model_values(); mk_bool_model(); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 56b5d541a..631805b4d 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -216,6 +216,7 @@ namespace smt { void setup::setup_QF_DT() { setup_QF_UF(); + setup_datatypes(); } void setup::setup_QF_BVRE() { From 6c7a82edceef5e96476b2e80433d4b1a1a61b103 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Mon, 2 Oct 2017 09:20:59 -0700 Subject: [PATCH 13/41] update to _get_args to convert arguments from AstVector to a python list Signed-off-by: Miguel Angelo Da Terra Neves --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 39af03190..a521c5169 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -120,7 +120,7 @@ def _get_args(args): try: if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): return args[0] - elif len(args) == 1 and isinstance(args[0], set): + elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)): return [arg for arg in args[0]] else: return args From 2828126b725362ee08daf0cf8a774d0b09cc3dcb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 3 Oct 2017 10:20:49 -0700 Subject: [PATCH 14/41] add cancellation checks Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.h | 2 + src/util/lp/lp_primal_core_solver_tableau.h | 45 ++++++++++++--------- src/util/lp/lp_settings.h | 3 +- 3 files changed, 31 insertions(+), 19 deletions(-) diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 1ed30bd70..6d2cbea7d 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -417,6 +417,8 @@ public: for (unsigned i : m_rows_with_changed_bounds.m_index) { calculate_implied_bounds_for_row(i, bp); + if (settings().get_cancel_flag()) + return; } m_rows_with_changed_bounds.clear(); if (!use_tableau()) { diff --git a/src/util/lp/lp_primal_core_solver_tableau.h b/src/util/lp/lp_primal_core_solver_tableau.h index 5c7d4d2c2..d2b8c1a26 100644 --- a/src/util/lp/lp_primal_core_solver_tableau.h +++ b/src/util/lp/lp_primal_core_solver_tableau.h @@ -176,25 +176,34 @@ unsigned lp_primal_core_solver::solve_with_tableau() { default: break; // do nothing } - } while (this->get_status() != FLOATING_POINT_ERROR - && - this->get_status() != UNBOUNDED - && - this->get_status() != OPTIMAL - && - this->get_status() != INFEASIBLE - && - this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements - && - this->total_iterations() <= this->m_settings.max_total_number_of_iterations - && - !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)); + } while (this->get_status() != FLOATING_POINT_ERROR + && + this->get_status() != UNBOUNDED + && + this->get_status() != OPTIMAL + && + this->get_status() != INFEASIBLE + && + this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements + && + this->total_iterations() <= this->m_settings.max_total_number_of_iterations + && + !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) + && + m_settings.get_cancel_flag() == false); + + if (m_settings.get_cancel_flag()) { + this->set_status(CANCELLED); + } - SASSERT(this->get_status() == FLOATING_POINT_ERROR - || - this->current_x_is_feasible() == false - || - this->calc_current_x_is_feasible_include_non_basis()); + SASSERT( + this->get_status() == FLOATING_POINT_ERROR + || + this->get_status() == CANCELLED + || + this->current_x_is_feasible() == false + || + this->calc_current_x_is_feasible_include_non_basis()); return this->total_iterations(); } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index 70a9f1504..a7e6e2665 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -61,7 +61,8 @@ enum lp_status { TIME_EXHAUSTED, ITERATIONS_EXHAUSTED, EMPTY, - UNSTABLE + UNSTABLE, + CANCELLED }; // when the ratio of the vector lenth to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only From fd3d785a5b41715a5a1c61ea03038c550483030e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Oct 2017 14:49:45 -0700 Subject: [PATCH 15/41] add this-> Signed-off-by: Lev Nachmanson --- src/util/lp/lp_primal_core_solver_tableau.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/lp/lp_primal_core_solver_tableau.h b/src/util/lp/lp_primal_core_solver_tableau.h index d2b8c1a26..0c56f0ab9 100644 --- a/src/util/lp/lp_primal_core_solver_tableau.h +++ b/src/util/lp/lp_primal_core_solver_tableau.h @@ -190,10 +190,10 @@ unsigned lp_primal_core_solver::solve_with_tableau() { && !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only) && - m_settings.get_cancel_flag() == false); + this->m_settings.get_cancel_flag() == false); - if (m_settings.get_cancel_flag()) { - this->set_status(CANCELLED); + if (this->m_settings.get_cancel_flag()) { + this->set_status(CANCELLED); } SASSERT( From 110d558ee4262721f3ab2c999d789eaf84ac15d6 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 5 Oct 2017 08:53:12 +0100 Subject: [PATCH 16/41] dom_simplify_tactic: micro opt --- src/tactic/core/dom_simplify_tactic.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 595f8f7c6..d4a3031cd 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -225,9 +225,8 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { } else { expr_dominators::tree_t const& t = m_dominators.get_tree(); - if (t.contains(e)) { - ptr_vector const& children = t[e]; - for (expr * child : children) { + if (auto children = t.find_core(e)) { + for (expr * child : children->get_data().m_value) { simplify(child); } } From 53fc6ac11b25593e3827c943f5d61ce9f28da7ca Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 5 Oct 2017 14:27:56 +0100 Subject: [PATCH 17/41] [TravisCI] Refactor as many CI default options as possible so that the Docker and "TravisCI macOS" builds share most of the same defaults by sourcing the `ci_defaults.sh` file. --- contrib/ci/Dockerfiles/z3_build.Dockerfile | 50 ++++++++--------- contrib/ci/scripts/ci_defaults.sh | 54 +++++++++++++++++++ .../ci/scripts/travis_ci_linux_entry_point.sh | 4 +- .../ci/scripts/travis_ci_osx_entry_point.sh | 30 ++--------- 4 files changed, 86 insertions(+), 52 deletions(-) create mode 100644 contrib/ci/scripts/ci_defaults.sh diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 2d16d5394..5f7608cf4 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -2,34 +2,33 @@ ARG DOCKER_IMAGE_BASE FROM ${DOCKER_IMAGE_BASE} -# Specify defaults. This can be changed when invoking +# Build arguments. 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 ASAN_BUILD +ARG BUILD_DOCS +ARG CC +ARG CXX +ARG DOTNET_BINDINGS +ARG JAVA_BINDINGS +ARG NO_SUPPRESS_OUTPUT +ARG PYTHON_BINDINGS +ARG PYTHON_EXECUTABLE +ARG RUN_SYSTEM_TESTS +ARG RUN_UNIT_TESTS +ARG TARGET_ARCH +ARG TEST_INSTALL +ARG UBSAN_BUILD +ARG USE_LIBGMP +ARG USE_LTO +ARG USE_OPENMP 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_BUILD_TYPE +ARG Z3_CMAKE_GENERATOR +ARG Z3_INSTALL_PREFIX +ARG Z3_STATIC_BUILD ARG Z3_SYSTEM_TEST_GIT_REVISION -ARG Z3_WARNINGS_AS_ERRORS=SERIOUS_ONLY -ARG Z3_VERBOSE_BUILD_OUTPUT=0 +ARG Z3_WARNINGS_AS_ERRORS +ARG Z3_VERBOSE_BUILD_OUTPUT ENV \ ASAN_BUILD=${ASAN_BUILD} \ @@ -74,6 +73,7 @@ ADD *.txt *.md RELEASE_NOTES ${Z3_SRC_DIR}/ ADD \ /contrib/ci/scripts/build_z3_cmake.sh \ + /contrib/ci/scripts/ci_defaults.sh \ /contrib/ci/scripts/set_compiler_flags.sh \ /contrib/ci/scripts/set_generator_args.sh \ ${Z3_SRC_DIR}/contrib/ci/scripts/ diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh new file mode 100644 index 000000000..354ea95b7 --- /dev/null +++ b/contrib/ci/scripts/ci_defaults.sh @@ -0,0 +1,54 @@ +# This file should be sourced by other scripts +# and not executed directly + +# Set CI build defaults + +export ASAN_BUILD="${ASAN_BUILD:-0}" +export BUILD_DOCS="${BUILD_DOCS:-0}" +export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}" +export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" +export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" +export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" +export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}" +export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" +export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" +export TARGET_ARCH="${TARGET_ARCH:-x86_64}" +export TEST_INSTALL="${TEST_INSTALL:-1}" +export UBSAN_BUILD="${UBSAN_BUILD:-0}" +export USE_LIBGMP="${USE_LIBGMP:-0}" +export USE_LTO="${USE_LTO:-0}" +export USE_OPENMP="${USE_OPENMP:-1}" + +export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}" +export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}" +export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}" +# Default is blank which means get latest revision +export Z3_SYSTEM_TEST_GIT_REVISION="${Z3_SYSTEM_TEST_GIT_REVISION:-}" +export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}" +export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}" + +# Platform specific defaults +PLATFORM="$(uname -s)" +case "${PLATFORM}" in + Linux*) + export C_COMPILER="${C_COMPILER:-gcc}" + export CXX_COMPILER="${CXX_COMPILER:-g++}" + export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr}" + ;; + Darwin*) + export C_COMPILER="${C_COMPILER:-clang}" + export CXX_COMPILER="${CXX_COMPILER:-clang++}" + export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}" + ;; + *) + echo "Unknown platform \"${PLATFORM}\"" + exit 1 + ;; +esac +unset PLATFORM + +# NOTE: The following variables are not set here because +# they are specific to the CI implementation +# Z3_SRC_DIR +# Z3_BUILD_DIR +# Z3_SYSTEM_TEST_DIR diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index 84b2dd400..c0f856faa 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -11,13 +11,15 @@ 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 +# Get defaults +source "${SCRIPT_DIR}/ci_defaults.sh" + BUILD_OPTS=() # Override options if they have been provided. # Otherwise the defaults in the Docker file will be used diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh index c5e8b4c02..7dd566877 100755 --- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh @@ -6,26 +6,8 @@ set -x set -e set -o pipefail -# Set defaults -# FIXME: Refactor this so we don't need to stay in sync with -# `z3_build.Dockerfile`. -export ASAN_BUILD="${ASAN_BUILD:-0}" -export BUILD_DOCS="${BUILD_DOCS:-0}" -export C_COMPILER="${C_COMPILER:-clang}" -export CXX_COMPILER="${CXX_COMPILER:-clang++}" -export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}" -export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" -export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" -export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" -export PYTHON_EXECUTABLE="$(which python)" -export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" -export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" -export TARGET_ARCH="${TARGET_ARCH:-x86_64}" -export TEST_INSTALL="${TEST_INSTALL:-1}" -export UBSAN_BUILD="${UBSAN_BUILD:-0}" -export USE_LIBGMP="${USE_LIBGMP:-0}" -export USE_LTO="${USE_LTO:-0}" -export USE_OPENMP="${USE_OPENMP:-1}" +# Get defaults +source "${SCRIPT_DIR}/ci_defaults.sh" if [ -z "${TRAVIS_BUILD_DIR}" ]; then echo "TRAVIS_BUILD_DIR must be set to root of Z3 repository" @@ -37,15 +19,11 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then exit 1 fi +# These three variables are specific to the macOS TravisCI +# implementation and are not set in `ci_defaults.sh`. export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}" export Z3_BUILD_DIR="${Z3_SRC_DIR}/build" -export Z3_BUILD_TYPE="${Z3_BUILD_TYPE:-RelWithDebInfo}" -export Z3_CMAKE_GENERATOR="${Z3_CMAKE_GENERATOR:-Ninja}" -export Z3_INSTALL_PREFIX="${Z3_INSTALL_PREFIX:-/usr/local}" -export Z3_STATIC_BUILD="${Z3_STATIC_BUILD:-0}" export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test" -export Z3_WARNINGS_AS_ERRORS="${Z3_WARNINGS_AS_ERRORS:-SERIOUS_ONLY}" -export Z3_VERBOSE_BUILD_OUTPUT="${Z3_VERBOSE_BUILD_OUTPUT:-0}" # Overwrite whatever what set in TravisCI export CC="${C_COMPILER}" From eb975a49d606bcdb076b523d0506bf855ef8d267 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 5 Oct 2017 14:44:41 +0100 Subject: [PATCH 18/41] [TravisCI] Fix bug where `Z3_BUILD_TYPE` was not being passed as a Docker build argument. Also update an out of date comment. --- contrib/ci/scripts/travis_ci_linux_entry_point.sh | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/contrib/ci/scripts/travis_ci_linux_entry_point.sh b/contrib/ci/scripts/travis_ci_linux_entry_point.sh index c0f856faa..bd2c9d2d1 100755 --- a/contrib/ci/scripts/travis_ci_linux_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_linux_entry_point.sh @@ -21,8 +21,11 @@ fi source "${SCRIPT_DIR}/ci_defaults.sh" BUILD_OPTS=() -# Override options if they have been provided. -# Otherwise the defaults in the Docker file will be used +# Pass Docker build arguments +if [ -n "${Z3_BUILD_TYPE}" ]; then + BUILD_OPTS+=("--build-arg" "Z3_BUILD_TYPE=${Z3_BUILD_TYPE}") +fi + if [ -n "${Z3_CMAKE_GENERATOR}" ]; then BUILD_OPTS+=("--build-arg" "Z3_CMAKE_GENERATOR=${Z3_CMAKE_GENERATOR}") fi From 0633d5819f8b996b3300f177efe6b1406a1285a5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 5 Oct 2017 15:09:16 +0100 Subject: [PATCH 19/41] [TravisCI] Fix bug. `PYTHON_EXECUTABLE` should not be in common defaults. The location is dependent on the implementation. This triggered a build failure on TravisCI because the location of the default Python binary is different to what is in the Docker container. --- contrib/ci/Dockerfiles/z3_build.Dockerfile | 2 +- contrib/ci/scripts/ci_defaults.sh | 2 +- contrib/ci/scripts/travis_ci_osx_entry_point.sh | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/contrib/ci/Dockerfiles/z3_build.Dockerfile b/contrib/ci/Dockerfiles/z3_build.Dockerfile index 5f7608cf4..07504e6b9 100644 --- a/contrib/ci/Dockerfiles/z3_build.Dockerfile +++ b/contrib/ci/Dockerfiles/z3_build.Dockerfile @@ -12,7 +12,7 @@ ARG DOTNET_BINDINGS ARG JAVA_BINDINGS ARG NO_SUPPRESS_OUTPUT ARG PYTHON_BINDINGS -ARG PYTHON_EXECUTABLE +ARG PYTHON_EXECUTABLE=/usr/bin/python2.7 ARG RUN_SYSTEM_TESTS ARG RUN_UNIT_TESTS ARG TARGET_ARCH diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh index 354ea95b7..2fb3fa52a 100644 --- a/contrib/ci/scripts/ci_defaults.sh +++ b/contrib/ci/scripts/ci_defaults.sh @@ -9,7 +9,6 @@ export DOTNET_BINDINGS="${DOTNET_BINDINGS:-1}" export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" -export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}" export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" export TARGET_ARCH="${TARGET_ARCH:-x86_64}" @@ -49,6 +48,7 @@ unset PLATFORM # NOTE: The following variables are not set here because # they are specific to the CI implementation +# PYTHON_EXECUTABLE # Z3_SRC_DIR # Z3_BUILD_DIR # Z3_SYSTEM_TEST_DIR diff --git a/contrib/ci/scripts/travis_ci_osx_entry_point.sh b/contrib/ci/scripts/travis_ci_osx_entry_point.sh index 7dd566877..ad3b0c7ab 100755 --- a/contrib/ci/scripts/travis_ci_osx_entry_point.sh +++ b/contrib/ci/scripts/travis_ci_osx_entry_point.sh @@ -19,8 +19,9 @@ if [ ! -d "${TRAVIS_BUILD_DIR}" ]; then exit 1 fi -# These three variables are specific to the macOS TravisCI +# These variables are specific to the macOS TravisCI # implementation and are not set in `ci_defaults.sh`. +export PYTHON_EXECUTABLE="${PYTHON_EXECUTABLE:-$(which python)}" export Z3_SRC_DIR="${TRAVIS_BUILD_DIR}" export Z3_BUILD_DIR="${Z3_SRC_DIR}/build" export Z3_SYSTEM_TEST_DIR="${Z3_SRC_DIR}/z3_system_test" From 6268ff1fa13d283c9b4b0461f2b4423509a554ee Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 5 Oct 2017 18:10:20 +0100 Subject: [PATCH 20/41] dom_simplify improvements with Nikolaj --- src/tactic/core/dom_simplify_tactic.cpp | 129 ++++++++++++++++-------- src/tactic/core/dom_simplify_tactic.h | 19 +++- 2 files changed, 102 insertions(+), 46 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index d4a3031cd..85b7fd9d6 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -95,13 +95,16 @@ void expr_dominators::compute_dominators() { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; SASSERT(!p.empty()); - expr * new_idom = p[0], * idom2 = 0; - for (unsigned j = 1; j < p.size(); ++j) { - if (m_doms.find(p[j], idom2)) { + expr * new_idom = 0, *idom2 = 0; + for (unsigned j = 0; j < p.size(); ++j) { + if (!new_idom) { + m_doms.find(p[j], new_idom); + } + else if (m_doms.find(p[j], idom2)) { new_idom = intersect(new_idom, idom2); } } - if (!m_doms.find(child, idom2) || idom2 != new_idom) { + if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) { m_doms.insert(child, new_idom); change = true; } @@ -113,7 +116,7 @@ void expr_dominators::extract_tree() { for (auto const& kv : m_doms) { add_edge(m_tree, kv.m_value, kv.m_key); } -} +} void expr_dominators::compile(expr * e) { reset(); @@ -147,9 +150,9 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) { } void dom_simplify_tactic::operator()( - goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, + goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { mc = 0; pc = 0; core = 0; @@ -162,33 +165,41 @@ void dom_simplify_tactic::operator()( } void dom_simplify_tactic::cleanup() { - m_trail.reset(); - m_args.reset(); - m_args2.reset(); - m_result.reset(); - m_dominators.reset(); + m_trail.reset(); + m_args.reset(); + m_args2.reset(); + m_result.reset(); + m_dominators.reset(); } expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr_ref r(m); - expr * c = 0, * t = 0, * e = 0; + expr * c = 0, *t = 0, *e = 0; VERIFY(m.is_ite(ite, c, t, e)); unsigned old_lvl = scope_level(); expr_ref new_c = simplify(c); if (m.is_true(new_c)) { r = simplify(t); - } - else if (m.is_false(new_c) || !assert_expr(new_c, false)) { + } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { r = simplify(e); - } - else { - expr_ref new_t = simplify(t); + } else { + for (expr * child : tree(ite)) { + if (is_subexpr(child, t) && !is_subexpr(child, e)) { + simplify(child); + } + } pop(scope_level() - old_lvl); + expr_ref new_t = simplify(t); if (!assert_expr(new_c, true)) { return new_t; } - expr_ref new_e = simplify(e); + for (expr * child : tree(ite)) { + if (is_subexpr(child, e) && !is_subexpr(child, t)) { + simplify(child); + } + } pop(scope_level() - old_lvl); + expr_ref new_e = simplify(e); if (c == new_c && t == new_t && e == new_e) { r = ite; } @@ -197,7 +208,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { } else { TRACE("tactic", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";); - r = m.mk_ite(new_c, new_t, new_c); + r = m.mk_ite(new_c, new_t, new_e); } } return r; @@ -224,11 +235,8 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { r = simplify_or(to_app(e)); } else { - expr_dominators::tree_t const& t = m_dominators.get_tree(); - if (auto children = t.find_core(e)) { - for (expr * child : children->get_data().m_value) { - simplify(child); - } + for (expr * child : tree(e)) { + simplify(child); } if (is_app(e)) { m_args.reset(); @@ -251,27 +259,33 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { expr_ref r(m); unsigned old_lvl = scope_level(); - m_args.reset(); + + auto is_subexpr_arg = [&](expr * child, expr * except) { + if (!is_subexpr(child, except)) + return false; + for (expr * arg : *e) { + if (arg != except && is_subexpr(child, arg)) + return false; + } + return true; + }; + + expr_ref_vector args(m); for (expr * arg : *e) { - r = simplify(arg); - if (!assert_expr(r, !is_and)) { - r = is_and ? m.mk_false() : m.mk_true(); + for (expr * child : tree(arg)) { + if (is_subexpr_arg(child, arg)) { + simplify(child); + } + } + r = simplify(arg); + args.push_back(r); + if (!assert_expr(simplify(arg), !is_and)) { + r = is_and ? m.mk_false() : m.mk_true(); + return r; } - m_args.push_back(r); } pop(scope_level() - old_lvl); - m_args.reverse(); - m_args2.reset(); - for (expr * arg : m_args) { - r = simplify(arg); - if (!assert_expr(r, !is_and)) { - r = is_and ? m.mk_false() : m.mk_true(); - } - m_args2.push_back(r); - } - pop(scope_level() - old_lvl); - m_args2.reverse(); - r = is_and ? mk_and(m_args2) : mk_or(m_args2); + r = is_and ? mk_and(args) : mk_or(args); return r; } @@ -332,11 +346,36 @@ void dom_simplify_tactic::simplify_goal(goal& g) { SASSERT(scope_level() == 0); } +bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { + if (a == b) + return true; + + bool r; + if (m_subexpr_cache.find(a, b, r)) + return r; + + for (expr * e : tree(b)) { + if (is_subexpr(a, e)) { + m_subexpr_cache.insert(a, b, true); + return true; + } + } + m_subexpr_cache.insert(a, b, false); + return false; +} + +ptr_vector const & dom_simplify_tactic::tree(expr * e) { + if (auto p = m_dominators.get_tree().find_core(e)) + return p->get_data().get_value(); + return m_empty; +} + // ---------------------- // expr_substitution_simplifier bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) { + m_scoped_substitution.push(); expr* tt; if (!sign) { update_substitution(t, 0); @@ -439,3 +478,7 @@ void expr_substitution_simplifier::compute_depth(expr* e) { m_expr2depth.insert(e, d + 1); } } + +tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(dom_simplify_tactic, m, alloc(expr_substitution_simplifier, m), p)); +} diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 2fa79dd1d..9fe59de23 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -23,6 +23,8 @@ Notes: #include "ast/ast.h" #include "ast/expr_substitution.h" #include "tactic/tactic.h" +#include "tactic/tactical.h" +#include "util/obj_pair_hashtable.h" class expr_dominators { @@ -89,6 +91,8 @@ private: unsigned m_scope_level; unsigned m_depth; unsigned m_max_depth; + ptr_vector m_empty; + obj_pair_map m_subexpr_cache; expr_ref simplify(expr* t); expr_ref simplify_ite(app * ite); @@ -97,9 +101,13 @@ private: expr_ref simplify_and_or(bool is_and, app * ite); void simplify_goal(goal& g); - expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(r, r)) r = t; return expr_ref(r, m); } + bool is_subexpr(expr * a, expr * b); + + expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); } void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); } + ptr_vector const & tree(expr * e); + unsigned scope_level() { return m_scope_level; } void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); } bool assert_expr(expr* f, bool sign) { m_scope_level++; return m_simplifier->assert_expr(f, sign); } @@ -156,8 +164,13 @@ public: SASSERT(m_subst.empty()); return alloc(expr_substitution_simplifier, m); } - - }; + +tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* +ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)") +*/ + #endif From f59cf2452d9a335785bd1691dbf04b93973193d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Oct 2017 22:20:31 +0100 Subject: [PATCH 21/41] #1284 build problems Signed-off-by: Nikolaj Bjorner --- src/tactic/core/CMakeLists.txt | 2 + src/tactic/core/dom_simplify_tactic.cpp | 1 + src/tactic/core/dom_simplify_tactic.h | 53 +++++++++++++------------ 3 files changed, 31 insertions(+), 25 deletions(-) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index f192b4fa6..16778d8dd 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -7,6 +7,7 @@ z3_add_component(core_tactics ctx_simplify_tactic.cpp der_tactic.cpp distribute_forall_tactic.cpp + dom_simplify_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp injectivity_tactic.cpp @@ -32,6 +33,7 @@ z3_add_component(core_tactics ctx_simplify_tactic.h der_tactic.h distribute_forall_tactic.h + dom_simplify_tactic.h elim_term_ite_tactic.h elim_uncnstr_tactic.h injectivity_tactic.h diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 85b7fd9d6..bba27cf46 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -188,6 +188,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { simplify(child); } } + pop(scope_level() - old_lvl); expr_ref new_t = simplify(t); if (!assert_expr(new_c, true)) { diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 9fe59de23..825a173bf 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -58,32 +58,35 @@ public: }; +class dom_simplifier { + public: + dom_simplifier() {} + + virtual ~dom_simplifier() {} + /** + \brief assert_expr performs an implicit push + */ + virtual bool assert_expr(expr * t, bool sign) = 0; + + /** + \brief apply simplification. + */ + virtual void operator()(expr_ref& r) = 0; + + /** + \brief pop scopes accumulated from assertions. + */ + virtual void pop(unsigned num_scopes) = 0; + + virtual dom_simplifier * translate(ast_manager & m) = 0; + +}; + class dom_simplify_tactic : public tactic { public: - class simplifier { - public: - virtual ~simplifier() {} - /** - \brief assert_expr performs an implicit push - */ - virtual bool assert_expr(expr * t, bool sign) = 0; - - /** - \brief apply simplification. - */ - virtual void operator()(expr_ref& r) = 0; - - /** - \brief pop scopes accumulated from assertions. - */ - virtual void pop(unsigned num_scopes) = 0; - - virtual simplifier * translate(ast_manager & m); - - }; private: ast_manager& m; - simplifier* m_simplifier; + dom_simplifier* m_simplifier; params_ref m_params; expr_ref_vector m_trail, m_args, m_args2; obj_map m_result; @@ -115,7 +118,7 @@ private: void init(goal& g); public: - dom_simplify_tactic(ast_manager & m, simplifier* s, params_ref const & p = params_ref()): + dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()): m(m), m_simplifier(s), m_params(p), m_trail(m), m_args(m), m_args2(m), m_dominators(m), @@ -138,7 +141,7 @@ public: virtual void cleanup(); }; -class expr_substitution_simplifier : public dom_simplify_tactic::simplifier { +class expr_substitution_simplifier : public dom_simplifier { ast_manager& m; expr_substitution m_subst; scoped_expr_substitution m_scoped_substitution; @@ -160,7 +163,7 @@ public: virtual void pop(unsigned num_scopes) { m_scoped_substitution.pop(num_scopes); } - virtual simplifier * translate(ast_manager & m) { + virtual dom_simplifier * translate(ast_manager & m) { SASSERT(m_subst.empty()); return alloc(expr_substitution_simplifier, m); } From eac659f748fc3209fca947556d94d9b08a3c8c82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 11:34:14 +0100 Subject: [PATCH 22/41] deal with empty set of post-orders Signed-off-by: Nikolaj Bjorner --- src/muz/rel/karr_relation.cpp | 4 ++-- .../transforms/dl_mk_interp_tail_simplifier.cpp | 4 ++-- src/smt/theory_lra.cpp | 4 ++-- src/tactic/core/dom_simplify_tactic.cpp | 14 ++++++++------ src/tactic/core/dom_simplify_tactic.h | 4 ++-- 5 files changed, 16 insertions(+), 14 deletions(-) diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp index 572d5e8d5..c8a489d69 100644 --- a/src/muz/rel/karr_relation.cpp +++ b/src/muz/rel/karr_relation.cpp @@ -111,8 +111,8 @@ namespace datalog { void filter_interpreted(app* cond) { rational one(1), mone(-1); - expr* e1, *e2, *en; - var* v, *w; + expr* e1 = 0, *e2 = 0, *en = 0; + var* v = 0, *w = 0; rational n1, n2; expr_ref_vector conjs(m); flatten_and(cond, conjs); diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 30505a5e8..7bd35b4ef 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -398,8 +398,8 @@ namespace datalog { } bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) { - if (!m_context.get_params ().xform_tail_simplifier_pve ()) - return false; + if (!m_context.get_params ().xform_tail_simplifier_pve ()) + return false; unsigned u_len = r->get_uninterpreted_tail_size(); unsigned len = r->get_tail_size(); if (u_len == len) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0bb76cd90..7fec6f836 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -721,7 +721,7 @@ namespace smt { SASSERT(!ctx().b_internalized(atom)); bool_var bv = ctx().mk_bool_var(atom); ctx().set_var_theory(bv, get_id()); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; rational r; lra_lp::bound_kind k; theory_var v = null_theory_var; @@ -862,7 +862,7 @@ namespace smt { void relevant_eh(app* n) { TRACE("arith", tout << mk_pp(n, m) << "\n";); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; if (a.is_mod(n, n1, n2)) mk_idiv_mod_axioms(n1, n2); else if (a.is_rem(n, n1, n2)) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index bba27cf46..17262a9d6 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -90,8 +90,8 @@ void expr_dominators::compute_dominators() { bool change = true; while (change) { change = false; - SASSERT(m_post2expr.back() == e); - for (unsigned i = 0; i < m_post2expr.size() - 1; ++i) { + SASSERT(m_post2expr.empty() || m_post2expr.back() == e); + for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; SASSERT(!p.empty()); @@ -167,7 +167,6 @@ void dom_simplify_tactic::operator()( void dom_simplify_tactic::cleanup() { m_trail.reset(); m_args.reset(); - m_args2.reset(); m_result.reset(); m_dominators.reset(); } @@ -180,9 +179,11 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr_ref new_c = simplify(c); if (m.is_true(new_c)) { r = simplify(t); - } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { + } + else if (m.is_false(new_c) || !assert_expr(new_c, false)) { r = simplify(e); - } else { + } + else { for (expr * child : tree(ite)) { if (is_subexpr(child, t) && !is_subexpr(child, e)) { simplify(child); @@ -254,6 +255,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { cache(e0, r); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); --m_depth; + m_subexpr_cache.reset(); return r; } @@ -361,7 +363,7 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { return true; } } - m_subexpr_cache.insert(a, b, false); + m_subexpr_cache.insert(a, b, false); return false; } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 825a173bf..c62651c5c 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -88,7 +88,7 @@ private: ast_manager& m; dom_simplifier* m_simplifier; params_ref m_params; - expr_ref_vector m_trail, m_args, m_args2; + expr_ref_vector m_trail, m_args; obj_map m_result; expr_dominators m_dominators; unsigned m_scope_level; @@ -120,7 +120,7 @@ private: public: dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()): m(m), m_simplifier(s), m_params(p), - m_trail(m), m_args(m), m_args2(m), + m_trail(m), m_args(m), m_dominators(m), m_scope_level(0), m_depth(0), m_max_depth(1024) {} From 6df628edc7043a08dd11eae3d2ab8d44e07a172c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 11:45:29 +0100 Subject: [PATCH 23/41] pin elements in expr2depth Signed-off-by: Nikolaj Bjorner --- src/smt/smt_implied_equalities.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- src/tactic/bv/bv_bounds_tactic.cpp | 6 ++++-- src/tactic/core/dom_simplify_tactic.cpp | 2 ++ src/tactic/core/dom_simplify_tactic.h | 3 ++- 5 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index 7d54e714e..d021708fc 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -284,7 +284,7 @@ namespace smt { } lbool reduce_cond(model_ref& model, expr* e) { - expr* e1, *e2; + expr* e1 = 0, *e2 = 0; if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) { if (e1 == e2) { return l_true; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 7fec6f836..292d2ab0d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -689,7 +689,7 @@ namespace smt { SASSERT(!ctx().b_internalized(atom)); bool_var bv = ctx().mk_bool_var(atom); ctx().set_var_theory(bv, get_id()); - expr* n1, *n2; + expr* n1 = 0, *n2 = 0; rational r; lra_lp::bound_kind k; theory_var v = null_theory_var; diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index d2cd0d66c..1f0bb8473 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -70,11 +70,13 @@ struct interval { if (is_wrapped()) { // l >= b.l >= b.h >= h return b.is_wrapped() && h <= b.h && l >= b.l; - } else if (b.is_wrapped()) { + } + else if (b.is_wrapped()) { // b.l > b.h >= h >= l // h >= l >= b.l > b.h return h <= b.h || l >= b.l; - } else { + } + else { // return l >= b.l && h <= b.h; } diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 17262a9d6..08037fe18 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -430,6 +430,8 @@ void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) { if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) { compute_depth(lhs); compute_depth(rhs); + m_trail.push_back(lhs); + m_trail.push_back(rhs); if (is_gt(lhs, rhs)) { TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";); m_scoped_substitution.insert(lhs, rhs, pr); diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index c62651c5c..25fb7c24f 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -146,6 +146,7 @@ class expr_substitution_simplifier : public dom_simplifier { expr_substitution m_subst; scoped_expr_substitution m_scoped_substitution; obj_map m_expr2depth; + expr_ref_vector m_trail; // move from asserted_formulas to here.. void compute_depth(expr* e); @@ -153,7 +154,7 @@ class expr_substitution_simplifier : public dom_simplifier { unsigned depth(expr* e) { return m_expr2depth[e]; } public: - expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst) {} + expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {} virtual ~expr_substitution_simplifier() {} virtual bool assert_expr(expr * t, bool sign); From cb548404bc1ad5a55628e1dd23fc4efe69de8856 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 12:08:37 +0100 Subject: [PATCH 24/41] bail out dominators after log number of steps Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/bv_bounds_tactic.cpp | 1227 ++++++++++++++--------- src/tactic/core/dom_simplify_tactic.cpp | 25 +- src/tactic/core/dom_simplify_tactic.h | 8 +- 3 files changed, 792 insertions(+), 468 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 1f0bb8473..2d5eb216a 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -18,6 +18,7 @@ Author: #include "tactic/bv/bv_bounds_tactic.h" #include "tactic/core/ctx_simplify_tactic.h" +#include "tactic/core/dom_simplify_tactic.h" #include "ast/bv_decl_plugin.h" #include "ast/ast_pp.h" #include @@ -29,509 +30,825 @@ static uint64 uMaxInt(unsigned sz) { namespace { -struct interval { - // l < h: [l, h] - // l > h: [0, h] U [l, UMAX_INT] - uint64 l, h; - unsigned sz; - bool tight; + struct interval { + // l < h: [l, h] + // l > h: [0, h] U [l, UMAX_INT] + uint64 l, h; + unsigned sz; + bool tight; - interval() {} - interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { - // canonicalize full set - if (is_wrapped() && l == h + 1) { - this->l = 0; - this->h = uMaxInt(sz); - } - SASSERT(invariant()); - } - - bool invariant() const { - return l <= uMaxInt(sz) && h <= uMaxInt(sz) && - (!is_wrapped() || l != h+1); - } - - bool is_full() const { return l == 0 && h == uMaxInt(sz); } - bool is_wrapped() const { return l > h; } - bool is_singleton() const { return l == h; } - - bool operator==(const interval& b) const { - SASSERT(sz == b.sz); - return l == b.l && h == b.h && tight == b.tight; - } - bool operator!=(const interval& b) const { return !(*this == b); } - - bool implies(const interval& b) const { - if (b.is_full()) - return true; - if (is_full()) - return false; - - if (is_wrapped()) { - // l >= b.l >= b.h >= h - return b.is_wrapped() && h <= b.h && l >= b.l; - } - else if (b.is_wrapped()) { - // b.l > b.h >= h >= l - // h >= l >= b.l > b.h - return h <= b.h || l >= b.l; - } - else { - // - return l >= b.l && h <= b.h; - } - } - - /// return false if intersection is unsat - bool intersect(const interval& b, interval& result) const { - if (is_full() || *this == b) { - result = b; - return true; - } - if (b.is_full()) { - result = *this; - return true; + interval() {} + interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { + // canonicalize full set + if (is_wrapped() && l == h + 1) { + this->l = 0; + this->h = uMaxInt(sz); + } + SASSERT(invariant()); } - if (is_wrapped()) { - if (b.is_wrapped()) { - if (h >= b.l) { - result = b; - } else if (b.h >= l) { - result = *this; + bool invariant() const { + return l <= uMaxInt(sz) && h <= uMaxInt(sz) && + (!is_wrapped() || l != h+1); + } + + bool is_full() const { return l == 0 && h == uMaxInt(sz); } + bool is_wrapped() const { return l > h; } + bool is_singleton() const { return l == h; } + + bool operator==(const interval& b) const { + SASSERT(sz == b.sz); + return l == b.l && h == b.h && tight == b.tight; + } + bool operator!=(const interval& b) const { return !(*this == b); } + + bool implies(const interval& b) const { + if (b.is_full()) + return true; + if (is_full()) + return false; + + if (is_wrapped()) { + // l >= b.l >= b.h >= h + return b.is_wrapped() && h <= b.h && l >= b.l; + } + else if (b.is_wrapped()) { + // b.l > b.h >= h >= l + // h >= l >= b.l > b.h + return h <= b.h || l >= b.l; + } + else { + // + return l >= b.l && h <= b.h; + } + } + + /// return false if intersection is unsat + bool intersect(const interval& b, interval& result) const { + if (is_full() || *this == b) { + result = b; + return true; + } + if (b.is_full()) { + result = *this; + return true; + } + + if (is_wrapped()) { + if (b.is_wrapped()) { + if (h >= b.l) { + result = b; + } else if (b.h >= l) { + result = *this; + } else { + result = interval(std::max(l, b.l), std::min(h, b.h), sz); + } } else { - result = interval(std::max(l, b.l), std::min(h, b.h), sz); + return b.intersect(*this, result); + } + } + else if (b.is_wrapped()) { + // ... b.h ... l ... h ... b.l .. + if (h < b.l && l > b.h) { + return false; + } + // ... l ... b.l ... h ... + if (h >= b.l && l <= b.h) { + result = b; + } else if (h >= b.l) { + result = interval(b.l, h, sz); + } else { + // ... l .. b.h .. h .. b.l ... + SASSERT(l <= b.h); + result = interval(l, std::min(h, b.h), sz); } } else { - return b.intersect(*this, result); - } - } else if (b.is_wrapped()) { - // ... b.h ... l ... h ... b.l .. - if (h < b.l && l > b.h) { - return false; - } - // ... l ... b.l ... h ... - if (h >= b.l && l <= b.h) { - result = b; - } else if (h >= b.l) { - result = interval(b.l, h, sz); - } else { - // ... l .. b.h .. h .. b.l ... - SASSERT(l <= b.h); - result = interval(l, std::min(h, b.h), sz); - } - } else { - if (l > b.h || h < b.l) - return false; + if (l > b.h || h < b.l) + return false; - // 0 .. l.. l' ... h ... h' - result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight); - } - return true; - } - - /// return false if negation is empty - bool negate(interval& result) const { - if (!tight) { - result = interval(0, uMaxInt(sz), true); + // 0 .. l.. l' ... h ... h' + result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight); + } return true; } - if (is_full()) - return false; - if (l == 0) { - result = interval(h + 1, uMaxInt(sz), sz); - } else if (uMaxInt(sz) == h) { - result = interval(0, l - 1, sz); - } else { - result = interval(h + 1, l - 1, sz); + /// return false if negation is empty + bool negate(interval& result) const { + if (!tight) { + result = interval(0, uMaxInt(sz), true); + return true; + } + + if (is_full()) + return false; + if (l == 0) { + result = interval(h + 1, uMaxInt(sz), sz); + } else if (uMaxInt(sz) == h) { + result = interval(0, l - 1, sz); + } else { + result = interval(h + 1, l - 1, sz); + } + return true; } - return true; - } -}; + }; #ifdef _TRACE -std::ostream& operator<<(std::ostream& o, const interval& I) { - o << "[" << I.l << ", " << I.h << "]"; - return o; -} -#endif - - -struct undo_bound { - expr* e; - interval b; - bool fresh; - undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} -}; - -class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { - typedef obj_map map; - typedef obj_map expr_set; - typedef obj_map expr_cnt; - - ast_manager& m; - params_ref m_params; - bool m_propagate_eq; - bv_util m_bv; - vector m_scopes; - map m_bound; - svector m_expr_vars; - svector m_bound_exprs; - - bool is_number(expr *e, uint64& n, unsigned& sz) const { - rational r; - if (m_bv.is_numeral(e, r, sz) && sz <= 64) { - n = r.get_uint64(); - return true; - } - return false; - } - - bool is_bound(expr *e, expr*& v, interval& b) const { - uint64 n; - expr *lhs, *rhs; - unsigned sz; - - if (m_bv.is_bv_ule(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C ule x <=> x uge C - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, uMaxInt(sz), sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { // x ule C - b = interval(0, n, sz, true); - v = lhs; - return true; - } - } else if (m_bv.is_bv_sle(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C sle x <=> x sge C - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, (1ull << (sz-1)) - 1, sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { // x sle C - b = interval(1ull << (sz-1), n, sz, true); - v = lhs; - return true; - } - } else if (m.is_eq(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, n, sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { - b = interval(n, n, sz, true); - v = lhs; - return true; - } - } - return false; - } - -#if 0 - expr_set* get_expr_vars(expr* t) { - unsigned id = t->get_id(); - m_expr_vars.reserve(id + 1); - expr_set*& entry = m_expr_vars[id]; - if (entry) - return entry; - - expr_set* set = alloc(expr_set); - entry = set; - - if (!m_bv.is_numeral(t)) - set->insert(t, true); - - if (!is_app(t)) - return set; - - app* a = to_app(t); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_set* set_arg = get_expr_vars(a->get_arg(i)); - for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { - set->insert(I->m_key, true); - } - } - return set; + std::ostream& operator<<(std::ostream& o, const interval& I) { + o << "[" << I.l << ", " << I.h << "]"; + return o; } #endif -#if 0 - expr_cnt* get_expr_bounds(expr* t) { - unsigned id = t->get_id(); - m_bound_exprs.reserve(id + 1); - expr_cnt*& entry = m_bound_exprs[id]; - if (entry) - return entry; - expr_cnt* set = alloc(expr_cnt); - entry = set; - - if (!is_app(t)) - return set; - - interval b; + struct undo_bound { expr* e; - if (is_bound(t, e, b)) { - set->insert_if_not_there2(e, 0)->get_data().m_value++; + interval b; + bool fresh; + undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} + }; + + class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { + typedef obj_map map; + typedef obj_map expr_set; + typedef obj_map expr_cnt; + + ast_manager& m; + params_ref m_params; + bool m_propagate_eq; + bv_util m_bv; + vector m_scopes; + map m_bound; + svector m_expr_vars; + svector m_bound_exprs; + + bool is_number(expr *e, uint64& n, unsigned& sz) const { + rational r; + if (m_bv.is_numeral(e, r, sz) && sz <= 64) { + n = r.get_uint64(); + return true; + } + return false; } - app* a = to_app(t); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_cnt* set_arg = get_expr_bounds(a->get_arg(i)); - for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { - set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value; + bool is_bound(expr *e, expr*& v, interval& b) const { + uint64 n; + expr *lhs = 0, *rhs = 0; + unsigned sz; + + if (m_bv.is_bv_ule(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C ule x <=> x uge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, uMaxInt(sz), sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x ule C + b = interval(0, n, sz, true); + v = lhs; + return true; + } + } + else if (m_bv.is_bv_sle(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C sle x <=> x sge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, (1ull << (sz-1)) - 1, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x sle C + b = interval(1ull << (sz-1), n, sz, true); + v = lhs; + return true; + } + } else if (m.is_eq(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, n, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { + b = interval(n, n, sz, true); + v = lhs; + return true; + } } + return false; + } + +#if 0 + expr_set* get_expr_vars(expr* t) { + unsigned id = t->get_id(); + m_expr_vars.reserve(id + 1); + expr_set*& entry = m_expr_vars[id]; + if (entry) + return entry; + + expr_set* set = alloc(expr_set); + entry = set; + + if (!m_bv.is_numeral(t)) + set->insert(t, true); + + if (!is_app(t)) + return set; + + app* a = to_app(t); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr_set* set_arg = get_expr_vars(a->get_arg(i)); + for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { + set->insert(I->m_key, true); + } + } + return set; } - return set; - } #endif -public: - bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { - updt_params(p); - } +#if 0 + expr_cnt* get_expr_bounds(expr* t) { + unsigned id = t->get_id(); + m_bound_exprs.reserve(id + 1); + expr_cnt*& entry = m_bound_exprs[id]; + if (entry) + return entry; - virtual void updt_params(params_ref const & p) { - m_propagate_eq = p.get_bool("propagate_eq", false); - } + expr_cnt* set = alloc(expr_cnt); + entry = set; - static void get_param_descrs(param_descrs& r) { - r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); - } + if (!is_app(t)) + return set; - virtual ~bv_bounds_simplifier() { - for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { - dealloc(m_expr_vars[i]); - } - for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { - dealloc(m_bound_exprs[i]); - } - } - - virtual bool assert_expr(expr * t, bool sign) { - while (m.is_not(t, t)) { - sign = !sign; - } - - interval b; - expr* t1; - if (is_bound(t, t1, b)) { - SASSERT(!m_bv.is_numeral(t1)); - if (sign) - VERIFY(b.negate(b)); - - TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); - map::obj_map_entry* e = m_bound.find_core(t1); - if (e) { - interval& old = e->get_data().m_value; - interval intr; - if (!old.intersect(b, intr)) - return false; - if (old == intr) - return true; - m_scopes.insert(undo_bound(t1, old, false)); - old = intr; - } else { - m_bound.insert(t1, b); - m_scopes.insert(undo_bound(t1, interval(), true)); - } - } - return true; - } - - virtual bool simplify(expr* t, expr_ref& result) { - expr* t1; - interval b; - - if (m_bound.find(t, b) && b.is_singleton()) { - result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); - return true; - } - - if (!m.is_bool(t)) - return false; - - bool sign = false; - while (m.is_not(t, t)) { - sign = !sign; - } - - if (!is_bound(t, t1, b)) - return false; - - if (sign && b.tight) { - sign = false; - if (!b.negate(b)) { - result = m.mk_false(); - return true; - } - } - - interval ctx, intr; - result = 0; - - if (b.is_full() && b.tight) { - result = m.mk_true(); - } else if (m_bound.find(t1, ctx)) { - if (ctx.implies(b)) { - result = m.mk_true(); - } else if (!b.intersect(ctx, intr)) { - result = m.mk_false(); - } else if (m_propagate_eq && intr.is_singleton()) { - result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), - m.get_sort(t1))); - } - } - - CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); - if (sign && result != 0) - result = m.mk_not(result); - return result != 0; - } - - // check if t contains v - ptr_vector todo; - bool contains(expr* t, expr* v) { - ast_fast_mark1 mark; - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark.is_marked(t)) { - continue; - } - if (t == v) { - todo.reset(); - return true; - } - mark.mark(t); - - if (!is_app(t)) { - continue; - } - app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); - } - return false; - } - - bool contains_bound(expr* t) { - ast_fast_mark1 mark1; - ast_fast_mark2 mark2; - - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark1.is_marked(t)) { - continue; - } - mark1.mark(t); - - if (!is_app(t)) { - continue; - } interval b; expr* e; if (is_bound(t, e, b)) { - if (mark2.is_marked(e)) { - todo.reset(); - return true; - } - mark2.mark(e); - if (m_bound.contains(e)) { - todo.reset(); - return true; - } + set->insert_if_not_there2(e, 0)->get_data().m_value++; } app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); - } - return false; - } - - virtual bool may_simplify(expr* t) { - if (m_bv.is_numeral(t)) - return false; - - while (m.is_not(t, t)); - - for (auto & v : m_bound) { - if (contains(t, v.m_key)) return true; - } - -#if 0 - expr_set* used_exprs = get_expr_vars(t); - for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { - if (contains(t, I->m_key)) return true; - if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) - return true; + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr_cnt* set_arg = get_expr_bounds(a->get_arg(i)); + for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { + set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value; + } + } + return set; } #endif - expr* t1; - interval b; - // skip common case: single bound constraint without any context for simplification - if (is_bound(t, t1, b)) { - return b.is_full() || m_bound.contains(t1); + public: + bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { + updt_params(p); } - if (contains_bound(t)) { - return true; + virtual void updt_params(params_ref const & p) { + m_propagate_eq = p.get_bool("propagate_eq", false); } -#if 0 - expr_cnt* bounds = get_expr_bounds(t); - for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { - if (I->m_value > 1 || m_bound.contains(I->m_key)) - return true; - } -#endif - return false; - } - virtual void pop(unsigned num_scopes) { - TRACE("bv", tout << "pop: " << num_scopes << "\n";); - if (m_scopes.empty()) - return; - unsigned target = m_scopes.size() - num_scopes; - if (target == 0) { - m_bound.reset(); - m_scopes.reset(); - return; + static void get_param_descrs(param_descrs& r) { + r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); } - for (unsigned i = m_scopes.size()-1; i >= target; --i) { - undo_bound& undo = m_scopes[i]; - SASSERT(m_bound.contains(undo.e)); - if (undo.fresh) { - m_bound.erase(undo.e); - } else { - m_bound.insert(undo.e, undo.b); + + virtual ~bv_bounds_simplifier() { + for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { + dealloc(m_expr_vars[i]); + } + for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { + dealloc(m_bound_exprs[i]); } } - m_scopes.shrink(target); - } - virtual simplifier * translate(ast_manager & m) { - return alloc(bv_bounds_simplifier, m, m_params); - } + virtual bool assert_expr(expr * t, bool sign) { + while (m.is_not(t, t)) { + sign = !sign; + } - virtual unsigned scope_level() const { - return m_scopes.size(); - } -}; + interval b; + expr* t1; + if (is_bound(t, t1, b)) { + SASSERT(!m_bv.is_numeral(t1)); + if (sign) + VERIFY(b.negate(b)); + + TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); + map::obj_map_entry* e = m_bound.find_core(t1); + if (e) { + interval& old = e->get_data().m_value; + interval intr; + if (!old.intersect(b, intr)) + return false; + if (old == intr) + return true; + m_scopes.insert(undo_bound(t1, old, false)); + old = intr; + } else { + m_bound.insert(t1, b); + m_scopes.insert(undo_bound(t1, interval(), true)); + } + } + return true; + } + + virtual bool simplify(expr* t, expr_ref& result) { + expr* t1; + interval b; + + if (m_bound.find(t, b) && b.is_singleton()) { + result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); + return true; + } + + if (!m.is_bool(t)) + return false; + + bool sign = false; + while (m.is_not(t, t)) { + sign = !sign; + } + + if (!is_bound(t, t1, b)) + return false; + + if (sign && b.tight) { + sign = false; + if (!b.negate(b)) { + result = m.mk_false(); + return true; + } + } + + interval ctx, intr; + result = 0; + + if (b.is_full() && b.tight) { + result = m.mk_true(); + } else if (m_bound.find(t1, ctx)) { + if (ctx.implies(b)) { + result = m.mk_true(); + } else if (!b.intersect(ctx, intr)) { + result = m.mk_false(); + } else if (m_propagate_eq && intr.is_singleton()) { + result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), + m.get_sort(t1))); + } + } + + CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); + if (sign && result != 0) + result = m.mk_not(result); + return result != 0; + } + + // check if t contains v + ptr_vector todo; + bool contains(expr* t, expr* v) { + ast_fast_mark1 mark; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark.is_marked(t)) { + continue; + } + if (t == v) { + todo.reset(); + return true; + } + mark.mark(t); + + if (!is_app(t)) { + continue; + } + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + bool contains_bound(expr* t) { + ast_fast_mark1 mark1; + ast_fast_mark2 mark2; + + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark1.is_marked(t)) { + continue; + } + mark1.mark(t); + + if (!is_app(t)) { + continue; + } + interval b; + expr* e; + if (is_bound(t, e, b)) { + if (mark2.is_marked(e)) { + todo.reset(); + return true; + } + mark2.mark(e); + if (m_bound.contains(e)) { + todo.reset(); + return true; + } + } + + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + virtual bool may_simplify(expr* t) { + if (m_bv.is_numeral(t)) + return false; + + while (m.is_not(t, t)); + + for (auto & v : m_bound) { + if (contains(t, v.m_key)) return true; + } + +#if 0 + expr_set* used_exprs = get_expr_vars(t); + for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { + if (contains(t, I->m_key)) return true; + if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) + return true; + } +#endif + + expr* t1; + interval b; + // skip common case: single bound constraint without any context for simplification + if (is_bound(t, t1, b)) { + return b.is_full() || m_bound.contains(t1); + } + + if (contains_bound(t)) { + return true; + } +#if 0 + expr_cnt* bounds = get_expr_bounds(t); + for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { + if (I->m_value > 1 || m_bound.contains(I->m_key)) + return true; + } +#endif + return false; + } + + virtual void pop(unsigned num_scopes) { + TRACE("bv", tout << "pop: " << num_scopes << "\n";); + if (m_scopes.empty()) + return; + unsigned target = m_scopes.size() - num_scopes; + if (target == 0) { + m_bound.reset(); + m_scopes.reset(); + return; + } + for (unsigned i = m_scopes.size()-1; i >= target; --i) { + undo_bound& undo = m_scopes[i]; + SASSERT(m_bound.contains(undo.e)); + if (undo.fresh) { + m_bound.erase(undo.e); + } else { + m_bound.insert(undo.e, undo.b); + } + } + m_scopes.shrink(target); + } + + virtual simplifier * translate(ast_manager & m) { + return alloc(bv_bounds_simplifier, m, m_params); + } + + virtual unsigned scope_level() const { + return m_scopes.size(); + } + }; + + + class dom_bv_bounds_simplifier : public dom_simplifier { + typedef obj_map map; + typedef obj_map expr_set; + typedef obj_map expr_cnt; + + ast_manager& m; + params_ref m_params; + bool m_propagate_eq; + bv_util m_bv; + vector m_scopes; + map m_bound; + svector m_expr_vars; + svector m_bound_exprs; + + bool is_number(expr *e, uint64& n, unsigned& sz) const { + rational r; + if (m_bv.is_numeral(e, r, sz) && sz <= 64) { + n = r.get_uint64(); + return true; + } + return false; + } + + bool is_bound(expr *e, expr*& v, interval& b) const { + uint64 n; + expr *lhs = 0, *rhs = 0; + unsigned sz; + + if (m_bv.is_bv_ule(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C ule x <=> x uge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, uMaxInt(sz), sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x ule C + b = interval(0, n, sz, true); + v = lhs; + return true; + } + } + else if (m_bv.is_bv_sle(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { // C sle x <=> x sge C + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, (1ull << (sz-1)) - 1, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { // x sle C + b = interval(1ull << (sz-1), n, sz, true); + v = lhs; + return true; + } + } else if (m.is_eq(e, lhs, rhs)) { + if (is_number(lhs, n, sz)) { + if (m_bv.is_numeral(rhs)) + return false; + b = interval(n, n, sz, true); + v = rhs; + return true; + } + if (is_number(rhs, n, sz)) { + b = interval(n, n, sz, true); + v = lhs; + return true; + } + } + return false; + } + + + public: + dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { + updt_params(p); + } + + virtual void updt_params(params_ref const & p) { + m_propagate_eq = p.get_bool("propagate_eq", false); + } + + static void get_param_descrs(param_descrs& r) { + r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); + } + + virtual ~dom_bv_bounds_simplifier() { + for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { + dealloc(m_expr_vars[i]); + } + for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { + dealloc(m_bound_exprs[i]); + } + } + + virtual bool assert_expr(expr * t, bool sign) { + while (m.is_not(t, t)) { + sign = !sign; + } + + interval b; + expr* t1; + if (is_bound(t, t1, b)) { + SASSERT(!m_bv.is_numeral(t1)); + if (sign) + VERIFY(b.negate(b)); + + TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); + map::obj_map_entry* e = m_bound.find_core(t1); + if (e) { + interval& old = e->get_data().m_value; + interval intr; + if (!old.intersect(b, intr)) + return false; + if (old == intr) + return true; + m_scopes.insert(undo_bound(t1, old, false)); + old = intr; + } else { + m_bound.insert(t1, b); + m_scopes.insert(undo_bound(t1, interval(), true)); + } + } + return true; + } + + virtual void operator()(expr_ref& r) { + expr* t1, * t = r; + interval b; + + if (m_bound.find(t, b) && b.is_singleton()) { + r = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); + return; + } + + if (!m.is_bool(t)) + return; + + bool sign = false; + while (m.is_not(t, t)) { + sign = !sign; + } + + if (!is_bound(t, t1, b)) + return; + + if (sign && b.tight) { + sign = false; + if (!b.negate(b)) { + r = m.mk_false(); + return; + } + } + + interval ctx, intr; + bool unchanged = false; + if (b.is_full() && b.tight) { + r = m.mk_true(); + } else if (m_bound.find(t1, ctx)) { + if (ctx.implies(b)) { + r = m.mk_true(); + } else if (!b.intersect(ctx, intr)) { + r = m.mk_false(); + } else if (m_propagate_eq && intr.is_singleton()) { + r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), + m.get_sort(t1))); + } + } + else { + unchanged = true; + } + + CTRACE("bv", !unchanged, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); + if (sign && unchanged) + r = m.mk_not(r); + } + + // check if t contains v + ptr_vector todo; + bool contains(expr* t, expr* v) { + ast_fast_mark1 mark; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark.is_marked(t)) { + continue; + } + if (t == v) { + todo.reset(); + return true; + } + mark.mark(t); + + if (!is_app(t)) { + continue; + } + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + bool contains_bound(expr* t) { + ast_fast_mark1 mark1; + ast_fast_mark2 mark2; + + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark1.is_marked(t)) { + continue; + } + mark1.mark(t); + + if (!is_app(t)) { + continue; + } + interval b; + expr* e; + if (is_bound(t, e, b)) { + if (mark2.is_marked(e)) { + todo.reset(); + return true; + } + mark2.mark(e); + if (m_bound.contains(e)) { + todo.reset(); + return true; + } + } + + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + virtual bool may_simplify(expr* t) { + if (m_bv.is_numeral(t)) + return false; + + while (m.is_not(t, t)); + + for (auto & v : m_bound) { + if (contains(t, v.m_key)) return true; + } + +#if 0 + expr_set* used_exprs = get_expr_vars(t); + for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { + if (contains(t, I->m_key)) return true; + if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) + return true; + } +#endif + + expr* t1; + interval b; + // skip common case: single bound constraint without any context for simplification + if (is_bound(t, t1, b)) { + return b.is_full() || m_bound.contains(t1); + } + + if (contains_bound(t)) { + return true; + } +#if 0 + expr_cnt* bounds = get_expr_bounds(t); + for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { + if (I->m_value > 1 || m_bound.contains(I->m_key)) + return true; + } +#endif + return false; + } + + virtual void pop(unsigned num_scopes) { + TRACE("bv", tout << "pop: " << num_scopes << "\n";); + if (m_scopes.empty()) + return; + unsigned target = m_scopes.size() - num_scopes; + if (target == 0) { + m_bound.reset(); + m_scopes.reset(); + return; + } + for (unsigned i = m_scopes.size()-1; i >= target; --i) { + undo_bound& undo = m_scopes[i]; + SASSERT(m_bound.contains(undo.e)); + if (undo.fresh) { + m_bound.erase(undo.e); + } else { + m_bound.insert(undo.e, undo.b); + } + } + m_scopes.shrink(target); + } + + virtual dom_simplifier * translate(ast_manager & m) { + return alloc(dom_bv_bounds_simplifier, m, m_params); + } + + virtual unsigned scope_level() const { + return m_scopes.size(); + } + }; } tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m, p), p)); } + +tactic * mk_dom_bv_bounds_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(dom_simplify_tactic, m, alloc(dom_bv_bounds_simplifier, m, p), p)); +} diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 08037fe18..d38324db9 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -83,11 +83,12 @@ expr* expr_dominators::intersect(expr* x, expr * y) { return x; } -void expr_dominators::compute_dominators() { +bool expr_dominators::compute_dominators() { expr * e = m_root; SASSERT(m_doms.empty()); m_doms.insert(e, e); bool change = true; + unsigned iterations = 1; while (change) { change = false; SASSERT(m_post2expr.empty() || m_post2expr.back() == e); @@ -109,7 +110,12 @@ void expr_dominators::compute_dominators() { change = true; } } + iterations *= 2; + if (change && iterations > m_post2expr.size()) { + return false; + } } + return true; } void expr_dominators::extract_tree() { @@ -118,17 +124,18 @@ void expr_dominators::extract_tree() { } } -void expr_dominators::compile(expr * e) { +bool expr_dominators::compile(expr * e) { reset(); m_root = e; compute_post_order(); - compute_dominators(); + if (!compute_dominators()) return false; extract_tree(); + return true; } -void expr_dominators::compile(unsigned sz, expr * const* es) { +bool expr_dominators::compile(unsigned sz, expr * const* es) { expr_ref e(m.mk_and(sz, es), m); - compile(e); + return compile(e); } void expr_dominators::reset() { @@ -293,14 +300,14 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { } -void dom_simplify_tactic::init(goal& g) { +bool dom_simplify_tactic::init(goal& g) { expr_ref_vector args(m); unsigned sz = g.size(); for (unsigned i = 0; i < sz; ++i) args.push_back(g.form(i)); expr_ref fml = mk_and(args); m_result.reset(); m_trail.reset(); - m_dominators.compile(fml); + return m_dominators.compile(fml); } void dom_simplify_tactic::simplify_goal(goal& g) { @@ -312,7 +319,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { change = false; // go forwards - init(g); + if (!init(g)) return; unsigned sz = g.size(); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { expr_ref r = simplify(g.form(i)); @@ -329,7 +336,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { pop(scope_level()); // go backwards - init(g); + if (!init(g)) return; sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { --i; diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 25fb7c24f..6e5833cdb 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -45,14 +45,14 @@ private: void compute_post_order(); expr* intersect(expr* x, expr * y); - void compute_dominators(); + bool compute_dominators(); void extract_tree(); public: expr_dominators(ast_manager& m): m(m), m_root(m) {} - void compile(expr * e); - void compile(unsigned sz, expr * const* es); + bool compile(expr * e); + bool compile(unsigned sz, expr * const* es); tree_t const& get_tree() { return m_tree; } void reset(); @@ -115,7 +115,7 @@ private: void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); } bool assert_expr(expr* f, bool sign) { m_scope_level++; return m_simplifier->assert_expr(f, sign); } - void init(goal& g); + bool init(goal& g); public: dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()): From 755ca46df65209f275966886acc968ea02533992 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 12:15:41 +0100 Subject: [PATCH 25/41] adding bv_bounds tactic dominator style Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/bv_bounds_tactic.cpp | 58 +++++------------------------- 1 file changed, 9 insertions(+), 49 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 2d5eb216a..44f920840 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -560,7 +560,7 @@ namespace { bool is_bound(expr *e, expr*& v, interval& b) const { uint64 n; expr *lhs = 0, *rhs = 0; - unsigned sz; + unsigned sz = 0; if (m_bv.is_bv_ule(e, lhs, rhs)) { if (is_number(lhs, n, sz)) { // C ule x <=> x uge C @@ -689,25 +689,27 @@ namespace { } interval ctx, intr; - bool unchanged = false; + bool was_updated = true; if (b.is_full() && b.tight) { r = m.mk_true(); } else if (m_bound.find(t1, ctx)) { if (ctx.implies(b)) { r = m.mk_true(); - } else if (!b.intersect(ctx, intr)) { + } + else if (!b.intersect(ctx, intr)) { r = m.mk_false(); - } else if (m_propagate_eq && intr.is_singleton()) { + } + else if (m_propagate_eq && intr.is_singleton()) { r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), m.get_sort(t1))); } } else { - unchanged = true; + was_updated = false; } - CTRACE("bv", !unchanged, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); - if (sign && unchanged) + CTRACE("bv", was_updated, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); + if (sign && was_updated) r = m.mk_not(r); } @@ -773,45 +775,6 @@ namespace { return false; } - virtual bool may_simplify(expr* t) { - if (m_bv.is_numeral(t)) - return false; - - while (m.is_not(t, t)); - - for (auto & v : m_bound) { - if (contains(t, v.m_key)) return true; - } - -#if 0 - expr_set* used_exprs = get_expr_vars(t); - for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { - if (contains(t, I->m_key)) return true; - if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) - return true; - } -#endif - - expr* t1; - interval b; - // skip common case: single bound constraint without any context for simplification - if (is_bound(t, t1, b)) { - return b.is_full() || m_bound.contains(t1); - } - - if (contains_bound(t)) { - return true; - } -#if 0 - expr_cnt* bounds = get_expr_bounds(t); - for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { - if (I->m_value > 1 || m_bound.contains(I->m_key)) - return true; - } -#endif - return false; - } - virtual void pop(unsigned num_scopes) { TRACE("bv", tout << "pop: " << num_scopes << "\n";); if (m_scopes.empty()) @@ -838,9 +801,6 @@ namespace { return alloc(dom_bv_bounds_simplifier, m, m_params); } - virtual unsigned scope_level() const { - return m_scopes.size(); - } }; } From 690b17fc25d8b8bac8af63ae4788e37b29b20cee Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 6 Oct 2017 12:33:47 +0100 Subject: [PATCH 26/41] Removed Ubuntu x86 VSTS/CI build (not supported by VSTS anymore). --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 197928877..701556cc8 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 | 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) +| Windows x86 | Windows x64 | Ubuntu x64 | 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) | [![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 d47aea398730634444bd31172fd2a04739a9efa7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 11:23:44 +0100 Subject: [PATCH 27/41] [TravisCI] Workaround slow unit test execution for Debug builds. Unit tests execute very slowly in Debug (i.e. unoptimized) builds. This causes TravisCI to terminate the job due to no console output being seen. To workaround this for the debug builds the tests are just compiled but not executed. To implement this the `RUN_UNIT_TESTS` environment variable now can take on the values `BUILD_ONLY`, `BUILD_AND_RUN`, and `SKIP` rather than `0` or `1`. --- .travis.yml | 11 ++++-- contrib/ci/README.md | 2 +- contrib/ci/scripts/ci_defaults.sh | 2 +- .../ci/scripts/test_z3_unit_tests_cmake.sh | 36 ++++++++++++++----- 4 files changed, 38 insertions(+), 13 deletions(-) diff --git a/.travis.yml b/.travis.yml index 50d63e593..ac00ef918 100644 --- a/.travis.yml +++ b/.travis.yml @@ -22,10 +22,17 @@ env: # 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 + # Debug builds + # + # Note the unit tests for the debug builds are compiled but **not** + # executed. This is because the debug build of unit tests takes a large + # amount of time to execute compared to the optimized builds. The hope is + # that just running the optimized unit tests is sufficient. + # # 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 + - 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 RUN_UNIT_TESTS=BUILD_ONLY # 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 + - 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 RUN_UNIT_TESTS=BUILD_ONLY # 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 diff --git a/contrib/ci/README.md b/contrib/ci/README.md index 2e117c8b1..e4c9aecfd 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -31,7 +31,7 @@ the future. * `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`) +* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`) * `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`) diff --git a/contrib/ci/scripts/ci_defaults.sh b/contrib/ci/scripts/ci_defaults.sh index 2fb3fa52a..d8e9376d8 100644 --- a/contrib/ci/scripts/ci_defaults.sh +++ b/contrib/ci/scripts/ci_defaults.sh @@ -10,7 +10,7 @@ export JAVA_BINDINGS="${JAVA_BINDINGS:-1}" export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}" export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}" export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}" -export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}" +export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}" export TARGET_ARCH="${TARGET_ARCH:-x86_64}" export TEST_INSTALL="${TEST_INSTALL:-1}" export UBSAN_BUILD="${UBSAN_BUILD:-0}" diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh index 666673328..e1c927f58 100755 --- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh +++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh @@ -10,17 +10,35 @@ 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[@]}" -# Run all tests that don't require arguments -run_quiet ./test-z3 /a +function build_unit_tests() { + # Build internal tests + cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}" +} + +function run_unit_tests() { + # Run all tests that don't require arguments + run_quiet ./test-z3 /a +} + +case "${RUN_UNIT_TESTS}" in + BUILD_AND_RUN) + build_unit_tests + run_unit_tests + ;; + BUILD_ONLY) + build_unit_tests + ;; + SKIP) + echo "RUN_UNIT_TESTS set to \"${RUN_UNIT_TESTS}\" so skipping build and run" + exit 0 + ;; + *) + echo "Error: RUN_UNIT_TESTS set to unhandled value \"${RUN_UNIT_TESTS}\"" + exit 1 + ;; +esac From 2519719d3f452eb2cbbaf0db822e58b671e4e74f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 11:30:06 +0100 Subject: [PATCH 28/41] Fix typo --- contrib/ci/scripts/set_generator_args.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/ci/scripts/set_generator_args.sh b/contrib/ci/scripts/set_generator_args.sh index 0ef7b76aa..a704c518b 100644 --- a/contrib/ci/scripts/set_generator_args.sh +++ b/contrib/ci/scripts/set_generator_args.sh @@ -1,4 +1,4 @@ -# This script should is intended to be included by other +# This script is intended to be included by other # scripts and should not be executed directly : ${Z3_CMAKE_GENERATOR?"Z3_CMAKE_GENERATOR must be specified"} From 0be28b66fe3319be01492a0391514727e099916c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 11:48:20 +0100 Subject: [PATCH 29/41] [TravisCI] Update out of date `README.md` file. --- contrib/ci/README.md | 46 ++++++++++++++++++++++++++++++++++++++------ 1 file changed, 40 insertions(+), 6 deletions(-) diff --git a/contrib/ci/README.md b/contrib/ci/README.md index e4c9aecfd..99bbcd7a6 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -58,8 +58,9 @@ The `scripts/travis_ci_linux_entry_point.sh` script 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`. +The default values of the configuration environment variables +can be found in +[`scripts/ci_defaults.sh`](scripts/ci_defaults.sh). #### Linux specific configuration variables @@ -67,8 +68,9 @@ found in `Dockerfiles/z3_build.Dockerfile`. #### 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. +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. @@ -104,11 +106,43 @@ 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. +image every time. An [organization](https://hub.docker.com/u/z3prover/) has been created on DockerHub for this. ### macOS -Not yet implemented. +For macOS we execute directly on TravisCI's macOS environment. The entry point +for the TravisCI builds is the +[`scripts/travis_ci_osx_entry_point.sh`](scripts/travis_ci_osx_entry_point.sh) +scripts. + +#### macOS specific configuration variables + +* `MACOS_SKIP_DEPS_UPDATE` - If set to `1` installing the necessary build dependencies + is skipped. This is useful for local testing if the dependencies are already installed. +* `MACOS_UPDATE_CMAKE` - If set to `1` the installed version of CMake will be upgraded. + +#### Reproducing a build locally + +To reproduce a build (e.g. like the one shown below) + +```yaml +- os: osx + osx_image: xcode8.3 + # Note: Apple Clang does not support OpenMP + env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 +``` + +Run the following: + +```bash +TRAVIS_BUILD_DIR=$(pwd) \ +Z3_BUILD_TYPE=RelWithDebInfo \ +USE_OPEN_MP=0 \ +contrib/ci/scripts/travis_ci_osx_entry_point.sh +``` + +Note this assumes that the current working directory is the root of the Z3 +git repository. From 50042ab6388f5bd4bb7b8ba23622b96b7ef59131 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 6 Oct 2017 13:00:09 +0100 Subject: [PATCH 30/41] removed unused variables --- src/ast/fpa/fpa2bv_converter.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index f09ddcd42..13a7599a9 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1180,8 +1180,6 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) { void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); expr * x = args[0], * y = args[1]; @@ -1227,8 +1225,6 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); expr * x = args[0], *y = args[1]; @@ -3081,8 +3077,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * mk_is_nan(x, x_is_nan); sort * fp_srt = m.get_sort(x); - unsigned ebits = m_util.get_ebits(fp_srt); - unsigned sbits = m_util.get_sbits(fp_srt); expr_ref unspec(m); mk_to_ieee_bv_unspecified(f, num, args, unspec); From 2634be01aa0c615e3b8b1362ce317f783b7109fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 13:43:01 +0100 Subject: [PATCH 31/41] adding backwards pass Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 35 +++++++++++++++++-------- src/tactic/core/dom_simplify_tactic.h | 3 ++- 2 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index d38324db9..da704bd0b 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -281,17 +281,28 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { }; expr_ref_vector args(m); - for (expr * arg : *e) { - for (expr * child : tree(arg)) { - if (is_subexpr_arg(child, arg)) { - simplify(child); - } - } - r = simplify(arg); - args.push_back(r); - if (!assert_expr(simplify(arg), !is_and)) { - r = is_and ? m.mk_false() : m.mk_true(); - return r; + if (m_forward) { + for (expr * arg : *e) { +#define _SIMP_ARG(arg) \ + for (expr * child : tree(arg)) { \ + if (is_subexpr_arg(child, arg)) { \ + simplify(child); \ + } \ + } \ + r = simplify(arg); \ + args.push_back(r); \ + if (!assert_expr(simplify(arg), !is_and)) { \ + r = is_and ? m.mk_false() : m.mk_true(); \ + return r; \ + } + _SIMP_ARG(arg); + } + } + else { + for (unsigned i = e->get_num_args(); i > 0; ) { + --i; + expr* arg = e->get_arg(i); + _SIMP_ARG(arg); } } pop(scope_level() - old_lvl); @@ -319,6 +330,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { change = false; // go forwards + m_forward = true; if (!init(g)) return; unsigned sz = g.size(); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { @@ -336,6 +348,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { pop(scope_level()); // go backwards + m_forward = false; if (!init(g)) return; sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 6e5833cdb..581d40cd0 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -96,6 +96,7 @@ private: unsigned m_max_depth; ptr_vector m_empty; obj_pair_map m_subexpr_cache; + bool m_forward; expr_ref simplify(expr* t); expr_ref simplify_ite(app * ite); @@ -122,7 +123,7 @@ public: m(m), m_simplifier(s), m_params(p), m_trail(m), m_args(m), m_dominators(m), - m_scope_level(0), m_depth(0), m_max_depth(1024) {} + m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {} virtual ~dom_simplify_tactic() {} From 9aa6386be94e96651b5c12065cb95a9e4dea74b8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 6 Oct 2017 15:27:16 +0100 Subject: [PATCH 32/41] fix debug build --- src/util/lp/indexed_vector_instances.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/lp/indexed_vector_instances.cpp b/src/util/lp/indexed_vector_instances.cpp index ee078f021..79c3ee1a1 100644 --- a/src/util/lp/indexed_vector_instances.cpp +++ b/src/util/lp/indexed_vector_instances.cpp @@ -33,6 +33,7 @@ template void indexed_vector::resize(unsigned int); template void indexed_vector::set_value(const mpq&, unsigned int); template void indexed_vector::set_value(const unsigned&, unsigned int); #ifdef Z3DEBUG +template bool indexed_vector::is_OK() const; template bool indexed_vector::is_OK() const; template bool indexed_vector::is_OK() const; template bool indexed_vector >::is_OK() const; From ba8bff76ae9a68bef78c88913cbc2c62a193b299 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 15:52:01 +0100 Subject: [PATCH 33/41] [TravisCI] Modify Debug configuration that I forgot to change with `RUN_UNIT_TESTS=BUILD_ONLY`. --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index ac00ef918..81ddefb8b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -64,7 +64,7 @@ env: # 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 + - 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 RUN_UNIT_TESTS=BUILD_ONLY # macOS (a.k.a OSX) support matrix: From c3f615dbfcf1436a142d1112598f358ed6c27bbd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 16:03:43 +0100 Subject: [PATCH 34/41] reverse arguments Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index da704bd0b..67b039814 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -291,7 +291,7 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { } \ r = simplify(arg); \ args.push_back(r); \ - if (!assert_expr(simplify(arg), !is_and)) { \ + if (!assert_expr(r, !is_and)) { \ r = is_and ? m.mk_false() : m.mk_true(); \ return r; \ } @@ -304,6 +304,7 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { expr* arg = e->get_arg(i); _SIMP_ARG(arg); } + args.reverse(); } pop(scope_level() - old_lvl); r = is_and ? mk_and(args) : mk_or(args); @@ -338,6 +339,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } + CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";); change |= r != g.form(i); proof* new_pr = 0; if (g.proofs_enabled()) { @@ -358,6 +360,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { r = m.mk_false(); } change |= r != g.form(i); + CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";); proof* new_pr = 0; if (g.proofs_enabled()) { new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, 0)); From 31c6b3eb5b94053c8c40f2939ad429c31471edaa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Oct 2017 16:07:25 +0100 Subject: [PATCH 35/41] fix leak Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 4 ++++ src/tactic/core/dom_simplify_tactic.h | 4 +--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 67b039814..99f83799b 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -152,6 +152,10 @@ void expr_dominators::reset() { // ----------------------- // dom_simplify_tactic +dom_simplify_tactic::~dom_simplify_tactic() { + dealloc(m_simplifier); +} + tactic * dom_simplify_tactic::translate(ast_manager & m) { return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 581d40cd0..c1660a941 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -83,8 +83,6 @@ class dom_simplifier { }; class dom_simplify_tactic : public tactic { -public: -private: ast_manager& m; dom_simplifier* m_simplifier; params_ref m_params; @@ -126,7 +124,7 @@ public: m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {} - virtual ~dom_simplify_tactic() {} + virtual ~dom_simplify_tactic(); virtual tactic * translate(ast_manager & m); virtual void updt_params(params_ref const & p) {} From 1d12a9c86de07feafe1261fa52b8248fe1d494ef Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 6 Oct 2017 18:19:37 +0100 Subject: [PATCH 36/41] dom_simplifier: fix dominator computation --- src/tactic/core/dom_simplify_tactic.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 99f83799b..16d8500a4 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -95,17 +95,17 @@ bool expr_dominators::compute_dominators() { for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; - SASSERT(!p.empty()); expr * new_idom = 0, *idom2 = 0; - for (unsigned j = 0; j < p.size(); ++j) { - if (!new_idom) { - m_doms.find(p[j], new_idom); - } - else if (m_doms.find(p[j], idom2)) { - new_idom = intersect(new_idom, idom2); + for (auto& pred : p) { + if (m_doms.contains(pred)) { + new_idom = !new_idom ? pred : intersect(new_idom, pred); } } - if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) { + if (!new_idom) { + m_doms.insert(child, p[0]); + change = true; + } + else if (!m_doms.find(child, idom2) || idom2 != new_idom) { m_doms.insert(child, new_idom); change = true; } From a18236bc7f2a9037ccd1d7d078cb54c132328474 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 00:07:53 +0100 Subject: [PATCH 37/41] have quantifier equality take names into account Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 3 ++ src/ast/expr_abstract.cpp | 9 ++++ src/ast/expr_substitution.cpp | 7 +++ src/ast/expr_substitution.h | 3 ++ src/tactic/core/dom_simplify_tactic.cpp | 65 ++++++++++++++++++++----- src/tactic/core/dom_simplify_tactic.h | 5 +- 6 files changed, 78 insertions(+), 14 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c98307ee0..cac12413e 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -471,6 +471,9 @@ bool compare_nodes(ast const * n1, ast const * n2) { compare_arrays(to_quantifier(n1)->get_decl_sorts(), to_quantifier(n2)->get_decl_sorts(), to_quantifier(n1)->get_num_decls()) && + compare_arrays(to_quantifier(n1)->get_decl_names(), + to_quantifier(n2)->get_decl_names(), + to_quantifier(n1)->get_num_decls()) && to_quantifier(n1)->get_expr() == to_quantifier(n2)->get_expr() && to_quantifier(n1)->get_weight() == to_quantifier(n2)->get_weight() && to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() && diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp index 46682eed6..43035e203 100644 --- a/src/ast/expr_abstract.cpp +++ b/src/ast/expr_abstract.cpp @@ -19,6 +19,7 @@ Notes: #include "ast/expr_abstract.h" #include "util/map.h" +#include "ast/ast_pp.h" void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { @@ -109,6 +110,9 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) { expr_abstractor abs(m); abs(base, num_bound, bound, n, result); + TRACE("expr_abstract", + tout << expr_ref(n, m) << "\n"; + tout << result << "\n";); } expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) { @@ -123,6 +127,11 @@ expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* } result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result); } + TRACE("expr_abstract", + tout << expr_ref(n, m) << "\n"; + for (unsigned i = 0; i < num_bound; ++i) tout << expr_ref(bound[i], m) << " "; + tout << "\n"; + tout << result << "\n";); return result; } diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp index 149a59ce5..3ce038250 100644 --- a/src/ast/expr_substitution.cpp +++ b/src/ast/expr_substitution.cpp @@ -56,6 +56,13 @@ expr_substitution::~expr_substitution() { reset(); } +std::ostream& expr_substitution::display(std::ostream& out) { + for (auto & kv : m_subst) { + out << expr_ref(kv.m_key, m()) << " |-> " << expr_ref(kv.m_value, m()) << "\n"; + } + return out; +} + void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) { obj_map::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0); if (entry->get_data().m_value == 0) { diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index d360356eb..90154d163 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -50,6 +50,8 @@ public: bool contains(expr * s); void reset(); void cleanup(); + + std::ostream& display(std::ostream& out); }; class scoped_expr_substitution { @@ -84,6 +86,7 @@ public: bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); } bool contains(expr * s) { return m_subst.contains(s); } void cleanup() { m_subst.cleanup(); } + std::ostream& display(std::ostream& out) { return m_subst.display(out); } }; #endif diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 99f83799b..60207e823 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -91,23 +91,42 @@ bool expr_dominators::compute_dominators() { unsigned iterations = 1; while (change) { change = false; + TRACE("simplify", + for (auto & kv : m_doms) { + tout << expr_ref(kv.m_key, m) << " |-> " << expr_ref(kv.m_value, m) << "\n"; + }); + SASSERT(m_post2expr.empty() || m_post2expr.back() == e); for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; SASSERT(!p.empty()); - expr * new_idom = 0, *idom2 = 0; - for (unsigned j = 0; j < p.size(); ++j) { - if (!new_idom) { - m_doms.find(p[j], new_idom); - } - else if (m_doms.find(p[j], idom2)) { - new_idom = intersect(new_idom, idom2); - } + if (p.size() == 1) { + if (!m_doms.contains(child)) { + m_doms.insert(child, p[0]); + change = true; + } } - if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) { - m_doms.insert(child, new_idom); - change = true; + else { + expr * new_idom = 0, *idom2 = 0; + for (unsigned j = 0; j < p.size(); ++j) { + if (!new_idom) { + m_doms.find(p[j], new_idom); + } + else if (m_doms.find(p[j], idom2)) { + new_idom = intersect(new_idom, idom2); + } + } + if (!new_idom) { + m_doms.insert(child, p[0]); + TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(p[0], m) << "\n";); + change = true; + } + else if (!m_doms.find(child, idom2) || idom2 != new_idom) { + m_doms.insert(child, new_idom); + TRACE("simplify", tout << expr_ref(child, m) << " |-> " << expr_ref(new_idom, m) << "\n";); + change = true; + } } } iterations *= 2; @@ -130,6 +149,7 @@ bool expr_dominators::compile(expr * e) { compute_post_order(); if (!compute_dominators()) return false; extract_tree(); + TRACE("simplify", display(tout);); return true; } @@ -147,6 +167,22 @@ void expr_dominators::reset() { m_root.reset(); } +std::ostream& expr_dominators::display(std::ostream& out) { + return display(out, 0, m_root); +} + +std::ostream& expr_dominators::display(std::ostream& out, unsigned indent, expr* r) { + for (unsigned i = 0; i < indent; ++i) out << " "; + out << expr_ref(r, m); + if (m_tree.contains(r)) { + for (expr* child : m_tree[r]) { + if (child != r) + display(out, indent + 1, child); + } + } + out << "\n"; + return out; +} // ----------------------- @@ -200,7 +236,6 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { simplify(child); } } - pop(scope_level() - old_lvl); expr_ref new_t = simplify(t); if (!assert_expr(new_c, true)) { @@ -230,6 +265,8 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr_ref dom_simplify_tactic::simplify(expr * e0) { expr_ref r(m); expr* e = 0; + + TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); if (!m_result.find(e0, e)) { e = e0; } @@ -254,7 +291,9 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { if (is_app(e)) { m_args.reset(); for (expr* arg : *to_app(e)) { - m_args.push_back(get_cached(arg)); // TBD is cache really applied to all sub-terms? + r = get_cached(arg); + (*m_simplifier)(r); + m_args.push_back(r); } r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr()); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index c1660a941..d99f799b4 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -48,6 +48,8 @@ private: bool compute_dominators(); void extract_tree(); + std::ostream& display(std::ostream& out, unsigned indent, expr* r); + public: expr_dominators(ast_manager& m): m(m), m_root(m) {} @@ -55,7 +57,8 @@ public: bool compile(unsigned sz, expr * const* es); tree_t const& get_tree() { return m_tree; } void reset(); - + + std::ostream& display(std::ostream& out); }; class dom_simplifier { From 76c309a595639cbbde974f8efe2b42f24a9d7e8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 00:20:58 +0100 Subject: [PATCH 38/41] disable caching of simplifier when applied to direct arguments of terms. Caching is only valid when applied to dominator children Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 31 +++++++++++++------------ src/tactic/core/dom_simplify_tactic.h | 2 +- 2 files changed, 17 insertions(+), 16 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 830d44c7a..1bd685bb1 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -101,7 +101,8 @@ bool expr_dominators::compute_dominators() { expr * child = m_post2expr[i]; ptr_vector const& p = m_parents[child]; expr * new_idom = 0, *idom2 = 0; - for (auto& pred : p) { + + for (expr * pred : p) { if (m_doms.contains(pred)) { new_idom = !new_idom ? pred : intersect(new_idom, pred); } @@ -209,31 +210,31 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr * c = 0, *t = 0, *e = 0; VERIFY(m.is_ite(ite, c, t, e)); unsigned old_lvl = scope_level(); - expr_ref new_c = simplify(c); + expr_ref new_c = simplify(c, false); if (m.is_true(new_c)) { - r = simplify(t); + r = simplify(t, false); } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { - r = simplify(e); + r = simplify(e, false); } else { for (expr * child : tree(ite)) { if (is_subexpr(child, t) && !is_subexpr(child, e)) { - simplify(child); + simplify(child, true); } } pop(scope_level() - old_lvl); - expr_ref new_t = simplify(t); + expr_ref new_t = simplify(t, false); if (!assert_expr(new_c, true)) { return new_t; } for (expr * child : tree(ite)) { if (is_subexpr(child, e) && !is_subexpr(child, t)) { - simplify(child); + simplify(child, true); } } pop(scope_level() - old_lvl); - expr_ref new_e = simplify(e); + expr_ref new_e = simplify(e, false); if (c == new_c && t == new_t && e == new_e) { r = ite; } @@ -248,7 +249,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { return r; } -expr_ref dom_simplify_tactic::simplify(expr * e0) { +expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) { expr_ref r(m); expr* e = 0; @@ -272,7 +273,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { } else { for (expr * child : tree(e)) { - simplify(child); + simplify(child, true); } if (is_app(e)) { m_args.reset(); @@ -288,7 +289,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) { } } (*m_simplifier)(r); - cache(e0, r); + if (cache_result) cache(e0, r); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); --m_depth; m_subexpr_cache.reset(); @@ -315,10 +316,10 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { #define _SIMP_ARG(arg) \ for (expr * child : tree(arg)) { \ if (is_subexpr_arg(child, arg)) { \ - simplify(child); \ + simplify(child, true); \ } \ } \ - r = simplify(arg); \ + r = simplify(arg, false); \ args.push_back(r); \ if (!assert_expr(r, !is_and)) { \ r = is_and ? m.mk_false() : m.mk_true(); \ @@ -364,7 +365,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { if (!init(g)) return; unsigned sz = g.size(); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { - expr_ref r = simplify(g.form(i)); + expr_ref r = simplify(g.form(i), true); if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } @@ -384,7 +385,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { --i; - expr_ref r = simplify(g.form(i)); + expr_ref r = simplify(g.form(i), true); if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index d99f799b4..e79777215 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -99,7 +99,7 @@ class dom_simplify_tactic : public tactic { obj_pair_map m_subexpr_cache; bool m_forward; - expr_ref simplify(expr* t); + expr_ref simplify(expr* t, bool cache); expr_ref simplify_ite(app * ite); expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); } expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); } From 7e4f5322023ddf5d1a4ae485d710c4f8c59a65f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 00:37:44 +0100 Subject: [PATCH 39/41] fix build by including mk_pp Signed-off-by: Nikolaj Bjorner --- src/ast/expr_substitution.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp index 3ce038250..f9333c443 100644 --- a/src/ast/expr_substitution.cpp +++ b/src/ast/expr_substitution.cpp @@ -16,8 +16,9 @@ Author: Notes: --*/ -#include "ast/expr_substitution.h" #include "util/ref_util.h" +#include "ast/expr_substitution.h" +#include "ast/ast_pp.h" typedef obj_map expr2proof; typedef obj_map expr2expr_dependency; @@ -58,7 +59,7 @@ expr_substitution::~expr_substitution() { std::ostream& expr_substitution::display(std::ostream& out) { for (auto & kv : m_subst) { - out << expr_ref(kv.m_key, m()) << " |-> " << expr_ref(kv.m_value, m()) << "\n"; + out << mk_pp(kv.m_key, m()) << " |-> " << mk_pp(kv.m_value, m()) << "\n"; } return out; } From b898b077953c8e4a18d9b49567af37952e889eb8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 11:12:09 +0100 Subject: [PATCH 40/41] distinguish simplify_rec from simplify immediate argument Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 40 ++++++++++++++----------- src/tactic/core/dom_simplify_tactic.h | 3 +- 2 files changed, 25 insertions(+), 18 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 1bd685bb1..366e1edb0 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -210,31 +210,31 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { expr * c = 0, *t = 0, *e = 0; VERIFY(m.is_ite(ite, c, t, e)); unsigned old_lvl = scope_level(); - expr_ref new_c = simplify(c, false); + expr_ref new_c = simplify_arg(c); if (m.is_true(new_c)) { - r = simplify(t, false); + r = simplify_arg(t); } else if (m.is_false(new_c) || !assert_expr(new_c, false)) { - r = simplify(e, false); + r = simplify_arg(e); } else { for (expr * child : tree(ite)) { if (is_subexpr(child, t) && !is_subexpr(child, e)) { - simplify(child, true); + simplify_rec(child); } } pop(scope_level() - old_lvl); - expr_ref new_t = simplify(t, false); + expr_ref new_t = simplify_arg(t); if (!assert_expr(new_c, true)) { return new_t; } for (expr * child : tree(ite)) { if (is_subexpr(child, e) && !is_subexpr(child, t)) { - simplify(child, true); + simplify_rec(child); } } pop(scope_level() - old_lvl); - expr_ref new_e = simplify(e, false); + expr_ref new_e = simplify_arg(e); if (c == new_c && t == new_t && e == new_e) { r = ite; } @@ -249,7 +249,15 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) { return r; } -expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) { +expr_ref dom_simplify_tactic::simplify_arg(expr * e) { + expr_ref r(m); + r = get_cached(e); + (*m_simplifier)(r); + TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e, m) << " -> " << r << "\n";); + return r; +} + +expr_ref dom_simplify_tactic::simplify_rec(expr * e0) { expr_ref r(m); expr* e = 0; @@ -273,14 +281,12 @@ expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) { } else { for (expr * child : tree(e)) { - simplify(child, true); + simplify_rec(child); } if (is_app(e)) { m_args.reset(); for (expr* arg : *to_app(e)) { - r = get_cached(arg); - (*m_simplifier)(r); - m_args.push_back(r); + m_args.push_back(simplify_arg(arg)); } r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr()); } @@ -289,7 +295,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) { } } (*m_simplifier)(r); - if (cache_result) cache(e0, r); + cache(e0, r); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); --m_depth; m_subexpr_cache.reset(); @@ -316,10 +322,10 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) { #define _SIMP_ARG(arg) \ for (expr * child : tree(arg)) { \ if (is_subexpr_arg(child, arg)) { \ - simplify(child, true); \ + simplify_rec(child); \ } \ } \ - r = simplify(arg, false); \ + r = simplify_arg(arg); \ args.push_back(r); \ if (!assert_expr(r, !is_and)) { \ r = is_and ? m.mk_false() : m.mk_true(); \ @@ -365,7 +371,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { if (!init(g)) return; unsigned sz = g.size(); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { - expr_ref r = simplify(g.form(i), true); + expr_ref r = simplify_rec(g.form(i)); if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } @@ -385,7 +391,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) { --i; - expr_ref r = simplify(g.form(i), true); + expr_ref r = simplify_rec(g.form(i)); if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { r = m.mk_false(); } diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index e79777215..4f9851514 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -99,7 +99,8 @@ class dom_simplify_tactic : public tactic { obj_pair_map m_subexpr_cache; bool m_forward; - expr_ref simplify(expr* t, bool cache); + expr_ref simplify_rec(expr* t); + expr_ref simplify_arg(expr* t); expr_ref simplify_ite(app * ite); expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); } expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); } From deba7d4d6e74c2896b2f75aeeacc205618157f05 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Oct 2017 14:35:44 +0100 Subject: [PATCH 41/41] use idom for checking dominator relationships Signed-off-by: Nikolaj Bjorner --- src/tactic/core/dom_simplify_tactic.cpp | 24 ++++++++++++++++-------- src/tactic/core/dom_simplify_tactic.h | 2 ++ 2 files changed, 18 insertions(+), 8 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 366e1edb0..3a6d55569 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -257,11 +257,14 @@ expr_ref dom_simplify_tactic::simplify_arg(expr * e) { return r; } +/** + \brief simplify e recursively. +*/ expr_ref dom_simplify_tactic::simplify_rec(expr * e0) { expr_ref r(m); expr* e = 0; - TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); + TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << "\n";); if (!m_result.find(e0, e)) { e = e0; } @@ -408,6 +411,12 @@ void dom_simplify_tactic::simplify_goal(goal& g) { SASSERT(scope_level() == 0); } +/** + \brief determine if a is dominated by b. + Walk the immediate dominators of a upwards until hitting b or a term that is deeper than b. + Save intermediary results in a cache to avoid recomputations. +*/ + bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { if (a == b) return true; @@ -416,14 +425,13 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) { if (m_subexpr_cache.find(a, b, r)) return r; - for (expr * e : tree(b)) { - if (is_subexpr(a, e)) { - m_subexpr_cache.insert(a, b, true); - return true; - } + if (get_depth(a) >= get_depth(b)) { + return false; } - m_subexpr_cache.insert(a, b, false); - return false; + SASSERT(a != idom(a) && get_depth(idom(a)) > get_depth(a)); + r = is_subexpr(idom(a), b); + m_subexpr_cache.insert(a, b, r); + return r; } ptr_vector const & dom_simplify_tactic::tree(expr * e) { diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 4f9851514..79bc9728c 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -57,6 +57,7 @@ public: bool compile(unsigned sz, expr * const* es); tree_t const& get_tree() { return m_tree; } void reset(); + expr* idom(expr *e) const { return m_doms[e]; } std::ostream& display(std::ostream& out); }; @@ -113,6 +114,7 @@ class dom_simplify_tactic : public tactic { void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); } ptr_vector const & tree(expr * e); + expr* idom(expr *e) const { return m_dominators.idom(e); } unsigned scope_level() { return m_scope_level; } void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); }