From 7e7360dd0c04cdee95c3f74a59908209742c5212 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 May 2021 17:40:42 -0700 Subject: [PATCH] #5223 --- src/ast/macros/quantifier_macro_info.cpp | 6 ++++-- src/sat/smt/q_solver.cpp | 4 +++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/macros/quantifier_macro_info.cpp b/src/ast/macros/quantifier_macro_info.cpp index 24e5a32e4..2647baf2f 100644 --- a/src/ast/macros/quantifier_macro_info.cpp +++ b/src/ast/macros/quantifier_macro_info.cpp @@ -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), diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index ebb553365..26d170fb8 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -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; }