From 99d10d1224d92c7fd7091faa116fba7841752fee Mon Sep 17 00:00:00 2001 From: Wensheng Tang Date: Thu, 8 Dec 2016 15:09:59 +0800 Subject: [PATCH 01/23] Fixed utf-8 version string handling for python2. Resolved #787 --- scripts/mk_util.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index cdd7bdeec..d5b045d96 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -881,8 +881,8 @@ def is_CXX_gpp(): return is_compiler(CXX, 'g++') def is_clang_in_gpp_form(cc): - version_string = check_output([cc, '--version']) - return str(version_string).find('clang') != -1 + version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8') + return version_string.find('clang') != -1 def is_CXX_clangpp(): if is_compiler(CXX, 'g++'): From aca3d0545c4948a147a8efda7f2bd1e5efa4c131 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Wed, 14 Sep 2016 15:21:29 -0700 Subject: [PATCH 02/23] Set soname version correctly in cmake build --- contrib/cmake/src/CMakeLists.txt | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index f12c56f8e..6693b4f5b 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -117,14 +117,13 @@ else() set(lib_type "STATIC") endif() add_library(libz3 ${lib_type} ${object_files}) -# FIXME: Set "VERSION" and "SOVERSION" properly set_target_properties(libz3 PROPERTIES - # FIXME: Should we be using ${Z3_VERSION} here? - # VERSION: Sets up symlinks, does it do anything else? + # VERSION determines the version in the filename of the shared library. + # SOVERSION determines the value of the DT_SONAME field on ELF platforms. + # On ELF platforms the final compiled filename will be libz3.so.W.X.Y.Z + # but symlinks will be made to this file from libz3.so and also from libz3.so.W VERSION ${Z3_VERSION} - # SOVERSION: On platforms that use ELF this sets the API version - # and should be incremented everytime the API changes - SOVERSION ${Z3_VERSION}) + SOVERSION ${Z3_VERSION_MAJOR}) if (NOT MSVC) # On UNIX like platforms if we don't change the OUTPUT_NAME From 657b0de2fcb1c25009139e296532c6b8a5dc52d8 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Sun, 11 Dec 2016 08:27:35 -0800 Subject: [PATCH 03/23] cmake build: set SOVERSION to include the minor version number --- contrib/cmake/src/CMakeLists.txt | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 6693b4f5b..65eef8094 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -121,9 +121,12 @@ set_target_properties(libz3 PROPERTIES # VERSION determines the version in the filename of the shared library. # SOVERSION determines the value of the DT_SONAME field on ELF platforms. # On ELF platforms the final compiled filename will be libz3.so.W.X.Y.Z - # but symlinks will be made to this file from libz3.so and also from libz3.so.W + # but symlinks will be made to this file from libz3.so and also from + # libz3.so.W.X. + # This indicates that no breaking API changes will be made within a single + # minor version. VERSION ${Z3_VERSION} - SOVERSION ${Z3_VERSION_MAJOR}) + SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}) if (NOT MSVC) # On UNIX like platforms if we don't change the OUTPUT_NAME From 5796e150886e7479c5e35261cd4cda12b0593af9 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Fri, 27 Jan 2017 11:06:14 -0800 Subject: [PATCH 04/23] Thread labels through tactic system --- src/cmd_context/tactic_cmds.cpp | 21 ++++++++++++-- src/smt/tactic/smt_tactic.cpp | 8 ++++-- src/solver/tactic2solver.cpp | 3 +- src/tactic/filter_model_converter.cpp | 3 ++ src/tactic/filter_model_converter.h | 2 ++ src/tactic/model_converter.cpp | 40 ++++++++++++++++++++++++++- src/tactic/model_converter.h | 4 +++ src/tactic/tactic.cpp | 8 ++++-- src/tactic/tactic.h | 2 +- 9 files changed, 82 insertions(+), 9 deletions(-) diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 86900e175..158f361dd 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -165,7 +165,23 @@ public: } }; -typedef simple_check_sat_result check_sat_tactic_result; +struct check_sat_tactic_result : public simple_check_sat_result { +public: + svector labels; + + check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) { + } + + virtual void get_labels(svector & r) { + r.append(labels); + } + + virtual void add_labels(svector & r) { + labels.append(r); + } +}; + +typedef svector & labels_ref; class check_sat_using_tactict_cmd : public exec_given_tactic_cmd { public: @@ -189,6 +205,7 @@ public: ast_manager & m = ctx.m(); unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); + svector labels; goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); TRACE("check_sat_using", g->display(tout);); @@ -208,7 +225,7 @@ public: cmd_context::scoped_watch sw(ctx); lbool r = l_undef; try { - r = check_sat(t, g, md, pr, core, reason_unknown); + r = check_sat(t, g, md, result->labels, pr, core, reason_unknown); ctx.display_sat_result(r); result->set_status(r); if (r == l_undef) { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index f2fbcf6d9..d9e6da303 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -256,7 +256,9 @@ public: if (in->models_enabled()) { model_ref md; m_ctx->get_model(md); - mc = model2model_converter(md.get()); + buffer r; + m_ctx->get_relevant_labels(0, r); + mc = model_and_labels2model_converter(md.get(), r); mc = concat(fmc.get(), mc.get()); } pc = 0; @@ -308,7 +310,9 @@ public: if (in->models_enabled()) { model_ref md; m_ctx->get_model(md); - mc = model2model_converter(md.get()); + buffer r; + m_ctx->get_relevant_labels(0, r); + mc = model_and_labels2model_converter(md.get(), r); } pc = 0; core = 0; diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index f53301948..586d59d4f 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -144,8 +144,9 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass proof_ref pr(m); expr_dependency_ref core(m); std::string reason_unknown = "unknown"; + svector labels; try { - switch (::check_sat(*m_tactic, g, md, pr, core, reason_unknown)) { + switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) { case l_true: m_result->set_status(l_true); break; diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp index ba6ee4f0d..247f2e91d 100644 --- a/src/tactic/filter_model_converter.cpp +++ b/src/tactic/filter_model_converter.cpp @@ -51,6 +51,9 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx TRACE("filter_mc", tout << "after filter_model_converter\n"; model_v2_pp(tout, *old_model);); } +void filter_model_converter::operator()(svector & labels, unsigned goal_idx) { +} + void filter_model_converter::display(std::ostream & out) { out << "(filter-model-converter"; for (unsigned i = 0; i < m_decls.size(); i++) { diff --git a/src/tactic/filter_model_converter.h b/src/tactic/filter_model_converter.h index 6fc8fdd77..0b67a6c5a 100644 --- a/src/tactic/filter_model_converter.h +++ b/src/tactic/filter_model_converter.h @@ -32,6 +32,8 @@ public: virtual void operator()(model_ref & md, unsigned goal_idx); + virtual void operator()(svector & labels, unsigned goal_idx); + virtual void operator()(model_ref & md) { operator()(md, 0); } // TODO: delete virtual void cancel() {} diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 7ac3e898a..061d12afa 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -33,6 +33,12 @@ public: this->m_c1->operator()(m, 0); } + virtual void operator()(svector & r, unsigned goal_idx) { + this->m_c2->operator()(r, goal_idx); + this->m_c1->operator()(r, 0); + } + + virtual char const * get_name() const { return "concat-model-converter"; } virtual model_converter * translate(ast_translation & translator) { @@ -76,6 +82,24 @@ public: } UNREACHABLE(); } + + virtual void operator()(svector & r, unsigned goal_idx) { + unsigned num = this->m_c2s.size(); + for (unsigned i = 0; i < num; i++) { + if (goal_idx < this->m_szs[i]) { + // found the model converter that should be used + model_converter * c2 = this->m_c2s[i]; + if (c2) + c2->operator()(r, goal_idx); + if (m_c1) + this->m_c1->operator()(r, i); + return; + } + // invalid goal + goal_idx -= this->m_szs[i]; + } + UNREACHABLE(); + } virtual char const * get_name() const { return "concat-star-model-converter"; } @@ -102,8 +126,12 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter * class model2mc : public model_converter { model_ref m_model; + buffer m_labels; public: model2mc(model * m):m_model(m) {} + + model2mc(model * m, buffer r):m_model(m), m_labels(r) {} + virtual ~model2mc() {} virtual void operator()(model_ref & m) { @@ -114,7 +142,11 @@ public: m = m_model; } - virtual void cancel() { + virtual void operator()(svector & r, unsigned goal_idx) { + r.append(m_labels.size(), m_labels.c_ptr()); + } + + virtual void cancel() { } virtual void display(std::ostream & out) { @@ -135,6 +167,12 @@ model_converter * model2model_converter(model * m) { return alloc(model2mc, m); } +model_converter * model_and_labels2model_converter(model * m, buffer & r) { + if (m == 0) + return 0; + return alloc(model2mc, m, r); +} + void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) { if (mc) { m = alloc(model, mng); diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index 00c50a15f..4395fc546 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -32,6 +32,8 @@ public: SASSERT(goal_idx == 0); operator()(m); } + + virtual void operator()(svector & r, unsigned goal_idx) {} virtual model_converter * translate(ast_translation & translator) = 0; }; @@ -49,6 +51,8 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter * model_converter * model2model_converter(model * m); +model_converter * model_and_labels2model_converter(model * m, buffer &r); + void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m); void apply(model_converter_ref & mc, model_ref & m, unsigned gidx); diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 92e916d80..6eec018c7 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -174,7 +174,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve } } -lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { bool models_enabled = g->models_enabled(); bool proofs_enabled = g->proofs_enabled(); bool cores_enabled = g->unsat_core_enabled(); @@ -199,6 +199,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d if (is_decided_sat(r)) { if (models_enabled) { + (*mc)(labels, 0); model_converter2model(m, mc.get(), md); if (!md) { // create empty model. @@ -215,7 +216,10 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d return l_false; } else { - if (models_enabled) model_converter2model(m, mc.get(), md); + if (models_enabled) { + model_converter2model(m, mc.get(), md); + (*mc)(labels, 0); + } reason_unknown = "incomplete"; return l_undef; } diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index a9e50ff10..7c65c83e5 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -153,7 +153,7 @@ public: #define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;) void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); -lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); // Throws an exception if goal \c in requires proof generation. void fail_if_proof_generation(char const * tactic_name, goal_ref const & in); From a9d61d48ae5c21ee6bfafbd6baa244f8cbb53a1d Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Fri, 21 Oct 2016 12:08:46 -0700 Subject: [PATCH 05/23] Add basic Sine Qua Non filtering --- contrib/cmake/src/tactic/CMakeLists.txt | 1 + src/tactic/sine_filter.cpp | 252 ++++++++++++++++++++++++ src/tactic/sine_filter.h | 28 +++ 3 files changed, 281 insertions(+) create mode 100644 src/tactic/sine_filter.cpp create mode 100644 src/tactic/sine_filter.h diff --git a/contrib/cmake/src/tactic/CMakeLists.txt b/contrib/cmake/src/tactic/CMakeLists.txt index 318803cd2..324d8089b 100644 --- a/contrib/cmake/src/tactic/CMakeLists.txt +++ b/contrib/cmake/src/tactic/CMakeLists.txt @@ -12,6 +12,7 @@ z3_add_component(tactic probe.cpp proof_converter.cpp replace_proof_converter.cpp + sine_filter.cpp tactical.cpp tactic.cpp COMPONENT_DEPENDENCIES diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp new file mode 100644 index 000000000..15f0fca7a --- /dev/null +++ b/src/tactic/sine_filter.cpp @@ -0,0 +1,252 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + sine_filter.cpp + +Abstract: + + Tactic that performs Sine Qua Non premise selection + +Revision History: +--*/ + +#include "sine_filter.h" +#include "tactical.h" +#include "filter_model_converter.h" +#include "datatype_decl_plugin.h" +#include "rewriter_def.h" +#include "filter_model_converter.h" +#include "extension_model_converter.h" +#include "var_subst.h" +#include "ast_util.h" +#include "obj_pair_hashtable.h" + +#if 0 +TODO documentation here +#endif + + +class sine_tactic : public tactic { + + ast_manager& m; + params_ref m_params; + datatype_util m_dt; + ref m_ext; + ref m_filter; + unsigned m_num_transformed; + +public: + + sine_tactic(ast_manager& m, params_ref const& p): + m(m), m_params(p), m_dt(m) {} + + virtual tactic * translate(ast_manager & m) { + return alloc(sine_tactic, m, m_params); + } + + virtual void updt_params(params_ref const & 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; pc = 0; core = 0; + + TRACE("sine", g->display(tout);); + TRACE("sine", tout << g->size();); + ptr_vector new_forms; + filter_expressions(g, new_forms); + TRACE("sine", tout << new_forms.size();); + g->reset(); + for (unsigned i = 0; i < new_forms.size(); i++) { + g->assert_expr(new_forms.get(i), 0, 0); + } + g->inc_depth(); + g->updt_prec(goal::OVER); + result.push_back(g.get()); + TRACE("sine", result[0]->display(tout);); + SASSERT(g->is_well_sorted()); + filter_model_converter * fmc = alloc(filter_model_converter, m); + mc = fmc; + } + + virtual void cleanup() { + } + +private: + + // is this a user-defined symbol name? + bool is_name(func_decl * f) { + return f->get_family_id() < 0; + } + + typedef std::pair t_work_item; + + t_work_item work_item(expr *e, expr *root) { + return std::pair(e, root); + } + + void find_constants(expr *e, obj_hashtable &consts) { + ptr_vector stack; + stack.push_back(e); + expr *curr; + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr)) { + app *a = to_app(curr); + func_decl *f = a->get_decl(); + if (is_name(f) && !consts.contains(f)) { + consts.insert(f); + } + } + } + } + + bool quantifier_matches(quantifier *q, + obj_hashtable const & consts, + ptr_vector & next_consts) { + TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";); + for (obj_hashtable::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) { + TRACE("sine", tout << *constit; tout << "\n";); + } + bool matched = false; + for (int i = 0; i < q->get_num_patterns(); i++) { + bool p_matched = true; + vector stack; + expr *curr; + // patterns are wrapped with "pattern" + stack.push_back(to_app(q->get_pattern(i))->get_arg(0)); + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr)) { + app *a = to_app(curr); + func_decl *f = a->get_decl(); + if (!consts.contains(f)) { + TRACE("sine", tout << f; tout << "\n";); + p_matched = false; + next_consts.push_back(f); + break; + } + for (int j = 0; j < a->get_num_args(); j++) { + stack.push_back(a->get_arg(j)); + } + } + } + if (p_matched) { + matched = true; + break; + } + } + return matched; + } + + void filter_expressions(goal_ref const & g, ptr_vector & new_exprs) { + obj_map > const2exp; + obj_map > exp2const; + obj_map > const2quantifier; + obj_hashtable consts; + vector stack; + for (int i = 0; i < g->size(); i++) { + stack.push_back(work_item(g->form(i), g->form(i))); + } + t_work_item curr; + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr.first)) { + app *a = to_app(curr.first); + func_decl *f = a->get_decl(); + if (is_name(f)) { + if (!consts.contains(f)) { + consts.insert(f); + if (const2quantifier.contains(f)) { + for (obj_pair_hashtable::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) { + stack.push_back(*it); + } + const2quantifier.remove(f); + } + } + if (!const2exp.contains(f)) { + const2exp.insert(f, obj_hashtable()); + } + if (!const2exp[f].contains(curr.second)) { + const2exp[f].insert(curr.second); + } + if (!exp2const.contains(curr.second)) { + exp2const.insert(curr.second, obj_hashtable()); + } + if (!exp2const[curr.second].contains(f)) { + exp2const[curr.second].insert(f); + } + } + for (int i = 0; i < a->get_num_args(); i++) { + stack.push_back(work_item(a->get_arg(i), curr.second)); + } + } + else if (is_quantifier(curr.first)) { + quantifier *q = to_quantifier(curr.first); + if (q->is_forall()) { + if (q->has_patterns()) { + ptr_vector next_consts; + if (quantifier_matches(q, consts, next_consts)) { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + else { + for (unsigned i = 0; i < next_consts.size(); i++) { + func_decl *c = next_consts.get(i); + if (!const2quantifier.contains(c)) { + const2quantifier.insert(c, obj_pair_hashtable()); + } + if (!const2quantifier[c].contains(curr)) { + const2quantifier[c].insert(curr); + } + } + } + } + else { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + } + else if (q->is_exists()) { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + } + } + // ok, now we just need to find the connected component of the last term + + obj_hashtable visited; + ptr_vector to_visit; + to_visit.push_back(g->form(g->size() - 1)); + expr *visiting; + while (!to_visit.empty()) { + visiting = to_visit.back(); + to_visit.pop_back(); + visited.insert(visiting); + for (obj_hashtable::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) { + for (obj_hashtable::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) { + if (!visited.contains(*exprit)) { + to_visit.push_back(*exprit); + } + } + } + } + for (int i = 0; i < g->size(); i++) { + if (visited.contains(g->form(i))) { + new_exprs.push_back(g->form(i)); + } + } + } +}; + +tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) { + return alloc(sine_tactic, m, p); +} diff --git a/src/tactic/sine_filter.h b/src/tactic/sine_filter.h new file mode 100644 index 000000000..9b9e279a4 --- /dev/null +++ b/src/tactic/sine_filter.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + sine_filter.h + +Abstract: + + Tactic that performs Sine Qua Non premise selection + +Revision History: + +--*/ +#ifndef SINE_TACTIC_H_ +#define SINE_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_sine_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("sine-filter", "eliminate premises using Sine Qua Non", "mk_sine_tactic(m, p)") +*/ + +#endif From 379181092032b105c35d2b0576233633d212e97e Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 15:09:57 -0800 Subject: [PATCH 06/23] add const & --- src/tactic/model_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 061d12afa..efe80f226 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -130,7 +130,7 @@ class model2mc : public model_converter { public: model2mc(model * m):m_model(m) {} - model2mc(model * m, buffer r):m_model(m), m_labels(r) {} + model2mc(model * m, buffer const & r):m_model(m), m_labels(r) {} virtual ~model2mc() {} From 8196173e293032fb298ebd9b8e25907725a7201e Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 15:50:34 -0800 Subject: [PATCH 07/23] Introduce and use labels_vec --- src/cmd_context/tactic_cmds.cpp | 6 ++---- src/solver/tactic2solver.cpp | 2 +- src/tactic/model_converter.cpp | 6 +++--- src/tactic/model_converter.h | 4 +++- src/tactic/tactic.cpp | 2 +- src/tactic/tactic.h | 2 +- 6 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 158f361dd..4febb1597 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -167,7 +167,7 @@ public: struct check_sat_tactic_result : public simple_check_sat_result { public: - svector labels; + labels_vec labels; check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) { } @@ -181,8 +181,6 @@ public: } }; -typedef svector & labels_ref; - class check_sat_using_tactict_cmd : public exec_given_tactic_cmd { public: check_sat_using_tactict_cmd(): @@ -205,7 +203,7 @@ public: ast_manager & m = ctx.m(); unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); - svector labels; + labels_vec labels; goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); TRACE("check_sat_using", g->display(tout);); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 586d59d4f..6b1a7916f 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -144,7 +144,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass proof_ref pr(m); expr_dependency_ref core(m); std::string reason_unknown = "unknown"; - svector labels; + labels_vec labels; try { switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) { case l_true: diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index efe80f226..6f6dd3da1 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -33,7 +33,7 @@ public: this->m_c1->operator()(m, 0); } - virtual void operator()(svector & r, unsigned goal_idx) { + virtual void operator()(labels_vec & r, unsigned goal_idx) { this->m_c2->operator()(r, goal_idx); this->m_c1->operator()(r, 0); } @@ -83,7 +83,7 @@ public: UNREACHABLE(); } - virtual void operator()(svector & r, unsigned goal_idx) { + virtual void operator()(labels_vec & r, unsigned goal_idx) { unsigned num = this->m_c2s.size(); for (unsigned i = 0; i < num; i++) { if (goal_idx < this->m_szs[i]) { @@ -142,7 +142,7 @@ public: m = m_model; } - virtual void operator()(svector & r, unsigned goal_idx) { + virtual void operator()(labels_vec & r, unsigned goal_idx) { r.append(m_labels.size(), m_labels.c_ptr()); } diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index 4395fc546..e2bc3cf83 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -23,6 +23,8 @@ Notes: #include"converter.h" #include"ref.h" +class labels_vec : public svector {}; + class model_converter : public converter { public: virtual void operator()(model_ref & m) {} // TODO: delete @@ -33,7 +35,7 @@ public: operator()(m); } - virtual void operator()(svector & r, unsigned goal_idx) {} + virtual void operator()(labels_vec & r, unsigned goal_idx) {} virtual model_converter * translate(ast_translation & translator) = 0; }; diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 6eec018c7..0a95e8f65 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -174,7 +174,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve } } -lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { bool models_enabled = g->models_enabled(); bool proofs_enabled = g->proofs_enabled(); bool cores_enabled = g->unsat_core_enabled(); diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 7c65c83e5..645b53681 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -153,7 +153,7 @@ public: #define MK_SIMPLE_TACTIC_FACTORY(NAME, ST) MK_TACTIC_FACTORY(NAME, return ST;) void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core); -lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); +lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown); // Throws an exception if goal \c in requires proof generation. void fail_if_proof_generation(char const * tactic_name, goal_ref const & in); From b00c4d2e64ad0aaa15f8a7dc5252ead76eac7a08 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 20:54:24 -0800 Subject: [PATCH 08/23] add name --- src/tactic/sine_filter.cpp | 4 ++++ src/tactic/sine_filter.h | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 15f0fca7a..2052035f7 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -9,6 +9,10 @@ Abstract: Tactic that performs Sine Qua Non premise selection +Author: + + Doug Woos + Revision History: --*/ diff --git a/src/tactic/sine_filter.h b/src/tactic/sine_filter.h index 9b9e279a4..769ef474f 100644 --- a/src/tactic/sine_filter.h +++ b/src/tactic/sine_filter.h @@ -9,6 +9,10 @@ Abstract: Tactic that performs Sine Qua Non premise selection +Author: + + Doug Woos + Revision History: --*/ From da63f6b0ffce1b11260bc505cbfa01efb66b1ecf Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 20:54:33 -0800 Subject: [PATCH 09/23] delete comment --- src/tactic/sine_filter.cpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 2052035f7..d76e8f6b5 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -27,11 +27,6 @@ Revision History: #include "ast_util.h" #include "obj_pair_hashtable.h" -#if 0 -TODO documentation here -#endif - - class sine_tactic : public tactic { ast_manager& m; From c0bb6dd2be9cabb4cc774babb6bae9a530298161 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 20:54:40 -0800 Subject: [PATCH 10/23] delete unused args --- src/tactic/sine_filter.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index d76e8f6b5..60482d86e 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -31,15 +31,11 @@ class sine_tactic : public tactic { ast_manager& m; params_ref m_params; - datatype_util m_dt; - ref m_ext; - ref m_filter; - unsigned m_num_transformed; public: sine_tactic(ast_manager& m, params_ref const& p): - m(m), m_params(p), m_dt(m) {} + m(m), m_params(p) {} virtual tactic * translate(ast_manager & m) { return alloc(sine_tactic, m, m_params); From 89ba99918eed693a97b4378b448726e1758e2e90 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Mon, 30 Jan 2017 21:02:09 -0800 Subject: [PATCH 11/23] reindent --- src/tactic/sine_filter.cpp | 302 ++++++++++++++++++------------------- 1 file changed, 151 insertions(+), 151 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 60482d86e..f5ecc36a3 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -3,15 +3,15 @@ Copyright (c) 2016 Microsoft Corporation Module Name: - sine_filter.cpp + sine_filter.cpp Abstract: - Tactic that performs Sine Qua Non premise selection + Tactic that performs Sine Qua Non premise selection Author: - Doug Woos + Doug Woos Revision History: --*/ @@ -35,7 +35,7 @@ class sine_tactic : public tactic { public: sine_tactic(ast_manager& m, params_ref const& p): - m(m), m_params(p) {} + m(m), m_params(p) {} virtual tactic * translate(ast_manager & m) { return alloc(sine_tactic, m, m_params); @@ -61,7 +61,7 @@ public: TRACE("sine", tout << new_forms.size();); g->reset(); for (unsigned i = 0; i < new_forms.size(); i++) { - g->assert_expr(new_forms.get(i), 0, 0); + g->assert_expr(new_forms.get(i), 0, 0); } g->inc_depth(); g->updt_prec(goal::OVER); @@ -77,169 +77,169 @@ public: private: - // is this a user-defined symbol name? - bool is_name(func_decl * f) { - return f->get_family_id() < 0; - } + // is this a user-defined symbol name? + bool is_name(func_decl * f) { + return f->get_family_id() < 0; + } - typedef std::pair t_work_item; + typedef std::pair t_work_item; - t_work_item work_item(expr *e, expr *root) { - return std::pair(e, root); - } + t_work_item work_item(expr *e, expr *root) { + return std::pair(e, root); + } - void find_constants(expr *e, obj_hashtable &consts) { - ptr_vector stack; - stack.push_back(e); - expr *curr; - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - if (is_app(curr)) { - app *a = to_app(curr); - func_decl *f = a->get_decl(); - if (is_name(f) && !consts.contains(f)) { - consts.insert(f); + void find_constants(expr *e, obj_hashtable &consts) { + ptr_vector stack; + stack.push_back(e); + expr *curr; + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr)) { + app *a = to_app(curr); + func_decl *f = a->get_decl(); + if (is_name(f) && !consts.contains(f)) { + consts.insert(f); + } + } } - } } - } - bool quantifier_matches(quantifier *q, - obj_hashtable const & consts, - ptr_vector & next_consts) { - TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";); - for (obj_hashtable::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) { - TRACE("sine", tout << *constit; tout << "\n";); - } - bool matched = false; - for (int i = 0; i < q->get_num_patterns(); i++) { - bool p_matched = true; - vector stack; - expr *curr; - // patterns are wrapped with "pattern" - stack.push_back(to_app(q->get_pattern(i))->get_arg(0)); - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - if (is_app(curr)) { - app *a = to_app(curr); - func_decl *f = a->get_decl(); - if (!consts.contains(f)) { - TRACE("sine", tout << f; tout << "\n";); - p_matched = false; - next_consts.push_back(f); - break; - } - for (int j = 0; j < a->get_num_args(); j++) { - stack.push_back(a->get_arg(j)); - } + bool quantifier_matches(quantifier *q, + obj_hashtable const & consts, + ptr_vector & next_consts) { + TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";); + for (obj_hashtable::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) { + TRACE("sine", tout << *constit; tout << "\n";); } - } - if (p_matched) { - matched = true; - break; - } + bool matched = false; + for (int i = 0; i < q->get_num_patterns(); i++) { + bool p_matched = true; + vector stack; + expr *curr; + // patterns are wrapped with "pattern" + stack.push_back(to_app(q->get_pattern(i))->get_arg(0)); + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr)) { + app *a = to_app(curr); + func_decl *f = a->get_decl(); + if (!consts.contains(f)) { + TRACE("sine", tout << f; tout << "\n";); + p_matched = false; + next_consts.push_back(f); + break; + } + for (int j = 0; j < a->get_num_args(); j++) { + stack.push_back(a->get_arg(j)); + } + } + } + if (p_matched) { + matched = true; + break; + } + } + return matched; } - return matched; - } - void filter_expressions(goal_ref const & g, ptr_vector & new_exprs) { - obj_map > const2exp; - obj_map > exp2const; - obj_map > const2quantifier; - obj_hashtable consts; - vector stack; - for (int i = 0; i < g->size(); i++) { - stack.push_back(work_item(g->form(i), g->form(i))); - } - t_work_item curr; - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - if (is_app(curr.first)) { - app *a = to_app(curr.first); - func_decl *f = a->get_decl(); - if (is_name(f)) { - if (!consts.contains(f)) { - consts.insert(f); - if (const2quantifier.contains(f)) { - for (obj_pair_hashtable::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) { - stack.push_back(*it); - } - const2quantifier.remove(f); - } - } - if (!const2exp.contains(f)) { - const2exp.insert(f, obj_hashtable()); - } - if (!const2exp[f].contains(curr.second)) { - const2exp[f].insert(curr.second); - } - if (!exp2const.contains(curr.second)) { - exp2const.insert(curr.second, obj_hashtable()); - } - if (!exp2const[curr.second].contains(f)) { - exp2const[curr.second].insert(f); - } + void filter_expressions(goal_ref const & g, ptr_vector & new_exprs) { + obj_map > const2exp; + obj_map > exp2const; + obj_map > const2quantifier; + obj_hashtable consts; + vector stack; + for (int i = 0; i < g->size(); i++) { + stack.push_back(work_item(g->form(i), g->form(i))); } - for (int i = 0; i < a->get_num_args(); i++) { - stack.push_back(work_item(a->get_arg(i), curr.second)); - } - } - else if (is_quantifier(curr.first)) { - quantifier *q = to_quantifier(curr.first); - if (q->is_forall()) { - if (q->has_patterns()) { - ptr_vector next_consts; - if (quantifier_matches(q, consts, next_consts)) { - stack.push_back(work_item(q->get_expr(), curr.second)); - } - else { - for (unsigned i = 0; i < next_consts.size(); i++) { - func_decl *c = next_consts.get(i); - if (!const2quantifier.contains(c)) { - const2quantifier.insert(c, obj_pair_hashtable()); + t_work_item curr; + while (!stack.empty()) { + curr = stack.back(); + stack.pop_back(); + if (is_app(curr.first)) { + app *a = to_app(curr.first); + func_decl *f = a->get_decl(); + if (is_name(f)) { + if (!consts.contains(f)) { + consts.insert(f); + if (const2quantifier.contains(f)) { + for (obj_pair_hashtable::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) { + stack.push_back(*it); + } + const2quantifier.remove(f); + } + } + if (!const2exp.contains(f)) { + const2exp.insert(f, obj_hashtable()); + } + if (!const2exp[f].contains(curr.second)) { + const2exp[f].insert(curr.second); + } + if (!exp2const.contains(curr.second)) { + exp2const.insert(curr.second, obj_hashtable()); + } + if (!exp2const[curr.second].contains(f)) { + exp2const[curr.second].insert(f); + } } - if (!const2quantifier[c].contains(curr)) { - const2quantifier[c].insert(curr); + for (int i = 0; i < a->get_num_args(); i++) { + stack.push_back(work_item(a->get_arg(i), curr.second)); + } + } + else if (is_quantifier(curr.first)) { + quantifier *q = to_quantifier(curr.first); + if (q->is_forall()) { + if (q->has_patterns()) { + ptr_vector next_consts; + if (quantifier_matches(q, consts, next_consts)) { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + else { + for (unsigned i = 0; i < next_consts.size(); i++) { + func_decl *c = next_consts.get(i); + if (!const2quantifier.contains(c)) { + const2quantifier.insert(c, obj_pair_hashtable()); + } + if (!const2quantifier[c].contains(curr)) { + const2quantifier[c].insert(curr); + } + } + } + } + else { + stack.push_back(work_item(q->get_expr(), curr.second)); + } + } + else if (q->is_exists()) { + stack.push_back(work_item(q->get_expr(), curr.second)); } - } } - } - else { - stack.push_back(work_item(q->get_expr(), curr.second)); - } } - else if (q->is_exists()) { - stack.push_back(work_item(q->get_expr(), curr.second)); - } - } - } - // ok, now we just need to find the connected component of the last term + // ok, now we just need to find the connected component of the last term - obj_hashtable visited; - ptr_vector to_visit; - to_visit.push_back(g->form(g->size() - 1)); - expr *visiting; - while (!to_visit.empty()) { - visiting = to_visit.back(); - to_visit.pop_back(); - visited.insert(visiting); - for (obj_hashtable::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) { - for (obj_hashtable::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) { - if (!visited.contains(*exprit)) { - to_visit.push_back(*exprit); - } + obj_hashtable visited; + ptr_vector to_visit; + to_visit.push_back(g->form(g->size() - 1)); + expr *visiting; + while (!to_visit.empty()) { + visiting = to_visit.back(); + to_visit.pop_back(); + visited.insert(visiting); + for (obj_hashtable::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) { + for (obj_hashtable::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) { + if (!visited.contains(*exprit)) { + to_visit.push_back(*exprit); + } + } + } + } + for (int i = 0; i < g->size(); i++) { + if (visited.contains(g->form(i))) { + new_exprs.push_back(g->form(i)); + } } - } } - for (int i = 0; i < g->size(); i++) { - if (visited.contains(g->form(i))) { - new_exprs.push_back(g->form(i)); - } - } - } }; tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) { From d9e43f0e6d592d6b385b673a3c1dc8e12ca753c4 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Tue, 31 Jan 2017 11:47:44 -0800 Subject: [PATCH 12/23] use insert_if_not_there --- src/tactic/sine_filter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index f5ecc36a3..71ae58f8c 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -98,8 +98,8 @@ private: if (is_app(curr)) { app *a = to_app(curr); func_decl *f = a->get_decl(); - if (is_name(f) && !consts.contains(f)) { - consts.insert(f); + if (is_name(f)) { + consts.insert_if_not_there(f); } } } From a147e2bc3530da587c4128eeae020cd33e3bbdaf Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Wed, 1 Feb 2017 16:20:40 -0800 Subject: [PATCH 13/23] use is_uninterp --- src/tactic/sine_filter.cpp | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 71ae58f8c..43c15bf74 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -77,11 +77,6 @@ public: private: - // is this a user-defined symbol name? - bool is_name(func_decl * f) { - return f->get_family_id() < 0; - } - typedef std::pair t_work_item; t_work_item work_item(expr *e, expr *root) { @@ -97,8 +92,8 @@ private: stack.pop_back(); if (is_app(curr)) { app *a = to_app(curr); - func_decl *f = a->get_decl(); - if (is_name(f)) { + if (is_uninterp(a)) { + func_decl *f = a->get_decl(); consts.insert_if_not_there(f); } } @@ -159,8 +154,8 @@ private: stack.pop_back(); if (is_app(curr.first)) { app *a = to_app(curr.first); - func_decl *f = a->get_decl(); - if (is_name(f)) { + if (is_uninterp(a)) { + func_decl *f = a->get_decl(); if (!consts.contains(f)) { consts.insert(f); if (const2quantifier.contains(f)) { From 44c417904b268c6bbb175082c81f58c0ada1a422 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Wed, 1 Feb 2017 16:21:01 -0800 Subject: [PATCH 14/23] correctly pretty-print --- src/tactic/sine_filter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 43c15bf74..059608b4c 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -26,6 +26,7 @@ Revision History: #include "var_subst.h" #include "ast_util.h" #include "obj_pair_hashtable.h" +#include "ast_pp.h" class sine_tactic : public tactic { @@ -121,7 +122,7 @@ private: app *a = to_app(curr); func_decl *f = a->get_decl(); if (!consts.contains(f)) { - TRACE("sine", tout << f; tout << "\n";); + TRACE("sine", tout << mk_pp(f, m) << "\n";); p_matched = false; next_consts.push_back(f); break; From d6fbfe401e282f3a86abbe21a5363256996e3ea6 Mon Sep 17 00:00:00 2001 From: Doug Woos Date: Wed, 1 Feb 2017 16:21:15 -0800 Subject: [PATCH 15/23] add and use new is_pattern recognizer --- src/ast/ast.cpp | 16 ++++++++++++++++ src/ast/ast.h | 2 ++ src/tactic/sine_filter.cpp | 6 ++++-- 3 files changed, 22 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 440179ba8..7be7300a2 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2326,6 +2326,22 @@ bool ast_manager::is_pattern(expr const * n) const { return true; } + +bool ast_manager::is_pattern(expr const * n, ptr_vector &args) { + if (!is_app_of(n, m_pattern_family_id, OP_PATTERN)) { + return false; + } + for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) { + expr *arg = to_app(n)->get_arg(i); + if (!is_app(arg)) { + return false; + } + args.push_back(arg); + } + return true; +} + + quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, int weight , symbol const & qid, symbol const & skid, unsigned num_patterns, expr * const * patterns, diff --git a/src/ast/ast.h b/src/ast/ast.h index 47ea0f812..9259d5431 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1840,6 +1840,8 @@ public: bool is_pattern(expr const * n) const; + bool is_pattern(expr const *n, ptr_vector &args); + public: quantifier * mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index 059608b4c..e180eea5e 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -111,10 +111,12 @@ private: bool matched = false; for (int i = 0; i < q->get_num_patterns(); i++) { bool p_matched = true; - vector stack; + ptr_vector stack; expr *curr; // patterns are wrapped with "pattern" - stack.push_back(to_app(q->get_pattern(i))->get_arg(0)); + if (!m.is_pattern(q->get_pattern(i), stack)) { + continue; + } while (!stack.empty()) { curr = stack.back(); stack.pop_back(); From d6b4e9948959513431bca4d8cd18f06c26bed4f9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 5 Feb 2017 16:03:00 +0000 Subject: [PATCH 16/23] Fixed signed/unsigned warnings --- src/tactic/sine_filter.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index e180eea5e..f2d6a9653 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -109,7 +109,7 @@ private: TRACE("sine", tout << *constit; tout << "\n";); } bool matched = false; - for (int i = 0; i < q->get_num_patterns(); i++) { + for (unsigned i = 0; i < q->get_num_patterns(); i++) { bool p_matched = true; ptr_vector stack; expr *curr; @@ -129,7 +129,7 @@ private: next_consts.push_back(f); break; } - for (int j = 0; j < a->get_num_args(); j++) { + for (unsigned j = 0; j < a->get_num_args(); j++) { stack.push_back(a->get_arg(j)); } } @@ -148,7 +148,7 @@ private: obj_map > const2quantifier; obj_hashtable consts; vector stack; - for (int i = 0; i < g->size(); i++) { + for (unsigned i = 0; i < g->size(); i++) { stack.push_back(work_item(g->form(i), g->form(i))); } t_work_item curr; @@ -181,7 +181,7 @@ private: exp2const[curr.second].insert(f); } } - for (int i = 0; i < a->get_num_args(); i++) { + for (unsigned i = 0; i < a->get_num_args(); i++) { stack.push_back(work_item(a->get_arg(i), curr.second)); } } @@ -232,7 +232,7 @@ private: } } } - for (int i = 0; i < g->size(); i++) { + for (unsigned i = 0; i < g->size(); i++) { if (visited.contains(g->form(i))) { new_exprs.push_back(g->form(i)); } From 54280b6cc508d7c6ce9867a4ade36a2a2f6782a3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 5 Feb 2017 17:20:45 +0000 Subject: [PATCH 17/23] Fixed model-converter segfault in ::check_sat. Relates to #881 --- src/tactic/tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 9315f73b0..e6f342300 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -200,7 +200,8 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p if (is_decided_sat(r)) { if (models_enabled) { - (*mc)(labels, 0); + if (mc) + (*mc)(labels, 0); model_converter2model(m, mc.get(), md); if (!md) { // create empty model. From e4411265ea6c78c2aa00df9860d5b25ab47ac42d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 5 Feb 2017 17:53:44 +0000 Subject: [PATCH 18/23] Fixed model-converter segfault in ::check_sat. Relates to #881 --- src/tactic/tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index e6f342300..67fce1486 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -220,7 +220,8 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p else { if (models_enabled) { model_converter2model(m, mc.get(), md); - (*mc)(labels, 0); + if (mc) + (*mc)(labels, 0); } reason_unknown = "incomplete"; return l_undef; From 3a0e9e8f53de9058f1813b8c461a3cc1fcc3c06d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 11:31:13 -0500 Subject: [PATCH 19/23] add itos/stoi conversion to API. Issue #895 Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 47 +++++++++++++++++++++------------------ src/api/api_seq.cpp | 4 ++++ src/api/c++/z3++.h | 11 +++++++++ src/api/dotnet/Context.cs | 23 +++++++++++++++++++ src/api/python/z3/z3.py | 28 +++++++++++++++++++++-- src/api/z3_api.h | 19 ++++++++++++++++ 6 files changed, 108 insertions(+), 24 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index fd2776079..c9cdc6ab3 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1110,29 +1110,32 @@ extern "C" { if (mk_c(c)->get_seq_fid() == _d->get_family_id()) { switch (_d->get_decl_kind()) { - case Z3_OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT; - case Z3_OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY; - case Z3_OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT; - case Z3_OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX; - case Z3_OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX; - case Z3_OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS; - case Z3_OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT; - case Z3_OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE; - case Z3_OP_SEQ_AT: return Z3_OP_SEQ_AT; - case Z3_OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH; - case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX; - case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; - case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; + case OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT; + case OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY; + case OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT; + case OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX; + case OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX; + case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS; + case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT; + case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE; + case OP_SEQ_AT: return Z3_OP_SEQ_AT; + case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH; + case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX; + case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; + case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; - case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS; - case Z3_OP_RE_STAR: return Z3_OP_RE_STAR; - case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION; - case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT; - case Z3_OP_RE_UNION: return Z3_OP_RE_UNION; - case Z3_OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT; - case Z3_OP_RE_LOOP: return Z3_OP_RE_LOOP; - case Z3_OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET; - case Z3_OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET; + case OP_STRING_STOI: return Z3_OP_STR_TO_INT; + case OP_STRING_ITOS: return Z3_OP_INT_TO_STR; + + case OP_RE_PLUS: return Z3_OP_RE_PLUS; + case OP_RE_STAR: return Z3_OP_RE_STAR; + case OP_RE_OPTION: return Z3_OP_RE_OPTION; + case OP_RE_CONCAT: return Z3_OP_RE_CONCAT; + case OP_RE_UNION: return Z3_OP_RE_UNION; + case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT; + case OP_RE_LOOP: return Z3_OP_RE_LOOP; + case OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET; + case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET; default: return Z3_OP_INTERNAL; } diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 478ee6274..986e6f497 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -141,6 +141,10 @@ extern "C" { MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP); MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP); + MK_UNARY(Z3_mk_int_to_str, mk_c(c)->get_seq_fid(), OP_STRING_ITOS, SKIP); + MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, SKIP); + + Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) { Z3_TRY; LOG_Z3_mk_re_loop(c, r, lo, hi); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 979d9aed7..e5d0acaab 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -964,6 +964,17 @@ namespace z3 { check_error(); return expr(ctx(), r); } + expr stoi() const { + Z3_ast r = Z3_mk_str_to_int(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + expr itos() const { + Z3_ast r = Z3_mk_int_to_str(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + friend expr range(expr const& lo, expr const& hi); /** \brief create a looping regular expression. diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index f5c4dc99d..a656be3eb 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2420,6 +2420,29 @@ namespace Microsoft.Z3 return new SeqExpr(this, Native.Z3_mk_string(nCtx, s)); } + /// + /// Convert an integer expression to a string. + /// + public SeqExpr IntToString(Expr e) + { + Contract.Requires(e != null); + Contract.Requires(e is ArithExpr); + Contract.Ensures(Contract.Result() != null); + return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject)); + } + + /// + /// Convert an integer expression to a string. + /// + public IntExpr StringToInt(Expr e) + { + Contract.Requires(e != null); + Contract.Requires(e is SeqExpr); + Contract.Ensures(Contract.Result() != null); + return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject)); + } + + /// /// Concatentate sequences. /// diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 77b74336e..f1fde1720 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1011,6 +1011,7 @@ def _coerce_exprs(a, b, ctx=None): b = s.cast(b) return (a, b) + def _reduce(f, l, a): r = a for e in l: @@ -1296,7 +1297,7 @@ class BoolSortRef(SortRef): if isinstance(val, bool): return BoolVal(val, self.ctx) if __debug__: - _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected") + _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val) _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value") return val @@ -2012,7 +2013,7 @@ class ArithSortRef(SortRef): if self.is_real(): return RealVal(val, self.ctx) if __debug__: - _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected") + _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self) def is_arith_sort(s): """Return `True` if s is an arithmetical sort (type). @@ -9660,6 +9661,29 @@ def Length(s): s = _coerce_seq(s) return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) +def StrToInt(s): + """Convert string expression to integer + >>> a = StrToInt("1") + >>> simplify(1 == a) + True + >>> b = StrToInt("2") + >>> simplify(1 == b) + False + >>> c = StrToInt(IntToStr(2)) + >>> simplify(1 == c) + False + """ + s = _coerce_seq(s) + return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx) + + +def IntToStr(s): + """Convert integer expression to string""" + if not is_expr(s): + s = _py2expr(s) + return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx) + + def Re(s, ctx=None): """The regular expression that accepts sequence 's' >>> s1 = Re("ab") diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 65c155d63..ee35c002e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1152,6 +1152,10 @@ typedef enum { Z3_OP_SEQ_TO_RE, Z3_OP_SEQ_IN_RE, + // strings + Z3_OP_STR_TO_INT, + Z3_OP_INT_TO_STR, + // regular expressions Z3_OP_RE_PLUS, Z3_OP_RE_STAR, @@ -3325,6 +3329,21 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset); + /** + \brief Convert string to integer. + + def_API('Z3_mk_str_to_int' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s); + + + /** + \brief Integer to string conversion. + + def_API('Z3_mk_int_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s); + /** \brief Create a regular expression that accepts the sequence \c seq. From b42973152fea616fd634dfb4c8a231e898b079a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 12:02:32 -0500 Subject: [PATCH 20/23] fix model generation for non-linear expressions, reported by Martin Suda and Giles Reger Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 1 + src/smt/theory_arith_core.h | 6 +++++- src/smt/theory_arith_nl.h | 12 +++++++++--- 3 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 5a0f8db95..77882f186 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -946,6 +946,7 @@ namespace smt { // // ----------------------------------- typedef int_hashtable > row_set; + bool m_model_depends_on_computed_epsilon; unsigned m_nl_rounds; bool m_nl_gb_exhausted; unsigned m_nl_strategy_idx; // for fairness diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 9db5e8c72..513cf36a4 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1405,6 +1405,7 @@ namespace smt { template final_check_status theory_arith::final_check_core() { + m_model_depends_on_computed_epsilon = false; unsigned old_idx = m_final_check_idx; final_check_status result = FC_DONE; final_check_status ok; @@ -1669,6 +1670,7 @@ namespace smt { m_liberal_final_check(true), m_changed_assignment(false), m_assume_eq_head(0), + m_model_depends_on_computed_epsilon(false), m_nl_rounds(0), m_nl_gb_exhausted(false), m_nl_new_exprs(m), @@ -3220,7 +3222,9 @@ namespace smt { m_factory = alloc(arith_factory, get_manager()); m.register_factory(m_factory); compute_epsilon(); - refine_epsilon(); + if (!m_model_depends_on_computed_epsilon) { + refine_epsilon(); + } } template diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index dd91ffbfb..52a117cd5 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -638,6 +638,7 @@ namespace smt { if (!val.get_infinitesimal().is_zero() && !computed_epsilon) { compute_epsilon(); computed_epsilon = true; + m_model_depends_on_computed_epsilon = true; } return val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational(); } @@ -652,14 +653,18 @@ namespace smt { bool theory_arith::check_monomial_assignment(theory_var v, bool & computed_epsilon) { SASSERT(is_pure_monomial(var2expr(v))); expr * m = var2expr(v); - rational val(1); + rational val(1), v_val; for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { expr * arg = to_app(m)->get_arg(i); theory_var curr = expr2var(arg); SASSERT(curr != null_theory_var); - val *= get_value(curr, computed_epsilon); + v_val = get_value(curr, computed_epsilon); + TRACE("non_linear", tout << mk_pp(arg, get_manager()) << " = " << v_val << "\n";); + val *= v_val; } - return get_value(v, computed_epsilon) == val; + v_val = get_value(v, computed_epsilon); + TRACE("non_linear", tout << "v" << v << " := " << v_val << " == " << val << "\n";); + return v_val == val; } @@ -2356,6 +2361,7 @@ namespace smt { */ template final_check_status theory_arith::process_non_linear() { + m_model_depends_on_computed_epsilon = false; if (m_nl_monomials.empty()) return FC_DONE; From 4c6efbbc8bce874cedbf8ffb14a3b883df62e767 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 16:02:51 -0500 Subject: [PATCH 21/23] expose numerator/denominators for Martin and Giles Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e5d0acaab..e60809646 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -758,6 +758,20 @@ namespace z3 { return result; } + expr numerator() const { + assert(is_numeral()); + Z3_ast r = Z3_get_numerator(ctx(), m_ast); + check_error(); + return expr(ctx(),r); + } + + + expr denominator() const { + assert(is_numeral()); + Z3_ast r = Z3_get_denominator(ctx(), m_ast); + check_error(); + return expr(ctx(),r); + } operator Z3_app() const { assert(is_app()); return reinterpret_cast(m_ast); } From b3dabc7ccf9fde3997d8aaf1c3c61fd708a24803 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 16:28:15 -0500 Subject: [PATCH 22/23] add missing mod/rem/is_int functionality to C++ API Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 72 ++++++++++++++++++++++++++++++++-------------- 1 file changed, 50 insertions(+), 22 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e60809646..d8027fbbc 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -435,6 +435,8 @@ namespace z3 { Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; } unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; } friend std::ostream & operator<<(std::ostream & out, ast const & n); + std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); } + /** \brief Return true if the ASTs are structurally identical. @@ -757,7 +759,11 @@ namespace z3 { } return result; } - + + Z3_lbool bool_value() const { + return Z3_get_bool_value(ctx(), m_ast); + } + expr numerator() const { assert(is_numeral()); Z3_ast r = Z3_get_numerator(ctx(), m_ast); @@ -889,13 +895,23 @@ namespace z3 { friend expr operator*(expr const & a, int b); friend expr operator*(int a, expr const & b); - /** - \brief Power operator - */ + /* \brief Power operator */ friend expr pw(expr const & a, expr const & b); friend expr pw(expr const & a, int b); friend expr pw(int a, expr const & b); + /* \brief mod operator */ + friend expr mod(expr const& a, expr const& b); + friend expr mod(expr const& a, int b); + friend expr mod(int a, expr const& b); + + /* \brief rem operator */ + friend expr rem(expr const& a, expr const& b); + friend expr rem(expr const& a, int b); + friend expr rem(int a, expr const& b); + + friend expr is_int(expr const& e); + friend expr operator/(expr const & a, expr const & b); friend expr operator/(expr const & a, int b); friend expr operator/(int a, expr const & b); @@ -1026,34 +1042,46 @@ namespace z3 { }; +#define _Z3_MK_BIN_(a, b, binop) \ + check_context(a, b); \ + Z3_ast r = binop(a.ctx(), a, b); \ + a.check_error(); \ + return expr(a.ctx(), r); \ + + inline expr implies(expr const & a, expr const & b) { - check_context(a, b); - assert(a.is_bool() && b.is_bool()); - Z3_ast r = Z3_mk_implies(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); + assert(a.is_bool() && b.is_bool()); + _Z3_MK_BIN_(a, b, Z3_mk_implies); } inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); } inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); } - inline expr pw(expr const & a, expr const & b) { - assert(a.is_arith() && b.is_arith()); - check_context(a, b); - Z3_ast r = Z3_mk_power(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); - } + inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); } inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); } inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); } + inline expr mod(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_mod); } + inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); } + inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); } - inline expr operator!(expr const & a) { - assert(a.is_bool()); - Z3_ast r = Z3_mk_not(a.ctx(), a); - a.check_error(); - return expr(a.ctx(), r); - } + inline expr rem(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_rem); } + inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); } + inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); } + +#undef _Z3_MK_BIN_ + +#define _Z3_MK_UN_(a, mkun) \ + Z3_ast r = mkun(a.ctx(), a); \ + a.check_error(); \ + return expr(a.ctx(), r); \ + + + inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); } + + inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); } + +#undef _Z3_MK_UN_ inline expr operator&&(expr const & a, expr const & b) { check_context(a, b); From 6fcba26ea6c695628fa701aee0e8cf78141ba8d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Feb 2017 09:56:49 -0800 Subject: [PATCH 23/23] make parameters accessible from expressions. Issue #896 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f1fde1720..6729d99b5 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -868,6 +868,9 @@ class ExprRef(AstRef): _args, sz = _to_ast_array((a, b)) return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx) + def params(self): + return self.decl().params() + def decl(self): """Return the Z3 function declaration associated with a Z3 application.