mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
setting partial equivalence priority lower so that it doesn't intefere with inlining (partial fix to the fact that inlining will remove such implicit relations). Using short-circuit negation in qe to avoid redundant double negations in intermediary results
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d4f41c0420
commit
8c538fd3f0
|
@ -30,7 +30,7 @@ namespace datalog {
|
|||
ast_manager & m;
|
||||
context & m_context;
|
||||
public:
|
||||
mk_partial_equivalence_transformer(context & ctx, unsigned priority=45000)
|
||||
mk_partial_equivalence_transformer(context & ctx, unsigned priority=30000)
|
||||
: plugin(priority),
|
||||
m(ctx.get_manager()),
|
||||
m_context(ctx) {}
|
||||
|
|
|
@ -307,8 +307,8 @@ namespace datalog {
|
|||
if (m_context.similarity_compressor()) {
|
||||
transf.register_plugin(alloc(mk_similarity_compressor, m_context));
|
||||
}
|
||||
transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
|
||||
transf.register_plugin(alloc(mk_rule_inliner, m_context));
|
||||
transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
|
||||
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
|
||||
transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
|
||||
|
||||
|
|
|
@ -596,7 +596,7 @@ namespace qe {
|
|||
p = m_pols.back();
|
||||
if (!m_is_relevant(e)) {
|
||||
pop();
|
||||
insert(e, p, p?e:m.mk_not(e));
|
||||
insert(e, p, p?e:mk_not(m, e));
|
||||
continue;
|
||||
}
|
||||
if (!is_app(e)) {
|
||||
|
@ -634,7 +634,7 @@ namespace qe {
|
|||
}
|
||||
else {
|
||||
pop();
|
||||
insert(e, p, p?e:m.mk_not(e));
|
||||
insert(e, p, p?e:mk_not(m, e));
|
||||
}
|
||||
|
||||
}
|
||||
|
@ -1208,7 +1208,7 @@ namespace qe {
|
|||
}
|
||||
bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), fml);
|
||||
|
||||
fml = m.mk_not(m.mk_iff(q, fml));
|
||||
fml = mk_not(m, m.mk_iff(q, fml));
|
||||
ast_smt_pp pp(m);
|
||||
out << "; eliminate " << mk_pp(m_var, m) << "\n";
|
||||
out << "(push)\n";
|
||||
|
@ -1303,12 +1303,7 @@ namespace qe {
|
|||
}
|
||||
}
|
||||
TRACE("qe_verbose", tout << "No plugin for " << mk_ismt2_pp(e, m) << "\n";);
|
||||
if (p || m.is_not(e, e)) {
|
||||
result = e;
|
||||
}
|
||||
else {
|
||||
result = m.mk_not(e);
|
||||
}
|
||||
result = p?e:mk_not(m, e);
|
||||
}
|
||||
|
||||
void i_solver_context::mk_atom_fn::operator()(expr* e, bool p, expr_ref& result) {
|
||||
|
@ -1436,7 +1431,7 @@ namespace qe {
|
|||
m_fml = f;
|
||||
f = m_subfml;
|
||||
m_solver.assert_expr(f);
|
||||
}
|
||||
}
|
||||
m_root.init(f);
|
||||
TRACE("qe",
|
||||
for (unsigned i = 0; i < num_vars; ++i) tout << mk_ismt2_pp(vars[i], m) << "\n";
|
||||
|
@ -1591,7 +1586,7 @@ namespace qe {
|
|||
}
|
||||
m_literals.reset();
|
||||
while (node) {
|
||||
m_literals.push_back(m.mk_not(node->assignment()));
|
||||
m_literals.push_back(mk_not(m, node->assignment()));
|
||||
node = node->parent();
|
||||
}
|
||||
add_literal(l1);
|
||||
|
@ -1865,7 +1860,7 @@ namespace qe {
|
|||
//
|
||||
app* mk_eq_value(app* b, rational const& vl) {
|
||||
if (m.is_bool(b)) {
|
||||
if (vl.is_zero()) return m.mk_not(b);
|
||||
if (vl.is_zero()) return to_app(mk_not(m, b));
|
||||
if (vl.is_one()) return b;
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
@ -2604,12 +2599,12 @@ namespace qe {
|
|||
TRACE("qe", tout << "variables extracted" << mk_pp(result, m) << "\n";);
|
||||
|
||||
if (old_q->is_forall()) {
|
||||
result = m.mk_not(result);
|
||||
result = mk_not(m, result);
|
||||
}
|
||||
m_ctx.solve(result, vars);
|
||||
if (old_q->is_forall()) {
|
||||
expr* e = 0;
|
||||
result = m.is_not(result, e)?e:m.mk_not(result);
|
||||
result = m.is_not(result, e)?e:mk_not(m, result);
|
||||
}
|
||||
var_shifter shift(m);
|
||||
shift(result, vars.size(), result);
|
||||
|
|
Loading…
Reference in a new issue