Merge branch 'main' into leanPrinter

Author: HanielB

.github/actions/install-dependencies/action.yml

@@ -30,7 +30,7 @@ runs:
           flex \
           libfl-dev \
           flexc++
-        python3 -m pip install pexpect setuptools toml
+        python3 -m pip install --user pexpect setuptools toml
         # Make ImageVersion accessible as env.image_version. Environment
         # variables of the runner are not automatically imported:
         #
@@ -73,7 +73,7 @@ runs:
           pkgconfig \
           flex \
           gnu-sed
-        python3 -m pip install pexpect setuptools toml
+        python3 -m pip install --user pexpect setuptools toml
         # Make ImageVersion accessible as env.image_version. Environment
         # variables of the runner are not automatically imported:
         #
@@ -91,9 +91,10 @@ runs:
       run: |
         echo "::group::Install software for Python bindings"
         python3 -m pip install -q --upgrade pip
-        python3 -m pip install pytest scikit-build
+        python3 -m pip install --user pytest scikit-build
         python3 -m pytest --version
-        python3 -m pip install Cython==0.29.*
+        python3 -m pip install --user Cython==0.29.*
+        # Add binary path of user site-packages to PATH
         echo "$(python3 -m site --user-base)/bin" >> $GITHUB_PATH
         echo "::endgroup::"
 
@@ -103,8 +104,8 @@ runs:
       run: |
         echo "::group::Install software for Python packaging"
         python3 -m pip install -q --upgrade pip
-        python3 -m pip install twine
-        python3 -m pip install -U urllib3 requests
+        python3 -m pip install --user twine
+        python3 -m pip install --user -U urllib3 requests
         echo "::endgroup::"
     
     - name: Install software for documentation
@@ -113,7 +114,7 @@ runs:
       run: |
         echo "::group::Install software for documentation"
         sudo apt-get install -y doxygen python3-docutils python3-jinja2
-        python3 -m pip install \
+        python3 -m pip install --user \
           sphinxcontrib-bibtex sphinx-tabs sphinx-rtd-theme breathe \
           sphinxcontrib-programoutput
         echo "::endgroup::"

.github/workflows/docs_upload.yml

@@ -80,6 +80,28 @@ jobs:
           echo "HASH=$HASH" >> $GITHUB_ENV
           echo "ISRELEASE=$ISRELEASE" >> $GITHUB_ENV
 
+      - name: Update versions
+        continue-on-error: true
+        run: |
+          python3 -m pip install beautifulsoup4 lxml
+
+          eval $(ssh-agent -s)
+          ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}"
+
+          git clone git@github.com:cvc5/docs.git target-releases/
+
+          TARGET_DIR=
+          if [ "$ISRELEASE" = true ]; then
+            TARGET_DIR=target-releases/$NAME
+          else
+            TARGET_DIR=target-releases/cvc5-main
+          fi
+          cp -r docs-new "${TARGET_DIR}"
+          pushd target-releases/
+          python3 genversions.py
+          popd
+          cp -rf "${TARGET_DIR}" docs-new
+
       - name: Update docs
         continue-on-error: true
         run: |
@@ -115,19 +137,11 @@ jobs:
         continue-on-error: true
         run: |
           if [ "$ISRELEASE" = true ]; then
-            python3 -m pip install beautifulsoup4 lxml
-
-            eval $(ssh-agent -s)
-            ssh-add - <<< "${{ secrets.CVC5_DOCS_RELEASE_TOKEN }}"
-
-            git clone git@github.com:cvc5/docs.git target-releases/
-            cp -r docs-new target-releases/$NAME
             cd target-releases/
 
             rm -f latest
             ln -s $NAME latest
 
-            python3 genversions.py
             git add .
 
             git commit -m "Update docs for $NAME"

CMakeLists.txt

@@ -132,6 +132,29 @@ option(BUILD_DOCS "Build Api documentation")
 cvc5_option(STATIC_BINARY "Link against static system libraries \
 (enabled by default for static builds)")
 
