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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Gereon Kremer
*
* 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.
* ****************************************************************************
*
* Abstract management of models for TheoryEngine.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__MODEL_MANAGER__H
#define CVC5__THEORY__MODEL_MANAGER__H
#include <memory>
#include "theory/ee_manager.h"
#include "theory/logic_info.h"
namespace cvc5 {
class TheoryEngine;
namespace theory {
class TheoryEngineModelBuilder;
class TheoryModel;
/**
* A base class for managing models. Its main feature is to implement a
* buildModel command. Overall, its behavior is specific to the kind of equality
* engine management mode we are using. In particular, the prepare model
* method is a manager-specific way for setting up the equality engine of the
* model in preparation for model building.
*/
class ModelManager
{
public:
ModelManager(TheoryEngine& te, EqEngineManager& eem);
virtual ~ModelManager();
/**
* Finish initializing this class, which allocates the model, the model
* builder as well as the equality engine of the model. The equality engine
* to use is determined by the virtual method initializeModelEqEngine.
*
* @param notify The object that wants to be notified for callbacks occurring
*/
void finishInit(eq::EqualityEngineNotify* notify);
/** Reset model, called during full effort check before the model is built */
void resetModel();
/**
* Build the model. If we have yet to build the model on this round, this
* method calls the (manager-specific) prepareModel method and then calls
* finishBuildModel.
*
* @return true if model building was successful.
*/
bool buildModel();
/**
* Have we called buildModel this round? Note this returns true whether or
* not the model building was successful.
*/
bool isModelBuilt() const;
/**
* Post process model, which is used as a way of each theory adding additional
* information to the model after successfully building a model.
*/
void postProcessModel(bool incomplete);
/** Get a pointer to model object maintained by this class. */
TheoryModel* getModel();
//------------------------ finer grained control over model building
/**
* Prepare model, which is the manager-specific method for setting up the
* equality engine of the model. This should assert all relevant information
* about the model into the equality engine of d_model.
*
* @return true if we are in conflict (i.e. the equality engine of the model
* equality engine is inconsistent).
*/
virtual bool prepareModel() = 0;
/**
* Finish build model, which calls the theory model builder to assign values
* to all equivalence classes. This should be run after prepareModel.
*
* @return true if model building was successful.
*/
virtual bool finishBuildModel() const = 0;
//------------------------ end finer grained control over model building
protected:
/**
* Initialize model equality engine. This is called at the end of finish
* init, after we have created a model object but before we have assigned it
* an equality engine.
*/
virtual void initializeModelEqEngine(eq::EqualityEngineNotify* notify) = 0;
/**
* Collect model Boolean variables.
* This asserts the values of all boolean variables to the equality engine of
* the model, based on their value in the prop engine.
*
* @return true if we are in conflict.
*/
bool collectModelBooleanVariables();
/**
* Collect asserted terms for theory with the given identifier, add to
* termSet.
*
* @param tid The theory whose assertions we are collecting
* @param termSet The set to add terms to
* @param includeShared Whether to include the shared terms of the theory
*/
void collectAssertedTerms(TheoryId tid,
std::set<Node>& termSet,
bool includeShared = true) const;
/**
* Helper function for collectAssertedTerms, adds all subterms
* belonging to theory tid to termSet.
*/
void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const;
/** Reference to the theory engine */
TheoryEngine& d_te;
/** Logic info of theory engine (cached) */
const LogicInfo& d_logicInfo;
/** The equality engine manager */
EqEngineManager& d_eem;
/**
* A dummy context for the model equality engine, so we can clear it
* independently of search context.
*/
context::Context d_modelEeContext;
/** Pointer to the equality engine of the model */
eq::EqualityEngine* d_modelEqualityEngine;
/** The equality engine of the model, if we allocated it */
std::unique_ptr<eq::EqualityEngine> d_modelEqualityEngineAlloc;
/** The model object we have allocated (if one exists) */
std::unique_ptr<TheoryModel> d_model;
/** The model builder object we are using */
TheoryEngineModelBuilder* d_modelBuilder;
/** The model builder object we have allocated (if one exists) */
std::unique_ptr<TheoryEngineModelBuilder> d_alocModelBuilder;
/** whether we have tried to build this model in the current context */
bool d_modelBuilt;
/** whether this model has been built successfully */
bool d_modelBuiltSuccess;
};
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__MODEL_MANAGER__H */
|
