From 49bd3ad159240ce4176756e8585302f54900e0ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Jul 2021 16:56:10 -0700 Subject: [PATCH] #5417 again, refining root clauses above search level Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_relevancy.cpp | 9 ++++++++- src/sat/smt/q_solver.cpp | 2 +- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp index 03f9f8ed1..7e9b20af7 100644 --- a/src/sat/smt/euf_relevancy.cpp +++ b/src/sat/smt/euf_relevancy.cpp @@ -38,11 +38,18 @@ namespace euf { } } + /** + * Add a root clause. Root clauses must all be satisfied by the + * final assignment. If a clause is added above search level it + * is subject to removal on backtracking. These clauses are therefore + * not tracked. + */ void solver::add_root(unsigned n, sat::literal const* lits) { if (!relevancy_enabled()) return; ensure_dual_solver(); - m_dual_solver->add_root(n, lits); + if (s().at_search_lvl()) + m_dual_solver->add_root(n, lits); } void solver::add_aux(unsigned n, sat::literal const* lits) { diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index f74ce4778..524c3f1c6 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -62,7 +62,7 @@ namespace q { if (l.sign() == is_forall(e)) { sat::literal lit = skolemize(q); add_clause(~l, lit); - ctx.add_aux(~l, lit); + ctx.add_root(~l, lit); } else { ctx.push_vec(m_universal, l);