blob: 8d65eb2f12fa9b4d122a14940ae71e728f3c6daf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
/********************* */
/*! \file ee_manager.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Utilities for management of equality engines.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__EE_MANAGER__H
#define CVC4__THEORY__EE_MANAGER__H
#include <map>
#include <memory>
#include "theory/ee_setup_info.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
class TheoryEngine;
namespace theory {
/**
* This is (theory-agnostic) information associated with the management of
* an equality engine for a single theory. This information is maintained
* by the manager class below.
*
* Currently, this simply is the equality engine itself, for memory
* management purposes.
*/
struct EeTheoryInfo
{
EeTheoryInfo() : d_usedEe(nullptr) {}
/** Equality engine that is used (if it exists) */
eq::EqualityEngine* d_usedEe;
/** Equality engine allocated specifically for this theory (if it exists) */
std::unique_ptr<eq::EqualityEngine> d_allocEe;
};
/** Virtual base class for equality engine managers */
class EqEngineManager
{
public:
EqEngineManager(TheoryEngine& te);
virtual ~EqEngineManager() {}
/**
* Initialize theories, called during TheoryEngine::finishInit after theory
* objects have been created but prior to their final initialization. This
* sets up equality engines for all theories.
*
* This method is context-independent, and is applied once during
* the lifetime of TheoryEngine (during finishInit).
*/
virtual void initializeTheories() = 0;
/**
* Get the equality engine theory information for theory with the given id.
*/
const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
/**
* Get the core equality engine, which is the equality engine that the
* quantifiers engine should use. This corresponds to the master equality
* engine if eeMode is distributed, or the central equality engine if eeMode
* is central.
*/
virtual eq::EqualityEngine* getCoreEqualityEngine() = 0;
/** Allocate equality engine that is context-dependent on c with info esi */
eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi,
context::Context* c);
protected:
/** Reference to the theory engine */
TheoryEngine& d_te;
/** Information related to the equality engine, per theory. */
std::map<TheoryId, EeTheoryInfo> d_einfo;
};
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__EE_MANAGER__H */
|