mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
remove qe-lite pass in quant_tatics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
701f32471e
commit
5e737641b7
|
@ -491,6 +491,10 @@ namespace eq {
|
|||
m_new_args.push_back(args[i]);
|
||||
}
|
||||
}
|
||||
if (m_new_args.size() == num_args) {
|
||||
r = q;
|
||||
return;
|
||||
}
|
||||
|
||||
expr_ref t(m);
|
||||
if (q->is_forall()) {
|
||||
|
@ -771,7 +775,7 @@ namespace eq {
|
|||
proof_ref curr_pr(m);
|
||||
q = to_quantifier(r);
|
||||
reduce_quantifier1(q, r, curr_pr);
|
||||
if (m.proofs_enabled()) {
|
||||
if (m.proofs_enabled() && r != q) {
|
||||
pr = m.mk_transitivity(pr, curr_pr);
|
||||
}
|
||||
} while (q != r && is_quantifier(r));
|
||||
|
@ -2297,7 +2301,7 @@ public:
|
|||
}
|
||||
m_imp(indices, true, result);
|
||||
if (is_forall(q)) {
|
||||
result = m.mk_not(result);
|
||||
result = push_not(result);
|
||||
}
|
||||
result = m.update_quantifier(
|
||||
q,
|
||||
|
@ -2476,6 +2480,41 @@ class qe_lite_tactic : public tactic {
|
|||
cooperate("qe-lite");
|
||||
}
|
||||
|
||||
void debug_diff(expr* a, expr* b) {
|
||||
ptr_vector<expr> as, bs;
|
||||
as.push_back(a);
|
||||
bs.push_back(b);
|
||||
expr* a1, *a2, *b1, *b2;
|
||||
while (!as.empty()) {
|
||||
a = as.back();
|
||||
b = bs.back();
|
||||
as.pop_back();
|
||||
bs.pop_back();
|
||||
if (a == b) {
|
||||
continue;
|
||||
}
|
||||
else if (is_forall(a) && is_forall(b)) {
|
||||
as.push_back(to_quantifier(a)->get_expr());
|
||||
bs.push_back(to_quantifier(b)->get_expr());
|
||||
}
|
||||
else if (m.is_and(a, a1, a2) && m.is_and(b, b1, b2)) {
|
||||
as.push_back(a1);
|
||||
as.push_back(a2);
|
||||
bs.push_back(b1);
|
||||
bs.push_back(b2);
|
||||
}
|
||||
else if (m.is_eq(a, a1, a2) && m.is_eq(b, b1, b2)) {
|
||||
as.push_back(a1);
|
||||
as.push_back(a2);
|
||||
bs.push_back(b1);
|
||||
bs.push_back(b2);
|
||||
}
|
||||
else {
|
||||
TRACE("qe", tout << mk_pp(a, m) << " != " << mk_pp(b, m) << "\n";);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
|
@ -2507,7 +2546,11 @@ class qe_lite_tactic : public tactic {
|
|||
new_pr = g->pr(i);
|
||||
}
|
||||
}
|
||||
g->update(i, new_f, new_pr, g->dep(i));
|
||||
if (f != new_f) {
|
||||
TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n";);
|
||||
debug_diff(f, new_f);
|
||||
g->update(i, new_f, new_pr, g->dep(i));
|
||||
}
|
||||
}
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
|
|
|
@ -105,6 +105,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
|
|||
m_eval.set_model_completion(model_completion);
|
||||
try {
|
||||
m_eval(e, result);
|
||||
std::cout << result << "\n";
|
||||
return true;
|
||||
}
|
||||
catch (model_evaluator_exception & ex) {
|
||||
|
|
|
@ -22,8 +22,6 @@ Revision History:
|
|||
#include"solve_eqs_tactic.h"
|
||||
#include"elim_uncnstr_tactic.h"
|
||||
#include"qe_tactic.h"
|
||||
#include"qe_sat_tactic.h"
|
||||
#include"qe_lite.h"
|
||||
#include"qsat.h"
|
||||
#include"nlqsat.h"
|
||||
#include"ctx_simplify_tactic.h"
|
||||
|
@ -54,7 +52,6 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
|
|||
using_params(mk_simplify_tactic(m), pull_ite_p),
|
||||
solve_eqs,
|
||||
mk_elim_uncnstr_tactic(m),
|
||||
mk_qe_lite_tactic(m),
|
||||
mk_simplify_tactic(m));
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue