Merge branch 'main' into ic3ia-cvc5-pred-rebase

.github/workflows/ci.yml

@@ -19,28 +19,30 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y \
             cmake \
+            ninja-build \
             libgmp-dev \
             openjdk-8-jdk
 
       - name: Install Packages (macOS)
         if: runner.os == 'macOS'
         run: |
           brew install \
+            ninja \
             gmp
 
-      # install previous version of setuptools as temporary fix
-      # see also recommendations here: https://github.com/pypa/setuptools/issues/3227
-      - name: Python Dependencies (macOS)
-        if: runner.os == 'macOS'
-        run: python3 -m pip install 'setuptools<61'
+      - name: Python Environment Setup
+        run: |
+          python3 -m venv ./.venv
+          echo "$PWD/.venv/bin" >> $GITHUB_PATH
 
       - name: Python Dependencies (all)
-        run: python3 -m pip install Cython pytest toml
+        run: python3 -m pip install Cython pytest pyparsing toml meson
 
       - name: Python Dependencies (all)
         run: python3 -m pip install scikit-build
 
       - name: Download MathSAT
+        if: runner.os != 'macOS'
         run: ./ci-scripts/setup-msat.sh --auto-yes
 
       - name: Setup Flex
@@ -52,12 +54,23 @@ jobs:
       - name: Setup Btor2Tools
         run: ./contrib/setup-btor2tools.sh
 
-      - name: Setup Smt-Switch
-        run: |
-          ./contrib/setup-smt-switch.sh --with-msat --python
-          python3 -m pip install -e ./deps/smt-switch/build/python
+      - name: Setup Smt-Switch (macOS)
+        if: runner.os == 'macOS'
+        run: ./contrib/setup-smt-switch.sh --python
+
+      - name: Setup Smt-Switch (non-macOS)
+        if: runner.os != 'macOS'
+        run: ./contrib/setup-smt-switch.sh --with-msat --python
+
+      - name: Set up Python bindings for smt-switch
+        run: python3 -m pip install -e ./deps/smt-switch/build/python
+
+      - name: Configure (macOS)
+        if: runner.os == 'macOS'
+        run: ./configure.sh --debug --python
 
-      - name: Configure
+      - name: Configure (non-macOS)
+        if: runner.os != 'macOS'
         run: ./configure.sh --with-msat --debug --python
 
       - name: Build

.gitignore

@@ -31,6 +31,15 @@
 *.out
 *.app
 
+# Build directories
 build
+install
+local
 deps
+
+# Cache directories
 __pycache__
+.cache
+
+# Generated files
+compile_commands.json

CMakeLists.txt

@@ -28,10 +28,18 @@ else()
   set(SHARED_LIB_EXT "so")
 endif()
 
+if (WITH_BOOLECTOR)
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_BOOLECTOR")
+endif()
+
 if (WITH_MSAT)
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_MSAT")
 endif()
 
+if (WITH_YICES2)
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_YICES2")
+endif()
+
 if (WITH_PROFILING)
   find_library(GOOGLE_PERF profiler REQUIRED)
   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DWITH_PROFILING")
@@ -52,8 +60,6 @@ if (BISON_FOUND)
   link_directories("${BISON_PARENT_DIR}/../lib/")
 endif()
 
-find_library(LIBRT rt)
-
 message("-- FOUND FLEX EXECUTABLE: ${FLEX_EXECUTABLE}")
 message("-- FOUND FLEX INCLUDE DIRS: ${FLEX_INCLUDE_DIRS}")
 
@@ -67,8 +73,13 @@ set(SMT_SWITCH_DIR "${PROJECT_SOURCE_DIR}/deps/smt-switch")
 set(CMAKE_MODULE_PATH ${SMT_SWITCH_DIR}/cmake)
 
 find_package(GMP REQUIRED)
+find_package(PkgConfig REQUIRED)
 
 # Check that dependencies are there
+list(APPEND CMAKE_PREFIX_PATH "${SMT_SWITCH_DIR}/deps/install")
+
+pkg_check_modules(BITWUZLA REQUIRED bitwuzla)
+
 if (NOT EXISTS "${SMT_SWITCH_DIR}/local/include/smt-switch/smt.h")
   message(FATAL_ERROR "Missing smt-switch headers -- try running ./contrib/setup-smt-switch.sh")
 endif()
@@ -77,12 +88,18 @@ if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch.a")
   message(FATAL_ERROR "Missing smt-switch library -- try running ./contrib/setup-smt-switch.sh")
 endif()
 
