Merge remote-tracking branch 'origin' into per-thread-state

.github/actions/build/action.yml

@@ -0,0 +1,47 @@
+name: Build
+
+inputs:
+  mode:
+    required: true
+  config-opt:
+    required: false
+    default: ""
+  env:
+    required: false
+    default: ""
+
+runs:
+  using: composite
+  steps:
+    - name: Build and install libpoly
+      shell: bash
+      run: |
+        pushd .
+        git clone https://github.com/SRI-CSL/libpoly.git
+        mkdir -p libpoly/build
+        cd libpoly/build
+        ${{ inputs.env }} cmake ..
+        make
+        sudo make install
+        popd
+    - name: Build and install CUDD
+      shell: bash
+      run: |
+        pushd .
+        git clone https://github.com/ivmai/cudd.git
+        cd cudd
+        git checkout tags/cudd-3.0.0
+        autoreconf -fi
+        ${{ inputs.env }} ./configure --enable-shared
+        make
+        sudo make install
+        popd
+    - name: Build and test Yices
+      shell: bash
+      run: |
+        autoconf
+        #CFLAGS='-Werror' ${{ inputs.env }} ./configure ${{ inputs.config-opt }}
+        ${{ inputs.env }} ./configure ${{ inputs.config-opt }}
+        # This is needed for yices2 to find libpoly.so.0. /usr/local/lib not searched by default?
+        export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH}
+        make MODE=${{ inputs.mode }}

.github/actions/coverage/action.yml

@@ -0,0 +1,9 @@
+name: Coverage
+
+runs:
+  using: composite
+  steps:
+    - name: Run Coverage
+      shell: bash
+      run: |
+        lcov --directory build --base-directory src --capture --output-file coverage.info

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

@@ -0,0 +1,16 @@
+name: Install Dependencies
+
+runs:
+  using: composite
+  steps:
+    - name: Install Linux Dependencies
+      if: runner.os == 'Linux'
+      shell: bash
+      run: |
+        echo "Install Linux dependencies"
+        sudo apt-get update
+        sudo apt-get install -y libgmp-dev gperf
+        sudo apt-get install -y python3-pip
+        sudo apt-get install -y lcov
+        sudo gem install coveralls-lcov
+        echo "Install Linux dependencies [DONE]"

.github/actions/test/action.yml

@@ -0,0 +1,15 @@
+name: Test
+
+inputs:
+  mode:
+    required: true
+
+runs:
+  using: composite
+  steps:
+    - name: Test Yices
+      shell: bash
+      run: |
+        # This is needed for yices2 to find libpoly.so.0. /usr/local/lib not searched by default?
+        export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH}
+        make MODE=${{ inputs.mode }} check

.github/workflows/ci.yml

@@ -0,0 +1,51 @@
+name: CI
+
+on:
+  push:
+  pull_request:
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        os: [ubuntu-latest]
+        mode: [debug, release]
+        config-opt: [--enable-mcsat, --enable-thread-safety]
+        env: [CC=gcc CXX=g++, CC=clang CXX=clang++]
+        include:
+          - os: ubuntu-latest
+            mode: gcov
+            config-opt: --enable-mcsat
+            env: CC=gcc CXX=g++
+
+    name: ${{ matrix.os }}|${{ matrix.mode }}|${{ matrix.config-opt }}|${{ matrix.env }}
+    runs-on: ${{ matrix.os }}
+
+    steps:
+    - uses: actions/checkout@v3
+
+    - name: Install Dependencies
+      uses: ./.github/actions/install-dependencies
+
+    - name: Build
+      uses: ./.github/actions/build
+      with:
+        mode: ${{ matrix.mode }}
+        config-opt: ${{ matrix.config-opt }}
+        env: ${{ matrix.env }}
+
+    - name: Test
+      uses: ./.github/actions/test
+      with:
+        mode: ${{ matrix.mode }}
+
+    - name: Coverage
+      if: matrix.mode == 'gcov'
+      uses: ./.github/actions/coverage
+
+    - name: Coveralls
+      if: matrix.mode == 'gcov'
+      uses: coverallsapp/github-action@master
+      with:
+        github-token: ${{ secrets.GITHUB_TOKEN }}
+        path-to-lcov: 'coverage.info'

INSTALL

@@ -83,8 +83,11 @@ instructions:
 1) Install SRI's library for polynomial manipulation. It's available
    on github (https://github.com/SRI-CSL/libpoly).
 
-2) After you've installed libpoly, add option --enable-mcsat to 
-   the configure command. In details, type this in the toplevel
+2) Install the CUDD library for binary-decision diagrams. We recommend
+   using the github distribution: https://github.com/ivmai/cudd.
+
+3) After you've installed libpoly and cudd, add option --enable-mcsat 
+   to the configure command. In details, type this in the toplevel
    Yices directory:
 
     autoconf

Makefile

@@ -66,6 +66,7 @@ YICES_VERSION = $(MAJOR).$(MINOR).$(PATCH_LEVEL)
 #
 ARCH=$(shell ./config.sub `./config.guess`)
 POSIXOS=$(shell ./autoconf/os)
+PLATFORM=$(shell uname -p)
 
 ifeq (,$(POSIXOS))
   $(error "Problem running ./autoconf/os")
@@ -150,12 +151,22 @@ ifneq ($(OPTION),)
     endif
   else
   ifeq ($(POSIXOS),darwin)
-    ifeq ($(OPTION),64bits)
-      newarch=$(subst i386,x86_64,$(ARCH))
+    ifeq ($(PLATFORM),powerpc)
+      ifeq ($(OPTION),64bits)
+        newarch=$(subst powerpc,powerpc64,$(ARCH))
+      else
+      ifeq ($(OPTION),32bits)
+        newarch=$(subst powerpc64,powerpc,$(ARCH))
+      endif
+      endif
     else
