From f736f7e83efc0d0e47147b1ba38db260edc0fdea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Mar 2020 18:15:29 -0800 Subject: [PATCH] merge Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 73 ++++++++++++++++++++++ src/api/api_context.cpp | 1 + src/api/api_context.h | 4 ++ src/api/python/z3/z3.py | 22 +++++++ src/api/python/z3/z3printer.py | 10 ++- src/api/z3_api.h | 52 +++++++++++++++ src/ast/CMakeLists.txt | 1 + src/ast/reg_decl_plugins.cpp | 4 ++ src/ast/static_features.cpp | 4 ++ src/ast/static_features.h | 3 + src/smt/CMakeLists.txt | 1 + src/smt/smt_internalizer.cpp | 3 +- src/smt/smt_setup.cpp | 7 +++ src/smt/smt_setup.h | 1 + src/solver/tactic2solver.cpp | 2 +- src/tactic/bv/bv_size_reduction_tactic.cpp | 4 +- src/tactic/core/elim_uncnstr_tactic.cpp | 4 +- 17 files changed, 189 insertions(+), 7 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index c512d58af80..fa213a6d495 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -249,6 +249,68 @@ extern "C" { MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP); MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP); + Z3_sort Z3_API Z3_mk_refinement_sort(Z3_context c, Z3_ast f) { + Z3_TRY; + LOG_Z3_mk_refinement_sort(c, f); + sort* s = nullptr; + if (to_ast(f)->get_kind() == AST_FUNC_DECL) { + func_decl* g = to_func_decl(to_ast(f)); + s = mk_c(c)->rsutil().mk_sort(g); + } + else { + CHECK_IS_EXPR(f, nullptr); + expr* e = to_expr(f); + s = mk_c(c)->rsutil().mk_sort(e); + } + mk_c(c)->save_ast_trail(s); + RETURN_Z3(of_sort(s)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_sort Z3_API Z3_refine_sort_basis(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_refine_sort_basis(c, s); + sort* s0 = nullptr; + RESET_ERROR_CODE(); + if (!mk_c(c)->rsutil().is_refine_sort(to_sort(s), s0)) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + RETURN_Z3(nullptr); + } + RETURN_Z3(of_sort(s0)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_refine_sort_predicate(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_refine_sort_predicate(c, s); + RESET_ERROR_CODE(); + sort* s0 = nullptr; + expr* e = nullptr; + func_decl* f = nullptr; + if (mk_c(c)->rsutil().is_refine_sort(to_sort(s), s0, e)) { + RETURN_Z3(of_ast(e)); + } + if (mk_c(c)->rsutil().is_refine_sort(to_sort(s), s0, f)) { + RETURN_Z3(of_ast(f)); + } + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + RETURN_Z3(nullptr); + Z3_CATCH_RETURN(nullptr); + } + + MK_UNARY(Z3_mk_relax, mk_c(c)->rsutil().fid(), OP_RS_RELAX, SKIP); + + Z3_ast Z3_API Z3_mk_restrict(Z3_context c, Z3_ast e, Z3_sort s) { + Z3_TRY; + LOG_Z3_mk_restrict(c, e, s); + RESET_ERROR_CODE(); + CHECK_IS_EXPR(e, nullptr); + expr* result = mk_c(c)->rsutil().mk_restrict(to_expr(e), to_sort(s)); + mk_c(c)->save_ast_trail(result); + RETURN_Z3(of_ast(result)); + Z3_CATCH_RETURN(nullptr); + } + Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) { expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3)); mk_c(c)->save_ast_trail(result); @@ -714,6 +776,9 @@ extern "C" { else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) { return Z3_RE_SORT; } + else if (fid == mk_c(c)->rsutil().fid() && k == REFINE_SORT) { + return Z3_REFINE_SORT; + } else { return Z3_UNKNOWN_SORT; } @@ -1290,6 +1355,14 @@ extern "C" { } } + if (mk_c(c)->get_rs_fid() == _d->get_family_id()) { + switch (_d->get_decl_kind()) { + case OP_RS_RELAX: return Z3_OP_RELAX; + case OP_RS_RESTRICT: return Z3_OP_RESTRICT; + default: break; + } + } + return Z3_OP_UNINTERPRETED; Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED); } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index bd0967ab214..b0d7999ed87 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -81,6 +81,7 @@ namespace api { m_fpa_util(m()), m_sutil(m()), m_recfun(m()), + m_rs_util(m()), m_last_result(m()), m_ast_trail(m()), m_pmanager(m_limit) { diff --git a/src/api/api_context.h b/src/api/api_context.h index 28fee34b36a..68347541f6d 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -33,6 +33,7 @@ Revision History: #include "ast/fpa_decl_plugin.h" #include "ast/recfun_decl_plugin.h" #include "ast/special_relations_decl_plugin.h" +#include "ast/refinement_sort_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" #include "smt/params/smt_params.h" #include "smt/smt_kernel.h" @@ -89,6 +90,7 @@ namespace api { fpa_util m_fpa_util; seq_util m_sutil; recfun::util m_recfun; + refinement_sort_util m_rs_util; // Support for old solver API smt_params m_fparams; @@ -157,6 +159,7 @@ namespace api { datatype_util& dtutil() { return m_dt_plugin->u(); } seq_util& sutil() { return m_sutil; } recfun::util& recfun() { return m_recfun; } + refinement_sort_util& rsutil() { return m_rs_util; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } family_id get_arith_fid() const { return m_arith_fid; } @@ -166,6 +169,7 @@ namespace api { family_id get_pb_fid() const { return m_pb_fid; } family_id get_fpa_fid() const { return m_fpa_fid; } family_id get_seq_fid() const { return m_seq_fid; } + family_id get_rs_fid() const { return m_rs_util.fid(); } datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; } family_id get_special_relations_fid() const { return m_special_relations_fid; } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 4c143f3ff63..9d6f7d1c4fb 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -629,6 +629,8 @@ def _to_sort_ref(s, ctx): return ReSortRef(s, ctx) elif k == Z3_SEQ_SORT: return SeqSortRef(s, ctx) + elif k == Z3_REFINE_SORT: + return RefinementSortRef(s, ctx) return SortRef(s, ctx) def _sort(ctx, a): @@ -10465,3 +10467,23 @@ def TransitiveClosure(f): The transitive closure R+ is a new relation. """ return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx) + +# Refinement sorts + +class RefinementSortRef(SortRef): + """Refinement sort.""" + + def basis(self): + return _to_sort_ref(Z3_refine_sort_basis(self.ctx_ref(), self.ast), self.ctx) + + def predicate(self): + return _to_expr_ref(Z3_refine_sort_predicate(self.ctx_ref(), self.ast), self.ctx) + +def Relax(e): + return _to_expr_ref(Z3_mk_relax(e.ctx_ref(), e.as_ast()), e.ctx) + +def Restrict(e, s): + return _to_expr_ref(Z3_mk_restrict(e.ctx_ref(), e.as_ast(), s.as_ast()), e.ctx) + +def RefineSort(p): + return _to_sort_ref(Z3_mk_refinement_sort(p.ctx_ref(), p.as_ast()), p.ctx) diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 6bc247b5831..3baadfe4bc5 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -46,7 +46,7 @@ def _z3_assert(cond, msg): Z3_OP_RE_INTERSECT : 'Intersect', Z3_OP_RE_COMPLEMENT : 'Complement', Z3_OP_FPA_IS_NAN : 'fpIsNaN', Z3_OP_FPA_IS_INF : 'fpIsInf', Z3_OP_FPA_IS_ZERO : 'fpIsZero', Z3_OP_FPA_IS_NORMAL : 'fpIsNormal', Z3_OP_FPA_IS_SUBNORMAL : 'fpIsSubnormal', - Z3_OP_FPA_IS_NEGATIVE : 'fpIsNegative', Z3_OP_FPA_IS_POSITIVE : 'fpIsPositive', + Z3_OP_FPA_IS_NEGATIVE : 'fpIsNegative', Z3_OP_FPA_IS_POSITIVE : 'fpIsPositive', } # List of infix operators @@ -566,6 +566,14 @@ def pp_sort(self, s): return seq1('FPSort', (to_format(s.ebits()), to_format(s.sbits()))) elif isinstance(s, z3.ReSortRef): return seq1('ReSort', (self.pp_sort(s.basis()), )) + elif isinstance(s, z3.RefinementSortRef): + f1 = self.pp_sort(s.basis()) + p = s.predicate() + if isinstance(p, z3.ExprRef): + s2 = self.pp_expr(p, 0, []) + else: + s2 = self.pp_fdecl(p, 0, []) + return seq1('RefineSort', [f1, to_format(s2)]) elif isinstance(s, z3.SeqSortRef): if s.is_string(): return to_format("String") diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 920665ca534..e02e5958e01 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -159,6 +159,7 @@ typedef enum Z3_ROUNDING_MODE_SORT, Z3_SEQ_SORT, Z3_RE_SORT, + Z3_REFINE_SORT, Z3_UNKNOWN_SORT = 1000 } Z3_sort_kind; @@ -998,6 +999,11 @@ typedef enum 3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE, 4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO. + - Z3_OP_RELAX: takes a term of refinement sort s | p, and injects to sort s. + + - Z3_OP_RESTRCIT: takes a term of sort s and projects to refinement sort s | p + + - Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information. @@ -1302,6 +1308,10 @@ typedef enum { Z3_OP_FPA_BVWRAP, Z3_OP_FPA_BV2RM, + // injection and projection to refinement sorts + Z3_OP_RELAX = 0xc000, + Z3_OP_RESTRICT, + Z3_OP_INTERNAL, Z3_OP_UNINTERPRETED @@ -3771,6 +3781,48 @@ extern "C" { /*@}*/ + /** @name Refinement sort */ + /*@{*/ + + /** + \brief creates refinement sort given lambda expression f (of sort Array(s, Bool)) + or given function f with signature s -> Bool + + def_API('Z3_mk_refinement_sort', SORT, (_in(CONTEXT), _in(AST))) + */ + Z3_sort Z3_API Z3_mk_refinement_sort(Z3_context c, Z3_ast f); + + + /** + \brief retrieve base sort from refinement sort + + def_API('Z3_refine_sort_basis', SORT, (_in(CONTEXT), _in(SORT))) + */ + Z3_sort Z3_API Z3_refine_sort_basis(Z3_context c, Z3_sort s); + + /** + \brief retrieve predicate from refinement sort + + def_API('Z3_refine_sort_predicate', AST, (_in(CONTEXT), _in(SORT))) + */ + Z3_ast Z3_API Z3_refine_sort_predicate(Z3_context c, Z3_sort s); + + + /** + \brief takes term e of refinement sort s | p and produces injection into s. + + def_API('Z3_mk_relax', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_relax(Z3_context c, Z3_ast e); + + /** + \brief takes term e of refinement sort s | p and produces injection into s. + + def_API('Z3_mk_restrict', AST, (_in(CONTEXT), _in(AST), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_restrict(Z3_context c, Z3_ast e, Z3_sort s); + /*@}*/ + /** @name Quantifiers */ /*@{*/ /** diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 0bcc4d84732..7908cccf0e5 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -38,6 +38,7 @@ z3_add_component(ast pb_decl_plugin.cpp pp.cpp recfun_decl_plugin.cpp + refinement_sort_decl_plugin.cpp reg_decl_plugins.cpp seq_decl_plugin.cpp shared_occs.cpp diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index 6c88f25031d..b2fcbd21432 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -28,6 +28,7 @@ Revision History: #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/special_relations_decl_plugin.h" +#include "ast/refinement_sort_decl_plugin.h" void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("arith")))) { @@ -60,4 +61,7 @@ void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("special_relations")))) { m.register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin)); } + if (!m.get_plugin(m.mk_family_id(symbol("refinement_sort")))) { + m.register_plugin(symbol("refinement_sort"), alloc(refinement_sort_decl_plugin)); + } } diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index 7bb34ed14c3..6d1af44c669 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -26,6 +26,7 @@ static_features::static_features(ast_manager & m): m_arrayutil(m), m_fpautil(m), m_sequtil(m), + m_rsutil(m), m_bfid(m.get_basic_family_id()), m_afid(m.mk_family_id("arith")), m_lfid(m.mk_family_id("label")), @@ -80,6 +81,7 @@ void static_features::reset() { m_has_bv = false; m_has_fpa = false; m_has_sr = false; + m_has_rs = false; m_has_str = false; m_has_seq_non_str = false; m_has_arrays = false; @@ -279,6 +281,8 @@ void static_features::update_core(expr * e) { m_has_fpa = true; if (is_app(e) && to_app(e)->get_family_id() == m_srfid) m_has_sr = true; + if (m_rsutil.is_refine_sort(e)) + m_has_rs = true; if (!m_has_arrays && m_arrayutil.is_array(e)) m_has_arrays = true; if (!m_has_ext_arrays && m_arrayutil.is_array(e) && diff --git a/src/ast/static_features.h b/src/ast/static_features.h index f7a59ca0061..871cbd94036 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -26,12 +26,14 @@ Revision History: #include "ast/fpa_decl_plugin.h" #include "ast/seq_decl_plugin.h" #include "ast/special_relations_decl_plugin.h" +#include "ast/refinement_sort_decl_plugin.h" #include "util/map.h" struct static_features { ast_manager & m; arith_util m_autil; bv_util m_bvutil; + refinement_sort_util m_rsutil; array_util m_arrayutil; fpa_util m_fpautil; seq_util m_sequtil; @@ -82,6 +84,7 @@ struct static_features { bool m_has_bv; // bool m_has_fpa; // bool m_has_sr; // has special relations + bool m_has_rs; // has refinement sorts bool m_has_str; // has String-typed terms bool m_has_seq_non_str; // has non-String-typed Sequence terms bool m_has_arrays; // diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index e08b55e30b1..80e8c00d471 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -65,6 +65,7 @@ z3_add_component(smt theory_opt.cpp theory_pb.cpp theory_recfun.cpp + theory_refinement_sort.cpp theory_seq.cpp theory_special_relations.cpp theory_str.cpp diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 2dfaa49c9a3..08a9a581914 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -840,7 +840,8 @@ namespace smt { \brief Internalize an uninterpreted function application or constant. */ void context::internalize_uninterpreted(app * n) { - SASSERT(!e_internalized(n)); + if (e_internalized(n)) + return; // process args for (expr * arg : *n) { internalize_rec(arg, false); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index cc4dff65e79..bd08727cf67 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -34,6 +34,7 @@ Revision History: #include "smt/theory_seq_empty.h" #include "smt/theory_seq.h" #include "smt/theory_special_relations.h" +#include "smt/theory_refinement_sort.h" #include "smt/theory_pb.h" #include "smt/theory_fpa.h" #include "smt/theory_str.h" @@ -942,6 +943,10 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_special_relations, m_manager)); } + void setup::setup_refinement_sort() { + m_context.register_plugin(alloc(smt::theory_refinement_sort, m_manager)); + } + void setup::setup_unknown() { static_features st(m_manager); ptr_vector fmls; @@ -958,6 +963,7 @@ namespace smt { setup_card(); setup_fpa(); if (st.m_has_sr) setup_special_relations(); + if (st.m_has_rs) setup_refinement_sort(); } void setup::setup_unknown(static_features & st) { @@ -975,6 +981,7 @@ namespace smt { setup_fpa(); setup_recfuns(); if (st.m_has_sr) setup_special_relations(); + if (st.m_has_rs) setup_refinement_sort(); return; } diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 53186f91c98..40477b6fefb 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -83,6 +83,7 @@ namespace smt { void setup_LRA(); void setup_CSP(); void setup_special_relations(); + void setup_refinement_sort(); void setup_AUFLIA(bool simple_array = true); void setup_AUFLIA(static_features const & st); void setup_AUFLIRA(bool simple_array = true); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 426eae75b03..e4b381aa1fb 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -188,7 +188,7 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as } break; } - m_mc = concat(g->mc(), m_mc.get()); + m_mc = concat(m_mc.get(), g->mc()); if (m_mc && md) { (*m_mc)(md); } diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 6b332d7be28..334cf1587db 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -178,7 +178,7 @@ class bv_size_reduction_tactic : public tactic { void run(goal & g, model_converter_ref & mc) { if (g.inconsistent()) return; - TRACE("before_bv_size_reduction", g.display(tout);); + TRACE("goal", g.display(tout);); m_produce_models = g.models_enabled(); mc = nullptr; m_mc = nullptr; @@ -365,7 +365,7 @@ class bv_size_reduction_tactic : public tactic { m_fmc = nullptr; } report_tactic_progress(":bv-reduced", num_reduced); - TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout);); + TRACE("goal", g.display(tout); if (m_mc) m_mc->display(tout);); } }; diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index d9329a13722..4ecfb2f571c 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -779,7 +779,7 @@ class elim_uncnstr_tactic : public tactic { void run(goal_ref const & g, goal_ref_buffer & result) { bool produce_proofs = g->proofs_enabled(); - TRACE("elim_uncnstr_bug", g->display(tout);); + TRACE("goal", g->display(tout);); tactic_report report("elim-uncnstr", *g); m_vars.reset(); collect_occs p; @@ -826,7 +826,7 @@ class elim_uncnstr_tactic : public tactic { m_rw = nullptr; result.push_back(g.get()); g->inc_depth(); - TRACE("elim_uncnstr_bug", g->display(tout);); + TRACE("goal", g->display(tout);); return; } modified = false;