-if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a")
-  message(FATAL_ERROR "Missing smt-switch boolector library -- try running ./contrib/setup-smt-switch.sh")
+if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-bitwuzla.a")
+  message(FATAL_ERROR "Missing smt-switch Bitwuzla library -- try running ./contrib/setup-smt-switch.sh")
 endif()
 
 if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-cvc5.a")
-  message(FATAL_ERROR "Missing smt-switch cvc5 library -- try running ./contrib/setup-smt-switch.sh --with-cvc5")
+  message(FATAL_ERROR "Missing smt-switch cvc5 library -- try running ./contrib/setup-smt-switch.sh")
+endif()
+
+if (WITH_BOOLECTOR)
+  if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a")
+    message(FATAL_ERROR "Missing smt-switch Boolector library -- try running ./contrib/setup-smt-switch.sh --with-btor")
+  endif()
 endif()
 
 if (WITH_MSAT)
@@ -91,6 +108,12 @@ if (WITH_MSAT)
   endif()
 endif()
 
+if (WITH_YICES2)
+  if (NOT EXISTS "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-yices2.a")
+    message(FATAL_ERROR "Missing smt-switch Yices2 library -- try running ./contrib/setup-smt-switch.sh --with-yices2")
+  endif()
+endif()
+
 if (WITH_MSAT_IC3IA)
   if (NOT EXISTS "${PROJECT_SOURCE_DIR}/deps/ic3ia/build/libic3ia.a")
     message(FATAL_ERROR "Missing ic3ia library -- try running ./contrib/setup-ic3ia.sh")
@@ -226,13 +249,21 @@ if (BUILD_PYTHON_BINDINGS)
   add_subdirectory(python)
 endif()
 
-target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a")
+target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-bitwuzla.a")
 target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-cvc5.a")
 
+if (WITH_BOOLECTOR)
+  target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-btor.a")
+endif()
+
 if (WITH_MSAT)
   target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-msat.a")
 endif()
 
+if (WITH_YICES2)
+  target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch-yices2.a")
+endif()
+
 if (WITH_MSAT_IC3IA)
   target_link_libraries(pono-lib PUBLIC "${PROJECT_SOURCE_DIR}/deps/ic3ia/build/libic3ia.a")
 endif()
@@ -264,15 +295,12 @@ endif()
 
 target_link_libraries(pono-lib PUBLIC "${SMT_SWITCH_DIR}/local/lib/libsmt-switch.a")
 target_link_libraries(pono-lib PUBLIC "${PROJECT_SOURCE_DIR}/deps/btor2tools/build/lib/libbtor2parser.a")
+target_link_libraries(pono-lib PUBLIC "${BITWUZLA_LDFLAGS}")
 target_link_libraries(pono-lib PUBLIC "${GMPXX_LIBRARIES}")
 target_link_libraries(pono-lib PUBLIC "${GMP_LIBRARIES}")
 target_link_libraries(pono-lib PUBLIC pthread)
 target_link_libraries(pono-lib PUBLIC y)
 
-if (LIBRT)
-  target_link_libraries(pono-lib PUBLIC ${LIBRT})
-endif()
-
 if (GOOGLE_PERF)
   target_link_libraries(pono-lib PUBLIC ${GOOGLE_PERF})
 endif()

README.md

