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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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.
* ****************************************************************************
*
* Equality engine manager for central equality engine architecture
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__EE_MANAGER_CENTRAL__H
#define CVC5__THEORY__EE_MANAGER_CENTRAL__H
#include <map>
#include <memory>
#include "theory/ee_manager.h"
#include "theory/quantifiers/master_eq_notify.h"
#include "theory/uf/equality_engine.h"
namespace cvc5 {
namespace theory {
/**
* The (central) equality engine manager. This encapsulates an architecture
* in which all applicable theories use a single central equality engine.
*
* This class is not responsible for actually initializing equality engines in
* theories (since this class does not have access to the internals of Theory).
* Instead, it is only responsible for the construction of the equality
* engine objects themselves. TheoryEngine is responsible for querying this
* class during finishInit() to determine the equality engines to pass to each
* theories based on getEeTheoryInfo.
*
* It also may allocate a "master" equality engine, which is intuitively the
* equality engine of the theory of quantifiers. If all theories use the
* central equality engine, then the master equality engine is the same as the
* central equality engine.
*
* The theories that use central equality engine are determined by
* Theory::usesCentralEqualityEngine.
*
* The main idea behind this class is to use a notification class on the
* central equality engine which dispatches *multiple* notifications to the
* theories that use the central equality engine.
*/
class EqEngineManagerCentral : public EqEngineManager
{
public:
EqEngineManagerCentral(TheoryEngine& te,
SharedSolver& shs,
ProofNodeManager* pnm);
~EqEngineManagerCentral();
/**
* Initialize theories. This method allocates unique equality engines
* per theories and connects them to a master equality engine.
*/
void initializeTheories() override;
/** Notify this class that we are building the model. */
void notifyBuildingModel();
private:
/**
* Notify class for central equality engine. This class dispatches
* notifications from the central equality engine to the appropriate
* theory(s).
*/
class CentralNotifyClass : public theory::eq::EqualityEngineNotify
{
public:
CentralNotifyClass(EqEngineManagerCentral& eemc);
bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
bool value) override;
void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
void eqNotifyNewClass(TNode t) override;
void eqNotifyMerge(TNode t1, TNode t2) override;
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
/** Parent */
EqEngineManagerCentral& d_eemc;
/** List of notify classes that need new class notification */
std::vector<eq::EqualityEngineNotify*> d_newClassNotify;
/** List of notify classes that need merge notification */
std::vector<eq::EqualityEngineNotify*> d_mergeNotify;
/** List of notify classes that need disequality notification */
std::vector<eq::EqualityEngineNotify*> d_disequalNotify;
/** The model notify class */
eq::EqualityEngineNotify* d_mNotify;
/** The quantifiers engine */
QuantifiersEngine* d_quantEngine;
};
/** Notification when predicate gets value in central equality engine */
bool eqNotifyTriggerPredicate(TNode predicate, bool value);
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
bool value);
/** Notification when constants are merged in central equality engine */
void eqNotifyConstantTermMerge(TNode t1, TNode t2);
/** The master equality engine notify class */
std::unique_ptr<quantifiers::MasterNotifyClass> d_masterEENotify;
/** The master equality engine. */
eq::EqualityEngine* d_masterEqualityEngine;
/** The master equality engine, if we allocated it */
std::unique_ptr<eq::EqualityEngine> d_masterEqualityEngineAlloc;
/** The central equality engine notify class */
CentralNotifyClass d_centralEENotify;
/** The central equality engine. */
eq::EqualityEngine d_centralEqualityEngine;
/** The proof equality engine for the central equality engine */
std::unique_ptr<eq::ProofEqEngine> d_centralPfee;
/**
* A table of from theory IDs to notify classes.
*/
eq::EqualityEngineNotify* d_theoryNotify[theory::THEORY_LAST];
};
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__EE_MANAGER_CENTRAL__H */
|
