mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
7e330c15e7
commit
7e7360dd0c
|
@ -25,14 +25,16 @@ quantifier_macro_info::quantifier_macro_info(ast_manager& m, quantifier* q) :
|
|||
m_is_auf(true),
|
||||
m_has_x_eq_y(false),
|
||||
m_the_one(m) {
|
||||
SASSERT(is_forall(q));
|
||||
collect_macro_candidates(q);
|
||||
}
|
||||
|
||||
void quantifier_macro_info::collect_macro_candidates(quantifier* q) {
|
||||
macro_util mutil(m);
|
||||
macro_util::macro_candidates candidates(m);
|
||||
mutil.collect_macro_candidates(q, candidates);
|
||||
quantifier_ref qa(q, m);
|
||||
if (is_exists(q))
|
||||
qa = m.update_quantifier(q, quantifier_kind::forall_k, m.mk_not(q->get_expr()));
|
||||
mutil.collect_macro_candidates(qa, candidates);
|
||||
unsigned num_candidates = candidates.size();
|
||||
for (unsigned i = 0; i < num_candidates; i++) {
|
||||
cond_macro* mc = alloc(cond_macro, m, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i),
|
||||
|
|
|
@ -148,8 +148,10 @@ namespace q {
|
|||
sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
|
||||
SASSERT(is_forall(e) || is_exists(e));
|
||||
sat::bool_var v = ctx.get_si().add_bool_var(e);
|
||||
sat::literal lit = ctx.attach_lit(sat::literal(v, sign), e);
|
||||
sat::literal lit = ctx.attach_lit(sat::literal(v, false), e);
|
||||
mk_var(ctx.get_egraph().find(e));
|
||||
if (sign)
|
||||
lit.neg();
|
||||
return lit;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue