Add BTOR2 Frontend (#74)

* Adding btor2 parser with antlr, not complete

* Adding support for btor2 parser using btor2tools

* Adding cmake file and updating README to explain btor2 frontend

* Fixing include for btor2parser

* Fixing cmake settings

* Adding btor2 parsing tests and fixing bug

* Disabling array types in btor2 for now

* Correctly implementing invariants in transition systems

* Implementing way to add invar via context

* Fixing issue with multi-root btor files

* Adding btor multi-root test

---------

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>

Author: cgjohannsen

CMakeLists.txt

@@ -109,6 +109,18 @@ if (OPENSMT2_FOUND)
   include_directories(${OPENSMT2_INCLUDE_DIR})
 endif()
 
+# Find Btor2Tools
+SET(BTOR2TOOLS_HOME CACHE STRING "Btor2Tools installation directory")
+find_package(Btor2Tools)
+if (BTOR2TOOLS_FOUND)
+  add_definitions(-DWITH_BTOR2TOOLS)
+  include_directories(${BTOR2TOOLS_INCLUDE_DIRS})
+  set(CMAKE_INSTALL_RPATH "${BTOR2TOOLS_LIBRARY_DIR}")
+  set(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE)
+  set(CMAKE_BUILD_WITH_INSTALL_RPATH TRUE)
+  set(CMAKE_INSTALL_RPATH "${BTOR2TOOLS_HOME}/build/lib")
+endif()
+
 # Make sure antlr C runtime is here
 include(ExternalProject)
 ExternalProject_Add(

README.md

@@ -60,6 +60,15 @@ make check
 ```
 You can also set YICES2_HOME, OPENSMT2_HOME, or DREAL_HOME.
 
+To compile with the Btor2 frontend, ensure that you have btor2tools installed 
+(using ``contrib/install_btor2tools.sh``).
+Then provide the BTOR2TOOLS_HOME directory to ``cmake`` and build with  
+```bash
+cd build
+cmake .. -DBTOR2TOOLS_HOME=path/to/contrib/btor2tools
+make
+make check
+```
 
 To compile Sally in debug mode, build with
 ```bash

cmake/FindBtor2Tools.cmake

@@ -0,0 +1,33 @@
+# - Try to find Btor2Tools
+# Once done this will define
+#  BTOR2TOOLS_FOUND - System has Btor2Tools
+#  BTOR2TOOLS_INCLUDE_DIRS - The Btor2Tools include directories
+#  BTOR2TOOLS_LIBRARIES - The libraries needed to use Btor2Tools
+
+if (BTOR2TOOLS_HOME)
+  find_path(BTOR2TOOLS_INCLUDE_DIR btor2parser/btor2parser.h PATHS "${BTOR2TOOLS_HOME}/src" NO_DEFAULT_PATH)
+else()
+  find_path(BTOR2TOOLS_INCLUDE_DIR btor2parser/btor2parser.h)
+endif()
+
+if (SALLY_STATIC_BUILD)
+  if (BTOR2TOOLS_HOME)
+    find_library(BTOR2TOOLS_LIBRARY libbtor2parser.a btor2parser PATHS "${BTOR2TOOLS_HOME}/build/lib" NO_DEFAULT_PATH)
+  else()
+    find_library(BTOR2TOOLS_LIBRARY libbtor2parser.a btor2parser)
+  endif()
+else()
+  if (BTOR2TOOLS_HOME)
+    find_library(BTOR2TOOLS_LIBRARY btor2parser PATHS "${BTOR2TOOLS_HOME}/build/lib" NO_DEFAULT_PATH)
+  else()
+    find_library(BTOR2TOOLS_LIBRARY btor2parser)
+  endif()
+endif()
+
+set(BTOR2TOOLS_LIBRARIES ${BTOR2TOOLS_LIBRARY})
+set(BTOR2TOOLS_INCLUDE_DIRS ${BTOR2TOOLS_INCLUDE_DIR})
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(Btor2Tools DEFAULT_MSG BTOR2TOOLS_LIBRARY BTOR2TOOLS_INCLUDE_DIR)
+
+mark_as_advanced(BTOR2TOOLS_INCLUDE_DIR BTOR2TOOLS_LIBRARY) 

contrib/install_btor2tools.sh

@@ -0,0 +1,43 @@
+#!/bin/bash
+set -e
+
+echo "Installing btor2tools..."
+
+# Clone the repository
+if ! git clone https://github.com/hwmcc/btor2tools.git; then
+    echo "Error: Failed to clone btor2tools repository." >&2
+    exit 1
+fi
+
+# Navigate to btor2tools directory
+if ! pushd btor2tools; then
+    echo "Error: Failed to enter btor2tools directory." >&2
+    exit 1
+fi
+
+# Run configure script
+if ! ./configure.sh; then
+    echo "Error: Configuration failed." >&2
+    popd > /dev/null 2>&1
+    exit 1
+fi
+
+# Enter build directory
+if ! pushd build; then
+    echo "Error: Failed to enter build directory." >&2
+    popd
+    exit 1
+fi
+
+# Run make
+if ! make; then
+    echo "Error: Build failed." >&2
+    popd; popd
+    exit 1
+fi
+
+# Return to original directories
+popd
+popd
+
+echo "btor2tools installation completed successfully!"

src/CMakeLists.txt

@@ -47,18 +47,31 @@ endif()
 if (DREAL_FOUND)
   target_link_libraries(sally ${DREAL_LIBRARIES})
 endif()
+if (BTOR2TOOLS_FOUND)
+  target_link_libraries(sally -lbtor2parser)
+endif()
 
 target_link_libraries(sally ${Boost_LIBRARIES} ${GMP_LIBRARY})
 
 # Add tests
 
-file(GLOB_RECURSE regressions 
-  ${sally_SOURCE_DIR}/test/regress/*.mcmt 
-  ${sally_SOURCE_DIR}/test/regress/*.btor
-  ${sally_SOURCE_DIR}/test/regress/*.sal
+# Build the list of regression files based on available solvers
+set(regression_patterns
+  ${sally_SOURCE_DIR}/test/regress/**/*.mcmt 
+  ${sally_SOURCE_DIR}/test/regress/**/*.btor
+  ${sally_SOURCE_DIR}/test/regress/**/*.sal
 )
+
+# Add btor2 files only if Btor2Tools is found
+if (BTOR2TOOLS_FOUND)
+  list(APPEND regression_patterns ${sally_SOURCE_DIR}/test/regress/**/*.btor2)
+endif()
+
+# Get all the regression files
+file(GLOB_RECURSE regressions ${regression_patterns})
 list(SORT regressions)
 
+
 foreach(FILE ${regressions})
   # Get the options for this test
   file(READ "${FILE}.options" ALL_OPTIONS)

src/expr/bitvector.cpp

@@ -72,22 +72,28 @@ size_t bitvector::hash() const {
   return hasher.get();
 }
 
-bitvector::bitvector(const char* bits)
-: integer(bits, 2)
-, d_size(strlen(bits))
+bitvector::bitvector(const char* bits, size_t base, size_t size)
+: integer(bits, base)
 {
-  assert(d_size > 0);
+  if (size == 0) {
+    d_size = strlen(bits);
+  } else {
+    d_size = size;
+  }
   assert(sgn() >= 0);
   if (mpz_sizeinbase(d_gmp_int.get_mpz_t(), 2) > d_size) {
     mpz_fdiv_r_2exp(d_gmp_int.get_mpz_t(), d_gmp_int.get_mpz_t(), d_size);
   }
 }
 
-bitvector::bitvector(std::string bits)
-: integer(bits, 2)
-, d_size(bits.size())
+bitvector::bitvector(std::string bits, size_t base, size_t size)
+: integer(bits, base)
 {
-  assert(d_size > 0);
+  if (size == 0) {
+    d_size = bits.size();
+  } else {
+    d_size = size;
+  }
   assert(sgn() >= 0);
   if (mpz_sizeinbase(d_gmp_int.get_mpz_t(), 2) > d_size) {
     mpz_fdiv_r_2exp(d_gmp_int.get_mpz_t(), d_gmp_int.get_mpz_t(), d_size);

src/expr/bitvector.h

@@ -47,11 +47,11 @@ class bitvector : protected integer {
   /** Construct from int */
   bitvector(size_t size, long x);
 
-  /** Construct from a string representation (0 terminated) */
-  explicit bitvector(const char* bits);
+  /** Construct from a string representation ('\0' terminated) */
+  explicit bitvector(const char* bits, size_t base = 2, size_t size = 0);
 
   /** Construct from a string representation */
-  explicit bitvector(std::string bits);
+  explicit bitvector(std::string bits, size_t base = 2, size_t size = 0);
 
   /** Get the size of the bitvector */
   size_t size() const { return d_size; }

src/expr/term.cpp

@@ -140,7 +140,7 @@ void term::mk_let_cache(term_manager& tm, expr_let_cache& let_cache, std::vector
     }
     break;
   default:
-    assert(false);
+    throw exception("Unsupported let caching for operator: " + std::to_string(d_op));
   }
 
   // Record the mapping
@@ -282,7 +282,10 @@ std::string get_smt_keyword(term_op op) {
     return "bvsrem";
   case TERM_BV_SMOD:
     return "bvsmod";
-
+  case TERM_BV_ROR:
+    return "bvror";
+  case TERM_BV_ROL:
+    return "bvrol";
   case TERM_ARRAY_READ:
     return "select";
   case TERM_ARRAY_WRITE:
@@ -660,7 +663,7 @@ void term::to_stream_smt_without_let(std::ostream& out, term_manager& tm, const
     break;
   }
   default:
-    assert(false);
+    throw exception("Unsupported term operation: " + std::to_string(d_op));
   }
 }
 
@@ -695,7 +698,7 @@ std::string get_nuxmv_operator(expr::term_op op) {
   case TERM_BV_UDIV: return "/";
   case TERM_BV_UREM: return "mod";
   default:
-    assert(false);
+    throw exception("Unsupported term operation: " + std::to_string(op));
   }
   return "unknown";
 }

src/expr/term_manager.cpp

@@ -874,6 +874,10 @@ term_ref term_manager::mk_or(const std::vector<term_ref>& disjuncts) {
 
 bool term_manager::is_type(term_ref t) const {
   return d_tm->is_type(t);
+} 
+
+bool term_manager::is_boolean_type(term_ref t) const {
+  return d_tm->is_boolean_type(t);
 }
 
 bool term_manager::is_function_type(term_ref t) const {

src/expr/term_manager.h

@@ -438,6 +438,9 @@ class term_manager {
   /** Check if t is a type */
   bool is_type(term_ref t) const;
 
+  /** Check if t is a boolean type */
+  bool is_boolean_type(term_ref t) const;
+
   /** Check if t is a function type */
   bool is_function_type(term_ref t) const;