+# Custom flags for WebAssembly compilation
+set(WASM_FLAGS "" CACHE STRING "Link flags for the WebAssembly binary generation")
+set(WASM "OFF" CACHE STRING "Use a specific extension for WebAssembly compilation")
+
+# Make sure no other available value will be assigned to this variable
+if(NOT(WASM STREQUAL "WASM" OR WASM STREQUAL "JS" OR WASM STREQUAL "HTML" OR WASM STREQUAL "OFF"))
+  message(FATAL_ERROR "${WASM} is not a valid wasm flag value.")
+endif()
+
+if(WASM STREQUAL "OFF")
+  set(WASM_FLAGS "")
+  set(CONFIGURE_CMD_WRAPPER "")
+# If it's a wasm compilation, but isn't using the right flags
+elseif(BUILD_SHARED_LIBS OR NOT(STATIC_BINARY) OR NOT(ENABLE_AUTO_DOWNLOAD))
+  message(FATAL_ERROR "Use --static, --static-binary and --auto-download flags for WebAssembly compilation. GMP will not compile with shared libraries.")
+else()
+  set(CONFIGURE_CMD_WRAPPER emconfigure)
+  set(TOOLCHAIN_PREFIX wasm64-unknown-emscripten)
+  string(TOLOWER ".${WASM}" WASM_EXTENSION)
+  set(CMAKE_EXECUTABLE_SUFFIX ${WASM_EXTENSION})
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " ${WASM_FLAGS}")
+endif()
+
 #-----------------------------------------------------------------------------#
 # Internal cmake variables
 

INSTALL.rst

@@ -54,6 +54,56 @@ The built binary ``cvc5.exe`` is located in ``<build_dir>/bin`` and the cvc5
 library can be found in ``<build_dir>/lib``.
 
 
+WebAssembly Compilation
+^^^^^^^^^^^^^^^^^^^^^^^^
+
+Compiling cvc5 to WebAssembly needs the Emscripten SDK (version 3.1.18 or 
+latter). Setting up emsdk can be done as follows:
+
+.. code:: bash
+
+  git clone https://github.com/emscripten-core/emsdk.git
+  cd emsdk
+  ./emsdk install <version>   # <version> = '3.1.18' is preferable, but 
+                              # <version> = 'latest' has high chance of working
+  ./emsdk activate <version>
+  source ./emsdk_env.sh   # Activate PATH and other environment variables in the
+                          # current terminal. Whenever Emscripten is going to be
+                          # used this command needs to be called before because 
+                          # emsdk doesn't insert the binaries paths directly in 
+                          # the system PATH variable.
+
+Refer to the `emscripten dependencies list <https://emscripten.org/docs/getting_started/downloads.html#platform-specific-notes>`_ 
+to ensure that all required dependencies are installed on the system.
+
+Then, in the cvc5 directory:
+
+.. code:: bash
+
+  ./configure.sh --static --static-binary --auto-download --wasm=<value> --wasm-flags='<emscripten flags>' <configure options...>
+
+  cd <build_dir>   # default is ./build
+  make             # use -jN for parallel build with N threads
+
+``--wasm`` can take three values: ``WASM`` (will generate the wasm file for cvc5), ``JS``
+(not only the wasm, but the .js glue code for web integration) and ``HTML`` (both
+the last two files and also an .html file which supports the run of the glue
+code).
+
+``--wasm-flags`` take a string wrapped by a single quote containing the
+`emscripten flags <https://github.com/emscripten-core/emscripten/blob/main/src/settings.js>`_,
+which modifies how the wasm and glue code are built and how they behave. An ``-s``
+should precede each flag.
+
+For example, to generate modularized glue code, use:
+
+.. code:: bash
+
+  ./configure.sh --static --static-binary --auto-download --wasm=JS --wasm-flags='-s MODULARIZE' --name=prod
+
+  cd prod
+  make            # use -jN for parallel build with N threads
+
 Build dependencies
 ------------------
 

NEWS.md

@@ -6,8 +6,14 @@ This file contains a summary of important user-visible changes.
     of the solver version.
 - Support for bit-vector overflow detection operators:
   * `BITVECTOR_UADDO` unsigned addition overflow detection
+  * `BITVECTOR_SADDO` signed addition overflow detection
   * `BITVECTOR_UMULO` unsigned multiplication overflow detection
   * `BITVECTOR_SMULO` signed multiplication overflow detection
+  * `BITVECTOR_USUBO` unsigned subtraction overflow detection
+  * `BITVECTOR_SSUBO` signed subtraction overflow detection
+  * `BITVECTOR_SDIVO` signed division overflow detection
+
+- Support for Web Assembly compilation using Emscripten.
 
 **Changes**
 

THANKS

@@ -54,3 +54,7 @@ Thanks to:
 - Fabian Wolff in 2016 for fixing several spelling mistakes.
 
 - Justin Xu for contributing to refactoring CVC4's preprocessing infrastructure.
