diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-11 20:00:18 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-11 20:00:18 +0100 |
| commit | f5486884229348516ac26300273e4f5458a74208 (patch) | |
| tree | 8e48bd833c3e55b247adca891ec2081fc9077528 /src/theory/bags/infer_info.cpp | |
| parent | 8fcb59d072b09bfaf8f56334182d425274842461 (diff) | |
Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)
This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
Diffstat (limited to 'src/theory/bags/infer_info.cpp')
| -rw-r--r-- | src/theory/bags/infer_info.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp index 9b5187689..c4e957087 100644 --- a/src/theory/bags/infer_info.cpp +++ b/src/theory/bags/infer_info.cpp @@ -20,7 +20,7 @@ namespace CVC4 { namespace theory { namespace bags { -InferInfo::InferInfo() : d_id(InferenceId::UNKNOWN) {} +InferInfo::InferInfo(InferenceId id) : TheoryInference(id) {} bool InferInfo::process(TheoryInferenceManager* im, bool asLemma) { @@ -77,7 +77,7 @@ bool InferInfo::isFact() const std::ostream& operator<<(std::ostream& out, const InferInfo& ii) { - out << "(infer :id " << ii.d_id << std::endl; + out << "(infer :id " << ii.getId() << std::endl; out << ":conclusion " << ii.d_conclusion << std::endl; if (!ii.d_premises.empty()) { |