Add BTOR2 Frontend

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;
 

src/expr/term_manager_internal.h

@@ -808,9 +808,13 @@ term_ref term_manager_internal::mk_term(term_op op, iterator begin, iterator end
     SWITCH_TO_TERM(TERM_BV_NOR)
     SWITCH_TO_TERM(TERM_BV_XNOR)
     SWITCH_TO_TERM(TERM_BV_CONCAT)
+    SWITCH_TO_TERM(TERM_BV_NEG)
+    SWITCH_TO_TERM(TERM_BV_ROR)
+    SWITCH_TO_TERM(TERM_BV_ROL)
     SWITCH_TO_TERM(TERM_FUN_APP)
     SWITCH_TO_TERM(TERM_TUPLE_CONSTRUCT)
   default:
+    std::cout << "Unsupported term operation: " << op << std::endl;
     assert(false);
   }
 

src/expr/term_ops.cpp

@@ -94,6 +94,10 @@ std::ostream& operator << (std::ostream& out, term_op op) {
     SWITCH_TO_STRING(TERM_BV_UGT)
     SWITCH_TO_STRING(TERM_BV_SGT)
     SWITCH_TO_STRING(TERM_BV_SGN_EXTEND)
+    SWITCH_TO_STRING(TERM_BV_NEG)
+    SWITCH_TO_STRING(TERM_BV_EXTEND)
+    SWITCH_TO_STRING(TERM_BV_ROR)
+    SWITCH_TO_STRING(TERM_BV_ROL)
     SWITCH_TO_STRING(TERM_ARRAY_READ)
     SWITCH_TO_STRING(TERM_ARRAY_WRITE)
     SWITCH_TO_STRING(TERM_ARRAY_LAMBDA)

src/expr/term_ops.h

@@ -113,6 +113,10 @@ enum term_op {
   TERM_BV_UGT,
   TERM_BV_SGT,
   TERM_BV_SGN_EXTEND,
+  TERM_BV_NEG,
+  TERM_BV_EXTEND,
+  TERM_BV_ROR,
+  TERM_BV_ROL,
 
   // Arrays
   TERM_ARRAY_READ,

src/expr/type_computation_visitor.cpp

@@ -513,6 +513,17 @@ void type_computation_visitor::visit(term_ref t_ref) {
       else error_message << "child must be a bit-vector";
     }
     break;
+  case TERM_BV_NEG:
+    if (t.size() != 1) {
+      d_ok = false;
+      error_message << "must have 1 child";
+    } else {
+      term_ref t0 = base_type_of(t[0]);
+      d_ok = d_tm.is_bitvector_type(t0);
+      if (d_ok) t_type = t0;
+      else error_message << "child must be a bit-vector";
+    }
+    break;
   case TERM_BV_SUB:
     if (t.size() == 1) {
       term_ref t0 = base_type_of(t[0]);
@@ -658,6 +669,7 @@ void type_computation_visitor::visit(term_ref t_ref) {
     }
     break;
   case TERM_BV_SGN_EXTEND:
+  case TERM_BV_EXTEND:
     if (t.size() != 1) {
       d_ok = false;
       error_message << "must have 1 child";
@@ -1007,6 +1019,7 @@ void type_computation_visitor::visit(term_ref t_ref) {
     else error_message << "no children allowed";
     break;
   default:
+    std::cout << "Unsupported term operation: " << t.op() << std::endl;
     assert(false);
   }
 

src/parser/CMakeLists.txt

@@ -78,7 +78,7 @@ set_source_files_properties(
     COMPILE_FLAGS "-Wno-parentheses-equality -Wno-sign-compare -Wno-unused-function -Wno-unused-variable -Wno-tautological-compare -x c++"
 )
 
-set_source_fileS_properties(
+set_source_files_properties(
   aiger/aiger-1.9.4/aiger.c
   PROPERTIES
     LANGUAGE C
@@ -97,6 +97,7 @@ add_library(parser
   btor/btorLexer.c 
   btor/btor_state.cpp
   btor/btor.cpp
+  btor2/btor2.cpp
   sal/salParser.c 
   sal/salLexer.c 
   sal/sal_state.cpp

src/parser/btor/btor_state.cpp

@@ -261,13 +261,14 @@ cmd::command* btor_state::finalize() const {
   cmd::command* transition_system_define = new cmd::define_transition_system("T", transition_system);
 
   // Query
+  // We cast the roots to booleans then conjunct them
   std::vector<term_ref> bad_children;
   for (size_t i = 0; i < d_roots.size(); ++ i) {
     term_ref bad = tm().substitute_and_cache(d_roots[i], btor_to_state_var);
+    bad = tm().mk_term(TERM_EQ, bad, d_zero);
     bad_children.push_back(bad);
   }
-  term_ref property = tm().mk_or(bad_children);
-  property = tm().mk_term(TERM_EQ, property, d_zero);
+  term_ref property = tm().mk_and(bad_children);
   system::state_formula* property_formula = new system::state_formula(tm(), state_type, property);
   cmd::command* query = new cmd::query(ctx(), "T", property_formula);