@@ -1,7 +1,7 @@
 [![CI](https://github.com/upscale-project/pono/actions/workflows/ci.yml/badge.svg)](https://github.com/upscale-project/pono/actions/workflows/ci.yml)
 
 # Pono: A Flexible and Extensible SMT-Based Model Checker
-Pono is a performant, adaptable, and extensible SMT-based model checker implemented in C++. It leverages [Smt-Switch](https://github.com/makaimann/smt-switch), a generic C++ API for SMT solving. Pono was developed as the next
+Pono is a performant, adaptable, and extensible SMT-based model checker implemented in C++. It leverages [Smt-Switch](https://github.com/stanford-centaur/smt-switch), a generic C++ API for SMT solving. Pono was developed as the next
 generation of [CoSA](https://github.com/cristian-mattarei/CoSA) and thus was originally named _cosa2_.
 
 [Pono](http://wehewehe.org/gsdl2.85/cgi-bin/hdict?e=q-11000-00---off-0hdict--00-1----0-10-0---0---0direct-10-ED--4--textpukuielbert%2ctextmamaka-----0-1l--11-en-Zz-1---Zz-1-home-pono--00-3-1-00-0--4----0-0-11-10-0utfZz-8-00&a=d&d=D18537) is the Hawaiian word for proper, correct, or goodness. It is often used colloquially in the moral sense of "goodness" or "rightness," but also refers to "proper procedure" or "correctness." We use the word for multiple meanings. Our goal is that Pono can be a useful tool for people to verify the _correctness_ of systems, which is surely the _right_ thing to do.
@@ -22,7 +22,7 @@ Pono was awarded the Oski Award under its original name _cosa2_ at [HWMCC'19](ht
 * [optional] Install bison and flex
   * If you don't have bison and flex installed globally, run `./contrib/setup-bison.sh` and `./contrib/setup-flex.sh`
   * Even if you do have bison, you might get errors about not being able to load `-ly`. In such a case, run the bison setup script.
-* Run `./contrib/setup-smt-switch.sh` -- it will build smt-switch with boolector
+* Run `./contrib/setup-smt-switch.sh` -- it will build smt-switch with Bitwuzla
   * [optional] to build with MathSAT (required for interpolant-based model checking) you need to obtain the libraries yourself
     * note that MathSAT is under a custom non-BSD compliant license and you must assume all responsibility for meeting the conditions
     * download the solver from https://mathsat.fbk.eu/download.html, unpack it and rename the directory to `./deps/mathsat`
@@ -72,7 +72,7 @@ There are two Transition System interfaces:
 ### Smt-Switch
 [Smt-switch](https://github.com/stanford-centaur/smt-switch) is a C++ solver-agnostic API for SMT solvers. The main thing to remember is that everything is a pointer. Objects might be "typedef-ed" with `using` statements, but they're still `shared_ptr`s. Thus, when using a solver or a term, you need to use `->` accesses.
 
-For more information, see the example usage in the [smt-switch tests](https://github.com/makaimann/smt-switch/tree/master/tests/btor).
+For more information, see the example usage in the [smt-switch tests](https://github.com/stanford-centaur/smt-switch/tree/master/tests/btor).
 Other useful files to visit include:
 * `smt-switch/include/solver.h`: this is the main interface you will be using
 * `smt-switch/include/ops.h`: this contains all the ops you might need

ci-scripts/setup-msat.sh

@@ -1,4 +1,5 @@
 #!/bin/bash
+set -e
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 DEPS=$DIR/../deps
@@ -60,7 +61,6 @@ if [ ! -d "$DEPS/mathsat" ]; then
 
 else
     echo "$DEPS/mathsat already exists. If you want to re-download, please remove it manually."
-    exit 1
 fi
 
 if [ -f $DEPS/mathsat/lib/libmathsat.a ] ; then \

configure.sh

@@ -13,8 +13,10 @@ Configures the CMAKE build environment.
 -h, --help              display this message and exit
 --prefix=STR            install directory       (default: /usr/local/)
 --build-dir=STR         custom build directory  (default: build)
+--with-btor             build with Boolector  (default: off)
 --with-msat             build with MathSAT which has a custom non-BSD compliant license.  (default : off)
                         Required for interpolant based model checking
+--with-yices2           build with Yices2 which has a custom non-BSD compliant license (default : off)
 --with-msat-ic3ia       build with the open-source IC3IA implementation as a backend. (default: off)
 --with-coreir           build the CoreIR frontend (default: off)
 --with-coreir-extern    build the CoreIR frontend using an installation of coreir in /usr/local/lib (default: off)
@@ -23,6 +25,7 @@ Configures the CMAKE build environment.
 --static-lib            build a static library (default: shared)
 --static                build a static executable (default: dynamic); implies --static-lib
 --with-profiling        build with gperftools for profiling (default: off)
+--no-system-gtest       do not use system GTest sources; forces download (default: off)
 EOF
   exit 0
 }
@@ -35,7 +38,9 @@ die () {
 build_dir=build
 install_prefix=default
 build_type=default
+with_boolector=default
 with_msat=default
+with_yices2=default
 with_msat_ic3ia=default
 with_coreir=default
 with_coreir_extern=default
@@ -44,6 +49,7 @@ python=default
 lib_type=SHARED
 static_exec=NO
 with_profiling=default
+system_gtest=default
 
 buildtype=Release
 
@@ -71,7 +77,9 @@ do
                 *) build_dir=$(pwd)/$build_dir ;; # make absolute path
             esac
             ;;
+        --with-btor) with_boolector=ON;;
         --with-msat) with_msat=ON;;
+        --with-yices2) with_yices2=ON;;
         --with-msat-ic3ia) with_msat_ic3ia=ON;;
         --with-coreir) with_coreir=ON;;
         --with-coreir-extern) with_coreir_extern=ON;;
@@ -90,6 +98,7 @@ do
             lib_type=STATIC;
             ;;
         --with-profiling) with_profiling=ON;;
+        --no-system-gtest) system_gtest=no;;
         *) die "unexpected argument: $1";;
     esac
     shift
