From c4ee4ffae441de6302ce85a86d47e170b707ddd3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Feb 2019 07:12:34 -0800 Subject: [PATCH] fix pre-prejection> Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbi.cpp | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 9bc92cb49..750dedbce 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -304,15 +304,22 @@ namespace qe { /** * \brief project private symbols. + * - project with respect to shared symbols only. + * retains equalities that are independent of arithmetic + * - project with respect to shared + arithmetic basic terms + * retains predicates that are projected by arithmetic */ void euf_arith_mbi_plugin::project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars) { - term_graph tg(m); + term_graph tg1(m), tg2(m); func_decl_ref_vector shared(m_shared); - //for (app* a : avars) shared.push_back(a->get_decl()); - tg.set_vars(shared, false); - tg.add_lits(lits); + tg1.set_vars(shared, false); + for (app* a : avars) shared.push_back(a->get_decl()); + tg2.set_vars(shared, false); + tg1.add_lits(lits); + tg2.add_lits(lits); lits.reset(); - lits.append(tg.project(*mdl.get())); + lits.append(tg1.project(*mdl.get())); + lits.append(tg2.project(*mdl.get())); TRACE("qe", tout << "project: " << lits << "\n";); }