------------------------------------------------------------------------------- -- Phase: Environment ------------------------------------------------------------------------------- NO_DEPENDS=1 UNAME_r=6.5 UNAME_m=x86_64 UNAME_p=x86_64 UNAME_v=unknown UNAME_s=DragonFly PATH=/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin SSL_NO_VERIFY_PEER=1 LANG=C HOME=/root USER=root TERM=dumb SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: showconfig ------------------------------------------------------------------------------- ===> The following configuration options are available for cvc4-1.7_6: CRYPTOMINISAT=on: Use CryptoMiniSat as the SAT solver JAVA=on: Java platform support PYTHON=on: Python bindings or support READLINE=on: Command line editing via libreadline ====> Options available for the radio NUMLIB: you can only select none or one of them GMP=on: Use GMP numeric library CLN=off: Use CLN numeric library (disables portfolio mode) ===> Use 'make config' to modify these settings SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: CONFIGURE_ENV ------------------------------------------------------------------------------- PKG_CONFIG=pkgconf PYTHON="/usr/local/bin/python3.9" XDG_DATA_HOME=/construction/math/cvc4 XDG_CONFIG_HOME=/construction/math/cvc4 XDG_CACHE_HOME=/construction/math/cvc4/.cache HOME=/construction/math/cvc4 TMPDIR="/tmp" PATH=/construction/math/cvc4/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin PKG_CONFIG_LIBDIR=/construction/math/cvc4/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig SHELL=/bin/sh CONFIG_SHELL=/bin/sh CCVER=gcc80 SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: CONFIGURE_ARGS ------------------------------------------------------------------------------- SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: MAKE_ENV ------------------------------------------------------------------------------- XDG_DATA_HOME=/construction/math/cvc4 XDG_CONFIG_HOME=/construction/math/cvc4 XDG_CACHE_HOME=/construction/math/cvc4/.cache HOME=/construction/math/cvc4 TMPDIR="/tmp" PATH=/construction/math/cvc4/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin PKG_CONFIG_LIBDIR=/construction/math/cvc4/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig NO_PIE=yes MK_DEBUG_FILES=no MK_KERNEL_SYMBOLS=no SHELL=/bin/sh NO_LINT=YES CCVER=gcc80 PREFIX=/usr/local LOCALBASE=/usr/local NOPROFILE=1 CC="cc" CFLAGS="-pipe -I/usr/local/include -I/usr/local/include/ncurses -O2 -fno-strict-aliasing " CPP="cpp" CPPFLAGS="-I/usr/local/include" LDFLAGS=" -L/usr/local/lib -Wl,-rpath=/usr/local/lib -L/usr/local/lib " LIBS="" CXX="c++" CXXFLAGS=" -pipe -I/usr/local/include -I/usr/local/include/ncurses -O2 -fno-strict-aliasing " MANPREFIX="/usr/local" BSD_INSTALL_PROGRAM="install -s -m 555" BSD_INSTALL_LIB="install -s -m 0644" BSD_INSTALL_SCRIPT="install -m 555" BSD_INSTALL_DATA="install -m 0644" BSD_INSTALL_MAN="install -m 444" SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: MAKE_ARGS ------------------------------------------------------------------------------- DESTDIR=/construction/math/cvc4/stage SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: PLIST_SUB ------------------------------------------------------------------------------- CLN="@comment " NO_CLN="" CRYPTOMINISAT="" NO_CRYPTOMINISAT="@comment " GMP="" NO_GMP="@comment " JAVA="" NO_JAVA="@comment " PYTHON="" NO_PYTHON="@comment " READLINE="" NO_READLINE="@comment " JAVASHAREDIR="share/java" JAVAJARDIR="share/java/classes" CMAKE_BUILD_TYPE="production" PYTHON_INCLUDEDIR=include/python3.9 PYTHON_LIBDIR=lib/python3.9 PYTHON_PLATFORM=dragonfly6 PYTHON_SITELIBDIR=lib/python3.9/site-packages PYTHON_SUFFIX=39 PYTHON_EXT_SUFFIX=.cpython-39 PYTHON_VER=3.9 PYTHON_VERSION=python3.9 PYTHON2="@comment " PYTHON3="" OSREL=6.5 PREFIX=%D LOCALBASE=/usr/local RESETPREFIX=/usr/local LIB32DIR=lib PROFILE="@comment " DOCSDIR="share/doc/cvc4" EXAMPLESDIR="share/examples/cvc4" DATADIR="share/cvc4" WWWDIR="www/cvc4" ETCDIR="etc/cvc4" SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: SUB_LIST ------------------------------------------------------------------------------- CLN="@comment " NO_CLN="" CRYPTOMINISAT="" NO_CRYPTOMINISAT="@comment " GMP="" NO_GMP="@comment " JAVA="" NO_JAVA="@comment " PYTHON="" NO_PYTHON="@comment " READLINE="" NO_READLINE="@comment " JAVASHAREDIR="/usr/local/share/java" JAVAJARDIR="/usr/local/share/java/classes" JAVALIBDIR="/usr/local/share/java/classes" PREFIX=/usr/local LOCALBASE=/usr/local DATADIR=/usr/local/share/cvc4 DOCSDIR=/usr/local/share/doc/cvc4 EXAMPLESDIR=/usr/local/share/examples/cvc4 WWWDIR=/usr/local/www/cvc4 ETCDIR=/usr/local/etc/cvc4 SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: /etc/make.conf ------------------------------------------------------------------------------- DPORTS_BUILDER=yes DISABLE_LICENSES=yes DEFAULT_VERSIONS=ssl=openssl FORCE_PACKAGE=yes DEVELOPER=yes DFLY_STING_XFAIL=yes USE_PACKAGE_DEPENDS_ONLY=yes PORTSDIR=/xports PORT_DBDIR=/options PKG_DBDIR=/var/db/pkg PKG_CACHEDIR=/var/cache/pkg PKG_COMPRESSION_FORMAT=.tgz DEVELOPER=1 WITH_CCACHE_BUILD=yes CCACHE_DIR=/ccache UID=0 ARCH=x86_64 OPSYS=DragonFly DFLYVERSION=600500 OSVERSION=9999999 OSREL=6.5 _OSRELEASE=6.5-SYNTH DISTDIR=/distfiles WRKDIRPREFIX=/construction BATCH=yes PACKAGE_BUILDING=yes PKG_CREATE_VERBOSE=yes MAKE_JOBS_NUMBER=16 SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: setup ------------------------------------------------------------------------------- Installing /packages/All/indexinfo-0.3.1.pkg Installing /packages/All/gettext-runtime-0.21.pkg Installing /packages/All/ncurses-6.3.pkg ===== Message from ncurses-6.3: -- To get the terminfo database please install the terminfo-db package: pkg install terminfo-db Installing /packages/All/bash-5.2_3.pkg Installing /packages/All/pcre-8.45_1.pkg Installing /packages/All/swig-4.0.2.pkg Installing /packages/All/brotli-1.0.9,1.pkg Installing /packages/All/png-1.6.37_1.pkg Installing /packages/All/freetype2-2.12.1_2.pkg ===== Message from freetype2-2.12.1_2: -- The 2.7.x series now uses the new subpixel hinting mode (V40 port's option) as the default, emulating a modern version of ClearType. This change inevitably leads to different rendering results, and you might change port's options to adapt it to your taste (or use the new "FREETYPE_PROPERTIES" environment variable). The environment variable "FREETYPE_PROPERTIES" can be used to control the driver properties. Example: FREETYPE_PROPERTIES=truetype:interpreter-version=35 \ cff:no-stem-darkening=1 \ autofitter:warping=1 This allows to select, say, the subpixel hinting mode at runtime for a given application. If LONG_PCF_NAMES port's option was enabled, the PCF family names may include the foundry and information whether they contain wide characters. For example, "Sony Fixed" or "Misc Fixed Wide", instead of "Fixed". This can be disabled at run time with using pcf:no-long-family-names property, if needed. Example: FREETYPE_PROPERTIES=pcf:no-long-family-names=1 How to recreate fontconfig cache with using such environment variable, if needed: # env FREETYPE_PROPERTIES=pcf:no-long-family-names=1 fc-cache -fsv The controllable properties are listed in the section "Controlling FreeType Modules" in the reference's table of contents (/usr/local/share/doc/freetype2/reference/index.html, if documentation was installed). Installing /packages/All/expat-2.4.9.pkg Installing /packages/All/fontconfig-2.14.0,1.pkg Running fc-cache to build fontconfig cache... Installing /packages/All/libinotify-20211018.pkg ===== Message from libinotify-20211018: -- You might want to consider increasing the kern.maxfiles tunable if you plan to use this library for applications that need to monitor activity of a lot of files. Installing /packages/All/alsa-lib-1.2.2_1.pkg ===== Message from alsa-lib-1.2.2_1: -- ===> NOTICE: The alsa-lib port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://docs.freebsd.org/en/articles/contributing/#ports-contributing Installing /packages/All/giflib-5.2.1.pkg Installing /packages/All/javavmwrapper-2.7.9.pkg Installing /packages/All/libfontenc-1.1.4.pkg Installing /packages/All/mkfontscale-1.2.1.pkg Installing /packages/All/dejavu-2.37_1.pkg Running fc-cache to build fontconfig cache... ===== Message from dejavu-2.37_1: -- Make sure that the freetype module is loaded. If it is not, add the following line to the "Modules" section of your X Windows configuration file: Load "freetype" Add the following line to the "Files" section of X Windows configuration file: FontPath "/usr/local/share/fonts/dejavu/" Note: your X Windows configuration file is typically /etc/X11/XF86Config if you are using XFree86, and /etc/X11/xorg.conf if you are using X.Org. Installing /packages/All/java-zoneinfo-2021.e.pkg Installing /packages/All/libpthread-stubs-0.4.pkg Installing /packages/All/libXau-1.0.9.pkg Installing /packages/All/xorgproto-2022.1.pkg Installing /packages/All/libXdmcp-1.1.3.pkg Installing /packages/All/libxcb-1.15.pkg Installing /packages/All/libX11-1.7.2,1.pkg Installing /packages/All/libXext-1.3.4,1.pkg Installing /packages/All/libXfixes-6.0.0.pkg Installing /packages/All/libXi-1.8,1.pkg Installing /packages/All/libXrender-0.9.10_2.pkg Installing /packages/All/libICE-1.0.10,1.pkg Installing /packages/All/libSM-1.2.3,1.pkg Installing /packages/All/libXt-1.2.1,1.pkg Installing /packages/All/libXtst-1.2.3_2.pkg Installing /packages/All/openjdk8-8.342.07.1_1.pkg ===== Message from openjdk8-8.342.07.1_1: -- This OpenJDK implementation requires procfs(5) mounted on /proc. If you have not done it yet, please do the following: mount -t procfs proc /proc To make it permanent, you need the following lines in /etc/fstab: proc /proc procfs rw 0 0 Installing /packages/All/libnghttp2-1.48.0.pkg Installing /packages/All/openssl-1.1.1q,1.pkg Installing /packages/All/libssh2-1.10.0,3.pkg Installing /packages/All/libunistring-1.0.pkg Installing /packages/All/libidn2-2.3.3.pkg Installing /packages/All/libpsl-0.21.1_4.pkg Installing /packages/All/ca_root_nss-3.83.pkg ===== Message from ca_root_nss-3.83: -- FreeBSD does not, and can not warrant that the certification authorities whose certificates are included in this package have in any way been audited for trustworthiness or RFC 3647 compliance. Assessment and verification of trust is the complete responsibility of the system administrator. This package installs symlinks to support root certificates discovery by default for software that uses OpenSSL. This enables SSL Certificate Verification by client software without manual intervention. If you prefer to do this manually, replace the following symlinks with either an empty file or your site-local certificate bundle. * /etc/ssl/cert.pem * /usr/local/etc/ssl/cert.pem * /usr/local/openssl/cert.pem Installing /packages/All/curl-7.86.0.pkg Installing /packages/All/libuv-1.44.2.pkg Installing /packages/All/rhash-1.4.3.pkg Installing /packages/All/liblz4-1.9.4,1.pkg Installing /packages/All/zstd-1.5.2_1.pkg Installing /packages/All/libarchive-3.6.1,1.pkg Installing /packages/All/cmake-core-3.24.0.pkg Installing /packages/All/pkgconf-1.8.0_1,1.pkg Installing /packages/All/libffi-3.4.2.pkg Installing /packages/All/mpdecimal-2.5.1.pkg Installing /packages/All/readline-8.1.2.pkg Installing /packages/All/python39-3.9.16.pkg ===== Message from python39-3.9.16: -- Note that some standard Python modules are provided as separate ports as they require additional dependencies. They are available as: py39-gdbm databases/py-gdbm@py39 py39-sqlite3 databases/py-sqlite3@py39 py39-tkinter x11-toolkits/py-tkinter@py39 Installing /packages/All/ccache-3.7.12_4.pkg Create compiler links... create symlink for cc create symlink for cc (world) create symlink for c++ create symlink for c++ (world) create symlink for CC create symlink for CC (world) create symlink for gcc create symlink for gcc (world) create symlink for g++ create symlink for g++ (world) ===== Message from ccache-3.7.12_4: -- NOTE: Please read /usr/local/share/doc/ccache/ccache-howto-freebsd.txt for information on using ccache with FreeBSD ports and src. Installing /packages/All/libantlr3c-3.4_1.pkg Installing /packages/All/icu-71.1,1.pkg Installing /packages/All/boost-libs-1.80.0.pkg ===== Message from boost-libs-1.80.0: -- You have built the Boost library with thread support. Don't forget to add -pthread to your linker options when linking your code. Installing /packages/All/M4RI-20200125.pkg Installing /packages/All/cryptominisat-5.8.0_2.pkg Installing /packages/All/gmp-6.2.1.pkg SUCCEEDED 00:00:16 ------------------------------------------------------------------------------- -- Phase: check-sanity ------------------------------------------------------------------------------- ===> NOTICE: The cvc4 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://docs.freebsd.org/en/articles/contributing/#ports-contributing SUCCEEDED 00:00:01 ------------------------------------------------------------------------------- -- Phase: pkg-depends ------------------------------------------------------------------------------- ===> cvc4-1.7_6 depends on file: /usr/local/sbin/pkg - found SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: fetch-depends ------------------------------------------------------------------------------- SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: fetch ------------------------------------------------------------------------------- ===> NOTICE: The cvc4 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://docs.freebsd.org/en/articles/contributing/#ports-contributing ===> cvc4-1.7_6 depends on file: /usr/local/sbin/pkg - found ===> Fetching all distfiles required by cvc4-1.7_6 for building SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: checksum ------------------------------------------------------------------------------- ===> NOTICE: The cvc4 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://docs.freebsd.org/en/articles/contributing/#ports-contributing ===> cvc4-1.7_6 depends on file: /usr/local/sbin/pkg - found ===> Fetching all distfiles required by cvc4-1.7_6 for building => SHA256 Checksum OK for antlr-3.4-complete.jar. => SHA256 Checksum OK for CVC4-CVC4-1.7_GH0.tar.gz. => SHA256 Checksum OK for fc8907afc08d.patch. SUCCEEDED 00:00:01 ------------------------------------------------------------------------------- -- Phase: extract-depends ------------------------------------------------------------------------------- SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: extract ------------------------------------------------------------------------------- ===> NOTICE: The cvc4 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://docs.freebsd.org/en/articles/contributing/#ports-contributing ===> cvc4-1.7_6 depends on file: /usr/local/sbin/pkg - found ===> Fetching all distfiles required by cvc4-1.7_6 for building ===> Extracting for cvc4-1.7_6 => SHA256 Checksum OK for antlr-3.4-complete.jar. => SHA256 Checksum OK for CVC4-CVC4-1.7_GH0.tar.gz. => SHA256 Checksum OK for fc8907afc08d.patch. Extracted Memory Use: 47.96M SUCCEEDED 00:00:01 ------------------------------------------------------------------------------- -- Phase: patch-depends ------------------------------------------------------------------------------- SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: patch ------------------------------------------------------------------------------- ===> Patching for cvc4-1.7_6 ===> Applying distribution patches for cvc4-1.7_6 ===> Applying ports patches for cvc4-1.7_6 from /xports/math/cvc4/files ===> Applying dragonfly patches for cvc4-1.7_6 from /xports/math/cvc4/dragonfly SUCCEEDED 00:00:01 ------------------------------------------------------------------------------- -- Phase: build-depends ------------------------------------------------------------------------------- ===> cvc4-1.7_6 depends on executable: bash - found ===> cvc4-1.7_6 depends on executable: swig - found ===> cvc4-1.7_6 depends on executable: swig - found ===> cvc4-1.7_6 depends on file: /usr/local/openjdk8/bin/java - found ===> cvc4-1.7_6 depends on file: /usr/local/bin/cmake - found ===> cvc4-1.7_6 depends on file: /usr/local/lib/libncurses.so.6 - found ===> cvc4-1.7_6 depends on package: pkgconf>=1.3.0_1 - found ===> cvc4-1.7_6 depends on file: /usr/local/bin/python3.9 - found ===> cvc4-1.7_6 depends on file: /usr/local/bin/ccache - found SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: lib-depends ------------------------------------------------------------------------------- ===> cvc4-1.7_6 depends on shared library: libantlr3c.so - found (/usr/local/lib/libantlr3c.so) ===> cvc4-1.7_6 depends on shared library: libboost_system.so - found (/usr/local/lib/libboost_system.so) ===> cvc4-1.7_6 depends on shared library: libcryptominisat5.so - found (/usr/local/lib/libcryptominisat5.so) ===> cvc4-1.7_6 depends on shared library: libgmp.so - found (/usr/local/lib/libgmp.so) ===> cvc4-1.7_6 depends on shared library: libboost_thread.so - found (/usr/local/lib/libboost_thread.so) ===> cvc4-1.7_6 depends on shared library: libreadline.so.8 - found (/usr/local/lib/libreadline.so.8) SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: configure ------------------------------------------------------------------------------- ===> cvc4-1.7_6 depends on executable: bash - found ===> cvc4-1.7_6 depends on executable: swig - found ===> cvc4-1.7_6 depends on executable: swig - found ===> cvc4-1.7_6 depends on file: /usr/local/openjdk8/bin/java - found ===> cvc4-1.7_6 depends on file: /usr/local/bin/cmake - found ===> cvc4-1.7_6 depends on file: /usr/local/lib/libncurses.so.6 - found ===> cvc4-1.7_6 depends on package: pkgconf>=1.3.0_1 - found ===> cvc4-1.7_6 depends on file: /usr/local/bin/python3.9 - found ===> cvc4-1.7_6 depends on file: /usr/local/bin/ccache - found ===> cvc4-1.7_6 depends on shared library: libantlr3c.so - found (/usr/local/lib/libantlr3c.so) ===> cvc4-1.7_6 depends on shared library: libboost_system.so - found (/usr/local/lib/libboost_system.so) ===> cvc4-1.7_6 depends on shared library: libcryptominisat5.so - found (/usr/local/lib/libcryptominisat5.so) ===> cvc4-1.7_6 depends on shared library: libgmp.so - found (/usr/local/lib/libgmp.so) ===> cvc4-1.7_6 depends on shared library: libboost_thread.so - found (/usr/local/lib/libboost_thread.so) ===> cvc4-1.7_6 depends on shared library: libreadline.so.8 - found (/usr/local/lib/libreadline.so.8) ===> Configuring for cvc4-1.7_6 ===> Performing out-of-source build /bin/mkdir -p /construction/math/cvc4/.build -- The C compiler identification is GNU 8.3.0 -- The CXX compiler identification is GNU 8.3.0 -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/local/libexec/ccache/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/local/libexec/ccache/c++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- Building Production build -- Performing Test HAVE_FLAG_O3 -- Performing Test HAVE_FLAG_O3 - Success -- Configuring with C flag '-O3' -- Configuring with CXX flag '-O3' -- Performing Test HAVE_FLAG_Wall -- Performing Test HAVE_FLAG_Wall - Success -- Configuring with C flag '-Wall' -- Configuring with CXX flag '-Wall' -- Performing Test HAVE_FLAG_fexceptions -- Performing Test HAVE_FLAG_fexceptions - Success -- Configuring with C flag '-fexceptions' -- Performing Test HAVE_FLAG_Wno_deprecated -- Performing Test HAVE_FLAG_Wno_deprecated - Success -- Configuring with C flag '-Wno-deprecated' -- Configuring with CXX flag '-Wno-deprecated' -- Performing Test HAVE_FLAG_Wsuggest_override -- Performing Test HAVE_FLAG_Wsuggest_override - Success -- Configuring with CXX flag '-Wsuggest-override' -- Performing Test HAVE_FLAG_Wnon_virtual_dtor -- Performing Test HAVE_FLAG_Wnon_virtual_dtor - Success -- Configuring with CXX flag '-Wnon-virtual-dtor' -- Performing Test HAVE_FLAG_Wno_class_memaccess -- Performing Test HAVE_FLAG_Wno_class_memaccess - Success -- Configuring with CXX flag '-Wno-class-memaccess' -- Found PythonInterp: /usr/local/bin/python3.9 (found suitable version "3.9.16", minimum required is "3") -- Found GMP: /usr/local/include -- Found GMP libs: /usr/local/lib/libgmp.so CMake Warning at /usr/local/share/cmake/Modules/FindBoost.cmake:1390 (message): New Boost version may have incorrect or missing dependencies and imported targets Call Stack (most recent call first): /usr/local/share/cmake/Modules/FindBoost.cmake:1513 (_Boost_COMPONENT_DEPENDENCIES) /usr/local/share/cmake/Modules/FindBoost.cmake:2124 (_Boost_MISSING_DEPENDENCIES) CMakeLists.txt:328 (find_package) CMake Warning at /usr/local/share/cmake/Modules/FindBoost.cmake:1390 (message): New Boost version may have incorrect or missing dependencies and imported targets Call Stack (most recent call first): /usr/local/share/cmake/Modules/FindBoost.cmake:1513 (_Boost_COMPONENT_DEPENDENCIES) /usr/local/share/cmake/Modules/FindBoost.cmake:2124 (_Boost_MISSING_DEPENDENCIES) CMakeLists.txt:328 (find_package) CMake Warning at /usr/local/share/cmake/Modules/FindBoost.cmake:1390 (message): New Boost version may have incorrect or missing dependencies and imported targets Call Stack (most recent call first): /usr/local/share/cmake/Modules/FindBoost.cmake:1513 (_Boost_COMPONENT_DEPENDENCIES) /usr/local/share/cmake/Modules/FindBoost.cmake:2124 (_Boost_MISSING_DEPENDENCIES) CMakeLists.txt:328 (find_package) -- Performing Test CMAKE_HAVE_LIBC_PTHREAD -- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Failed -- Looking for pthread_create in pthreads -- Looking for pthread_create in pthreads - not found -- Looking for pthread_create in pthread -- Looking for pthread_create in pthread - found -- Found Threads: TRUE -- Found Boost: /usr/local/include (found suitable version "1.80.0", minimum required is "1.50.0") found components: thread chrono atomic -- Configuring with C flag '-pthread' -- Configuring with CXX flag '-pthread' -- Configuring with C flag '-pthread' -- Configuring with CXX flag '-pthread' -- Found CryptoMiniSat: /usr/local/include -- Found CryptoMiniSat libs: /usr/local/lib/libcryptominisat5.so -- Found Readline: /usr/local/include -- Found Readline libs: /usr/local/lib/libreadline.so;/usr/local/lib/libtinfo.so -- Performing Test CVC4_NEED_INT64_T_OVERLOADS -- Performing Test CVC4_NEED_INT64_T_OVERLOADS - Failed -- Performing Test CVC4_NEED_HASH_UINT64_T_OVERLOAD -- Performing Test CVC4_NEED_HASH_UINT64_T_OVERLOAD - Failed -- Looking for unistd.h -- Looking for unistd.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 - 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 -- Performing Test STRERROR_R_CHAR_P -- Performing Test STRERROR_R_CHAR_P - Failed -- Found Boost: /usr/local/include (found suitable version "1.80.0", minimum required is "1.50.0") -- Found Java: /usr/local/bin/java (found version "1.8.0.342") -- Could NOT find Git (missing: GIT_EXECUTABLE) -- Looking for antlr3FileStreamNew -- Looking for antlr3FileStreamNew - found -- Found ANTLR: /construction/math/cvc4/antlr3 -- Found ANTLR libs: /usr/local/lib/libantlr3c.so -- Found Java: /usr/local/bin/java (found version "1.8.0.342") found components: Runtime -- Found SWIG: /usr/local/bin/swig (found suitable version "4.0.2", minimum required is "3.0.0") -- Found Java: /usr/local/bin/java (found version "1.8.0.342") -- Found JNI: /usr/local/openjdk8/include found components: AWT JVM CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:775 (message): Policy CMP0078 is not set: UseSWIG generates standard target names. Run "cmake --help-policy CMP0078" for policy details. Use the cmake_policy command to set the policy and suppress this warning. Call Stack (most recent call first): src/bindings/java/CMakeLists.txt:14 (swig_add_library) This warning is for project developers. Use -Wno-dev to suppress it. CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:617 (message): Policy CMP0086 is not set: UseSWIG honors SWIG_MODULE_NAME via -module flag. Run "cmake --help-policy CMP0086" for policy details. Use the cmake_policy command to set the policy and suppress this warning. Call Stack (most recent call first): /usr/local/share/cmake/Modules/UseSWIG.cmake:888 (SWIG_ADD_SOURCE_TO_MODULE) src/bindings/java/CMakeLists.txt:14 (swig_add_library) This warning is for project developers. Use -Wno-dev to suppress it. -- Found PythonLibs: /usr/local/lib/libpython3.9.so (found suitable version "3.9.16", minimum required is "3.9") CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:775 (message): Policy CMP0078 is not set: UseSWIG generates standard target names. Run "cmake --help-policy CMP0078" for policy details. Use the cmake_policy command to set the policy and suppress this warning. Call Stack (most recent call first): src/bindings/python/CMakeLists.txt:23 (swig_add_library) This warning is for project developers. Use -Wno-dev to suppress it. CMake Warning (dev) at /usr/local/share/cmake/Modules/UseSWIG.cmake:617 (message): Policy CMP0086 is not set: UseSWIG honors SWIG_MODULE_NAME via -module flag. Run "cmake --help-policy CMP0086" for policy details. Use the cmake_policy command to set the policy and suppress this warning. Call Stack (most recent call first): /usr/local/share/cmake/Modules/UseSWIG.cmake:888 (SWIG_ADD_SOURCE_TO_MODULE) src/bindings/python/CMakeLists.txt:23 (swig_add_library) This warning is for project developers. Use -Wno-dev to suppress it. CVC4 1.7 Build profile : production GPL : on Best configuration : off Optimized : on Optimization level : off Assertions : off Debug symbols : off Debug context mem mgr: off Dumping : off Muzzle : off Proofs : on Replay : off Statistics : on Tracing : off Asan : off Coverage (gcov) : off Profiling (gprof) : off Unit tests : off Valgrind : off Shared libs : on Static binary : off Java bindings : off Python bindings : off Python2 : off Python3 : off Portfolio : off ABC : off CaDiCaL : off CryptoMiniSat : off drat2er : off GLPK : off LFSC : off MP library : gmp Readline : off SymFPU : off CPPLAGS (-D...) : NDEBUG CVC4_PORTFOLIO CVC4_PROOF CVC4_STATISTICS_ON CVC4_USE_CRYPTOMINISAT CXXFLAGS : -pipe -I/usr/local/include -I/usr/local/include/ncurses -O2 -fno-strict-aliasing -O3 -Wall -Wno-deprecated -Wsuggest-override -Wnon-virtual-dtor -Wno-class-memaccess -pthread -pthread CFLAGS : -pipe -I/usr/local/include -I/usr/local/include/ncurses -O2 -fno-strict-aliasing -O3 -Wall -fexceptions -Wno-deprecated -pthread -pthread Install prefix : /usr/local CVC4 license : GPLv3 (due to optional libraries; see below) Please note that CVC4 will be built against the following GPLed libraries: readline As these libraries are covered under the GPLv3, so is this build of CVC4. CVC4 is also available to you under the terms of the (modified) BSD license. If you prefer to license CVC4 under those terms, please configure CVC4 to disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON). Now just type make, followed by make check or make install. -- Configuring done -- Generating done CMake Warning: Manually-specified variables were not used by the project: CMAKE_CXX_FLAGS_DEBUG CMAKE_CXX_FLAGS_RELEASE CMAKE_C_FLAGS_DEBUG CMAKE_C_FLAGS_RELEASE -- Build files have been written to: /construction/math/cvc4/.build SUCCEEDED 00:00:06 ------------------------------------------------------------------------------- -- Phase: build ------------------------------------------------------------------------------- ===> Building for cvc4-1.7_6 /usr/local/bin/cmake -S/construction/math/cvc4/CVC4-1.7 -B/construction/math/cvc4/.build --check-build-system CMakeFiles/Makefile.cmake 0 /usr/local/bin/cmake -E cmake_progress_start /construction/math/cvc4/.build/CMakeFiles /construction/math/cvc4/.build//CMakeFiles/progress.marks /usr/bin/make -f CMakeFiles/Makefile2 all --- src/base/CMakeFiles/gen-tags-trace.dir/all --- --- src/base/CMakeFiles/gen-tags-debug.dir/all --- --- src/base/CMakeFiles/gen-gitinfo.dir/all --- --- src/theory/CMakeFiles/gen-theory.dir/all --- --- src/options/CMakeFiles/gen-options.dir/all --- --- src/expr/CMakeFiles/gen-expr.dir/all --- --- src/main/CMakeFiles/gen-tokens.dir/all --- --- src/base/CMakeFiles/gen-tags-trace.dir/all --- /usr/bin/make -f src/base/CMakeFiles/gen-tags-trace.dir/build.make src/base/CMakeFiles/gen-tags-trace.dir/depend --- src/base/CMakeFiles/gen-gitinfo.dir/all --- /usr/bin/make -f src/base/CMakeFiles/gen-gitinfo.dir/build.make src/base/CMakeFiles/gen-gitinfo.dir/depend --- src/options/CMakeFiles/gen-options.dir/all --- /usr/bin/make -f src/options/CMakeFiles/gen-options.dir/build.make src/options/CMakeFiles/gen-options.dir/depend --- src/expr/CMakeFiles/gen-expr.dir/all --- /usr/bin/make -f src/expr/CMakeFiles/gen-expr.dir/build.make src/expr/CMakeFiles/gen-expr.dir/depend --- src/base/CMakeFiles/gen-tags-debug.dir/all --- /usr/bin/make -f src/base/CMakeFiles/gen-tags-debug.dir/build.make src/base/CMakeFiles/gen-tags-debug.dir/depend --- src/main/CMakeFiles/gen-tokens.dir/all --- /usr/bin/make -f src/main/CMakeFiles/gen-tokens.dir/build.make src/main/CMakeFiles/gen-tokens.dir/depend --- src/base/CMakeFiles/gen-gitinfo.dir/all --- --- src/base/CMakeFiles/gen-gitinfo.dir/depend --- --- src/theory/CMakeFiles/gen-theory.dir/all --- /usr/bin/make -f src/theory/CMakeFiles/gen-theory.dir/build.make src/theory/CMakeFiles/gen-theory.dir/depend --- src/base/CMakeFiles/gen-gitinfo.dir/all --- cd /construction/math/cvc4/.build && /usr/local/bin/cmake -E cmake_depends "Unix Makefiles" /construction/math/cvc4/CVC4-1.7 /construction/math/cvc4/CVC4-1.7/src/base /construction/math/cvc4/.build /construction/math/cvc4/.build/src/base /construction/math/cvc4/.build/src/base/CMakeFiles/gen-gitinfo.dir/DependInfo.cmake --- src/options/CMakeFiles/gen-options.dir/all --- --- src/options/CMakeFiles/gen-options.dir/depend --- cd /construction/math/cvc4/.build && /usr/local/bin/cmake -E cmake_depends "Unix Makefiles" /construction/math/cvc4/CVC4-1.7 /construction/math/cvc4/CVC4-1.7/src/options /construction/math/cvc4/.build /construction/math/cvc4/.build/src/options /construction/math/cvc4/.build/src/options/CMakeFiles/gen-options.dir/DependInfo.cmake --- src/base/CMakeFiles/gen-tags-trace.dir/all --- --- src/base/CMakeFiles/gen-tags-trace.dir/depend --- cd /construction/math/cvc4/.build && /usr/local/bin/cmake -E cmake_depends "Unix Makefiles" /construction/math/cvc4/CVC4-1.7 /construction/math/cvc4/CVC4-1.7/src/base /construction/math/cvc4/.build /construction/math/cvc4/.build/src/base /construction/math/cvc4/.build/src/base/CMakeFiles/gen-tags-trace.dir/DependInfo.cmake --- src/expr/CMakeFiles/gen-expr.dir/all --- --- src/expr/CMakeFiles/gen-expr.dir/depend --- cd /construction/math/cvc4/.build && /usr/local/bin/cmake -E cmake_depends "Unix Makefiles" /construction/math/cvc4/CVC4-1.7 /construction/math/cvc4/CVC4-1.7/src/expr /construction/math/cvc4/.build /construction/math/cvc4/.build/src/expr /construction/math/cvc4/.build/src/expr/CMakeFiles/gen-expr.dir/DependInfo.cmake --- src/base/CMakeFiles/gen-tags-debug.dir/all --- --- src/base/CMakeFiles/gen-tags-debug.dir/depend --- cd /construction/math/cvc4/.build && /usr/local/bin/cmake -E cmake_depends "Unix Makefiles" /construction/math/cvc4/CVC4-1.7 /construction/math/cvc4/CVC4-1.7/src/base /construction/math/cvc4/.build /construction/math/cvc4/.build/src/base /construction/math/cvc4/.build/src/base/CMakeFiles/gen-tags-debug.dir/DependInfo.cmake --- src/main/CMakeFiles/gen-tokens.dir/all --- --- src/main/CMakeFiles/gen-tokens.dir/depend --- cd /construction/math/cvc4/.build && /usr/local/bin/cmake -E cmake_depends "Unix Makefiles" /construction/math/cvc4/CVC4-1.7 /construction/math/cvc4/CVC4-1.7/src/main /construction/math/cvc4/.build /construction/math/cvc4/.build/src/main /construction/math/cvc4/.build/src/main/CMakeFiles/gen-tokens.dir/DependInfo.cmake --- src/base/CMakeFiles/gen-tags-trace.dir/all --- /usr/bin/make -f src/base/CMakeFiles/gen-tags-trace.dir/build.make src/base/CMakeFiles/gen-tags-trace.dir/build --- src/base/CMakeFiles/gen-gitinfo.dir/all --- /usr/bin/make -f src/base/CMakeFiles/gen-gitinfo.dir/build.make src/base/CMakeFiles/gen-gitinfo.dir/build --- src/options/CMakeFiles/gen-options.dir/all --- /usr/bin/make -f src/options/CMakeFiles/gen-options.dir/build.make src/options/CMakeFiles/gen-options.dir/build --- src/expr/CMakeFiles/gen-expr.dir/all --- /usr/bin/make -f src/expr/CMakeFiles/gen-expr.dir/build.make src/expr/CMakeFiles/gen-expr.dir/build --- src/base/CMakeFiles/gen-gitinfo.dir/all --- --- src/base/CMakeFiles/gen-gitinfo --- --- src/base/CMakeFiles/gen-tags-debug.dir/all --- /usr/bin/make -f src/base/CMakeFiles/gen-tags-debug.dir/build.make src/base/CMakeFiles/gen-tags-debug.dir/build --- src/base/CMakeFiles/gen-tags-trace.dir/all --- --- src/base/CMakeFiles/gen-tags-trace --- --- src/base/CMakeFiles/gen-gitinfo.dir/all --- cd /construction/math/cvc4/.build/src/base && /usr/local/bin/cmake -DGIT_FOUND=FALSE -P GitInfo.cmake --- src/theory/CMakeFiles/gen-theory.dir/all --- --- src/theory/CMakeFiles/gen-theory.dir/depend --- --- src/base/CMakeFiles/gen-tags-trace.dir/all --- cd /construction/math/cvc4/.build/src/base && /construction/math/cvc4/CVC4-1.7/src/base/gentmptags.sh /construction/math/cvc4/CVC4-1.7/src/base Trace /construction/math/cvc4/CVC4-1.7/src/api/cvc4cpp.cpp\ /construction/math/cvc4/CVC4-1.7/src/api/cvc4cpp.h\ /construction/math/cvc4/CVC4-1.7/src/api/cvc4cppkind.h\ /construction/math/cvc4/CVC4-1.7/src/base/configuration.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/configuration.h\ /construction/math/cvc4/CVC4-1.7/src/base/configuration_private.h\ /construction/math/cvc4/CVC4-1.7/src/base/cvc4_assert.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/cvc4_assert.h\ /construction/math/cvc4/CVC4-1.7/src/base/cvc4_check.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/cvc4_check.h\ /construction/math/cvc4/CVC4-1.7/src/base/exception.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/exception.h\ /construction/math/cvc4/CVC4-1.7/src/base/listener.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/listener.h\ /construction/math/cvc4/CVC4-1.7/src/base/map_util.h\ /construction/math/--- src/theory/CMakeFiles/gen-theory.dir/all --- cd /construction/math/cvc4/.build && /usr/local/bin/cmake -E cmake_depends "Unix Makefiles" /construction/math/cvc4/CVC4-1.7 /construction/math/cvc4/CVC4-1.7/src/theory /construction/math/cvc4/.build /construction/math/cvc4/.build/src/theory /construction/math/cvc4/.build/src/theory/CMakeFiles/gen-theory.dir/DependInfo.cmake --- src/options/CMakeFiles/gen-options.dir/all --- --- src/options/options.cpp --- --- src/expr/CMakeFiles/gen-expr.dir/all --- --- src/expr/kind.h --- --- src/expr/metakind.h --- --- src/expr/type_checker.cpp --- --- src/expr/type_properties.h --- --- src/base/CMakeFiles/gen-tags-trace.dir/all --- cvc4/CVC4-1.7/src/base/modal_exception.h\ /construction/math/cvc4/CVC4-1.7/src/base/output.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/output.h\ /construction/math/cvc4/CVC4-1.7/src/bindings/java_iterator_adapter.h\ /construction/math/cvc4/CVC4-1.7/src/bindings/java_stream_adapters.h\ /construction/math/cvc4/CVC4-1.7/src/bindings/swig.h\ /construction/math/cvc4/CVC4-1.7/src/context/backtrackable.h\ /construction/math/cvc4/CVC4-1.7/src/context/cddense_set.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdhashmap.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdhashmap_forward.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdhashset.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdhashset_forward.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdinsert_hashmap.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdinsert_hashmap_forward.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdlist.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdlist_forward.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdmaybe.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdo.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdqueue.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdtrail_queue.h\ /construction/math/cvc4/CVC4-1.7/src/context/context.cpp\ /construction/math/cvc4/CVC4-1.7/src/context/context.h\ /construction/math/cvc4/CVC4-1.7/src/context/context_mm.cpp\ /construction/math/cvc4/CVC4-1.7/src/context/context_mm.h\ /construction/math/cvc4/CVC4-1.7/src/decision/decision_attributes.h\ /construction/math/cvc4/CVC4-1.7/src/decision/decision_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/decision/decision_engine.h\ /construction/math/cvc4/CVC4-1.7/src/decision/decision_strategy.h\ /construction/math/cvc4/CVC4-1.7/src/decision/justification_heuristic.cpp\ /construction/math/cvc4/CVC4-1.7/src/decision/justification_heuristic.h\ /construction/math/cvc4/CVC4-1.7/src/expr/array.h\ /construction/math/cvc4/CVC4-1.7/src/expr/array_store_all.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/array_store_all.h\ /construction/math/cvc4/CVC4-1.7/src/expr/ascription_type.h\ /construction/math/cvc4/CVC4-1.7/src/expr/attribute.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/attribute.h\ /construction/math/cvc4/CVC4-1.7/src/expr/attribute_internals.h\ /construction/math/cvc4/CVC4-1.7/src/expr/attribute_unique_id.h\ /construction/math/cvc4/CVC4-1.7/src/expr/chain.h\ /construction/math/cvc4/CVC4-1.7/src/expr/datatype.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/datatype.h\ /construction/math/cvc4/CVC4-1.7/src/expr/emptyset.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/emptyset.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_iomanip.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_iomanip.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_manager_scope.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_manager_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_manager_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_stream.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- --- src/base/CMakeFiles/gen-tags-debug --- --- src/base/CMakeFiles/gen-tags-trace.dir/all --- expr_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/kind_map.h\ /construction/math/cvc4/CVC4-1.7/src/expr/kind_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/kind_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/matcher.h\ /construction/math/cvc4/CVC4-1.7/src/expr/metakind_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/metakind_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_algorithm.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_algorithm.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_builder.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager_attributes.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager_listeners.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager_listeners.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_self_iterator.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_trie.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_trie.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_value.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_value.h\ /construction/math/cvc4/CVC4-1.7/src/expr/pickle_data.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/pickle_data.h\ /construction/math/cvc4/CVC4-1.7/src/expr/pickler.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/pickler.h\ /construction/math/cvc4/CVC4-1.7/src/expr/record.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/record.h\ /construction/math/cvc4/CVC4-1.7/src/expr/symbol_table.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/symbol_table.h\ /construction/math/cvc4/CVC4-1.7/src/expr/type.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/type.h\ /construction/math/cvc4/CVC4-1.7/src/expr/type_checker.h\ /construction/math/cvc4/CVC4-1.7/src/expr/type_checker_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/type_node.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/typ--- src/base/CMakeFiles/gen-tags-debug.dir/all --- cd /construction/math/cvc4/.build/src/base && /construction/math/cvc4/CVC4-1.7/src/base/gentmptags.sh /construction/math/cvc4/CVC4-1.7/src/base Debug /construction/math/cvc4/CVC4-1.7/src/api/cvc4cpp.cpp\ /construction/math/cvc4/CVC4-1.7/src/api/cvc4cpp.h\ /construction/math/cvc4/CVC4-1.7/src/api/cvc4cppkind.h\ /construction/math/cvc4/CVC4-1.7/src/base/configuration.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/configuration.h\ /construction/math/cvc4/CVC4-1.7/src/base/configuration_private.h\ /construction/math/cvc4/CVC4-1.7/src/base/cvc4_assert.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/cvc4_assert.h\ /construction/math/cvc4/CVC4-1.7/src/base/cvc4_check.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/cvc4_check.h\ /construction/math/cvc4/CVC4-1.7/src/base/exception.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/exception.h\ /construction/math/cvc4/CVC4-1.7/src/base/listener.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/listener.h\ /construction/math/cvc4/CVC4-1.7/src/base/map_util.h\ /construction/math/--- src/expr/CMakeFiles/gen-expr.dir/all --- --- src/expr/kind.h --- [ 0%] Generating kind.h --- src/base/CMakeFiles/gen-tags-trace.dir/all --- e_node.h\ /construction/math/cvc4/CVC4-1.7/src/expr/type_properties_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/uninterpreted_constant.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/uninterpreted_constant.h\ /construction/math/cvc4/CVC4-1.7/src/expr/variable_type_map.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4_private.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4_private_library.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4_public.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4parser_private.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4parser_public.h\ /construction/math/cvc4/CVC4-1.7/src/lib/clock_gettime.h\ /construction/math/cvc4/CVC4-1.7/src/lib/ffs.h\ /construction/math/cvc4/CVC4-1.7/src/lib/replacements.h\ /construction/math/cvc4/CVC4-1.7/src/lib/strtok_r.h\ /construction/math/cvc4/CVC4-1.7/src/main/command_executor.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/command_executor.h\ /construction/math/cvc4/C--- src/base/CMakeFiles/gen-tags-debug.dir/all --- cvc4/CVC4-1.7/src/base/modal_exception.h\ /construction/math/cvc4/CVC4-1.7/src/base/output.cpp\ /construction/math/cvc4/CVC4-1.7/src/base/output.h\ /construction/math/cvc4/CVC4-1.7/src/bindings/java_iterator_adapter.h\ /construction/math/cvc4/CVC4-1.7/src/bindings/java_stream_adapters.h\ /construction/math/cvc4/CVC4-1.7/src/bindings/swig.h\ /construction/math/cvc4/CVC4-1.7/src/context/backtrackable.h\ /construction/math/cvc4/CVC4-1.7/src/context/cddense_set.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdhashmap.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdhashmap_forward.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdhashset.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdhashset_forward.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdinsert_hashmap.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdinsert_hashmap_forward.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdlist.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdlist_forward.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdmaybe.h\--- src/expr/CMakeFiles/gen-expr.dir/all --- cd /construction/math/cvc4/.build/src/expr && /construction/math/cvc4/CVC4-1.7/src/expr/mkkind /construction/math/cvc4/CVC4-1.7/src/expr/kind_template.h /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/expr/kind.h --- src/expr/type_properties.h --- [ 0%] Generating type_properties.h --- src/base/CMakeFiles/gen-tags-trace.dir/all --- VC4-1.7/src/main/command_executor_portfolio.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/command_executor_portfolio.h\ /construction/math/cvc4/CVC4-1.7/src/main/driver_unified.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/interactive_shell.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/interactive_shell.h\ /construction/math/cvc4/CVC4-1.7/src/main/main.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/main.h\ /construction/math/cvc4/CVC4-1.7/src/main/portfolio.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/portfolio.h\ /construction/math/cvc4/CVC4-1.7/src/main/portfolio_util.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/portfolio_util.h\ /construction/math/cvc4/CVC4-1.7/src/main/util.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/argument_extender.h\ /construction/math/cvc4/CVC4-1.7/src/options/argument_extender_implementation.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/argument_extender_implementation.h\ /construction/math/cvc4/CVC4-1.7/src/options/arith_heuristic_pivot_rule.cpp\ /construction/math--- src/base/CMakeFiles/gen-tags-debug.dir/all --- /construction/math/cvc4/CVC4-1.7/src/context/cdo.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdqueue.h\ /construction/math/cvc4/CVC4-1.7/src/context/cdtrail_queue.h\ /construction/math/cvc4/CVC4-1.7/src/context/context.cpp\ /construction/math/cvc4/CVC4-1.7/src/context/context.h\ /construction/math/cvc4/CVC4-1.7/src/context/context_mm.cpp\ /construction/math/cvc4/CVC4-1.7/src/context/context_mm.h\ /construction/math/cvc4/CVC4-1.7/src/decision/decision_attributes.h\ /construction/math/cvc4/CVC4-1.7/src/decision/decision_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/decision/decision_engine.h\ /construction/math/cvc4/CVC4-1.7/src/decision/decision_strategy.h\ /construction/math/cvc4/CVC4-1.7/src/decision/justification_heuristic.cpp\ /construction/math/cvc4/CVC4-1.7/src/decision/justification_heuristic.h\ /construction/math/cvc4/CVC4-1.7/src/expr/array.h\ /construction/math/cvc4/CVC4-1.7/src/expr/array_store_all.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/array_store_all.h\ /construction/math/cvc4/CVC4--- src/options/CMakeFiles/gen-options.dir/all --- [ 1%] Generating options.cpp, options_holder.h, arith_options.cpp, arrays_options.cpp, base_options.cpp, booleans_options.cpp, builtin_options.cpp, bv_options.cpp, datatypes_options.cpp, decision_options.cpp, expr_options.cpp, fp_options.cpp, idl_options.cpp, main_options.cpp, parser_options.cpp, printer_options.cpp, proof_options.cpp, prop_options.cpp, quantifiers_options.cpp, sep_options.cpp, sets_options.cpp, smt_options.cpp, strings_options.cpp, theory_options.cpp, uf_options.cpp, arith_options.h, arrays_options.h, base_options.h, booleans_options.h, builtin_options.h, bv_options.h, datatypes_options.h, decision_options.h, expr_options.h, fp_options.h, idl_options.h, main_options.h, parser_options.h, printer_options.h, proof_options.h, prop_options.h, quantifiers_options.h, sep_options.h, sets_options.h, smt_options.h, strings_options.h, theory_options.h, uf_options.h --- src/expr/CMakeFiles/gen-expr.dir/all --- cd /construction/math/cvc4/.build/src/expr && /construction/math/cvc4/CVC4-1.7/src/expr/mkkind /construction/math/cvc4/CVC4-1.7/src/expr/type_properties_template.h /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/expr/type_properties.h --- src/base/CMakeFiles/gen-tags-trace.dir/all --- /cvc4/CVC4-1.7/src/options/arith_heuristic_pivot_rule.h\ /construction/math/cvc4/CVC4-1.7/src/options/arith_propagation_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/arith_propagation_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/arith_unate_lemma_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/arith_unate_lemma_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/base_handlers.h\ /construction/math/cvc4/CVC4-1.7/src/options/bool_to_bv_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/bool_to_bv_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/bv_bitblast_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/bv_bitblast_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/datatypes_modes.h\ /construction/math/cvc4/CVC4-1.7/src/options/decision_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/decision_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/decision_weight.h\ /construction/math/cvc4/CVC4-1.7/src/options/didyoumean.cpp\ /construction/math/cvc4/CVC4-1.7/src/opt--- src/base/CMakeFiles/gen-tags-debug.dir/all --- -1.7/src/expr/ascription_type.h\ /construction/math/cvc4/CVC4-1.7/src/expr/attribute.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/attribute.h\ /construction/math/cvc4/CVC4-1.7/src/expr/attribute_internals.h\ /construction/math/cvc4/CVC4-1.7/src/expr/attribute_unique_id.h\ /construction/math/cvc4/CVC4-1.7/src/expr/chain.h\ /construction/math/cvc4/CVC4-1.7/src/expr/datatype.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/datatype.h\ /construction/math/cvc4/CVC4-1.7/src/expr/emptyset.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/emptyset.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_iomanip.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_iomanip.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_manager_scope.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_manager_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_manager_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_stream.h\ /construction/math/cvc4/CVC4-1.7/src/expr/expr_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/--- src/options/CMakeFiles/gen-options.dir/all --- cd /construction/math/cvc4/.build/src/options && /usr/local/bin/python3.9 /construction/math/cvc4/CVC4-1.7/src/options/mkoptions.py /construction/math/cvc4/CVC4-1.7/src/options /construction/math/cvc4/.build/src/options/../../doc /construction/math/cvc4/.build/src/options /construction/math/cvc4/CVC4-1.7/src/options/arith_options.toml /construction/math/cvc4/CVC4-1.7/src/options/arrays_options.toml /construction/math/cvc4/CVC4-1.7/src/options/base_options.toml /construction/math/cvc4/CVC4-1.7/src/options/booleans_options.toml /construction/math/cvc4/CVC4-1.7/src/options/builtin_options.toml /construction/math/cvc4/CVC4-1.7/src/options/bv_options.toml /construction/math/cvc4/CVC4-1.7/src/options/datatypes_options.toml /construction/math/cvc4/CVC4-1.7/src/options/decision_options.toml /construction/math/cvc4/CVC4-1.7/src/options/expr_options.toml /construction/math/cvc4/CVC4-1.7/src/options/fp_options.toml /construction/math/cvc4/CVC4-1.7/src/options/idl_options.toml /construction/math/cvc4/CVC4-1.7/src/options--- src/expr/CMakeFiles/gen-expr.dir/all --- --- src/expr/type_checker.cpp --- [ 1%] Generating type_checker.cpp cd /construction/math/cvc4/.build/src/expr && /construction/math/cvc4/CVC4-1.7/src/expr/mkexpr /construction/math/cvc4/CVC4-1.7/src/expr/type_checker_template.cpp /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/expr/type_checker.cpp --- src/base/CMakeFiles/gen-gitinfo.dir/all --- [ 1%] Built target gen-gitinfo --- src/base/CMakeFiles/gen-tags-trace.dir/all --- ions/didyoumean.h\ /construction/math/cvc4/CVC4-1.7/src/options/didyoumean_test.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/language.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/language.h\ /construction/math/cvc4/CVC4-1.7/src/options/module_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/module_template.h\ /construction/math/cvc4/CVC4-1.7/src/options/open_ostream.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/open_ostream.h\ /construction/math/cvc4/CVC4-1.7/src/options/option_exception.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/option_exception.h\ /construction/math/cvc4/CVC4-1.7/src/options/options.h\ /construction/math/cvc4/CVC4-1.7/src/options/options_handler.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/options_handler.h\ /construction/math/cvc4/CVC4-1.7/src/options/options_holder_template.h\ /construction/math/cvc4/CVC4-1.7/src/options/options_public_functions.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/options_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- expr_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/kind_map.h\ /construction/math/cvc4/CVC4-1.7/src/expr/kind_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/kind_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/matcher.h\ /construction/math/cvc4/CVC4-1.7/src/expr/metakind_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/metakind_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_algorithm.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_algorithm.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_builder.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager_attributes.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager_listeners.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_manager_listeners.h\ /construction/math/cvc4/CVC4-1.7/src/expr/nod--- src/options/CMakeFiles/gen-options.dir/all --- /main_options.toml /construction/math/cvc4/CVC4-1.7/src/options/parser_options.toml /construction/math/cvc4/CVC4-1.7/src/options/printer_options.toml /construction/math/cvc4/CVC4-1.7/src/options/proof_options.toml /construction/math/cvc4/CVC4-1.7/src/options/prop_options.toml /construction/math/cvc4/CVC4-1.7/src/options/quantifiers_options.toml /construction/math/cvc4/CVC4-1.7/src/options/sep_options.toml /construction/math/cvc4/CVC4-1.7/src/options/sets_options.toml /construction/math/cvc4/CVC4-1.7/src/options/smt_options.toml /construction/math/cvc4/CVC4-1.7/src/options/strings_options.toml /construction/math/cvc4/CVC4-1.7/src/options/theory_options.toml /construction/math/cvc4/CVC4-1.7/src/options/uf_options.toml --- src/base/CMakeFiles/gen-tags-trace.dir/all --- options/printer_modes.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/printer_modes.h\ /construction/math/cvc4/CVC4-1.7/src/options/quantifiers_modes.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/quantifiers_modes.h\ /construction/math/cvc4/CVC4-1.7/src/options/set_language.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/set_language.h\ /construction/math/cvc4/CVC4-1.7/src/options/smt_modes.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/smt_modes.h\ /construction/math/cvc4/CVC4-1.7/src/options/strings_process_loop_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/strings_process_loop_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/sygus_out_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/theoryof_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/theoryof_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/ufss_mode.h\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_input.h\ /construction/math/cvc4/CVC4-1.7/src/parse--- src/base/CMakeFiles/gen-tags-debug.dir/all --- e_self_iterator.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_trie.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_trie.h\ /construction/math/cvc4/CVC4-1.7/src/expr/node_value.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/node_value.h\ /construction/math/cvc4/CVC4-1.7/src/expr/pickle_data.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/pickle_data.h\ /construction/math/cvc4/CVC4-1.7/src/expr/pickler.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/pickler.h\ /construction/math/cvc4/CVC4-1.7/src/expr/record.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/record.h\ /construction/math/cvc4/CVC4-1.7/src/expr/symbol_table.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/symbol_table.h\ /construction/math/cvc4/CVC4-1.7/src/expr/type.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/type.h\ /construction/math/cvc4/CVC4-1.7/src/expr/type_checker.h\ /construction/math/cvc4/CVC4-1.7/src/expr/type_checker_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/type_node.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/typ--- src/base/CMakeFiles/gen-tags-trace.dir/all --- r/antlr_input_imports.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_line_buffered_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_line_buffered_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_tracing.h\ /construction/math/cvc4/CVC4-1.7/src/parser/bounded_token_buffer.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/bounded_token_buffer.h\ /construction/math/cvc4/CVC4-1.7/src/parser/bounded_token_factory.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/bounded_token_factory.h\ /construction/math/cvc4/CVC4-1.7/src/parser/cvc/Cvc.g\ /construction/math/cvc4/CVC4-1.7/src/parser/cvc/cvc_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/cvc/cvc_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/line_buffer.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/line_buffer.h\ /construction/math/cvc4/CVC4-1.7/src/parser/memory_mapped_input_buffer.cpp\ /construction/math/cvc4/CVC--- src/base/CMakeFiles/gen-tags-debug.dir/all --- e_node.h\ /construction/math/cvc4/CVC4-1.7/src/expr/type_properties_template.h\ /construction/math/cvc4/CVC4-1.7/src/expr/uninterpreted_constant.cpp\ /construction/math/cvc4/CVC4-1.7/src/expr/uninterpreted_constant.h\ /construction/math/cvc4/CVC4-1.7/src/expr/variable_type_map.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4_private.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4_private_library.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4_public.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4parser_private.h\ /construction/math/cvc4/CVC4-1.7/src/include/cvc4parser_public.h\ /construction/math/cvc4/CVC4-1.7/src/lib/clock_gettime.h\ /construction/math/cvc4/CVC4-1.7/src/lib/ffs.h\ /construction/math/cvc4/CVC4-1.7/src/lib/replacements.h\ /construction/math/cvc4/CVC4-1.7/src/lib/strtok_r.h\ /construction/math/cvc4/CVC4-1.7/src/main/command_executor.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/command_executor.h\ /construction/math/cvc4/C--- src/base/CMakeFiles/gen-tags-trace.dir/all --- 4-1.7/src/parser/memory_mapped_input_buffer.h\ /construction/math/cvc4/CVC4-1.7/src/parser/parser.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/parser.h\ /construction/math/cvc4/CVC4-1.7/src/parser/parser_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/parser_builder.h\ /construction/math/cvc4/CVC4-1.7/src/parser/parser_exception.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/Smt1.g\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/smt1.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/smt1.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/smt1_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/smt1_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/Smt2.g\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/smt2.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/smt2.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/smt2_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/smt2_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/sygus_input.cpp\ /construc--- src/base/CMakeFiles/gen-tags-debug.dir/all --- VC4-1.7/src/main/command_executor_portfolio.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/command_executor_portfolio.h\ /construction/math/cvc4/CVC4-1.7/src/main/driver_unified.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/interactive_shell.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/interactive_shell.h\ /construction/math/cvc4/CVC4-1.7/src/main/main.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/main.h\ /construction/math/cvc4/CVC4-1.7/src/main/portfolio.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/portfolio.h\ /construction/math/cvc4/CVC4-1.7/src/main/portfolio_util.cpp\ /construction/math/cvc4/CVC4-1.7/src/main/portfolio_util.h\ /construction/math/cvc4/CVC4-1.7/src/main/util.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/argument_extender.h\ /construction/math/cvc4/CVC4-1.7/src/options/argument_extender_implementation.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/argument_extender_implementation.h\ /construction/math/cvc4/CVC4-1.7/src/options/arith_heuristic_pivot_rule.cpp\ /construction/math--- src/base/CMakeFiles/gen-tags-trace.dir/all --- tion/math/cvc4/CVC4-1.7/src/parser/smt2/sygus_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/Tptp.g\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/tptp.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/tptp.h\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/tptp_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/tptp_input.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/assertion_pipeline.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/assertion_pipeline.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/apply_substs.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/apply_substs.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/apply_to_const.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/apply_to_const.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bool_to_bv.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bool_to_bv.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_abstracti--- src/base/CMakeFiles/gen-tags-debug.dir/all --- /cvc4/CVC4-1.7/src/options/arith_heuristic_pivot_rule.h\ /construction/math/cvc4/CVC4-1.7/src/options/arith_propagation_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/arith_propagation_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/arith_unate_lemma_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/arith_unate_lemma_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/base_handlers.h\ /construction/math/cvc4/CVC4-1.7/src/options/bool_to_bv_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/bool_to_bv_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/bv_bitblast_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/bv_bitblast_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/datatypes_modes.h\ /construction/math/cvc4/CVC4-1.7/src/options/decision_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/decision_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/decision_weight.h\ /construction/math/cvc4/CVC4-1.7/src/options/didyoumean.cpp\ /construction/math/cvc4/CVC4-1.7/src/opt--- src/base/CMakeFiles/gen-tags-trace.dir/all --- on.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_abstraction.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_ackermann.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_ackermann.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_eager_atoms.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_eager_atoms.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_gauss.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_gauss.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_intro_pow2.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_intro_pow2.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_to_bool.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_to_bool.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/extended_rewriter_pass.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/extended_rewriter_pass.h\ /construction/math/cvc4/CV--- src/base/CMakeFiles/gen-tags-debug.dir/all --- ions/didyoumean.h\ /construction/math/cvc4/CVC4-1.7/src/options/didyoumean_test.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/language.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/language.h\ /construction/math/cvc4/CVC4-1.7/src/options/module_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/module_template.h\ /construction/math/cvc4/CVC4-1.7/src/options/open_ostream.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/open_ostream.h\ /construction/math/cvc4/CVC4-1.7/src/options/option_exception.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/option_exception.h\ /construction/math/cvc4/CVC4-1.7/src/options/options.h\ /construction/math/cvc4/CVC4-1.7/src/options/options_handler.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/options_handler.h\ /construction/math/cvc4/CVC4-1.7/src/options/options_holder_template.h\ /construction/math/cvc4/CVC4-1.7/src/options/options_public_functions.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/options_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- C4-1.7/src/preprocessing/passes/global_negate.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/global_negate.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/int_to_bv.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/int_to_bv.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/ite_removal.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/ite_removal.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/ite_simp.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/ite_simp.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/miplib_trick.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/miplib_trick.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/nl_ext_purify.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/nl_ext_purify.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/non_clausal_simp.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/non_clausal_simp.h\ /con--- src/base/CMakeFiles/gen-tags-debug.dir/all --- options/printer_modes.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/printer_modes.h\ /construction/math/cvc4/CVC4-1.7/src/options/quantifiers_modes.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/quantifiers_modes.h\ /construction/math/cvc4/CVC4-1.7/src/options/set_language.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/set_language.h\ /construction/math/cvc4/CVC4-1.7/src/options/smt_modes.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/smt_modes.h\ /construction/math/cvc4/CVC4-1.7/src/options/strings_process_loop_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/strings_process_loop_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/sygus_out_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/theoryof_mode.cpp\ /construction/math/cvc4/CVC4-1.7/src/options/theoryof_mode.h\ /construction/math/cvc4/CVC4-1.7/src/options/ufss_mode.h\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_input.h\ /construction/math/cvc4/CVC4-1.7/src/parse--- src/base/CMakeFiles/gen-tags-trace.dir/all --- struction/math/cvc4/CVC4-1.7/src/preprocessing/passes/pseudo_boolean_processor.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/pseudo_boolean_processor.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/quantifier_macros.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/quantifier_macros.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/quantifiers_preprocess.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/quantifiers_preprocess.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/real_to_int.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/real_to_int.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/rewrite.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/rewrite.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sep_skolem_emp.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sep_skolem_emp.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sort_infer.cpp\ /constru--- src/base/CMakeFiles/gen-tags-debug.dir/all --- r/antlr_input_imports.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_line_buffered_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_line_buffered_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/antlr_tracing.h\ /construction/math/cvc4/CVC4-1.7/src/parser/bounded_token_buffer.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/bounded_token_buffer.h\ /construction/math/cvc4/CVC4-1.7/src/parser/bounded_token_factory.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/bounded_token_factory.h\ /construction/math/cvc4/CVC4-1.7/src/parser/cvc/Cvc.g\ /construction/math/cvc4/CVC4-1.7/src/parser/cvc/cvc_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/cvc/cvc_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/line_buffer.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/line_buffer.h\ /construction/math/cvc4/CVC4-1.7/src/parser/memory_mapped_input_buffer.cpp\ /construction/math/cvc4/CVC--- src/base/CMakeFiles/gen-tags-trace.dir/all --- ction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sort_infer.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/static_learning.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/static_learning.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sygus_abduct.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sygus_abduct.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sygus_inference.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sygus_inference.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/symmetry_breaker.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/symmetry_breaker.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/symmetry_detect.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/symmetry_detect.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/synth_rew_rules.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/synth_rew_rules.h\ /construction/math/cvc4/CVC4--- src/base/CMakeFiles/gen-tags-debug.dir/all --- 4-1.7/src/parser/memory_mapped_input_buffer.h\ /construction/math/cvc4/CVC4-1.7/src/parser/parser.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/parser.h\ /construction/math/cvc4/CVC4-1.7/src/parser/parser_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/parser_builder.h\ /construction/math/cvc4/CVC4-1.7/src/parser/parser_exception.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/Smt1.g\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/smt1.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/smt1.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/smt1_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/smt1/smt1_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/Smt2.g\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/smt2.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/smt2.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/smt2_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/smt2_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/smt2/sygus_input.cpp\ /construc--- src/base/CMakeFiles/gen-tags-trace.dir/all --- -1.7/src/preprocessing/passes/theory_preprocess.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/theory_preprocess.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/unconstrained_simplifier.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/unconstrained_simplifier.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass_context.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass_context.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass_registry.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass_registry.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/util/ite_utilities.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/util/ite_utilities.h\ /construction/math/cvc4/CVC4-1.7/src/printer/ast/ast_printer.cpp\ /construction/math/cvc4/CV--- src/base/CMakeFiles/gen-tags-debug.dir/all --- tion/math/cvc4/CVC4-1.7/src/parser/smt2/sygus_input.h\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/Tptp.g\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/tptp.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/tptp.h\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/tptp_input.cpp\ /construction/math/cvc4/CVC4-1.7/src/parser/tptp/tptp_input.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/assertion_pipeline.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/assertion_pipeline.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/apply_substs.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/apply_substs.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/apply_to_const.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/apply_to_const.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bool_to_bv.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bool_to_bv.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_abstracti--- src/base/CMakeFiles/gen-tags-trace.dir/all --- C4-1.7/src/printer/ast/ast_printer.h\ /construction/math/cvc4/CVC4-1.7/src/printer/cvc/cvc_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/cvc/cvc_printer.h\ /construction/math/cvc4/CVC4-1.7/src/printer/dagification_visitor.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/dagification_visitor.h\ /construction/math/cvc4/CVC4-1.7/src/printer/printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/printer.h\ /construction/math/cvc4/CVC4-1.7/src/printer/smt2/smt2_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/smt2/smt2_printer.h\ /construction/math/cvc4/CVC4-1.7/src/printer/sygus_print_callback.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/sygus_print_callback.h\ /construction/math/cvc4/CVC4-1.7/src/printer/tptp/tptp_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/tptp/tptp_printer.h\ /construction/math/cvc4/CVC4-1.7/src/proof/arith_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/arith_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/arith_proof_recorder.cpp\ /constr--- src/base/CMakeFiles/gen-tags-debug.dir/all --- on.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_abstraction.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_ackermann.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_ackermann.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_eager_atoms.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_eager_atoms.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_gauss.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_gauss.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_intro_pow2.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_intro_pow2.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_to_bool.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/bv_to_bool.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/extended_rewriter_pass.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/extended_rewriter_pass.h\ /construction/math/cvc4/CV--- src/base/CMakeFiles/gen-tags-trace.dir/all --- uction/math/cvc4/CVC4-1.7/src/proof/arith_proof_recorder.h\ /construction/math/cvc4/CVC4-1.7/src/proof/array_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/array_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/bitvector_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/bitvector_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/clausal_bitvector_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/clausal_bitvector_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/clause_id.h\ /construction/math/cvc4/CVC4-1.7/src/proof/cnf_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/cnf_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/dimacs_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/dimacs_printer.h\ /construction/math/cvc4/CVC4-1.7/src/proof/drat/drat_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/drat/drat_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/er/er_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/er/er_proof.h\ /construction/math/cvc4/CVC4-1.7/src/pro--- src/base/CMakeFiles/gen-tags-debug.dir/all --- C4-1.7/src/preprocessing/passes/global_negate.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/global_negate.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/int_to_bv.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/int_to_bv.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/ite_removal.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/ite_removal.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/ite_simp.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/ite_simp.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/miplib_trick.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/miplib_trick.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/nl_ext_purify.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/nl_ext_purify.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/non_clausal_simp.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/non_clausal_simp.h\ /con--- src/base/CMakeFiles/gen-tags-trace.dir/all --- of/lemma_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/lemma_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/lfsc_proof_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/lfsc_proof_printer.h\ /construction/math/cvc4/CVC4-1.7/src/proof/lrat/lrat_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/lrat/lrat_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_manager.h\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_output_channel.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_output_channel.h\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_utils.h\ /construction/math/cvc4/CVC4-1.7/src/proof/resolution_bitvector_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/resolution_bitvector_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/sat_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/sat_proof_imp--- src/base/CMakeFiles/gen-tags-debug.dir/all --- struction/math/cvc4/CVC4-1.7/src/preprocessing/passes/pseudo_boolean_processor.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/pseudo_boolean_processor.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/quantifier_macros.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/quantifier_macros.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/quantifiers_preprocess.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/quantifiers_preprocess.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/real_to_int.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/real_to_int.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/rewrite.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/rewrite.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sep_skolem_emp.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sep_skolem_emp.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sort_infer.cpp\ /constru--- src/base/CMakeFiles/gen-tags-trace.dir/all --- lementation.h\ /construction/math/cvc4/CVC4-1.7/src/proof/simplify_boolean_node.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/simplify_boolean_node.h\ /construction/math/cvc4/CVC4-1.7/src/proof/skolemization_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/skolemization_manager.h\ /construction/math/cvc4/CVC4-1.7/src/proof/theory_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/theory_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/uf_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/uf_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/unsat_core.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/unsat_core.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bv_sat_solver_notify.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/bvminisat.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/bvminisat.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/Dimacs.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/Main.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/co--- src/base/CMakeFiles/gen-tags-debug.dir/all --- ction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sort_infer.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/static_learning.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/static_learning.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sygus_abduct.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sygus_abduct.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sygus_inference.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/sygus_inference.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/symmetry_breaker.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/symmetry_breaker.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/symmetry_detect.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/symmetry_detect.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/synth_rew_rules.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/synth_rew_rules.h\ /construction/math/cvc4/CVC4--- src/base/CMakeFiles/gen-tags-trace.dir/all --- re/Solver.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/Solver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/SolverTypes.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Alg.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Alloc.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Heap.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/IntTypes.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Map.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Queue.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Sort.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Vec.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/XAlloc.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/simp/Main.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/simp/SimpSolver.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/simp/SimpSolver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/Options.cc\ /constructi--- src/base/CMakeFiles/gen-tags-debug.dir/all --- -1.7/src/preprocessing/passes/theory_preprocess.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/theory_preprocess.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/unconstrained_simplifier.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/passes/unconstrained_simplifier.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass_context.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass_context.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass_registry.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/preprocessing_pass_registry.h\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/util/ite_utilities.cpp\ /construction/math/cvc4/CVC4-1.7/src/preprocessing/util/ite_utilities.h\ /construction/math/cvc4/CVC4-1.7/src/printer/ast/ast_printer.cpp\ /construction/math/cvc4/CV--- src/base/CMakeFiles/gen-tags-trace.dir/all --- on/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/Options.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/ParseUtils.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/System.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/System.h\ /construction/math/cvc4/CVC4-1.7/src/prop/cadical.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/cadical.h\ /construction/math/cvc4/CVC4-1.7/src/prop/cnf_stream.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/cnf_stream.h\ /construction/math/cvc4/CVC4-1.7/src/prop/cryptominisat.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/cryptominisat.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/Dimacs.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/Main.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/Solver.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/Solver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/SolverTypes.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/minisat.cpp\ /construction/math/cvc--- src/base/CMakeFiles/gen-tags-debug.dir/all --- C4-1.7/src/printer/ast/ast_printer.h\ /construction/math/cvc4/CVC4-1.7/src/printer/cvc/cvc_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/cvc/cvc_printer.h\ /construction/math/cvc4/CVC4-1.7/src/printer/dagification_visitor.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/dagification_visitor.h\ /construction/math/cvc4/CVC4-1.7/src/printer/printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/printer.h\ /construction/math/cvc4/CVC4-1.7/src/printer/smt2/smt2_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/smt2/smt2_printer.h\ /construction/math/cvc4/CVC4-1.7/src/printer/sygus_print_callback.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/sygus_print_callback.h\ /construction/math/cvc4/CVC4-1.7/src/printer/tptp/tptp_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/printer/tptp/tptp_printer.h\ /construction/math/cvc4/CVC4-1.7/src/proof/arith_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/arith_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/arith_proof_recorder.cpp\ /constr--- src/base/CMakeFiles/gen-tags-trace.dir/all --- 4/CVC4-1.7/src/prop/minisat/minisat.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Alg.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Alloc.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Heap.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/IntTypes.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Map.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Queue.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Sort.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Vec.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/XAlloc.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/simp/Main.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/simp/SimpSolver.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/simp/SimpSolver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/utils/Options.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/utils/Options.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/utils/ParseUtils.h\ /construction/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- uction/math/cvc4/CVC4-1.7/src/proof/arith_proof_recorder.h\ /construction/math/cvc4/CVC4-1.7/src/proof/array_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/array_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/bitvector_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/bitvector_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/clausal_bitvector_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/clausal_bitvector_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/clause_id.h\ /construction/math/cvc4/CVC4-1.7/src/proof/cnf_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/cnf_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/dimacs_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/dimacs_printer.h\ /construction/math/cvc4/CVC4-1.7/src/proof/drat/drat_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/drat/drat_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/er/er_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/er/er_proof.h\ /construction/math/cvc4/CVC4-1.7/src/pro--- src/base/CMakeFiles/gen-tags-trace.dir/all --- math/cvc4/CVC4-1.7/src/prop/minisat/utils/System.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/utils/System.h\ /construction/math/cvc4/CVC4-1.7/src/prop/prop_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/prop_engine.h\ /construction/math/cvc4/CVC4-1.7/src/prop/registrar.h\ /construction/math/cvc4/CVC4-1.7/src/prop/sat_solver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/sat_solver_factory.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/sat_solver_factory.h\ /construction/math/cvc4/CVC4-1.7/src/prop/sat_solver_types.h\ /construction/math/cvc4/CVC4-1.7/src/prop/theory_proxy.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/theory_proxy.h\ /construction/math/cvc4/CVC4-1.7/src/smt/command.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/command.h\ /construction/math/cvc4/CVC4-1.7/src/smt/command_list.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/command_list.h\ /construction/math/cvc4/CVC4-1.7/src/smt/dump.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/dump.h\ /construction/math/cvc4/CVC4-1.7/src/smt/logic--- src/base/CMakeFiles/gen-tags-debug.dir/all --- of/lemma_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/lemma_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/lfsc_proof_printer.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/lfsc_proof_printer.h\ /construction/math/cvc4/CVC4-1.7/src/proof/lrat/lrat_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/lrat/lrat_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_manager.h\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_output_channel.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_output_channel.h\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/proof_utils.h\ /construction/math/cvc4/CVC4-1.7/src/proof/resolution_bitvector_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/resolution_bitvector_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/sat_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/sat_proof_imp--- src/theory/CMakeFiles/gen-theory.dir/all --- /usr/bin/make -f src/theory/CMakeFiles/gen-theory.dir/build.make src/theory/CMakeFiles/gen-theory.dir/build --- src/expr/CMakeFiles/gen-expr.dir/all --- --- src/expr/metakind.h --- [ 1%] Generating metakind.h cd /construction/math/cvc4/.build/src/expr && /construction/math/cvc4/CVC4-1.7/src/expr/mkmetakind /construction/math/cvc4/CVC4-1.7/src/expr/metakind_template.h /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/expr/metakind.h --- src/base/CMakeFiles/gen-tags-trace.dir/all --- _exception.h\ /construction/math/cvc4/CVC4-1.7/src/smt/logic_request.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/logic_request.h\ /construction/math/cvc4/CVC4-1.7/src/smt/managed_ostreams.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/managed_ostreams.h\ /construction/math/cvc4/CVC4-1.7/src/smt/model.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/model.h\ /construction/math/cvc4/CVC4-1.7/src/smt/model_core_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/model_core_builder.h\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_engine.h\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_engine_scope.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_engine_scope.h\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_statistics_registry.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_statistics_registry.h\ /construction/math/cvc4/CVC4-1.7/src/smt/term_formula_removal.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/term_formula_removal.h\ /construction/math/cvc4/CVC4-1.7--- src/base/CMakeFiles/gen-tags-debug.dir/all --- lementation.h\ /construction/math/cvc4/CVC4-1.7/src/proof/simplify_boolean_node.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/simplify_boolean_node.h\ /construction/math/cvc4/CVC4-1.7/src/proof/skolemization_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/skolemization_manager.h\ /construction/math/cvc4/CVC4-1.7/src/proof/theory_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/theory_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/uf_proof.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/uf_proof.h\ /construction/math/cvc4/CVC4-1.7/src/proof/unsat_core.cpp\ /construction/math/cvc4/CVC4-1.7/src/proof/unsat_core.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bv_sat_solver_notify.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/bvminisat.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/bvminisat.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/Dimacs.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/Main.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/co--- src/base/CMakeFiles/gen-tags-trace.dir/all --- /src/smt/update_ostream.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/boolean_simplification.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt_util/boolean_simplification.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/lemma_channels.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt_util/lemma_channels.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/lemma_input_channel.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/lemma_output_channel.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/nary_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt_util/nary_builder.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/node_visitor.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/approx_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/approx_simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_ite_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_ite_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_msum.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- re/Solver.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/Solver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/SolverTypes.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Alg.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Alloc.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Heap.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/IntTypes.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Map.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Queue.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Sort.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/Vec.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/mtl/XAlloc.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/simp/Main.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/simp/SimpSolver.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/simp/SimpSolver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/Options.cc\ /constructi--- src/base/CMakeFiles/gen-tags-trace.dir/all --- arith_msum.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_static_learner.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_static_learner.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_utilities.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arithvar.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arithvar.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arithvar_node_map.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/attempt_solution_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/attempt_solution_simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/bound_counts.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/callbacks.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/callbacks.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/congruence_manager.cpp\ /construction/math/cvc4/CVC4-1--- src/base/CMakeFiles/gen-tags-debug.dir/all --- on/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/Options.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/ParseUtils.h\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/System.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/bvminisat/utils/System.h\ /construction/math/cvc4/CVC4-1.7/src/prop/cadical.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/cadical.h\ /construction/math/cvc4/CVC4-1.7/src/prop/cnf_stream.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/cnf_stream.h\ /construction/math/cvc4/CVC4-1.7/src/prop/cryptominisat.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/cryptominisat.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/Dimacs.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/Main.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/Solver.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/Solver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/core/SolverTypes.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/minisat.cpp\ /construction/math/cvc--- src/base/CMakeFiles/gen-tags-trace.dir/all --- .7/src/theory/arith/congruence_manager.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/constraint.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/constraint.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/constraint_forward.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/cut_log.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/cut_log.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/delta_rational.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/delta_rational.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/dio_solver.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/dio_solver.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/dual_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/dual_simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/error_set.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/error_set.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/fc_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/fc_simplex--- src/base/CMakeFiles/gen-tags-debug.dir/all --- 4/CVC4-1.7/src/prop/minisat/minisat.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Alg.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Alloc.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Heap.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/IntTypes.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Map.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Queue.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Sort.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/Vec.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/mtl/XAlloc.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/simp/Main.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/simp/SimpSolver.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/simp/SimpSolver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/utils/Options.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/utils/Options.h\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/utils/ParseUtils.h\ /construction/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- .h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/infer_bounds.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/infer_bounds.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/linear_equality.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/linear_equality.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/matrix.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/matrix.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/nonlinear_extension.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/nonlinear_extension.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/normal_form.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/normal_form.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/partial_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/partial_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/simplex_update.cpp\ /construction/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- math/cvc4/CVC4-1.7/src/prop/minisat/utils/System.cc\ /construction/math/cvc4/CVC4-1.7/src/prop/minisat/utils/System.h\ /construction/math/cvc4/CVC4-1.7/src/prop/prop_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/prop_engine.h\ /construction/math/cvc4/CVC4-1.7/src/prop/registrar.h\ /construction/math/cvc4/CVC4-1.7/src/prop/sat_solver.h\ /construction/math/cvc4/CVC4-1.7/src/prop/sat_solver_factory.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/sat_solver_factory.h\ /construction/math/cvc4/CVC4-1.7/src/prop/sat_solver_types.h\ /construction/math/cvc4/CVC4-1.7/src/prop/theory_proxy.cpp\ /construction/math/cvc4/CVC4-1.7/src/prop/theory_proxy.h\ /construction/math/cvc4/CVC4-1.7/src/smt/command.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/command.h\ /construction/math/cvc4/CVC4-1.7/src/smt/command_list.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/command_list.h\ /construction/math/cvc4/CVC4-1.7/src/smt/dump.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/dump.h\ /construction/math/cvc4/CVC4-1.7/src/smt/logic--- src/base/CMakeFiles/gen-tags-trace.dir/all --- math/cvc4/CVC4-1.7/src/theory/arith/simplex_update.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/soi_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/soi_simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/tableau.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/tableau.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/tableau_sizes.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/tableau_sizes.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith_private.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith_private.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith_private_forward.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/array_info.cpp\--- src/base/CMakeFiles/gen-tags-debug.dir/all --- _exception.h\ /construction/math/cvc4/CVC4-1.7/src/smt/logic_request.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/logic_request.h\ /construction/math/cvc4/CVC4-1.7/src/smt/managed_ostreams.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/managed_ostreams.h\ /construction/math/cvc4/CVC4-1.7/src/smt/model.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/model.h\ /construction/math/cvc4/CVC4-1.7/src/smt/model_core_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/model_core_builder.h\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_engine.h\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_engine_scope.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_engine_scope.h\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_statistics_registry.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/smt_statistics_registry.h\ /construction/math/cvc4/CVC4-1.7/src/smt/term_formula_removal.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt/term_formula_removal.h\ /construction/math/cvc4/CVC4-1.7--- src/base/CMakeFiles/gen-tags-trace.dir/all --- /construction/math/cvc4/CVC4-1.7/src/theory/arrays/array_info.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/array_proof_reconstruction.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/array_proof_reconstruction.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/static_fact_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/static_fact_manager.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/union_find.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/union_find.h\ /construction/math/cvc4/CVC4-1.7/src/theory/assertion.cpp\ /construct--- src/base/CMakeFiles/gen-tags-debug.dir/all --- /src/smt/update_ostream.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/boolean_simplification.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt_util/boolean_simplification.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/lemma_channels.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt_util/lemma_channels.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/lemma_input_channel.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/lemma_output_channel.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/nary_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/smt_util/nary_builder.h\ /construction/math/cvc4/CVC4-1.7/src/smt_util/node_visitor.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/approx_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/approx_simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_ite_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_ite_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_msum.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- ion/math/cvc4/CVC4-1.7/src/theory/assertion.h\ /construction/math/cvc4/CVC4-1.7/src/theory/atom_requests.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/atom_requests.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/circuit_propagator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/circuit_propagator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/theory_builtin.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/theory_builtin.h\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/theory_builtin_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- arith_msum.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_static_learner.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_static_learner.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arith_utilities.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arithvar.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arithvar.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/arithvar_node_map.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/attempt_solution_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/attempt_solution_simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/bound_counts.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/callbacks.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/callbacks.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/congruence_manager.cpp\ /construction/math/cvc4/CVC4-1--- src/base/CMakeFiles/gen-tags-trace.dir/all --- src/theory/builtin/theory_builtin_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/theory_builtin_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/type_enumerator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/abstraction.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/abstraction.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/aig_bitblaster.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/aig_bitblaster.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/bitblast_strategies_template.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/bitblast_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/bitblaster.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/eager_bitblaster.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/eager_bitblaster.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/lazy_bitblaster.cpp\ /construction/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- .7/src/theory/arith/congruence_manager.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/constraint.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/constraint.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/constraint_forward.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/cut_log.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/cut_log.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/delta_rational.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/delta_rational.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/dio_solver.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/dio_solver.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/dual_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/dual_simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/error_set.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/error_set.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/fc_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/fc_simplex--- src/base/CMakeFiles/gen-tags-trace.dir/all --- math/cvc4/CVC4-1.7/src/theory/bv/bitblast/lazy_bitblaster.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_eager_solver.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_eager_solver.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_inequality_graph.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_inequality_graph.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_quick_check.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_quick_check.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_algebraic.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_algebraic.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_bitblast.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_bitblast.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_core.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_core.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_--- src/base/CMakeFiles/gen-tags-debug.dir/all --- .h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/infer_bounds.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/infer_bounds.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/linear_equality.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/linear_equality.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/matrix.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/matrix.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/nonlinear_extension.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/nonlinear_extension.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/normal_form.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/normal_form.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/partial_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/partial_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/simplex_update.cpp\ /construction/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- inequality.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_inequality.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/slicer.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/slicer.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_core.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_normalization.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_simplification.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- math/cvc4/CVC4-1.7/src/theory/arith/simplex_update.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/soi_simplex.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/soi_simplex.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/tableau.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/tableau.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/tableau_sizes.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/tableau_sizes.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith_private.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith_private.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith_private_forward.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/theory_arith_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arith/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/array_info.cpp\--- src/base/CMakeFiles/gen-tags-trace.dir/all --- theory/bv/theory_bv_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/care_graph.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/datatypes_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/datatypes_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/datatypes_sygus.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/datatypes_sygus.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/sygus_simple_sym.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/sygus_simple_sym.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/theory_datatypes.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/theory_datatypes.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/theory_datatypes_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/d--- src/base/CMakeFiles/gen-tags-debug.dir/all --- /construction/math/cvc4/CVC4-1.7/src/theory/arrays/array_info.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/array_proof_reconstruction.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/array_proof_reconstruction.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/static_fact_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/static_fact_manager.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/theory_arrays_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/union_find.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/arrays/union_find.h\ /construction/math/cvc4/CVC4-1.7/src/theory/assertion.cpp\ /construct--- src/base/CMakeFiles/gen-tags-trace.dir/all --- atatypes/type_enumerator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/decision_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/decision_manager.h\ /construction/math/cvc4/CVC4-1.7/src/theory/decision_strategy.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/decision_strategy.h\ /construction/math/cvc4/CVC4-1.7/src/theory/evaluator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/evaluator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/example/ecdata.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/example/ecdata.h\ /construction/math/cvc4/CVC4-1.7/src/theory/example/theory_uf_tim.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/example/theory_uf_tim.h\ /construction/math/cvc4/CVC4-1.7/src/theory/ext_theory.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/ext_theory.h\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/fp_converter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/fp_converter.h\ /construction/math/cvc4/CVC4-1.--- src/base/CMakeFiles/gen-tags-debug.dir/all --- ion/math/cvc4/CVC4-1.7/src/theory/assertion.h\ /construction/math/cvc4/CVC4-1.7/src/theory/atom_requests.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/atom_requests.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/circuit_propagator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/circuit_propagator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/theory_bool_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/booleans/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/theory_builtin.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/theory_builtin.h\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/theory_builtin_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- 7/src/theory/fp/theory_fp.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/theory_fp.h\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/theory_fp_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/theory_fp_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/theory_fp_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_assertion.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_assertion.h\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_assertion_db.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_assertion_db.h\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/theory_idl.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/theory_idl.h\ /construction/math/cvc4/CVC4-1.7/src/theory/interrupted.h\ /construction/math/cvc4/CVC4-1.7/src/theory/logic_info.cpp\ /construction/mat--- src/base/CMakeFiles/gen-tags-debug.dir/all --- src/theory/builtin/theory_builtin_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/theory_builtin_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/type_enumerator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/builtin/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/abstraction.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/abstraction.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/aig_bitblaster.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/aig_bitblaster.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/bitblast_strategies_template.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/bitblast_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/bitblaster.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/eager_bitblaster.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/eager_bitblaster.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/lazy_bitblaster.cpp\ /construction/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- h/cvc4/CVC4-1.7/src/theory/logic_info.h\ /construction/math/cvc4/CVC4-1.7/src/theory/output_channel.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/alpha_equivalence.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/alpha_equivalence.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/anti_skolem.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/anti_skolem.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/bv_inverter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/bv_inverter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/bv_inverter_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/bv_inverter_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_database.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_database.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_filter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/candi--- src/base/CMakeFiles/gen-tags-debug.dir/all --- math/cvc4/CVC4-1.7/src/theory/bv/bitblast/lazy_bitblaster.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_eager_solver.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_eager_solver.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_inequality_graph.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_inequality_graph.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_quick_check.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_quick_check.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_algebraic.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_algebraic.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_bitblast.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_bitblast.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_core.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_core.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_--- src/base/CMakeFiles/gen-tags-trace.dir/all --- date_rewrite_filter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- inequality.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/bv_subtheory_inequality.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/slicer.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/slicer.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_core.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_normalization.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewrite_rules_simplification.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- theory/quantifiers/cegqi/ceg_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/conjecture_generator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/conjecture_generator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/dynamic_rewrite.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/dynamic_rewrite.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/candidate_generator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/candidate_generator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ho_trigger.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ho_trigger.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/inst_match_generator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ema--- src/base/CMakeFiles/gen-tags-debug.dir/all --- theory/bv/theory_bv_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/theory_bv_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/bv/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/care_graph.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/datatypes_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/datatypes_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/datatypes_sygus.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/datatypes_sygus.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/sygus_simple_sym.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/sygus_simple_sym.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/theory_datatypes.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/theory_datatypes.h\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/theory_datatypes_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/d--- src/base/CMakeFiles/gen-tags-trace.dir/all --- tching/inst_match_generator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/inst_strategy_e_matching.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/instantiation_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/instantiation_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/trigger.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/trigger.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/equality_infer.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/equality_infer.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/equality_query.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/equality_query.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/expr_miner.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/expr_miner.h\ /construction/math/cvc4--- src/base/CMakeFiles/gen-tags-debug.dir/all --- atatypes/type_enumerator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/decision_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/decision_manager.h\ /construction/math/cvc4/CVC4-1.7/src/theory/decision_strategy.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/decision_strategy.h\ /construction/math/cvc4/CVC4-1.7/src/theory/evaluator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/evaluator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/example/ecdata.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/example/ecdata.h\ /construction/math/cvc4/CVC4-1.7/src/theory/example/theory_uf_tim.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/example/theory_uf_tim.h\ /construction/math/cvc4/CVC4-1.7/src/theory/ext_theory.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/ext_theory.h\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/fp_converter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/fp_converter.h\ /construction/math/cvc4/CVC4-1.--- src/base/CMakeFiles/gen-tags-trace.dir/all --- /CVC4-1.7/src/theory/quantifiers/expr_miner_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/expr_miner_manager.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/extended_rewrite.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/extended_rewrite.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/first_order_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/first_order_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/bounded_integers.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/bounded_integers.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/full_model_check.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/full_model_check.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/model_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/model_builder.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/model_engine.cpp\ /construction/math/cv--- src/base/CMakeFiles/gen-tags-debug.dir/all --- 7/src/theory/fp/theory_fp.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/theory_fp.h\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/theory_fp_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/theory_fp_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/theory_fp_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/fp/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_assertion.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_assertion.h\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_assertion_db.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_assertion_db.h\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/idl_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/theory_idl.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/idl/theory_idl.h\ /construction/math/cvc4/CVC4-1.7/src/theory/interrupted.h\ /construction/math/cvc4/CVC4-1.7/src/theory/logic_info.cpp\ /construction/mat--- src/base/CMakeFiles/gen-tags-trace.dir/all --- c4/CVC4-1.7/src/theory/quantifiers/fmf/model_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fun_def_process.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fun_def_process.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_match.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_match.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_match_trie.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_match_trie.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_propagator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_propagator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_strategy_enumerative.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_strategy_enumerative.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/instantiate.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/instantiate.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers--- src/base/CMakeFiles/gen-tags-debug.dir/all --- h/cvc4/CVC4-1.7/src/theory/logic_info.h\ /construction/math/cvc4/CVC4-1.7/src/theory/output_channel.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/alpha_equivalence.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/alpha_equivalence.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/anti_skolem.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/anti_skolem.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/bv_inverter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/bv_inverter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/bv_inverter_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/bv_inverter_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_database.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_database.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/candidate_rewrite_filter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/candi--- src/base/CMakeFiles/gen-tags-trace.dir/all --- /lazy_trie.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/lazy_trie.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/local_theory_ext.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/local_theory_ext.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_conflict_find.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_conflict_find.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_epr.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_epr.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_relevance.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_relevance.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_split.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_split.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_util.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_util.h\ /construction/math/cvc4/CVC4-1.7/src/theory/qua--- src/base/CMakeFiles/gen-tags-debug.dir/all --- date_rewrite_filter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ceg_instantiator.cpp\ /construction/math/cvc4/CVC4-1.7/src/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- ntifiers/quantifiers_attributes.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quantifiers_attributes.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quantifiers_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quantifiers_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/query_generator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/query_generator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/relevant_domain.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/relevant_domain.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/rewrite_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/rewrite_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/single_inv_partition.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/single_inv_partition.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/skolemize.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/--- src/base/CMakeFiles/gen-tags-debug.dir/all --- theory/quantifiers/cegqi/ceg_instantiator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/conjecture_generator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/conjecture_generator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/dynamic_rewrite.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/dynamic_rewrite.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/candidate_generator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/candidate_generator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ho_trigger.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ho_trigger.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/inst_match_generator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ema--- src/base/CMakeFiles/gen-tags-trace.dir/all --- skolemize.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/solution_filter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/solution_filter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/cegis.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/cegis.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/cegis_unif.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/cegis_unif.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/enum_stream_substitution.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/enum_stream_substitution.h\ /construction/math/cvc4--- src/base/CMakeFiles/gen-tags-debug.dir/all --- tching/inst_match_generator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/inst_strategy_e_matching.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/instantiation_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/instantiation_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/trigger.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/trigger.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/equality_infer.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/equality_infer.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/equality_query.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/equality_query.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/expr_miner.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/expr_miner.h\ /construction/math/cvc4--- src/base/CMakeFiles/gen-tags-trace.dir/all --- /CVC4-1.7/src/theory/quantifiers/sygus/sygus_enumerator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_eval_unfold.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_explain.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_explain.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_cons.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_norm.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_red.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_red.h\ /construction/math/cvc4/CVC4-1.7/src/theory/q--- src/base/CMakeFiles/gen-tags-debug.dir/all --- /CVC4-1.7/src/theory/quantifiers/expr_miner_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/expr_miner_manager.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/extended_rewrite.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/extended_rewrite.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/first_order_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/first_order_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/bounded_integers.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/bounded_integers.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/full_model_check.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/full_model_check.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/model_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/model_builder.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/model_engine.cpp\ /construction/math/cv--- src/base/CMakeFiles/gen-tags-trace.dir/all --- uantifiers/sygus/sygus_invariance.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_invariance.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_module.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_module.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_pbe.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_pbe.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_process_conj.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_process_conj.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_repair_const.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_repair_const.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_io.cpp\ /construction/math--- src/base/CMakeFiles/gen-tags-debug.dir/all --- c4/CVC4-1.7/src/theory/quantifiers/fmf/model_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fun_def_process.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/fun_def_process.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_match.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_match.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_match_trie.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_match_trie.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_propagator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_propagator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_strategy_enumerative.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/inst_strategy_enumerative.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/instantiate.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/instantiate.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers--- src/base/CMakeFiles/gen-tags-trace.dir/all --- /cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_io.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_rl.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_rl.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_strat.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_strat.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/synth_conjecture.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/synth_conjecture.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/synth_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/synth_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/term_database_sygus.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/term_database_sygus.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus_sampler.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus_samp--- src/base/CMakeFiles/gen-tags-debug.dir/all --- /lazy_trie.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/lazy_trie.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/local_theory_ext.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/local_theory_ext.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_conflict_find.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_conflict_find.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_epr.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_epr.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_relevance.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_relevance.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_split.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_split.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_util.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quant_util.h\ /construction/math/cvc4/CVC4-1.7/src/theory/qua--- src/base/CMakeFiles/gen-tags-trace.dir/all --- ler.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_canonize.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_canonize.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_database.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_database.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_enumeration.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_enumeration.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_util.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_util.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/theory_quantifiers.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/theory_quantifiers.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/theory_quantifiers_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/re--- src/base/CMakeFiles/gen-tags-debug.dir/all --- ntifiers/quantifiers_attributes.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quantifiers_attributes.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quantifiers_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/quantifiers_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/query_generator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/query_generator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/relevant_domain.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/relevant_domain.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/rewrite_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/rewrite_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/single_inv_partition.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/single_inv_partition.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/skolemize.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/--- src/base/CMakeFiles/gen-tags-trace.dir/all --- p_set.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/rep_set.h\ /construction/math/cvc4/CVC4-1.7/src/theory/rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/rewriter_attributes.h\ /construction/math/cvc4/CVC4-1.7/src/theory/rewriter_tables_template.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/normal_form.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/rels_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_private.cpp\ /construction/math/cvc4/CVC4-1.--- src/base/CMakeFiles/gen-tags-debug.dir/all --- skolemize.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/solution_filter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/solution_filter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/cegis.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/cegis.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/cegis_unif.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/cegis_unif.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/enum_stream_substitution.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/enum_stream_substitution.h\ /construction/math/cvc4--- src/base/CMakeFiles/gen-tags-trace.dir/all --- 7/src/theory/sets/theory_sets_private.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_rels.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_rels.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/shared_terms_database.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/shared_terms_database.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sort_inference.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sort_inference.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_elim.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_elim.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_operation.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_opera--- src/base/CMakeFiles/gen-tags-debug.dir/all --- /CVC4-1.7/src/theory/quantifiers/sygus/sygus_enumerator.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_eval_unfold.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_explain.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_explain.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_cons.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_norm.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_red.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_grammar_red.h\ /construction/math/cvc4/CVC4-1.7/src/theory/q--- src/base/CMakeFiles/gen-tags-trace.dir/all --- tion.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_solver.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_solver.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/skolem_cache.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/skolem_cache.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_preprocess.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_preprocess.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/subs_minimize.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/subs_minimize--- src/base/CMakeFiles/gen-tags-debug.dir/all --- uantifiers/sygus/sygus_invariance.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_invariance.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_module.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_module.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_pbe.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_pbe.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_process_conj.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_process_conj.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_repair_const.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_repair_const.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_io.cpp\ /construction/math--- src/base/CMakeFiles/gen-tags-trace.dir/all --- .h\ /construction/math/cvc4/CVC4-1.7/src/theory/substitutions.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/substitutions.h\ /construction/math/cvc4/CVC4-1.7/src/theory/term_registration_visitor.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/term_registration_visitor.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/theory.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_model_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_model_builder.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_registrar.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_test_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_traits_template.h\ /construction/math/cvc4/CVC4-1.7/src/theory/type_enumer--- src/base/CMakeFiles/gen-tags-debug.dir/all --- /cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_io.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_rl.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_rl.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_strat.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/sygus_unif_strat.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/synth_conjecture.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/synth_conjecture.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/synth_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/synth_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/term_database_sygus.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/term_database_sygus.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus_sampler.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus_samp--- src/base/CMakeFiles/gen-tags-trace.dir/all --- ator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/type_enumerator_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/type_set.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/type_set.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/equality_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/equality_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/equality_engine_types.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/symmetry_breaker.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/symmetry_breaker.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_strong_solver.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_strong_solver.h\ /constructi--- src/base/CMakeFiles/gen-tags-debug.dir/all --- ler.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_canonize.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_canonize.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_database.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_database.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_enumeration.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_enumeration.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_util.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/term_util.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/theory_quantifiers.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/theory_quantifiers.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/theory_quantifiers_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/re--- src/base/CMakeFiles/gen-tags-trace.dir/all --- on/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/valuation.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/valuation.h\ /construction/math/cvc4/CVC4-1.7/src/util/abstract_value.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/abstract_value.h\ /construction/math/cvc4/CVC4-1.7/src/util/bin_heap.h\ /construction/math/cvc4/CVC4-1.7/src/util/bitvector.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/bitvector.h\ /construction/math/cvc4/CVC4-1.7/src/util/bool.h\ /construction/math/cvc4/CVC4-1.7/src/util/cardinality.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/cardinality.h\ /construction/math/cvc4/CVC4-1.7/src/util/channel.h\ /construction/math/cvc4/CVC4-1.7/src/util/debug.h\ /construction/math/cvc4/CVC4-1.7/src/util/dense_map.h\ /construction/math/cvc4/CVC4-1.7/src/util/divisible.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/divisible.h\ /construction/math/cvc4/CVC4-1.7/src/util/floatingpoint.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/gmp_util.h\ /constru--- src/base/CMakeFiles/gen-tags-debug.dir/all --- p_set.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/rep_set.h\ /construction/math/cvc4/CVC4-1.7/src/theory/rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/rewriter_attributes.h\ /construction/math/cvc4/CVC4-1.7/src/theory/rewriter_tables_template.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sep/theory_sep_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/normal_form.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/rels_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_private.cpp\ /construction/math/cvc4/CVC4-1.--- src/base/CMakeFiles/gen-tags-trace.dir/all --- ction/math/cvc4/CVC4-1.7/src/util/hash.h\ /construction/math/cvc4/CVC4-1.7/src/util/index.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/index.h\ /construction/math/cvc4/CVC4-1.7/src/util/integer_cln_imp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/integer_cln_imp.h\ /construction/math/cvc4/CVC4-1.7/src/util/integer_gmp_imp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/integer_gmp_imp.h\ /construction/math/cvc4/CVC4-1.7/src/util/maybe.h\ /construction/math/cvc4/CVC4-1.7/src/util/ostream_util.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/ostream_util.h\ /construction/math/cvc4/CVC4-1.7/src/util/proof.h\ /construction/math/cvc4/CVC4-1.7/src/util/random.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/random.h\ /construction/math/cvc4/CVC4-1.7/src/util/rational_cln_imp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/rational_cln_imp.h\ /construction/math/cvc4/CVC4-1.7/src/util/rational_gmp_imp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/rational_gmp_imp.h\ /construction/math/cvc4/CVC4-1.7/src/util/regexp.cpp--- src/base/CMakeFiles/gen-tags-debug.dir/all --- 7/src/theory/sets/theory_sets_private.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_rels.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_rels.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sets/theory_sets_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/shared_terms_database.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/shared_terms_database.h\ /construction/math/cvc4/CVC4-1.7/src/theory/sort_inference.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/sort_inference.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_elim.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_elim.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_operation.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_opera--- src/base/CMakeFiles/gen-tags-trace.dir/all --- \ /construction/math/cvc4/CVC4-1.7/src/util/regexp.h\ /construction/math/cvc4/CVC4-1.7/src/util/resource_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/resource_manager.h\ /construction/math/cvc4/CVC4-1.7/src/util/result.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/result.h\ /construction/math/cvc4/CVC4-1.7/src/util/safe_print.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/safe_print.h\ /construction/math/cvc4/CVC4-1.7/src/util/sampler.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/sampler.h\ /construction/math/cvc4/CVC4-1.7/src/util/sexpr.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/sexpr.h\ /construction/math/cvc4/CVC4-1.7/src/util/smt2_quote_string.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/smt2_quote_string.h\ /construction/math/cvc4/CVC4-1.7/src/util/statistics.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/statistics.h\ /construction/math/cvc4/CVC4-1.7/src/util/statistics_registry.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/statistics_registry.h\ /construction/math/cvc4/CVC4-1.7/src/u--- src/base/CMakeFiles/gen-tags-debug.dir/all --- tion.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_solver.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/regexp_solver.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/skolem_cache.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/skolem_cache.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_preprocess.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_preprocess.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_rewriter.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/theory_strings_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/strings/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/subs_minimize.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/subs_minimize--- src/base/CMakeFiles/gen-tags-trace.dir/all --- til/tuple.h\ /construction/math/cvc4/CVC4-1.7/src/util/unsafe_interrupt_exception.h\ /construction/math/cvc4/CVC4-1.7/src/util/utility.h --- src/base/CMakeFiles/gen-tags-debug.dir/all --- .h\ /construction/math/cvc4/CVC4-1.7/src/theory/substitutions.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/substitutions.h\ /construction/math/cvc4/CVC4-1.7/src/theory/term_registration_visitor.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/term_registration_visitor.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/theory.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_model_builder.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_model_builder.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_registrar.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_test_utils.h\ /construction/math/cvc4/CVC4-1.7/src/theory/theory_traits_template.h\ /construction/math/cvc4/CVC4-1.7/src/theory/type_enumerator.h\ /construction/math/cvc4/CVC4-1.7/src/theory/type_enumerator_template.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/type_set.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/type_set.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/equality_engine.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/equality_engine.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/equality_engine_types.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/symmetry_breaker.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/symmetry_breaker.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_model.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_model.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_rewriter.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_strong_solver.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_strong_solver.h\ /construction/math/cvc4/CVC4-1.7/src/theory/uf/theory_uf_type_rules.h\ /construction/math/cvc4/CVC4-1.7/src/theory/valuation.cpp\ /construction/math/cvc4/CVC4-1.7/src/theory/valuation.h\ /construction/math/cvc4/CVC4-1.7/src/util/abstract_value.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/abstract_value.h\ /construction/math/cvc4/CVC4-1.7/src/util/bin_heap.h\ /construction/math/cvc4/CVC4-1.7/src/util/bitvector.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/bitvector.h\ /construction/math/cvc4/CVC4-1.7/src/util/bool.h\ /construction/math/cvc4/CVC4-1.7/src/util/cardinality.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/cardinality.h\ /construction/math/cvc4/CVC4-1.7/src/util/channel.h\ /construction/math/cvc4/CVC4-1.7/src/util/debug.h\ /construction/math/cvc4/CVC4-1.7/src/util/dense_map.h\ /construction/math/cvc4/CVC4-1.7/src/util/divisible.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/divisible.h\ /construction/math/cvc4/CVC4-1.7/src/util/floatingpoint.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/gmp_util.h\ /construction/math/cvc4/CVC4-1.7/src/util/hash.h\ /construction/math/cvc4/CVC4-1.7/src/util/index.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/index.h\ /construction/math/cvc4/CVC4-1.7/src/util/integer_cln_imp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/integer_cln_imp.h\ /construction/math/cvc4/CVC4-1.7/src/util/integer_gmp_imp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/integer_gmp_imp.h\ /construction/math/cvc4/CVC4-1.7/src/util/maybe.h\ /construction/math/cvc4/CVC4-1.7/src/util/ostream_util.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/ostream_util.h\ /construction/math/cvc4/CVC4-1.7/src/util/proof.h\ /construction/math/cvc4/CVC4-1.7/src/util/random.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/random.h\ /construction/math/cvc4/CVC4-1.7/src/util/rational_cln_imp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/rational_cln_imp.h\ /construction/math/cvc4/CVC4-1.7/src/util/rational_gmp_imp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/rational_gmp_imp.h\ /construction/math/cvc4/CVC4-1.7/src/util/regexp.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/regexp.h\ /construction/math/cvc4/CVC4-1.7/src/util/resource_manager.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/resource_manager.h\ /construction/math/cvc4/CVC4-1.7/src/util/result.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/result.h\ /construction/math/cvc4/CVC4-1.7/src/util/safe_print.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/safe_print.h\ /construction/math/cvc4/CVC4-1.7/src/util/sampler.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/sampler.h\ /construction/math/cvc4/CVC4-1.7/src/util/sexpr.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/sexpr.h\ /construction/math/cvc4/CVC4-1.7/src/util/smt2_quote_string.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/smt2_quote_string.h\ /construction/math/cvc4/CVC4-1.7/src/util/statistics.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/statistics.h\ /construction/math/cvc4/CVC4-1.7/src/util/statistics_registry.cpp\ /construction/math/cvc4/CVC4-1.7/src/util/statistics_registry.h\ /construction/math/cvc4/CVC4-1.7/src/util/tuple.h\ /construction/math/cvc4/CVC4-1.7/src/util/unsafe_interrupt_exception.h\ /construction/math/cvc4/CVC4-1.7/src/util/utility.h --- src/main/CMakeFiles/gen-tokens.dir/all --- /usr/bin/make -f src/main/CMakeFiles/gen-tokens.dir/build.make src/main/CMakeFiles/gen-tokens.dir/build --- src/main/cvc_tokens.h --- --- src/main/smt1_tokens.h --- --- src/main/smt2_tokens.h --- --- src/main/tptp_tokens.h --- --- src/main/smt2_tokens.h --- [ 1%] Generating smt2_tokens.h cd /construction/math/cvc4/.build/src/main && sh /construction/math/cvc4/CVC4-1.7/src/main/gen-token-header.sh /construction/math/cvc4/CVC4-1.7/src/main/../parser/smt2/Smt2.g /construction/math/cvc4/.build/src/main/smt2_tokens.h --- src/main/cvc_tokens.h --- [ 1%] Generating cvc_tokens.h --- src/main/smt1_tokens.h --- [ 1%] Generating smt1_tokens.h --- src/main/cvc_tokens.h --- cd /construction/math/cvc4/.build/src/main && sh /construction/math/cvc4/CVC4-1.7/src/main/gen-token-header.sh /construction/math/cvc4/CVC4-1.7/src/main/../parser/cvc/Cvc.g /construction/math/cvc4/.build/src/main/cvc_tokens.h --- src/main/smt1_tokens.h --- cd /construction/math/cvc4/.build/src/main && sh /construction/math/cvc4/CVC4-1.7/src/main/gen-token-header.sh /construction/math/cvc4/CVC4-1.7/src/main/../parser/smt1/Smt1.g /construction/math/cvc4/.build/src/main/smt1_tokens.h --- src/base/CMakeFiles/gen-tags-debug.dir/all --- [ 1%] Built target gen-tags-debug --- src/main/CMakeFiles/gen-tokens.dir/all --- --- src/main/tptp_tokens.h --- [ 2%] Generating tptp_tokens.h cd /construction/math/cvc4/.build/src/main && sh /construction/math/cvc4/CVC4-1.7/src/main/gen-token-header.sh /construction/math/cvc4/CVC4-1.7/src/main/../parser/tptp/Tptp.g /construction/math/cvc4/.build/src/main/tptp_tokens.h --- src/theory/CMakeFiles/gen-theory.dir/all --- --- src/theory/rewriter_tables.h --- --- src/theory/theory_traits.h --- --- src/theory/type_enumerator.cpp --- --- src/theory/rewriter_tables.h --- [ 3%] Generating rewriter_tables.h cd /construction/math/cvc4/.build/src/theory && /construction/math/cvc4/CVC4-1.7/src/theory/mkrewriter /construction/math/cvc4/CVC4-1.7/src/theory/rewriter_tables_template.h /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/theory/rewriter_tables.h --- src/theory/theory_traits.h --- [ 3%] Generating theory_traits.h cd /construction/math/cvc4/.build/src/theory && /construction/math/cvc4/CVC4-1.7/src/theory/mktheorytraits /construction/math/cvc4/CVC4-1.7/src/theory/theory_traits_template.h /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/theory/theory_traits.h --- src/theory/type_enumerator.cpp --- [ 3%] Generating type_enumerator.cpp cd /construction/math/cvc4/.build/src/theory && /construction/math/cvc4/CVC4-1.7/src/theory/mktheorytraits /construction/math/cvc4/CVC4-1.7/src/theory/type_enumerator_template.cpp /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/theory/type_enumerator.cpp --- src/main/CMakeFiles/gen-tokens.dir/all --- [ 3%] Built target gen-tokens --- src/base/CMakeFiles/gen-tags-trace.dir/all --- [ 3%] Built target gen-tags-trace --- src/base/CMakeFiles/gen-tags.dir/all --- /usr/bin/make -f src/base/CMakeFiles/gen-tags.dir/build.make src/base/CMakeFiles/gen-tags.dir/depend --- src/base/CMakeFiles/gen-tags.dir/depend --- cd /construction/math/cvc4/.build && /usr/local/bin/cmake -E cmake_depends "Unix Makefiles" /construction/math/cvc4/CVC4-1.7 /construction/math/cvc4/CVC4-1.7/src/base /construction/math/cvc4/.build /construction/math/cvc4/.build/src/base /construction/math/cvc4/.build/src/base/CMakeFiles/gen-tags.dir/DependInfo.cmake /usr/bin/make -f src/base/CMakeFiles/gen-tags.dir/build.make src/base/CMakeFiles/gen-tags.dir/build --- src/base/Debug_tags --- --- src/base/Trace_tags --- --- src/options/CMakeFiles/gen-options.dir/all --- [ 3%] Built target gen-options --- src/base/CMakeFiles/gen-tags.dir/all --- --- src/base/Debug_tags --- [ 3%] Generating Debug_tags cd /construction/math/cvc4/.build/src/base && /construction/math/cvc4/CVC4-1.7/src/base/gentags.sh Debug --- src/base/Debug_tags.h --- --- src/base/Trace_tags --- [ 3%] Generating Trace_tags cd /construction/math/cvc4/.build/src/base && /construction/math/cvc4/CVC4-1.7/src/base/gentags.sh Trace --- src/base/Debug_tags.h --- [ 3%] Generating Debug_tags.h cd /construction/math/cvc4/.build/src/base && /construction/math/cvc4/CVC4-1.7/src/base/genheader.sh /construction/math/cvc4/CVC4-1.7/src/base Debug --- src/base/Trace_tags.h --- [ 3%] Generating Trace_tags.h cd /construction/math/cvc4/.build/src/base && /construction/math/cvc4/CVC4-1.7/src/base/genheader.sh /construction/math/cvc4/CVC4-1.7/src/base Trace [ 3%] Built target gen-tags --- src/expr/CMakeFiles/gen-expr.dir/all --- --- src/expr/expr.h --- --- src/expr/kind.cpp --- --- src/expr/expr.h --- [ 3%] Generating expr.h cd /construction/math/cvc4/.build/src/expr && /construction/math/cvc4/CVC4-1.7/src/expr/mkexpr /construction/math/cvc4/CVC4-1.7/src/expr/expr_template.h /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/expr/expr.h --- src/expr/kind.cpp --- [ 4%] Generating kind.cpp cd /construction/math/cvc4/.build/src/expr && /construction/math/cvc4/CVC4-1.7/src/expr/mkkind /construction/math/cvc4/CVC4-1.7/src/expr/kind_template.cpp /construction/math/cvc4/CVC4-1.7/src/theory/builtin/kinds /construction/math/cvc4/CVC4-1.7/src/theory/booleans/kinds /construction/math/cvc4/CVC4-1.7/src/theory/uf/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arith/kinds /construction/math/cvc4/CVC4-1.7/src/theory/bv/kinds /construction/math/cvc4/CVC4-1.7/src/theory/fp/kinds /construction/math/cvc4/CVC4-1.7/src/theory/arrays/kinds /construction/math/cvc4/CVC4-1.7/src/theory/datatypes/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sep/kinds /construction/math/cvc4/CVC4-1.7/src/theory/sets/kinds /construction/math/cvc4/CVC4-1.7/src/theory/strings/kinds /construction/math/cvc4/CVC4-1.7/src/theory/quantifiers/kinds /construction/math/cvc4/CVC4-1.7/src/theory/idl/kinds > /construction/math/cvc4/.build/src/expr/kind.cpp --- src/theory/CMakeFiles/gen-theory.dir/all --- [ 4%] Built target gen-theory --- src/expr/CMakeFiles/gen-expr.dir/all --- --- src/expr/expr.h --- /construction/math/cvc4/CVC4-1.7/src/expr/expr_template.h:0: error: undefined replacement ${getConst_instantiations} *** [src/expr/expr.h] Error code 1 make[3]: *** src/expr/expr.h removed make[3]: stopped in /construction/math/cvc4/.build --- src/expr/metakind.h --- /construction/math/cvc4/CVC4-1.7/src/expr/metakind_template.h:0: error: undefined replacement ${metakind_getConst_decls} *** [src/expr/metakind.h] Error code 1 make[3]: *** src/expr/metakind.h removed make[3]: stopped in /construction/math/cvc4/.build 2 errors make[3]: stopped in /construction/math/cvc4/.build *** [src/expr/CMakeFiles/gen-expr.dir/all] Error code 2 make[2]: stopped in /construction/math/cvc4/.build 1 error make[2]: stopped in /construction/math/cvc4/.build *** [all] Error code 2 make[1]: stopped in /construction/math/cvc4/.build 1 error make[1]: stopped in /construction/math/cvc4/.build ===> Compilation failed unexpectedly. Try to set MAKE_JOBS_UNSAFE=yes and rebuild before reporting the failure to the maintainer. *** Error code 1 Stop. make: stopped in /xports/math/cvc4 FAILED 00:00:03