mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

towards acceleration

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-02-01 10:36:23 -08:00
parent 2883fed770
commit ca74b2d6cf
1 changed files with 54 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

71
src/muz_qe/tab_context.cpp
View file

@ -1048,7 +1048,6 @@ namespace tb {
class unifier { class unifier {
ast_manager& m; ast_manager& m;
datalog::context& m_ctx;
::unifier m_unifier; ::unifier m_unifier;
substitution m_S1; substitution m_S1;
var_subst m_S2; var_subst m_S2;
@ -1056,9 +1055,8 @@ namespace tb {
expr_ref_vector m_sub1; expr_ref_vector m_sub1;
expr_ref_vector m_sub2; expr_ref_vector m_sub2;
public: public:
unifier(ast_manager& m, datalog::context& ctx): unifier(ast_manager& m):
m(m), m(m),
m_ctx(ctx),
m_unifier(m), m_unifier(m),
m_S1(m), m_S1(m),
m_S2(m, false), m_S2(m, false),
@ -1066,8 +1064,8 @@ namespace tb {
m_sub1(m), m_sub1(m),
m_sub2(m) {} m_sub2(m) {}
bool operator()(ref<clause>& tgt, ref<clause>& src, bool compute_subst, ref<clause>& result) { bool operator()(ref<clause>& tgt, unsigned idx, ref<clause>& src, bool compute_subst, ref<clause>& result) {
return unify(*tgt, *src, compute_subst, result); return unify(*tgt, idx, *src, compute_subst, result);
} }
expr_ref_vector get_rule_subst(bool is_tgt) { expr_ref_vector get_rule_subst(bool is_tgt) {
@ -1079,10 +1077,9 @@ namespace tb {
} }
} }
bool unify(clause const& tgt, clause const& src, bool compute_subst, ref<clause>& result) { bool unify(clause const& tgt, unsigned idx, clause const& src, bool compute_subst, ref<clause>& result) {
qe_lite qe(m); qe_lite qe(m);
reset(); reset();
unsigned idx = tgt.get_predicate_index();
SASSERT(tgt.get_predicate(idx)->get_decl() == src.get_head()->get_decl()); SASSERT(tgt.get_predicate(idx)->get_decl() == src.get_head()->get_decl());
unsigned var_cnt = std::max(tgt.get_num_vars(), src.get_num_vars()); unsigned var_cnt = std::max(tgt.get_num_vars(), src.get_num_vars());
m_S1.reserve(2, var_cnt); m_S1.reserve(2, var_cnt);
@ -1101,11 +1098,13 @@ namespace tb {
m_S1.apply(2, delta, expr_offset(tgt.get_predicate(i), 0), tmp); m_S1.apply(2, delta, expr_offset(tgt.get_predicate(i), 0), tmp);
predicates.push_back(to_app(tmp)); predicates.push_back(to_app(tmp));
} }
} else {
for (unsigned i = 0; i < src.get_num_predicates(); ++i) { for (unsigned j = 0; j < src.get_num_predicates(); ++j) {
m_S1.apply(2, delta, expr_offset(src.get_predicate(i), 1), tmp); m_S1.apply(2, delta, expr_offset(src.get_predicate(j), 1), tmp);
predicates.push_back(to_app(tmp)); predicates.push_back(to_app(tmp));
} }
}
}
m_S1.apply(2, delta, expr_offset(tgt.get_constraint(), 0), tmp); m_S1.apply(2, delta, expr_offset(tgt.get_constraint(), 0), tmp);
m_S1.apply(2, delta, expr_offset(src.get_constraint(), 1), tmp2); m_S1.apply(2, delta, expr_offset(src.get_constraint(), 1), tmp2);
constraint = m.mk_and(tmp, tmp2); constraint = m.mk_and(tmp, tmp2);
@ -1200,6 +1199,18 @@ namespace tb {
} }
}; };
class extract_delta {
ast_manager& m;
unifier m_unifier;
public:
extract_delta(ast_manager& m):
m(m),
m_unifier(m)
{}
// //
// Given a clause // Given a clause
// P(s) :- P(t), Phi(x). // P(s) :- P(t), Phi(x).
@ -1209,14 +1220,7 @@ namespace tb {
// delta2: Delta(z,s) :- Delta(z,t), Phi(x). // delta2: Delta(z,s) :- Delta(z,t), Phi(x).
// //
class extract_delta { void mk_delta_clauses(clause const& g, ref<clause>& acc, ref<clause>& delta1, ref<clause>& delta2) {
ast_manager& m;
public:
extract_delta(ast_manager& m):
m(m)
{}
void operator()(clause const& g, ref<clause>& acc, ref<clause>& delta1, ref<clause>& delta2) {
SASSERT(g.get_num_predicates() > 0); SASSERT(g.get_num_predicates() > 0);
app* p = g.get_head(); app* p = g.get_head();
app* q = g.get_predicate(0); app* q = g.get_predicate(0);
@ -1260,6 +1264,31 @@ namespace tb {
acc->display(verbose_stream() << "acc:\n");); acc->display(verbose_stream() << "acc:\n"););
} }
//
// Given a sequence of clauses and inference rules
// compute a super-predicate and auxiliary clauses.
//
// P1(x) :- P2(y), R(z)
// P2(y) :- P3(z), T(u)
// P3(z) :- P1(x), U(v)
// =>
// P1(x) :- P1(x), R(z), T(u), U(v)
//
ref<clause> resolve_rules(unsigned num_clauses, clause*const* clauses, unsigned const* positions) {
ref<clause> result = clauses[0];
ref<clause> tmp;
unsigned offset = 0;
for (unsigned i = 0; i + 1 < num_clauses; ++i) {
clause const& cl = *clauses[i+1];
offset += positions[i];
VERIFY (m_unifier.unify(*result, offset, cl, false, tmp));
result = tmp;
}
return result;
}
private: private:
expr_ref_vector mk_fresh_vars(clause const& g) { expr_ref_vector mk_fresh_vars(clause const& g) {
@ -1330,7 +1359,7 @@ namespace datalog {
m_index(m), m_index(m),
m_selection(ctx), m_selection(ctx),
m_solver(m, m_fparams), m_solver(m, m_fparams),
m_unifier(m, ctx), m_unifier(m),
m_rules(), m_rules(),
m_seqno(0), m_seqno(0),
m_instruction(tb::SELECT_PREDICATE), m_instruction(tb::SELECT_PREDICATE),
@ -1428,7 +1457,7 @@ namespace datalog {
void apply_rule(ref<tb::clause>& r) { void apply_rule(ref<tb::clause>& r) {
ref<tb::clause> clause = get_clause(); ref<tb::clause> clause = get_clause();
ref<tb::clause> next_clause; ref<tb::clause> next_clause;
if (m_unifier(clause, r, false, next_clause) && if (m_unifier(clause, clause->get_predicate_index(), r, false, next_clause) &&
!query_is_tautology(*next_clause)) { !query_is_tautology(*next_clause)) {
init_clause(next_clause); init_clause(next_clause);
unsigned subsumer = 0; unsigned subsumer = 0;
@ -1585,7 +1614,7 @@ namespace datalog {
unsigned pi = parent->get_predicate_index(); unsigned pi = parent->get_predicate_index();
func_decl* pred = parent->get_predicate(pi)->get_decl(); func_decl* pred = parent->get_predicate(pi)->get_decl();
ref<tb::clause> rl = m_rules.get_rule(pred, p_rule); ref<tb::clause> rl = m_rules.get_rule(pred, p_rule);
VERIFY(m_unifier(parent, rl, true, replayed_clause)); VERIFY(m_unifier(parent, parent->get_predicate_index(), rl, true, replayed_clause));
expr_ref_vector s1(m_unifier.get_rule_subst(true)); expr_ref_vector s1(m_unifier.get_rule_subst(true));
expr_ref_vector s2(m_unifier.get_rule_subst(false)); expr_ref_vector s2(m_unifier.get_rule_subst(false));
resolve_rule(pc, *parent, *rl, s1, s2, *clause); resolve_rule(pc, *parent, *rl, s1, s2, *clause);