blob: 7f04ccd7529e9332c378396273fc6f9881b05592 (
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
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
|
/******************************************************************************
* 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 interface for theory combination.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__COMBINATION_ENGINE__H
#define CVC5__THEORY__COMBINATION_ENGINE__H
#include <vector>
#include <memory>
#include "theory/ee_manager.h"
#include "theory/valuation.h"
namespace cvc5 {
class TheoryEngine;
class Env;
class EagerProofGenerator;
namespace theory {
class ModelManager;
class SharedSolver;
/**
* Manager for doing theory combination. This class is responsible for:
* (1) Initializing the various components of theory combination (equality
* engine manager, model manager, shared solver) based on the equality engine
* mode, and
* (2) Implementing the main combination method (combineTheories).
*/
class CombinationEngine
{
public:
CombinationEngine(TheoryEngine& te,
Env& env,
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm);
virtual ~CombinationEngine();
/** Finish initialization */
void finishInit();
/** Get equality engine theory information for theory with identifier tid. */
const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
//-------------------------- model
/**
* Reset the model maintained by this class. This resets all local information
* that is unique to each check.
*/
void resetModel();
/**
* Build the model maintained by this class.
*
* @return true if model building was successful.
*/
virtual bool buildModel() = 0;
/**
* Post process the model maintained by this class. This is called after
* a successful call to buildModel. This does any theory-specific
* postprocessing of the model.
*
* @param incomplete Whether we are answering "unknown" instead of "sat".
*/
void postProcessModel(bool incomplete);
/**
* Get the model object maintained by this class.
*/
TheoryModel* getModel();
//-------------------------- end model
/**
* Get the shared solver, which is the active component of theory combination
* that TheoryEngine interacts with prior to calling combineTheories.
*/
SharedSolver* getSharedSolver();
/**
* Called at the beginning of full effort
*/
virtual void resetRound();
/**
* Combine theories, called after FULL effort passes with no lemmas
* and before LAST_CALL effort is run. This adds necessary lemmas for
* theory combination (e.g. splitting lemmas) to the parent TheoryEngine.
*/
virtual void combineTheories() = 0;
protected:
/** Is proof enabled? */
bool isProofEnabled() const;
/**
* Get model equality engine notify. Return the notification object for
* who listens to the model's equality engine (if any).
*/
virtual eq::EqualityEngineNotify* getModelEqualityEngineNotify();
/** Reference to the theory engine */
TheoryEngine& d_te;
/** Reference to the environment */
Env& d_env;
/** Valuation for the engine */
Valuation d_valuation;
/** The proof node manager */
ProofNodeManager* d_pnm;
/** Logic info of theory engine (cached) */
const LogicInfo& d_logicInfo;
/** List of parametric theories of theory engine */
const std::vector<Theory*> d_paraTheories;
/**
* The equality engine manager we are using. This class is responsible for
* configuring equality engines for each theory.
*/
std::unique_ptr<EqEngineManager> d_eemanager;
/**
* The model manager we are using. This class is responsible for building the
* model.
*/
std::unique_ptr<ModelManager> d_mmanager;
/**
* The shared solver. This class is responsible for performing combination
* tasks (e.g. preregistration) during solving.
*/
std::unique_ptr<SharedSolver> d_sharedSolver;
/**
* An eager proof generator, if proofs are enabled. This proof generator is
* responsible for proofs of splitting lemmas generated in combineTheories.
*/
std::unique_ptr<EagerProofGenerator> d_cmbsPg;
};
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__COMBINATION_DISTRIBUTED__H */
|
