Merge 77c5031 into 7400442

CMakeLists.txt

@@ -27,6 +27,7 @@ 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)
 
 include(CMakeDependentOption)
 

azure-pipelines.yml

@@ -30,7 +30,7 @@ jobs:
       cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON
       cmake --build .
       cmake --build . --target install 
-      cmake --build . --target test
+      ./test/unit_tests
     displayName: 'build'
 
 - job: macOS_Mojave
@@ -56,7 +56,7 @@ jobs:
       cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON
       cmake --build .
       cmake --build . --target install 
-      cmake --build . --target test
+      ./test/unit_tests --gtest_filter=TestVlgVerifInvSyn.*
     displayName: 'build'
 
 - job: Linux
@@ -139,3 +139,4 @@ jobs:
       cmake .. -DZ3_INCLUDE_DIR=$(Build.Repository.LocalPath)/z3/include -DZ3_LIBRARY=$(Build.Repository.LocalPath)/z3/bin/libz3.lib -DZ3_EXEC=$(Build.Repository.LocalPath)/z3/bin/z3.exe
       cmake --build . 
     displayName: 'starter'
+

cmake/config.cmake.in

@@ -5,6 +5,9 @@ include(CMakeFindDependencyMacro)
 find_dependency(glog REQUIRED)
 find_dependency(nlohmann_json REQUIRED)
 find_dependency(verilogparser REQUIRED)
+find_dependency(vcdparser REQUIRED)
+find_dependency(smtparser REQUIRED)
+
 find_dependency(Z3 REQUIRED)
 
 if(@ILANG_BUILD_SYNTH@)

extern/CMakeLists.txt

@@ -36,6 +36,43 @@ if(NOT NLOHMANN_JSON_FOUND)
 endif() # NLOHMANN_JSON_FOUND
 
 
+# ---------------------------------------------------------------------------- #
+# VCD Parser
+# 
+#   TARGET vcdparser::vcdparser
+#   SOURCE https://github.com/zhanghongce/verilog-vcd-parser.git
+#   PATH   extern/vcd-parser
+# ---------------------------------------------------------------------------- #
+# find installed package
+find_package(vcdparser 1.0 QUIET)
+
+# build from embeded subtree (in-source)
+if(NOT VCDPARSER_FOUND)
+
+  set(JSON_BuildTests OFF CACHE INTERNAL "")
+  add_subdirectory(vcd-parser)
+
+endif() # VCDPARSER_FOUND
+
+
+# ---------------------------------------------------------------------------- #
+# SMT Parser
+# 
+#   TARGET smtparser::smtparser
+#   SOURCE https://github.com/zhanghongce/smtlib2parser.git
+#   PATH   extern/smt-parser
+# ---------------------------------------------------------------------------- #
+# find installed package
+find_package(smtparser 1.0 QUIET)
+
+# build from embeded subtree (in-source)
+if(NOT SMTPARSER_FOUND)
+
+  set(JSON_BuildTests OFF CACHE INTERNAL "")
+  add_subdirectory(smt-parser)
+
+endif() # SMTPARSER_FOUND
+
 # ---------------------------------------------------------------------------- #
 # Verilog Parser
 # 

extern/smt-parser/.gitignore

