Description
Describe the bug
Not a bug but a source for potential performance optimization. I have attached two sets of assertions that are exactly the same except for an additional assertion in symcc-assertions-11-extra-assertion.smt2 on line 227. This assertion is of the form: not (contains (substr S 0 (indexOf S "x" 0)) "x").
This assertion should always be true, unless I've overlooked some corner case.
Adding this assertion reduces the solve time from ~1 minute to ~25 seconds, so there may be potential for optimization.
symcc-assertions-11.smt2.txt
symcc-assertions-11-extra-assertion.smt2.txt
Note: If the bug is triggered with an SMT2 input file please minimize it with ddsmt.
Command line arguments:
cvc5 version/commit: This is cvc5 version 1.1.3-dev.441.2d09b3c91 [git 2d09b3c on branch main with local modifications]
Operating system: Ubuntu 22.04.4 LTS
configure.sh options
#!/usr/bin/env bash
#--------------------------------------------------------------------------#
set -e -o pipefail
usage () {
cat <<EOF
Usage: $0 [] [ ...]
Build types:
production
debug
testing
competition
competition-inc
General options;
-h, --help display this help and exit
--prefix=STR install directory
--program-prefix=STR prefix of binaries prepended on make install
--name=STR use custom build directory name (optionally: +path)
--best turn on dependencies and options known to give best performance
--gpl permit GPL dependencies, if available
--arm64 cross-compile for Linux ARM 64 bit
--win64 cross-compile for Windows 64 bit
--win64-native natively compile for Windows 64 bit
--ninja use Ninja build system
--docs build Api documentation
Features:
The following flags enable optional features (disable with --no-).
--static build static libraries and binaries [default=no]
--static-binary link against static system libraries
--auto-download automatically download dependencies if necessary
--debug-symbols include debug symbols
--valgrind Valgrind instrumentation
--debug-context-mm use the debug context memory manager
--statistics include statistics
--assertions turn on assertions
--tracing include tracing code
--muzzle complete silence (no non-result output)
--coverage support for gcov coverage testing
--profiling support for gprof profiling
--unit-testing support for unit testing
--python-bindings build Python bindings based on new C++ API
--python-only-src create only Python bindings source files
--java-bindings build Java bindings based on new C++ API
--all-bindings build bindings for all supported languages
--asan build with ASan instrumentation
--ubsan build with UBSan instrumentation
--tsan build with TSan instrumentation
--werror build with -Werror
--ipo build with interprocedural optimization
Optional Packages:
The following flags enable optional packages (disable with --no-).
--cln use CLN instead of GMP
--glpk use GLPK simplex solver
--cryptominisat use the CryptoMiniSat SAT solver
--kissat use the Kissat SAT solver
--poly use the LibPoly library [default=yes]
--cocoa use the CoCoA library
--editline support the editline library
Optional Path to Optional Packages:
--glpk-dir=PATH path to top level of GLPK installation
--dep-path=PATH path to a dependency installation dir
--pythonic-path=PATH path to the Pythonic API's repository
CMake Options (Advanced)
-DVAR=VALUE manually add CMake options
Wasm Options
--wasm=VALUE set compilation extension for WebAssembly <WASM, JS or HTML>
--wasm-flags='STR' Emscripten flags used in the WebAssembly binary compilation
EOF
exit 0
}
#--------------------------------------------------------------------------#
die () {
echo "*** configure.sh: $*" 1>&2
exit 1
}
msg () {
echo "[configure.sh] $*"
}
#--------------------------------------------------------------------------#
[ ! -e src/theory ] && die "$0 not called from cvc5 base directory"
#--------------------------------------------------------------------------#
build_dir=build
install_prefix=default
program_prefix=""
#--------------------------------------------------------------------------#
buildtype=default
asan=default
assertions=default
auto_download=default
cln=default
comp_inc=default
coverage=default
cryptominisat=default
debug_context_mm=default
debug_symbols=default
docs=default
glpk=default
gpl=default
kissat=default
poly=ON
cocoa=default
muzzle=default
ninja=default
profiling=default
python_bindings=default
python_only_src=default
pyvenv=default
java_bindings=default
editline=default
build_shared=ON
static_binary=default
statistics=default
tracing=default
tsan=default
ubsan=default
unit_testing=default
valgrind=default
win64=default
win64_native=default
arm64=default
werror=default
ipo=default
glpk_dir=default
wasm=default
wasm_flags=""
#--------------------------------------------------------------------------#
uname_output=$(uname)
if [[ $uname_output =~ ^MSYS || $uname_output =~ ^MINGW ]]; then
win64_native=ON
fi
cmake_opts=""
Set python3 interpreter executable to make sure that CMake picks up the
correct Python version.
if command -v python3 &> /dev/null; then
cmake_opts="$cmake_opts -DPython_EXECUTABLE=$(command -v python3)"
fi
while [ $# -gt 0 ]
do
case $1 in
-h|--help) usage;;
--asan) asan=ON;;
--no-asan) asan=OFF;;
--ubsan) ubsan=ON;;
--no-ubsan) ubsan=OFF;;
--tsan) tsan=ON;;
--no-tsan) tsan=OFF;;
--werror) werror=ON;;
--ipo) ipo=ON;;
--no-ipo) ipo=OFF;;
93B3
--assertions) assertions=ON;;
--no-assertions) assertions=OFF;;
# Best configuration
--best)
cln=ON
cryptominisat=ON
editline=ON
glpk=ON
ipo=ON
;;
--prefix) die "missing argument to $1 (try -h)" ;;
--prefix=*)
install_prefix=${1##*=}
# Check if install_prefix is an absolute path and if not, make it
# absolute.
case $install_prefix in
/*) ;; # absolute path
*) install_prefix=$(pwd)/$install_prefix ;; # make absolute path
esac
;;
--program-prefix) die "missing argument to $1 (try -h)" ;;
--program-prefix=*) program_prefix=${1##*=} ;;
--name) die "missing argument to $1 (try -h)" ;;
--name=*) build_dir=${1##*=} ;;
--cln) cln=ON;;
--no-cln) cln=OFF;;
--coverage) coverage=ON;;
--no-coverage) coverage=OFF;;
--cryptominisat) cryptominisat=ON;;
--no-cryptominisat) cryptominisat=OFF;;
--debug-symbols) debug_symbols=ON;;
--no-debug-symbols) debug_symbols=OFF;;
--debug-context-mm) debug_context_mm=ON;;
--no-debug-context-mm) debug_context_mm=OFF;;
--gpl) gpl=ON;;
--no-gpl) gpl=OFF;;
--kissat) kissat=ON;;
--no-kissat) kissat=OFF;;
--win64) win64=ON;;
--win64-native) win64_native=ON;;
--arm64) arm64=ON;;
--ninja) ninja=ON;;
--docs) docs=ON;;
--no-docs) docs=OFF;;
--glpk) glpk=ON;;
--no-glpk) glpk=OFF;;
--poly) poly=ON;;
--no-poly) poly=OFF;;
--cocoa) cocoa=ON;;
--no-cocoa) cocoa=OFF;;
--muzzle) muzzle=ON;;
--no-muzzle) muzzle=OFF;;
--static) build_shared=OFF;;
--no-static) build_shared=ON;;
--static-binary) static_binary=ON;;
--no-static-binary) static_binary=OFF;;
--auto-download) auto_download=ON;;
--no-auto-download) auto_download=OFF;;
--pyvenv) pyvenv=ON;;
--no-pyvenv) pyvenv=OFF;;
--statistics) statistics=ON;;
--no-statistics) statistics=OFF;;
--tracing) tracing=ON;;
--no-tracing) tracing=OFF;;
--unit-testing) unit_testing=ON;;
--no-unit-testing) unit_testing=OFF;;
--python-bindings) python_bindings=ON;;
--no-python-bindings) python_bindings=OFF;;
--python-only-src) python_only_src=ON;;
--no-python-only-src) python_only_src=OFF;;
--java-bindings) java_bindings=ON;;
--no-java-bindings) java_bindings=OFF;;
--all-bindings)
python_bindings=ON
java_bindings=ON;;
--valgrind) valgrind=ON;;
--no-valgrind) valgrind=OFF;;
--profiling) profiling=ON;;
--no-profiling) profiling=OFF;;
--editline) editline=ON;;
--no-editline) editline=OFF;;
--glpk-dir) die "missing argument to $1 (try -h)" ;;
--glpk-dir=*) glpk_dir=${1##*=} ;;
--dep-path) die "missing argument to $1 (try -h)" ;;
--dep-path=*) dep_path="${dep_path};${1##*=}" ;;
--pythonic-path) die "missing argument to $1 (try -h)" ;;
--pythonic-path=*)
pythonic_path="${1##*=}"
# Check if pythonic is an absolute path and if not, make it
# absolute.
case $pythonic_path in
/*) ;; # absolute path
*) pythonic_path=$(pwd)/$pythonic_path ;; # make absolute path
esac
;;
--wasm) wasm=WASM ;;
--wasm=*) wasm="${1##*=}" ;;
--wasm-flags) die "missing argument to $1 (try -h)" ;;
--wasm-flags=*) wasm_flags="${1#*=}" ;;
-D*) cmake_opts="${cmake_opts} $1" ;;
-*) die "invalid option '$1' (try -h)";;
*) case $1 in
production) buildtype=Production;;
debug) buildtype=Debug;;
testing) buildtype=Testing;;
competition) buildtype=Competition;;
competition-inc) buildtype=Competition; comp_inc=ON;;
*) die "invalid build type (try -h)";;
esac
;;
esac
shift
done
#--------------------------------------------------------------------------#
if [ $werror != default ]; then
export CFLAGS=-Werror
export CXXFLAGS=-Werror
fi
[ $buildtype != default ]
&& cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$buildtype"
[ $asan != default ]
&& cmake_opts="$cmake_opts -DENABLE_ASAN=$asan"
[ $auto_download != default ]
&& cmake_opts="$cmake_opts -DENABLE_AUTO_DOWNLOAD=$auto_download"
[ $pyvenv != default ]
&& cmake_opts="$cmake_opts -DUSE_PYTHON_VENV=$pyvenv"
[ $ubsan != default ]
&& cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan"
[ $tsan != default ]
&& cmake_opts="$cmake_opts -DENABLE_TSAN=$tsan"
[ $ipo != default ]
&& cmake_opts="$cmake_opts -DENABLE_IPO=$ipo"
[ $assertions != default ]
&& cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
[ $comp_inc != default ]
&& cmake_opts="$cmake_opts -DENABLE_COMP_INC_TRACK=$comp_inc"
[ $coverage != default ]
&& cmake_opts="$cmake_opts -DENABLE_COVERAGE=$coverage"
[ $debug_symbols != default ]
&& cmake_opts="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols"
[ $debug_context_mm != default ]
&& cmake_opts="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm"
[ $gpl != default ]
&& cmake_opts="$cmake_opts -DENABLE_GPL=$gpl"
[ $win64 != default ]
&& cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake"
Because 'MSYS Makefiles' has a space in it, we set the variable vs. adding to 'cmake_opts'
[ $win64_native != default ]
&& [ $ninja == default ] && export CMAKE_GENERATOR="MSYS Makefiles"
[ $arm64 != default ]
&& cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake"
[ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
[ $muzzle != default ]
&& cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
[ $build_shared != default ]
&& cmake_opts="$cmake_opts -DBUILD_SHARED_LIBS=$build_shared"
[ $static_binary != default ]
&& cmake_opts="$cmake_opts -DSTATIC_BINARY=$static_binary"
[ $statistics != default ]
&& cmake_opts="$cmake_opts -DENABLE_STATISTICS=$statistics"
[ $tracing != default ]
&& cmake_opts="$cmake_opts -DENABLE_TRACING=$tracing"
[ $unit_testing != default ]
&& cmake_opts="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing"
[ $docs != default ]
&& cmake_opts="$cmake_opts -DBUILD_DOCS=$docs"
[ $python_bindings != default ]
&& cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings"
[ $python_only_src != default ]
&& cmake_opts="$cmake_opts -DONLY_PYTHON_EXT_SRC=$python_only_src"
[ $java_bindings != default ]
&& cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$java_bindings"
[ $valgrind != default ]
&& cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind"
[ $profiling != default ]
&& cmake_opts="$cmake_opts -DENABLE_PROFILING=$profiling"
[ $editline != default ]
&& cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline"
[ $cln != default ]
&& cmake_opts="$cmake_opts -DUSE_CLN=$cln"
[ $cryptominisat != default ]
&& cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
[ $glpk != default ]
&& cmake_opts="$cmake_opts -DUSE_GLPK=$glpk"
[ $kissat != default ]
&& cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
[ $poly != default ]
&& cmake_opts="$cmake_opts -DUSE_POLY=$poly"
[ $cocoa != default ]
&& cmake_opts="$cmake_opts -DUSE_COCOA=$cocoa"
[ "$glpk_dir" != default ]
&& cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
[ "$dep_path" != default ]
&& cmake_opts="$cmake_opts -DCMAKE_PREFIX_PATH=$dep_path"
[ "$pythonic_path" != default ]
&& cmake_opts="$cmake_opts -DPYTHONIC_PATH=$pythonic_path"
[ "$install_prefix" != default ]
&& cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
[ -n "$program_prefix" ]
&& cmake_opts="$cmake_opts -DPROGRAM_PREFIX=$program_prefix"
[ "$wasm" != default ]
&& cmake_opts="$cmake_opts -DWASM=$wasm"
root_dir=$(pwd)
cmake_wrapper=
cmake_opts=($cmake_opts)
if [ "$wasm" == "WASM" ] || [ "$wasm" == "JS" ] || [ "$wasm" == "HTML" ] ; then
cmake_wrapper=emcmake
cmake_opts=(${cmake_opts[@]} -DWASM_FLAGS="${wasm_flags}")
fi
The cmake toolchain can't be changed once it is configured in $build_dir.
Thus, remove $build_dir and create an empty directory.
[ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
[ $arm64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
mkdir -p "$build_dir"
cd "$build_dir"
[ -e CMakeCache.txt ] && rm CMakeCache.txt
build_dir_escaped=$(echo "$build_dir" | sed 's///\//g')
$cmake_wrapper cmake "$root_dir" "${cmake_opts[@]}" 2>&1 |
sed "s/^Now just/Now change to '$build_dir_escaped' and/"
configure.sh output
-- The C compiler identification is GNU 11.4.0
-- The CXX compiler identification is GNU 11.4.0
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found Git: /usr/bin/git (found version "2.34.1")
-- Building Production build
-- Performing Test HAVE_C_FLAG_O3
-- Performing Test HAVE_C_FLAG_O3 - Success
-- Configuring with C flag '-O3'
-- Performing Test HAVE_CXX_FLAG_O3
-- Performing Test HAVE_CXX_FLAG_O3 - Success
-- Configuring with CXX flag '-O3'
-- Performing Test HAVE_C_FLAG_Wall
-- Performing Test HAVE_C_FLAG_Wall - Success
-- Configuring with C flag '-Wall'
-- Performing Test HAVE_CXX_FLAG_Wall
-- Performing Test HAVE_CXX_FLAG_Wall - Success
-- Configuring with CXX flag '-Wall'
-- Performing Test HAVE_C_FLAG_Wunused_private_field
-- Performing Test HAVE_C_FLAG_Wunused_private_field - Failed
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field
-- Performing Test HAVE_CXX_FLAG_Wunused_private_field - Failed
-- Performing Test HAVE_C_FLAG_Wdangling_reference
-- Performing Test HAVE_C_FLAG_Wdangling_reference - Failed
-- Performing Test HAVE_CXX_FLAG_Wdangling_reference
-- Performing Test HAVE_CXX_FLAG_Wdangling_reference - Failed
-- Performing Test HAVE_C_FLAG_fexceptions
-- Performing Test HAVE_C_FLAG_fexceptions - Success
-- Configuring with C flag '-fexceptions'
-- Performing Test HAVE_CXX_FLAG_Wsuggest_override
-- Performing Test HAVE_CXX_FLAG_Wsuggest_override - Success
-- Configuring with CXX flag '-Wsuggest-override'
-- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor
-- Performing Test HAVE_CXX_FLAG_Wnon_virtual_dtor - Success
-- Configuring with CXX flag '-Wnon-virtual-dtor'
-- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough
-- Performing Test HAVE_C_FLAG_Wimplicit_fallthrough - Success
-- Configuring with C flag '-Wimplicit-fallthrough'
-- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough
-- Performing Test HAVE_CXX_FLAG_Wimplicit_fallthrough - Success
-- Configuring with CXX flag '-Wimplicit-fallthrough'
-- Performing Test HAVE_C_FLAG_Wshadow
-- Performing Test HAVE_C_FLAG_Wshadow - Success
-- Configuring with C flag '-Wshadow'
-- Performing Test HAVE_CXX_FLAG_Wshadow
-- Performing Test HAVE_CXX_FLAG_Wshadow - Success
-- Configuring with CXX flag '-Wshadow'
-- Performing Test HAVE_C_FLAG_fno_operator_names
-- Performing Test HAVE_C_FLAG_fno_operator_names - Failed
-- Performing Test HAVE_CXX_FLAG_fno_operator_names
-- Performing Test HAVE_CXX_FLAG_fno_operator_names - Success
-- Configuring with CXX flag '-fno-operator-names'
-- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init
-- Performing Test HAVE_CXX_FLAG_fno_extern_tls_init - Success
-- Configuring with CXX flag '-fno-extern-tls-init'
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess
-- Performing Test HAVE_CXX_FLAG_Wclass_memaccess - Success
-- Configuring with CXX flag '-Wno-class-memaccess'
-- Using GNU gold linker.
-- Disabling unit tests since assertions are disabled.
-- Found Python: /usr/bin/python3 (found version "3.10.12") found components: Interpreter
-- Found GMP 6.2.1: /usr/lib/x86_64-linux-gnu/libgmp.so
-- Looking for getc_unlocked
-- Looking for getc_unlocked - not found
-- Building CaDiCaL rel-1.7.4: /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build/deps/lib/libcadical.a
-- Building Poly 0.1.13: /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build/deps/lib/libpoly.so, /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build/deps/lib/libpolyxx.so
-- Building SymFPU: /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build/deps/include/
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS
-- Performing Test CVC5_NEED_INT64_T_OVERLOADS - Failed
-- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD
-- Performing Test CVC5_NEED_HASH_UINT64_T_OVERLOAD - Failed
-- Looking for unistd.h
-- Looking for unistd.h - found
-- Looking for sys/wait.h
-- Looking for sys/wait.h - found
-- Looking for C++ include ext/stdio_filebuf.h
-- Looking for C++ include ext/stdio_filebuf.h - found
-- Looking for clock_gettime
-- Looking for clock_gettime - found
-- Looking for ffs
-- Looking for ffs - found
-- Looking for optreset
-- Looking for optreset - not found
-- Looking for sigaltstack
-- Looking for sigaltstack - found
-- Looking for strerror_r
-- Looking for strerror_r - found
-- Looking for strtok_r
-- Looking for strtok_r - found
-- Looking for setitimer
-- Looking for setitimer - found
-- Performing Test STRERROR_R_CHAR_P
-- Performing Test STRERROR_R_CHAR_P - Failed
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_VISIBILITY - Success
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY
-- Performing Test COMPILER_HAS_HIDDEN_INLINE_VISIBILITY - Success
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR
-- Performing Test COMPILER_HAS_DEPRECATED_ATTR - Success
cvc5 1.1.3-dev
Build profile : production
Assertions : off
Debug symbols : off
Debug context mem mgr : off
Muzzle : off
Statistics : on
Tracing : off
ASan : off
UBSan : off
TSan : off
Coverage (gcov) : off
Profiling (gprof) : off
Unit tests : off
Valgrind : off
Shared build : on
Python bindings : off
Java bindings : off
Interprocedural opt. : off
CryptoMiniSat : off
GLPK : off
Kissat : off
LibPoly : on (local)
CoCoALib : off
MP library : gmp (system)
Editline : off
Api docs : off
CPPLAGS (-D...): NDEBUG CVC5_STATISTICS_ON CVC5_USE_POLY
CXXFLAGS : -O3 -Wall -Wsuggest-override -Wnon-virtual-dtor -Wimplicit-fallthrough -Wshadow -fno-operator-names -fno-extern-tls-init -Wno-class-memaccess
CFLAGS : -O3 -Wall -fexceptions -Wimplicit-fallthrough -Wshadow
Linker flags : -fuse-ld=gold
Install prefix : /usr/local
cvc5 license: modified BSD
Note that this configuration is NOT built against any GPL'ed libraries, so
it is covered by the (modified) BSD license. To build against GPL'ed
libraries which can improve cvc5's performance on arithmetic and bit-vector
logics, use the 'configure.sh' script to re-configure with '--best --gpl'.
Now change to 'build' and type 'make', followed by 'make check' or 'make install'.
-- Configuring done
-- Generating done
-- Build files have been written to: /home/rachel/programming/SymEx-Project/symcc/runtime/simple_backend/smt-switch/deps/cvc5/build