mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-13 09:17:35 -08:00
parent 50e00b615f 68ae5d434c
commit b335661d5a
6 changed files with 67 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/dl_mk_slice.h
View file

@ -97,10 +97,14 @@ namespace datalog {
the \c goal must be present in the \c rule_set that is being transformed.
*/
mk_slice(context & ctx);
virtual ~mk_slice() { }
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; }
obj_map<func_decl, func_decl*> const& get_predicates() { return m_predicates; }
};
};

28
src/muz_qe/pdr_context.cpp
View file

@ -20,6 +20,9 @@ Revision History:
Notes:
TODO:
- fix the slicing with covers.
-
--*/
@ -350,7 +353,7 @@ namespace pdr {
}
}
expr_ref pred_transformer::get_cover_delta(int level) {
expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level) {
expr_ref result(m.mk_true(), m), v(m), c(m);
if (level == -1) {
result = pm.mk_and(m_invariants);
@ -368,6 +371,25 @@ namespace pdr {
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
rep->set_substitution(&sub);
(*rep)(result);
// adjust result according to model converter.
unsigned arity = m_head->get_arity();
model_ref md = alloc(model, m);
if (arity == 0) {
md->register_decl(m_head, result);
}
else {
func_interp* fi = alloc(func_interp, m, arity);
fi->set_else(result);
md->register_decl(m_head, fi);
}
apply(ctx.get_model_converter(), md, 0);
if (p_orig->get_arity() == 0) {
result = md->get_const_interp(p_orig);
}
else {
result = md->get_func_interp(p_orig)->get_interp();
}
return result;
}
@ -1181,10 +1203,10 @@ namespace pdr {
}
}
expr_ref context::get_cover_delta(int level, func_decl* p) {
expr_ref context::get_cover_delta(int level, func_decl* p_orig, func_decl* p) {
pred_transformer* pt = 0;
if (m_rels.find(p, pt)) {
return pt->get_cover_delta(level);
return pt->get_cover_delta(p_orig, level);
}
else {
IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";);

6
src/muz_qe/pdr_context.h
View file

@ -126,7 +126,7 @@ namespace pdr {
qinst* get_quantifiers(datalog::rule const* r) const { qinst* q = 0; m_rule2qinst.find(r, q); return q; }
expr* rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); }
unsigned get_num_levels() { return m_levels.size(); }
expr_ref get_cover_delta(int level);
expr_ref get_cover_delta(func_decl* p_orig, int level);
void add_cover(unsigned level, expr* property);
std::ostream& display(std::ostream& strm) const;
@ -385,6 +385,8 @@ namespace pdr {
void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
model_converter_ref get_model_converter() { return m_mc; }
void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
void update_rules(datalog::rule_set& rules);
@ -395,7 +397,7 @@ namespace pdr {
unsigned get_num_levels(func_decl* p);
expr_ref get_cover_delta(int level, func_decl* p);
expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
void add_cover(int level, func_decl* pred, expr* property);

29
src/muz_qe/pdr_dl_interface.cpp
View file

@ -39,7 +39,8 @@ dl_interface::dl_interface(datalog::context& ctx) :
m_ctx(ctx),
m_pdr_rules(ctx),
m_old_rules(ctx),
m_context(0) {
m_context(0),
m_refs(ctx.get_manager()) {
m_context = alloc(pdr::context, ctx.get_fparams(), ctx.get_params(), ctx.get_manager());
}
@ -78,6 +79,8 @@ lbool dl_interface::query(expr * query) {
//we restore the initial state in the datalog context
m_ctx.ensure_opened();
m_pdr_rules.reset();
m_refs.reset();
m_pred2slice.reset();
m_ctx.get_rmanager().reset_relations();
ast_manager& m = m_ctx.get_manager();
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
@ -116,10 +119,20 @@ lbool dl_interface::query(expr * query) {
m_ctx.transform_rules(transformer, mc, pc);
query_pred = slice->get_predicate(query_pred.get());
m_ctx.set_output_predicate(query_pred);
// track sliced predicates.
obj_map<func_decl, func_decl*> const& preds = slice->get_predicates();
obj_map<func_decl, func_decl*>::iterator it = preds.begin();
obj_map<func_decl, func_decl*>::iterator end = preds.end();
for (; it != end; ++it) {
m_pred2slice.insert(it->m_key, it->m_value);
m_refs.push_back(it->m_key);
m_refs.push_back(it->m_value);
}
}
if (m_ctx.get_params().get_uint(":unfold-rules",0) > 0) {
unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules",0);
unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules", 0);
datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
if (m_ctx.get_params().get_uint(":coalesce-rules", false)) {
transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
@ -160,15 +173,23 @@ lbool dl_interface::query(expr * query) {
}
}
expr_ref dl_interface::get_cover_delta(int level, func_decl* pred) {
return m_context->get_cover_delta(level, pred);
expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {
func_decl* pred = pred_orig;
m_pred2slice.find(pred_orig, pred);
SASSERT(pred);
return m_context->get_cover_delta(level, pred_orig, pred);
}
void dl_interface::add_cover(int level, func_decl* pred, expr* property) {
if (m_ctx.get_params().get_bool(":slice", true)) {
throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers");
}
m_context->add_cover(level, pred, property);
}
unsigned dl_interface::get_num_levels(func_decl* pred) {
m_pred2slice.find(pred, pred);
SASSERT(pred);
return m_context->get_num_levels(pred);
}

4
src/muz_qe/pdr_dl_interface.h
View file

@ -37,7 +37,9 @@ namespace pdr {
datalog::context& m_ctx;
datalog::rule_set m_pdr_rules;
datalog::rule_set m_old_rules;
context* m_context;
context* m_context;
obj_map<func_decl, func_decl*> m_pred2slice;
ast_ref_vector m_refs;
void check_reset();

16
src/muz_qe/pdr_manager.cpp
View file

@ -58,24 +58,20 @@ namespace pdr {
expr_ref inductive_property::fixup_clause(expr* fml) const {
expr_ref_vector disjs(m);
datalog::flatten_or(fml, disjs);
switch(disjs.size()) {
case 0: return expr_ref(m.mk_false(), m);
case 1: return expr_ref(disjs[0].get(), m);
default: return expr_ref(m.mk_or(disjs.size(), disjs.c_ptr()), m);
}
expr_ref result(m);
bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result);
return result;
}
expr_ref inductive_property::fixup_clauses(expr* fml) const {
expr_ref_vector conjs(m);
expr_ref result(m);
datalog::flatten_and(fml, conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
conjs[i] = fixup_clause(conjs[i].get());
}
switch(conjs.size()) {
case 0: return expr_ref(m.mk_true(), m);
case 1: return expr_ref(conjs[0].get(), m);
default: return expr_ref(m.mk_and(conjs.size(), conjs.c_ptr()), m);
}
bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result);
return result;
}
std::string inductive_property::to_string() const {