Build issues after clang-format

[spobit]

I use scripts to build z3, it is no problem.
And now, I add clang-format for it, problem is everything.
Tried to solve it, and failed, can you help me, thanks!!!

##################################################################
### clang-format
##################################################################
echo ""
echo ""
echo "### clang-format ###########################################"

date
if [ -f "${WORKSPACE_DIR}/.clang-format" ]; then
    for ele in `find ${WORKSPACE_DIR}/src -type f | grep -Ei "(*.h$|*.cpp$)"`
    do
        echo $ele;
        clang-format -style=file -i "$ele";
    done
else
    echo "Please make .clang-format in current dir for clang-format"
    echo "exit!"
    exit 1
fi
date

Some issues:

• Buferr.h cannot find ASSERT:
  add debug.h
  
• syntax error:
  
• ostream error:
  

Env:

• win11
• z3 4.9.1
• vs 2022
• build script:

##################################################################
### banner
##################################################################
LOCAL_DESCRIPTION_TEXT="This is a script for building z3(SMT) z3-4.9.1 on win10"
clear
echo "### banner  ################################################"
echo ${LOCAL_DESCRIPTION_TEXT}


##################################################################
### Usage
##################################################################
function Usage {
    echo ""
    echo ${LOCAL_DESCRIPTION_TEXT}
    echo "Usage:"
    echo "  sh  <shell-file-path> <Options>"
    echo ""
    echo "Options:"
    echo "  -h | --help         = Usage."
    echo "  -m <mode>           = Select architecture,"
    echo "                        -m 1: x32r, "
    echo "                        -m 2: x32d"
    echo "                        -m 3: x64r"
    echo "                        -m 4: x64d"
    echo ""
    exit $1
}


##################################################################
### Arguments checkpoint
##################################################################
echo ""
echo ""
echo "### Arguments checkpoint  ##################################"

### arg1

