mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

exposing hyper resolution rule over C API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorne@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-09 11:03:35 -07:00
parent 78f29416f1
commit 2fb2636d76
12 changed files with 153 additions and 141 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lib/api_ast.cpp
View file

@ -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;

84
lib/ast.cpp
View file

@ -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<std::pair<unsigned, unsigned> > const& positions,
vector<expr_ref_vector> const& substs) {
ptr_vector<expr> 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<parameter> 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<sort> sorts;
ptr_vector<expr> 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<std::pair<unsigned, unsigned> > & positions,
vector<expr_ref_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<unsigned>(params[i].get_int());
unsigned y = static_cast<unsigned>(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;
}
// -----------------------------------
//

14
lib/ast.h
View file

@ -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<func_decl> m_cnf_star_decls;
ptr_vector<func_decl> 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<std::pair<unsigned, unsigned> > const& positions,
vector<ref_vector<expr, ast_manager> > 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<expr>& 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<proof, ast_manager>& premises,
obj_ref<expr, ast_manager>& conclusion,
svector<std::pair<unsigned, unsigned> > & positions,
vector<ref_vector<expr, ast_manager> >& substs);
bool is_def_intro(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_DEF_INTRO); }

4
lib/dl_bmc_engine.cpp
View file

@ -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;
}

7
lib/dl_context.cpp
View file

@ -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;
}
}
};

86
lib/dl_decl_plugin.cpp
View file

@ -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<std::pair<unsigned, unsigned> > const& positions,
vector<expr_ref_vector> const& substs) {
ptr_vector<expr> 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<parameter> 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<sort> sorts;
ptr_vector<expr> 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<std::pair<unsigned, unsigned> > & positions,
vector<expr_ref_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<unsigned>(params[i].get_int());
unsigned y = static_cast<unsigned>(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;
}
};

43
lib/dl_decl_plugin.h
View file

@ -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<std::pair<unsigned, unsigned> > const& positions,
vector<expr_ref_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<std::pair<unsigned, unsigned> > & positions,
vector<expr_ref_vector>& substs) const;
};
};

2
lib/dl_mk_rule_inliner.cpp
View file

@ -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<bool> valid;
valid.reset();

4
lib/dl_mk_slice.cpp
View file

@ -181,7 +181,7 @@ namespace datalog {
proof_ref_vector premises0(m);
vector<expr_ref_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());

2
lib/dl_util.cpp
View file

@ -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);
}

2
lib/pdr_context.cpp
View file

@ -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);

44
lib/z3_api.h
View file

@ -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.
*/