1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Utilities for management of equality engines.
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__EE_MANAGER__H
18 #define CVC4__THEORY__EE_MANAGER__H
23 #include "theory/ee_setup_info.h"
24 #include "theory/theory.h"
25 #include "theory/uf/equality_engine.h"
36 * This is (theory-agnostic) information associated with the management of
37 * an equality engine for a single theory. This information is maintained
38 * by the manager class below.
40 * Currently, this simply is the equality engine itself, for memory
41 * management purposes.
45 EeTheoryInfo() : d_usedEe(nullptr) {}
46 /** Equality engine that is used (if it exists) */
47 eq::EqualityEngine
* d_usedEe
;
48 /** Equality engine allocated specifically for this theory (if it exists) */
49 std::unique_ptr
<eq::EqualityEngine
> d_allocEe
;
52 /** Virtual base class for equality engine managers */
57 * @param te Reference to the theory engine
58 * @param sharedSolver The shared solver that is being used in combination
59 * with this equality engine manager
61 EqEngineManager(TheoryEngine
& te
, SharedSolver
& shs
);
62 virtual ~EqEngineManager() {}
64 * Initialize theories, called during TheoryEngine::finishInit after theory
65 * objects have been created but prior to their final initialization. This
66 * sets up equality engines for all theories.
68 * This method is context-independent, and is applied once during
69 * the lifetime of TheoryEngine (during finishInit).
71 virtual void initializeTheories() = 0;
73 * Get the equality engine theory information for theory with the given id.
75 const EeTheoryInfo
* getEeTheoryInfo(TheoryId tid
) const;
77 * Get the core equality engine, which is the equality engine that the
78 * quantifiers engine should use. This corresponds to the master equality
79 * engine if eeMode is distributed, or the central equality engine if eeMode
82 virtual eq::EqualityEngine
* getCoreEqualityEngine() = 0;
84 /** Allocate equality engine that is context-dependent on c with info esi */
85 eq::EqualityEngine
* allocateEqualityEngine(EeSetupInfo
& esi
,
89 /** Reference to the theory engine */
91 /** Reference to the shared solver */
92 SharedSolver
& d_sharedSolver
;
93 /** Information related to the equality engine, per theory. */
94 std::map
<TheoryId
, EeTheoryInfo
> d_einfo
;
100 #endif /* CVC4__THEORY__EE_MANAGER__H */