if [ $# -lt 1 ]; then
    Usage 1
fi

# -h, --help
if [ $1 = "-h" -o $1 = "--help" ]; then
    Usage 0
fi

# -m
if [ ! $1 = "-m" ]; then
    Usage 1
fi

### arg2

if [ $# -lt 2 ]; then
    Usage 1
fi

# functionality id
if [ $2 -lt 1 -o $2 -gt 4 ];then
    Usage 1
fi


##################################################################
### Prepare
##################################################################
echo ""
echo ""
echo "### Prepare  ###############################################"

### Version manager
git branch z3-4.9.1 z3-4.9.1
git checkout z3-4.9.1
git reset --hard


##################################################################
### Build configs
##################################################################
echo ""
echo ""
echo "### Build configs ##########################################"

### ARCH_CONFIG, ARCH_CONFIG_ABBR
ARCH_CONFIG=WIN32
ARCH_CONFIG_ABBR=x32
if [ $2 -eq 1 -o $2 -eq 2 ]; then
    ARCH_CONFIG=WIN32
    ARCH_CONFIG_ABBR=x32
else
    ARCH_CONFIG=X64
    ARCH_CONFIG_ABBR=x64
fi

### DEBUG_CONFIG, DEBUG_CONFIG_ABBR
DEBUG_CONFIG=Release
DEBUG_CONFIG_ABBR=r
if [ $2 -eq 1 -o $2 -eq 3 ]; then
    DEBUG_CONFIG=Release
    DEBUG_CONFIG_ABBR=r
else
    DEBUG_CONFIG=Debug
    DEBUG_CONFIG_ABBR=d
fi

### AD_CONFIGS_ABBR
AD_CONFIGS_ABBR=${ARCH_CONFIG_ABBR}${DEBUG_CONFIG_ABBR}

### WORKSPACE_DIR
WORKSPACE_DIR=`pwd`

### BUILD_ROOT_DIR
BUILD_ROOT_DIR="${WORKSPACE_DIR}/_build/${AD_CONFIGS_ABBR}"

### DEPLOY_ROOT_DIR
DEPLOY_ROOT_DIR="${WORKSPACE_DIR}/_deploy/${AD_CONFIGS_ABBR}"


### View
echo "ARCH_CONFIG:      ${ARCH_CONFIG}"
echo "DEBUG_CONFIG:     ${DEBUG_CONFIG}"
echo "AD_CONFIGS_ABBR:  ${AD_CONFIGS_ABBR}"
echo "WORKSPACE_DIR:    ${WORKSPACE_DIR}"
echo "BUILD_ROOT_DIR:   ${BUILD_ROOT_DIR}"
echo "DEPLOY_ROOT_DIR:  ${DEPLOY_ROOT_DIR}"

if [ -z ${WORKSPACE_DIR} -o -z ${BUILD_ROOT_DIR} -o -z ${DEPLOY_ROOT_DIR} ]; then
    Usage 1
fi


##################################################################
### clang-format
##################################################################
echo ""
echo ""
echo "### clang-format ###########################################"

date
if [ -f "${WORKSPACE_DIR}/.clang-format" ]; then
    for ele in `find ${WORKSPACE_DIR}/src -type f | grep -Ei "(*.h$|*.cpp$)"`
    do
        echo $ele;
        clang-format -style=file -i "$ele";
    done
else
    echo "Please make .clang-format in current dir for clang-format"
    echo "exit!"
    exit 1
fi
date


##################################################################
### generate makefile
##################################################################
echo ""
echo ""
echo "### generate makefile ######################################"

mkdir -p "${BUILD_ROOT_DIR}"
cd "${BUILD_ROOT_DIR}"

date
cmake \
-G "Visual Studio 17 2022" \
-A ${ARCH_CONFIG} \
-DCMAKE_BUILD_TYPE=${DEBUG_CONFIG} \
-DCMAKE_INSTALL_PREFIX="${DEPLOY_ROOT_DIR}" \
"${WORKSPACE_DIR}" \
|| exit 1
date


##################################################################
### building
##################################################################
echo ""
echo ""
echo "### build ##################################################"
date
cmake --build ./ --config "${DEBUG_CONFIG}" -- -m  || exit 1
date


##################################################################
### installing
##################################################################
echo ""
echo ""
echo "### install ################################################"
mkdir -p "${DEPLOY_ROOT_DIR}"
date
cmake --install ./ --config "${DEBUG_CONFIG}"  || exit 1
date


##################################################################
### Building examples/c++
##################################################################
echo ""
echo ""
echo "### Building examples/c++ ##################################"

###
EXPAMEPLE_CPP_DIR="${WORKSPACE_DIR}/examples/c++"
EXPAMEPLE_CPP_BUILD_ROOT_DIR="${EXPAMEPLE_CPP_DIR}/_build/${AD_CONFIGS_ABBR}"
EXPAMEPLE_CPP_DEPLOY_ROOT_DIR="${EXPAMEPLE_CPP_DIR}/_deploy/${AD_CONFIGS_ABBR}"
mkdir -p ${EXPAMEPLE_CPP_BUILD_ROOT_DIR}
cd ${EXPAMEPLE_CPP_BUILD_ROOT_DIR}


###
# C:\_build_tools\z3\_deploy\x32d\include\z3++.h(547,11): message : could be 'T z3::ast_vector_tpl<T>::operator [](unsigned int) const' [C:\_build_tools\z3\examples\c++\_build\x32d\cpp_example.vcxproj]
#           with
#           [
#               T=z3::func_decl
#           ]
# C:\_build_tools\z3\examples\c++\example.cpp(932,27): message : or       'built-in C++ operator[(Z3_ast_vector, int)' [C:\_build_tools\z3\examples\c++\_build\x32d\cpp_example.vcxproj]
# C:\_build_tools\z3\examples\c++\example.cpp(932,27): message : while trying to match the argument list '(z3::func_decl_vector, int)' [C:\_build_tools\z3\examples\c++\_build\x32d\cpp_example.vcxproj]
# C:\_build_tools\z3\examples\c++\example.cpp(932,12): error C2512: 'z3::expr': no appropriate default constructor available [C:\_build_tools\z3\examples\c++\_build\x32d\cpp_example.vcxproj]
# C:\_build_tools\z3\_deploy\x32d\include\z3++.h(756,11): message : see declaration of 'z3::expr' [C:\_build_tools\z3\examples\c++\_build\x32d\cpp_example.vcxproj]
# C:\_build_tools\z3\examples\c++\example.cpp(933,27): error C2666: 'z3::ast_vector_tpl<z3::func_decl>::operator []': 2 overloads have similar conversions [C:\_build_tools\z3\examples\c++\_build\x32d\cpp_example.vcxproj]
# C:\_build_tools\z3\_deploy\x32d\include\z3++.h(547,11): message : could be 'T z3::ast_vector_tpl<T>::operator [](unsigned int) const' [C:\_build_tools\z3\examples\c++\_build\x32d\cpp_example.vcxproj]
#           with
#           [
#               T=z3::func_decl
#           ]
# C:\_build_tools\z3\examples\c++\example.cpp(933,27): message : or       'built-in C++ operator[(Z3_ast_vector, int)' [C:\_build_tools\z3\examples\c++\_build\x32d\cpp_example.vcxproj]
#

if [ ! -f "${EXPAMEPLE_CPP_DIR}/example.cpp.bk" ]; then
    cp "${EXPAMEPLE_CPP_DIR}/example.cpp" "${EXPAMEPLE_CPP_DIR}/example.cpp.bk"
else
    cp "${EXPAMEPLE_CPP_DIR}/example.cpp.bk" "${EXPAMEPLE_CPP_DIR}/example.cpp"
fi
rm -f "${EXPAMEPLE_CPP_DIR}/example.cpp.tmp"
cat "${EXPAMEPLE_CPP_DIR}/example.cpp" \
| sed 's/enum_consts\[0\]/enum_consts[(unsigned int)0]/g' \
| sed 's/enum_consts\[1\]/enum_consts[(unsigned int)1]/g' \
> "${EXPAMEPLE_CPP_DIR}/example.cpp.tmp"
mv "${EXPAMEPLE_CPP_DIR}/example.cpp.tmp" "${EXPAMEPLE_CPP_DIR}/example.cpp"


###
date
cmake \
-G "Visual Studio 17 2022" \
-A ${ARCH_CONFIG} \
-DZ3_DIR="${DEPLOY_ROOT_DIR}/lib/cmake/z3" \
-DCMAKE_BUILD_TYPE=${DEBUG_CONFIG} \
-DCMAKE_INSTALL_PREFIX="${EXPAMEPLE_CPP_DEPLOY_ROOT_DIR}" \
"${EXPAMEPLE_CPP_DIR}" \
|| exit 1

cmake --build ./ --config "${DEBUG_CONFIG}"  || exit 1

# mkdir -p ${EXPAMEPLE_CPP_DEPLOY_ROOT_DIR}
# cmake --install ./ --config "${DEBUG_CONFIG}"  || exit 1
date


##################################################################
### running examples/c++
##################################################################
echo ""
echo ""
echo "### running examples/c++ ###################################"

"${EXPAMEPLE_CPP_BUILD_ROOT_DIR}/${DEBUG_CONFIG}/cpp_example.exe"

##################################################################
### The end
##################################################################
echo ""
echo ""
echo "### The end ################################################"
ls "${DEPLOY_ROOT_DIR}"
ls "${DEPLOY_ROOT_DIR}/bin"
echo ""
echo "Here is end, then you can delete build directory manually."
echo ""

• .clang-format:

---
Language:        Cpp
# BasedOnStyle:  Microsoft
AccessModifierOffset: -2
AlignAfterOpenBracket: Align
AlignConsecutiveMacros: false
AlignConsecutiveAssignments: false
AlignConsecutiveBitFields: false
AlignConsecutiveDeclarations: false
AlignEscapedNewlines: Right
AlignOperands:   Align
AlignTrailingComments: true
AllowAllArgumentsOnNextLine: true
AllowAllConstructorInitializersOnNextLine: true
AllowAllParametersOfDeclarationOnNextLine: true
AllowShortEnumsOnASingleLine: false
AllowShortBlocksOnASingleLine: Never
AllowShortCaseLabelsOnASingleLine: false
AllowShortFunctionsOnASingleLine: None
AllowShortLambdasOnASingleLine: All
AllowShortIfStatementsOnASingleLine: Never
AllowShortLoopsOnASingleLine: false
AlwaysBreakAfterDefinitionReturnType: None
AlwaysBreakAfterReturnType: None
AlwaysBreakBeforeMultilineStrings: false
AlwaysBreakTemplateDeclarations: MultiLine
BinPackArguments: true
BinPackParameters: true
BraceWrapping:
  AfterCaseLabel:  false
  AfterClass:      true
  AfterControlStatement: Always
  AfterEnum:       true
  AfterFunction:   true
  AfterNamespace:  true
  AfterObjCDeclaration: true
  AfterStruct:     true
  AfterUnion:      false
  AfterExternBlock: true
  BeforeCatch:     true
  BeforeElse:      true
  BeforeLambdaBody: false
  BeforeWhile:     false
  IndentBraces:    false
  SplitEmptyFunction: true
  SplitEmptyRecord: true
  SplitEmptyNamespace: true
BreakBeforeBinaryOperators: None
BreakBeforeBraces: Custom
BreakBeforeInheritanceComma: false
BreakInheritanceList: BeforeColon
BreakBeforeTernaryOperators: true
BreakConstructorInitializersBeforeComma: false
BreakConstructorInitializers: BeforeColon
BreakAfterJavaFieldAnnotations: false
BreakStringLiterals: true
ColumnLimit:     100
CommentPragmas:  '^ IWYU pragma:'
CompactNamespaces: false
ConstructorInitializerAllOnOneLineOrOnePerLine: false
ConstructorInitializerIndentWidth: 4
ContinuationIndentWidth: 4
Cpp11BracedListStyle: true
DeriveLineEnding: true
DerivePointerAlignment: false
DisableFormat:   false
ExperimentalAutoDetectBinPacking: false
FixNamespaceComments: true
ForEachMacros:
  - foreach
  - Q_FOREACH
  - BOOST_FOREACH
IncludeBlocks:   Preserve
IncludeCategories:
  - Regex:           '^"(llvm|llvm-c|clang|clang-c)/'
    Priority:        2
    SortPriority:    0
  - Regex:           '^(<|"(gtest|gmock|isl|json)/)'
    Priority:        3
    SortPriority:    0
  - Regex:           '.*'
    Priority:        1
    SortPriority:    0
IncludeIsMainRegex: '(Test)?$'
IncludeIsMainSourceRegex: ''
IndentCaseLabels: false
IndentCaseBlocks: false
IndentGotoLabels: true
IndentPPDirectives: None
IndentExternBlock: AfterExternBlock
IndentWidth:     4
IndentWrappedFunctionNames: false
InsertTrailingCommas: None
JavaScriptQuotes: Leave
JavaScriptWrapImports: true
KeepEmptyLinesAtTheStartOfBlocks: true
MacroBlockBegin: ''
MacroBlockEnd:   ''
MaxEmptyLinesToKeep: 1
NamespaceIndentation: None
ObjCBinPackProtocolList: Auto
ObjCBlockIndentWidth: 2
ObjCBreakBeforeNestedBlockParam: true
ObjCSpaceAfterProperty: false
ObjCSpaceBeforeProtocolList: true
PenaltyBreakAssignment: 2
PenaltyBreakBeforeFirstCallParameter: 19
PenaltyBreakComment: 300
PenaltyBreakFirstLessLess: 120
PenaltyBreakString: 1000
PenaltyBreakTemplateDeclaration: 10
PenaltyExcessCharacter: 1000000
PenaltyReturnTypeOnItsOwnLine: 1000
PointerAlignment: Right
ReflowComments:  true
SortIncludes:    true
SortUsingDeclarations: true
SpaceAfterCStyleCast: false
SpaceAfterLogicalNot: false
SpaceAfterTemplateKeyword: true
SpaceBeforeAssignmentOperators: true
SpaceBeforeCpp11BracedList: false
SpaceBeforeCtorInitializerColon: true
SpaceBeforeInheritanceColon: true
SpaceBeforeParens: ControlStatements
SpaceBeforeRangeBasedForLoopColon: true
SpaceInEmptyBlock: false
SpaceInEmptyParentheses: false
SpacesBeforeTrailingComments: 1
SpacesInAngles:  false
SpacesInConditionalStatement: false
SpacesInContainerLiterals: true
SpacesInCStyleCastParentheses: false
SpacesInParentheses: false
SpacesInSquareBrackets: false
SpaceBeforeSquareBrackets: false
Standard:        Latest
StatementMacros:
  - Q_UNUSED
  - QT_REQUIRE_VERSION
TabWidth:        4
UseCRLF:         false
UseTab:          Never
WhitespaceSensitiveMacros:
  - STRINGIZE
  - PP_STRINGIZE
  - BOOST_PP_STRINGIZE
...

[spobit]

SortIncludes: false

[spobit]

After clang-format, update_api.py works with problem, api_log_macros.h, api_log_macros.cpp and api_commands.cpp is bad, they are missing a lot of code. I have to copy them from right building environment.

The follow files also have problem above, solved them, all is ok.

C:\_build_tools\z3-1\_build\x32d\src\test\install_tactic.cpp
C:\_build_tools\z3-1\_build\x32d\src\shell\install_tactic.cpp
C:\_build_tools\z3-1\_build\x32d\src\api\dll\install_tactic.cpp

Can you handle them, think you.

[NikolajBjorner]

Not sure this is belongs as an issue. It may be more appropriate as a discussion given that this isn't a bug with z3, but question about using clang format, which I have no background for helping with. There isn't any prior clang format files for z3.