diff --git a/lib/api_ast.cpp b/lib/api_ast.cpp index 7e3db046f..425ec26a5 100644 --- a/lib/api_ast.cpp +++ b/lib/api_ast.cpp @@ -964,7 +964,7 @@ extern "C" { case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR; case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ; case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA; - + case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE; default: UNREACHABLE(); return Z3_OP_UNINTERPRETED; diff --git a/lib/ast.cpp b/lib/ast.cpp index ac854c1ac..8d997c4e9 100644 --- a/lib/ast.cpp +++ b/lib/ast.cpp @@ -646,7 +646,8 @@ basic_decl_plugin::basic_decl_plugin(): m_def_intro_decl(0), m_iff_oeq_decl(0), m_skolemize_decl(0), - m_mp_oeq_decl(0) { + m_mp_oeq_decl(0), + m_hyper_res_decl0(0) { } bool basic_decl_plugin::check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const { @@ -751,6 +752,9 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_param SASSERT(num_parents == 0); return mk_proof_decl("quant-inst", k, num_parameters, params, num_parents); } + case PR_HYPER_RESOLVE: { + return mk_proof_decl("hyper-res", k, num_parameters, params, num_parents); + } default: UNREACHABLE(); return 0; @@ -813,6 +817,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl); case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl); case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls); + case PR_HYPER_RESOLVE: return mk_proof_decl("hyper-res", k, num_parents, m_hyper_res_decl0); default: UNREACHABLE(); return 0; @@ -934,6 +939,7 @@ void basic_decl_plugin::finalize() { DEC_ARRAY_REF(m_cnf_star_decls); DEC_ARRAY_REF(m_th_lemma_decls); + DEC_REF(m_hyper_res_decl0); } @@ -2830,6 +2836,82 @@ proof * ast_manager::mk_th_lemma( return mk_app(m_basic_family_id, PR_TH_LEMMA, num_params+1, parameters.c_ptr(), args.size(), args.c_ptr()); } +proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl, + svector > const& positions, + vector const& substs) { + ptr_vector fmls; + SASSERT(positions.size() + 1 == substs.size()); + for (unsigned i = 0; i < num_premises; ++i) { + TRACE("dl", tout << mk_pp(premises[i], *this) << "\n";); + fmls.push_back(get_fact(premises[i])); + } + SASSERT(is_bool(concl)); + vector params; + for (unsigned i = 0; i < substs.size(); ++i) { + expr_ref_vector const& vec = substs[i]; + for (unsigned j = 0; j < vec.size(); ++j) { + params.push_back(parameter(vec[j])); + } + if (i + 1 < substs.size()) { + params.push_back(parameter(positions[i].first)); + params.push_back(parameter(positions[i].second)); + } + } + ptr_vector sorts; + ptr_vector args; + for (unsigned i = 0; i < num_premises; ++i) { + sorts.push_back(mk_proof_sort()); + args.push_back(premises[i]); + } + sorts.push_back(mk_bool_sort()); + args.push_back(concl); + app* result = mk_app(m_basic_family_id, PR_HYPER_RESOLVE, params.size(), params.c_ptr(), args.size(), args.c_ptr()); + SASSERT(result->get_family_id() == m_basic_family_id); + SASSERT(result->get_decl_kind() == PR_HYPER_RESOLVE); + return result; +} + +bool ast_manager::is_hyper_resolve( + proof* p, + proof_ref_vector& premises, + expr_ref& conclusion, + svector > & positions, + vector & substs) { + if (!is_hyper_resolve(p)) { + return false; + } + unsigned sz = p->get_num_args(); + SASSERT(sz > 0); + for (unsigned i = 0; i + 1 < sz; ++i) { + premises.push_back(to_app(p->get_arg(i))); + } + conclusion = p->get_arg(sz-1); + func_decl* d = p->get_decl(); + unsigned num_p = d->get_num_parameters(); + parameter const* params = d->get_parameters(); + + substs.push_back(expr_ref_vector(*this)); + for (unsigned i = 0; i < num_p; ++i) { + if (params[i].is_int()) { + SASSERT(i + 1 < num_p); + SASSERT(params[i+1].is_int()); + unsigned x = static_cast(params[i].get_int()); + unsigned y = static_cast(params[i+1].get_int()); + positions.push_back(std::make_pair(x, y)); + substs.push_back(expr_ref_vector(*this)); + ++i; + } + else { + SASSERT(params[i].is_ast()); + ast* a = params[i].get_ast(); + SASSERT(is_expr(a)); + substs.back().push_back(to_expr(a)); + } + } + + return true; +} + // ----------------------------------- // diff --git a/lib/ast.h b/lib/ast.h index 86ebcf1fe..8691ed1f4 100644 --- a/lib/ast.h +++ b/lib/ast.h @@ -972,7 +972,7 @@ enum basic_op_kind { PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM, PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR, - PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, LAST_BASIC_PR + PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR }; class basic_decl_plugin : public decl_plugin { @@ -1034,6 +1034,7 @@ protected: ptr_vector m_cnf_star_decls; ptr_vector m_th_lemma_decls; + func_decl * m_hyper_res_decl0; static bool is_proof(decl_kind k) { return k > LAST_BASIC_OP; } bool check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const; @@ -1928,6 +1929,11 @@ public: bool is_proof(expr const * n) const { return is_app(n) && to_app(n)->get_decl()->get_range() == m_proof_sort; } + proof* mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl, + svector > const& positions, + vector > const& substs); + + bool is_undef_proof(expr const * e) const { return e == m_undef_proof; } bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); } bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); } @@ -1947,6 +1953,12 @@ public: bool is_lemma(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_LEMMA); } bool is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector& binding) const; bool is_rewrite(expr const* e, expr*& r1, expr*& r2) const; + bool is_hyper_resolve(proof* p) const { return is_app_of(p, m_basic_family_id, PR_HYPER_RESOLVE); } + bool is_hyper_resolve(proof* p, + ref_vector& premises, + obj_ref& conclusion, + svector > & positions, + vector >& substs); bool is_def_intro(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_DEF_INTRO); } diff --git a/lib/dl_bmc_engine.cpp b/lib/dl_bmc_engine.cpp index c8d917d82..8ad46ae3e 100644 --- a/lib/dl_bmc_engine.cpp +++ b/lib/dl_bmc_engine.cpp @@ -179,7 +179,7 @@ namespace datalog { substs.push_back(sub1); substs.push_back(sub); - pr = util.mk_hyper_resolve(2, premises, concl, positions, substs); + pr = m.mk_hyper_resolve(2, premises, concl, positions, substs); r0 = r1; } else { @@ -191,7 +191,7 @@ namespace datalog { } else { substs.push_back(sub); - pr = util.mk_hyper_resolve(1, &p, concl, positions, substs); + pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); } r0 = r2; } diff --git a/lib/dl_context.cpp b/lib/dl_context.cpp index 6c6f2bce5..079fcaa9e 100644 --- a/lib/dl_context.cpp +++ b/lib/dl_context.cpp @@ -54,6 +54,7 @@ Revision History: #include"expr_functors.h" #include"dl_mk_partial_equiv.h" #include"dl_mk_bit_blast.h" +#include"datatype_decl_plugin.h" namespace datalog { @@ -1118,10 +1119,11 @@ namespace datalog { class context::engine_type_proc { ast_manager& m; arith_util a; + datatype_util dt; DL_ENGINE m_engine; public: - engine_type_proc(ast_manager& m): m(m), a(m), m_engine(DATALOG_ENGINE) {} + engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {} DL_ENGINE get_engine() const { return m_engine; } void operator()(expr* e) { @@ -1134,6 +1136,9 @@ namespace datalog { else if (is_var(e) && m.is_bool(e)) { m_engine = PDR_ENGINE; } + else if (dt.is_datatype(m.get_sort(e))) { + m_engine = PDR_ENGINE; + } } }; diff --git a/lib/dl_decl_plugin.cpp b/lib/dl_decl_plugin.cpp index e1df89285..db1fbd1dc 100644 --- a/lib/dl_decl_plugin.cpp +++ b/lib/dl_decl_plugin.cpp @@ -489,12 +489,6 @@ namespace datalog { return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info); } - func_decl * dl_decl_plugin::mk_hyper_res(unsigned num_params, parameter const* params, unsigned arity, sort *const* domain) { - ast_manager& m = *m_manager; - func_decl_info info(m_family_id, OP_DL_HYPER_RESOLVE, num_params, params); - return m_manager->mk_func_decl(m_hyper_resolve_sym, arity, domain, m_manager->mk_proof_sort(), info); - } - func_decl * dl_decl_plugin::mk_func_decl( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -606,10 +600,6 @@ namespace datalog { result = mk_compare(OP_DL_LT, m_lt_sym, domain); break; - case OP_DL_HYPER_RESOLVE: - result = mk_hyper_res(num_parameters, parameters, arity, domain); - break; - default: m_manager->raise_exception("operator not recognized"); return 0; @@ -752,80 +742,4 @@ namespace datalog { return m.mk_app(f, num_args, args); } - proof* dl_decl_util::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl, - svector > const& positions, - vector const& substs) { - ptr_vector fmls; - SASSERT(positions.size() + 1 == substs.size()); - for (unsigned i = 0; i < num_premises; ++i) { - TRACE("dl", tout << mk_pp(premises[i], m) << "\n";); - fmls.push_back(m.get_fact(premises[i])); - } - SASSERT(m.is_bool(concl)); - vector params; - for (unsigned i = 0; i < substs.size(); ++i) { - expr_ref_vector const& vec = substs[i]; - for (unsigned j = 0; j < vec.size(); ++j) { - params.push_back(parameter(vec[j])); - } - if (i + 1 < substs.size()) { - params.push_back(parameter(positions[i].first)); - params.push_back(parameter(positions[i].second)); - } - } - ptr_vector sorts; - ptr_vector args; - for (unsigned i = 0; i < num_premises; ++i) { - sorts.push_back(m.mk_proof_sort()); - args.push_back(premises[i]); - } - sorts.push_back(m.mk_bool_sort()); - args.push_back(concl); - app* result = m.mk_app(m_fid, OP_DL_HYPER_RESOLVE, params.size(), params.c_ptr(), args.size(), args.c_ptr()); - SASSERT(result->get_family_id() == m_fid); - SASSERT(result->get_decl_kind() == OP_DL_HYPER_RESOLVE); - return result; - } - - bool dl_decl_util::is_hyper_resolve( - proof* p, - proof_ref_vector& premises, - expr_ref& conclusion, - svector > & positions, - vector & substs) const { - if (!is_hyper_resolve(p)) { - return false; - } - unsigned sz = p->get_num_args(); - SASSERT(sz > 0); - for (unsigned i = 0; i + 1 < sz; ++i) { - premises.push_back(to_app(p->get_arg(i))); - } - conclusion = p->get_arg(sz-1); - func_decl* d = p->get_decl(); - unsigned num_p = d->get_num_parameters(); - parameter const* params = d->get_parameters(); - - substs.push_back(expr_ref_vector(m)); - for (unsigned i = 0; i < num_p; ++i) { - if (params[i].is_int()) { - SASSERT(i + 1 < num_p); - SASSERT(params[i+1].is_int()); - unsigned x = static_cast(params[i].get_int()); - unsigned y = static_cast(params[i+1].get_int()); - positions.push_back(std::make_pair(x, y)); - substs.push_back(expr_ref_vector(m)); - ++i; - } - else { - SASSERT(params[i].is_ast()); - ast* a = params[i].get_ast(); - SASSERT(is_expr(a)); - substs.back().push_back(to_expr(a)); - } - } - - return true; - } - }; diff --git a/lib/dl_decl_plugin.h b/lib/dl_decl_plugin.h index 504e5ac85..6e824b639 100644 --- a/lib/dl_decl_plugin.h +++ b/lib/dl_decl_plugin.h @@ -48,7 +48,6 @@ namespace datalog { OP_RA_CLONE, OP_DL_CONSTANT, OP_DL_LT, - OP_DL_HYPER_RESOLVE, LAST_RA_OP }; @@ -211,48 +210,6 @@ namespace datalog { family_id get_family_id() const { return m_fid; } - /** - \brief Hyper-resolution rule that works for Horn clauses (implication) - - Somewhat related to unit resolution and resolution rule from SPC, but - a general sledgehammer rule. - The clause/implication from the first premise is the main clause. - One of the literals in each of the other premises is resolved with the main clause. - - The facts in the premises are closed formulas. Substitutions required for unification - are passed in. - - positions is a vector of pairs of positions in the main clause and the side clause. - - For clauses that are disjunctions the positions are indexed from 0 starting with the first - literal. - - We use the following (Prolog style) convention for Horn implications: - The head of a Horn implication is position 0, - the first conjunct in the body of an implication is position 1 - the second conjunct in the body of an implication is position 2 - - For general implications where the head is a disjunction, the - first n positions correspond to the n disjuncts in the head. - The next m positions correspond to the m conjuncts in the body. - */ - proof* mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl, - svector > const& positions, - vector const& substs); - - bool is_hyper_resolve(proof* p) const { return is_app_of(p, m_fid, OP_DL_HYPER_RESOLVE); } - - - /** - \brief extract components of a hyper-resolution proof rule. - - */ - bool is_hyper_resolve(proof* p, - proof_ref_vector& premises, - expr_ref& conclusion, - svector > & positions, - vector& substs) const; - }; }; diff --git a/lib/dl_mk_rule_inliner.cpp b/lib/dl_mk_rule_inliner.cpp index 5cccb0051..2c6874adf 100644 --- a/lib/dl_mk_rule_inliner.cpp +++ b/lib/dl_mk_rule_inliner.cpp @@ -735,7 +735,7 @@ namespace datalog { } m_subst.reset(); m_subst.reserve_vars(max_var+1); - m_subst.reserve_offsets(std::max(m_tail_index.get_approx_num_regs(), m_head_index.get_approx_num_regs())); + m_subst.reserve_offsets(std::max(m_tail_index.get_approx_num_regs(), 2+m_head_index.get_approx_num_regs())); svector valid; valid.reset(); diff --git a/lib/dl_mk_slice.cpp b/lib/dl_mk_slice.cpp index 979dd8183..846dd6c72 100644 --- a/lib/dl_mk_slice.cpp +++ b/lib/dl_mk_slice.cpp @@ -181,7 +181,7 @@ namespace datalog { proof_ref_vector premises0(m); vector substs, substs0; - if (!util.is_hyper_resolve(p, premises0, slice_concl, positions, substs0)) { + if (!m.is_hyper_resolve(p, premises0, slice_concl, positions, substs0)) { return false; } unsigned num_args = p->get_num_args(); @@ -240,7 +240,7 @@ namespace datalog { r1 = r3; } r1->to_formula(concl); - proof* new_p = util.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs); + proof* new_p = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs); m_pinned_exprs.push_back(new_p); m_pinned_rules.push_back(r1.get()); m_sliceform2rule.insert(slice_concl, r1.get()); diff --git a/lib/dl_util.cpp b/lib/dl_util.cpp index 304e6de68..57be631c2 100644 --- a/lib/dl_util.cpp +++ b/lib/dl_util.cpp @@ -634,7 +634,7 @@ namespace datalog { tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n"; tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";); - pr = util.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs); + pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs); pc->insert(pr); } diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index 752050940..8c09607c4 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -1093,7 +1093,7 @@ namespace pdr { } expr_ref fml_concl(m); reduced_rule->to_formula(fml_concl); - p1 = util.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs); + p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs); } cache.insert(n->state(), p1); rules.insert(n->state(), reduced_rule); diff --git a/lib/z3_api.h b/lib/z3_api.h index 24fcc7f10..6303a0080 100644 --- a/lib/z3_api.h +++ b/lib/z3_api.h @@ -761,6 +761,47 @@ typedef enum - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. + - Z3_OP_PR_HYPER_RESOLVE: Hyper-resolution rule. + + The premises of the rules is a sequence of clauses. + The first clause argument is the main clause of the rule. + One literal from the second, third, .. clause is resolved + with a literal from the first (main) clause. + + Premises of the rules are of the form + \nicebox{ + (or l0 l1 l2 .. ln) + } + or + \nicebox{ + (=> (and ln+1 ln+2 .. ln+m) l0) + } + or in the most general (ground) form: + \nicebox{ + (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)) + } + In other words we use the following (Prolog style) convention for Horn + implications: + The head of a Horn implication is position 0, + the first conjunct in the body of an implication is position 1 + the second conjunct in the body of an implication is position 2 + + For general implications where the head is a disjunction, the + first n positions correspond to the n disjuncts in the head. + The next m positions correspond to the m conjuncts in the body. + + The premises can be universally quantified so that the most + general non-ground form is: + + \nicebox{ + (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))) + } + + The hyper-resolution rule takes a sequence of parameters. + The parameters are substitutions of bound variables separated by pairs + of literal positions from the main clause and side clause. + + - Z3_OP_RA_STORE: Insert a record into a relation. The function takes \c n+1 arguments, where the first argument is the relation and the remaining \c n elements correspond to the \c n columns of the relation. @@ -982,6 +1023,7 @@ typedef enum { Z3_OP_PR_SKOLEMIZE, Z3_OP_PR_MODUS_PONENS_OEQ, Z3_OP_PR_TH_LEMMA, + Z3_OP_PR_HYPER_RESOLVE, // Sequences Z3_OP_RA_STORE = 0x600, @@ -5039,7 +5081,7 @@ END_MLAPI_EXCLUDE /** \brief Backtrack one backtracking point. - \sa Z3_fixedpoing_push + \sa Z3_fixedpoint_push \pre The number of calls to pop cannot exceed calls to push. */