@@ -103,9 +112,15 @@ cmake_opts="-DCMAKE_BUILD_TYPE=$buildtype -DPONO_LIB_TYPE=${lib_type} -DPONO_STA
 [ $install_prefix != default ] \
     && cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
 
+[ $with_boolector != default ] \
+    && cmake_opts="$cmake_opts -DWITH_BOOLECTOR=$with_boolector"
+
 [ $with_msat != default ] \
     && cmake_opts="$cmake_opts -DWITH_MSAT=$with_msat"
 
+[ $with_yices2 != default ] \
+    && cmake_opts="$cmake_opts -DWITH_YICES2=$with_yices2"
+
 [ $with_msat_ic3ia != default ] \
     && cmake_opts="$cmake_opts -DWITH_MSAT_IC3IA=$with_msat_ic3ia"
 
@@ -121,6 +136,9 @@ cmake_opts="-DCMAKE_BUILD_TYPE=$buildtype -DPONO_LIB_TYPE=${lib_type} -DPONO_STA
 [ $with_profiling != default ] \
     && cmake_opts="$cmake_opts -DWITH_PROFILING=$with_profiling"
 
+[ $system_gtest != default ] \
+    && cmake_opts="$cmake_opts -DSYSTEM_GTEST=$system_gtest"
+
 root_dir=$(pwd)
 
 [ -e "$build_dir" ] && rm -r "$build_dir"

contrib/setup-bison.sh

@@ -1,4 +1,7 @@
 #!/bin/bash
+set -e
+
+BISON_VERSION=3.7.4
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 DEPS=$DIR/../deps
@@ -11,17 +14,17 @@ if [ -d "$DEPS/bison" ]; then
     exit 1
 fi
 
-curl http://ftp.gnu.org/gnu/bison/bison-3.7.tar.gz --output $DEPS/bison-3.7.tar.gz
+curl http://ftp.gnu.org/gnu/bison/bison-$BISON_VERSION.tar.gz --output $DEPS/bison-$BISON_VERSION.tar.gz
 
-if [ ! -f "$DEPS/bison-3.7.tar.gz" ]; then
-    echo "It seems like downloading bison to $DEPS/bison-3.7.tar.gz failed"
+if [ ! -f "$DEPS/bison-$BISON_VERSION.tar.gz" ]; then
+    echo "It seems like downloading bison to $DEPS/bison-$BISON_VERSION.tar.gz failed"
     exit 1
 fi
 
 cd $DEPS
-tar -xzf bison-3.7.tar.gz
-rm bison-3.7.tar.gz
-mv ./bison-3.7 ./bison
+tar -xzf bison-$BISON_VERSION.tar.gz
+rm bison-$BISON_VERSION.tar.gz
+mv ./bison-$BISON_VERSION ./bison
 cd bison
 mkdir bison-install
 ./configure --prefix $DEPS/bison/bison-install --exec-prefix $DEPS/bison/bison-install

contrib/setup-btor2tools.sh

@@ -1,6 +1,7 @@
 #!/bin/bash
+set -e
 
-BTOR2TOOLS_VERSION=9831f9909fb283752a3d6d60d43613173bd8af42
+BTOR2TOOLS_VERSION=ff44a21e113667f4cb27dbf96ee46b95c612caf9
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 DEPS=$DIR/../deps
@@ -9,7 +10,7 @@ mkdir -p $DEPS
 
 if [ ! -d "$DEPS/btor2tools" ]; then
     cd $DEPS
-    git clone --depth 1 https://github.com/Boolector/btor2tools.git btor2tools
+    git clone https://github.com/Boolector/btor2tools.git btor2tools
     cd btor2tools
     git checkout -f $BTOR2TOOLS_VERSION
     CFLAGS="-fPIC" ./configure.sh --static
@@ -29,4 +30,3 @@ else
     echo "Please see their github page for installation instructions: https://github.com/Boolector/btor2tools.git"
     exit 1
 fi
-

contrib/setup-coreir.sh

@@ -1,4 +1,5 @@
 #!/bin/bash
+set -e
 
 COREIR_VERSION=2f5035c6712481346c20c0a9956dc3f880cac1d2
 
@@ -76,4 +77,3 @@ else
     echo "Please see their github page for installation instructions:https://github.com/rdaly525/coreir"
     exit 1
 fi
-

contrib/setup-flex.sh

@@ -1,4 +1,5 @@
 #!/bin/bash
+set -e
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 DEPS=$DIR/../deps

contrib/setup-ic3ia.sh

@@ -1,4 +1,5 @@
 #!/bin/bash
+set -e
 
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 DEPS=$DIR/../deps