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"
34 * This is (theory-agnostic) information associated with the management of
35 * an equality engine for a single theory. This information is maintained
36 * by the manager class below.
38 * Currently, this simply is the equality engine itself, for memory
39 * management purposes.
43 EeTheoryInfo() : d_usedEe(nullptr) {}
44 /** Equality engine that is used (if it exists) */
45 eq::EqualityEngine
* d_usedEe
;
46 /** Equality engine allocated specifically for this theory (if it exists) */
47 std::unique_ptr
<eq::EqualityEngine
> d_allocEe
;
50 /** Virtual base class for equality engine managers */
54 EqEngineManager(TheoryEngine
& te
);
55 virtual ~EqEngineManager() {}
57 * Initialize theories, called during TheoryEngine::finishInit after theory
58 * objects have been created but prior to their final initialization. This
59 * sets up equality engines for all theories.
61 * This method is context-independent, and is applied once during
62 * the lifetime of TheoryEngine (during finishInit).
64 virtual void initializeTheories() = 0;
66 * Get the equality engine theory information for theory with the given id.
68 const EeTheoryInfo
* getEeTheoryInfo(TheoryId tid
) const;
70 * Get the core equality engine, which is the equality engine that the
71 * quantifiers engine should use. This corresponds to the master equality
72 * engine if eeMode is distributed, or the central equality engine if eeMode
75 virtual eq::EqualityEngine
* getCoreEqualityEngine() = 0;
77 /** Allocate equality engine that is context-dependent on c with info esi */
78 eq::EqualityEngine
* allocateEqualityEngine(EeSetupInfo
& esi
,
82 /** Reference to the theory engine */
84 /** Information related to the equality engine, per theory. */
85 std::map
<TheoryId
, EeTheoryInfo
> d_einfo
;
91 #endif /* CVC4__THEORY__EE_MANAGER__H */