From b54ef3623b796586af7f2915077946409d1734e3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 3 Jun 2016 20:26:05 +0100 Subject: [PATCH 1/7] added collect-statistics tactic --- src/tactic/core/collect_statistics_tactic.cpp | 173 ++++++++++++++++++ src/tactic/core/collect_statistics_tactic.h | 33 ++++ 2 files changed, 206 insertions(+) create mode 100644 src/tactic/core/collect_statistics_tactic.cpp create mode 100644 src/tactic/core/collect_statistics_tactic.h diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp new file mode 100644 index 000000000..f50195673 --- /dev/null +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -0,0 +1,173 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + collect_statistics_tactic.cpp + +Abstract: + + A tactic for collection of various statistics. + +Author: + + Mikolas Janota (mikjan) 2016-06-03 + Christoph (cwinter) 2016-06-03 + +Notes: + +--*/ +#include +#include + +#include"ast.h" +#include"params.h" +#include"arith_decl_plugin.h" +#include"array_decl_plugin.h" +#include"bv_decl_plugin.h" +#include"datatype_decl_plugin.h" +#include"fpa_decl_plugin.h" +#include"tactical.h" +#include"stats.h" + +#include"collect_statistics_tactic.h" + +class collect_statistics_tactic : public tactic { + ast_manager & m; + params_ref m_params; + basic_decl_plugin m_basic_pi; + arith_decl_plugin m_arith_pi; + array_decl_plugin m_array_pi; + bv_decl_plugin m_bv_pi; + datatype_decl_plugin m_datatype_pi; + fpa_decl_plugin m_fpa_pi; + + typedef std::unordered_map stats_type; + stats_type m_stats; + +public: + collect_statistics_tactic(ast_manager & m, params_ref const & p) : + m(m), + m_params(p) { + } + + virtual ~collect_statistics_tactic() {} + + virtual tactic * translate(ast_manager & m_) { + return alloc(collect_statistics_tactic, m_, m_params); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + } + + virtual void collect_param_descrs(param_descrs & r) {} + + virtual void operator()(goal_ref const & g, goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, + expr_dependency_ref & core) { + mc = 0; + tactic_report report("collect-statistics", *g); + + collect_proc cp(m, m_stats); + expr_mark visited; + const unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) + for_each_expr(cp, visited, g->form(i)); + + std::cout << "(" << std::endl; + stats_type::iterator it = m_stats.begin(); + stats_type::iterator end = m_stats.end(); + for (; it != end; it++) + std::cout << " :" << it->first << " " << it->second << std::endl; + std::cout << ")" << std::endl; + + g->inc_depth(); + result.push_back(g.get()); + } + + virtual void cleanup() {} + + virtual void collect_statistics(statistics & st) const { + } + + virtual void reset_statistics() { reset(); } + virtual void reset() { cleanup(); } + +protected: + class collect_proc { + public: + ast_manager & m; + stats_type & m_stats; + obj_hashtable m_seen_sorts; + obj_hashtable m_seen_func_decls; + + collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s) {} + + void operator()(var * v) { + m_stats["bound-variables"]++; + this->operator()(v->get_sort()); + } + + void operator()(quantifier * q) { + m_stats["quantifiers"]++; + SASSERT(is_app(q->get_expr())); + app * body = to_app(q->get_expr()); + this->operator()(body); + } + + void operator()(app * n) { + m_stats["function-applications"]++; + this->operator()(n->get_decl()); + } + + void operator()(sort * s) { + if (m.is_uninterp(s)) { + if (!m_seen_sorts.contains(s)) { + m_stats["uninterpreted-sorts"]++; + m_seen_sorts.insert(s); + } + m_stats["uninterpreted-sort-occurrences"]++; + } + else { + params_ref prms; + prms.set_bool("pp.single_line", true); + std::stringstream ss; + ss << mk_ismt2_pp(s, m, prms); + m_stats[ss.str().c_str()]++; + } + } + + void operator()(func_decl * f) { + for (unsigned i = 0; i < f->get_arity(); i++) + this->operator()(f->get_domain()[i]); + this->operator()(f->get_range()); + + if (f->get_family_id() == null_family_id) { + if (!m_seen_func_decls.contains(f)) { + if (f->get_arity() == 0) + m_stats["uninterpreted-constants"]++; + else + m_stats["uninterpreted-functions"]++; + m_seen_func_decls.insert(f); + } + + if (f->get_arity() > 0) + m_stats["uninterpreted-function-occurrences"]++; + } + else { + params_ref prms; + prms.set_bool("pp.single_line", true); + std::stringstream ss; + ss << mk_ismt2_pp(f, m, prms); + m_stats[ss.str().c_str()]++; + } + m_stats["function-applications"]++; + } + }; +}; + + +tactic * mk_collect_statistics_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(collect_statistics_tactic, m, p)); +} diff --git a/src/tactic/core/collect_statistics_tactic.h b/src/tactic/core/collect_statistics_tactic.h new file mode 100644 index 000000000..5734af3c7 --- /dev/null +++ b/src/tactic/core/collect_statistics_tactic.h @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + collect_statistics_tactic.h + +Abstract: + + A tactic for collection of various statistics. + +Author: + + Mikolas Janota (mikjan) 2016-06-03 + Christoph (cwinter) 2016-06-03 + +Notes: + +--*/ +#ifndef COLLECT_STATISTICS_H_ +#define COLLECT_STATISTICS_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_collect_statistics_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("collect-statistics", "Collects various statistics.", "mk_collect_statistics_tactic(m, p)") +*/ + + +#endif From 626b9160bfb1e7032202b489ff9bb86a64b087e5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 3 Jun 2016 20:45:42 +0100 Subject: [PATCH 2/7] collect-statistics additions --- src/tactic/core/collect_statistics_tactic.cpp | 20 ++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index f50195673..99af8f773 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -133,8 +133,14 @@ protected: params_ref prms; prms.set_bool("pp.single_line", true); std::stringstream ss; - ss << mk_ismt2_pp(s, m, prms); - m_stats[ss.str().c_str()]++; + ss << "(declare-sort " << mk_ismt2_pp(s, m, prms) << ")"; + m_stats[ss.str()]++; + + if (s->get_info()->get_num_parameters() > 0) { + std::stringstream ssname; + ssname << "(declare-sort (_ " << s->get_name() << " *))"; + m_stats[ssname.str()]++; + } } } @@ -160,8 +166,16 @@ protected: prms.set_bool("pp.single_line", true); std::stringstream ss; ss << mk_ismt2_pp(f, m, prms); - m_stats[ss.str().c_str()]++; + m_stats[ss.str()]++; + + std::stringstream ssfname; + if (f->get_num_parameters() > 0) + ssfname << "(declare-fun (_ " << f->get_name() << " *) *)"; + else + ssfname << "(declare-fun " << f->get_name() << " *)"; + m_stats[ssfname.str()]++; } + m_stats["function-applications"]++; } }; From f2a869fb5807f01e007c8ac55a7076b72e6628db Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 4 Jun 2016 11:01:46 +0100 Subject: [PATCH 3/7] std::unordered_map -> std::map --- src/tactic/core/collect_statistics_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index 99af8f773..8e8879fef 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include -#include +#include #include"ast.h" #include"params.h" @@ -42,7 +42,7 @@ class collect_statistics_tactic : public tactic { datatype_decl_plugin m_datatype_pi; fpa_decl_plugin m_fpa_pi; - typedef std::unordered_map stats_type; + typedef std::map stats_type; stats_type m_stats; public: From e8d85f91d7246f62825e72e42eff9b2107efaa99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Jun 2016 20:08:13 -0700 Subject: [PATCH 4/7] disable filtering on negated tails. Issue #634 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_filter_rules.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_filter_rules.cpp b/src/muz/transforms/dl_mk_filter_rules.cpp index d23da72fb..b112f4c99 100644 --- a/src/muz/transforms/dl_mk_filter_rules.cpp +++ b/src/muz/transforms/dl_mk_filter_rules.cpp @@ -111,7 +111,7 @@ namespace datalog { bool rule_modified = false; for (unsigned i = 0; i < sz; i++) { app * tail = r->get_tail(i); - if (is_candidate(tail)) { + if (is_candidate(tail) && !r->is_neg_tail(i)) { TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m) << "\n";); var_idx_set non_local_vars = rm.collect_rule_vars_ex(r, tail); func_decl * filter_decl = mk_filter_decl(tail, non_local_vars); From 9df2a183d6972cb408e88a3d3d245d0a2cfe45ce Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Mon, 6 Jun 2016 18:06:45 +0100 Subject: [PATCH 5/7] Adding translation to ackr_model_converter. --- src/ackermannization/ackr_info.h | 24 +++++++++++++++---- src/ackermannization/ackr_model_converter.cpp | 11 ++++++++- 2 files changed, 29 insertions(+), 6 deletions(-) diff --git a/src/ackermannization/ackr_info.h b/src/ackermannization/ackr_info.h index 703f1f3d5..76be45e2b 100644 --- a/src/ackermannization/ackr_info.h +++ b/src/ackermannization/ackr_info.h @@ -20,6 +20,7 @@ Revision History: #include"ast.h" #include"ref.h" #include"expr_replacer.h" +#include"ast_translation.h" /** \brief Information about how a formula is being converted into @@ -35,7 +36,6 @@ class ackr_info { public: ackr_info(ast_manager& m) : m_m(m) - , m_consts(m) , m_er(mk_default_expr_replacer(m)) , m_subst(m_m) , m_ref_count(0) @@ -43,16 +43,20 @@ class ackr_info { {} virtual ~ackr_info() { - m_consts.reset(); + for (t2ct::iterator i = m_t2c.begin(); i != m_t2c.end(); ++i) { + m_m.dec_ref(i->m_key); + m_m.dec_ref(i->m_value); + } } inline void set_abstr(app* term, app* c) { SASSERT(!m_sealed); - SASSERT(c); + SASSERT(c && term); m_t2c.insert(term,c); m_c2t.insert(c->get_decl(),term); m_subst.insert(term, c); - m_consts.push_back(c); + m_m.inc_ref(term); + m_m.inc_ref(c); } inline void abstract(expr * e, expr_ref& res) { @@ -77,6 +81,17 @@ class ackr_info { m_er->set_substitution(&m_subst); } + virtual ackr_info * translate(ast_translation & translator) { + ackr_info * const retv = alloc(ackr_info, translator.to()); + for (t2ct::iterator i = m_t2c.begin(); i != m_t2c.end(); ++i) { + app * const k = translator(i->m_key); + app * const v = translator(i->m_value); + retv->set_abstr(k, v); + } + if (m_sealed) retv->seal(); + return retv; + } + // // Reference counting // @@ -94,7 +109,6 @@ class ackr_info { t2ct m_t2c; // terms to constants c2tt m_c2t; // constants to terms (inversion of m_t2c) - expr_ref_vector m_consts; // the constants introduced during abstraction // replacer and substitution used to compute abstractions scoped_ptr m_er; diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index eb24ee927..ea4f858ad 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -53,7 +53,16 @@ public: //void display(std::ostream & out); - virtual model_converter * translate(ast_translation & translator) {NOT_IMPLEMENTED_YET();} + virtual model_converter * translate(ast_translation & translator) { + ackr_info_ref retv_info = info->translate(translator); + if (fixed_model) { + model_ref retv_mod_ref = abstr_model->translate(translator); + return alloc(ackr_model_converter, translator.to(), retv_info, retv_mod_ref); + } + else { + return alloc(ackr_model_converter, translator.to(), retv_info); + } + } protected: ast_manager& m; const ackr_info_ref info; From 9bfa73ee062370b35eb0dedc9611b6443f83939b Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Wed, 8 Jun 2016 11:17:26 +0900 Subject: [PATCH 6/7] Take into account number of monomials for rlimit counting Should fix issue #611 --- src/math/grobner/grobner.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index 0c96dfde3..baa16b405 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -446,6 +446,7 @@ void grobner::merge_monomials(ptr_vector & monomials) { SASSERT(&m_del_monomials != &monomials); ptr_vector& to_delete = m_del_monomials; to_delete.reset(); + m_manager.limit().inc(sz); for (unsigned i = 1; i < sz; ++i) { monomial * m1 = monomials[j]; monomial * m2 = monomials[i]; From a2eb8245900c84607c7e55ac501b75fb6d0407dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 8 Jun 2016 12:07:13 +0100 Subject: [PATCH 7/7] Added __nonzero__ and __bool__ functions to Python Z3 ASTs to enable use of Python lists (and similar). Thanks to Vlad Shcherbina for the recommendation (see http://stackoverflow.com/questions/37669576/converting-z3-cnf-formula-into-list-of-lists-representation-using-z3py/37679447?noredirect=1#comment62859886_37679447)! --- src/api/python/z3.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index c9aa9beb5..ff6e91c4a 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -292,6 +292,19 @@ class AstRef(Z3PPObject): def __hash__(self): return self.hash() + def __nonzero__(self): + return self.__bool__() + + def __bool__(self): + if is_true(self): + return True + elif is_false(self): + return False + elif is_eq(self) and self.num_args() == 2: + return self.arg(0).eq(self.arg(1)) + else: + raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.") + def sexpr(self): """Return an string representing the AST node in s-expression notation.