From 2d7a38e95e2c29ed32b8e75954ea6eac6535e5de Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Dec 2022 16:07:41 -0800 Subject: [PATCH 1/6] fix #6488 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/elim_unconstrained.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index bb7a4fa49..2e950868a 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -65,7 +65,6 @@ void elim_unconstrained::eliminate() { expr_ref r(m), side_cond(m); int v = m_heap.erase_min(); node& n = get_node(v); - IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " @ " << n.m_refcount << "\n"); if (n.m_refcount == 0) continue; if (n.m_refcount > 1) @@ -203,10 +202,11 @@ void elim_unconstrained::freeze(expr* t) { return; node& n = get_node(t); if (!n.m_term) - return; - n.m_refcount = UINT_MAX / 2; - if (m_heap.contains(root(t))) + return; + if (m_heap.contains(root(t))) { + n.m_refcount = UINT_MAX / 2; m_heap.increased(root(t)); + } } void elim_unconstrained::gc(expr* t) { From cd3d38caf79ccc0ecbf18f28044451b135f69cb2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Dec 2022 16:17:38 -0800 Subject: [PATCH 2/6] sort out terminology/add explanations, add shortcut to C++, fix #6491 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 17 +++++++++++++++++ src/api/python/z3/z3.py | 4 +++- src/api/z3_api.h | 8 ++++++-- 3 files changed, 26 insertions(+), 3 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index caf7ce07e..838a34be6 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -366,8 +366,14 @@ namespace z3 { void recdef(func_decl, expr_vector const& args, expr const& body); func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range); + /** + \brief create an uninterpreted constant. + */ expr constant(symbol const & name, sort const & s); expr constant(char const * name, sort const & s); + /** + \brief create uninterpreted constants of a given sort. + */ expr bool_const(char const * name); expr int_const(char const * name); expr real_const(char const * name); @@ -378,6 +384,12 @@ namespace z3 { template expr fpa_const(char const * name); + /** + \brief create a de-Bruijn variable. + */ + expr variable(unsigned index, sort const& s); + + expr fpa_rounding_mode(); expr bool_val(bool b); @@ -3580,6 +3592,11 @@ namespace z3 { return expr(*this, r); } inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); } + inline expr context::variable(unsigned idx, sort const& s) { + Z3_ast r = Z3_mk_bound(m_ctx, idx, s); + check_error(); + return expr(*this, r); + } inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); } inline expr context::int_const(char const * name) { return constant(name, int_sort()); } inline expr context::real_const(char const * name) { return constant(name, real_sort()); } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index c97cd2124..e829fdafb 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1469,7 +1469,9 @@ def FreshConst(sort, prefix="c"): def Var(idx, s): """Create a Z3 free variable. Free variables are used to create quantified formulas. - + A free variable with index n is bound when it occurs within the scope of n+1 quantified + declarations. + >>> Var(0, IntSort()) Var(0) >>> eq(Var(0, IntSort()), Var(0, BoolSort())) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 1100d60dd..467f30792 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4051,7 +4051,10 @@ extern "C" { Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]); /** - \brief Create a bound variable. + \brief Create a variable. + + Variables are intended to be bound by a scope created by a quantifier. So we call them bound variables + even if they appear as free variables in the expression produced by \c Z3_mk_bound. Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from @@ -5318,8 +5321,9 @@ extern "C" { Z3_ast const to[]); /** - \brief Substitute the free variables in \c a with the expressions in \c to. + \brief Substitute the variables in \c a with the expressions in \c to. For every \c i smaller than \c num_exprs, the variable with de-Bruijn index \c i is replaced with term \ccode{to[i]}. + Note that a variable is created using the function \ref Z3_mk_bound. def_API('Z3_substitute_vars', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST))) */ From 9054e729203931be474a9cdb15d6bc16e000cf01 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Dec 2022 19:35:20 -0800 Subject: [PATCH 3/6] fix #6467 --- src/muz/base/dl_rule.cpp | 25 ++++++++------- src/muz/base/dl_rule.h | 2 +- src/muz/base/dl_util.h | 23 +++++++------- src/muz/rel/dl_base.h | 2 +- src/muz/rel/dl_finite_product_relation.cpp | 2 +- src/muz/rel/dl_mk_explanations.cpp | 37 ++++++++++++---------- src/muz/rel/dl_relation_manager.cpp | 2 +- src/muz/rel/dl_sieve_relation.cpp | 4 +-- 8 files changed, 51 insertions(+), 46 deletions(-) diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index a1864d3b9..4ef02c03c 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -1013,28 +1013,31 @@ namespace datalog { } } - void rule::display(context & ctx, std::ostream & out) const { + void rule::display(context & ctx, std::ostream & out, bool compact) const { ast_manager & m = ctx.get_manager(); - out << m_name.str () << ":\n"; + if (!compact) + out << m_name.str () << ":\n"; output_predicate(ctx, m_head, out); if (m_tail_size == 0) { - out << ".\n"; + out << "."; + if (!compact) + out << "\n"; return; } out << " :- "; for (unsigned i = 0; i < m_tail_size; i++) { if (i > 0) out << ","; - out << "\n "; + if (!compact) + out << "\n"; + out << " "; if (is_neg_tail(i)) out << "not "; app * t = get_tail(i); - if (ctx.is_predicate(t)) { + if (ctx.is_predicate(t)) output_predicate(ctx, t, out); - } - else { + else out << mk_pp(t, m); - } } out << '.'; if (ctx.output_profile()) { @@ -1042,10 +1045,10 @@ namespace datalog { output_profile(out); out << '}'; } - out << '\n'; - if (m_proof) { + if (!compact) + out << '\n'; + if (m_proof) out << mk_pp(m_proof, m) << '\n'; - } } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 6a21a2621..60b2bbe8f 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -365,7 +365,7 @@ namespace datalog { void get_vars(ast_manager& m, ptr_vector& sorts) const; - void display(context & ctx, std::ostream & out) const; + void display(context & ctx, std::ostream & out, bool compact = false) const; /** \brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules. diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index 4688a67fd..623f287f7 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -320,32 +320,31 @@ namespace datalog { unsigned_vector & res, bool & identity); template - void permutate_by_cycle(T & container, unsigned cycle_len, const unsigned * permutation_cycle) { - if (cycle_len<2) { + void permute_by_cycle(T& container, unsigned cycle_len, const unsigned * permutation_cycle) { + if (cycle_len < 2) return; - } auto aux = container[permutation_cycle[0]]; - for (unsigned i=1; i - void permutate_by_cycle(ref_vector & container, unsigned cycle_len, const unsigned * permutation_cycle) { + void permute_by_cycle(ref_vector & container, unsigned cycle_len, const unsigned * permutation_cycle) { if (cycle_len<2) { return; } + verbose_stream() << "ptr\n"; T * aux = container.get(permutation_cycle[0]); - for (unsigned i=1; i - void permutate_by_cycle(T & container, const unsigned_vector & permutation_cycle) { - permutate_by_cycle(container, permutation_cycle.size(), permutation_cycle.data()); + void permute_by_cycle(T & container, const unsigned_vector & permutation_cycle) { + permute_by_cycle(container, permutation_cycle.size(), permutation_cycle.data()); } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index ea317ca45..f6d031624 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -160,7 +160,7 @@ namespace datalog { SASSERT(cycle_len>=2); result=src; - permutate_by_cycle(result, cycle_len, permutation_cycle); + permute_by_cycle(result, cycle_len, permutation_cycle); } /** diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index a991c9e6c..b1cdf0553 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -674,7 +674,7 @@ namespace datalog { unsigned sig_sz = r.get_signature().size(); unsigned_vector permutation; add_sequence(0, sig_sz, permutation); - permutate_by_cycle(permutation, cycle_len, permutation_cycle); + permute_by_cycle(permutation, cycle_len, permutation_cycle); unsigned_vector table_permutation; diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 7c5691c0a..37c67e0c8 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -70,20 +70,16 @@ namespace datalog { m_union_decl(mk_explanations::get_union_decl(get_context()), get_ast_manager()) {} ~explanation_relation_plugin() override { - for (unsigned i = 0; i < m_pool.size(); ++i) { - for (unsigned j = 0; j < m_pool[i].size(); ++j) { + for (unsigned i = 0; i < m_pool.size(); ++i) + for (unsigned j = 0; j < m_pool[i].size(); ++j) dealloc(m_pool[i][j]); - } - } } bool can_handle_signature(const relation_signature & s) override { unsigned n=s.size(); - for (unsigned i=0; iget_sort()), m_data[0]); + verbose_stream() << "FORMULA " << fml << "\n"; } bool is_undefined(unsigned col_idx) const { @@ -339,6 +340,7 @@ namespace datalog { if (!r.empty()) { relation_fact proj_data = r.m_data; project_out_vector_columns(proj_data, m_removed_cols); + verbose_stream() << "project\n"; res->assign_data(proj_data); } return res; @@ -365,9 +367,9 @@ namespace datalog { explanation_relation * res = static_cast(plugin.mk_empty(get_result_signature())); if (!r.empty()) { - relation_fact permutated_data = r.m_data; - permutate_by_cycle(permutated_data, m_cycle); - res->assign_data(permutated_data); + relation_fact permuted_data = r.m_data; + permute_by_cycle(dynamic_cast(permuted_data), m_cycle); + res->assign_data(permuted_data); } return res; } @@ -406,6 +408,7 @@ namespace datalog { } else { if (tgt.empty()) { + verbose_stream() << "union\n"; tgt.assign_data(src.m_data); if (delta && delta->empty()) { delta->assign_data(src.m_data); @@ -704,7 +707,7 @@ namespace datalog { symbol mk_explanations::get_rule_symbol(rule * r) { if (r->name() == symbol::null) { std::stringstream sstm; - r->display(m_context, sstm); + r->display(m_context, sstm, true); std::string res = sstm.str(); res = res.substr(0, res.find_last_not_of('\n')+1); return symbol(res.c_str()); diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 9410e2ab0..8de25c8f3 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1149,7 +1149,7 @@ namespace datalog { } void modify_fact(table_fact & f) const override { - permutate_by_cycle(f, m_cycle); + permute_by_cycle(f, m_cycle); } table_base * operator()(const table_base & t) override { diff --git a/src/muz/rel/dl_sieve_relation.cpp b/src/muz/rel/dl_sieve_relation.cpp index c7eab9549..801108999 100644 --- a/src/muz/rel/dl_sieve_relation.cpp +++ b/src/muz/rel/dl_sieve_relation.cpp @@ -413,14 +413,14 @@ namespace datalog { unsigned sig_sz = r.get_signature().size(); unsigned_vector permutation; add_sequence(0, sig_sz, permutation); - permutate_by_cycle(permutation, cycle_len, permutation_cycle); + permute_by_cycle(permutation, cycle_len, permutation_cycle); bool inner_identity; unsigned_vector inner_permutation; collect_sub_permutation(permutation, r.m_sig2inner, inner_permutation, inner_identity); bool_vector result_inner_cols = r.m_inner_cols; - permutate_by_cycle(result_inner_cols, cycle_len, permutation_cycle); + permute_by_cycle(result_inner_cols, cycle_len, permutation_cycle); relation_signature result_sig; relation_signature::from_rename(r.get_signature(), cycle_len, permutation_cycle, result_sig); From dbb4bbe7dc8b494c7a3aff206672a7fcab69317c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Dec 2022 19:36:55 -0800 Subject: [PATCH 4/6] remove debug out --- src/muz/rel/dl_mk_explanations.cpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 37c67e0c8..a4b704597 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -147,7 +147,6 @@ namespace datalog { void assign_data(const relation_fact & f) { m_empty = false; - verbose_stream() << "assign data " << f << "\n"; unsigned n = get_signature().size(); SASSERT(f.size()==n); m_data.reset(); @@ -159,7 +158,6 @@ namespace datalog { m_data.resize(get_signature().size()); } void unite_with_data(const relation_fact & f) { - verbose_stream() << "unite data " << f << "\n"; if (empty()) { assign_data(f); @@ -186,7 +184,6 @@ namespace datalog { void to_formula(expr_ref& fml) const override { ast_manager& m = fml.get_manager(); fml = m.mk_eq(m.mk_var(0, m_data[0]->get_sort()), m_data[0]); - verbose_stream() << "FORMULA " << fml << "\n"; } bool is_undefined(unsigned col_idx) const { @@ -340,7 +337,6 @@ namespace datalog { if (!r.empty()) { relation_fact proj_data = r.m_data; project_out_vector_columns(proj_data, m_removed_cols); - verbose_stream() << "project\n"; res->assign_data(proj_data); } return res; @@ -408,7 +404,6 @@ namespace datalog { } else { if (tgt.empty()) { - verbose_stream() << "union\n"; tgt.assign_data(src.m_data); if (delta && delta->empty()) { delta->assign_data(src.m_data); From c4b2acac24c1e660df99bbf4364f531826186b11 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Dec 2022 09:27:43 -0800 Subject: [PATCH 5/6] add missing error checking #6492 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 838a34be6..ec7b451fa 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1919,21 +1919,21 @@ namespace z3 { inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); } inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; } - inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); } + inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); } inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); } inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; } - inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); } + inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); } inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); } inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; } - inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); } + inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); } inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); } inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; } - inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); } - inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); } - inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); } + inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); } + inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); } + inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); } inline expr min(expr const& a, expr const& b) { check_context(a, b); Z3_ast r; @@ -1947,6 +1947,7 @@ namespace z3 { assert(a.is_fpa()); r = Z3_mk_fpa_min(a.ctx(), a, b); } + a.check_error(); return expr(a.ctx(), r); } inline expr max(expr const& a, expr const& b) { @@ -1962,6 +1963,7 @@ namespace z3 { assert(a.is_fpa()); r = Z3_mk_fpa_max(a.ctx(), a, b); } + a.check_error(); return expr(a.ctx(), r); } inline expr bvredor(expr const & a) { From d47dd159d7019c103e5a78d9ec1c291919418c9f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Dec 2022 09:43:29 -0800 Subject: [PATCH 6/6] set encoding into gparams because this is the only entry point in zstring #6490 --- src/params/context_params.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index 294c5cbbe..fbdd90b8c 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -109,6 +109,7 @@ void context_params::set(char const * param, char const * value) { else if (p == "encoding") { if (strcmp(value, "unicode") == 0 || strcmp(value, "bmp") == 0 || strcmp(value, "ascii") == 0) { m_encoding = value; + gparams::set("encoding", value); } else { std::stringstream strm;