+
+- Vinicius Braga Freire for a modification in the proof printer for dot format,
+  allowing the clusterization of the proof into logic groups. Furthermore,for
+  implementing a built-in Web Assembly compilation method in 2022.

cmake/FindANTLR3.cmake

@@ -127,7 +127,7 @@ if(NOT ANTLR3_FOUND_SYSTEM)
           <INSTALL_DIR>/share/config.sub
           <SOURCE_DIR>/config.sub
         CONFIGURE_COMMAND
-          <SOURCE_DIR>/configure
+          ${CONFIGURE_CMD_WRAPPER} <SOURCE_DIR>/configure
             ${compilers}
             --with-pic
             --disable-antlrdebug

cmake/FindGMP.cmake

@@ -113,7 +113,7 @@ if(NOT GMP_FOUND_SYSTEM)
     URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822
     CONFIGURE_COMMAND
       ${CONFIGURE_ENV}
-        <SOURCE_DIR>/configure
+          ${CONFIGURE_CMD_WRAPPER} <SOURCE_DIR>/configure
           ${LINK_OPTS}
           --prefix=<INSTALL_DIR>
           --with-pic

cmake/FindPoly.cmake

@@ -156,6 +156,13 @@ if(NOT Poly_FOUND_SYSTEM)
       sed -i.orig
       "s,add_subdirectory(test/polyxx),add_subdirectory(test/polyxx EXCLUDE_FROM_ALL),g"
       <SOURCE_DIR>/CMakeLists.txt
+    COMMAND
+      # LibPoly declares a variable `enabled_count` whose value is only written
+      # and never read. Newer versions of Clang throw a warning for this, which
+      # aborts the compilation when -Wall is enabled.
+      sed -i.orig
+      "/enabled_count/d"
+      <SOURCE_DIR>/src/upolynomial/factorization.c
       ${POLY_PATCH_CMD}
     CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release
                -DCMAKE_INSTALL_PREFIX=<INSTALL_DIR>

configure.sh

@@ -69,6 +69,10 @@ Optional Path to Optional Packages:
 CMake Options (Advanced)
   -DVAR=VALUE              manually add CMake options
 
+Wasm Options
+  --wasm=VALUE             set compilation extension for WebAssembly <WASM, JS or HTML>
+  --wasm-flags='STR'       Emscripten flags used in the WebAssembly binary compilation
+
 EOF
   exit 0
 }
@@ -134,6 +138,9 @@ ipo=default
 
 glpk_dir=default
 
+wasm=default
+wasm_flags=""
+
 #--------------------------------------------------------------------------#
 
 cmake_opts=""
@@ -272,6 +279,12 @@ do
     --dep-path) die "missing argument to $1 (try -h)" ;;
     --dep-path=*) dep_path="${dep_path};${1##*=}" ;;
 
+    --wasm) wasm=WASM ;;
+    --wasm=*) wasm="${1##*=}" ;;
+
+    --wasm-flags) die "missing argument to $1 (try -h)" ;;
+    --wasm-flags=*) wasm_flags="${1#*=}" ;;
+
     -D*) cmake_opts="${cmake_opts} $1" ;;
 
     -*) die "invalid option '$1' (try -h)";;
@@ -370,9 +383,18 @@ fi
   && cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
 [ -n "$program_prefix" ] \
   && cmake_opts="$cmake_opts -DPROGRAM_PREFIX=$program_prefix"
+[ "$wasm" != default ] \
+  && cmake_opts="$cmake_opts -DWASM=$wasm"
 
 root_dir=$(pwd)
 
+cmake_wrapper=
+cmake_opts=($cmake_opts)
+if [ "$wasm" == "WASM" ] || [ "$wasm" == "JS" ] || [ "$wasm" == "HTML" ] ; then
+  cmake_wrapper=emcmake
+  cmake_opts=(${cmake_opts[@]} -DWASM_FLAGS="${wasm_flags}")
+fi
+
 # The cmake toolchain can't be changed once it is configured in $build_dir.
 # Thus, remove $build_dir and create an empty directory.
 [ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir"
@@ -383,5 +405,5 @@ cd "$build_dir"
 
 [ -e CMakeCache.txt ] && rm CMakeCache.txt
 build_dir_escaped=$(echo "$build_dir" | sed 's/\//\\\//g')
-cmake "$root_dir" $cmake_opts 2>&1 | \
+$cmake_wrapper cmake "$root_dir" "${cmake_opts[@]}" 2>&1 | \
   sed "s/^Now just/Now change to '$build_dir_escaped' and/"