3c82e43de17b4e555d52e19c164bd7e9a67f8906
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"
31 * This is (theory-agnostic) information associated with the management of
32 * an equality engine for a single theory. This information is maintained
33 * by the manager class below.
35 * Currently, this simply is the equality engine itself, for memory
36 * management purposes.
40 EeTheoryInfo() : d_usedEe(nullptr) {}
41 /** Equality engine that is used (if it exists) */
42 eq::EqualityEngine
* d_usedEe
;
43 /** Equality engine allocated specifically for this theory (if it exists) */
44 std::unique_ptr
<eq::EqualityEngine
> d_allocEe
;
47 /** Virtual base class for equality engine managers */
51 virtual ~EqEngineManager() {}
53 * Finish initialize, called by TheoryEngine::finishInit after theory
54 * objects have been created but prior to their final initialization. This
55 * sets up equality engines for all theories.
57 * This method is context-independent, and is applied once during
58 * the lifetime of TheoryEngine (during finishInit).
60 virtual void initializeTheories() = 0;
62 * Finish initialize, called by TheoryEngine::finishInit after theory
63 * objects have been created but prior to their final initialization. This
64 * sets up equality engines for all theories.
66 * This method is context-independent, and is applied once during
67 * the lifetime of TheoryEngine (during finishInit).
69 virtual void initializeModel(TheoryModel
* m
) = 0;
71 * Get the equality engine theory information for theory with the given id.
73 const EeTheoryInfo
* getEeTheoryInfo(TheoryId tid
) const;
75 * Get the core equality engine, which is the equality engine that the
76 * quantifiers engine should use. This corresponds to the master equality
77 * engine if eeMode is distributed, or the central equality engine if eeMode
80 virtual eq::EqualityEngine
* getCoreEqualityEngine() = 0;
83 /** Information related to the equality engine, per theory. */
84 std::map
<TheoryId
, EeTheoryInfo
> d_einfo
;
90 #endif /* CVC4__THEORY__EE_MANAGER__H */