-    ifeq ($(OPTION),32bits)
-      newarch=$(subst x86_64,i386,$(ARCH))
-    endif
+      ifeq ($(OPTION),64bits)
+        newarch=$(subst i386,x86_64,$(ARCH))
+      else
+      ifeq ($(OPTION),32bits)
+        newarch=$(subst x86_64,i386,$(ARCH))
+      endif
+      endif
     endif
   else
   ifeq ($(POSIXOS),cygwin)

Makefile.build

@@ -89,7 +89,7 @@ srcsubdirs = mt io terms utils solvers solvers/floyd_warshall \
     solvers/funs solvers/bv solvers/egraph solvers/cdcl solvers/simplex solvers/quant \
     parser_utils model scratch api frontend frontend/common \
     frontend/smt1 frontend/yices frontend/smt2 context exists_forall \
-    mcsat mcsat/eq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/bv \
+    mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/bv \
     mcsat/bv/explain mcsat/utils
 
 testdir = tests/unit

README.md

@@ -1,5 +1,5 @@
 [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0)
-[![Build Status](https://travis-ci.org/SRI-CSL/yices2.svg?branch=master)](https://travis-ci.org/SRI-CSL/yices2)
+[![CI](https://github.com/SRI-CSL/yices2/actions/workflows/ci.yml/badge.svg)](https://github.com/SRI-CSL/yices2/actions/workflows/ci.yml)
 [![Coverity Scan Build Status](https://scan.coverity.com/projects/12768/badge.svg)](https://scan.coverity.com/projects/sri-csl-yices2)
 [![Coverage Status](https://coveralls.io/repos/github/SRI-CSL/yices2/badge.svg?branch=master)](https://coveralls.io/github/SRI-CSL/yices2?branch=master)
 
@@ -45,8 +45,9 @@ Running Yices on the above problem gives a solution
 ```
 > yices-smt2 lra.smt2
 sat
-(= x 2)
-(= y (- 1))
+(model
+  (define-fun x () Real 2.0)
+  (define-fun y () Real (- 1.0)))
 ```
 
 #### Bit-Vectors
@@ -72,8 +73,9 @@ Running Yices on the above problem gives
 ```
 > yices-smt2 bv.smt2
 sat
-(= x #b01000000000000000000000000000000)
-(= y #b01000000000000000000000000000000)
+(model
+  (define-fun x () (_ BitVec 32) #b01000000000000000000000000000000)
+  (define-fun y () (_ BitVec 32) #b01000000000000000000000000000000))
 ```
 
 #### Non-Linear Arithmetic
@@ -98,8 +100,9 @@ Running Yices on the above problem gives
 
 ```
 sat
-(= x 0.894427)
-(= y 0.447214)
+(model
+  (define-fun x () Real 0.894427)
+  (define-fun y () Real 0.447214))
 ```
 
 ## Installing Prebuilt Binaries

configure.ac

@@ -76,7 +76,7 @@ AC_PROG_LN_S
 AC_PROG_MKDIR_P
 AC_PROG_INSTALL
 
-AC_PROG_CC_C99
+AC_PROG_CC
 
 AC_PROG_RANLIB
 AC_PROG_EGREP
@@ -870,10 +870,6 @@ fi
 AC_SUBST(THREAD_SAFE)
 if test "x$thread_safe" = xyes ; then
    THREAD_SAFE=1
-   # iam: the aim is to eventually eliminate this restriction, but not before the 2.6.2 release.
-   if test $use_mcsat = yes ; then
-      AC_MSG_ERROR([Building with both --enable-mcsat and --enable-thread-safety is currently not supported.])
-   fi
 fi
 
 dnl

doc/COMPILING

@@ -633,7 +633,7 @@ dynamic and static libraries in different locations:
 2) Build GMP as a static library in a different location (say
    /tools/static_gmp/). This can be done by giving options
 
-      --disable-share --enable-static --prefix=/tools/static_gmp
+      --disable-shared --enable-static --prefix=/tools/static_gmp
 
    to GMP's configure script.  This will build
 

doc/GMP

@@ -373,20 +373,21 @@ For GMP 5.0.1, it's also a good idea to get the patch at
 Otherwise, make check will fail for t-perfpow.
 
 
-Then, give the following options to GMP's configure script:
+Then, give the following options to GMP's configure script
+(update the prefix path) for the dynamic GMP:
 
   ./configure --disable-static --enable-shared \
     --prefix=.... \
-    --host=x86_64-pc-mingw32 --build=i686-pc-cygwin \
-    CC=/usr/bin/x86_64-w64-mingw32-gcc \
-    NM=/usr/bin/x86_64-w64-mingw32-nm \
-    AR=/usr/bin/x86_64-w64-mingw32-ar \
-    CC_FOR_BUILD=gcc \
+    --host=x86_64-pc-mingw32 --build=i686-pc-cygwin 
 
+Then, for the static GMP (update the prefix path -- use a 
+different path from the dynamic GMP path):
 
-It's important to specify NM as the x86_64 version. Otherwise the
-'./configure' fails. Not sure specifying AR=... is required.
+   ./configure --host=x86_64-w64-mingw32 --enable-static \
+     --prefix=.... \
+     --disable-shared --build=i686-pc-cygwin
 
+Add the dynamic and static bin paths to the PATH env variable.
 
 
 UPDATE (2012/02/15)
@@ -400,7 +401,4 @@ mingw64, 'make check' failed with this complaint:
 To fix this, I just did:
    /usr/bin/x86_64-w64-mingw32-ranlib ./tests/.libs/libtests.a
 
-(Playing with with RANLIB= ... or other options to configure
- did not help).
-
 Then 'make check' proceeded without problems after that.