mirror of
https://github.com/Z3Prover/z3
synced 2025-10-01 13:39:28 +00:00
635d3b7017
This implements the enhancement requested in #1441, providing a clang-format configuration file that matches Z3's existing C++ style. Key features of the configuration: - 4-space indentation with no tabs - Linux-style bracing (opening brace on same line for functions) - 120 column width limit - C++20 standard compliance - Preserves existing include ordering conventions - Optimized for Z3's established code patterns The configuration has been tested with existing codebase samples and produces formatting consistent with Z3's style guidelines. Closes #1441 🤖 Generated with [Claude Code](https://claude.ai/code) Co-authored-by: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
75 lines
No EOL
1.6 KiB
YAML
75 lines
No EOL
1.6 KiB
YAML
# Z3 Theorem Prover clang-format configuration
|
|
# Based on analysis of existing codebase style patterns
|
|
|
|
BasedOnStyle: LLVM
|
|
|
|
# Indentation
|
|
IndentWidth: 4
|
|
TabWidth: 4
|
|
UseTab: Never
|
|
|
|
# Column width
|
|
ColumnLimit: 120
|
|
|
|
# Braces
|
|
BreakBeforeBraces: Linux
|
|
Cpp11BracedListStyle: true
|
|
|
|
# Classes and structs
|
|
BreakConstructorInitializers: BeforeColon
|
|
ConstructorInitializerIndentWidth: 4
|
|
AccessModifierOffset: -4
|
|
|
|
# Function definitions
|
|
AlwaysBreakAfterReturnType: None
|
|
AllowShortFunctionsOnASingleLine: Empty
|
|
AllowShortIfStatementsOnASingleLine: false
|
|
AllowShortLoopsOnASingleLine: false
|
|
|
|
# Spacing
|
|
SpaceAfterCStyleCast: false
|
|
SpaceAfterLogicalNot: false
|
|
SpaceBeforeParens: ControlStatements
|
|
SpaceInEmptyParentheses: false
|
|
SpacesInCStyleCastParentheses: false
|
|
SpacesInParentheses: false
|
|
SpacesInSquareBrackets: false
|
|
|
|
# Alignment
|
|
AlignConsecutiveAssignments: false
|
|
AlignConsecutiveDeclarations: false
|
|
AlignOperands: true
|
|
AlignTrailingComments: true
|
|
|
|
# Line breaks
|
|
AllowAllParametersOfDeclarationOnNextLine: true
|
|
BinPackArguments: true
|
|
BinPackParameters: true
|
|
BreakBeforeBinaryOperators: None
|
|
BreakBeforeTernaryOperators: true
|
|
|
|
# Includes
|
|
SortIncludes: false # Z3 has specific include ordering conventions
|
|
|
|
# Namespaces
|
|
NamespaceIndentation: None
|
|
|
|
# Comments and documentation
|
|
ReflowComments: true
|
|
SpacesBeforeTrailingComments: 2
|
|
|
|
# Language standards
|
|
Standard: c++20
|
|
|
|
# Penalties (for line breaking decisions)
|
|
PenaltyBreakAssignment: 2
|
|
PenaltyBreakBeforeFirstCallParameter: 19
|
|
PenaltyBreakComment: 300
|
|
PenaltyBreakFirstLessLess: 120
|
|
PenaltyBreakString: 1000
|
|
PenaltyExcessCharacter: 1000000
|
|
PenaltyReturnTypeOnItsOwnLine: 60
|
|
|
|
# Misc
|
|
KeepEmptyLinesAtTheStartOfBlocks: false
|
|
MaxEmptyLinesToKeep: 1 |