From cbd66977993708a89638beccd625cdbdd32eed7f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 10 Feb 2021 13:42:23 -0600 Subject: Refactor term registration visitors (#5875) This refactors the term registration visitors (PreRegisterVisitor and SharedTermsVisitor), which are responsible for calling Theory::preRegisterTerm and Theory::addSharedTerm. The purpose of this PR is to resolve a subtle bug in the implementation of PreRegisterVisitor (see explanation below), and to improve performance in particular on the Facebook benchmarks (where preregistering terms is currently 25-35% of runtime on certain challenge benchmarks). This PR makes it so that that SharedTermsVisitor now subsumes PreRegisterVisitor and should be run when sharing is enabled only. Previously, we ran both PreRegisterVisitor and SharedTermsVisitor, and moreover the former misclassified when a literal had multiple theories since the d_theories field of PreRegisterVisitor is never reset. This meant we would consider a literal to have multiple theories as soon as we saw any literal that had multipleTheories. After this PR, we run SharedTermsVisitor only which also handles calling preRegisterTerm, since it has the ability to anyways (it computes the same information as PreRegisterVisitor regarding which theories care about a term). The refactoring merges the blocks of code that were copy and pasted in term_registration_visitor.cpp and makes them more optimal, by reducing our calls to Theory::theoryOf. FYI @barrettcw --- src/theory/shared_solver.cpp | 31 ++++++++++++++++++++++--------- 1 file changed, 22 insertions(+), 9 deletions(-) (limited to 'src/theory/shared_solver.cpp') diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp index 01dd37f19..4bee75247 100644 --- a/src/theory/shared_solver.cpp +++ b/src/theory/shared_solver.cpp @@ -30,7 +30,8 @@ SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm) : d_te(te), d_logicInfo(te.getLogicInfo()), d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm), - d_sharedTermsVisitor(d_sharedTerms) + d_preRegistrationVisitor(&te, d_te.getSatContext()), + d_sharedTermsVisitor(&te, d_sharedTerms) { } @@ -39,19 +40,31 @@ bool SharedSolver::needsEqualityEngine(theory::EeSetupInfo& esi) return false; } -void SharedSolver::preRegisterShared(TNode t, bool multipleTheories) +void SharedSolver::preRegister(TNode atom) { - // register it with the equality engine manager if sharing is enabled + // This method uses two different implementations for preregistering terms, + // which depends on whether sharing is enabled. + // If sharing is disabled, we use PreRegisterVisitor, which keeps a global + // SAT-context dependent cache of terms visited. + // If sharing is disabled, we use SharedTermsVisitor which does *not* keep a + // global cache. This is because shared terms must be associated with the + // given atom, and thus it must traverse the set of subterms in each atom. + // See term_registration_visitor.h for more details. if (d_logicInfo.isSharingEnabled()) { - preRegisterSharedInternal(t); + // register it with the shared terms database if sharing is enabled + preRegisterSharedInternal(atom); + // Collect the shared terms in atom, as well as calling preregister on the + // appropriate theories in atom. + // This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly + // multiple times. + NodeVisitor::run(d_sharedTermsVisitor, atom); } - // if multiple theories are present in t - if (multipleTheories) + else { - // Collect the shared terms if there are multiple theories - // This calls Theory::addSharedTerm, possibly multiple times - NodeVisitor::run(d_sharedTermsVisitor, t); + // just use the normal preregister visitor, which calls + // Theory::preRegisterTerm possibly multiple times. + NodeVisitor::run(d_preRegistrationVisitor, atom); } } -- cgit v1.2.3