diff --git a/potassco/aspif.h b/potassco/aspif.h
index ee7067c..669be3c 100644
--- a/potassco/aspif.h
+++ b/potassco/aspif.h
@@ -34,13 +34,15 @@ namespace Potassco {
  */
 int readAspif(std::istream& prg, AbstractProgram& out);
 
-enum class Theory_t;
+//! Supported aspif theory statements.
+enum class TheoryType : uint32_t { number = 0, symbol = 1, compound = 2, element = 4, atom = 5, atom_with_guard = 6 };
+POTASSCO_SET_DEFAULT_ENUM_MAX(TheoryType::atom_with_guard);
 
 //! Class for parsing logic programs in asp intermediate format.
 class AspifInput : public ProgramReader {
 public:
     //! Creates a new parser object that calls @c out on each parsed element.
-    AspifInput(AbstractProgram& out);
+    explicit AspifInput(AbstractProgram& out);
 
 protected:
     //! Checks whether stream starts with aspif header.
@@ -51,11 +53,6 @@ class AspifInput : public ProgramReader {
      * output object before/after parsing the current step.
      */
     bool doParse() override;
-    //! Attempts to parse a theory directive of type @c t.
-    /*!
-     * \see Potassco::Theory_t
-     */
-    virtual void matchTheory(Theory_t t);
 
 private:
     struct Extra;
@@ -64,6 +61,7 @@ class AspifInput : public ProgramReader {
     void matchWLits(bool positive);
     void matchString();
     void matchIds();
+    void matchTheory(TheoryType t);
 
     AbstractProgram& out_;
     Extra*           data_;
@@ -77,7 +75,7 @@ class AspifInput : public ProgramReader {
 class AspifOutput : public AbstractProgram {
 public:
     //! Creates a new object and associates it with the given output stream.
-    AspifOutput(std::ostream& os);
+    explicit AspifOutput(std::ostream& os);
     AspifOutput(const AspifOutput&)            = delete;
     AspifOutput& operator=(const AspifOutput&) = delete;
 
@@ -86,15 +84,15 @@ class AspifOutput : public AbstractProgram {
     //! Prepares the object for a new program step.
     void beginStep() override;
     //! Writes an aspif rule directive.
-    void rule(Head_t ht, const AtomSpan& head, const LitSpan& body) override;
+    void rule(HeadType ht, const AtomSpan& head, const LitSpan& body) override;
     //! Writes an aspif rule directive.
-    void rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits) override;
+    void rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits) override;
     //! Writes an aspif minimize directive.
     void minimize(Weight_t prio, const WeightLitSpan& lits) override;
     //! Writes an aspif output directive.
     void output(const std::string_view& str, const LitSpan& cond) override;
     //! Writes an aspif external directive.
-    void external(Atom_t a, Value_t v) override;
+    void external(Atom_t a, TruthValue v) override;
     //! Writes an aspif assumption directive.
     void assume(const LitSpan& lits) override;
     //! Writes an aspif projection directive.
@@ -102,7 +100,7 @@ class AspifOutput : public AbstractProgram {
     //! Writes an aspif edge directive.
     void acycEdge(int s, int t, const LitSpan& condition) override;
     //! Writes an aspif heuristic directive.
-    void heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& condition) override;
+    void heuristic(Atom_t a, DomModifier t, int bias, unsigned prio, const LitSpan& condition) override;
 
     //! Writes an aspif theory number term.
     void theoryTerm(Id_t termId, int number) override;
@@ -121,7 +119,7 @@ class AspifOutput : public AbstractProgram {
 
 protected:
     //! Starts writing an aspif directive.
-    AspifOutput& startDir(Directive_t r);
+    AspifOutput& startDir(AspifType r);
     //! Writes @c x.
     template <typename T>
     AspifOutput& add(T x);
diff --git a/potassco/aspif_text.h b/potassco/aspif_text.h
index 7932181..7b99e09 100644
--- a/potassco/aspif_text.h
+++ b/potassco/aspif_text.h
@@ -35,7 +35,7 @@ namespace Potassco {
 class AspifTextInput : public ProgramReader {
 public:
     //! Creates a new object and associates it with the given output if any.
-    AspifTextInput(AbstractProgram* out);
+    explicit AspifTextInput(AbstractProgram* out);
     //! Sets the program to which parsed elements should be output.
     void setOutput(AbstractProgram& out);
 
@@ -52,22 +52,22 @@ class AspifTextInput : public ProgramReader {
     void parseStatements();
 
 private:
-    bool        matchDirective();
-    void        matchRule(char peek);
-    void        matchAtoms(std::string_view sv);
-    void        matchLits();
-    void        matchCondition();
-    void        matchAgg();
-    void        matchDelim(char);
-    bool        matchOpt(std::string_view ts);
-    Atom_t      matchId();
-    Lit_t       matchLit();
-    int         matchInt();
-    Heuristic_t matchHeuMod();
-    void        matchTerm();
-    void        matchAtomArg();
-    void        matchStr();
-    void        push(char c);
+    bool   matchDirective();
+    void   matchRule(char peek);
+    void   matchAtoms(std::string_view sv);
+    void   matchLits();
+    void   matchCondition();
+    void   matchAgg();
+    void   matchDelim(char);
+    bool   matchOpt(std::string_view ts);
+    Atom_t matchId();
+    Lit_t  matchLit();
+    int    matchInt();
+    auto   matchHeuMod() -> DomModifier;
+    void   matchTerm();
+    void   matchAtomArg();
+    void   matchStr();
+    void   push(char c);
     struct Data;
     AbstractProgram* out_;
     Data*            data_;
@@ -78,23 +78,23 @@ class AspifTextInput : public ProgramReader {
  * Writes a logic program in human-readable text format.
  * \ingroup WriteType
  */
-class AspifTextOutput : public Potassco::AbstractProgram {
+class AspifTextOutput : public AbstractProgram {
 public:
-    AspifTextOutput(std::ostream& os);
+    explicit AspifTextOutput(std::ostream& os);
     ~AspifTextOutput() override;
     AspifTextOutput(AspifTextOutput&&) = delete;
 
     void initProgram(bool incremental) override;
     void beginStep() override;
-    void rule(Head_t ht, const AtomSpan& head, const LitSpan& body) override;
-    void rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits) override;
+    void rule(HeadType ht, const AtomSpan& head, const LitSpan& body) override;
+    void rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits) override;
     void minimize(Weight_t prio, const WeightLitSpan& lits) override;
     void output(const std::string_view& str, const LitSpan& cond) override;
-    void external(Atom_t a, Value_t v) override;
+    void external(Atom_t a, TruthValue v) override;
     void assume(const LitSpan& lits) override;
     void project(const AtomSpan& atoms) override;
     void acycEdge(int s, int t, const LitSpan& condition) override;
-    void heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& condition) override;
+    void heuristic(Atom_t a, DomModifier t, int bias, unsigned prio, const LitSpan& condition) override;
 
     void theoryTerm(Id_t termId, int number) override;
     void theoryTerm(Id_t termId, const std::string_view& name) override;
diff --git a/potassco/basic_types.h b/potassco/basic_types.h
index e690501..0467688 100644
--- a/potassco/basic_types.h
+++ b/potassco/basic_types.h
@@ -76,7 +76,7 @@ constexpr auto id_max = static_cast<Id_t>(-1);
 //! Atom ids are positive integers in the range [atom_min;atom_max].
 using Atom_t = uint32_t;
 //! Minimum value for atom ids (must not be 0).
-constexpr auto atom_min = static_cast<Atom_t>(1);
+constexpr auto atom_min = static_cast<Atom_t>(1u);
 //! Maximum value for atom ids.
 constexpr auto atom_max = static_cast<Atom_t>(((1u) << 31) - 1);
 //! Literals are signed atoms.
@@ -84,24 +84,24 @@ using Lit_t = int32_t;
 //! (Literal) weights are integers.
 using Weight_t = int32_t;
 //! A literal with an associated weight.
-struct WeightLit_t {
+struct WeightLit {
     Lit_t    lit;    //!< Literal.
     Weight_t weight; //!< Associated weight.
 
-    friend constexpr bool operator==(const WeightLit_t& lhs, const WeightLit_t& rhs) noexcept  = default;
-    friend constexpr auto operator<=>(const WeightLit_t& lhs, const WeightLit_t& rhs) noexcept = default;
-    friend constexpr auto operator==(const WeightLit_t& lhs, Lit_t rhs) noexcept {
+    friend constexpr bool operator==(const WeightLit& lhs, const WeightLit& rhs) noexcept  = default;
+    friend constexpr auto operator<=>(const WeightLit& lhs, const WeightLit& rhs) noexcept = default;
+    friend constexpr auto operator==(const WeightLit& lhs, Lit_t rhs) noexcept {
         return lhs.lit == rhs && lhs.weight == 1;
     }
-    friend constexpr auto operator<=>(const WeightLit_t& lhs, Lit_t rhs) noexcept {
-        return lhs <=> WeightLit_t{.lit = rhs, .weight = 1};
+    friend constexpr auto operator<=>(const WeightLit& lhs, Lit_t rhs) noexcept {
+        return lhs <=> WeightLit{.lit = rhs, .weight = 1};
     }
 };
 
 using IdSpan        = std::span<const Id_t>;
 using AtomSpan      = std::span<const Atom_t>;
 using LitSpan       = std::span<const Lit_t>;
-using WeightLitSpan = std::span<const WeightLit_t>;
+using WeightLitSpan = std::span<const WeightLit>;
 //! Convert a single lvalue into a span with one element.
 template <typename T>
 requires(std::is_lvalue_reference_v<T>)
@@ -110,33 +110,33 @@ constexpr auto toSpan(T&& x) -> std::span<std::remove_reference_t<T>> {
 }
 
 //! Supported rule head types.
-enum class Head_t : unsigned { disjunctive = 0, choice = 1 };
-POTASSCO_SET_DEFAULT_ENUM_MAX(Head_t::choice);
+enum class HeadType : unsigned { disjunctive = 0, choice = 1 };
+POTASSCO_SET_DEFAULT_ENUM_MAX(HeadType::choice);
 
 //! Supported rule body types.
-enum class Body_t : unsigned { normal = 0, sum = 1, count = 2 };
-POTASSCO_SET_DEFAULT_ENUM_MAX(Body_t::count);
+enum class BodyType : unsigned { normal = 0, sum = 1, count = 2 };
+POTASSCO_SET_DEFAULT_ENUM_MAX(BodyType::count);
 
-//! Type representing an external value.
-enum class Value_t : unsigned { free = 0, true_ = 1, false_ = 2, release = 3 };
-[[maybe_unused]] consteval auto enable_meta(std::type_identity<Value_t>) {
-    using enum Value_t;
+//! Type representing a truth or external value.
+enum class TruthValue : unsigned { free = 0, true_ = 1, false_ = 2, release = 3 };
+[[maybe_unused]] consteval auto enable_meta(std::type_identity<TruthValue>) {
+    using enum TruthValue;
     using namespace std::literals;
     return EnumEntries(free, "free"sv, true_, "true"sv, false_, "false"sv, release, "release"sv);
 }
 
 //! Supported modifications for domain heuristic.
-enum class Heuristic_t : unsigned { level = 0, sign = 1, factor = 2, init = 3, true_ = 4, false_ = 5 };
-[[maybe_unused]] consteval auto enable_ops(std::type_identity<Heuristic_t>) -> CmpOps;
-[[maybe_unused]] consteval auto enable_meta(std::type_identity<Heuristic_t>) {
-    using enum Heuristic_t;
+enum class DomModifier : unsigned { level = 0, sign = 1, factor = 2, init = 3, true_ = 4, false_ = 5 };
+[[maybe_unused]] consteval auto enable_ops(std::type_identity<DomModifier>) -> CmpOps;
+[[maybe_unused]] consteval auto enable_meta(std::type_identity<DomModifier>) {
+    using enum DomModifier;
     using namespace std::literals;
     return EnumEntries(level, "level"sv, sign, "sign"sv, factor, "factor"sv, init, "init"sv, true_, "true"sv, false_,
                        "false"sv);
 }
 
-//! Supported aspif directives.
-enum class Directive_t : unsigned {
+//! Supported aspif statements.
+enum class AspifType : unsigned {
     end       = 0,
     rule      = 1,
     minimize  = 2,
@@ -149,7 +149,7 @@ enum class Directive_t : unsigned {
     theory    = 9,
     comment   = 10
 };
-POTASSCO_SET_DEFAULT_ENUM_MAX(Directive_t::comment);
+POTASSCO_SET_DEFAULT_ENUM_MAX(AspifType::comment);
 
 //! Basic callback interface for constructing a logic program.
 class AbstractProgram {
@@ -161,9 +161,9 @@ class AbstractProgram {
     virtual void beginStep();
 
     //! Add the given rule to the program.
-    virtual void rule(Head_t ht, const AtomSpan& head, const LitSpan& body) = 0;
+    virtual void rule(HeadType ht, const AtomSpan& head, const LitSpan& body) = 0;
     //! Add the given sum rule to the program.
-    virtual void rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) = 0;
+    virtual void rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) = 0;
     //! Add the given minimize statement to the program.
     virtual void minimize(Weight_t prio, const WeightLitSpan& lits) = 0;
 
@@ -178,13 +178,13 @@ class AbstractProgram {
     virtual void project(const AtomSpan& atoms);
     //! Output @c str whenever condition is true in a stable model.
     virtual void output(const std::string_view& str, const LitSpan& condition);
-    //! If `v` is not equal to `Value_t::release`, mark `a` as external and assume value `v`. Otherwise, treat `a` as
+    //! If `v` is not equal to `TruthValue::release`, mark `a` as external and assume value `v`. Otherwise, treat `a` as
     //! regular atom.
-    virtual void external(Atom_t a, Value_t v);
+    virtual void external(Atom_t a, TruthValue v);
     //! Assume the given literals to true during solving.
     virtual void assume(const LitSpan& lits);
     //! Apply the given heuristic modification to atom @c a whenever condition is true.
-    virtual void heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& condition);
+    virtual void heuristic(Atom_t a, DomModifier t, int bias, unsigned prio, const LitSpan& condition);
     //! Assume an edge between @c s and @c t whenever condition is true.
     virtual void acycEdge(int s, int t, const LitSpan& condition);
     //@}
@@ -230,13 +230,13 @@ constexpr Atom_t atom(Atom_t atom) { return atom; }
 //! Returns the atom of the given literal.
 constexpr Atom_t atom(Lit_t lit) { return static_cast<Atom_t>(lit >= 0 ? lit : -lit); }
 //! Returns the atom of the given weight literal.
-constexpr Atom_t atom(const WeightLit_t& w) { return atom(w.lit); }
+constexpr Atom_t atom(const WeightLit& w) { return atom(w.lit); }
 //! Returns the positive literal of the given atom.
 constexpr Lit_t lit(Atom_t atom) { return static_cast<Lit_t>(atom); }
 //! Identity function for literals.
 constexpr Lit_t lit(Lit_t lit) { return lit; }
 //! Returns the literal of the given weight literal.
-constexpr Lit_t lit(const WeightLit_t& w) { return w.lit; }
+constexpr Lit_t lit(const WeightLit& w) { return w.lit; }
 //! Returns the negative literal of the given atom.
 constexpr Lit_t neg(Atom_t a) { return -lit(a); }
 //! Returns the complement of the given literal.
@@ -246,7 +246,7 @@ constexpr Weight_t weight(Atom_t) { return 1; }
 //! Returns the weight of the given literal, which is always 1.
 constexpr Weight_t weight(Lit_t) { return 1; }
 //! Returns the weight of the given weight literal.
-constexpr Weight_t weight(const WeightLit_t& w) { return w.weight; }
+constexpr Weight_t weight(const WeightLit& w) { return w.weight; }
 
 ///@}
 
@@ -326,9 +326,9 @@ class Bitset {
     static constexpr auto max_count = sizeof(T) * CHAR_BIT;
 
     //! Creates an empty set, i.e. all bits are zero.
-    constexpr Bitset() noexcept : set_{} {}
+    constexpr Bitset() noexcept = default;
     //! Creates a set with the given elements, i.e. bits at the given positions are set.
-    constexpr Bitset(std::initializer_list<ElemType> elems) : set_{} {
+    constexpr Bitset(std::initializer_list<ElemType> elems) {
         for (StorageType zero{}; auto e : elems) { set_ |= Potassco::set_bit(zero, +e); }
     }
     //! Constructs a bitset with all bits in `r` set.
@@ -353,13 +353,12 @@ class Bitset {
 
 private:
     constexpr explicit Bitset(StorageType r) : set_(r) {}
-    StorageType set_;
+    StorageType set_{0};
 };
 static_assert(Bitset<uint32_t>::max_count == 32);
 static_assert(Bitset<uint32_t>{}.rep() == 0u);
 static_assert(Bitset<uint32_t>::fromRep(8u).contains(3));
 static_assert(Bitset<uint32_t>::fromRep(15u).count() == 4u);
-static_assert(Bitset<uint32_t>{1, 2, 3}.rep() == 14u);
 
 class DynamicBitset {
 public:
@@ -413,7 +412,7 @@ class RuleBuilder;
  * a pointer referencing a buffer internal to the string, making relocation non-trivial.
  * In contrast, this class uses an SSO implementation that is more similar to the one from libc++.
  */
-class ConstString {
+class ConstString final {
 public:
     using trivially_relocatable = std::true_type; // NOLINT
     //! Supported creation modes.
diff --git a/potassco/bits.h b/potassco/bits.h
index 4cac9c0..b846a29 100644
--- a/potassco/bits.h
+++ b/potassco/bits.h
@@ -83,7 +83,7 @@ static_assert(clear_bit(7u, 0) == 6u && clear_bit(8u, 3) == 0u);
 //! Effect: x = clear_bit(x, n)
 template <std::unsigned_integral T>
 POTASSCO_FORCE_INLINE constexpr T& store_clear_bit(T& x, unsigned n) noexcept {
-    return (x &= ~nth_bit<T>(n));
+    return x &= ~nth_bit<T>(n);
 }
 //! Returns a copy of @c x with bit @c n toggled.
 template <std::unsigned_integral T>
@@ -94,7 +94,7 @@ static_assert(toggle_bit(6u, 0) == 7u && toggle_bit(7u, 1) == 5u);
 //! Effect: x = toggle_bit(x, n)
 template <std::unsigned_integral T>
 POTASSCO_FORCE_INLINE constexpr T& store_toggle_bit(T& x, unsigned n) noexcept {
-    return (x ^= nth_bit<T>(n));
+    return x ^= nth_bit<T>(n);
 }
 ///@}
 /*!
@@ -122,7 +122,7 @@ static_assert(set_mask(6u, 3u) == 7u && set_mask(1024u, 7u) == 1031u);
 //! Effect: x = set_mask(x, m)
 template <std::unsigned_integral T>
 POTASSCO_FORCE_INLINE constexpr T& store_set_mask(T& x, std::type_identity_t<T> m) noexcept {
-    return (x |= m);
+    return x |= m;
 }
 //! Returns a copy of @c x with all set bits in the mask @c m cleared.
 template <std::unsigned_integral T>
@@ -133,7 +133,7 @@ static_assert(clear_mask(7u, 3u) == 4u && clear_mask(19u, 17u) == 2u);
 //! Effect: x = clear_mask(x, m)
 template <std::unsigned_integral T>
 POTASSCO_FORCE_INLINE constexpr T& store_clear_mask(T& x, std::type_identity_t<T> m) noexcept {
-    return (x &= ~m);
+    return x &= ~m;
 }
 //! Returns a copy of @c x with all bits in the mask @c m toggled.
 template <std::unsigned_integral T>
@@ -143,7 +143,7 @@ template <std::unsigned_integral T>
 //! Effect: x = toggle_mask(x, m)
 template <std::unsigned_integral T>
 POTASSCO_FORCE_INLINE constexpr T& store_toggle_mask(T& x, std::type_identity_t<T> m) noexcept {
-    return (x ^= m);
+    return x ^= m;
 }
 ///@}
 //! Returns a value of T with first @c numBits set.
@@ -158,7 +158,7 @@ template <std::unsigned_integral T>
 [[nodiscard]] POTASSCO_FORCE_INLINE constexpr T right_most_bit(T x) noexcept {
     POTASSCO_WARNING_PUSH()
     POTASSCO_WARNING_IGNORE_MSVC(4146) // unary minus operator applied to unsigned type, result still unsigned
-    return x & (-x);
+    return x & -x;
     POTASSCO_WARNING_POP()
 }
 static_assert(right_most_bit(0b00000000u) == 0b00000000u && right_most_bit(0b00010100u) == 0b00000100u);
diff --git a/potassco/clingo.h b/potassco/clingo.h
index 5ff5dee..32ee9b5 100644
--- a/potassco/clingo.h
+++ b/potassco/clingo.h
@@ -34,16 +34,16 @@ namespace Potassco {
 ///@{
 
 //! Supported clause types in theory propagation.
-enum class Clause_t : unsigned {
+enum class ClauseType : unsigned {
     learnt           = 0u, //!< Cumulative removable (i.e. subject to nogood deletion) clause.
     locked           = 1u, //!< Cumulative unremovable clause.
     transient        = 2u, //!< Removable clause associated with current solving step.
     transient_locked = 3u  //!< Unremovable clause associated with current solving step.
 };
-[[maybe_unused]] consteval auto enable_ops(std::type_identity<Clause_t>) -> BitOps;
+[[maybe_unused]] consteval auto enable_ops(std::type_identity<ClauseType>) -> BitOps;
 
 //! Named constants.
-enum class Statistics_t {
+enum class StatisticsType {
     empty = 0, //!< Empty (invalid) object.
     value = 1, //!< Single statistic value that is convertible to a double.
     array = 2, //!< Composite object mapping int keys to statistics types.
@@ -53,8 +53,6 @@ enum class Statistics_t {
 //! Represents an assignment of a particular solver.
 class AbstractAssignment {
 public:
-    using Value_t = Potassco::Value_t;
-    using Lit_t   = Potassco::Lit_t;
     virtual ~AbstractAssignment();
     //! Returns the number of variables in the assignment.
     [[nodiscard]] virtual uint32_t size() const = 0;
@@ -68,8 +66,8 @@ class AbstractAssignment {
     [[nodiscard]] virtual uint32_t rootLevel() const = 0;
     //! Returns whether @c lit is a valid literal in this assignment.
     [[nodiscard]] virtual bool hasLit(Lit_t lit) const = 0;
-    //! Returns the truth value that is currently assigned to @c lit or @c Value_t::free if @c lit is unassigned.
-    [[nodiscard]] virtual Value_t value(Lit_t lit) const = 0;
+    //! Returns the truth value that is currently assigned to @c lit or @c TruthValue::free if @c lit is unassigned.
+    [[nodiscard]] virtual TruthValue value(Lit_t lit) const = 0;
     //! Returns the decision level on which @c lit was assigned or @c UINT32_MAX if @c lit is unassigned.
     [[nodiscard]] virtual uint32_t level(Lit_t lit) const = 0;
     //! Returns the decision literal of the given decision level.
@@ -109,7 +107,6 @@ class AbstractAssignment {
 //! Represents one particular solver instance.
 class AbstractSolver {
 public:
-    using Lit = Potassco::Lit_t;
     virtual ~AbstractSolver();
     //! Returns the id of the solver that is associated with this object.
     [[nodiscard]] virtual Id_t id() const = 0;
@@ -129,8 +126,8 @@ class AbstractSolver {
      * that was created with @c Solver::addVariable(), it is also considered volatile.
      *
      */
-    [[nodiscard]] virtual bool addClause(const Potassco::LitSpan& clause, Clause_t prop) = 0;
-    bool addClause(const Potassco::LitSpan& clause) { return addClause(clause, Clause_t::learnt); }
+    [[nodiscard]] virtual bool addClause(const LitSpan& clause, ClauseType prop) = 0;
+    bool                       addClause(const LitSpan& clause) { return addClause(clause, ClauseType::learnt); }
 
     //! Adds a new volatile variable to this solver instance.
     /*!
@@ -139,7 +136,7 @@ class AbstractSolver {
      *
      * \return The positive literal of the new variable.
      */
-    [[nodiscard]] virtual Lit addVariable() = 0;
+    [[nodiscard]] virtual Lit_t addVariable() = 0;
     //! Propagates any newly implied literals.
     virtual bool propagate() = 0;
 
@@ -150,19 +147,19 @@ class AbstractSolver {
      * @{ */
 
     //! Returns whether the active propagator watches @c lit in this solver instance.
-    [[nodiscard]] virtual bool hasWatch(Lit lit) const = 0;
+    [[nodiscard]] virtual bool hasWatch(Lit_t lit) const = 0;
 
     //! Adds the active propagator to the list of propagators to be notified when the given literal is assigned in this
     //! solver instance.
     /*!
      * \post @c hasWatch(lit) returns true.
      */
-    virtual void addWatch(Lit lit) = 0;
+    virtual void addWatch(Lit_t lit) = 0;
     //! Removes the active propagator from the list of propagators watching @c lit in the given solver.
     /*!
      * \post @c hasWatch(lit) returns false.
      */
-    virtual void removeWatch(Lit lit) = 0;
+    virtual void removeWatch(Lit_t lit) = 0;
     //@}
 };
 
@@ -170,12 +167,12 @@ class AbstractSolver {
 class AbstractPropagator {
 public:
     //! Type for representing a set of literals that have recently changed.
-    using ChangeList = Potassco::LitSpan;
+    using ChangeList = LitSpan;
     virtual ~AbstractPropagator();
     //! Shall propagate the newly assigned literals given in @c changes.
-    virtual void propagate(AbstractSolver& solver, const ChangeList& changes) = 0;
+    virtual void propagate(AbstractSolver& solver, const LitSpan& changes) = 0;
     //! May update internal state of the newly unassigned literals given in @c undo.
-    virtual void undo(const AbstractSolver& solver, const ChangeList& undo) = 0;
+    virtual void undo(const AbstractSolver& solver, const LitSpan& undo) = 0;
     //! Similar to propagate but called on an assignment without a list of changes.
     virtual void check(AbstractSolver& solver) = 0;
 };
@@ -183,7 +180,6 @@ class AbstractPropagator {
 //! Base class for implementing heuristics.
 class AbstractHeuristic {
 public:
-    using Lit = Potassco::Lit_t;
     virtual ~AbstractHeuristic();
     //! Shall return the literal that the solver with the given id should decide on next.
     /*!
@@ -196,7 +192,7 @@ class AbstractHeuristic {
      * \note If the function returns 0 or a literal that is already assigned, the returned lit
      *       is implicitly replaced with fallback.
      */
-    virtual Lit decide(Id_t solverId, const AbstractAssignment& assignment, Lit fallback) = 0;
+    virtual Lit_t decide(Id_t solverId, const AbstractAssignment& assignment, Lit_t fallback) = 0;
 };
 
 //! Base class for providing (solver) statistics.
@@ -209,13 +205,14 @@ class AbstractStatistics {
 public:
     //! Opaque type for representing (sub) keys.
     using Key_t = uint64_t;
+    using Type  = StatisticsType;
 
     virtual ~AbstractStatistics();
 
     //! Returns the root key of this statistic object.
     [[nodiscard]] virtual Key_t root() const = 0;
     //! Returns the type of the object with the given key.
-    [[nodiscard]] virtual Statistics_t type(Key_t key) const = 0;
+    [[nodiscard]] virtual Type type(Key_t key) const = 0;
     //! Returns the child count of the object with the given key or 0 if it is a value.
     [[nodiscard]] virtual size_t size(Key_t key) const = 0;
     //! Returns whether the object with the given key can be updated.
@@ -240,7 +237,7 @@ class AbstractStatistics {
      * \return The key of the created statistic object.
      *
      */
-    virtual Key_t push(Key_t arr, Statistics_t type) = 0;
+    virtual Key_t push(Key_t arr, Type type) = 0;
     //@}
 
     /*!
@@ -280,7 +277,7 @@ class AbstractStatistics {
      *       the function either returns its key provided that the types match,
      *       or otherwise signals failure by throwing a std::logic_error.
      */
-    virtual Key_t add(Key_t mapK, const char* name, Statistics_t type) = 0;
+    virtual Key_t add(Key_t mapK, const char* name, Type type) = 0;
     //@}
     /*!
      * \name Value
diff --git a/potassco/convert.h b/potassco/convert.h
index de153df..b062b83 100644
--- a/potassco/convert.h
+++ b/potassco/convert.h
@@ -52,17 +52,17 @@ class SmodelsConvert : public AbstractProgram {
     //! Calls @c beginStep() on the associated output program.
     void beginStep() override;
     //! Converts the given rule into one or more smodels rules.
-    void rule(Head_t t, const AtomSpan& head, const LitSpan& body) override;
+    void rule(HeadType t, const AtomSpan& head, const LitSpan& body) override;
     //! Converts the given rule into one or more smodels rules or throws an exception if body contains negative weights.
-    void rule(Head_t t, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override;
+    void rule(HeadType t, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override;
     //! Converts literals associated with a priority to a set of corresponding smodels minimize rules.
     void minimize(Weight_t prio, const WeightLitSpan& lits) override;
     //! Adds an atom with the given name that is equivalent to the condition to the symbol table.
     void output(const std::string_view& name, const LitSpan& cond) override;
     //! Marks the atom that is equivalent to @c 'a' as external.
-    void external(Atom_t a, Value_t v) override;
+    void external(Atom_t a, TruthValue v) override;
     //! Adds an @a _heuristic predicate over the given atom to the symbol table that is equivalent to @c condition.
-    void heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& condition) override;
+    void heuristic(Atom_t a, DomModifier t, int bias, unsigned prio, const LitSpan& condition) override;
     //! Adds an @a _edge(s,t) predicate to the symbol table that is equivalent to @c condition.
     void acycEdge(int s, int t, const LitSpan& condition) override;
 
diff --git a/potassco/match_basic_types.h b/potassco/match_basic_types.h
index afa9b21..ad09c97 100644
--- a/potassco/match_basic_types.h
+++ b/potassco/match_basic_types.h
@@ -129,7 +129,7 @@ class ProgramReader {
 
 protected:
     using StreamType = BufferedStream;
-    using WLit_t     = WeightLit_t;
+    using WLit_t     = WeightLit;
     //! Shall return true if the format of the input stream is supported by this object.
     /*!
      * \param[out] inc Whether the input stream represents an incremental program.
@@ -168,7 +168,7 @@ class ProgramReader {
     //! Extracts a literal (i.e. positive or negative atom) or fails with a std::exception.
     Lit_t matchLit(const char* error = "literal expected") {
         auto res = matchInt(-static_cast<Lit_t>(varMax_), static_cast<Lit_t>(varMax_), error);
-        (void) require(res != 0, error);
+        require(res != 0, error);
         return static_cast<Lit_t>(res);
     }
     //! Extracts a weight or fails with a std::exception.
diff --git a/potassco/program_opts/program_options.h b/potassco/program_opts/program_options.h
index 6dff151..92a4717 100644
--- a/potassco/program_opts/program_options.h
+++ b/potassco/program_opts/program_options.h
@@ -93,12 +93,12 @@ class OptionOutput;
 class OptionGroup {
 public:
     using OptionList      = std::vector<SharedOptPtr>;
-    using option_iterator = OptionList::const_iterator;
+    using option_iterator = OptionList::const_iterator; // NOLINT
 
     /*!
      * Creates a new group of options under the given caption.
      */
-    OptionGroup(std::string_view caption = "", DescriptionLevel descLevel = desc_level_default);
+    explicit OptionGroup(std::string_view caption = "", DescriptionLevel descLevel = desc_level_default);
 
     //! Returns the caption of this group.
     [[nodiscard]] const std::string& caption() const { return caption_; }
@@ -174,16 +174,16 @@ class OptionContext {
     using KeyType        = std::size_t;
     using Name2Key       = std::map<std::string, KeyType>;
     using GroupList      = std::vector<OptionGroup>;
-    using index_iterator = Name2Key::const_iterator;
+    using index_iterator = Name2Key::const_iterator; // NOLINT
     using PrefixRange    = std::pair<index_iterator, index_iterator>;
     using OptionList     = OptionGroup::OptionList;
 
 public:
     //! Type for identifying an option within a context
-    using option_iterator = OptionList::const_iterator;
+    using option_iterator = OptionList::const_iterator; // NOLINT
     using OptionRange     = PrefixRange;
 
-    OptionContext(std::string_view caption = "", DescriptionLevel desc_default = desc_level_default);
+    explicit OptionContext(std::string_view caption = "", DescriptionLevel desc_default = desc_level_default);
 
     [[nodiscard]] const std::string& caption() const;
 
@@ -328,7 +328,7 @@ class ParsedValues {
 public:
     using OptionAndValue = std::pair<SharedOptPtr, std::string>;
     using Values         = std::vector<OptionAndValue>;
-    using iterator       = Values::const_iterator;
+    using iterator       = Values::const_iterator; // NOLINT
 
     /*!
      * \param a_ctx The OptionContext for which this object stores raw-values.
@@ -418,10 +418,10 @@ class OptionOutputImpl : public OptionOutput {
               form) {}
     //! Writes formatted option descriptions to given std::string.
     explicit OptionOutputImpl(std::string& str, const Formatter& form = Formatter())
-        : OptionOutputImpl([&str](std::string_view view) { str.append(view.data(), std::size(view)); }, form) {}
+        : OptionOutputImpl([&str](std::string_view view) { str.append(std::data(view), std::size(view)); }, form) {}
     //! Writes formatted option descriptions to given std::ostream.
     explicit OptionOutputImpl(std::ostream& os, const Formatter& form = Formatter())
-        : OptionOutputImpl([&os](std::string_view view) { os.write(view.data(), std::ssize(view)); }, form) {}
+        : OptionOutputImpl([&os](std::string_view view) { os.write(std::data(view), std::ssize(view)); }, form) {}
     //! Writes formatted option descriptions to given sink.
     explicit OptionOutputImpl(Sink sink, const Formatter& form = Formatter())
         : sink_(std::move(sink))
diff --git a/potassco/program_opts/string_convert.h b/potassco/program_opts/string_convert.h
index 4a93efe..e364953 100644
--- a/potassco/program_opts/string_convert.h
+++ b/potassco/program_opts/string_convert.h
@@ -55,12 +55,12 @@ constexpr auto ok(T ec) {
     }
 }
 constexpr std::from_chars_result error(std::string_view& x, std::errc ec = std::errc::invalid_argument) {
-    return {.ptr = x.data(), .ec = ec};
+    return {.ptr = std::data(x), .ec = ec};
 }
 constexpr std::from_chars_result success(std::string_view& x, std::size_t pop) {
     assert(pop <= x.length());
     x.remove_prefix(pop);
-    return {.ptr = x.data(), .ec = {}};
+    return {.ptr = std::data(x), .ec = {}};
 }
 bool matchOpt(std::string_view& in, char v);
 bool eqIgnoreCase(const char* lhs, const char* rhs, std::size_t n);
diff --git a/potassco/program_opts/typed_value.h b/potassco/program_opts/typed_value.h
index 1e6d9a6..0dd57b5 100644
--- a/potassco/program_opts/typed_value.h
+++ b/potassco/program_opts/typed_value.h
@@ -77,7 +77,7 @@ bool parseValue(const std::vector<std::pair<std::string, EnumT>>& candidates, co
 template <typename Callable>
 class TypedValue : public Value {
 public:
-    TypedValue(Callable func) : func_(std::move(func)) {}
+    explicit TypedValue(Callable func) : func_(std::move(func)) {}
     bool doParse(const std::string& opt, const std::string& value) override { return func_(opt, value); }
 
 private:
diff --git a/potassco/rule_utils.h b/potassco/rule_utils.h
index 15fc954..5bea7ff 100644
--- a/potassco/rule_utils.h
+++ b/potassco/rule_utils.h
@@ -32,31 +32,30 @@ namespace Potassco {
 ///@{
 
 //! A sum aggregate with a lower bound.
-struct Sum_t {
+struct Sum {
     WeightLitSpan lits;  //!< Weight literals of the aggregate.
     Weight_t      bound; //!< Lower bound of the aggregate.
 };
 //! A type that can represent an aspif rule.
-struct Rule_t {
-    Rule_t() : ht{Head_t::disjunctive}, bt{Body_t::normal}, cond{} {}
-
-    Head_t   ht;   //!< Head type of the rule.
-    AtomSpan head; //!< Head atoms of the rule.
-    Body_t   bt;   //!< Type of rule body.
+struct Rule {
+    constexpr Rule() {}
+    HeadType ht{HeadType::disjunctive}; //!< Head type of the rule.
+    AtomSpan head{};                    //!< Head atoms of the rule.
+    BodyType bt{BodyType::normal};      //!< Type of rule body.
     union {
-        LitSpan cond;
-        Sum_t   agg;
+        LitSpan cond{};
+        Sum     agg;
     };
     //! Named constructor for creating a rule.
-    static Rule_t normal(Head_t ht, const AtomSpan& head, const LitSpan& body);
+    static Rule normal(HeadType ht, const AtomSpan& head, const LitSpan& body);
     //! Named constructor for creating a sum rule.
-    static Rule_t sum(Head_t ht, const AtomSpan& head, const Sum_t& sum);
+    static Rule sum(HeadType ht, const AtomSpan& head, const Sum& sum);
     //! Named constructor for creating a sum rule.
-    static Rule_t sum(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits);
+    static Rule sum(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits);
     //! Returns whether the rule has a normal body, i.e. whether the body is a conjunction of literals.
-    [[nodiscard]] bool normal() const { return bt == Body_t::normal; }
+    [[nodiscard]] bool normal() const { return bt == BodyType::normal; }
     //! Returns whether the body of the rule is a sum aggregate.
-    [[nodiscard]] bool sum() const { return bt != Body_t::normal; }
+    [[nodiscard]] bool sum() const { return bt != BodyType::normal; }
 };
 
 //! A builder class for creating a rule.
@@ -80,7 +79,7 @@ class RuleBuilder {
      */
     //@{
     //! Start definition of the rule's head, which can be either disjunctive or a choice.
-    RuleBuilder& start(Head_t ht = Head_t::disjunctive);
+    RuleBuilder& start(HeadType ht = HeadType::disjunctive);
     //! Start definition of a minimize rule. No head allowed.
     RuleBuilder& startMinimize(Weight_t prio);
     //! Start definition of a conjunction to be used as the rule's body.
@@ -102,8 +101,8 @@ class RuleBuilder {
     RuleBuilder& addHead(Atom_t a);
     //! Add lit to the rule's body.
     RuleBuilder& addGoal(Lit_t lit);
-    RuleBuilder& addGoal(WeightLit_t lit);
-    RuleBuilder& addGoal(Lit_t lit, Weight_t w) { return addGoal(WeightLit_t{.lit = lit, .weight = w}); }
+    RuleBuilder& addGoal(WeightLit lit);
+    RuleBuilder& addGoal(Lit_t lit, Weight_t w) { return addGoal(WeightLit{.lit = lit, .weight = w}); }
     //@}
 
     //! Stop definition of rule and add rule to out if given.
@@ -118,7 +117,7 @@ class RuleBuilder {
     //! Discard head of active rule but keep body if any.
     RuleBuilder& clearHead();
     //! Weaken active sum aggregate body to a normal body or count aggregate.
-    RuleBuilder& weaken(Body_t to, bool resetWeights = true);
+    RuleBuilder& weaken(BodyType to, bool resetWeights = true);
 
     /*!
      * \name Query functions.
@@ -126,16 +125,16 @@ class RuleBuilder {
      * \note The result of these functions is only valid until the next call to an update function.
      */
     //@{
-    [[nodiscard]] auto headType() const -> Head_t;
+    [[nodiscard]] auto headType() const -> HeadType;
     [[nodiscard]] auto head() const -> AtomSpan;
     [[nodiscard]] auto isMinimize() const -> bool;
-    [[nodiscard]] auto bodyType() const -> Body_t;
+    [[nodiscard]] auto bodyType() const -> BodyType;
     [[nodiscard]] auto body() const -> LitSpan;
     [[nodiscard]] auto bound() const -> Weight_t;
-    [[nodiscard]] auto sumLits() const -> std::span<WeightLit_t>;
-    [[nodiscard]] auto findSumLit(Lit_t lit) const -> WeightLit_t*;
-    [[nodiscard]] auto sum() const -> Sum_t;
-    [[nodiscard]] auto rule() const -> Rule_t;
+    [[nodiscard]] auto sumLits() const -> std::span<WeightLit>;
+    [[nodiscard]] auto findSumLit(Lit_t lit) const -> WeightLit*;
+    [[nodiscard]] auto sum() const -> Sum;
+    [[nodiscard]] auto rule() const -> Rule;
     [[nodiscard]] auto frozen() const -> bool;
     //@}
 private:
diff --git a/potassco/smodels.h b/potassco/smodels.h
index 30a6e2c..b233081 100644
--- a/potassco/smodels.h
+++ b/potassco/smodels.h
@@ -34,7 +34,7 @@ namespace Potassco {
  */
 ///@{
 //! Smodels rule types.
-enum class SmodelsRule_t : unsigned {
+enum class SmodelsType : unsigned {
     end               = 0,  //!< Not a rule, marks the end of all rules.
     basic             = 1,  //!< Normal rule, i.e. h :- l1, ..., ln.
     cardinality       = 2,  //!< Cardinality constraint, i.e. h :- lb {l1, ..., ln}.
@@ -55,7 +55,6 @@ class SmodelsInput : public ProgramReader {
     using AtomLookup = std::function<Atom_t(std::string_view name)>;
     //! Options for configuring reading of smodels format.
     struct Options {
-        Options() : claspExt(false), cEdge(false), cHeuristic(false), filter(false) {}
         //! Enable clasp extensions for handling incremental programs.
         Options& enableClaspExt() {
             claspExt = true;
@@ -76,10 +75,10 @@ class SmodelsInput : public ProgramReader {
             filter = true;
             return *this;
         }
-        bool claspExt;
-        bool cEdge;
-        bool cHeuristic;
-        bool filter;
+        bool claspExt{false};
+        bool cEdge{false};
+        bool cHeuristic{false};
+        bool filter{false};
     };
     //! Creates a new parser object that calls @c out on each parsed element.
     /*!
@@ -121,7 +120,7 @@ class SmodelsInput : public ProgramReader {
     Options                    opts_;
 };
 //! Tries to extract a heuristic modification from a given _heuristic/3 or _heuristic/4 predicate.
-bool matchDomHeuPred(std::string_view pred, std::string_view& atom, Heuristic_t& type, int& bias, unsigned& prio);
+bool matchDomHeuPred(std::string_view pred, std::string_view& atom, DomModifier& type, int& bias, unsigned& prio);
 //! Tries to extract source and target from a given _edge/2 or _acyc_/0 predicate.
 bool matchEdgePred(std::string_view pred, std::string_view& n0, std::string_view& n1);
 
@@ -163,9 +162,9 @@ class SmodelsOutput : public AbstractProgram {
     //! Starts a new step.
     void beginStep() override;
     //! Writes a basic, choice, or disjunctive rule or throws an exception if rule is not representable.
-    void rule(Head_t t, const AtomSpan& head, const LitSpan& body) override;
+    void rule(HeadType ht, const AtomSpan& head, const LitSpan& body) override;
     //! Writes a cardinality or weight rule or throws an exception if rule is not representable.
-    void rule(Head_t t, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override;
+    void rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override;
     //! Writes the given minimize rule while ignoring its priority.
     void minimize(Weight_t prio, const WeightLitSpan& lits) override;
     //! Writes the entry (atom, str) to the symbol table provided that condition equals atom.
@@ -179,15 +178,15 @@ class SmodelsOutput : public AbstractProgram {
      */
     void assume(const LitSpan& lits) override;
     //! Requires enableClaspExt or throws exception.
-    void external(Atom_t a, Value_t v) override;
+    void external(Atom_t a, TruthValue v) override;
     //! Terminates the current step.
     void endStep() override;
 
 protected:
     //! Starts writing a rule of type @c rt.
-    SmodelsOutput& startRule(SmodelsRule_t rt);
+    SmodelsOutput& startRule(SmodelsType rt);
     //! Writes the given head.
-    SmodelsOutput& add(Head_t ht, const AtomSpan& head);
+    SmodelsOutput& add(HeadType ht, const AtomSpan& head);
     //! Writes the given normal body in smodels format, i.e. @c size(lits) @c size(B-) atoms in B- atoms in B+
     SmodelsOutput& add(const LitSpan& lits);
     //! Writes the given extended body in smodels format.
diff --git a/potassco/theory_data.h b/potassco/theory_data.h
index 3bb428b..4725a17 100644
--- a/potassco/theory_data.h
+++ b/potassco/theory_data.h
@@ -34,19 +34,19 @@ class TheoryData;
  * \addtogroup BasicTypes
  */
 ///@{
-//! Supported aspif theory directives.
-enum class Theory_t { number = 0, symbol = 1, compound = 2, reserved = 3, element = 4, atom = 5, atom_with_guard = 6 };
-POTASSCO_SET_DEFAULT_ENUM_MAX(Theory_t::atom_with_guard);
+//! Supported aspif theory terms.
+enum class TheoryTermType : uint32_t { number = 0, symbol = 1, compound = 2 };
+POTASSCO_SET_DEFAULT_ENUM_MAX(TheoryTermType::compound);
 
 //! Supported aspif theory tuple types.
-enum class Tuple_t { bracket = -3, brace = -2, paren = -1 };
-POTASSCO_SET_DEFAULT_ENUM_COUNT(Tuple_t, 3u, -3);
-[[nodiscard]] constexpr auto parens(Tuple_t t) -> std::string_view {
+enum class TupleType { bracket = -3, brace = -2, paren = -1 };
+POTASSCO_SET_DEFAULT_ENUM_COUNT(TupleType, 3u, -3);
+[[nodiscard]] constexpr auto parens(TupleType t) -> std::string_view {
     using namespace std::literals;
     switch (t) {
-        case Tuple_t::bracket: return "[]"sv;
-        case Tuple_t::brace  : return "{}"sv;
-        case Tuple_t::paren  : return "()"sv;
+        case TupleType::bracket: return "[]"sv;
+        case TupleType::brace  : return "{}"sv;
+        case TupleType::paren  : return "()"sv;
     }
     POTASSCO_ASSERT_NOT_REACHED("unexpected tuple type");
 }
@@ -55,10 +55,12 @@ POTASSCO_SET_DEFAULT_ENUM_COUNT(Tuple_t, 3u, -3);
 class TheoryTerm {
 public:
     TheoryTerm() noexcept = default;
+    //! Term type.
+    using Type = TheoryTermType;
     //! Iterator type for iterating over arguments of a compound term.
     using iterator = const Id_t*; // NOLINT
     //! Returns the type of this term.
-    [[nodiscard]] Theory_t type() const;
+    [[nodiscard]] Type type() const;
     //! Returns the number stored in this or throws if type() != Number.
     [[nodiscard]] int number() const;
     //! Returns the symbol stored in this or throws if type() != Symbol.
@@ -72,7 +74,7 @@ class TheoryTerm {
     //! Returns whether this is a tuple.
     [[nodiscard]] bool isTuple() const;
     //! Returns the tuple id stored in this or throws if not isTuple().
-    [[nodiscard]] Tuple_t tuple() const;
+    [[nodiscard]] TupleType tuple() const;
     //! Returns the number of arguments in this term.
     [[nodiscard]] uint32_t size() const;
     //! Returns an iterator pointing to the first argument of this term.
@@ -88,7 +90,8 @@ class TheoryTerm {
     friend class TheoryData;
     [[nodiscard]] uintptr_t getPtr() const;
     [[nodiscard]] FuncData* func() const;
-    uint64_t                data_ = 0;
+
+    uint64_t data_ = 0;
 };
 
 //! A basic building block for a theory atom.
@@ -211,7 +214,7 @@ class TheoryData {
      */
     void addTerm(Id_t termId, Id_t funcSym, const IdSpan& args);
     //! Adds a new tuple term with the given id.
-    void addTerm(Id_t termId, Tuple_t type, const IdSpan& args);
+    void addTerm(Id_t termId, TupleType type, const IdSpan& args);
 
     //! Removes the term with the given id.
     /*!
@@ -302,11 +305,11 @@ class TheoryData {
 
 inline void print(AbstractProgram& out, Id_t termId, const TheoryTerm& term) {
     switch (term.type()) {
-        case Theory_t::number  : out.theoryTerm(termId, term.number()); break;
-        case Theory_t::symbol  : out.theoryTerm(termId, term.symbol()); break;
-        case Theory_t::compound: out.theoryTerm(termId, term.compound(), term.terms()); break;
-        default                : break;
+        case TheoryTermType::number  : out.theoryTerm(termId, term.number()); return;
+        case TheoryTermType::symbol  : out.theoryTerm(termId, term.symbol()); return;
+        case TheoryTermType::compound: out.theoryTerm(termId, term.compound(), term.terms()); return;
     }
+    POTASSCO_ASSERT_NOT_REACHED("invalid term");
 }
 inline void print(AbstractProgram& out, const TheoryAtom& a) {
     if (a.guard()) {
diff --git a/src/application.cpp b/src/application.cpp
index a53c54c..7213895 100644
--- a/src/application.cpp
+++ b/src/application.cpp
@@ -101,10 +101,11 @@ static int fetchDec(T& x) {
 /////////////////////////////////////////////////////////////////////////////////////////
 // Application
 /////////////////////////////////////////////////////////////////////////////////////////
-static Application* g_instance; // running instance (only valid during run()).
-struct Application::Error : std::runtime_error {
+struct Application::Error final : std::runtime_error {
     explicit Error(const char* msg) : std::runtime_error(msg) {}
 };
+static Application* g_instance; // running instance (only valid during run()).
+
 Application::Application()
     : exitCode_(EXIT_FAILURE)
     , timeout_(0)
@@ -318,18 +319,16 @@ bool Application::applyOptions(int argc, char** argv) {
     bool          version = false;
     ParsedOptions parsed; // options found in command-line
     OptionContext allOpts(std::string("<").append(getName()).append(">"));
-    HelpOpt       helpO = getHelpOption();
     OptionGroup   basic("Basic Options");
-    if (helpO.second > 0) {
-        Value* hv = helpO.second == 1
-                        ? storeTo(help)->flag()
-                        : storeTo(help,
-                                  [maxV = helpO.second](const std::string& v, unsigned& out) {
-                                      return Potassco::stringTo(v, out) == std::errc{} && out > 0 && out <= maxV;
-                                  })
-                              ->arg("<n>")
-                              ->implicit("1");
-        basic.addOptions()("help,h", hv, helpO.first);
+    if (auto [message, level] = getHelpOption(); level > 0) {
+        Value* hv = level == 1 ? storeTo(help)->flag()
+                               : storeTo(help,
+                                         [maxV = level](const std::string& v, unsigned& out) {
+                                             return Potassco::stringTo(v, out) == std::errc{} && out > 0 && out <= maxV;
+                                         })
+                                     ->arg("<n>")
+                                     ->implicit("1");
+        basic.addOptions()("help,h", hv, message);
     }
     basic.addOptions()                                                                                 //
         ("version,v", flag(version), "Print version information and exit")                             //
diff --git a/src/aspif.cpp b/src/aspif.cpp
index b68ecb5..9b9b56e 100644
--- a/src/aspif.cpp
+++ b/src/aspif.cpp
@@ -66,52 +66,52 @@ bool AspifInput::doParse() {
     data_      = &data;
     auto& rule = data.rule;
     out_.beginStep();
-    for (Directive_t rt; (rt = matchEnum<Directive_t>("rule type or 0 expected")) != Directive_t::end; rule.clear()) {
+    for (AspifType rt; (rt = matchEnum<AspifType>("rule type or 0 expected")) != AspifType::end; rule.clear()) {
         switch (rt) {
             default:
-                require(rt == Directive_t::comment, "unrecognized rule type");
+                require(rt == AspifType::comment, "unrecognized rule type");
                 skipLine();
                 break;
-            case Directive_t::rule: {
-                rule.start(matchEnum<Head_t>("invalid head type"));
+            case AspifType::rule: {
+                rule.start(matchEnum<HeadType>("invalid head type"));
                 matchAtoms();
-                if (auto bt = matchEnum<Body_t>("invalid body type"); bt == Body_t::normal) {
+                if (auto bt = matchEnum<BodyType>("invalid body type"); bt == BodyType::normal) {
                     matchLits();
                 }
                 else {
-                    require(bt == Body_t::sum, "unexpected body type");
+                    require(bt == BodyType::sum, "unexpected body type");
                     rule.startSum(matchWeight());
                     matchWLits(true);
                 }
                 rule.end(&out_);
                 break;
             }
-            case Directive_t::minimize:
+            case AspifType::minimize:
                 rule.startMinimize(matchWeight(false, "priority expected"));
                 matchWLits(false);
                 rule.end(&out_);
                 break;
-            case Directive_t::project:
+            case AspifType::project:
                 matchAtoms();
                 out_.project(rule.head());
                 break;
-            case Directive_t::output: {
+            case AspifType::output: {
                 matchString();
                 matchLits();
                 out_.output(data.sym.view(), rule.body());
                 break;
             }
-            case Directive_t::external:
+            case AspifType::external:
                 if (auto atom = matchAtom()) {
-                    out_.external(atom, matchEnum<Value_t>("value expected"));
+                    out_.external(atom, matchEnum<TruthValue>("value expected"));
                 }
                 break;
-            case Directive_t::assume:
+            case AspifType::assume:
                 matchLits();
                 out_.assume(rule.body());
                 break;
-            case Directive_t::heuristic: {
-                auto type = matchEnum<Heuristic_t>("invalid heuristic modifier");
+            case AspifType::heuristic: {
+                auto type = matchEnum<DomModifier>("invalid heuristic modifier");
                 auto atom = matchAtom();
                 auto bias = matchInt();
                 auto prio = matchUint("invalid heuristic priority");
@@ -119,14 +119,14 @@ bool AspifInput::doParse() {
                 out_.heuristic(atom, type, bias, prio, rule.body());
                 break;
             }
-            case Directive_t::edge: {
+            case AspifType::edge: {
                 auto start = matchInt("invalid edge, start node expected");
                 auto end   = matchInt("invalid edge, end node expected");
                 matchLits();
                 out_.acycEdge(start, end, rule.body());
                 break;
             }
-            case Directive_t::theory: matchTheory(static_cast<Theory_t>(matchUint())); break;
+            case AspifType::theory: matchTheory(matchEnum<TheoryType>("invalid theory directive")); break;
         }
     }
     out_.endStep();
@@ -154,32 +154,32 @@ void AspifInput::matchIds() {
     data_->ids.resize(len);
     for (uint32_t i = 0; i != len; ++i) { data_->ids[i] = matchId(); }
 }
-void AspifInput::matchTheory(Theory_t rt) {
+void AspifInput::matchTheory(TheoryType t) {
     auto tId = matchId();
-    switch (rt) {
-        default              : error("unrecognized theory directive type"); return;
-        case Theory_t::number: out_.theoryTerm(tId, matchInt()); break;
-        case Theory_t::symbol:
+    switch (t) {
+        default                : error("unrecognized theory directive type"); return;
+        case TheoryType::number: out_.theoryTerm(tId, matchInt()); break;
+        case TheoryType::symbol:
             matchString();
             out_.theoryTerm(tId, data_->sym.view());
             break;
-        case Theory_t::compound: {
+        case TheoryType::compound: {
             auto type = matchInt("unrecognized compound term type");
             matchIds();
             out_.theoryTerm(tId, type, data_->ids);
             break;
         }
-        case Theory_t::element: {
+        case TheoryType::element: {
             matchIds();
             matchLits();
             out_.theoryElement(tId, data_->ids, data_->rule.body());
             break;
         }
-        case Theory_t::atom: // fall through
-        case Theory_t::atom_with_guard: {
+        case TheoryType::atom: // fall through
+        case TheoryType::atom_with_guard: {
             auto termId = matchId();
             matchIds();
-            if (rt == Theory_t::atom) {
+            if (t == TheoryType::atom) {
                 out_.theoryAtom(tId, termId, data_->ids);
             }
             else {
@@ -191,18 +191,18 @@ void AspifInput::matchTheory(Theory_t rt) {
     }
 }
 
-int readAspif(std::istream& in, AbstractProgram& out) {
+int readAspif(std::istream& prg, AbstractProgram& out) {
     AspifInput reader(out);
-    return readProgram(in, reader);
+    return readProgram(prg, reader);
 }
 /////////////////////////////////////////////////////////////////////////////////////////
 // AspifOutput
 /////////////////////////////////////////////////////////////////////////////////////////
-static std::ostream& operator<<(std::ostream& os, WeightLit_t wl) { return os << lit(wl) << " " << weight(wl); }
+static std::ostream& operator<<(std::ostream& os, WeightLit wl) { return os << lit(wl) << " " << weight(wl); }
 
 AspifOutput::AspifOutput(std::ostream& os) : os_(os) {}
 
-AspifOutput& AspifOutput::startDir(Directive_t r) {
+AspifOutput& AspifOutput::startDir(AspifType r) {
     os_ << to_underlying(r);
     return *this;
 }
@@ -238,45 +238,45 @@ void AspifOutput::initProgram(bool inc) {
     }
     os_ << '\n';
 }
-void AspifOutput::rule(Head_t ht, const AtomSpan& head, const LitSpan& body) {
-    startDir(Directive_t::rule).add(ht).add(head).add(Body_t::normal).add(body).endDir();
+void AspifOutput::rule(HeadType ht, const AtomSpan& head, const LitSpan& body) {
+    startDir(AspifType::rule).add(ht).add(head).add(BodyType::normal).add(body).endDir();
 }
-void AspifOutput::rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) {
-    startDir(Directive_t::rule).add(ht).add(head).add(Body_t::sum).add(bound).add(body).endDir();
+void AspifOutput::rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) {
+    startDir(AspifType::rule).add(ht).add(head).add(BodyType::sum).add(bound).add(body).endDir();
 }
 void AspifOutput::minimize(Weight_t prio, const WeightLitSpan& lits) {
-    startDir(Directive_t::minimize).add(prio).add(lits).endDir();
+    startDir(AspifType::minimize).add(prio).add(lits).endDir();
 }
 void AspifOutput::output(const std::string_view& str, const LitSpan& cond) {
-    startDir(Directive_t::output).add(str).add(cond).endDir();
+    startDir(AspifType::output).add(str).add(cond).endDir();
 }
-void AspifOutput::external(Atom_t a, Value_t v) { startDir(Directive_t::external).add(a).add(v).endDir(); }
-void AspifOutput::assume(const LitSpan& lits) { startDir(Directive_t::assume).add(lits).endDir(); }
-void AspifOutput::project(const AtomSpan& atoms) { startDir(Directive_t::project).add(atoms).endDir(); }
+void AspifOutput::external(Atom_t a, TruthValue v) { startDir(AspifType::external).add(a).add(v).endDir(); }
+void AspifOutput::assume(const LitSpan& lits) { startDir(AspifType::assume).add(lits).endDir(); }
+void AspifOutput::project(const AtomSpan& atoms) { startDir(AspifType::project).add(atoms).endDir(); }
 void AspifOutput::acycEdge(int s, int t, const LitSpan& cond) {
-    startDir(Directive_t::edge).add(s).add(t).add(cond).endDir();
+    startDir(AspifType::edge).add(s).add(t).add(cond).endDir();
 }
-void AspifOutput::heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& cond) {
-    startDir(Directive_t::heuristic).add(t).add(a).add(bias).add(prio).add(cond).endDir();
+void AspifOutput::heuristic(Atom_t a, DomModifier t, int bias, unsigned prio, const LitSpan& cond) {
+    startDir(AspifType::heuristic).add(t).add(a).add(bias).add(prio).add(cond).endDir();
 }
 void AspifOutput::theoryTerm(Id_t termId, int number) {
-    startDir(Directive_t::theory).add(Theory_t::number).add(termId).add(number).endDir();
+    startDir(AspifType::theory).add(TheoryType::number).add(termId).add(number).endDir();
 }
 void AspifOutput::theoryTerm(Id_t termId, const std::string_view& name) {
-    startDir(Directive_t::theory).add(Theory_t::symbol).add(termId).add(name).endDir();
+    startDir(AspifType::theory).add(TheoryType::symbol).add(termId).add(name).endDir();
 }
 void AspifOutput::theoryTerm(Id_t termId, int cId, const IdSpan& args) {
-    startDir(Directive_t::theory).add(Theory_t::compound).add(termId).add(cId).add(args).endDir();
+    startDir(AspifType::theory).add(TheoryType::compound).add(termId).add(cId).add(args).endDir();
 }
 void AspifOutput::theoryElement(Id_t elementId, const IdSpan& terms, const LitSpan& cond) {
-    startDir(Directive_t::theory).add(Theory_t::element).add(elementId).add(terms).add(cond).endDir();
+    startDir(AspifType::theory).add(TheoryType::element).add(elementId).add(terms).add(cond).endDir();
 }
 void AspifOutput::theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements) {
-    startDir(Directive_t::theory).add(Theory_t::atom).add(atomOrZero).add(termId).add(elements).endDir();
+    startDir(AspifType::theory).add(TheoryType::atom).add(atomOrZero).add(termId).add(elements).endDir();
 }
 void AspifOutput::theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& elements, Id_t op, Id_t rhs) {
-    startDir(Directive_t::theory)
-        .add(Theory_t::atom_with_guard)
+    startDir(AspifType::theory)
+        .add(TheoryType::atom_with_guard)
         .add(atomOrZero)
         .add(termId)
         .add(elements)
diff --git a/src/aspif_text.cpp b/src/aspif_text.cpp
index 596b50e..72762d9 100644
--- a/src/aspif_text.cpp
+++ b/src/aspif_text.cpp
@@ -103,7 +103,7 @@ void AspifTextInput::parseStatements() {
 void AspifTextInput::matchRule(char c) {
     if (c == '{') {
         matchDelim('{');
-        data_->rule.start(Head_t::choice);
+        data_->rule.start(HeadType::choice);
         matchAtoms(";,"sv);
         matchDelim('}');
     }
@@ -152,10 +152,10 @@ bool AspifTextInput::matchDirective() {
     }
     else if (matchOpt("#external"sv)) {
         auto a = matchId();
-        auto v = Value_t::false_;
+        auto v = TruthValue::false_;
         matchDelim('.');
         if (matchOpt("["sv)) {
-            require(std::ranges::any_of(enum_entries<Value_t>(),
+            require(std::ranges::any_of(enum_entries<TruthValue>(),
                                         [&](const auto& e) {
                                             v = e.first;
                                             return matchOpt(e.second);
@@ -210,8 +210,8 @@ bool AspifTextInput::matchDirective() {
     }
     return true;
 }
-bool AspifTextInput::matchOpt(std::string_view term) {
-    if (match(term)) {
+bool AspifTextInput::matchOpt(std::string_view ts) {
+    if (match(ts)) {
         skipWs();
         return true;
     }
@@ -223,13 +223,13 @@ void AspifTextInput::matchDelim(char c) {
     skipWs();
 }
 
-void AspifTextInput::matchAtoms(std::string_view seps) {
+void AspifTextInput::matchAtoms(std::string_view sv) {
     if (isLower(skipWs())) {
         do {
             auto x = matchLit();
             require(x > 0, "positive atom expected");
             data_->rule.addHead(static_cast<Atom_t>(x));
-        } while (seps.find(peek()) != std::string_view::npos && get() && (skipWs(), true));
+        } while (sv.find(peek()) != std::string_view::npos && get() && (skipWs(), true));
     }
 }
 void AspifTextInput::matchLits() {
@@ -247,7 +247,7 @@ void AspifTextInput::matchAgg() {
     matchDelim('{');
     if (not matchOpt("}"sv)) {
         do {
-            auto wl = WeightLit_t{matchLit(), 1};
+            auto wl = WeightLit{matchLit(), 1};
             if (matchOpt("="sv)) {
                 wl.weight = matchInt();
             }
@@ -280,10 +280,8 @@ Atom_t AspifTextInput::matchId() {
         require(i > 0, "<pos-integer> expected");
         return static_cast<Atom_t>(i);
     }
-    else {
-        skipWs();
-        return static_cast<Atom_t>(c - 'a') + 1;
-    }
+    skipWs();
+    return static_cast<Atom_t>(c - 'a') + 1;
 }
 void AspifTextInput::push(char c) { data_->symbol.push(c); }
 
@@ -341,9 +339,9 @@ void AspifTextInput::matchStr() {
     push('"');
 }
 
-Heuristic_t AspifTextInput::matchHeuMod() {
+DomModifier AspifTextInput::matchHeuMod() {
     auto first = peek();
-    for (const auto& [k, n] : enum_entries<Heuristic_t>()) {
+    for (const auto& [k, n] : enum_entries<DomModifier>()) {
         if (not n.empty() && n[0] == first && ProgramReader::match(n)) {
             skipWs();
             return k;
@@ -391,7 +389,7 @@ struct AspifTextOutput::Data {
 
     void addOutput(const std::string_view& str, const LitSpan& cond) {
         out.push_back(&*strings.try_emplace(str, id_max).first);
-        push(Directive_t::output).push(out.size() - 1).push(cond);
+        push(AspifType::output).push(out.size() - 1).push(cond);
     }
 
     void convertToOutput(StringMap::const_pointer node) {
@@ -400,7 +398,7 @@ struct AspifTextOutput::Data {
                                node->second, node->first.c_str());
             atoms[node->second] = &c_gen_name;
             out.push_back(node);
-            push(Directive_t::output).push(out.size() - 1).push(1).push(node->second);
+            push(AspifType::output).push(out.size() - 1).push(1).push(node->second);
             const_cast<StringMap::pointer>(node)->second = 0;
         }
     }
@@ -546,26 +544,26 @@ void AspifTextOutput::beginStep() {
         data_->startAtom = std::max(size_cast<Atom_t>(data_->atoms), data_->maxGenAtom + 1);
     }
 }
-void AspifTextOutput::rule(Head_t ht, const AtomSpan& head, const LitSpan& body) {
-    data_->push(Directive_t::rule).push(ht).push(head).push(Body_t::normal).push(body);
+void AspifTextOutput::rule(HeadType ht, const AtomSpan& head, const LitSpan& body) {
+    data_->push(AspifType::rule).push(ht).push(head).push(BodyType::normal).push(body);
 }
-void AspifTextOutput::rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits) {
+void AspifTextOutput::rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits) {
     if (lits.empty()) {
         AspifTextOutput::rule(ht, head, {});
     }
-    data_->push(Directive_t::rule).push(ht).push(head);
+    data_->push(AspifType::rule).push(ht).push(head);
     if (std::ranges::adjacent_find(lits, [](const auto& lhs, const auto& rhs) { return lhs.weight != rhs.weight; }) !=
         lits.end()) {
-        data_->push(Body_t::sum).push(bound).push(lits);
+        data_->push(BodyType::sum).push(bound).push(lits);
     }
     else {
         bound = (bound + lits[0].weight - 1) / lits[0].weight;
-        data_->push(Body_t::count).push(bound).push(lits.size());
+        data_->push(BodyType::count).push(bound).push(lits.size());
         for (const auto& wl : lits) { data_->push(Potassco::lit(wl)); }
     }
 }
 void AspifTextOutput::minimize(Weight_t prio, const WeightLitSpan& lits) {
-    data_->push(Directive_t::minimize).push(prio).push(lits);
+    data_->push(AspifType::minimize).push(prio).push(lits);
 }
 void AspifTextOutput::output(const std::string_view& str, const LitSpan& cond) {
     auto atom = cond.size() == 1 && cond.front() > 0 ? Potassco::atom(cond.front()) : 0;
@@ -573,14 +571,14 @@ void AspifTextOutput::output(const std::string_view& str, const LitSpan& cond) {
         data_->addOutput(str, cond);
     }
 }
-void AspifTextOutput::external(Atom_t a, Value_t v) { data_->push(Directive_t::external).push(a).push(v); }
-void AspifTextOutput::assume(const LitSpan& lits) { data_->push(Directive_t::assume).push(lits); }
-void AspifTextOutput::project(const AtomSpan& atoms) { data_->push(Directive_t::project).push(atoms); }
+void AspifTextOutput::external(Atom_t a, TruthValue v) { data_->push(AspifType::external).push(a).push(v); }
+void AspifTextOutput::assume(const LitSpan& lits) { data_->push(AspifType::assume).push(lits); }
+void AspifTextOutput::project(const AtomSpan& atoms) { data_->push(AspifType::project).push(atoms); }
 void AspifTextOutput::acycEdge(int s, int t, const LitSpan& condition) {
-    data_->push(Directive_t::edge).push(s).push(t).push(condition);
+    data_->push(AspifType::edge).push(s).push(t).push(condition);
 }
-void AspifTextOutput::heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& condition) {
-    data_->push(Directive_t::heuristic).push(a).push(condition).push(bias).push(prio).push(t);
+void AspifTextOutput::heuristic(Atom_t a, DomModifier t, int bias, unsigned prio, const LitSpan& condition) {
+    data_->push(AspifType::heuristic).push(a).push(condition).push(bias).push(prio).push(t);
 }
 void AspifTextOutput::theoryTerm(Id_t termId, int number) { data_->theory.addTerm(termId, number); }
 void AspifTextOutput::theoryTerm(Id_t termId, const std::string_view& name) { data_->theory.addTerm(termId, name); }
@@ -589,7 +587,7 @@ void AspifTextOutput::theoryTerm(Id_t termId, int compound, const IdSpan& args)
         data_->theory.addTerm(termId, static_cast<Id_t>(compound), args);
     }
     else {
-        data_->theory.addTerm(termId, Potassco::enum_cast<Tuple_t>(compound).value(), args);
+        data_->theory.addTerm(termId, Potassco::enum_cast<TupleType>(compound).value(), args);
     }
 }
 void AspifTextOutput::theoryElement(Id_t id, const IdSpan& terms, const LitSpan& cond) {
@@ -604,13 +602,13 @@ void AspifTextOutput::theoryAtom(Id_t atomOrZero, Id_t termId, const IdSpan& ele
 
 std::ostream& AspifTextOutput::Data::appendTerm(std::ostream& os, Id_t tId) const {
     const auto& term = theory.getTerm(tId);
-    if (term.type() == Theory_t::number) {
+    if (term.type() == TheoryTermType::number) {
         return os << term.number();
     }
-    if (term.type() == Theory_t::symbol) {
+    if (term.type() == TheoryTermType::symbol) {
         return os << term.symbol();
     }
-    POTASSCO_CHECK_PRE(term.type() == Theory_t::compound);
+    POTASSCO_CHECK_PRE(term.type() == TheoryTermType::compound);
     if (term.isFunction()) {
         const auto* fSym = theory.getTerm(term.function()).symbol();
         if (term.size() <= 2 && std::strchr("/!<=>+-*\\?&@|:;~^.", *fSym)) {
@@ -623,7 +621,7 @@ std::ostream& AspifTextOutput::Data::appendTerm(std::ostream& os, Id_t tId) cons
         }
         os << fSym;
     }
-    auto parens = Potassco::parens(term.isTuple() ? term.tuple() : Potassco::Tuple_t::paren);
+    auto parens = Potassco::parens(term.isTuple() ? term.tuple() : TupleType::paren);
     auto sep    = ""sv;
     os << parens.substr(0, 1);
     for (auto e : term) { appendTerm(os << std::exchange(sep, ", "sv), e); }
@@ -722,11 +720,11 @@ void AspifTextOutput::Data::endStep(std::ostream& os, bool more) {
     visitTheoryAtoms(os);
     for (const auto *pos = directives.data(), *end = pos + directives.size(); pos != end;) {
         const auto *sep = "", *term = ".";
-        switch (next<Directive_t>(pos)) {
+        switch (next<AspifType>(pos)) {
             default: POTASSCO_ASSERT_NOT_REACHED("unexpected directive");
-            case Directive_t::rule:
+            case AspifType::rule:
                 term = "";
-                if (next<Head_t>(pos) == Head_t::choice) {
+                if (next<HeadType>(pos) == HeadType::choice) {
                     os << "{";
                     term = "}";
                 }
@@ -739,27 +737,27 @@ void AspifTextOutput::Data::endStep(std::ostream& os, bool more) {
                     os << ":- ";
                 }
                 term = ".";
-                switch (auto bt = next<Body_t>(pos)) {
-                    case Body_t::normal: printCondition(os, pos, sep); break;
-                    case Body_t::count : // fall through
-                    case Body_t::sum   : printAggregate(os << sep, pos, bt == Body_t::sum); break;
-                    default            : break;
+                switch (auto bt = next<BodyType>(pos)) {
+                    case BodyType::normal: printCondition(os, pos, sep); break;
+                    case BodyType::count : // fall through
+                    case BodyType::sum   : printAggregate(os << sep, pos, bt == BodyType::sum); break;
+                    default              : break;
                 }
                 break;
-            case Directive_t::minimize: printMinimize(os, pos); break;
-            case Directive_t::project : printCondition(os << "#project{", pos) << '}'; break;
-            case Directive_t::output:
+            case AspifType::minimize: printMinimize(os, pos); break;
+            case AspifType::project : printCondition(os << "#project{", pos) << '}'; break;
+            case AspifType::output:
                 printCondition(os << "#show " << out.at(next(pos))->first.view(), pos, " : ");
                 break;
-            case Directive_t::external:
+            case AspifType::external:
                 printName(os << "#external ", next<Atom_t>(pos));
-                if (auto v = next<Value_t>(pos); v != Value_t::false_) {
+                if (auto v = next<TruthValue>(pos); v != TruthValue::false_) {
                     os << ". [" << enum_name(v) << "]";
                     term = "";
                 }
                 break;
-            case Directive_t::assume: printCondition(os << "#assume{", pos) << '}'; break;
-            case Directive_t::heuristic:
+            case AspifType::assume: printCondition(os << "#assume{", pos) << '}'; break;
+            case AspifType::heuristic:
                 term = "";
                 os << "#heuristic ";
                 printName(os, next<Atom_t>(pos));
@@ -767,9 +765,9 @@ void AspifTextOutput::Data::endStep(std::ostream& os, bool more) {
                 if (auto p = next(pos)) {
                     os << "@" << p;
                 }
-                os << ", " << Potassco::enum_name(next<Heuristic_t>(pos)) << "]";
+                os << ", " << Potassco::enum_name(next<DomModifier>(pos)) << "]";
                 break;
-            case Directive_t::edge:
+            case AspifType::edge:
                 os << "#edge(" << next<int32_t>(pos) << ",";
                 os << next<int32_t>(pos) << ")";
                 printCondition(os, pos, " : ");
diff --git a/src/clingo.cpp b/src/clingo.cpp
index 20a73fe..34881c0 100644
--- a/src/clingo.cpp
+++ b/src/clingo.cpp
@@ -30,9 +30,9 @@ AbstractHeuristic::~AbstractHeuristic()   = default;
 AbstractStatistics::~AbstractStatistics() = default;
 
 auto AbstractAssignment::isTotal() const -> bool { return unassigned() == 0u; }
-auto AbstractAssignment::isFixed(Lit_t lit) const -> bool { return value(lit) != Value_t::free && level(lit) == 0; }
-auto AbstractAssignment::isTrue(Lit_t lit) const -> bool { return value(lit) == Value_t::true_; }
-auto AbstractAssignment::isFalse(Lit_t lit) const -> bool { return value(lit) == Value_t::false_; }
+auto AbstractAssignment::isFixed(Lit_t lit) const -> bool { return value(lit) != TruthValue::free && level(lit) == 0; }
+auto AbstractAssignment::isTrue(Lit_t lit) const -> bool { return value(lit) == TruthValue::true_; }
+auto AbstractAssignment::isFalse(Lit_t lit) const -> bool { return value(lit) == TruthValue::false_; }
 auto AbstractAssignment::trailEnd(uint32_t lev) const -> uint32_t {
     return lev < level() ? trailBegin(lev + 1) : trailSize();
 }
diff --git a/src/convert.cpp b/src/convert.cpp
index 1486529..0f236da 100644
--- a/src/convert.cpp
+++ b/src/convert.cpp
@@ -62,20 +62,20 @@ struct SmodelsConvert::SmData {
         return scratch.view();
     }
     struct Atom {
-        Atom() : smId(0), head(0), show(0), extn(0) {}
-        std::string_view makePred(ScratchType& scratch) const { return SmData::makePred(scratch, "_atom"sv, smId); }
-        operator Atom_t() const { return smId; }
-        uint32_t smId : 28; // corresponding smodels atom
-        uint32_t head : 1;  // atom occurs in a head of a rule
-        uint32_t show : 1;  // atom has a name
-        uint32_t extn : 2;  // value if atom is external
+        std::string_view     makePred(ScratchType& scratch) const { return SmData::makePred(scratch, "_atom"sv, smId); }
+        [[nodiscard]] Atom_t sm() const { return smId; }
+
+        uint32_t smId : 28 {0}; // corresponding smodels atom
+        uint32_t head : 1 {0};  // atom occurs in a head of a rule
+        uint32_t show : 1 {0};  // atom has a name
+        uint32_t extn : 2 {0};  // value if atom is external
     };
     struct Heuristic {
         std::string_view makePred(ScratchType& scratch, std::string_view atomName) const {
             return SmData::makePred(scratch, "_heuristic"sv, atomName, enum_name(type), bias, prio);
         }
         Atom_t      atom;
-        Heuristic_t type;
+        DomModifier type;
         int         bias{};
         unsigned    prio{};
         unsigned    cond{};
@@ -87,7 +87,7 @@ struct SmodelsConvert::SmData {
             int32_t s;
             int32_t t;
         };
-        Output(SymTab::iterator it) : atom(it->first), type(type_name), name(&it->second) {}
+        explicit Output(SymTab::iterator it) : atom(it->first), type(type_name), name(&it->second) {}
         Output(Atom_t a, int32_t s, int32_t t) : atom(a), type(type_edge), edge{s, t} {}
         std::string_view makePred(ScratchType& scratch) const {
             return type == type_name ? name->view() : SmData::makePred(scratch, "_edge"sv, edge.s, edge.t);
@@ -100,11 +100,11 @@ struct SmodelsConvert::SmData {
         };
     };
     static_assert(amc::is_trivially_relocatable_v<Atom> && amc::is_trivially_relocatable_v<Atom_t> &&
-                  amc::is_trivially_relocatable_v<Lit_t> && amc::is_trivially_relocatable_v<WeightLit_t> &&
+                  amc::is_trivially_relocatable_v<Lit_t> && amc::is_trivially_relocatable_v<WeightLit> &&
                   amc::is_trivially_relocatable_v<Heuristic> && amc::is_trivially_relocatable_v<Output>);
     using AtomMap = amc::vector<Atom>;
     using AtomVec = amc::vector<Atom_t>;
-    using WLitVec = amc::vector<WeightLit_t>;
+    using WLitVec = amc::vector<WeightLit>;
     using HeuVec  = amc::vector<Heuristic>;
     using OutVec  = amc::vector<Output>;
     struct Minimize {
@@ -114,10 +114,10 @@ struct SmodelsConvert::SmData {
         unsigned startPos;
         unsigned endPos;
     };
-    static_assert(amc::is_trivially_relocatable_v<Minimize>);
-    using MinSet                       = amc::vector<Minimize>;
     static constexpr Atom_t false_atom = 1;
-    SmData() : next(2) {}
+    static_assert(amc::is_trivially_relocatable_v<Minimize>);
+    using MinSet = amc::vector<Minimize>;
+    SmData()     = default;
     Atom_t newAtom() { return next++; }
     bool   mapped(Atom_t a) const { return a < atoms.size() && atoms[a].smId != 0; }
     Atom&  mapAtom(Atom_t a) {
@@ -131,19 +131,19 @@ struct SmodelsConvert::SmData {
         return atoms[a];
     }
     Lit_t mapLit(Lit_t in) {
-        auto x = static_cast<Lit_t>(mapAtom(atom(in)));
+        auto x = static_cast<Lit_t>(mapAtom(atom(in)).sm());
         return in < 0 ? -x : x;
     }
-    WeightLit_t mapLit(WeightLit_t in) {
+    WeightLit mapLit(WeightLit in) {
         in.lit = mapLit(in.lit);
         return in;
     }
     Atom_t mapHeadAtom(Atom_t a) {
         Atom& x = mapAtom(a);
         x.head  = 1;
-        return x;
+        return x.sm();
     }
-    RuleBuilder& mapHead(const AtomSpan& h, Head_t ht = Head_t::disjunctive) {
+    RuleBuilder& mapHead(const AtomSpan& h, HeadType ht = HeadType::disjunctive) {
         rule.clear().start(ht);
         for (auto a : h) { rule.addHead(mapHeadAtom(a)); }
         if (h.empty()) {
@@ -179,13 +179,13 @@ struct SmodelsConvert::SmData {
         }
         vec.endPos = minLits.size();
     }
-    void addExternal(Atom_t a, Value_t v) {
+    void addExternal(Atom_t a, TruthValue v) {
         if (auto& ma = mapAtom(a); not ma.head) {
             ma.extn = static_cast<unsigned>(v);
             external.push_back(a);
         }
     }
-    void addHeuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, Atom_t cond) {
+    void addHeuristic(Atom_t a, DomModifier t, int bias, unsigned prio, Atom_t cond) {
         Heuristic h = {a, t, bias, prio, cond};
         heuristic.push_back(h);
     }
@@ -205,7 +205,7 @@ struct SmodelsConvert::SmData {
     WLitVec     minLits;   // minimize literals
     OutVec      output;    // list of output atoms not yet processed
     RuleBuilder rule;      // active (mapped) rule
-    Atom_t      next;      // next unused output atom
+    Atom_t      next{2};   // next unused output atom
 };
 /////////////////////////////////////////////////////////////////////////////////////////
 // SmodelsConvert
@@ -233,14 +233,14 @@ Atom_t   SmodelsConvert::makeAtom(const LitSpan& cond, bool named) {
 }
 void SmodelsConvert::initProgram(bool inc) { out_.initProgram(inc); }
 void SmodelsConvert::beginStep() { out_.beginStep(); }
-void SmodelsConvert::rule(Head_t ht, const AtomSpan& head, const LitSpan& body) {
-    if (not head.empty() || ht == Head_t::disjunctive) {
+void SmodelsConvert::rule(HeadType ht, const AtomSpan& head, const LitSpan& body) {
+    if (not head.empty() || ht == HeadType::disjunctive) {
         data_->mapHead(head, ht).startBody();
         data_->mapBody(body).end(&out_);
     }
 }
-void SmodelsConvert::rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) {
-    if (not head.empty() || ht == Head_t::disjunctive) {
+void SmodelsConvert::rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) {
+    if (not head.empty() || ht == HeadType::disjunctive) {
         POTASSCO_CHECK_PRE(std::ranges::none_of(body, [](const auto wl) { return weight(wl) < 0; }),
                            "negative weights in body are not supported");
         if (bound <= 0) {
@@ -251,13 +251,13 @@ void SmodelsConvert::rule(Head_t ht, const AtomSpan& head, Weight_t bound, const
         data_->mapBody(body);
         auto mHead = data_->rule.head();
         auto mBody = data_->rule.sum().lits;
-        if (ht == Head_t::disjunctive && mHead.size() == 1) {
+        if (ht == HeadType::disjunctive && mHead.size() == 1) {
             data_->rule.end(&out_);
             return;
         }
         auto auxH = data_->newAtom();
         auto auxB = lit(auxH);
-        out_.rule(Head_t::disjunctive, toSpan(auxH), bound, mBody);
+        out_.rule(HeadType::disjunctive, toSpan(auxH), bound, mBody);
         out_.rule(ht, mHead, toSpan(auxB));
     }
 }
@@ -268,8 +268,8 @@ void SmodelsConvert::output(const std::string_view& str, const LitSpan& cond) {
     data_->addOutput(makeAtom(cond, true), str);
 }
 
-void SmodelsConvert::external(Atom_t a, Value_t v) { data_->addExternal(a, v); }
-void SmodelsConvert::heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& cond) {
+void SmodelsConvert::external(Atom_t a, TruthValue v) { data_->addExternal(a, v); }
+void SmodelsConvert::heuristic(Atom_t a, DomModifier t, int bias, unsigned prio, const LitSpan& cond) {
     if (not ext_) {
         out_.heuristic(a, t, bias, prio, cond);
     }
@@ -321,25 +321,25 @@ void SmodelsConvert::flushExternal() {
     data_->rule.clear();
     for (auto ext : data_->external) {
         SmData::Atom& a  = data_->mapAtom(ext);
-        auto          vt = static_cast<Value_t>(a.extn);
+        auto          vt = static_cast<TruthValue>(a.extn);
         if (not ext_) {
             if (a.head) {
                 continue;
             }
-            Atom_t at = a;
-            if (vt == Value_t::free) {
+            Atom_t at = a.sm();
+            if (vt == TruthValue::free) {
                 data_->rule.addHead(at);
             }
-            else if (vt == Value_t::true_) {
-                out_.rule(Head_t::disjunctive, toSpan(at), trueBody);
+            else if (vt == TruthValue::true_) {
+                out_.rule(HeadType::disjunctive, toSpan(at), trueBody);
             }
         }
         else {
-            out_.external(a, vt);
+            out_.external(a.sm(), vt);
         }
     }
     if (auto head = data_->rule.head(); not head.empty()) {
-        out_.rule(Head_t::choice, head, trueBody);
+        out_.rule(HeadType::choice, head, trueBody);
     }
 }
 void SmodelsConvert::flushHeuristic() {
@@ -355,7 +355,7 @@ void SmodelsConvert::flushHeuristic() {
         auto          it = ma.show ? data_->symTab.find(ma.smId) : data_->symTab.end();
         if (it == data_->symTab.end()) {
             ma.show = 1;
-            it      = data_->addOutput(ma, ma.makePred(scratch));
+            it      = data_->addOutput(ma.sm(), ma.makePred(scratch));
         }
         auto c = static_cast<Lit_t>(heu.cond);
         out_.output(heu.makePred(scratch, it->second.view()), toSpan(c));
diff --git a/src/error.cpp b/src/error.cpp
index b2c35c4..e5ee98f 100644
--- a/src/error.cpp
+++ b/src/error.cpp
@@ -91,11 +91,11 @@ static void appendExpression(std::span<char>& span, const ExpressionInfo& info,
 constinit AbortHandler g_abortHandler = nullptr;
 extern AbortHandler    setAbortHandler(AbortHandler handler) { return std::exchange(g_abortHandler, handler); }
 
-extern void failAbort(const ExpressionInfo& info, const char* fmt, ...) {
-    char            message[1024];
-    std::span<char> span(message, std::size(message) - 1);
-    auto            hasMessage = fmt && *fmt;
-    appendExpression(span, info, true, "Assertion"sv, hasMessage);
+extern void failAbort(const ExpressionInfo& expressionInfo, const char* fmt, ...) {
+    char      message[1024];
+    std::span span(message, std::size(message) - 1);
+    auto      hasMessage = fmt && *fmt;
+    appendExpression(span, expressionInfo, true, "Assertion"sv, hasMessage);
     if (hasMessage) {
         va_list args;
         va_start(args, fmt);
@@ -112,16 +112,16 @@ extern void failAbort(const ExpressionInfo& info, const char* fmt, ...) {
     std::abort();
 }
 
-extern void failThrow(Errc ec, const ExpressionInfo& info, const char* fmt, ...) {
+extern void failThrow(Errc ec, const ExpressionInfo& expressionInfo, const char* fmt, ...) {
     if (ec == Errc::bad_alloc) {
         throw std::bad_alloc();
     }
 
-    char            message[1024];
-    std::span<char> span(message, std::size(message) - 1);
-    auto            hasMessage = fmt && *fmt;
+    char      message[1024];
+    std::span span(message, std::size(message) - 1);
+    auto      hasMessage = fmt && *fmt;
     if (ec == Errc::precondition_fail) {
-        appendExpression(span, info, false, "Precondition"sv, hasMessage);
+        appendExpression(span, expressionInfo, false, "Precondition"sv, hasMessage);
     }
     auto next = std::string_view{};
     if (hasMessage) {
@@ -140,7 +140,7 @@ extern void failThrow(Errc ec, const ExpressionInfo& info, const char* fmt, ...)
     append(span, next);
     append(span, std::generic_category().message(static_cast<int>(ec)));
     append(span, "\n");
-    appendExpression(span, info, false, info.expression.empty() ? ""sv : "check"sv, false);
+    appendExpression(span, expressionInfo, false, expressionInfo.expression.empty() ? ""sv : "check"sv, false);
     *span.data() = 0;
     switch (ec) {
         // logic
@@ -150,7 +150,7 @@ extern void failThrow(Errc ec, const ExpressionInfo& info, const char* fmt, ...)
         case Errc::out_of_range    : throw std::out_of_range(message);
         // runtime
         case Errc::overflow_error: throw std::overflow_error(message);
-        default                  : throw RuntimeError(ec, info.location, message);
+        default                  : throw RuntimeError(ec, expressionInfo.location, message);
     }
 }
 
diff --git a/src/match_basic_types.cpp b/src/match_basic_types.cpp
index bb3da02..7c461ca 100644
--- a/src/match_basic_types.cpp
+++ b/src/match_basic_types.cpp
@@ -40,9 +40,9 @@ void AbstractProgram::project(const AtomSpan&) { POTASSCO_UNSUPPORTED("projectio
 void AbstractProgram::output(const std::string_view&, const LitSpan&) {
     POTASSCO_UNSUPPORTED("output directive not supported");
 }
-void AbstractProgram::external(Atom_t, Value_t) { POTASSCO_UNSUPPORTED("external directive not supported"); }
+void AbstractProgram::external(Atom_t, TruthValue) { POTASSCO_UNSUPPORTED("external directive not supported"); }
 void AbstractProgram::assume(const LitSpan&) { POTASSCO_UNSUPPORTED("assumption directive not supported"); }
-void AbstractProgram::heuristic(Atom_t, Heuristic_t, int, unsigned, const LitSpan&) {
+void AbstractProgram::heuristic(Atom_t, DomModifier, int, unsigned, const LitSpan&) {
     POTASSCO_UNSUPPORTED("heuristic directive not supported");
 }
 void AbstractProgram::acycEdge(int, int, const LitSpan&) { POTASSCO_UNSUPPORTED("edge directive not supported"); }
@@ -110,7 +110,7 @@ bool BufferedStream::unget(char c) {
     if (not rpos_) {
         return false;
     }
-    if ((buf_[--rpos_] = c) == '\n') {
+    if (buf_[--rpos_] = c; c == '\n') {
         --line_;
     }
     return true;
@@ -124,7 +124,7 @@ bool BufferedStream::match(std::string_view w) {
         rpos_ = 0;
     }
     if (std::strncmp(w.data(), buf_ + rpos_, w.length()) == 0) {
-        if (not buf_[rpos_ += w.length()]) {
+        if (rpos_ += w.length(); not buf_[rpos_]) {
             underflow();
         }
         return true;
@@ -178,7 +178,7 @@ bool ProgramReader::accept(std::istream& str) {
     return doAttach(inc_);
 }
 bool ProgramReader::incremental() const { return inc_; }
-bool ProgramReader::parse(ReadMode m) {
+bool ProgramReader::parse(ReadMode r) {
     POTASSCO_CHECK_PRE(str_ != nullptr, "no input stream");
     do {
         if (not doParse()) {
@@ -186,7 +186,7 @@ bool ProgramReader::parse(ReadMode m) {
         }
         skipWs();
         require(not more() || incremental(), "invalid extra input");
-    } while (m == read_complete && more());
+    } while (r == read_complete && more());
     return true;
 }
 bool ProgramReader::more() { return str_ && (str_->skipWs(), not str_->end()); }
@@ -262,13 +262,13 @@ DynamicBuffer::DynamicBuffer(DynamicBuffer&& other) noexcept
     , size_(std::exchange(other.size_, 0)) {}
 DynamicBuffer::DynamicBuffer(const DynamicBuffer& other) : DynamicBuffer() { append(other.data(), other.size_); }
 DynamicBuffer::~DynamicBuffer() { release(); }
-DynamicBuffer& DynamicBuffer::operator=(Potassco::DynamicBuffer&& other) noexcept {
+DynamicBuffer& DynamicBuffer::operator=(DynamicBuffer&& other) noexcept {
     if (this != &other) {
         DynamicBuffer(std::move(other)).swap(*this);
     }
     return *this;
 }
-DynamicBuffer& DynamicBuffer::operator=(const Potassco::DynamicBuffer& other) {
+DynamicBuffer& DynamicBuffer::operator=(const DynamicBuffer& other) {
     if (this != &other) {
         DynamicBuffer(other).swap(*this);
     }
@@ -356,16 +356,19 @@ auto DynamicBitset::compare(const DynamicBitset& other) const -> std::strong_ord
 /////////////////////////////////////////////////////////////////////////////////////////
 // ConstString
 /////////////////////////////////////////////////////////////////////////////////////////
+using RefCount = std::atomic<int32_t>;
 ConstString::ConstString(std::string_view n, CreateMode m) {
     if (n.size() > c_max_small) {
         storage_[c_max_small] = static_cast<char>(c_large_tag + m);
-        auto* buf             = new char[(m == create_shared ? sizeof(std::atomic<int32_t>) : 0) + n.size() + 1];
+        auto  mem             = std::make_unique<char[]>((m == create_shared ? sizeof(RefCount) : 0) + n.size() + 1);
+        auto* buf             = mem.get();
         if (m == create_shared) {
-            new (buf) std::atomic<int32_t>(1);
-            buf += sizeof(std::atomic<int32_t>);
+            new (buf) RefCount(1);
+            buf += sizeof(RefCount);
         }
         *std::ranges::copy(n, buf).out = 0;
         new (storage_) Large{.str = buf, .size = n.size()};
+        mem.release();
     }
     else {
         *std::ranges::copy(n, storage_).out = 0;
@@ -389,13 +392,13 @@ ConstString& ConstString::operator=(const ConstString& other) {
     return *this;
 }
 void ConstString::release() {
-    if (not shareable() || addRef(-1) == 0) {
-        delete[] (large()->str - (shareable() * sizeof(std::atomic<int32_t>)));
+    if (auto off = shareable() * sizeof(RefCount); off == 0 || addRef(-1) == 0) {
+        delete[] (large()->str - off);
     }
 }
 int32_t ConstString::addRef(int32_t x) {
     POTASSCO_DEBUG_ASSERT(shareable());
-    auto& r   = *reinterpret_cast<std::atomic<int32_t>*>(large()->str - sizeof(std::atomic<int32_t>));
+    auto& r   = *reinterpret_cast<RefCount*>(large()->str - sizeof(RefCount));
     return r += x;
 }
 
diff --git a/src/program_options.cpp b/src/program_options.cpp
index e57ec6f..84e3e7f 100644
--- a/src/program_options.cpp
+++ b/src/program_options.cpp
@@ -41,13 +41,13 @@ namespace Potassco::ProgramOptions {
 ///////////////////////////////////////////////////////////////////////////////
 // DefaultFormat
 ///////////////////////////////////////////////////////////////////////////////
-std::size_t DefaultFormat::format(std::string& buf, const Option& o, std::size_t maxW) {
+std::size_t DefaultFormat::format(std::string& buffer, const Option& o, std::size_t maxW) {
     auto        bufSize = std::max(maxW, o.maxColumn()) + 3;
     const auto* arg     = o.argName();
     auto        np      = ""sv;
     auto        ap      = ""sv;
     if (o.value()->isNegatable()) {
-        if (!*arg) {
+        if (not *arg) {
             np = "[no-]"sv;
         }
         else {
@@ -55,43 +55,43 @@ std::size_t DefaultFormat::format(std::string& buf, const Option& o, std::size_t
             bufSize += ap.size();
         }
     }
-    const auto startSize = buf.size();
-    buf.reserve(startSize + bufSize);
-    buf.append("  --"sv).append(np).append(o.name());
+    const auto startSize = buffer.size();
+    buffer.reserve(startSize + bufSize);
+    buffer.append("  --"sv).append(np).append(o.name());
     if (o.value()->isImplicit() && *arg) {
-        buf.append("[="sv).append(arg).append(ap).append("]"sv);
+        buffer.append("[="sv).append(arg).append(ap).append("]"sv);
     }
     if (auto c = o.alias(); c) {
-        buf.append(",-"sv).append(1, c);
+        buffer.append(",-"sv).append(1, c);
     }
     if (not o.value()->isImplicit()) {
-        buf.append(1, not o.alias() ? '=' : ' ').append(arg).append(ap);
+        buffer.append(1, not o.alias() ? '=' : ' ').append(arg).append(ap);
     }
-    if (auto sz = buf.size() - startSize; sz < maxW) {
-        buf.append(maxW - sz, ' ');
+    if (auto sz = buffer.size() - startSize; sz < maxW) {
+        buffer.append(maxW - sz, ' ');
     }
-    return buf.size() - startSize;
+    return buffer.size() - startSize;
 }
-std::size_t DefaultFormat::format(std::string& buf, const char* desc, const Value& val, std::size_t) {
+std::size_t DefaultFormat::format(std::string& buffer, const char* desc, const Value& val, std::size_t) {
     std::size_t minS = strlen(desc);
     const char* temp = nullptr;
     if (not desc) {
         desc = "";
     }
 
-    const auto startSize = buf.size();
-    buf.reserve(startSize + minS + 2);
-    buf.append(1, ':').append(1, ' ');
+    const auto startSize = buffer.size();
+    buffer.reserve(startSize + minS + 2);
+    buffer.append(1, ':').append(1, ' ');
     for (const char* look;; ++desc) {
         look = desc;
         while (*look && *look != '%') { ++look; }
         if (look != desc) {
-            buf.append(desc, look);
+            buffer.append(desc, look);
         }
-        if (!*look++ || !*look) {
+        if (not *look++ || not *look) {
             break;
         }
-        else if (*look == 'D') {
+        if (*look == 'D') {
             temp = val.defaultsTo();
         }
         else if (*look == 'A') {
@@ -101,16 +101,16 @@ std::size_t DefaultFormat::format(std::string& buf, const char* desc, const Valu
             temp = val.implicit();
         }
         else {
-            buf.push_back(*look);
+            buffer.push_back(*look);
         }
         if (temp) {
-            buf.append(temp);
+            buffer.append(temp);
         }
         desc = look;
         temp = nullptr;
     }
-    buf.push_back('\n');
-    return buf.size() - startSize;
+    buffer.push_back('\n');
+    return buffer.size() - startSize;
 }
 std::size_t DefaultFormat::format(std::string& buffer, const OptionGroup& grp) {
     const auto startSize = buffer.size();
@@ -150,18 +150,18 @@ const char* Value::arg() const {
     return isFlag() ? "" : "<arg>";
 }
 
-Value* Value::desc(DescType t, const char* n) {
-    if (n == nullptr) {
+Value* Value::desc(DescType t, const char* d) {
+    if (d == nullptr) {
         return this;
     }
     if (t == desc_implicit) {
         implicit_ = 1;
-        if (!*n) {
+        if (not *d) {
             return this;
         }
     }
     if (descFlag_ == 0 || descFlag_ == t) {
-        desc_.value = n;
+        desc_.value = d;
         descFlag_   = static_cast<uint8_t>(t);
         return this;
     }
@@ -173,7 +173,7 @@ Value* Value::desc(DescType t, const char* n) {
         descFlag_                                     = desc_pack;
         desc_.pack[oldKey]                            = oldVal;
     }
-    desc_.pack[t >> 1u] = n;
+    desc_.pack[t >> 1u] = d;
     return this;
 }
 const char* Value::desc(DescType t) const {
@@ -296,7 +296,7 @@ OptionInitHelper& OptionInitHelper::operator()(const char* name, Value* val, con
                 ++x;
             }
         }
-        if (!*n || *x || level > desc_level_hidden) {
+        if (not *n || *x || level > desc_level_hidden) {
             throw Error(std::string("Invalid Key '").append(name).append("'"));
         }
         val->level(static_cast<DescriptionLevel>(level));
@@ -318,11 +318,11 @@ OptionInitHelper& OptionInitHelper::operator()(const char* name, Value* val, con
 ///////////////////////////////////////////////////////////////////////////////
 // class OptionContext
 ///////////////////////////////////////////////////////////////////////////////
-OptionContext::OptionContext(std::string_view cap, DescriptionLevel def) : caption_(cap), descLevel_(def) {}
+OptionContext::OptionContext(std::string_view caption, DescriptionLevel def) : caption_(caption), descLevel_(def) {}
 
-const std::string& OptionContext::caption() const { return caption_; }
-void               OptionContext::setActiveDescLevel(DescriptionLevel x) { descLevel_ = std::min(x, desc_level_all); }
-size_t             OptionContext::findGroupKey(const std::string& name) const {
+auto   OptionContext::caption() const -> const std::string& { return caption_; }
+void   OptionContext::setActiveDescLevel(DescriptionLevel level) { descLevel_ = std::min(level, desc_level_all); }
+size_t OptionContext::findGroupKey(const std::string& name) const {
     for (size_t i = 0; i != groups_.size(); ++i) {
         if (groups_[i].caption() == name) {
             return i;
@@ -331,22 +331,22 @@ size_t             OptionContext::findGroupKey(const std::string& name) const {
     return static_cast<size_t>(-1);
 }
 
-OptionContext& OptionContext::add(const OptionGroup& options) {
-    size_t k = findGroupKey(options.caption());
+OptionContext& OptionContext::add(const OptionGroup& group) {
+    size_t k = findGroupKey(group.caption());
     if (k >= groups_.size()) {
         // add as new group
         k = groups_.size();
-        groups_.emplace_back(options.caption(), options.descLevel());
+        groups_.emplace_back(group.caption(), group.descLevel());
     }
-    for (const auto& opt : options) { insertOption(k, opt); }
-    groups_[k].setDescriptionLevel(std::min(options.descLevel(), groups_[k].descLevel()));
+    for (const auto& opt : group) { insertOption(k, opt); }
+    groups_[k].setDescriptionLevel(std::min(group.descLevel(), groups_[k].descLevel()));
     return *this;
 }
 
 OptionContext& OptionContext::addAlias(const std::string& aliasName, option_iterator option) {
     if (option != end() && not aliasName.empty()) {
-        auto k = static_cast<KeyType>(option - begin());
-        if (not index_.insert(Name2Key::value_type(aliasName, k)).second) {
+        if (auto k = static_cast<KeyType>(option - begin());
+            not index_.insert(Name2Key::value_type(aliasName, k)).second) {
             throw DuplicateOption(caption(), aliasName);
         }
     }
@@ -354,8 +354,7 @@ OptionContext& OptionContext::addAlias(const std::string& aliasName, option_iter
 }
 
 const OptionGroup& OptionContext::findGroup(const std::string& name) const {
-    std::size_t x = findGroupKey(name);
-    if (x < groups_.size()) {
+    if (std::size_t x = findGroupKey(name); x < groups_.size()) {
         return groups_[x];
     }
     throw ContextError(caption(), ContextError::unknown_group, name);
@@ -377,16 +376,12 @@ void OptionContext::insertOption(size_t groupId, const SharedOptPtr& opt) {
     const string& l = opt->name();
     KeyType       k(options_.size());
     if (opt->alias()) {
-        char        sName[2] = {'-', opt->alias()};
-        std::string shortName(sName, 2);
-        if (not index_.insert(Name2Key::value_type(shortName, k)).second) {
+        if (char sName[2] = {'-', opt->alias()}; not index_.try_emplace({sName, 2}, k).second) {
             throw DuplicateOption(caption(), l);
         }
     }
-    if (not l.empty()) {
-        if (not index_.insert(Name2Key::value_type(l, k)).second) {
-            throw DuplicateOption(caption(), l);
-        }
+    if (not l.empty() && not index_.try_emplace(l, k).second) {
+        throw DuplicateOption(caption(), l);
     }
     options_.push_back(opt);
     groups_[groupId].options_.push_back(opt);
@@ -639,11 +634,10 @@ class CommandLineParser : public OptionParser {
         // either -o value or -o[value|opts]
         char optn[2];
         optn[1] = '\0';
-        SharedOptPtr o;
         while (*optName) {
             optn[0]         = *optName;
             const char* val = optName + 1;
-            if ((o = getOption(optn, OptionContext::find_alias)).get()) {
+            if (auto o = getOption(optn, OptionContext::find_alias); o.get()) {
                 if (o->value()->isImplicit()) {
                     // -ovalue or -oopts
                     if (not o->value()->isFlag()) {
@@ -651,14 +645,12 @@ class CommandLineParser : public OptionParser {
                         addOptionValue(o, val);
                         return true;
                     }
-                    else {
-                        // -o + more options
-                        addOptionValue(o, "");
-                        ++optName;
-                    }
+                    // -o + more options
+                    addOptionValue(o, "");
+                    ++optName;
                 }
-                else if (*val != 0 || (val = next()) != nullptr) {
-                    // -ovalue or -o value
+                else if (val = *val == 0 ? next() : val; val) {
+                    //  -ovalue or -o value
                     addOptionValue(o, val);
                     return true;
                 }
@@ -673,10 +665,9 @@ class CommandLineParser : public OptionParser {
         return true;
     }
     bool handleLongOpt(const char* optName) {
-        string            name(optName);
-        string            value;
-        string::size_type p = name.find('=');
-        if (p != string::npos) {
+        string name(optName);
+        string value;
+        if (auto p = name.find('='); p != string::npos) {
             value.assign(name, p + 1, string::npos);
             name.erase(p, string::npos);
         }
@@ -686,7 +677,8 @@ class CommandLineParser : public OptionParser {
             try {
                 on = getOption(optName + 3, OptionContext::find_name_or_prefix);
             }
-            catch (...) {
+            catch (...) { // NOLINT(*-empty-catch)
+                // ignore - will try name next.
             }
             if (on.get() && not on->value()->isNegatable()) {
                 on.reset();
@@ -730,7 +722,6 @@ class ArgvParser : public CommandLineParser {
 public:
     ArgvParser(ParseContext& ctx, int startPos, int endPos, const char* const* argv, unsigned cmdFlags)
         : CommandLineParser(ctx, cmdFlags)
-        , currentArg_(nullptr)
         , argPos_(startPos)
         , endPos_(endPos)
         , argv_(argv) {}
@@ -740,7 +731,7 @@ class ArgvParser : public CommandLineParser {
         currentArg_ = argPos_ != endPos_ ? argv_[argPos_++] : nullptr;
         return currentArg_;
     }
-    const char*        currentArg_;
+    const char*        currentArg_{nullptr};
     int                argPos_;
     int                endPos_;
     const char* const* argv_;
@@ -759,12 +750,13 @@ class CommandStringParser : public CommandLineParser {
     const char* next() override {
         // skip leading white
         while (std::isspace(static_cast<unsigned char>(*cmd_))) { ++cmd_; }
-        if (!*cmd_) {
+        if (not *cmd_) {
             return nullptr;
         }
         tok_.clear();
+        static constexpr std::string_view special{"\"'\\"};
         // find end of current arg
-        for (char c, t = ' ', n; (c = *cmd_) != 0; ++cmd_) {
+        for (char c, t = ' '; (c = *cmd_) != 0; ++cmd_) {
             if (c == t) {
                 if (t == ' ') {
                     break;
@@ -774,15 +766,12 @@ class CommandStringParser : public CommandLineParser {
             else if ((c == '\'' || c == '"') && t == ' ') {
                 t = c;
             }
-            else if (c != '\\') {
+            else if (c != '\\' || special.find(cmd_[1]) == std::string_view::npos) {
                 tok_ += c;
             }
-            else if ((n = cmd_[1]) == '"' || n == '\'' || n == '\\') {
-                tok_ += n;
-                ++cmd_;
-            }
             else {
-                tok_ += c;
+                tok_ += cmd_[1];
+                ++cmd_;
             }
         }
         return tok_.c_str();
@@ -824,25 +813,24 @@ class CfgFileParser : public OptionParser {
     void doParse() override {
         [[maybe_unused]] auto lineNr = 0;
 
-        std::string  sectionName;       // current section name
-        std::string  sectionValue;      // current section value
-        bool         inSection = false; // true if multi line section value
-        FindType     ft        = OptionContext::find_name_or_prefix;
-        SharedOptPtr opt;
+        std::string sectionName;       // current section name
+        std::string sectionValue;      // current section value
+        bool        inSection = false; // true if multi line section value
+        FindType    ft        = OptionContext::find_name_or_prefix;
         // reads the config file.
         // A config file may only contain empty lines, single line comments or
         // sections structured in a name = value fashion.
         // value can span multiple lines, but parts in different lines than name
-        // must not contain a '='-Character.
+        // must not contain a `=`-Character.
         for (std::string line; std::getline(in_, line);) {
             ++lineNr;
             trimLeft(line);
             trimRight(line);
 
-            if (line.empty() || line.find('#') == 0) {
+            if (line.empty() || line.starts_with('#')) {
                 // An empty line or single line comment stops a multi line section value.
                 if (inSection) {
-                    if ((opt = getOption(sectionName.c_str(), ft)).get()) {
+                    if (auto opt = getOption(sectionName.c_str(), ft); opt.get()) {
                         addOptionValue(opt, sectionValue);
                     }
                     inSection = false;
@@ -853,7 +841,7 @@ class CfgFileParser : public OptionParser {
             if (auto pos = line.find('='); pos != std::string::npos) {
                 // A new section terminates a multi line section value.
                 // First process the current section value...
-                if (inSection && (opt = getOption(sectionName.c_str(), ft)).get()) {
+                if (auto opt = inSection ? getOption(sectionName.c_str(), ft) : SharedOptPtr{}; opt.get()) {
                     addOptionValue(opt, sectionValue);
                 }
                 // ...then save the new section's value.
@@ -871,7 +859,7 @@ class CfgFileParser : public OptionParser {
             }
         }
         if (inSection) { // file does not end with an empty line
-            if ((opt = getOption(sectionName.c_str(), ft)).get()) {
+            if (auto opt = getOption(sectionName.c_str(), ft); opt.get()) {
                 addOptionValue(opt, sectionValue);
             }
         }
@@ -906,10 +894,11 @@ class DefaultContext : public ParseContext {
 
 } // end unnamed namespace
 
-ParsedValues parseCommandLine(int& argc, char** argv, const OptionContext& o, bool allowUnreg, PosOption po,
+ParsedValues parseCommandLine(int& argc, char** argv, const OptionContext& ctx, bool allowUnreg, PosOption posParser,
                               unsigned flags) {
-    DefaultContext ctx(o, allowUnreg, std::move(po));
-    return static_cast<DefaultContext&>(parseCommandLine(argc, argv, ctx, flags)).parsed;
+    DefaultContext parseCtx(ctx, allowUnreg, std::move(posParser));
+    parseCommandLine(argc, argv, parseCtx, flags);
+    return parseCtx.parsed;
 }
 ParseContext& parseCommandLine(int& argc, char** argv, ParseContext& ctx, unsigned flags) {
     while (argv[argc]) { ++argc; }
@@ -922,85 +911,78 @@ ParseContext& parseCommandLine(int& argc, char** argv, ParseContext& ctx, unsign
     argv[argc] = nullptr;
     return ctx;
 }
-ParsedValues parseCommandArray(const char* const* argv, int nArgs, const OptionContext& o, bool allowUnreg,
-                               PosOption po, unsigned flags) {
-    DefaultContext ctx(o, allowUnreg, std::move(po));
-    ArgvParser     parser(ctx, 0, nArgs, argv, flags);
+ParsedValues parseCommandArray(const char* const* argv, int nArgs, const OptionContext& ctx, bool allowUnreg,
+                               PosOption posParser, unsigned flags) {
+    DefaultContext parseCtx(ctx, allowUnreg, std::move(posParser));
+    ArgvParser     parser(parseCtx, 0, nArgs, argv, flags);
     parser.parse();
-    return static_cast<DefaultContext&>(ctx).parsed;
+    return parseCtx.parsed;
 }
 ParseContext& parseCommandString(const char* cmd, ParseContext& ctx, unsigned flags) {
     return CommandStringParser(cmd, ctx, flags).parse();
 }
-ParsedValues parseCommandString(const std::string& cmd, const OptionContext& o, bool allowUnreg, PosOption po,
+ParsedValues parseCommandString(const std::string& cmd, const OptionContext& ctx, bool allowUnreg, PosOption posParser,
                                 unsigned flags) {
-    DefaultContext ctx(o, allowUnreg, std::move(po));
-    return static_cast<DefaultContext&>(CommandStringParser(cmd.c_str(), ctx, flags).parse()).parsed;
+    DefaultContext parseCtx(ctx, allowUnreg, std::move(posParser));
+    CommandStringParser(cmd.c_str(), parseCtx, flags).parse();
+    return parseCtx.parsed;
 }
 
 ParsedValues parseCfgFile(std::istream& in, const OptionContext& o, bool allowUnreg) {
-    DefaultContext ctx(o, allowUnreg, nullptr);
-    return static_cast<DefaultContext&>(CfgFileParser(ctx, in).parse()).parsed;
+    DefaultContext parseCtx(o, allowUnreg, nullptr);
+    CfgFileParser(parseCtx, in).parse();
+    return parseCtx.parsed;
 }
 
 ///////////////////////////////////////////////////////////////////////////////
 // Errors
 ///////////////////////////////////////////////////////////////////////////////
-static std::string quote(const std::string& x) { return std::string("'").append(x).append("'"); }
+static std::string quote(const std::string& x) { return std::string(1, '\'').append(x).append(1, '\''); }
 static std::string format(SyntaxError::Type t, const std::string& key) {
-    std::string ret("SyntaxError: ");
-    ret += quote(key);
-    switch (t) {
-        case SyntaxError::missing_value : ret += " requires a value!"; break;
-        case SyntaxError::extra_value   : ret += " does not take a value!"; break;
-        case SyntaxError::invalid_format: ret += " unrecognized line!"; break;
-        default                         : ret += " unknown syntax!";
-    };
-    return ret;
+    return std::string("SyntaxError: "sv).append(quote(key)).append([](SyntaxError::Type type) {
+        switch (type) {
+            case SyntaxError::missing_value : return " requires a value!"sv;
+            case SyntaxError::extra_value   : return " does not take a value!"sv;
+            case SyntaxError::invalid_format: return " unrecognized line!"sv;
+            default                         : return " unknown syntax!"sv;
+        }
+    }(t));
 }
-static std::string format(ContextError::Type t, const std::string& ctx, const std::string& key,
-                          const std::string& alt) {
+static std::string formatContext(const std::string& ctx) {
     std::string ret;
     if (not ctx.empty()) {
-        ret += "In context ";
-        ret += quote(ctx);
-        ret += ": ";
+        ret.append("In context "sv).append(quote(ctx)).append(": "sv);
     }
+    return ret;
+}
+static std::string format(ContextError::Type t, const std::string& ctx, const std::string& key,
+                          const std::string& alt) {
+    std::string ret = formatContext(ctx);
     switch (t) {
-        case ContextError::duplicate_option: ret += "duplicate option: "; break;
-        case ContextError::unknown_option  : ret += "unknown option: "; break;
-        case ContextError::ambiguous_option: ret += "ambiguous option: "; break;
-        case ContextError::unknown_group   : ret += "unknown group: "; break;
-        default                            : ret += "unknown error in: ";
-    };
-    ret += quote(key);
+        case ContextError::duplicate_option: ret.append("duplicate option: "sv); break;
+        case ContextError::unknown_option  : ret.append("unknown option: "sv); break;
+        case ContextError::ambiguous_option: ret.append("ambiguous option: "sv); break;
+        case ContextError::unknown_group   : ret.append("unknown group: "sv); break;
+        default                            : ret.append("unknown error in: "sv);
+    }
+    ret.append(quote(key));
     if (t == ContextError::ambiguous_option && not alt.empty()) {
-        ret += " could be:\n";
-        ret += alt;
+        ret.append(" could be:\n"sv).append(alt);
     }
     return ret;
 }
 static std::string format(ValueError::Type t, const std::string& ctx, const std::string& key,
                           const std::string& value) {
-    std::string ret;
-    const char* x = "";
-    if (not ctx.empty()) {
-        ret += "In context ";
-        ret += quote(ctx);
-        ret += ": ";
-    }
-    switch (t) {
-        case ValueError::multiple_occurrences: ret += "multiple occurrences: "; break;
-        case ValueError::invalid_default     : x = "default "; [[fallthrough]];
+    std::string ret = formatContext(ctx);
+    switch (std::string_view x; t) {
+        case ValueError::multiple_occurrences: ret.append("multiple occurrences: "sv); break;
+        case ValueError::invalid_default     : x = "default "sv; [[fallthrough]];
         case ValueError::invalid_value:
-            ret += quote(value);
-            ret += " invalid ";
-            ret += x;
-            ret += "value for: ";
+            ret.append(quote(value)).append(" invalid "sv).append(x).append("value for: "sv);
             break;
-        default: ret += "unknown error in: ";
-    };
-    ret += quote(key);
+        default: ret.append("unknown error in: "sv);
+    }
+    ret.append(quote(key));
     return ret;
 }
 SyntaxError::SyntaxError(Type t, const std::string& key) : Error(format(t, key)), key_(key), type_(t) {}
diff --git a/src/rule_utils.cpp b/src/rule_utils.cpp
index 155a897..6456503 100644
--- a/src/rule_utils.cpp
+++ b/src/rule_utils.cpp
@@ -31,23 +31,23 @@
 #include <utility>
 
 namespace Potassco {
-Rule_t Rule_t::normal(Head_t ht, const AtomSpan& head, const LitSpan& body) {
-    Rule_t r;
+Rule Rule::normal(HeadType ht, const AtomSpan& head, const LitSpan& body) {
+    Rule r;
     r.ht   = ht;
     r.head = head;
-    r.bt   = Body_t::normal;
+    r.bt   = BodyType::normal;
     r.cond = body;
     return r;
 }
-Rule_t Rule_t::sum(Head_t ht, const AtomSpan& head, const Sum_t& sum) {
-    Rule_t r;
+Rule Rule::sum(HeadType ht, const AtomSpan& head, const Sum& sum) {
+    Rule r;
     r.ht   = ht;
     r.head = head;
-    r.bt   = Body_t::sum;
+    r.bt   = BodyType::sum;
     r.agg  = sum;
     return r;
 }
-Rule_t Rule_t::sum(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits) {
+Rule Rule::sum(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& lits) {
     return sum(ht, head, {lits, bound});
 }
 /////////////////////////////////////////////////////////////////////////////////////////
@@ -122,8 +122,8 @@ void RuleBuilder::clear(Range& r) {
 /////////////////////////////////////////////////////////////////////////////////////////
 // RuleBuilder - Head management
 /////////////////////////////////////////////////////////////////////////////////////////
-RuleBuilder& RuleBuilder::start(Head_t ht) {
-    start(head_, static_cast<uint32_t>(ht));
+RuleBuilder& RuleBuilder::start(HeadType ht) {
+    start(head_, to_underlying(ht));
     return *this;
 }
 RuleBuilder& RuleBuilder::addHead(Atom_t a) {
@@ -134,35 +134,35 @@ RuleBuilder& RuleBuilder::clearHead() {
     clear(head_);
     return *this;
 }
-Head_t   RuleBuilder::headType() const { return static_cast<Head_t>(head_.type()); }
+HeadType RuleBuilder::headType() const { return static_cast<HeadType>(head_.type()); }
 AtomSpan RuleBuilder::head() const { return makeSpan<Atom_t>(mem_, head_); }
-bool     RuleBuilder::isMinimize() const { return headType() == static_cast<Head_t>(Directive_t::minimize); }
+bool     RuleBuilder::isMinimize() const { return headType() == static_cast<HeadType>(AspifType::minimize); }
 /////////////////////////////////////////////////////////////////////////////////////////
 // RuleBuilder - Body management
 /////////////////////////////////////////////////////////////////////////////////////////
 static constexpr auto boundPos(uint32_t pos) { return static_cast<uint32_t>(pos - sizeof(Weight_t)); }
 RuleBuilder&          RuleBuilder::startBody() {
-    start(body_, static_cast<uint32_t>(Body_t::normal));
+    start(body_, to_underlying(BodyType::normal));
     return *this;
 }
 RuleBuilder& RuleBuilder::startSum(Weight_t bound) {
     if (not isMinimize() || frozen()) {
-        start(body_, static_cast<uint32_t>(Body_t::sum), &bound);
+        start(body_, to_underlying(BodyType::sum), &bound);
     }
     return *this;
 }
 RuleBuilder& RuleBuilder::startMinimize(Weight_t prio) {
-    start(head_, static_cast<uint32_t>(Directive_t::minimize));
-    start(body_, static_cast<uint32_t>(Body_t::sum), &prio);
+    start(head_, to_underlying(AspifType::minimize));
+    start(body_, to_underlying(BodyType::sum), &prio);
     return *this;
 }
 RuleBuilder& RuleBuilder::addGoal(Lit_t lit) {
-    bodyType() == Body_t::normal ? extend(body_, lit, "Body")
-                                 : extend(body_, WeightLit_t{.lit = lit, .weight = 1}, "Sum");
+    bodyType() == BodyType::normal ? extend(body_, lit, "Body")
+                                   : extend(body_, WeightLit{.lit = lit, .weight = 1}, "Sum");
     return *this;
 }
-RuleBuilder& RuleBuilder::addGoal(WeightLit_t lit) {
-    if (bodyType() == Body_t::normal) {
+RuleBuilder& RuleBuilder::addGoal(WeightLit lit) {
+    if (bodyType() == BodyType::normal) {
         POTASSCO_CHECK_PRE(lit.weight == 1, "non-trivial weight literal not supported in normal body");
         extend(body_, lit.lit, "Body");
     }
@@ -176,43 +176,44 @@ RuleBuilder& RuleBuilder::clearBody() {
     return *this;
 }
 RuleBuilder& RuleBuilder::setBound(Weight_t bound) {
-    POTASSCO_CHECK_PRE(bodyType() != Body_t::normal && not frozen(), "Invalid call to setBound");
+    POTASSCO_CHECK_PRE(bodyType() != BodyType::normal && not frozen(), "Invalid call to setBound");
     *storage_cast<Weight_t*>(mem_, boundPos(body_.start())) = bound;
     return *this;
 }
-RuleBuilder& RuleBuilder::weaken(Body_t to, bool resetWeights) {
+RuleBuilder& RuleBuilder::weaken(BodyType to, bool resetWeights) {
     POTASSCO_CHECK_PRE(not isMinimize(), "Invalid call to weaken");
-    if (auto t = bodyType(); t != Body_t::normal && t != to) {
-        auto s           = sum();
-        body_.start_type = (to == Body_t::normal ? boundPos(body_.start()) : body_.start()) | static_cast<uint32_t>(to);
-        if (to == Body_t::normal) { // drop bound and weights of literals
-            std::ranges::transform(s.lits, storage_cast<Lit_t*>(mem_, body_.start()),
-                                   [](WeightLit_t wl) { return wl.lit; });
-            auto drop = (s.lits.size() * sizeof(Weight_t)) + sizeof(Weight_t);
+    if (auto t = bodyType(); t != BodyType::normal && t != to) {
+        auto sLits       = sumLits();
+        auto sBound      = bound();
+        body_.start_type = (to == BodyType::normal ? boundPos(body_.start()) : body_.start()) | to_underlying(to);
+        if (to == BodyType::normal) { // drop bound and weights of literals
+            std::ranges::transform(sLits, storage_cast<Lit_t*>(mem_, body_.start()),
+                                   [](WeightLit wl) { return wl.lit; });
+            auto drop = (sLits.size() * sizeof(Weight_t)) + sizeof(Weight_t);
             if (body_.start() > head_.start()) {
                 mem_.pop(drop);
             }
             body_.end_flag -= static_cast<uint32_t>(drop);
         }
-        else if (not s.lits.empty() && resetWeights && to == Body_t::count) { // set weight of all lits to 1
-            auto minW = s.lits[0].weight;
-            for (auto& wl : s.lits) {
-                minW                                = std::min(minW, wl.weight);
-                const_cast<WeightLit_t&>(wl).weight = 1;
+        else if (not sLits.empty() && resetWeights && to == BodyType::count) { // set weight of all lits to 1
+            auto minW = sLits[0].weight;
+            for (auto& wl : sLits) {
+                minW      = std::min(minW, wl.weight);
+                wl.weight = 1;
             }
-            setBound((s.bound + (minW - 1)) / minW);
+            setBound((sBound + (minW - 1)) / minW);
         }
     }
     return *this;
 }
-Body_t   RuleBuilder::bodyType() const { return static_cast<Body_t>(body_.type()); }
+BodyType RuleBuilder::bodyType() const { return static_cast<BodyType>(body_.type()); }
 LitSpan  RuleBuilder::body() const { return makeSpan<Lit_t>(mem_, body_); }
-auto     RuleBuilder::sumLits() const -> std::span<WeightLit_t> { return makeSpan<WeightLit_t>(mem_, body_); }
+auto     RuleBuilder::sumLits() const -> std::span<WeightLit> { return makeSpan<WeightLit>(mem_, body_); }
 Weight_t RuleBuilder::bound() const {
-    return bodyType() != Body_t::normal ? *storage_cast<Weight_t*>(mem_, boundPos(body_.start())) : -1;
+    return bodyType() != BodyType::normal ? *storage_cast<Weight_t*>(mem_, boundPos(body_.start())) : -1;
 }
-Sum_t RuleBuilder::sum() const { return {sumLits(), bound()}; }
-auto  RuleBuilder::findSumLit(Lit_t lit) const -> WeightLit_t* {
+Sum  RuleBuilder::sum() const { return {sumLits(), bound()}; }
+auto RuleBuilder::findSumLit(Lit_t lit) const -> WeightLit* {
     for (auto& wl : sumLits()) {
         if (wl.lit == lit) {
             return &wl;
@@ -223,12 +224,12 @@ auto  RuleBuilder::findSumLit(Lit_t lit) const -> WeightLit_t* {
 /////////////////////////////////////////////////////////////////////////////////////////
 // RuleBuilder - Product
 /////////////////////////////////////////////////////////////////////////////////////////
-Rule_t RuleBuilder::rule() const {
-    Rule_t ret;
+Rule RuleBuilder::rule() const {
+    Rule ret;
     ret.ht   = headType();
     ret.head = head();
     ret.bt   = bodyType();
-    if (ret.bt == Body_t::normal) {
+    if (ret.bt == BodyType::normal) {
         ret.cond = body();
     }
     else {
@@ -240,7 +241,7 @@ RuleBuilder& RuleBuilder::end(AbstractProgram* out) {
     store_set_mask(head_.end_flag, Range::mask);
     store_set_mask(body_.end_flag, Range::mask);
     if (out) {
-        if (bodyType() == Body_t::normal) {
+        if (bodyType() == BodyType::normal) {
             out->rule(headType(), head(), body());
         }
         else if (auto s = sum(); isMinimize()) {
diff --git a/src/smodels.cpp b/src/smodels.cpp
index ceaa8da..2c976bb 100644
--- a/src/smodels.cpp
+++ b/src/smodels.cpp
@@ -68,7 +68,8 @@ SmodelsInput::SmodelsInput(AbstractProgram& out, const Options& opts, AtomLookup
 SmodelsInput::~SmodelsInput() = default;
 void SmodelsInput::doReset() {}
 bool SmodelsInput::doAttach(bool& inc) {
-    if (auto n = peek(); BufferedStream::isDigit(n) && ((inc = (n == '9')) == false || opts_.claspExt)) {
+    if (auto n = peek(); BufferedStream::isDigit(n) && (n != '9' || opts_.claspExt)) {
+        inc = n == '9';
         out_.initProgram(inc);
         return true;
     }
@@ -122,45 +123,45 @@ void SmodelsInput::matchSum(RuleBuilder& rule, bool weights) {
 bool SmodelsInput::readRules() {
     RuleBuilder rule;
     Weight_t    minPrio = 0;
-    for (SmodelsRule_t rt; (rt = matchEnum<SmodelsRule_t>("rule type expected")) != SmodelsRule_t::end;) {
+    for (SmodelsType rt; (rt = matchEnum<SmodelsType>("rule type expected")) != SmodelsType::end;) {
         rule.clear();
         switch (rt) {
             default: error("unrecognized rule type"); return false;
-            case SmodelsRule_t::choice:
-            case SmodelsRule_t::disjunctive: // n a1...an
-                rule.start(rt == SmodelsRule_t::choice ? Head_t::choice : Head_t::disjunctive);
+            case SmodelsType::choice:
+            case SmodelsType::disjunctive: // n a1...an
+                rule.start(rt == SmodelsType::choice ? HeadType::choice : HeadType::disjunctive);
                 for (unsigned i = matchAtom("positive head size expected"); i--;) { rule.addHead(matchAtom()); }
                 matchBody(rule);
                 rule.end(&out_);
                 break;
-            case SmodelsRule_t::basic:
-                rule.start(Head_t::disjunctive).addHead(matchAtom());
+            case SmodelsType::basic:
+                rule.start(HeadType::disjunctive).addHead(matchAtom());
                 matchBody(rule);
                 rule.end(&out_);
                 break;
-            case SmodelsRule_t::cardinality: // fall through
-            case SmodelsRule_t::weight:      // fall through
-                rule.start(Head_t::disjunctive).addHead(matchAtom());
-                matchSum(rule, rt == SmodelsRule_t::weight);
+            case SmodelsType::cardinality: // fall through
+            case SmodelsType::weight:      // fall through
+                rule.start(HeadType::disjunctive).addHead(matchAtom());
+                matchSum(rule, rt == SmodelsType::weight);
                 rule.end(&out_);
                 break;
-            case SmodelsRule_t::optimize:
+            case SmodelsType::optimize:
                 rule.startMinimize(minPrio++);
                 matchSum(rule, true);
                 rule.end(&out_);
                 break;
-            case SmodelsRule_t::clasp_increment:
+            case SmodelsType::clasp_increment:
                 require(opts_.claspExt && matchId() == 0, "unrecognized rule type");
                 break;
-            case SmodelsRule_t::clasp_assign_ext:
-            case SmodelsRule_t::clasp_release_ext:
+            case SmodelsType::clasp_assign_ext:
+            case SmodelsType::clasp_release_ext:
                 require(opts_.claspExt, "unrecognized rule type");
-                if (rt == SmodelsRule_t::clasp_assign_ext) {
+                if (rt == SmodelsType::clasp_assign_ext) {
                     auto rHead = matchAtom();
-                    out_.external(rHead, static_cast<Value_t>((matchUint(0u, 2u, "0..2 expected") ^ 3) - 1));
+                    out_.external(rHead, static_cast<TruthValue>((matchUint(0u, 2u, "0..2 expected") ^ 3) - 1));
                 }
                 else {
-                    out_.external(matchAtom(), Value_t::release);
+                    out_.external(matchAtom(), TruthValue::release);
                 }
                 break;
         }
@@ -171,7 +172,7 @@ bool SmodelsInput::readRules() {
 bool SmodelsInput::readSymbols() {
     std::string_view n0, n1;
     DynamicBuffer    scratch;
-    auto             heuType = Heuristic_t::init;
+    auto             heuType = DomModifier::init;
     auto             bias    = 0;
     auto             prio    = 0u;
     struct Deferred {
@@ -240,18 +241,18 @@ bool SmodelsInput::readSymbols() {
         }
     }
     for (auto dom = deferredDom.view(); dom.size() >= def_size;) {
-        Deferred data;
+        Deferred data{};
         std::memcpy(&data, dom.data(), def_size);
         dom.remove_prefix(def_size);
         auto atomId = data.sizeOrId;
         if (not data.atom) {
-            auto name = std::string_view{dom.data(), data.sizeOrId};
+            auto name = std::string_view{std::data(dom), data.sizeOrId};
             POTASSCO_ASSERT(dom.size() >= data.sizeOrId);
             dom.remove_prefix(data.sizeOrId);
             atomId = lookup_(name);
         }
         if (atomId) {
-            out_.heuristic(atomId, static_cast<Heuristic_t>(data.type), data.bias, data.prio, toSpan(data.cond));
+            out_.heuristic(atomId, static_cast<DomModifier>(data.type), data.bias, data.prio, toSpan(data.cond));
         }
     }
 
@@ -270,7 +271,7 @@ bool SmodelsInput::readCompute() {
             if (pos) {
                 x = neg(x);
             }
-            out_.rule(Head_t::disjunctive, {}, toSpan(x));
+            out_.rule(HeadType::disjunctive, {}, toSpan(x));
         }
     }
     return true;
@@ -278,7 +279,7 @@ bool SmodelsInput::readCompute() {
 
 bool SmodelsInput::readExtra() {
     if (skipWs() && match("E"sv)) {
-        for (Atom_t atom; (atom = matchAtomOrZero()) != 0;) { out_.external(atom, Value_t::free); }
+        for (Atom_t atom; (atom = matchAtomOrZero()) != 0;) { out_.external(atom, TruthValue::free); }
     }
     matchUint("number of models expected");
     return true;
@@ -317,10 +318,10 @@ static bool matchNum(std::string_view& in, std::string_view* sOut, int* nOut = n
     return true;
 }
 
-static bool match(std::string_view& input, Heuristic_t& heuType) {
-    for (const auto& [k, n] : enum_entries<Heuristic_t>()) {
+static bool match(std::string_view& input, DomModifier& heuType) {
+    for (const auto& [k, n] : enum_entries<DomModifier>()) {
         if (not n.empty() && match(input, n)) {
-            heuType = static_cast<Heuristic_t>(k);
+            heuType = static_cast<DomModifier>(k);
             return true;
         }
     }
@@ -337,7 +338,7 @@ bool matchEdgePred(std::string_view in, std::string_view& n0, std::string_view&
     }
     return false;
 }
-bool matchDomHeuPred(std::string_view in, std::string_view& atom, Heuristic_t& type, int& bias, unsigned& prio) {
+bool matchDomHeuPred(std::string_view in, std::string_view& atom, DomModifier& type, int& bias, unsigned& prio) {
     // _heuristic(<atom>,<type>,<bias>[,<prio>])
     if (match(in, heuristic_pred) && matchTerm(in, atom) && match(in, ',') && match(in, type) && match(in, ',') &&
         matchNum(in, nullptr, &bias)) {
@@ -357,7 +358,7 @@ bool matchDomHeuPred(std::string_view in, std::string_view& atom, Heuristic_t& t
 /////////////////////////////////////////////////////////////////////////////////////////
 // SmodelsOutput
 /////////////////////////////////////////////////////////////////////////////////////////
-static constexpr Lit_t smLit(const WeightLit_t& x) { return x.weight >= 0 ? x.lit : -x.lit; }
+static constexpr Lit_t smLit(const WeightLit& x) { return x.weight >= 0 ? x.lit : -x.lit; }
 static constexpr Lit_t smLit(Lit_t x) { return x; }
 template <typename T>
 static constexpr unsigned negSize(const std::span<T>& lits) {
@@ -392,8 +393,8 @@ SmodelsOutput::SmodelsOutput(std::ostream& os, bool ext, Atom_t fAtom)
     , ext_(ext)
     , inc_(false)
     , fHead_(false) {}
-SmodelsOutput& SmodelsOutput::startRule(SmodelsRule_t rt) {
-    POTASSCO_CHECK_PRE(sec_ == 0 || rt == SmodelsRule_t::end || rt >= SmodelsRule_t::clasp_increment,
+SmodelsOutput& SmodelsOutput::startRule(SmodelsType rt) {
+    POTASSCO_CHECK_PRE(sec_ == 0 || rt == SmodelsType::end || rt >= SmodelsType::clasp_increment,
                        "adding rules after symbols not supported");
     os_ << to_underlying(rt);
     return *this;
@@ -402,13 +403,13 @@ SmodelsOutput& SmodelsOutput::add(unsigned i) {
     os_ << " " << i;
     return *this;
 }
-SmodelsOutput& SmodelsOutput::add(Head_t ht, const AtomSpan& head) {
+SmodelsOutput& SmodelsOutput::add(HeadType ht, const AtomSpan& head) {
     if (head.empty()) {
-        POTASSCO_CHECK_PRE(false_ != 0 && ht == Head_t::disjunctive, "empty head requires false atom");
+        POTASSCO_CHECK_PRE(false_ != 0 && ht == HeadType::disjunctive, "empty head requires false atom");
         fHead_ = true;
         return add(false_);
     }
-    if (ht == Head_t::choice || head.size() > 1) {
+    if (ht == HeadType::choice || head.size() > 1) {
         add(size_cast<unsigned>(head));
     }
     for (auto atom : head) { add(atom); }
@@ -432,8 +433,7 @@ SmodelsOutput& SmodelsOutput::add(Weight_t bound, const WeightLitSpan& lits, boo
     }
     print(os_, lits, neg, size - neg);
     if (not card) {
-        print(os_, lits, neg, size - neg,
-              [](const WeightLit_t& wl) { return wl.weight >= 0 ? wl.weight : -wl.weight; });
+        print(os_, lits, neg, size - neg, [](const WeightLit& wl) { return wl.weight >= 0 ? wl.weight : -wl.weight; });
     }
     return *this;
 }
@@ -449,63 +449,63 @@ void SmodelsOutput::beginStep() {
     sec_   = 0;
     fHead_ = false;
     if (ext_ && inc_) {
-        startRule(SmodelsRule_t::clasp_increment).add(0).endRule();
+        startRule(SmodelsType::clasp_increment).add(0).endRule();
     }
 }
-void SmodelsOutput::rule(Head_t ht, const AtomSpan& head, const LitSpan& body) {
-    if (head.empty() && ht == Head_t::choice) {
+void SmodelsOutput::rule(HeadType ht, const AtomSpan& head, const LitSpan& body) {
+    if (head.empty() && ht == HeadType::choice) {
         return;
     }
     POTASSCO_CHECK_PRE(false_ != 0 || not head.empty(), "empty head requires false atom");
-    auto rt = ht == Head_t::choice ? SmodelsRule_t::choice
-              : head.size() > 1    ? SmodelsRule_t::disjunctive
-                                   : SmodelsRule_t::basic;
+    auto rt = ht == HeadType::choice ? SmodelsType::choice
+              : head.size() > 1      ? SmodelsType::disjunctive
+                                     : SmodelsType::basic;
     startRule(rt).add(ht, head).add(body).endRule();
 }
-void SmodelsOutput::rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) {
-    if (head.empty() && ht == Head_t::choice) {
+void SmodelsOutput::rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) {
+    if (head.empty() && ht == HeadType::choice) {
         return;
     }
-    POTASSCO_CHECK_PRE(ht == Head_t::disjunctive && head.size() < 2, "normal head expected");
+    POTASSCO_CHECK_PRE(ht == HeadType::disjunctive && head.size() < 2, "normal head expected");
     POTASSCO_CHECK_PRE(false_ != 0 || not head.empty(), "empty head requires false atom");
     bound   = std::max(bound, 0);
-    auto rt = SmodelsRule_t::cardinality;
+    auto rt = SmodelsType::cardinality;
     for (const auto& wl : body) {
         POTASSCO_CHECK_PRE(weight(wl) >= 0, "negative weights not supported");
         if (weight(wl) != 1) {
-            rt = SmodelsRule_t::weight;
+            rt = SmodelsType::weight;
         }
     }
-    startRule(rt).add(ht, head).add(bound, body, rt == SmodelsRule_t::cardinality).endRule();
+    startRule(rt).add(ht, head).add(bound, body, rt == SmodelsType::cardinality).endRule();
 }
 void SmodelsOutput::minimize(Weight_t, const WeightLitSpan& lits) {
-    startRule(SmodelsRule_t::optimize).add(0, lits, false).endRule();
+    startRule(SmodelsType::optimize).add(0, lits, false).endRule();
 }
 void SmodelsOutput::output(const std::string_view& str, const LitSpan& cond) {
     POTASSCO_CHECK_PRE(sec_ <= 1, "adding symbols after compute not supported");
     POTASSCO_CHECK_PRE(cond.size() == 1 && lit(cond.front()) > 0,
                        "general output directive not supported in smodels format");
     if (sec_ == 0) {
-        startRule(SmodelsRule_t::end).endRule();
+        startRule(SmodelsType::end).endRule();
         sec_ = 1;
     }
     os_ << static_cast<unsigned>(cond[0]) << " ";
-    os_.write(str.data(), std::ssize(str));
+    os_.write(std::data(str), std::ssize(str));
     os_ << '\n';
 }
-void SmodelsOutput::external(Atom_t a, Value_t t) {
+void SmodelsOutput::external(Atom_t a, TruthValue t) {
     POTASSCO_CHECK_PRE(ext_, "external directive not supported in smodels format");
-    if (t != Value_t::release) {
-        startRule(SmodelsRule_t::clasp_assign_ext).add(a).add((to_underlying(t) ^ 3) - 1).endRule();
+    if (t != TruthValue::release) {
+        startRule(SmodelsType::clasp_assign_ext).add(a).add((to_underlying(t) ^ 3) - 1).endRule();
     }
     else {
-        startRule(SmodelsRule_t::clasp_release_ext).add(a).endRule();
+        startRule(SmodelsType::clasp_release_ext).add(a).endRule();
     }
 }
 void SmodelsOutput::assume(const LitSpan& lits) {
     POTASSCO_CHECK_PRE(sec_ < 2, "at most one compute statement supported in smodels format");
     while (sec_ != 2) {
-        startRule(SmodelsRule_t::end).endRule();
+        startRule(SmodelsType::end).endRule();
         ++sec_;
     }
     os_ << "B+\n";
diff --git a/src/string_convert.cpp b/src/string_convert.cpp
index dba13fe..b1971d3 100644
--- a/src/string_convert.cpp
+++ b/src/string_convert.cpp
@@ -61,8 +61,7 @@ std::from_chars_result parseChar(std::string_view in, unsigned char& out) {
         return Parse::error(in);
     }
 
-    std::string_view::size_type pos;
-    if (in.size() > 1 && in.front() == '\\' && (pos = c_from.find(in[1])) != std::string_view::npos) {
+    if (auto pos = in[0] == '\\' ? c_from.find(in[in.size() > 1]) : std::string_view::npos; pos < c_to.size()) {
         out = static_cast<unsigned char>(c_to[pos]);
         return Parse::success(in, 2);
     }
@@ -207,26 +206,23 @@ std::from_chars_result fromChars(std::string_view in, bool& out) {
     if (in.empty()) {
         return Parse::error(in);
     }
-
     if (in.starts_with('0') || in.starts_with('1')) {
         out = in[0] == '1';
         return Parse::success(in, 1);
     }
-    else if (in.starts_with("no") || in.starts_with("on")) {
+    if (in.starts_with("no") || in.starts_with("on")) {
         out = in[0] == 'o';
         return Parse::success(in, 2);
     }
-    else if (in.starts_with("off") || in.starts_with("yes")) {
+    if (in.starts_with("off") || in.starts_with("yes")) {
         out = in[0] == 'y';
         return Parse::success(in, 3);
     }
-    else if (in.starts_with("false") || in.starts_with("true")) {
+    if (in.starts_with("false") || in.starts_with("true")) {
         out = in[0] == 't';
         return Parse::success(in, 4u + static_cast<unsigned>(not out));
     }
-    else {
-        return Parse::error(in);
-    }
+    return Parse::error(in);
 }
 
 } // namespace Potassco
diff --git a/src/theory_data.cpp b/src/theory_data.cpp
index 7cee9bc..9535d59 100644
--- a/src/theory_data.cpp
+++ b/src/theory_data.cpp
@@ -30,7 +30,6 @@
 #include <algorithm>
 #include <cstring>
 
-#include <stdexcept>
 namespace Potassco {
 template <typename T>
 static constexpr std::size_t computeExtraBytes(const T& arg [[maybe_unused]]) {
@@ -59,42 +58,40 @@ struct TheoryTerm::FuncData {
 
 constexpr auto  c_nul_term  = static_cast<uint64_t>(-1);
 constexpr auto  c_type_mask = static_cast<uint64_t>(3);
-static uint64_t assertPtr(const void* p, Theory_t type) {
+static uint64_t assertPtr(const void* p, TheoryTermType type) {
     auto data = static_cast<uint64_t>(reinterpret_cast<uintptr_t>(p));
     auto mask = static_cast<uint32_t>(type);
     POTASSCO_ASSERT(not test_any(data, mask), "Invalid pointer alignment");
     return data | mask;
 }
-Theory_t TheoryTerm::type() const { return static_cast<Theory_t>(clear_mask(data_, ~c_type_mask)); }
-int      TheoryTerm::number() const {
-    POTASSCO_CHECK(type() == Theory_t::number, Errc::invalid_argument, "Term is not a number");
+auto TheoryTerm::type() const -> Type { return static_cast<TheoryTermType>(clear_mask(data_, ~c_type_mask)); }
+int  TheoryTerm::number() const {
+    POTASSCO_CHECK(type() == TheoryTermType::number, Errc::invalid_argument, "Term is not a number");
     return static_cast<int>(data_ >> 2);
 }
 uintptr_t   TheoryTerm::getPtr() const { return static_cast<uintptr_t>(clear_mask(data_, c_type_mask)); }
 const char* TheoryTerm::symbol() const {
-    POTASSCO_CHECK(type() == Theory_t::symbol, Errc::invalid_argument, "Term is not a symbol");
+    POTASSCO_CHECK(type() == Type::symbol, Errc::invalid_argument, "Term is not a symbol");
     return reinterpret_cast<const char*>(getPtr());
 }
 TheoryTerm::FuncData* TheoryTerm::func() const { return reinterpret_cast<FuncData*>(getPtr()); }
 int                   TheoryTerm::compound() const {
-    POTASSCO_CHECK(type() == Theory_t::compound, Errc::invalid_argument, "Term is not a compound");
+    POTASSCO_CHECK(type() == Type::compound, Errc::invalid_argument, "Term is not a compound");
     return func()->base;
 }
-bool TheoryTerm::isFunction() const { return type() == Theory_t::compound && func()->base >= 0; }
-bool TheoryTerm::isTuple() const { return type() == Theory_t::compound && func()->base < 0; }
+bool TheoryTerm::isFunction() const { return type() == Type::compound && func()->base >= 0; }
+bool TheoryTerm::isTuple() const { return type() == Type::compound && func()->base < 0; }
 Id_t TheoryTerm::function() const {
     POTASSCO_CHECK(isFunction(), Errc::invalid_argument, "Term is not a function");
     return static_cast<Id_t>(func()->base);
 }
-Tuple_t TheoryTerm::tuple() const {
+TupleType TheoryTerm::tuple() const {
     POTASSCO_CHECK(isTuple(), Errc::invalid_argument, "Term is not a tuple");
-    return static_cast<Tuple_t>(func()->base);
-}
-uint32_t             TheoryTerm::size() const { return type() == Theory_t::compound ? func()->size : 0; }
-TheoryTerm::iterator TheoryTerm::begin() const { return type() == Theory_t::compound ? func()->args : nullptr; }
-TheoryTerm::iterator TheoryTerm::end() const {
-    return type() == Theory_t::compound ? func()->args + func()->size : nullptr;
+    return static_cast<TupleType>(func()->base);
 }
+uint32_t TheoryTerm::size() const { return type() == Type::compound ? func()->size : 0; }
+auto     TheoryTerm::begin() const -> iterator { return type() == Type::compound ? func()->args : nullptr; }
+auto TheoryTerm::end() const -> iterator { return type() == Type::compound ? func()->args + func()->size : nullptr; }
 TheoryElement::TheoryElement(const IdSpan& terms, const Id_t* c)
     : nTerms_(static_cast<uint32_t>(terms.size()))
     , nCond_(c != nullptr) {
@@ -134,10 +131,10 @@ struct TheoryData::DestroyT {
     void operator()(const TheoryTerm& raw) const {
         if (raw.data_ != c_nul_term) {
             // TheoryTerm term(raw);
-            if (auto type = raw.type(); type == Theory_t::compound) {
+            if (auto type = raw.type(); type == TheoryTermType::compound) {
                 (*this)(raw.func());
             }
-            else if (type == Theory_t::symbol) {
+            else if (type == TheoryTermType::symbol) {
                 delete[] const_cast<char*>(raw.symbol());
             }
         }
@@ -159,21 +156,20 @@ struct TheoryData::Data {
     amc::vector<TheoryElement*> elems;
     amc::vector<TheoryTerm>     terms;
     struct Up {
-        Up() : atom(0), term(0), elem(0) {}
-        uint32_t atom;
-        uint32_t term;
-        uint32_t elem;
+        uint32_t atom{0};
+        uint32_t term{0};
+        uint32_t elem{0};
     } frame;
 };
 TheoryData::TheoryData() : data_(std::make_unique<Data>()) {}
 TheoryData::~TheoryData() { reset(); }
 void TheoryData::addTerm(Id_t termId, int number) {
     auto& term = setTerm(termId);
-    term       = (static_cast<uint64_t>(number) << 2) | to_underlying(Theory_t::number);
+    term       = (static_cast<uint64_t>(number) << 2) | to_underlying(TheoryTermType::number);
 }
 void TheoryData::addTerm(Id_t termId, const std::string_view& name) {
     auto& term = setTerm(termId);
-    term       = assertPtr(Data::allocCString(name), Theory_t::symbol);
+    term       = assertPtr(Data::allocCString(name), TheoryTermType::symbol);
     POTASSCO_DEBUG_ASSERT(getTerm(termId).symbol() == name);
 }
 void TheoryData::addTerm(Id_t termId, const char* name) {
@@ -183,12 +179,12 @@ void TheoryData::addTerm(Id_t termId, const char* name) {
 void TheoryData::addTerm(Id_t termId, Id_t funcId, const IdSpan& args) {
     using D    = TheoryTerm::FuncData;
     auto& term = setTerm(termId);
-    term       = assertPtr(Data::allocConstruct<D>(static_cast<int32_t>(funcId), args), Theory_t::compound);
+    term       = assertPtr(Data::allocConstruct<D>(static_cast<int32_t>(funcId), args), TheoryTermType::compound);
 }
-void TheoryData::addTerm(Id_t termId, Tuple_t type, const IdSpan& args) {
+void TheoryData::addTerm(Id_t termId, TupleType type, const IdSpan& args) {
     using D    = TheoryTerm::FuncData;
     auto& term = setTerm(termId);
-    term       = assertPtr(Data::allocConstruct<D>(static_cast<int32_t>(type), args), Theory_t::compound);
+    term       = assertPtr(Data::allocConstruct<D>(static_cast<int32_t>(type), args), TheoryTermType::compound);
 }
 void TheoryData::removeTerm(Id_t termId) {
     if (hasTerm(termId)) {
@@ -241,19 +237,19 @@ void TheoryData::update() {
     data_->frame.term = numTerms();
     data_->frame.elem = numElems();
 }
-uint32_t                  TheoryData::numAtoms() const { return data_->atoms.size(); }
-uint32_t                  TheoryData::numTerms() const { return data_->terms.size(); }
-uint32_t                  TheoryData::numElems() const { return data_->elems.size(); }
-void                      TheoryData::resizeAtoms(uint32_t newSize) { data_->atoms.resize(newSize); }
-void                      TheoryData::destroyAtom(TheoryAtom* atom) { DestroyT{}(atom); }
-TheoryData::atom_iterator TheoryData::begin() const { return data_->atoms.begin(); }
-TheoryData::atom_iterator TheoryData::currBegin() const { return begin() + data_->frame.atom; }
-TheoryData::atom_iterator TheoryData::end() const { return begin() + numAtoms(); }
-bool       TheoryData::hasTerm(Id_t id) const { return id < numTerms() && data_->terms[id].data_ != c_nul_term; }
-bool       TheoryData::isNewTerm(Id_t id) const { return hasTerm(id) && id >= data_->frame.term; }
-bool       TheoryData::hasElement(Id_t id) const { return id < numElems() && data_->elems[id] != nullptr; }
-bool       TheoryData::isNewElement(Id_t id) const { return hasElement(id) && id >= data_->frame.elem; }
-TheoryTerm TheoryData::getTerm(Id_t id) const {
+uint32_t TheoryData::numAtoms() const { return data_->atoms.size(); }
+uint32_t TheoryData::numTerms() const { return data_->terms.size(); }
+uint32_t TheoryData::numElems() const { return data_->elems.size(); }
+void     TheoryData::resizeAtoms(uint32_t newSize) { data_->atoms.resize(newSize); }
+void     TheoryData::destroyAtom(TheoryAtom* atom) { DestroyT{}(atom); }
+auto     TheoryData::begin() const -> atom_iterator { return data_->atoms.begin(); }
+auto     TheoryData::currBegin() const -> atom_iterator { return begin() + data_->frame.atom; }
+auto     TheoryData::end() const -> atom_iterator { return begin() + numAtoms(); }
+bool     TheoryData::hasTerm(Id_t id) const { return id < numTerms() && data_->terms[id].data_ != c_nul_term; }
+bool     TheoryData::isNewTerm(Id_t id) const { return hasTerm(id) && id >= data_->frame.term; }
+bool     TheoryData::hasElement(Id_t id) const { return id < numElems() && data_->elems[id] != nullptr; }
+bool     TheoryData::isNewElement(Id_t id) const { return hasElement(id) && id >= data_->frame.elem; }
+auto     TheoryData::getTerm(Id_t id) const -> TheoryTerm {
     POTASSCO_CHECK(hasTerm(id), Errc::out_of_range, "Unknown term '%u'", id);
     return data_->terms[id];
 }
@@ -267,7 +263,7 @@ void TheoryData::accept(Visitor& out, VisitMode m) const {
     }
 }
 void TheoryData::accept(const TheoryTerm& t, Visitor& out, VisitMode m) const {
-    if (t.type() == Theory_t::compound) {
+    if (t.type() == TheoryTermType::compound) {
         for (auto id : t) {
             if (doVisitTerm(m, id)) {
                 out.visit(*this, id, getTerm(id));
diff --git a/tests/test_aspif.cpp b/tests/test_aspif.cpp
index d0ddf92..6f68a89 100644
--- a/tests/test_aspif.cpp
+++ b/tests/test_aspif.cpp
@@ -40,24 +40,24 @@ namespace Potassco::Test::Aspif {
 constexpr Weight_t bound_none = -1;
 static void        finalize(std::stringstream& str) { str << "0\n"; }
 static void        rule(std::ostream& os, const Rule& r) {
-    os << static_cast<unsigned>(Directive_t::rule) << " " << static_cast<unsigned>(r.ht) << " ";
+    os << static_cast<unsigned>(AspifType::rule) << " " << static_cast<unsigned>(r.ht) << " ";
     os << r.head.size();
     for (auto x : r.head) { os << " " << x; }
     os << " " << static_cast<unsigned>(r.bt) << " ";
-    if (r.bt == Body_t::sum) {
+    if (r.bt == BodyType::sum) {
         os << r.bnd << " " << r.body.size();
-        std::ranges::for_each(r.body, [&os](WeightLit_t x) { os << " " << x.lit << " " << x.weight; });
+        std::ranges::for_each(r.body, [&os](WeightLit x) { os << " " << x.lit << " " << x.weight; });
     }
     else {
         os << r.body.size();
-        std::ranges::for_each(r.body, [&os](WeightLit_t x) { os << " " << x.lit; });
+        std::ranges::for_each(r.body, [&os](WeightLit x) { os << " " << x.lit; });
     }
     os << "\n";
 }
-static std::ostream& operator<<(std::ostream& os, const WeightLit_t& wl) {
+static std::ostream& operator<<(std::ostream& os, const WeightLit& wl) {
     return os << "(" << wl.lit << "," << wl.weight << ")";
 }
-static std::ostream& operator<<(std::ostream& os, const std::pair<Atom_t, Potassco::Value_t>& wl) {
+static std::ostream& operator<<(std::ostream& os, const std::pair<Atom_t, Potassco::TruthValue>& wl) {
     return os << "(" << wl.first << "," << static_cast<unsigned>(wl.second) << ")";
 }
 static std::ostream& operator<<(std::ostream& os, const Heuristic& h);
@@ -85,13 +85,13 @@ template <Potassco::ScopedEnum E>
 namespace {
 class ReadObserver final : public Test::ReadObserver {
 public:
-    void rule(Head_t ht, const AtomSpan& head, const LitSpan& body) override {
-        rules.push_back({ht, {begin(head), end(head)}, Body_t::normal, bound_none, {}});
-        Vec<WeightLit_t>& wb = rules.back().body;
+    void rule(HeadType ht, const AtomSpan& head, const LitSpan& body) override {
+        rules.push_back({ht, {begin(head), end(head)}, BodyType::normal, bound_none, {}});
+        Vec<WeightLit>& wb = rules.back().body;
         std::ranges::for_each(body, [&wb](Lit_t x) { wb.push_back({x, 1}); });
     }
-    void rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override {
-        rules.push_back({ht, {begin(head), end(head)}, Body_t::sum, bound, {begin(body), end(body)}});
+    void rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override {
+        rules.push_back({ht, {begin(head), end(head)}, BodyType::sum, bound, {begin(body), end(body)}});
     }
     void minimize(Weight_t prio, const WeightLitSpan& lits) override {
         min.push_back({prio, {begin(lits), end(lits)}});
@@ -101,7 +101,7 @@ class ReadObserver final : public Test::ReadObserver {
         shows.push_back({{begin(str), end(str)}, {begin(cond), end(cond)}});
     }
 
-    void external(Atom_t a, Value_t v) override { externals.emplace_back(a, v); }
+    void external(Atom_t a, TruthValue v) override { externals.emplace_back(a, v); }
     void assume(const LitSpan& lits) override { assumes.insert(assumes.end(), begin(lits), end(lits)); }
     void theoryTerm(Id_t termId, int number) override { theory.addTerm(termId, number); }
     void theoryTerm(Id_t termId, const std::string_view& name) override { theory.addTerm(termId, name); }
@@ -119,9 +119,9 @@ class ReadObserver final : public Test::ReadObserver {
     }
 
     Vec<Rule>                               rules;
-    Vec<std::pair<int, Vec<WeightLit_t>>>   min;
+    Vec<std::pair<int, Vec<WeightLit>>>     min;
     Vec<std::pair<std::string, Vec<Lit_t>>> shows;
-    Vec<std::pair<Atom_t, Value_t>>         externals;
+    Vec<std::pair<Atom_t, TruthValue>>      externals;
     Vec<Atom_t>                             projects;
     Vec<Lit_t>                              assumes;
     TheoryData                              theory;
@@ -448,7 +448,7 @@ TEST_CASE("Test Basic", "[rule]") {
         CHECK_FALSE(validAtom(neg(x)));
     }
     SECTION("weight literal") {
-        WeightLit_t wl{.lit = -4, .weight = 3};
+        WeightLit wl{.lit = -4, .weight = 3};
         CHECK(weight(wl) == 3);
         CHECK(lit(wl) == -4);
         CHECK(wl == wl);
@@ -465,38 +465,42 @@ TEST_CASE("Test Basic", "[rule]") {
     }
     SECTION("enums") {
         using std::literals::operator""sv;
-        CHECK(enum_min<Directive_t>() == 0);
-        CHECK(enum_max<Directive_t>() == 10);
-        CHECK(enum_count<Directive_t>() == 11);
+        CHECK(enum_min<AspifType>() == 0);
+        CHECK(enum_max<AspifType>() == 10);
+        CHECK(enum_count<AspifType>() == 11);
 
-        CHECK(enum_min<Head_t>() == 0);
-        CHECK(enum_max<Head_t>() == 1);
-        CHECK(enum_count<Head_t>() == 2);
+        CHECK(enum_min<HeadType>() == 0);
+        CHECK(enum_max<HeadType>() == 1);
+        CHECK(enum_count<HeadType>() == 2);
 
-        CHECK(enum_min<Body_t>() == 0);
-        CHECK(enum_max<Body_t>() == 2);
-        CHECK(enum_count<Body_t>() == 3);
+        CHECK(enum_min<BodyType>() == 0);
+        CHECK(enum_max<BodyType>() == 2);
+        CHECK(enum_count<BodyType>() == 3);
 
-        CHECK(enum_min<Value_t>() == 0);
-        CHECK(enum_max<Value_t>() == 3);
-        CHECK(enum_count<Value_t>() == 4);
-        static_assert(enum_name(Value_t::false_) == "false"sv);
-        static_assert(enum_name(Value_t::release) == "release"sv);
+        CHECK(enum_min<TruthValue>() == 0);
+        CHECK(enum_max<TruthValue>() == 3);
+        CHECK(enum_count<TruthValue>() == 4);
+        static_assert(enum_name(TruthValue::false_) == "false"sv);
+        static_assert(enum_name(TruthValue::release) == "release"sv);
 
-        CHECK(enum_min<Heuristic_t>() == 0);
-        CHECK(enum_max<Heuristic_t>() == 5);
-        CHECK(enum_count<Heuristic_t>() == 6);
+        CHECK(enum_min<DomModifier>() == 0);
+        CHECK(enum_max<DomModifier>() == 5);
+        CHECK(enum_count<DomModifier>() == 6);
 
-        static_assert(enum_name(Heuristic_t::init) == "init"sv);
-        static_assert(enum_name(Heuristic_t::level) == "level"sv);
+        static_assert(enum_name(DomModifier::init) == "init"sv);
+        static_assert(enum_name(DomModifier::level) == "level"sv);
 
-        CHECK(enum_min<Theory_t>() == 0);
-        CHECK(enum_max<Theory_t>() == 6);
-        CHECK(enum_count<Theory_t>() == 7);
+        CHECK(enum_min<TheoryTermType>() == 0);
+        CHECK(enum_max<TheoryTermType>() == 2);
+        CHECK(enum_count<TheoryTermType>() == 3);
 
-        CHECK(enum_min<Tuple_t>() == -3);
-        CHECK(enum_max<Tuple_t>() == -1);
-        CHECK(enum_count<Tuple_t>() == 3);
+        CHECK(enum_min<TheoryType>() == 0);
+        CHECK(enum_max<TheoryType>() == 6);
+        CHECK(enum_count<TheoryType>() == 7);
+
+        CHECK(enum_min<TupleType>() == -3);
+        CHECK(enum_max<TupleType>() == -1);
+        CHECK(enum_count<TupleType>() == 3);
     }
     SECTION("bits") {
         unsigned n = 0;
@@ -607,79 +611,79 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
     SECTION("simple rule") {
         rb.start().addHead(1).addGoal(2).addGoal(-3).end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{1}));
-        REQUIRE(rb.bodyType() == Body_t::normal);
+        REQUIRE(rb.bodyType() == BodyType::normal);
         REQUIRE(spanEq(rb.body(), std::vector{2, -3}));
     }
     SECTION("simple constraint") {
         SECTION("head first") { rb.start().addGoal(2).addGoal(-3).end(); }
         SECTION("body first") { rb.startBody().addGoal(2).addGoal(-3).start().end(); }
         CHECK(spanEq(rb.head(), std::vector<Atom_t>{}));
-        CHECK(rb.bodyType() == Body_t::normal);
+        CHECK(rb.bodyType() == BodyType::normal);
         CHECK(spanEq(rb.body(), std::vector{2, -3}));
     }
     SECTION("simple choice") {
-        SECTION("head first") { rb.start(Head_t::choice).addHead(1).addHead(2).startBody().end(); }
-        SECTION("body first") { rb.startBody().start(Head_t::choice).addHead(1).addHead(2).end(); }
+        SECTION("head first") { rb.start(HeadType::choice).addHead(1).addHead(2).startBody().end(); }
+        SECTION("body first") { rb.startBody().start(HeadType::choice).addHead(1).addHead(2).end(); }
         CHECK(spanEq(rb.head(), std::vector<Atom_t>{1, 2}));
-        CHECK(rb.bodyType() == Body_t::normal);
+        CHECK(rb.bodyType() == BodyType::normal);
         CHECK(spanEq(rb.body(), std::vector<Lit_t>{}));
     }
     SECTION("simple weight rule") {
         rb.start().addHead(1).startSum(2).addGoal(2, 1).addGoal(-3, 1).addGoal(4, 2).end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{1}));
-        REQUIRE(rb.bodyType() == Body_t::sum);
+        REQUIRE(rb.bodyType() == BodyType::sum);
         REQUIRE(rb.bound() == 2);
-        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit_t>{{2, 1}, {-3, 1}, {4, 2}}));
+        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit>{{2, 1}, {-3, 1}, {4, 2}}));
         REQUIRE(spanEq(rb.sum().lits, rb.sumLits()));
         REQUIRE(rb.findSumLit(4)->weight == 2);
         REQUIRE(rb.findSumLit(-4) == nullptr);
 
         auto r = rb.rule();
         REQUIRE(spanEq(r.head, rb.head()));
-        REQUIRE(r.bt == Body_t::sum);
+        REQUIRE(r.bt == BodyType::sum);
         REQUIRE(r.agg.bound == 2);
         REQUIRE(spanEq(r.agg.lits, rb.sum().lits));
     }
     SECTION("update bound") {
         rb.start().addHead(1).startSum(2).addGoal(2, 1).addGoal(-3, 1).addGoal(4, 2).setBound(3);
-        REQUIRE(rb.bodyType() == Body_t::sum);
+        REQUIRE(rb.bodyType() == BodyType::sum);
         REQUIRE(rb.bound() == 3);
         rb.clear();
         rb.startSum(2).addGoal(2, 1).addGoal(-3, 1).addGoal(4, 2).addHead(1).setBound(4);
-        REQUIRE(rb.bodyType() == Body_t::sum);
+        REQUIRE(rb.bodyType() == BodyType::sum);
         REQUIRE(rb.bound() == 4);
         rb.clear();
         rb.startSum(2).addGoal(2, 1).addGoal(-3, 1).addGoal(4, 2).addHead(1).end();
         REQUIRE_THROWS_AS(rb.setBound(4), std::logic_error);
     }
     SECTION("weaken to cardinality rule") {
-        rb.start().addHead(1).startSum(2).addGoal(2, 2).addGoal(-3, 2).addGoal(4, 2).weaken(Body_t::count).end();
+        rb.start().addHead(1).startSum(2).addGoal(2, 2).addGoal(-3, 2).addGoal(4, 2).weaken(BodyType::count).end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{1}));
-        REQUIRE(rb.bodyType() == Body_t::count);
+        REQUIRE(rb.bodyType() == BodyType::count);
         REQUIRE(rb.bound() == 1);
-        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit_t>{{2, 1}, {-3, 1}, {4, 1}}));
+        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit>{{2, 1}, {-3, 1}, {4, 1}}));
         REQUIRE(spanEq(rb.sum().lits, rb.sumLits()));
         auto r = rb.rule();
         REQUIRE(spanEq(r.head, rb.head()));
-        REQUIRE(r.bt == Body_t::count);
+        REQUIRE(r.bt == BodyType::count);
         REQUIRE(r.agg.bound == 1);
         REQUIRE(spanEq(r.agg.lits, rb.sum().lits));
     }
     SECTION("weaken to normal rule") {
-        rb.start().addHead(1).startSum(3).addGoal(2, 2).addGoal(-3, 2).addGoal(4, 2).weaken(Body_t::normal).end();
+        rb.start().addHead(1).startSum(3).addGoal(2, 2).addGoal(-3, 2).addGoal(4, 2).weaken(BodyType::normal).end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{1}));
-        REQUIRE(rb.bodyType() == Body_t::normal);
+        REQUIRE(rb.bodyType() == BodyType::normal);
         REQUIRE(spanEq(rb.body(), std::vector<Lit_t>{2, -3, 4}));
 
         auto r = rb.rule();
         REQUIRE(spanEq(r.head, rb.head()));
-        REQUIRE(r.bt == Body_t::normal);
+        REQUIRE(r.bt == BodyType::normal);
         REQUIRE(spanEq(r.cond, rb.body()));
     }
     SECTION("weak to normal rule - inverse order") {
-        rb.startSum(3).addGoal(2, 2).addGoal(-3, 2).addGoal(4, 2).start().addHead(1).weaken(Body_t::normal).end();
+        rb.startSum(3).addGoal(2, 2).addGoal(-3, 2).addGoal(4, 2).start().addHead(1).weaken(BodyType::normal).end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{1}));
-        REQUIRE(rb.bodyType() == Body_t::normal);
+        REQUIRE(rb.bodyType() == BodyType::normal);
         REQUIRE(spanEq(rb.body(), std::vector<Lit_t>{2, -3, 4}));
     }
     SECTION("minimize rule") {
@@ -687,18 +691,18 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
             rb.startMinimize(1).addGoal(-3, 2).addGoal(4, 1).addGoal(5).end();
             REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{}));
             REQUIRE(rb.isMinimize());
-            REQUIRE(rb.bodyType() == Body_t::sum);
+            REQUIRE(rb.bodyType() == BodyType::sum);
             REQUIRE(rb.bound() == 1);
-            REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit_t>{{-3, 2}, {4, 1}, {5, 1}}));
+            REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit>{{-3, 2}, {4, 1}, {5, 1}}));
             REQUIRE(spanEq(rb.sum().lits, rb.sumLits()));
         }
         SECTION("explicit body") {
             rb.startMinimize(1).startSum(0).addGoal(-3, 2).addGoal(4, 1).addGoal(5).end();
             REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{}));
             REQUIRE(rb.isMinimize());
-            REQUIRE(rb.bodyType() == Body_t::sum);
+            REQUIRE(rb.bodyType() == BodyType::sum);
             REQUIRE(rb.bound() == 1);
-            REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit_t>{{-3, 2}, {4, 1}, {5, 1}}));
+            REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit>{{-3, 2}, {4, 1}, {5, 1}}));
             REQUIRE(spanEq(rb.sum().lits, rb.sumLits()));
         }
     }
@@ -714,7 +718,7 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
             .addGoal(5)
             .end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{1}));
-        REQUIRE(rb.bodyType() == Body_t::normal);
+        REQUIRE(rb.bodyType() == BodyType::normal);
         REQUIRE(spanEq(rb.body(), std::vector<Lit_t>{5}));
 
         rb.start()
@@ -728,7 +732,7 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
             .addGoal(5)
             .end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{1}));
-        REQUIRE(rb.bodyType() == Body_t::normal);
+        REQUIRE(rb.bodyType() == BodyType::normal);
         REQUIRE(spanEq(rb.body(), std::vector<Lit_t>{5}));
     }
     SECTION("clear head") {
@@ -743,8 +747,8 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
             .addHead(5)
             .end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{5}));
-        REQUIRE(rb.bodyType() == Body_t::sum);
-        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit_t>{{2, 2}, {-3, 2}, {4, 2}}));
+        REQUIRE(rb.bodyType() == BodyType::sum);
+        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit>{{2, 2}, {-3, 2}, {4, 2}}));
         REQUIRE(spanEq(rb.sum().lits, rb.sumLits()));
 
         rb.start()
@@ -758,16 +762,16 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
             .addHead(5)
             .end();
         REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{5}));
-        REQUIRE(rb.bodyType() == Body_t::sum);
-        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit_t>{{2, 2}, {-3, 2}, {4, 2}}));
+        REQUIRE(rb.bodyType() == BodyType::sum);
+        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit>{{2, 2}, {-3, 2}, {4, 2}}));
         REQUIRE(spanEq(rb.sum().lits, rb.sumLits()));
     }
 
     SECTION("copy and move") {
         rb.start().addHead(1).startSum(25);
-        std::vector<WeightLit_t> exp;
+        std::vector<WeightLit> exp;
         for (int i = 2; i != 20; ++i) {
-            auto wl = WeightLit_t{(i & 1) ? i : -i, i};
+            auto wl = WeightLit{(i & 1) ? i : -i, i};
             rb.addGoal(wl);
             exp.push_back(wl);
         }
@@ -782,7 +786,7 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
             REQUIRE(copy.sum().bound == 25);
             REQUIRE(spanEq(copy.sumLits(), exp));
 
-            auto newLit = WeightLit_t{4711, 31};
+            auto newLit = WeightLit{4711, 31};
             copy.addGoal(newLit);
             REQUIRE(spanEq(rb.sumLits(), exp));
 
@@ -800,7 +804,7 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
 
             rb.start().addHead(1).addGoal(2).addGoal(-3).end();
             REQUIRE(spanEq(rb.head(), std::vector<Atom_t>{1}));
-            REQUIRE(rb.bodyType() == Body_t::normal);
+            REQUIRE(rb.bodyType() == BodyType::normal);
             REQUIRE(spanEq(rb.body(), std::vector{2, -3}));
         }
         SECTION("memcpy") {
@@ -816,7 +820,7 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
             REQUIRE(spanEq(mc.head(), std::vector<Atom_t>{1}));
             REQUIRE(mc.sum().bound == 25);
             REQUIRE(spanEq(mc.sumLits(), exp));
-            auto newLit = WeightLit_t{4711, 31};
+            auto newLit = WeightLit{4711, 31};
             mc.addGoal(newLit);
             exp.push_back(newLit);
             REQUIRE(spanEq(mc.sumLits(), exp));
@@ -852,9 +856,9 @@ TEST_CASE("Test RuleBuilder", "[rule]") {
     SECTION("grow bug") {
         for (int i = 0; i != 12; ++i) { rb.addHead(static_cast<Atom_t>(i + 1)); }
         rb.startSum(22).addGoal(47, 11).addGoal(18, 15).addGoal(17, 7).end();
-        REQUIRE(rb.bodyType() == Body_t::sum);
+        REQUIRE(rb.bodyType() == BodyType::sum);
         REQUIRE(rb.bound() == 22);
-        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit_t>{{47, 11}, {18, 15}, {17, 7}}));
+        REQUIRE(spanEq(rb.sumLits(), std::vector<WeightLit>{{47, 11}, {18, 15}, {17, 7}}));
     }
 }
 TEST_CASE("Intermediate Format Reader ", "[aspif]") {
@@ -868,7 +872,7 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         REQUIRE(observer.incremental == false);
     }
     SECTION("read empty rule") {
-        rule(input, {Head_t::disjunctive, {}, Body_t::normal, bound_none, {}});
+        rule(input, {HeadType::disjunctive, {}, BodyType::normal, bound_none, {}});
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(observer.rules.size() == 1);
@@ -876,18 +880,18 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         REQUIRE(observer.rules[0].body.empty());
     }
     SECTION("read rules") {
-        Rule rules[] = {{Head_t::disjunctive, {1}, Body_t::normal, bound_none, {{-2, 1}, {3, 1}, {-4, 1}}},
-                        {Head_t::disjunctive, {1, 2, 3}, Body_t::normal, bound_none, {{5, 1}, {-6, 1}}},
-                        {Head_t::disjunctive, {}, Body_t::normal, bound_none, {{1, 1}, {2, 1}}},
-                        {Head_t::choice, {1, 2, 3}, Body_t::normal, bound_none, {{5, 1}, {-6, 1}}},
+        Rule rules[] = {{HeadType::disjunctive, {1}, BodyType::normal, bound_none, {{-2, 1}, {3, 1}, {-4, 1}}},
+                        {HeadType::disjunctive, {1, 2, 3}, BodyType::normal, bound_none, {{5, 1}, {-6, 1}}},
+                        {HeadType::disjunctive, {}, BodyType::normal, bound_none, {{1, 1}, {2, 1}}},
+                        {HeadType::choice, {1, 2, 3}, BodyType::normal, bound_none, {{5, 1}, {-6, 1}}},
                         // weight
-                        {Head_t::disjunctive, {1}, Body_t::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
-                        {Head_t::disjunctive, {2}, Body_t::sum, 1, {{3, 1}, {-4, 1}, {5, 1}}},
+                        {HeadType::disjunctive, {1}, BodyType::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
+                        {HeadType::disjunctive, {2}, BodyType::sum, 1, {{3, 1}, {-4, 1}, {5, 1}}},
                         // mixed
-                        {Head_t::choice, {1, 2}, Body_t::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
-                        {Head_t::disjunctive, {}, Body_t::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
+                        {HeadType::choice, {1, 2}, BodyType::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
+                        {HeadType::disjunctive, {}, BodyType::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
                         // negative weights
-                        {Head_t::disjunctive, {1}, Body_t::sum, 1, {{2, 1}, {-3, -2}, {-4, 3}, {5, 1}}}};
+                        {HeadType::disjunctive, {1}, BodyType::sum, 1, {{2, 1}, {-3, -2}, {-4, 3}, {5, 1}}}};
         using Pair   = std::pair<unsigned, unsigned>;
         Pair basic(0, 4);
         Pair weight(4, 2);
@@ -905,8 +909,8 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         }
     }
     SECTION("read minimize rule") {
-        input << Directive_t::minimize << " -1 3 4 5 6 1 3 2\n";
-        input << Directive_t::minimize << " 10 3 4 -52 -6 36 3 -20\n";
+        input << AspifType::minimize << " -1 3 4 5 6 1 3 2\n";
+        input << AspifType::minimize << " 10 3 4 -52 -6 36 3 -20\n";
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(observer.min.size() == 2);
@@ -914,14 +918,14 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         const auto& mr2 = observer.min[1];
         REQUIRE(mr1.first == -1);
         REQUIRE(mr2.first == 10);
-        auto lits = Vec<WeightLit_t>{{4, 5}, {6, 1}, {3, 2}};
+        auto lits = Vec<WeightLit>{{4, 5}, {6, 1}, {3, 2}};
         REQUIRE(mr1.second == lits);
-        lits = Vec<WeightLit_t>{{4, -52}, {-6, 36}, {3, -20}};
+        lits = Vec<WeightLit>{{4, -52}, {-6, 36}, {3, -20}};
         REQUIRE(mr2.second == lits);
     }
     SECTION("read output") {
-        input << Directive_t::output << " 1 a 1 1\n";
-        input << Directive_t::output << " 10 Hallo Welt 2 1 -2\n";
+        input << AspifType::output << " 1 a 1 1\n";
+        input << AspifType::output << " 10 Hallo Welt 2 1 -2\n";
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(observer.shows.size() == 2);
@@ -933,30 +937,30 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         REQUIRE(s2.second == Vec<Lit_t>({1, -2}));
     }
     SECTION("read projection") {
-        input << Directive_t::project << " 3 1 2 987232\n";
-        input << Directive_t::project << " 1 17\n";
+        input << AspifType::project << " 3 1 2 987232\n";
+        input << AspifType::project << " 1 17\n";
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(observer.projects == Vec<Atom_t>({1, 2, 987232, 17}));
     }
     SECTION("read external") {
-        std::pair<Atom_t, Value_t> exp[] = {
-            {1, Value_t::free}, {2, Value_t::true_}, {3, Value_t::false_}, {4, Value_t::release}};
-        for (auto&& e : exp) { input << Directive_t::external << " " << e.first << " " << e.second << "\n"; }
+        std::pair<Atom_t, TruthValue> exp[] = {
+            {1, TruthValue::free}, {2, TruthValue::true_}, {3, TruthValue::false_}, {4, TruthValue::release}};
+        for (auto&& e : exp) { input << AspifType::external << " " << e.first << " " << e.second << "\n"; }
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(spanEq(observer.externals, std::span{exp, std::size(exp)}));
     }
     SECTION("read assumptions") {
-        input << Directive_t::assume << " 2 1 987232\n";
-        input << Directive_t::assume << " 1 -2\n";
+        input << AspifType::assume << " 2 1 987232\n";
+        input << AspifType::assume << " 1 -2\n";
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(observer.assumes == Vec<Lit_t>({1, 987232, -2}));
     }
     SECTION("read edges") {
-        input << Directive_t::edge << " 0 1 2 1 -2\n";
-        input << Directive_t::edge << " 1 0 1 3\n";
+        input << AspifType::edge << " 0 1 2 1 -2\n";
+        input << AspifType::edge << " 1 0 1 3\n";
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(observer.edges.size() == 2);
@@ -968,12 +972,12 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         REQUIRE(observer.edges[1].cond == Vec<Lit_t>({3}));
     }
     SECTION("read heuristic") {
-        Heuristic exp[] = {{1, Heuristic_t::sign, -1, 1, {10}},
-                           {2, Heuristic_t::level, 10, 3, {-1, 10}},
-                           {1, Heuristic_t::init, 20, 1, {}},
-                           {1, Heuristic_t::factor, 2, 2, {}}};
+        Heuristic exp[] = {{1, DomModifier::sign, -1, 1, {10}},
+                           {2, DomModifier::level, 10, 3, {-1, 10}},
+                           {1, DomModifier::init, 20, 1, {}},
+                           {1, DomModifier::factor, 2, 2, {}}};
         for (auto&& r : exp) {
-            input << Directive_t::heuristic << " " << r.type << " " << r.atom << " " << r.bias << " " << r.prio << " "
+            input << AspifType::heuristic << " " << r.type << " " << r.atom << " " << r.bias << " " << r.prio << " "
                   << r.cond.size();
             for (auto&& p : r.cond) { input << " " << p; }
             input << "\n";
@@ -983,19 +987,19 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         REQUIRE(spanEq(observer.heuristics, std::span{exp, std::size(exp)}));
     }
     SECTION("read theory") {
-        input << Directive_t::theory << " 0 1 200\n"
-              << Directive_t::theory << " 0 6 1\n"
-              << Directive_t::theory << " 0 11 2\n"
-              << Directive_t::theory << " 1 0 4 diff\n"
-              << Directive_t::theory << " 1 2 2 <=\n"
-              << Directive_t::theory << " 1 4 1 -\n"
-              << Directive_t::theory << " 1 5 3 end\n"
-              << Directive_t::theory << " 1 8 5 start\n"
-              << Directive_t::theory << " 2 10 4 2 7 9\n"
-              << Directive_t::theory << " 2 7 5 1 6\n"
-              << Directive_t::theory << " 2 9 8 1 6\n"
-              << Directive_t::theory << " 4 0 1 10 0\n"
-              << Directive_t::theory << " 6 0 0 1 0 2 1\n";
+        input << AspifType::theory << " 0 1 200\n"
+              << AspifType::theory << " 0 6 1\n"
+              << AspifType::theory << " 0 11 2\n"
+              << AspifType::theory << " 1 0 4 diff\n"
+              << AspifType::theory << " 1 2 2 <=\n"
+              << AspifType::theory << " 1 4 1 -\n"
+              << AspifType::theory << " 1 5 3 end\n"
+              << AspifType::theory << " 1 8 5 start\n"
+              << AspifType::theory << " 2 10 4 2 7 9\n"
+              << AspifType::theory << " 2 7 5 1 6\n"
+              << AspifType::theory << " 2 9 8 1 6\n"
+              << AspifType::theory << " 4 0 1 10 0\n"
+              << AspifType::theory << " 6 0 0 1 0 2 1\n";
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(observer.theory.numAtoms() == 1);
@@ -1003,10 +1007,10 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         class AtomVisitor : public TheoryData::Visitor {
         public:
             void visit(const TheoryData& data, Id_t, const TheoryTerm& t) override {
-                if (auto type = t.type(); type == Theory_t::number) {
+                if (auto type = t.type(); type == TheoryTermType::number) {
                     out << t.number();
                 }
-                else if (type == Theory_t::symbol) {
+                else if (type == TheoryTermType::symbol) {
                     out << t.symbol();
                 }
                 else if (t.isFunction()) {
@@ -1038,7 +1042,7 @@ TEST_CASE("Intermediate Format Reader ", "[aspif]") {
         REQUIRE(vis.out.str() == "&diff{-(end(1),start(1))}<=200");
     }
     SECTION("ignore comments") {
-        input << Directive_t::comment << "Hello World" << "\n";
+        input << AspifType::comment << "Hello World" << "\n";
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
     }
@@ -1055,9 +1059,9 @@ TEST_CASE("Intermediate Format Reader supports incremental programs", "[aspif]")
         REQUIRE(observer.nStep == 2);
     }
     SECTION("read rules in each steps") {
-        rule(input, {Head_t::disjunctive, {1, 2}, Body_t::normal, bound_none, {}});
+        rule(input, {HeadType::disjunctive, {1, 2}, BodyType::normal, bound_none, {}});
         finalize(input);
-        rule(input, {Head_t::disjunctive, {3, 4}, Body_t::normal, bound_none, {}});
+        rule(input, {HeadType::disjunctive, {3, 4}, BodyType::normal, bound_none, {}});
         finalize(input);
         REQUIRE(readAspif(input, observer) == 0);
         REQUIRE(observer.incremental == true);
@@ -1090,22 +1094,22 @@ TEST_CASE("Test AspifOutput", "[aspif]") {
     writer.beginStep();
     SECTION("Writer writes rules") {
         Rule rules[] = {
-            {Head_t::disjunctive, {1}, Body_t::normal, bound_none, {{-2, 1}, {3, 1}, {-4, 1}}},
-            {Head_t::disjunctive, {1, 2, 3}, Body_t::normal, bound_none, {{5, 1}, {-6, 1}}},
-            {Head_t::disjunctive, {}, Body_t::normal, bound_none, {{1, 1}, {2, 1}}},
-            {Head_t::choice, {1, 2, 3}, Body_t::normal, bound_none, {{5, 1}, {-6, 1}}},
+            {HeadType::disjunctive, {1}, BodyType::normal, bound_none, {{-2, 1}, {3, 1}, {-4, 1}}},
+            {HeadType::disjunctive, {1, 2, 3}, BodyType::normal, bound_none, {{5, 1}, {-6, 1}}},
+            {HeadType::disjunctive, {}, BodyType::normal, bound_none, {{1, 1}, {2, 1}}},
+            {HeadType::choice, {1, 2, 3}, BodyType::normal, bound_none, {{5, 1}, {-6, 1}}},
             // weight
-            {Head_t::disjunctive, {1}, Body_t::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
-            {Head_t::disjunctive, {2}, Body_t::sum, 1, {{3, 1}, {-4, 1}, {5, 1}}},
+            {HeadType::disjunctive, {1}, BodyType::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
+            {HeadType::disjunctive, {2}, BodyType::sum, 1, {{3, 1}, {-4, 1}, {5, 1}}},
             // mixed
-            {Head_t::choice, {1, 2}, Body_t::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
-            {Head_t::disjunctive, {}, Body_t::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
+            {HeadType::choice, {1, 2}, BodyType::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
+            {HeadType::disjunctive, {}, BodyType::sum, 1, {{2, 1}, {-3, 2}, {-4, 3}, {5, 1}}},
         };
         Vec<Lit_t> temp;
         for (auto&& r : rules) {
-            if (r.bt == Body_t::normal) {
+            if (r.bt == BodyType::normal) {
                 temp.clear();
-                std::ranges::transform(r.body, std::back_inserter(temp), [](const WeightLit_t& x) { return x.lit; });
+                std::ranges::transform(r.body, std::back_inserter(temp), [](const WeightLit& x) { return x.lit; });
                 writer.rule(r.ht, r.head, temp);
             }
             else {
@@ -1117,8 +1121,8 @@ TEST_CASE("Test AspifOutput", "[aspif]") {
         for (auto&& r : rules) { REQUIRE(std::ranges::find(observer.rules, r) != observer.rules.end()); }
     }
     SECTION("Writer writes minimize") {
-        auto m1 = Vec<WeightLit_t>{{1, -2}, {-3, 2}, {4, 1}};
-        auto m2 = Vec<WeightLit_t>{{-10, 1}, {-20, 2}};
+        auto m1 = Vec<WeightLit>{{1, -2}, {-3, 2}, {4, 1}};
+        auto m2 = Vec<WeightLit>{{-10, 1}, {-20, 2}};
         writer.minimize(1, m1);
         writer.minimize(-2, m2);
         writer.endStep();
@@ -1137,8 +1141,8 @@ TEST_CASE("Test AspifOutput", "[aspif]") {
         for (auto&& s : exp) { REQUIRE(std::ranges::find(observer.shows, s) != observer.shows.end()); }
     }
     SECTION("Writer writes external") {
-        std::pair<Atom_t, Value_t> exp[] = {
-            {1, Value_t::free}, {2, Value_t::true_}, {3, Value_t::false_}, {4, Value_t::release}};
+        std::pair<Atom_t, TruthValue> exp[] = {
+            {1, TruthValue::free}, {2, TruthValue::true_}, {3, TruthValue::false_}, {4, TruthValue::release}};
         for (auto&& e : exp) { writer.external(e.first, e.second); }
         writer.endStep();
         readAspif(out, observer);
@@ -1168,10 +1172,10 @@ TEST_CASE("Test AspifOutput", "[aspif]") {
         REQUIRE(spanEq(observer.edges, std::span{exp, std::size(exp)}));
     }
     SECTION("Writer writes heuristics") {
-        Heuristic exp[] = {{1, Heuristic_t::sign, -1, 1, {10}},
-                           {2, Heuristic_t::level, 10, 3, {-1, 10}},
-                           {1, Heuristic_t::init, 20, 1, {}},
-                           {1, Heuristic_t::factor, 2, 2, {}}};
+        Heuristic exp[] = {{1, DomModifier::sign, -1, 1, {10}},
+                           {2, DomModifier::level, 10, 3, {-1, 10}},
+                           {1, DomModifier::init, 20, 1, {}},
+                           {1, DomModifier::factor, 2, 2, {}}};
         for (auto&& h : exp) { writer.heuristic(h.atom, h.type, h.bias, h.prio, h.cond); }
         writer.endStep();
         readAspif(out, observer);
@@ -1188,7 +1192,7 @@ TEST_CASE("TheoryData", "[aspif]") {
     SECTION("Term 0 is ok") {
         data.addTerm(0, 0);
         REQUIRE(data.hasTerm(0));
-        REQUIRE(data.getTerm(0).type() == Theory_t::number);
+        REQUIRE(data.getTerm(0).type() == TheoryTermType::number);
     }
 
     SECTION("Visit theory") {
@@ -1236,9 +1240,9 @@ TEST_CASE("TheoryData", "[aspif]") {
                     return;
                 }
                 switch (t.type()) {
-                    case Theory_t::number: out.addTerm(termId, t.number()); break;
-                    case Theory_t::symbol: out.addTerm(termId, t.symbol()); break;
-                    case Theory_t::compound:
+                    case TheoryTermType::number: out.addTerm(termId, t.number()); break;
+                    case TheoryTermType::symbol: out.addTerm(termId, t.symbol()); break;
+                    case TheoryTermType::compound:
                         data.accept(t, *this);
                         if (t.isFunction()) {
                             out.addTerm(termId, t.function(), t.terms());
diff --git a/tests/test_common.h b/tests/test_common.h
index c440400..04b85bb 100644
--- a/tests/test_common.h
+++ b/tests/test_common.h
@@ -31,30 +31,26 @@ template <class T>
 using Vec = std::vector<T>;
 
 struct Rule {
-    Head_t           ht;
-    Vec<Atom_t>      head;
-    Body_t           bt;
-    Weight_t         bnd;
-    Vec<WeightLit_t> body;
-    bool             operator==(const Rule& rhs) const {
-        return ht == rhs.ht && head == rhs.head && bt == rhs.bt && bnd == rhs.bnd && body == rhs.body;
-    }
+    HeadType       ht;
+    Vec<Atom_t>    head;
+    BodyType       bt;
+    Weight_t       bnd;
+    Vec<WeightLit> body;
+    bool           operator==(const Rule& rhs) const = default;
 };
 struct Edge {
     int        s;
     int        t;
     Vec<Lit_t> cond;
-    bool       operator==(const Edge& rhs) const { return s == rhs.s && t == rhs.t && cond == rhs.cond; }
+    bool       operator==(const Edge& rhs) const = default;
 };
 struct Heuristic {
     Atom_t      atom;
-    Heuristic_t type;
+    DomModifier type;
     int         bias;
     unsigned    prio;
     Vec<Lit_t>  cond;
-    bool        operator==(const Heuristic& rhs) const {
-        return atom == rhs.atom && type == rhs.type && bias == rhs.bias && prio == rhs.prio && cond == rhs.cond;
-    }
+    bool        operator==(const Heuristic& rhs) const = default;
 };
 
 class ReadObserver : public AbstractProgram {
@@ -63,7 +59,7 @@ class ReadObserver : public AbstractProgram {
     void beginStep() override { ++nStep; }
     void endStep() override {}
 
-    void heuristic(Atom_t a, Heuristic_t t, int bias, unsigned prio, const LitSpan& cond) override {
+    void heuristic(Atom_t a, DomModifier t, int bias, unsigned prio, const LitSpan& cond) override {
         heuristics.push_back({a, t, bias, prio, {begin(cond), end(cond)}});
     }
     void acycEdge(int s, int t, const LitSpan& cond) override { edges.push_back({s, t, {begin(cond), end(cond)}}); }
diff --git a/tests/test_smodels.cpp b/tests/test_smodels.cpp
index aad5a3d..f1b7b03 100644
--- a/tests/test_smodels.cpp
+++ b/tests/test_smodels.cpp
@@ -55,13 +55,13 @@ static void finalize(std::stringstream& str, const AtomTab& atoms = AtomTab(), c
     str << "0\n1\n";
 }
 
-using Rule_t = SmodelsRule_t;
+using Rule_t = SmodelsType;
 
 class ReadObserver : public Test::ReadObserver {
 public:
-    void rule(Head_t ht, const AtomSpan& head, const LitSpan& body) override {
+    void rule(HeadType ht, const AtomSpan& head, const LitSpan& body) override {
         if (head.empty()) {
-            if (ht == Head_t::choice) {
+            if (ht == HeadType::choice) {
                 return;
             }
             compute.push_back(-lit(body[0]));
@@ -69,18 +69,18 @@ class ReadObserver : public Test::ReadObserver {
         else {
             Rule_t           rt = Rule_t::basic;
             std::vector<int> r(1, lit(head[0]));
-            if (size(head) > 1 || ht == Head_t::choice) {
+            if (size(head) > 1 || ht == HeadType::choice) {
                 r[0] = static_cast<int>(size(head));
                 r.insert(r.end(), begin(head), end(head));
-                rt = ht == Head_t::choice ? Rule_t::choice : Rule_t::disjunctive;
+                rt = ht == HeadType::choice ? Rule_t::choice : Rule_t::disjunctive;
             }
             r.insert(r.end(), begin(body), end(body));
             rules[rt].push_back(std::move(r));
         }
     }
-    void rule(Head_t ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override {
+    void rule(HeadType ht, const AtomSpan& head, Weight_t bound, const WeightLitSpan& body) override {
         REQUIRE(size(head) == 1);
-        REQUIRE(ht == Head_t::disjunctive);
+        REQUIRE(ht == HeadType::disjunctive);
         std::vector<int> r(1, lit(head[0]));
         r.push_back(bound);
         auto hasWeights = std::ranges::any_of(body, [](const auto& wl) { return weight(wl) != 1; });
@@ -109,8 +109,8 @@ class ReadObserver : public Test::ReadObserver {
         atoms[*begin(cond)].assign(begin(str), end(str));
     }
 
-    void external(Atom_t a, Value_t v) override {
-        if (v != Value_t::release) {
+    void external(Atom_t a, TruthValue v) override {
+        if (v != TruthValue::release) {
             rules[Rule_t::clasp_assign_ext].push_back(RawRule{static_cast<int>(a), static_cast<int>(v)});
         }
         else {
@@ -230,9 +230,9 @@ TEST_CASE("SmodelsExtReader ", "[smodels][smodels_ext]") {
         finalize(input);
         REQUIRE(Potassco::readSmodels(input, observer, opts) == 0);
         REQUIRE(observer.rules[Rule_t::clasp_assign_ext].size() == 3);
-        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][0] == RawRule({2, static_cast<int>(Value_t::false_)}));
-        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][1] == RawRule({3, static_cast<int>(Value_t::true_)}));
-        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][2] == RawRule({4, static_cast<int>(Value_t::free)}));
+        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][0] == RawRule({2, static_cast<int>(TruthValue::false_)}));
+        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][1] == RawRule({3, static_cast<int>(TruthValue::true_)}));
+        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][2] == RawRule({4, static_cast<int>(TruthValue::free)}));
     }
     SECTION("read release") {
         input << "91 2 0\n";
@@ -241,7 +241,7 @@ TEST_CASE("SmodelsExtReader ", "[smodels][smodels_ext]") {
         REQUIRE(Potassco::readSmodels(input, observer, opts) == 0);
         REQUIRE(observer.rules[Rule_t::clasp_assign_ext].size() == 1);
         REQUIRE(observer.rules[Rule_t::clasp_release_ext].size() == 1);
-        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][0] == RawRule({2, static_cast<int>(Value_t::false_)}));
+        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][0] == RawRule({2, static_cast<int>(TruthValue::false_)}));
         REQUIRE(observer.rules[Rule_t::clasp_release_ext][0] == RawRule({2}));
     }
 }
@@ -257,8 +257,8 @@ TEST_CASE("Write smodels", "[smodels]") {
         REQUIRE(str.str() == exp.str());
     }
     SECTION("constraints require false atom") {
-        REQUIRE_THROWS_AS(writer.rule(Head_t::disjunctive, {}, {}), std::logic_error);
-        REQUIRE_NOTHROW(writer.rule(Head_t::choice, {}, {}));
+        REQUIRE_THROWS_AS(writer.rule(HeadType::disjunctive, {}, {}), std::logic_error);
+        REQUIRE_NOTHROW(writer.rule(HeadType::choice, {}, {}));
         writer.endStep();
         exp << "0\n0\nB+\n0\nB-\n0\n1\n";
         REQUIRE(str.str() == exp.str());
@@ -266,16 +266,16 @@ TEST_CASE("Write smodels", "[smodels]") {
         str.str("");
         SmodelsOutput withFalse(str, false, 1);
         Vec<Lit_t>    body = {2, -3, -4, 5};
-        REQUIRE_NOTHROW(withFalse.rule(Head_t::disjunctive, {}, body));
-        Vec<WeightLit_t> wbody = {{2, 2}, {-3, 1}, {-4, 3}, {5, 4}};
-        REQUIRE_NOTHROW(withFalse.rule(Head_t::disjunctive, {}, 2, wbody));
+        REQUIRE_NOTHROW(withFalse.rule(HeadType::disjunctive, {}, body));
+        Vec<WeightLit> wbody = {{2, 2}, {-3, 1}, {-4, 3}, {5, 4}};
+        REQUIRE_NOTHROW(withFalse.rule(HeadType::disjunctive, {}, 2, wbody));
         REQUIRE(str.str().find("1 1 4 2 3 4 2 5") != std::string::npos);
         REQUIRE(str.str().find("5 1 2 4 2 3 4 2 5 1 3 2 4") != std::string::npos);
     }
     SECTION("body literals are correctly reordered") {
         Atom_t     a    = 1;
         Vec<Lit_t> body = {2, -3, -4, 5};
-        writer.rule(Head_t::disjunctive, toSpan(a), body);
+        writer.rule(HeadType::disjunctive, toSpan(a), body);
         writer.endStep();
         REQUIRE(readSmodels(str, observer) == 0);
         REQUIRE(observer.rules[Rule_t::basic].size() == 1);
@@ -283,9 +283,9 @@ TEST_CASE("Write smodels", "[smodels]") {
         REQUIRE(observer.rules[Rule_t::basic][0] == r);
     }
     SECTION("body literals with weights are correctly reordered") {
-        Atom_t           a    = 1;
-        Vec<WeightLit_t> body = {{2, 2}, {-3, 1}, {-4, 3}, {5, 4}};
-        writer.rule(Head_t::disjunctive, toSpan(a), 4, body);
+        Atom_t         a    = 1;
+        Vec<WeightLit> body = {{2, 2}, {-3, 1}, {-4, 3}, {5, 4}};
+        writer.rule(HeadType::disjunctive, toSpan(a), 4, body);
         writer.endStep();
         REQUIRE(readSmodels(str, observer) == 0);
         REQUIRE(observer.rules[Rule_t::weight].size() == 1);
@@ -293,9 +293,9 @@ TEST_CASE("Write smodels", "[smodels]") {
         REQUIRE(observer.rules[Rule_t::weight][0] == r);
     }
     SECTION("weights are removed from count bodies") {
-        Atom_t           a    = 1;
-        Vec<WeightLit_t> body = {{2, 1}, {-3, 1}, {-4, 1}, {5, 1}};
-        writer.rule(Head_t::disjunctive, toSpan(a), 3, body);
+        Atom_t         a    = 1;
+        Vec<WeightLit> body = {{2, 1}, {-3, 1}, {-4, 1}, {5, 1}};
+        writer.rule(HeadType::disjunctive, toSpan(a), 3, body);
         writer.endStep();
         REQUIRE(readSmodels(str, observer) == 0);
         REQUIRE(observer.rules[Rule_t::cardinality].size() == 1);
@@ -304,8 +304,8 @@ TEST_CASE("Write smodels", "[smodels]") {
     }
     SECTION("all head atoms are written") {
         Vec<Atom_t> atoms = {1, 2, 3, 4};
-        writer.rule(Head_t::disjunctive, atoms, {});
-        writer.rule(Head_t::choice, atoms, {});
+        writer.rule(HeadType::disjunctive, atoms, {});
+        writer.rule(HeadType::choice, atoms, {});
         writer.endStep();
         REQUIRE(readSmodels(str, observer) == 0);
         REQUIRE(observer.rules[Rule_t::disjunctive].size() == 1);
@@ -315,7 +315,7 @@ TEST_CASE("Write smodels", "[smodels]") {
         REQUIRE(observer.rules[Rule_t::choice][0] == r);
     }
     SECTION("minimize rules are written without priority") {
-        Vec<WeightLit_t> body = {{2, 2}, {-3, 1}, {-4, 3}, {5, 4}};
+        Vec<WeightLit> body = {{2, 2}, {-3, 1}, {-4, 3}, {5, 4}};
         writer.minimize(10, body);
         writer.endStep();
         REQUIRE(readSmodels(str, observer) == 0);
@@ -324,7 +324,7 @@ TEST_CASE("Write smodels", "[smodels]") {
         REQUIRE(observer.rules[Rule_t::optimize][0] == r);
     }
     SECTION("minimize lits with negative weights are inverted") {
-        Vec<WeightLit_t> body = {{2, -2}, {3, 1}, {4, -1}};
+        Vec<WeightLit> body = {{2, -2}, {3, 1}, {4, -1}};
         writer.minimize(10, body);
         writer.endStep();
         REQUIRE(readSmodels(str, observer) == 0);
@@ -345,12 +345,12 @@ TEST_CASE("Write smodels", "[smodels]") {
         std::string an = "Hallo";
         writer.output(an, toSpan(a));
         Atom_t b = 2;
-        REQUIRE_THROWS(writer.rule(Head_t::disjunctive, toSpan(b), {}));
+        REQUIRE_THROWS(writer.rule(HeadType::disjunctive, toSpan(b), {}));
     }
     SECTION("compute statement is written via assume") {
         Atom_t     a    = 1;
         Vec<Lit_t> body = {2, -3, -4, 5};
-        writer.rule(Head_t::disjunctive, toSpan(a), body);
+        writer.rule(HeadType::disjunctive, toSpan(a), body);
         Lit_t na = -1;
         writer.assume(toSpan(na));
         writer.endStep();
@@ -377,8 +377,8 @@ TEST_CASE("Write smodels", "[smodels]") {
     }
     SECTION("complex directives are not supported") {
         REQUIRE_THROWS(writer.project({}));
-        REQUIRE_THROWS(writer.external(1, Value_t::false_));
-        REQUIRE_THROWS(writer.heuristic(1, Heuristic_t::sign, 1, 0, {}));
+        REQUIRE_THROWS(writer.external(1, TruthValue::false_));
+        REQUIRE_THROWS(writer.heuristic(1, DomModifier::sign, 1, 0, {}));
         REQUIRE_THROWS(writer.acycEdge(1, 2, {}));
     }
 }
@@ -386,7 +386,7 @@ TEST_CASE("Write smodels", "[smodels]") {
 TEST_CASE("Match heuristic predicate", "[smodels]") {
     const char*      in;
     std::string_view atom;
-    Heuristic_t      type;
+    DomModifier      type;
     int              bias;
     unsigned         prio;
     SECTION("do not match invalid predicate name") {
@@ -422,14 +422,14 @@ TEST_CASE("Match heuristic predicate", "[smodels]") {
     }
     SECTION("match complex atom name") {
         REQUIRE(matchDomHeuPred(in = "_heuristic(_heuristic(x,y,z),init,1)", atom, type, bias, prio));
-        REQUIRE(type == Heuristic_t::init);
+        REQUIRE(type == DomModifier::init);
 
         REQUIRE(matchDomHeuPred(in = "_heuristic(a(\"foo\"),init,1)", atom, type, bias, prio));
-        REQUIRE(type == Heuristic_t::init);
+        REQUIRE(type == DomModifier::init);
         REQUIRE(atom == R"(a("foo"))");
 
         REQUIRE(matchDomHeuPred(in = "_heuristic(a(\"fo\\\"o\"),init,1)", atom, type, bias, prio));
-        REQUIRE(type == Heuristic_t::init);
+        REQUIRE(type == DomModifier::init);
         REQUIRE(atom == "a(\"fo\\\"o\")");
     }
     SECTION("do not match out of bounds") {
@@ -489,15 +489,15 @@ TEST_CASE("SmodelsOutput supports extended programs", "[smodels_ext]") {
     writer.initProgram(true);
     writer.beginStep();
     exp << "90 0\n";
-    Vec<Atom_t>      head = {1, 2};
-    Vec<Lit_t>       body = {3, -4};
-    Vec<WeightLit_t> min  = {{-1, 2}, {2, 1}};
-    writer.rule(Head_t::choice, head, body);
+    Vec<Atom_t>    head = {1, 2};
+    Vec<Lit_t>     body = {3, -4};
+    Vec<WeightLit> min  = {{-1, 2}, {2, 1}};
+    writer.rule(HeadType::choice, head, body);
     exp << static_cast<int>(Rule_t::choice) << " 2 2 3 2 1 5 4\n";
-    writer.external(3, Value_t::false_);
-    writer.external(4, Value_t::false_);
+    writer.external(3, TruthValue::false_);
+    writer.external(4, TruthValue::false_);
     writer.minimize(0, min);
-    writer.heuristic(1, Heuristic_t::sign, 1, 0, {});
+    writer.heuristic(1, DomModifier::sign, 1, 0, {});
     exp << "1 6 0 0\n";
     exp << static_cast<int>(Rule_t::optimize) << " 0 2 1 2 3 2 1\n";
     exp << static_cast<int>(Rule_t::clasp_assign_ext) << " 4 0\n";
@@ -508,7 +508,7 @@ TEST_CASE("SmodelsOutput supports extended programs", "[smodels_ext]") {
     exp << "90 0\n";
     head[0] = 3;
     head[1] = 4;
-    writer.rule(Head_t::choice, head, {});
+    writer.rule(HeadType::choice, head, {});
     exp << static_cast<int>(Rule_t::choice) << " 2 4 5 0 0\n";
     writer.endStep();
     exp << "0\n0\nB+\n0\nB-\n1\n0\n1\n";
@@ -517,7 +517,7 @@ TEST_CASE("SmodelsOutput supports extended programs", "[smodels_ext]") {
 
 TEST_CASE("Convert to smodels", "[convert]") {
     using BodyLits = std::initializer_list<Lit_t>;
-    using AggLits  = std::initializer_list<WeightLit_t>;
+    using AggLits  = std::initializer_list<WeightLit>;
     ReadObserver   observer;
     SmodelsConvert convert(observer, true);
     convert.initProgram(false);
@@ -525,7 +525,7 @@ TEST_CASE("Convert to smodels", "[convert]") {
     SECTION("convert rule") {
         Atom_t   a    = 1;
         BodyLits lits = {4, -3, -2, 5};
-        convert.rule(Head_t::disjunctive, toSpan(a), lits);
+        convert.rule(HeadType::disjunctive, toSpan(a), lits);
         REQUIRE(observer.rules[Rule_t::basic].size() == 1);
         RawRule r = {convert.get(lit(a)), convert.get(4), convert.get(-3), convert.get(-2), convert.get(5)};
         REQUIRE(observer.rules[Rule_t::basic][0] == r);
@@ -533,7 +533,7 @@ TEST_CASE("Convert to smodels", "[convert]") {
     SECTION("convert sum rule") {
         Atom_t  a    = 1;
         AggLits lits = {{4, 2}, {-3, 3}, {-2, 1}, {5, 4}};
-        convert.rule(Head_t::disjunctive, toSpan(a), 3, lits);
+        convert.rule(HeadType::disjunctive, toSpan(a), 3, lits);
         REQUIRE(observer.rules[Rule_t::weight].size() == 1);
         RawRule sr = {convert.get(lit(a)), 3, convert.get(4), 2, convert.get(-3), 3,
                       convert.get(-2),     1, convert.get(5), 4};
@@ -542,7 +542,7 @@ TEST_CASE("Convert to smodels", "[convert]") {
     SECTION("convert mixed rule") {
         std::initializer_list<Atom_t> h    = {1, 2, 3};
         AggLits                       lits = {{4, 2}, {-3, 3}, {-2, 1}, {5, 4}};
-        convert.rule(Head_t::choice, h, 3, lits);
+        convert.rule(HeadType::choice, h, 3, lits);
         REQUIRE(observer.rules[Rule_t::choice].size() == 1);
         REQUIRE(observer.rules[Rule_t::weight].size() == 1);
         int     aux = static_cast<int>(convert.maxAtom());
@@ -554,7 +554,7 @@ TEST_CASE("Convert to smodels", "[convert]") {
     SECTION("convert satisfied sum rule") {
         Atom_t  a    = 1;
         AggLits lits = {{4, 2}, {-3, 3}, {-2, 1}, {5, 4}};
-        convert.rule(Head_t::disjunctive, toSpan(a), -3, lits);
+        convert.rule(HeadType::disjunctive, toSpan(a), -3, lits);
         REQUIRE(observer.rules[Rule_t::weight].empty());
         REQUIRE(observer.rules[Rule_t::basic].size() == 1);
         RawRule sr = {convert.get(lit(a))};
@@ -563,7 +563,7 @@ TEST_CASE("Convert to smodels", "[convert]") {
     SECTION("convert invalid rule") {
         std::initializer_list<Atom_t> h       = {1, 2, 3};
         AggLits                       invalid = {{4, 2}, {-3, -3}};
-        REQUIRE_THROWS_AS(convert.rule(Head_t::choice, h, 2, invalid), std::logic_error);
+        REQUIRE_THROWS_AS(convert.rule(HeadType::choice, h, 2, invalid), std::logic_error);
     }
 
     SECTION("convert minimize") {
@@ -592,16 +592,16 @@ TEST_CASE("Convert to smodels", "[convert]") {
     }
 
     SECTION("convert external") {
-        convert.external(1, Value_t::free);
-        convert.external(2, Value_t::true_);
-        convert.external(3, Value_t::false_);
-        convert.external(4, Value_t::release);
+        convert.external(1, TruthValue::free);
+        convert.external(2, TruthValue::true_);
+        convert.external(3, TruthValue::false_);
+        convert.external(4, TruthValue::release);
         convert.endStep();
         REQUIRE(observer.rules[Rule_t::clasp_assign_ext].size() == 3);
         REQUIRE(observer.rules[Rule_t::clasp_release_ext].size() == 1);
-        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][0][1] == int(Value_t::free));
-        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][1][1] == int(Value_t::true_));
-        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][2][1] == int(Value_t::false_));
+        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][0][1] == int(TruthValue::free));
+        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][1][1] == int(TruthValue::true_));
+        REQUIRE(observer.rules[Rule_t::clasp_assign_ext][2][1] == int(TruthValue::false_));
     }
     SECTION("edges are converted to atoms") {
         Lit_t a = 1;
@@ -618,7 +618,7 @@ TEST_CASE("Convert to smodels", "[convert]") {
     SECTION("heuristics are converted to atoms") {
         SECTION("empty condition") {
             Lit_t a = 1;
-            convert.heuristic(static_cast<Atom_t>(a), Heuristic_t::factor, 10, 2, {});
+            convert.heuristic(static_cast<Atom_t>(a), DomModifier::factor, 10, 2, {});
             convert.output("a", toSpan(a));
             convert.endStep();
             REQUIRE(observer.rules[Rule_t::basic].size() == 1);
@@ -629,8 +629,8 @@ TEST_CASE("Convert to smodels", "[convert]") {
             Lit_t a = 1, b = 2, c = 3;
             convert.output("a", toSpan(a));
             convert.output("b", toSpan(b));
-            convert.heuristic(static_cast<Atom_t>(a), Heuristic_t::level, 10, 2, toSpan(b));
-            convert.heuristic(static_cast<Atom_t>(a), Heuristic_t::init, 10, 2, toSpan(c));
+            convert.heuristic(static_cast<Atom_t>(a), DomModifier::level, 10, 2, toSpan(b));
+            convert.heuristic(static_cast<Atom_t>(a), DomModifier::init, 10, 2, toSpan(c));
             convert.endStep();
             REQUIRE(observer.rules[Rule_t::basic].size() == 1);
             REQUIRE(observer.atoms[observer.rules[Rule_t::basic][0][0]] == "_heuristic(a,level,10,2)");
@@ -638,7 +638,7 @@ TEST_CASE("Convert to smodels", "[convert]") {
         }
         SECTION("unused atom is ignored") {
             Lit_t a = 1;
-            convert.heuristic(static_cast<Atom_t>(a), Heuristic_t::sign, -1, 2, {});
+            convert.heuristic(static_cast<Atom_t>(a), DomModifier::sign, -1, 2, {});
             convert.endStep();
             REQUIRE(observer.rules[Rule_t::basic].size() == 1);
             REQUIRE(convert.maxAtom() == 2);
@@ -646,8 +646,8 @@ TEST_CASE("Convert to smodels", "[convert]") {
         }
         SECTION("unnamed atom requires aux name") {
             Atom_t a = 1;
-            convert.rule(Head_t::choice, toSpan(a), {});
-            convert.heuristic(a, Heuristic_t::sign, -1, 2, {});
+            convert.rule(HeadType::choice, toSpan(a), {});
+            convert.heuristic(a, DomModifier::sign, -1, 2, {});
             convert.endStep();
             REQUIRE(observer.rules[Rule_t::basic].size() == 1);
             REQUIRE(convert.maxAtom() == 3);
@@ -666,7 +666,7 @@ TEST_CASE("Test Atom to directive conversion", "[clasp]") {
     std::vector<Atom_t> atoms = {1, 2, 3, 4, 5, 6};
     writer.initProgram(false);
     writer.beginStep();
-    writer.rule(Potassco::Head_t::choice, atoms, {});
+    writer.rule(Potassco::HeadType::choice, atoms, {});
     SECTION("_edge(X,Y) atoms are converted to edges directives") {
         Lit_t a = 1, b = 2, c = 3;
         writer.output("_edge(1,2)", toSpan(a));
@@ -723,10 +723,10 @@ TEST_CASE("Test Atom to directive conversion", "[clasp]") {
         }
 
         REQUIRE(observer.heuristics.size() == 4);
-        Heuristic exp[] = {{static_cast<Atom_t>(a), Heuristic_t::sign, -1, 1, {h1}},
-                           {static_cast<Atom_t>(a), Heuristic_t::true_, 1, 1, {h2}},
-                           {static_cast<Atom_t>(b), Heuristic_t::level, -1, 10, {h3}},
-                           {static_cast<Atom_t>(b), Heuristic_t::factor, 2, 1, {h4}}};
+        Heuristic exp[] = {{static_cast<Atom_t>(a), DomModifier::sign, -1, 1, {h1}},
+                           {static_cast<Atom_t>(a), DomModifier::true_, 1, 1, {h2}},
+                           {static_cast<Atom_t>(b), DomModifier::level, -1, 10, {h3}},
+                           {static_cast<Atom_t>(b), DomModifier::factor, 2, 1, {h4}}};
         REQUIRE(std::equal(std::begin(exp), std::end(exp), observer.heuristics.begin()) == true);
     }
 }
diff --git a/tests/test_string_convert.cpp b/tests/test_string_convert.cpp
index 3e900e5..7d7c642 100644
--- a/tests/test_string_convert.cpp
+++ b/tests/test_string_convert.cpp
@@ -295,53 +295,51 @@ TEST_CASE("String conversion", "[string]") {
     }
 }
 
-enum class Foo_t : unsigned { Value1 = 0, Value2 = 1, Value3 = 2, Value4, Value5 = 7, Value6 = 7 + 1 };
-[[maybe_unused]] consteval auto enable_meta(std::type_identity<Foo_t>) {
-    return Potassco::reflectEntries<Foo_t, 0u, 8u>();
-}
+enum class Foo : unsigned { Value1 = 0, Value2 = 1, Value3 = 2, Value4, Value5 = 7, Value6 = 7 + 1 };
+[[maybe_unused]] consteval auto enable_meta(std::type_identity<Foo>) { return Potassco::reflectEntries<Foo, 0u, 8u>(); }
 
 using namespace std::literals;
-static_assert(Potassco::enum_count<Foo_t>() == 6, "Wrong count");
-static_assert(Potassco::enum_name(Foo_t::Value3) == "Value3"sv, "Wrong name");
+static_assert(Potassco::enum_count<Foo>() == 6, "Wrong count");
+static_assert(Potassco::enum_name(Foo::Value3) == "Value3"sv, "Wrong name");
 TEST_CASE("Enum entries", "[enum]") {
-    using P = std::pair<Foo_t, std::string_view>;
-    using enum Foo_t;
-
-    REQUIRE(Potassco::enum_entries<Foo_t>() == std::array{P(Value1, "Value1"sv), P(Value2, "Value2"sv),
-                                                          P(Value3, "Value3"sv), P(Value4, "Value4"sv),
-                                                          P(Value5, "Value5"sv), P(Value6, "Value6"sv)});
-
-    REQUIRE(Potassco::enum_min<Foo_t>() == 0);
-    REQUIRE(Potassco::enum_max<Foo_t>() == 8);
-    REQUIRE_FALSE(Potassco::enum_cast<Foo_t>(4).has_value());
-    REQUIRE_FALSE(Potassco::enum_cast<Foo_t>(5).has_value());
-    REQUIRE_FALSE(Potassco::enum_cast<Foo_t>(6).has_value());
-    REQUIRE(Potassco::enum_cast<Foo_t>(7) == Foo_t::Value5);
+    using P = std::pair<Foo, std::string_view>;
+    using enum Foo;
+
+    REQUIRE(Potassco::enum_entries<Foo>() == std::array{P(Value1, "Value1"sv), P(Value2, "Value2"sv),
+                                                        P(Value3, "Value3"sv), P(Value4, "Value4"sv),
+                                                        P(Value5, "Value5"sv), P(Value6, "Value6"sv)});
+
+    REQUIRE(Potassco::enum_min<Foo>() == 0);
+    REQUIRE(Potassco::enum_max<Foo>() == 8);
+    REQUIRE_FALSE(Potassco::enum_cast<Foo>(4).has_value());
+    REQUIRE_FALSE(Potassco::enum_cast<Foo>(5).has_value());
+    REQUIRE_FALSE(Potassco::enum_cast<Foo>(6).has_value());
+    REQUIRE(Potassco::enum_cast<Foo>(7) == Foo::Value5);
     enum NoMeta : uint8_t {};
     REQUIRE(Potassco::enum_min<NoMeta>() == 0u);
     REQUIRE(Potassco::enum_max<NoMeta>() == 255u);
 }
 
 TEST_CASE("Enum to string", "[enum]") {
-    REQUIRE(toString(Foo_t::Value1) == "Value1");
-    REQUIRE(toString(Foo_t::Value2) == "Value2");
-    REQUIRE(toString(Foo_t::Value3) == "Value3");
-    REQUIRE(toString(Foo_t::Value4) == "Value4");
-    REQUIRE(toString(Foo_t::Value5) == "Value5");
-    REQUIRE(toString(Foo_t::Value6) == "Value6");
-    Foo_t unknown{12};
+    REQUIRE(toString(Foo::Value1) == "Value1");
+    REQUIRE(toString(Foo::Value2) == "Value2");
+    REQUIRE(toString(Foo::Value3) == "Value3");
+    REQUIRE(toString(Foo::Value4) == "Value4");
+    REQUIRE(toString(Foo::Value5) == "Value5");
+    REQUIRE(toString(Foo::Value6) == "Value6");
+    Foo unknown{12};
     REQUIRE(toString(unknown) == "12");
 }
 
 TEST_CASE("Enum from string", "[enum]") {
-    REQUIRE(string_cast<Foo_t>("Value3") == Foo_t::Value3);
-    REQUIRE(string_cast<Foo_t>("7") == Foo_t::Value5);
-    REQUIRE(string_cast<Foo_t>("Value4") == Foo_t::Value4);
-    REQUIRE(string_cast<Foo_t>("vAlUe4") == Foo_t::Value4);
-    REQUIRE(string_cast<Foo_t>("8") == Foo_t::Value6);
-    REQUIRE_FALSE(string_cast<Foo_t>("9").has_value());
-    REQUIRE_FALSE(string_cast<Foo_t>("Value98").has_value());
-    REQUIRE_FALSE(string_cast<Foo_t>("Value").has_value());
+    REQUIRE(string_cast<Foo>("Value3") == Foo::Value3);
+    REQUIRE(string_cast<Foo>("7") == Foo::Value5);
+    REQUIRE(string_cast<Foo>("Value4") == Foo::Value4);
+    REQUIRE(string_cast<Foo>("vAlUe4") == Foo::Value4);
+    REQUIRE(string_cast<Foo>("8") == Foo::Value6);
+    REQUIRE_FALSE(string_cast<Foo>("9").has_value());
+    REQUIRE_FALSE(string_cast<Foo>("Value98").has_value());
+    REQUIRE_FALSE(string_cast<Foo>("Value").has_value());
 }
 
 } // namespace Potassco::Test
diff --git a/tests/test_text.cpp b/tests/test_text.cpp
index 3957d42..9f73d55 100644
--- a/tests/test_text.cpp
+++ b/tests/test_text.cpp
@@ -235,7 +235,7 @@ TEST_CASE("Text writer ", "[text]") {
     }
     SECTION("classical negation") {
         out.beginStep();
-        out.rule(Head_t::choice, std::vector{static_cast<Atom_t>(1)}, {});
+        out.rule(HeadType::choice, std::vector{static_cast<Atom_t>(1)}, {});
         out.output("-a", std::vector{static_cast<Lit_t>(1)});
         out.output("-8", std::vector{static_cast<Lit_t>(1)});
         out.endStep();
@@ -246,7 +246,7 @@ TEST_CASE("Text writer ", "[text]") {
         Lit_t               cond1(1);
         Lit_t               cond2(2);
         out.beginStep();
-        out.rule(Head_t::choice, head, {});
+        out.rule(HeadType::choice, head, {});
         out.output("-a", toSpan(cond1));
         out.output("x_1", toSpan(cond2));
         out.endStep();
@@ -404,9 +404,9 @@ TEST_CASE("Text writer ", "[text]") {
             out.beginStep();
             std::vector<Atom_t> head;
             std::vector<Lit_t>  cond;
-            out.rule(Head_t::choice, head = {1, 2}, {}); // {1;2}.
-            out.output("x_3", cond = {1});               // #show x_3 : 1.
-            out.output("x_2", cond = {2});               // #show x_2 : 2.
+            out.rule(HeadType::choice, head = {1, 2}, {}); // {1;2}.
+            out.output("x_3", cond = {1});                 // #show x_3 : 1.
+            out.output("x_2", cond = {2});                 // #show x_2 : 2.
             out.endStep();
             REQUIRE(output.str() == "% #program base.\n"
                                     "{x_1;x_2}.\n"
@@ -415,7 +415,7 @@ TEST_CASE("Text writer ", "[text]") {
                                     "#show.\n");
             output.str("");
             out.beginStep();
-            out.rule(Head_t::choice, head = {3}, cond = {1, 2}); // {3} :- 1, 2.
+            out.rule(HeadType::choice, head = {3}, cond = {1, 2}); // {3} :- 1, 2.
             out.endStep();
             REQUIRE(output.str() == "% #program step(1).\n"
                                     "{x_3} :- x_1, x_2.\n");
@@ -426,9 +426,9 @@ TEST_CASE("Text writer ", "[text]") {
         out.beginStep();
         Atom_t a  = 1;
         auto   al = lit(a);
-        out.rule(Head_t::choice, toSpan(a), {}); // {x_1}.
-        out.output("x_1", toSpan(al));           // #show x_1 : x_1. NOTE: uses reserved name "x_1"
-        out.output("a", toSpan(al));             // #show a : x_1.
+        out.rule(HeadType::choice, toSpan(a), {}); // {x_1}.
+        out.output("x_1", toSpan(al));             // #show x_1 : x_1. NOTE: uses reserved name "x_1"
+        out.output("a", toSpan(al));               // #show a : x_1.
         SECTION("unique alternative") {
             out.endStep();
             REQUIRE(output.str() == "{x_1}.\n#show x_1 : x_1.\n#show a : x_1.\n#show.\n");
@@ -444,7 +444,7 @@ TEST_CASE("Text writer ", "[text]") {
         std::vector<Lit_t>  cond;
         out.initProgram(false);
         out.beginStep();
-        out.rule(Head_t::choice, head = {1, 2, 3, 4, 5}, {});
+        out.rule(HeadType::choice, head = {1, 2, 3, 4, 5}, {});
         out.output("a", cond = {1});
         out.output("a(1,2,3,4,5,6,7,8,9,10,11,12)", cond = {2});
         out.output("b(t(1,2,3))", cond = {3});
@@ -458,7 +458,7 @@ TEST_CASE("Text writer ", "[text]") {
         std::vector<Lit_t>  cond;
         out.initProgram(false);
         out.beginStep();
-        out.rule(Head_t::choice, head = {1}, {});
+        out.rule(HeadType::choice, head = {1}, {});
         SECTION("missing close") { REQUIRE_THROWS_AS(out.output("a(", cond = {1}), std::invalid_argument); }
         SECTION("missing arg") { REQUIRE_THROWS_AS(out.output("a(1,", cond = {1}), std::invalid_argument); }
         SECTION("missing arg on close") { REQUIRE_THROWS_AS(out.output("a(1,)", cond = {1}), std::invalid_argument); }
@@ -580,9 +580,9 @@ TEST_CASE("Text writer writes theory", "[text]") {
     out.beginStep();
     SECTION("parens") {
         using namespace std::literals;
-        CHECK(parens(Tuple_t::paren) == "()"sv);
-        CHECK(parens(Tuple_t::brace) == "{}"sv);
-        CHECK(parens(Tuple_t::bracket) == "[]"sv);
+        CHECK(parens(TupleType::paren) == "()"sv);
+        CHECK(parens(TupleType::brace) == "{}"sv);
+        CHECK(parens(TupleType::bracket) == "[]"sv);
     }
 
     SECTION("write empty atom") {
@@ -612,15 +612,15 @@ TEST_CASE("Text writer writes theory", "[text]") {
         auto ids  = std::vector<Id_t>{};
         REQUIRE_THROWS(out.theoryTerm(3, -4, (ids = {1, 2})));
         SECTION("tuple") {
-            comp = static_cast<int>(Tuple_t::paren);
+            comp = static_cast<int>(TupleType::paren);
             sep  = std::make_pair("("s, ")"s);
         }
         SECTION("set") {
-            comp = static_cast<int>(Tuple_t::brace);
+            comp = static_cast<int>(TupleType::brace);
             sep  = std::make_pair("{"s, "}"s);
         }
         SECTION("list") {
-            comp = static_cast<int>(Tuple_t::bracket);
+            comp = static_cast<int>(TupleType::bracket);
             sep  = std::make_pair("["s, "]"s);
         }
         SECTION("func") {
@@ -664,7 +664,7 @@ TEST_CASE("Text writer writes theory", "[text]") {
     SECTION("Use theory atom in rule") {
         Atom_t head = 2;
         Lit_t  body = 1;
-        out.rule(Head_t::disjunctive, toSpan(head), toSpan(body));
+        out.rule(HeadType::disjunctive, toSpan(head), toSpan(body));
         out.theoryTerm(0, "atom");
         out.theoryTerm(1, "x");
         out.theoryTerm(2, "y");
@@ -686,8 +686,8 @@ TEST_CASE("Text writer writes theory", "[text]") {
         std::vector<Atom_t> head;
         std::vector<Id_t>   ids;
         std::vector<Lit_t>  body;
-        out.rule(Head_t::choice, (head = {1, 2}), {});
-        out.rule(Head_t::disjunctive, (head = {4}), (body = {3}));
+        out.rule(HeadType::choice, (head = {1, 2}), {});
+        out.rule(HeadType::disjunctive, (head = {4}), (body = {3}));
         out.theoryTerm(0, "atom");
         out.theoryTerm(1, "elem");
         out.theoryTerm(2, "p");
@@ -757,7 +757,7 @@ TEST_CASE("Text writer writes theory", "[text]") {
         out.theoryTerm(0, "t");
         std::vector<Atom_t> head;
         std::vector<Lit_t>  body;
-        out.rule(Head_t::choice, (head = {1, 2}), {});
+        out.rule(HeadType::choice, (head = {1, 2}), {});
         out.output("a", (body = {1}));
         out.output("b", (body = {2}));
         out.endStep();
@@ -767,7 +767,7 @@ TEST_CASE("Text writer writes theory", "[text]") {
         output.str("");
         out.beginStep();
         out.theoryAtom(2, 0, {});
-        out.rule(Head_t::choice, (head = {4}), (body = {2}));
+        out.rule(HeadType::choice, (head = {4}), (body = {2}));
         REQUIRE_THROWS_AS(out.endStep(), std::logic_error);
     }
 }