mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

fix #3832

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-09 19:38:08 -07:00
parent c4b52edb29
commit 1fce2905ec
4 changed files with 24 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -190,13 +190,17 @@ namespace datalog {
m_g_vars.push_back(m_f_vars.back());
}
}
if (f->get_family_id() != null_family_id) {
return BR_FAILED;
}
func_decl* g = nullptr;
if (!m_pred2blast.find(f, g)) {
ptr_vector<sort> domain;
for (unsigned i = 0; i < m_args.size(); ++i) {
domain.push_back(m.get_sort(m_args[i].get()));
for (expr* arg : m_args) {
domain.push_back(m.get_sort(arg));
}
g = m_context.mk_fresh_head_predicate(f->get_name(), symbol("bv"), m_args.size(), domain.c_ptr(), f);
m_old_funcs.push_back(f);
@ -205,7 +209,7 @@ namespace datalog {
m_dst->inherit_predicate(*m_src, f, g);
}
result = m.mk_app(g, m_args.size(), m_args.c_ptr());
result = m.mk_app(g, m_args);
result_pr = nullptr;
return BR_DONE;
}

16
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -172,7 +172,8 @@ namespace datalog {
tgt.norm_vars(m_context.get_rule_manager());
SASSERT(!has_quantifier(src));
if (has_quantifier(src))
throw has_new_quantifier();
if (!m_unifier.unify_rules(tgt, tail_index, src)) {
return false;
@ -425,7 +426,11 @@ namespace datalog {
unsigned i = 0;
for (; i < pt_len && !inlining_allowed(orig, r->get_decl(i)); ++i) {};
SASSERT(!has_quantifier(*r.get()));
CTRACE("dl", has_quantifier(*r.get()), r->display(m_context, tout););
if (has_quantifier(*r.get())) {
tgt.add_rule(r);
continue;
}
if (i == pt_len) {
//there's nothing we can inline in this rule
@ -842,7 +847,12 @@ namespace datalog {
if (m_context.get_params().xform_inline_eager()) {
TRACE("dl", source.display(tout << "before eager inlining\n"););
plan_inlining(source);
something_done = transform_rules(source, *res);
try {
something_done = transform_rules(source, *res);
}
catch (has_new_quantifier) {
return nullptr;
}
VERIFY(res->close()); //this transformation doesn't break the negation stratification
// try eager inlining
if (do_eager_inlining(res)) {

2
src/muz/transforms/dl_mk_rule_inliner.h
View file

@ -82,6 +82,8 @@ namespace datalog {
class mk_rule_inliner : public rule_transformer::plugin {
struct has_new_quantifier {};
class visitor : public st_visitor {
context& m_context;
unsigned_vector m_unifiers;

5
src/smt/theory_arith_nl.h
View file

@ -166,8 +166,7 @@ std::pair<unsigned, int> theory_arith<Ext>::analyze_monomial(expr * m) const {
unsigned c = 0;
int free_var_idx = -1;
int idx = 0;
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
for (expr * arg : *to_app(m)) {
if (m_util.is_numeral(arg))
continue;
if (var == nullptr) {
@ -202,7 +201,7 @@ std::pair<unsigned, int> theory_arith<Ext>::analyze_monomial(expr * m) const {
template<typename Ext>
expr * theory_arith<Ext>::get_monomial_body(expr * m) const {
SASSERT(m_util.is_mul(m));
if (m_util.is_numeral(to_app(m)->get_arg(0)))
if (to_app(m)->get_num_args() == 2 && m_util.is_numeral(to_app(m)->get_arg(0)))
return to_app(m)->get_arg(1);
return m;
}