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/strings/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/strings/infer_info.cpp')
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index c543de0e0..7242c58bc 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -21,7 +21,7 @@ namespace CVC4 { namespace theory { namespace strings { -InferInfo::InferInfo() : d_sim(nullptr), d_id(InferenceId::UNKNOWN), d_idRev(false) +InferInfo::InferInfo(InferenceId id): TheoryInference(id), d_sim(nullptr), d_idRev(false) { } @@ -61,7 +61,7 @@ Node InferInfo::getPremises() const std::ostream& operator<<(std::ostream& out, const InferInfo& ii) { - out << "(infer " << ii.d_id << " " << ii.d_conc; + out << "(infer " << ii.getId() << " " << ii.d_conc; if (ii.d_idRev) { out << " :rev"; |