Merge branch 'master' into ilator_opt

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "extern/tmpl-synth"]
 	path = extern/tmpl-synth
 	url = https://github.com/PrincetonUniversity/ILA-Synthesis-Python.git
+[submodule "extern/smt-switch"]
+	path = extern/smt-switch
+	url = https://github.com/makaimann/smt-switch.git

.semaphore/semaphore.yml

@@ -0,0 +1,26 @@
+version: v1.0
+name: ILAng default build
+agent:
+  machine:
+    type: e1-standard-2
+    os_image: ubuntu1804
+blocks:
+  - name: build
+    task:
+      prologue:
+        commands:
+          - checkout
+      jobs:
+        - name: build_install_test
+          commands:
+            - sudo apt-get update
+            - sudo apt-get install -y bison flex libboost-all-dev z3 libz3-dev
+            - export CC=gcc-7
+            - export CXX=g++-7
+            - mkdir build
+            - cd build
+            - cmake .. -DCMAKE_BUILD_TYPE=Debug
+            - make -j$(nproc)
+            - sudo make install
+            - make run_test
+            - ctest -R ExampleCMakeBuild

.travis.yml

@@ -46,27 +46,6 @@ matrix:
       script:
         - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR
 
-    - name: "gcc49"
-      os: linux
-      dist: xenial
-      addons:
-        apt: 
-          sources:
-            - ubuntu-toolchain-r-test
-          packages:
-            - g++-4.9
-            - flex
-            - bison
-            - libboost-all-dev
-            - z3
-            - libz3-dev
-      env:
-        - MATRIX_EVAL="CC=gcc-4.9 && CXX=g++-4.9"
-      before_install:
-        - eval "${MATRIX_EVAL}"
-      script:
-        - source $TRAVIS_BUILD_DIR/scripts/travis/build.sh $TRAVIS_BUILD_DIR
-
     - name: "osx"
       os: osx
       before_install:

CMakeLists.txt

@@ -11,7 +11,7 @@ endif()
 # PROJECT
 # name version language
 # ---------------------------------------------------------------------------- #
