aboutsummaryrefslogtreecommitdiff
path: root/include/atp/normalize/formula.h
diff options
context:
space:
mode:
authorRichard Qin <richard.qin.x@gmail.com>2026-04-07 03:59:58 +0800
committerRichard Qin <richard.qin.x@gmail.com>2026-04-07 03:59:58 +0800
commit5ab3efd522cf0221481684b5bbc9c2ac6bfc9919 (patch)
tree9c521dedd2bc49bdbac642a0640dd048b6d8e4a1 /include/atp/normalize/formula.h
parentbf4f464cec8b6515d9e5131d43847ef9b2fd21d1 (diff)
downloadratp-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 'include/atp/normalize/formula.h')
-rw-r--r--include/atp/normalize/formula.h8
1 files changed, 4 insertions, 4 deletions
diff --git a/include/atp/normalize/formula.h b/include/atp/normalize/formula.h
index 1bcc021..5ee9b94 100644
--- a/include/atp/normalize/formula.h
+++ b/include/atp/normalize/formula.h
@@ -51,18 +51,18 @@ enum class FormulaKind : uint8_t {
/// All identifiers are interned: atoms as TermIds, quantifier variables as
/// SymbolIds. No raw strings survive past the parser.
struct Formula {
- FormulaKind kind;
+ FormulaKind kind_;
/// For kAtom / kEquality: the predicate/equality term, already interned.
- TermId atom = kInvalidId;
+ TermId atom_ = kInvalidId;
/// For kForall / kExists: the bound variable, as an interned SymbolId.
/// Using SymbolId (not string) so the clausifier can map bound variables
/// back to term-bank variables without string lookups.
- SymbolId bound_var = kInvalidId;
+ SymbolId bound_var_ = kInvalidId;
/// Sub-formulas (1 for Not/Quantifiers, 2 for binary connectives).
- std::vector<std::unique_ptr<Formula>> children;
+ std::vector<std::unique_ptr<Formula>> children_;
// ── Factory methods ──