From be174cef87727c324e3c39fc23afc1018365ce3f Mon Sep 17 00:00:00 2001
From: Daily Backlog Burner <github-actions[bot]@users.noreply.github.com>
Date: Wed, 17 Sep 2025 01:32:57 +0000
Subject: [PATCH] Add .clang-format file for consistent C++ code formatting

This addresses issue #1441 by providing a comprehensive clang-format
configuration that matches Z3's existing C++ coding style patterns.

Key features:
- 4-space indentation consistent with existing Z3 code
- Preserves existing include organization (no auto-sorting)
- Left-aligned pointers/references (type* var style)
- Attach brace style for control statements
- 120 character line limit
- Proper spacing and alignment rules

Usage:
  clang-format --sort-includes=false -i <file>     # Format file in-place
  git clang-format --style=file                    # Format staged changes

Based on analysis of existing Z3 source code patterns in:
- src/ast/*.cpp and src/ast/*.h files
- src/api/*.cpp and src/api/*.h files
- src/smt/*.cpp files
- Various utility and core library files

Resolves #1441
---
 .clang-format | 108 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 108 insertions(+)
 create mode 100644 .clang-format

diff --git a/.clang-format b/.clang-format
new file mode 100644
index 000000000..4eaa6626e
--- /dev/null
+++ b/.clang-format
@@ -0,0 +1,108 @@
+# Z3 C++ Code Style Configuration for clang-format
+# Based on analysis of existing Z3 source code patterns
+#
+# Usage:
+#   clang-format --sort-includes=false -i <file>     # Format file in-place
+#   git clang-format --style=file                    # Format staged changes
+#
+# References:
+# - https://clang.llvm.org/docs/ClangFormatStyleOptions.html
+# - Issue #1441: https://github.com/Z3Prover/z3/issues/1441
+
+BasedOnStyle: LLVM
+
+# Indentation - Z3 uses 4-space indentation
+IndentWidth: 4
+TabWidth: 4
+UseTab: Never
+ContinuationIndentWidth: 4
+ConstructorInitializerIndentWidth: 4
+AccessModifierOffset: -4
+IndentCaseLabels: false
+
+# Line length and wrapping
+ColumnLimit: 120
+ReflowComments: true
+
+# Brace wrapping - Z3 uses mixed style
+BreakBeforeBraces: Attach  # Braces attach to control statements, but classes/functions on new line
+
+# Spacing around pointers and references - Z3 uses "type* var" style
+PointerAlignment: Left
+ReferenceAlignment: Left
+SpaceAfterCStyleCast: false
+SpaceBeforeAssignmentOperators: true
+SpaceBeforeParens: ControlStatements
+SpaceInEmptyParentheses: false
+SpacesBeforeTrailingComments: 1
+SpacesInAngles: false
+SpacesInContainerLiterals: false
+SpacesInCStyleCastParentheses: false
+SpacesInParentheses: false
+SpacesInSquareBrackets: false
+
+# Function and method formatting
+AlwaysBreakAfterReturnType: None
+AlwaysBreakBeforeMultilineStrings: false
+BinPackArguments: true
+BinPackParameters: true
+
+# Constructor and class formatting
+BreakConstructorInitializers: BeforeComma
+ConstructorInitializerAllOnOneLineOrOnePerLine: false
+Cpp11BracedListStyle: true
+
+# Template formatting
+SpaceAfterTemplateKeyword: true
+
+# Include sorting - preserve Z3's existing organization
+SortIncludes: Never
+IncludeBlocks: Preserve
+
+# Statement formatting
+AllowShortBlocksOnASingleLine: Empty
+AllowShortCaseLabelsOnASingleLine: false
+AllowShortFunctionsOnASingleLine: Inline
+AllowShortIfStatementsOnASingleLine: Never
+AllowShortLoopsOnASingleLine: false
+
+# Break formatting
+BreakBeforeBinaryOperators: None
+BreakBeforeTernaryOperators: true
+BreakStringLiterals: true
+CompactNamespaces: false
+
+# Comment formatting
+CommentPragmas: '^(IWYU pragma:|NOLINT)'
+DisableFormat: false
+
+# Penalty settings for line breaking decisions
+PenaltyBreakAssignment: 2
+PenaltyBreakBeforeFirstCallParameter: 19
+PenaltyBreakComment: 300
+PenaltyBreakFirstLessLess: 120
+PenaltyBreakString: 1000
+PenaltyExcessCharacter: 1000000
+PenaltyReturnTypeOnItsOwnLine: 60
+
+# Namespace formatting
+NamespaceIndentation: None
+FixNamespaceComments: false
+
+# Language standard
+Standard: Cpp11
+
+# Keep empty lines
+KeepEmptyLinesAtTheStartOfBlocks: true
+MaxEmptyLinesToKeep: 2
+
+# Alignment
+AlignAfterOpenBracket: Align
+AlignConsecutiveAssignments: false
+AlignConsecutiveDeclarations: false
+AlignEscapedNewlines: Left
+AlignOperands: true
+AlignTrailingComments: false
+
+# Preprocessor formatting
+IndentPPDirectives: None
\ No newline at end of file