-project(ilang VERSION     1.0.2
+project(ilang VERSION     1.0.3
               LANGUAGES   CXX
 )
 
@@ -27,7 +27,8 @@ option(ILANG_INSTALL_DEV "Install dev features."                            OFF)
 option(ILANG_EXPORT_PACKAGE "Export CMake package if enabled."              OFF)
 option(ILANG_COVERITY    "Build for Coverity static analysis."              OFF)
 option(BUILD_SHARED_LIBS "Build shared libraries."                           ON)
-option(ILANG_BUILD_INVSYN  "Build invariant synthesis feature."              ON)
+option(ILANG_BUILD_INVSYN "Build invariant synthesis feature."               ON)
+option(ILANG_BUILD_SWITCH "Build smt-switch interface."                     OFF)
 
 include(CMakeDependentOption)
 

README.md

@@ -1,8 +1,8 @@
 [![ILAng](https://raw.githubusercontent.com/Bo-Yuan-Huang/ILAng/master/docs/pics/ilang-logo.png)](https://bo-yuan-huang.gitbook.io/ilang/)
 
 [![Build Status](https://dev.azure.com/byhuang/ILAng/_apis/build/status/Bo-Yuan-Huang.ILAng?branchName=master)](https://dev.azure.com/byhuang/ILAng/_build/latest?definitionId=1&branchName=master)
-[![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILAng)
-[![Build Status](https://semaphoreci.com/api/v1/bo-yuan-huang/ilang/branches/master/shields_badge.svg)](https://semaphoreci.com/bo-yuan-huang/ilang)
+[![Build Status](https://travis-ci.com/Bo-Yuan-Huang/ILAng.svg?branch=master)](https://travis-ci.com/Bo-Yuan-Huang/ILAng)
+[![Build Status](https://ilang.semaphoreci.com/badges/ILAng.svg)](https://ilang.semaphoreci.com/projects/ILAng)
 [![Build status](https://ci.appveyor.com/api/projects/status/cwhlq09513art6hw/branch/master?svg=true)](https://ci.appveyor.com/project/Bo-Yuan-Huang/ilang/branch/master)
 [![Coverity Scan Build Status](https://scan.coverity.com/projects/17719/badge.svg)](https://scan.coverity.com/projects/bo-yuan-huang-ilang)
 [![Coverage Status](https://coveralls.io/repos/github/Bo-Yuan-Huang/ILAng/badge.svg?branch=master)](https://coveralls.io/github/Bo-Yuan-Huang/ILAng?branch=master)
@@ -59,15 +59,16 @@ brew install bison flex boost boost-python z3
 
 | OS                        | Compiler     | CMake  | z3    | Boost | Bison | Flex   | Build   |
 | ------------------------- | ------------ | ------ | ----- | ----- | ----- | ------ | ------- |
-| Ubuntu 14.04 (Trusty)     | gcc 4.8.4    | 3.8.0  | 4.8.6 | 1.54  | 3.0.4 | 2.5.25 | Release |
-| Ubuntu 16.04 (Xenial)     | gcc 5.4.0    | 3.12.4 | 4.4.1 | 1.58  | 3.0.4 | 2.6.0  | Debug   |
 | Ubuntu 16.04 (Xenial)     | clang 7.0.0  | 3.12.4 | 4.4.1 | 1.58  | 3.0.4 | 2.6.0  | Debug   |
-| Ubuntu 16.04 (Xenial)     | gcc 5.4.0    | 3.12.4 | 4.4.1 | 1.69  | 3.0.4 | 2.6.0  | Release |
-| Ubuntu 18.04 (Bionic)     | gcc 7.4.0    | 3.15.2 | 4.8.6 | 1.65  | 3.0.4 | 2.6.4  | Release |
-| OSX 10.13.3 (High Sierra) | Xcode 9.4.1  | 3.11.3 | 4.8.7 | 1.72  | 3.5.0 | 2.5.35 | Debug   |
-| OSX 10.13.6 (High Sierra) | Xcode 10.1.0 | 3.16.2 | 4.8.7 | 1.72  | 3.5.0 | 2.5.35 | Release |
-| OSX 10.14.5 (Mojave)      | Xcode 10.2.1 | 3.16.2 | 4.8.7 | 1.72  | 3.5.0 | 2.5.35 | Release |
-| Windows Server 2016       | VS 2017      | 3.14.5 | 4.8.6 | -     | 3.3.2 | 2.6.4  | Release |
+| Ubuntu 16.04 (Xenial)     | gcc 5.4.0    | 3.12.4 | 4.4.1 | 1.58  | 3.0.4 | 2.6.0  | Debug   |
+| Ubuntu 16.04 (Xenial)     | gcc 5.4.0    | 3.17.0 | 4.4.1 | 1.58  | 3.0.4 | 2.6.0  | Release |
+| Ubuntu 18.04 (Bionic)     | gcc 7.5.0    | 3.10.2 | 4.4.1 | 1.65  | 3.0.4 | 2.6.4  | Debug   |
+| Ubuntu 18.04 (Bionic)     | gcc 7.5.0    | 3.17.0 | 4.4.1 | 1.65  | 3.0.4 | 2.6.4  | Release |
+| Ubuntu 20.04 (Focal Fosa) | gcc 7.4.0    | 3.17.0 | 4.4.1 | 1.65  | 3.0.4 | 2.6.4  | Release |
+| OSX 10.13.6 (High Sierra) | Xcode 9.4.1  | 3.15.5 | 4.8.8 | 1.72  | 3.6.2 | 2.5.35 | Release |
+| OSX 10.14.6 (Mojave)      | Xcode 11.3.1 | 3.17.2 | 4.8.8 | 1.72  | 3.6.2 | 2.5.35 | Release |
+| OSX 10.15.4 (Catalina)    | Xcode 11.4.1 | 3.17.2 | 4.8.8 | 1.72  | 3.6.2 | 2.5.35 | Release |
+| Windows Server 2016       | VS 2017      | 3.17.2 | 4.8.8 | -     | 3.3.2 | 2.6.4  | Release |
 
 ### Default Build
 
@@ -99,7 +100,9 @@ sudo make install
 -   Use `-DILANG_FETCH_DEPS=OFF` to disable config-time updating submodules for in-source dependencies.
 -   Use `-DILANG_BUILD_TEST=OFF` to disalbe building the unit tests.
 -   Use `-DILANG_BUILD_SYNTH=OFF` to disable building the synthesis engine. 
--   Use `-DILANG_INSTALL_DEV=ON` to enable installing working features. 
+-   Use `-DILANG_BUILD_INVSYN=ON` to enable building invariant synthesis feature.
+-   Use `-DILANG_BUILD_SWITCH=ON` to enable building [smt-switch](https://github.com/makaimann/smt-switch.git) interface support. 
+-   Use `-DILANG_INSTALL_DEV=ON` to install working features. 
 
 ## CMake Integration
 
@@ -196,7 +199,7 @@ source init.sh
 ```
 
 to initialize the environment settings. 
-This docker image also contains the model checker [CoSA](https://github.com/cristian-mattarei/CoSA) with the SMT solvers [z3](https://github.com/Z3Prover/z3).
+This docker image also contains the model checker [CoSA](https://github.com/cristian-mattarei/CoSA) with the SMT solver [z3](https://github.com/Z3Prover/z3).
 
 ## License
 
@@ -235,6 +238,9 @@ Copyright 2008, Google Inc.
 ILAng contains the [JSON library](https://github.com/nlohmann/json), which is licensed under the [MIT License](https://github.com/nlohmann/json/blob/develop/LICENSE.MIT). 
 Copyright (c) 2013-2019 Niels Lohmann.
 
+ILAng contains the [fmt](https://github.com/fmtlib/fmt.git), which is licensed under [License](https://github.com/fmtlib/fmt/blob/master/LICENSE.rst).
+Copyright (c) 2012-present, Victor Zverovich.
+
 ILAng uses the [Verilog parser](https://github.com/ben-marshall/verilog-parser), which is licensed under the [MIT License](https://github.com/ben-marshall/verilog-parser/blob/master/LICENSE.txt).
 Copyright (c) 2016 Ben Marshall.
 
@@ -244,6 +250,9 @@ Copyright (c) 2018 Ben Marshall.
 ILAng uses the [SMT parser](https://es-static.fbk.eu/people/griggio/misc/smtlib2parser.html), which is licensed under the [MIT License](https://es-static.fbk.eu/people/griggio/misc/smtlib2parser.html).
 Copyright (c) 2010 Alberto Griggio.
 
+ILAng uses the [smt-switch](https://github.com/makaimann/smt-switch.git), which is licensed under the [BSD 3-Clause License](https://github.com/makaimann/smt-switch/blob/master/LICENSE).
+Copyright (c) 2019-2020 the authors.
+
 ILAng uses [ItSy](https://github.com/PrincetonUniversity/ItSy), which is licensed under the [MIT License](https://github.com/PrincetonUniversity/ItSy/blob/master/LICENSE).
 Copyright (c) 2016 Princeton University.
 

azure-pipelines.yml

@@ -1,15 +1,15 @@
+# File: azure-pipelines.yml
+
 trigger:
 - master
 
 pr:
 - master
 
-# File: azure-pipelines.yml
-
 jobs:
-- job: macOS_High_Sierra
+- job: macOS_Mojave
   pool:
-    vmImage: 'macOS-10.13'
+    vmImage: 'macOS-10.14'
   steps:
   - script: |
       brew update
@@ -18,24 +18,24 @@ jobs:
       brew install boost-python
       brew install z3
     displayName: 'package'
-  - script: | 
+  - script: |
       cmake --version
       z3 --version
     displayName: 'printout'
   - script: |
       export PATH="/usr/local/opt/bison/bin:$PATH"
       export LDFLAGS="-L/usr/local/opt/bison/lib"
-      mkdir -p build 
+      mkdir -p build
       cd build
       cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON -DILANG_BUILD_INVSYN=OFF
       cmake --build .
-      cmake --build . --target install 
+      cmake --build . --target install
       cmake --build . --target test
     displayName: 'build'
 
-- job: macOS_Mojave
+- job: macOS_Catalina
   pool:
-    vmImage: 'macOS-10.14'
+    vmImage: 'macOS-10.15'
   steps:
   - script: |
       brew update
@@ -44,22 +44,22 @@ jobs:
       brew install boost-python
       brew install z3
     displayName: 'package'
-  - script: | 
+  - script: |
       cmake --version
       z3 --version
     displayName: 'printout'
   - script: |
       export PATH="/usr/local/opt/bison/bin:$PATH"
       export LDFLAGS="-L/usr/local/opt/bison/lib"
-      mkdir -p build 
+      mkdir -p build
       cd build
       cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON -DILANG_BUILD_INVSYN=OFF
       cmake --build .
       cmake --build . --target install 
       cmake --build . --target test
     displayName: 'build'
 
-- job: Linux
+- job: Ubuntu_1604_LTS
   pool:
     vmImage: 'ubuntu-16.04'
   steps:
@@ -80,7 +80,28 @@ jobs:
       cmake --build . --target test
     displayName: 'build'
 
-- job: Windows
+- job: Ubuntu_1804_LTS
+  pool:
+    vmImage: 'ubuntu-18.04'
+  steps:
+  - script: |
+      sudo apt-get update
+      sudo apt-get install bison
+      sudo apt-get install flex
+      sudo apt-get install libboost-all-dev
+      sudo apt-get install z3
+      sudo apt-get install libz3-dev
+    displayName: 'package'
+  - script: |
+      mkdir -p build
+      cd build
+      cmake .. -DCMAKE_BUILD_TYPE=Release
+      cmake --build .
+      sudo cmake --build . --target install 
+      cmake --build . --target test
+    displayName: 'build'
+
+- job: Windows_2016
   pool:
     vmImage: 'vs2017-win2016'
   steps:
@@ -91,35 +112,35 @@ jobs:
     displayName: 'package'
 
   - script: |
-      wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.6/z3-4.8.6-x86-win.zip
-      unzip z3-4.8.6-x86-win.zip
-      move z3-4.8.6-x86-win z3
+      wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x86-win.zip
+      unzip z3-4.8.8-x86-win.zip
+      move z3-4.8.8-x86-win z3
     displayName: 'z3'
 
   - script: |
-      cd extern 
+      cd extern
       cd glog
-      md build 
+      md build
       cd build
-      cmake .. 
+      cmake ..
       cmake --build . --target install
     displayName: 'glog'
 
   - script: |
-      cd extern 
+      cd extern
       cd json
-      md build 
+      md build
       cd build
       cmake .. -DJSON_BuildTests=OFF
       cmake --build . --target install
     displayName: 'json'
 
   - script: |
-      cd extern 
+      cd extern
       cd vlog-parser
-      md build 
+      md build
       cd build
-      cmake .. 
+      cmake ..
       cmake --build . --target install
     displayName: 'vlog-parser'