diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-01-08 11:07:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-08 11:07:32 -0600 |
| commit | a7d214409def441dcf072dd483f31823fd2620ed (patch) | |
| tree | 6d3deba5bec13f6d25ace9c3e4bda9600e045401 /src/theory/strings/infer_info.cpp | |
| parent | 2958e98eff88ce14aefcdeee3c6ec579fcc2bb1d (diff) | |
Rename getAntecedent to getPremises (#5754)
Changes:
renamed d_new_skolem to d_newSkolem
renamed d_ant to d_premises (antecedent is usually used with consequent, and premise is used with conclusion)
Diffstat (limited to 'src/theory/strings/infer_info.cpp')
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index e1cdc5ec3..15d8bbde7 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -131,10 +131,10 @@ bool InferInfo::isFact() const return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty(); } -Node InferInfo::getAntecedent() const +Node InferInfo::getPremises() const { // d_noExplain is a subset of d_ant - return utils::mkAnd(d_ant); + return utils::mkAnd(d_premises); } std::ostream& operator<<(std::ostream& out, const InferInfo& ii) @@ -144,9 +144,9 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii) { out << " :rev"; } - if (!ii.d_ant.empty()) + if (!ii.d_premises.empty()) { - out << " :ant (" << ii.d_ant << ")"; + out << " :ant (" << ii.d_premises << ")"; } if (!ii.d_noExplain.empty()) { |