aboutsummaryrefslogtreecommitdiff
path: root/include/atp/core/clause.h
diff options
context:
space:
mode:
Diffstat (limited to 'include/atp/core/clause.h')
-rw-r--r--include/atp/core/clause.h16
1 files changed, 8 insertions, 8 deletions
diff --git a/include/atp/core/clause.h b/include/atp/core/clause.h
index 7e0cbff..6387adf 100644
--- a/include/atp/core/clause.h
+++ b/include/atp/core/clause.h
@@ -33,20 +33,20 @@ namespace atp {
/// A clause: a disjunction of literals plus provenance for proof reconstruction.
struct Clause {
- ClauseId id = kInvalidId;
- std::vector<Literal> literals;
+ ClauseId id_ = kInvalidId;
+ std::vector<Literal> literals_;
// Provenance (for proof trace)
- InferenceRule rule = InferenceRule::kInput;
- ClauseId parent1 = kInvalidId;
- ClauseId parent2 = kInvalidId;
- uint16_t depth = 0; ///< Derivation depth (for BFS scheduling)
+ InferenceRule rule_ = InferenceRule::kInput;
+ ClauseId parent1_ = kInvalidId;
+ ClauseId parent2_ = kInvalidId;
+ uint16_t depth_ = 0; ///< Derivation depth (for BFS scheduling)
/// True if the clause has no literals (contradiction).
- [[nodiscard]] bool isEmpty() const { return literals.empty(); }
+ [[nodiscard]] bool isEmpty() const { return literals_.empty(); }
/// Number of literals.
- [[nodiscard]] size_t size() const { return literals.size(); }
+ [[nodiscard]] size_t size() const { return literals_.size(); }
};
} // namespace atp