@@ -0,0 +1,2 @@
+build/*
+

extern/smt-parser/CMakeLists.txt

@@ -0,0 +1,90 @@
+cmake_minimum_required(VERSION 3.8)
+
+project(smtparser VERSION 1.0 LANGUAGES C)
+
+option(SMT_PARSER_BUILD_DOCS "Build documents." OFF)
+option(SMT_PARSER_EXPORT_PACAKGE "Export package if enabled." OFF)
+option(SMT_PARSER_BUILD_YICES "Build Yices if enabled." OFF)
+
+# ------------------------------------------------------------------------
+set(SMT_PARSER_TARGET_NAME                 ${PROJECT_NAME})
+set(SMT_PARSER_CONFIG_INSTALL_DIR          "lib/cmake/${PROJECT_NAME}" CACHE INTERNAL "")
+set(SMT_PARSER_INCLUDE_INSTALL_DIR         "include")
+set(SMT_PARSER_INCLUDE_BUILD_DIR           "${PROJECT_SOURCE_DIR}/include")
+set(SMT_PARSER_TARGETS_EXPORT_NAME         "${PROJECT_NAME}Targets")
+set(SMT_PARSER_CMAKE_CONFIG_TEMPLATE       "cmake/config.cmake.in")
+set(SMT_PARSER_CMAKE_CONFIG_DIR            "${CMAKE_CURRENT_BINARY_DIR}")
+set(SMT_PARSER_CMAKE_VERSION_CONFIG_FILE   "${SMT_PARSER_CMAKE_CONFIG_DIR}/${PROJECT_NAME}ConfigVersion.camke")
+set(SMT_PARSER_CMAKE_PROJECT_CONFIG_FILE   "${SMT_PARSER_CMAKE_CONFIG_DIR}/${PROJECT_NAME}Config.cmake")
+set(SMT_PARSER_CMAKE_PROJECT_TARGETS_FILE  "${PROJECT_NAME}Targets.cmake")
+
+
+# ------------------------------------------------------------------------
+
+set(LIBRARY_NAME ${PROJECT_NAME}) 
+
+add_subdirectory(./src)
+
+
+# ------------------------------------------------------------------------
+# install
+
+include(CMakePackageConfigHelpers)
+write_basic_package_version_file(
+  ${SMT_PARSER_CMAKE_VERSION_CONFIG_FILE}
+  COMPATIBILITY AnyNewerVersion
+)
+
+configure_file(
+  ${SMT_PARSER_CMAKE_CONFIG_TEMPLATE}
+  ${SMT_PARSER_CMAKE_PROJECT_CONFIG_FILE}
+  @ONLY
+)
+
+install(
+  FILES ${SMT_PARSER_CMAKE_PROJECT_CONFIG_FILE} ${SMT_PARSER_CMAKE_VERSION_CONFIG_FILE}
+  DESTINATION ${SMT_PARSER_CONFIG_INSTALL_DIR}
+)
+
+
+
+install(
+  EXPORT ${SMT_PARSER_TARGETS_EXPORT_NAME}
+  DESTINATION ${SMT_PARSER_CONFIG_INSTALL_DIR}
+  NAMESPACE ${PROJECT_NAME}::
+  FILE ${SMT_PARSER_PROJECT_TARGETS_FILE}
+)
+
+
+export(
+  TARGETS ${LIBRARY_NAME}
+  NAMESPACE ${PROJECT_NAME}::
+  FILE ${SMT_PARSER_CMAKE_PROJECT_TARGETS_FILE}
+)
+
+if(${SMT_PARSER_EXPORT_PACKAGE})
+  export(PACKAGE ${PROJECT_NAME})
+endif()
+
+
+# ---------------------------------------------------------------------------- #
+# UNINSTALL
+# uninstall files listed in install_manifest.txt
+# ---------------------------------------------------------------------------- #
+if(NOT TARGET uninstall)
+  configure_file(
+    "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in"
+    "${CMAKE_CURRENT_BINARY_DIR}/cmake/cmake_uninstall.cmake"
+    IMMEDIATE @ONLY
+  )
+
+  add_custom_target(uninstall
+    COMMAND 
+      ${CMAKE_COMMAND} -P ${CMAKE_CURRENT_BINARY_DIR}/cmake/cmake_uninstall.cmake
+  )
+
+endif()
+
+
+# ------------------------------------------------------------------------
+

extern/smt-parser/LICENSE.txt

@@ -0,0 +1,19 @@
+Copyright (C) 2010 Alberto Griggio <griggio@fbk.eu>
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.

extern/smt-parser/Makefile.in

@@ -0,0 +1,52 @@
+YICES_DIR = /usr/local/yices-1.0.29
+
+CC = gcc
+FLEX = flex
+BISON = bison
+CFLAGS = -std=c99 -pedantic -g -Wall
+LDFLAGS = -g -lgmp -lgmpxx -lstdc++ 
+
+OBJECTS = smtlib2bisonparser.o \
+	  smtlib2flexlexer.o \
+	  smtlib2hashtable.o \
+	  smtlib2abstractparser.o \
+	  smtlib2termparser.o \
+	  smtlib2utils.o \
+	  smtlib2vector.o \
+	  smtlib2charbuf.o \
+	  smtlib2stream.o \
+	  smtlib2scanner.o
+
+YICES_OBJECTS = smtlib2yices.o \
+	        yicesmain.o
+
+all: libsmtlib2parser.a smtlib2yices
+
+clean:
+	rm -f $(OBJECTS) $(YICES_OBJECTS) libsmtlib2parser.a smtlib2yices smtlib2bisonparser.c smtlib2bisonparser.h smtlib2flexlexer.c smtlib2flexlexer.h
+
+
+smtlib2yices: libsmtlib2parser.a $(YICES_OBJECTS)
+	$(CC) $(YICES_OBJECTS) libsmtlib2parser.a $(YICES_DIR)/lib/libyices.a $(LDFLAGS) -o $@
+
+smtlib2yices.o: smtlib2yices.c
+	$(CC) $(CFLAGS) -I$(YICES_DIR)/include -c -o $@ $<
+yicesmain.o: yicesmain.c
+	$(CC) $(CFLAGS) -I$(YICES_DIR)/include -c -o $@ $<
+
+
+libsmtlib2parser.a: $(OBJECTS)
+	ar rc $@ $(OBJECTS)
+	ranlib $@
+
+
+
+%.o: %.c
+	$(CC) $(CFLAGS) -c -o $@ $<
+
+
+smtlib2bisonparser.c: smtlib2bisonparser.y smtlib2flexlexer.c
+	$(BISON) -o $@ $<
+
+smtlib2flexlexer.c: smtlib2flexlexer.l
+	$(FLEX) --header-file="smtlib2flexlexer.h" -o $@ $<

extern/smt-parser/README.txt

@@ -0,0 +1,66 @@
+A Generic Parser for SMT-LIB v2
+===============================
+
+Alberto Griggio <griggio@fbk.eu>
+
+
+This is a (complete, I think) parser/lexer for the SMT-LIB v2 language,
+implemented in Flex, Bison and C99, released under the MIT license (see
+LICENSE.txt). Besides a grammar and an abstract interface for implementing
+backends, a sample implementation using the Yices 1 solver
+(http://yices.csl.sri.com) is provided. The implementation is not 100%
+complete, but it should be enough for understanding how the interface is
+supposed to work.
+
+
+REQUIREMENTS: 
+-------------              
+
+- a C99 compiler (tested only under gcc), 
+- GNU flex >= 2.5.33
+- GNU bison (tested under bison 2.4.1)
+
+For compiling, copy Makefile.in to Makefile, edit the compilation flags and
+the YICES_DIR variable, and run make
+
+
+CONTENTS:
+---------
+
+LICENSE.txt: 
+  the license file
+
+Makefile.in: 
+  Makefile template
+
+smtlib2parserinterface.h:
+  abstract interface for implementing backends to the parser
+
+smtlib2abstractparser.h, smtlib2abstractparser.c: 
+  an abstract implementation of the parser interface, providing default
+  implementation for the callbacks and support for parsing terms  
+
+smtlib2abstractparser_private.h:
+  "protected" part of the abstract parser
+
+smtlib2bisonparser.y:
+  Bison grammar for the SMT-LIB v2 language, defining a re-entrant parser
+
+smtlib2flexlexer.l:
+  Flex definitions for a re-entrant SMT-LIB v2 lexical scanner
+
+smtlib2termparser.c, smtlib2termparser.h:
+  helper class for parsing terms and managing let bindings and definitions
+
+smtlib2charbuf.h, smtlib2charbuf.c, smtlib2genvector.h, smtlib2hashtable.c, 
+smtlib2hashtable.h, smtlib2scanner.c, smtlib2scanner.h, smtlib2stream.c,
+smtlib2stream.h, smtlib2types.h, smtlib2utils.c, smtlib2utils.h, 
+smtlib2vector.c, smtlib2vector.h:
+  several utility data structures and functions
+
+smtlib2yices.c, smtlib2yices.h, main.c: 
+  example backend using the Yices 1 SMT solver
+
+
+test1.smt2, test2.smt2, test3.smt2, test4.smt2, test5.smt2, test6.smt2:
+  small test inputs for the Yices backend

extern/smt-parser/azure-pipelines.yml

@@ -0,0 +1,56 @@
+trigger:
+- master
+
+pr:
+- master
+
+# File: azure-pipelines.yml
+
+jobs:
+
+- job: macOS
+  pool:
+    vmImage: 'macOS-10.13'
+  steps:
+  - script: |
+      brew update
+      brew install bison
+    displayName: 'package'
+  - script: |
+      export PATH="/usr/local/opt/bison/bin:$PATH"
+      export LDFLAGS="-L/usr/local/opt/bison/lib"
+      mkdir -p build 
+      cd build
+      cmake ..
+      cmake --build .
+    displayName: 'build'
+
+- job: Linux
+  pool:
+    vmImage: 'ubuntu-16.04'
+  steps:
+  - script: |
+      sudo apt-get update
+      sudo apt-get install bison
+      sudo apt-get install flex
+    displayName: 'package'
+  - script: |
+      mkdir -p build 
+      cd build
+      cmake .. 
+      cmake --build .
+    displayName: 'build'
+
+- job: Windows
+  pool:
+    vmImage: 'vs2017-win2016'
+  steps:
+  - script: |
+      choco install winflexbison3
+    displayName: 'package'
+  - script: |
+      md build 
+      cd build
+      cmake .. 
+      cmake --build .
+    displayName: 'build'