diff options
| author | Richard Qin <richard.qin.x@gmail.com> | 2026-04-07 03:59:58 +0800 |
|---|---|---|
| committer | Richard Qin <richard.qin.x@gmail.com> | 2026-04-07 03:59:58 +0800 |
| commit | 5ab3efd522cf0221481684b5bbc9c2ac6bfc9919 (patch) | |
| tree | 9c521dedd2bc49bdbac642a0640dd048b6d8e4a1 /src/simplify/tautology.cc | |
| parent | bf4f464cec8b6515d9e5131d43847ef9b2fd21d1 (diff) | |
| download | ratp-5ab3efd522cf0221481684b5bbc9c2ac6bfc9919.tar.gz ratp-5ab3efd522cf0221481684b5bbc9c2ac6bfc9919.tar.xz | |
refactor: rename struct members to follow trailing underscore naming convention across core, search, and frontend components
Diffstat (limited to 'src/simplify/tautology.cc')
| -rw-r--r-- | src/simplify/tautology.cc | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/simplify/tautology.cc b/src/simplify/tautology.cc index 70bdced..e35d874 100644 --- a/src/simplify/tautology.cc +++ b/src/simplify/tautology.cc @@ -18,14 +18,16 @@ #include "atp/simplify/tautology.h" +#include "atp/core/clause.h" + #include <cstddef> namespace atp { bool isTautology(const Clause& clause) { for (size_t i = 0; i < clause.size(); ++i) { for (size_t j = i + 1; j < clause.size(); ++j) { - if (clause.literals[i].atom == clause.literals[j].atom && - clause.literals[i].is_positive != clause.literals[j].is_positive) { + if (clause.literals_[i].atom_ == clause.literals_[j].atom_ && + clause.literals_[i].is_positive_ != clause.literals_[j].is_positive_) { return true; } } |
