Ipasir backend

CMakeLists.txt

@@ -110,7 +110,7 @@ if (BUILD_PYTHON_BINDINGS)
   find_package(PythonInterp 3.5 REQUIRED)
 endif()
 
-if (BUILD_BITWUZLA OR BUILD_CVC4 OR BUILD_MSAT OR BUILD_YICES2 OR BUILD_Z3)
+if (BUILD_BITWUZLA OR BUILD_CVC4 OR BUILD_MSAT OR BUILD_YICES2 OR BUILD_Z3 OR BUILD_IPASIR)
   find_package(GMP REQUIRED)
 endif()
 
@@ -205,6 +205,21 @@ if (BUILD_YICES2)
   add_definitions(-DYICES2_HOME=${YICES2_HOME})
 endif (BUILD_YICES2)
 
+# should we build ipasir?
+option (BUILD_IPASIR
+  "Should we build the libraries for ipasir" OFF)
+
+if (BUILD_IPASIR)
+  if (NOT DEFINED IPASIR_HOME)
+    set(IPASIR_HOME "${PROJECT_SOURCE_DIR}/deps/ipasir")
+  endif()
+  add_subdirectory (ipasir)
+  set (SOLVER_BACKEND_LIBS ${SOLVER_BACKEND_LIBS} smt-switch-ipasir)
+
+  add_definitions(-DBUILD_IPASIR)
+  add_definitions(-DIPASIR_HOME=${IPASIR_HOME})
+endif (BUILD_IPASIR)
+
 if (BUILD_PYTHON_BINDINGS)
   add_subdirectory(python)
 endif()

configure.sh

@@ -18,12 +18,14 @@ Configures the CMAKE build environment.
 --msat                  build MathSAT           (default: off)
 --yices2                build yices2            (default: off)
 --z3                    build z3                (default: off)
+--ipasir                build ipasir               (default: off)
 --btor-home=STR         custom BTOR location    (default: deps/boolector)
 --bitwuzla-home=STR     custom Bitwuzla location  (default: deps/bitwuzla)
 --cvc4-home=STR         custom CVC4 location    (default: deps/CVC4)
 --msat-home=STR         custom MathSAT location (default: deps/mathsat)
 --yices2-home=STR       custom YICES2 location  (default: deps/yices2)
 --z3-home=STR           custom Z3 location      (default: deps/z3)
+--ipasir-home=STR       custom IPASIR location      (default: deps/ipasir)
 --build-dir=STR         custom build directory  (default: build)
 --debug                 build debug with debug symbols (default: off)
 --static                create static libaries (default: off)
@@ -46,12 +48,14 @@ build_cvc4=default
 build_msat=default
 build_yices2=default
 build_z3=default
+build_ipasir=default
 btor_home=default
 bitwuzla_home=default
 cvc4_home=default
 msat_home=default
 yices2_home=default
 z3_home=default
+ipasir_home=default
 static=default
 python=default
 smtlib_reader=default
@@ -90,6 +94,9 @@ do
 		--z3)
 	   		build_z3=ON
 	    	;;
+        --ipasir)
+            build_ipasir=ON
+            ;;
         --btor-home) die "missing argument to $1 (see -h)" ;;
         --btor-home=*)
             btor_home=${1##*=}
@@ -150,6 +157,16 @@ do
                 *) yices2_home=$(pwd)/$yices2_home ;; # make absolute path
             esac
             ;;
+        --ipasir-home) die "missing argument to $1 (see -h)" ;;
+        --ipasir-home=*)
+            ipasir_home=${1##*=}
+            # Check if ipasir_home is an absolute path and if not, make it
+            # absolute.
+            case $ipasir_home in
+                /*) ;;                                      # absolute path
+                *) ipasir_home=$(pwd)/$ipasir_home ;; # make absolute path
+            esac
+            ;;
         --build-dir) die "missing argument to $1 (see -h)" ;;
         --build-dir=*)
             build_dir=${1##*=}
@@ -198,6 +215,10 @@ if [ $yices2_home != default -a $build_yices2 = default ]; then
     build_yices2=ON
 fi
 
+if [ $ipasir_home != default -a $build_ipasir = default ]; then
+    build_ipasir=ON
+fi
+
 cmake_opts="-DCMAKE_BUILD_TYPE=$build_type"
 
 [ $install_prefix != default ] \
@@ -221,6 +242,9 @@ cmake_opts="-DCMAKE_BUILD_TYPE=$build_type"
 [ $build_yices2 != default ] \
     && cmake_opts="$cmake_opts -DBUILD_YICES2=$build_yices2"
 
+[ $build_ipasir != default ] \
+    && cmake_opts="$cmake_opts -DBUILD_IPASIR=$build_ipasir"
+
 [ $btor_home != default ] \
     && cmake_opts="$cmake_opts -DBTOR_HOME=$btor_home"
 
@@ -239,6 +263,9 @@ cmake_opts="-DCMAKE_BUILD_TYPE=$build_type"
 [ $yices2_home != default ] \
     && cmake_opts="$cmake_opts -DYICES2_HOME=$yices2_home"
 
+[ $ipasir_home != default ] \
+    && cmake_opts="$cmake_opts -DIPASIR_HOME=$ipasir_home"
+
 [ $static != default ] \
     && cmake_opts="$cmake_opts -DSMT_SWITCH_LIB_TYPE=STATIC"
 

contrib/setup-ipasir.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+
+IPASIR_VERSION=c10e2663b6708223fe5b5f35ff3acf609215f363
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+DEPS=$DIR/../deps
+
+mkdir -p $DEPS
+
+if [ ! -d "$DEPS/ipasir" ]; then
+    cd $DEPS
+    git clone https://github.com/biotomas/ipasir.git
+    chmod -R 777 ipasir
+    cd ipasir
+    git checkout -f $IPASIR_VERSION
+
+    ./scripts/mkall.sh
+    cd build
+    make -j$(nproc)
+    cd $DIR
+else
+    echo "$DEPS/ipasir already exists. If you want to rebuild, please remove it manually."
+fi

include/utils.h

@@ -103,6 +103,9 @@ bool is_lit(const Term & l, const Sort & boolsort);
 // Returns a string in DIMACs format for a given cnf formula
 void cnf_to_dimacs(Term cnf, std::ostringstream & y);
 
+// Converts any boolean formula to cnf, formula is the formula to be converted to a cnf
+Term to_cnf(Term formula, SmtSolver s);
+
 // -----------------------------------------------------------------------------
 
 /** \class

ipasir/CMakeLists.txt

@@ -0,0 +1,46 @@
+set(CMAKE_POSITION_INDEPENDENT_CODE ON)
+
+add_library(smt-switch-btor "${SMT_SWITCH_LIB_TYPE}"
+  "${CMAKE_CURRENT_SOURCE_DIR}/src/boolector_extensions.cpp"
+  "${CMAKE_CURRENT_SOURCE_DIR}/src/boolector_factory.cpp"
+  "${CMAKE_CURRENT_SOURCE_DIR}/src/boolector_solver.cpp"
+  "${CMAKE_CURRENT_SOURCE_DIR}/src/boolector_sort.cpp"
+  "${CMAKE_CURRENT_SOURCE_DIR}/src/boolector_term.cpp"
+  "${PROJECT_SOURCE_DIR}/contrib/memstream-0.1/memstream.c"
+  )
+target_include_directories (smt-switch-btor PUBLIC "${PROJECT_SOURCE_DIR}/include")
+target_include_directories (smt-switch-btor PUBLIC "${PROJECT_SOURCE_DIR}/contrib/memstream-0.1/")
+target_include_directories (smt-switch-btor PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/include")
+target_include_directories (smt-switch-btor PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/btor/include")
+target_include_directories (smt-switch-btor PUBLIC "${BTOR_HOME}/src")
+
+target_link_libraries(smt-switch-btor "${BTOR_HOME}/build/lib/libboolector.a")
+target_link_libraries(smt-switch-btor "${BTOR_HOME}/deps/cadical/build/libcadical.a")
+target_link_libraries(smt-switch-btor "${BTOR_HOME}/deps/btor2tools/build/libbtor2parser.a")
+target_link_libraries(smt-switch-btor smt-switch)
+target_link_libraries(smt-switch-btor pthread)
+target_link_libraries(smt-switch-btor m)
+
+if (SMT_SWITCH_LIB_TYPE STREQUAL STATIC)
+  # we want the static library to include the boolector source
+  # we need to unpack and repack the libraries
+  add_custom_target(repack-btor-static-lib
+    ALL
+    COMMAND
+      mkdir smt-switch-btor && cd smt-switch-btor && ar -x "../$<TARGET_FILE_NAME:smt-switch-btor>" && cd ../ &&
+      mkdir boolector && cd boolector && ar -x "${BTOR_HOME}/build/lib/libboolector.a" &&
+      ar -x "${BTOR_HOME}/deps/cadical/build/libcadical.a" &&
+      ar -x "${BTOR_HOME}/deps/btor2tools/build/libbtor2parser.a" && cd ../ &&
+      ar -qc "$<TARGET_FILE_NAME:smt-switch-btor>" ./boolector/*.o ./smt-switch-btor/*.o &&
+      # now clean up
+      rm -rf smt-switch-btor boolector
+    DEPENDS
+      smt-switch-btor
+    )
+endif()
+
+install(TARGETS smt-switch-btor DESTINATION lib)
+# install headers -- for expert use only
+install(DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/include/"
+  DESTINATION include/smt-switch
+  FILES_MATCHING PATTERN "*.h")

ipasir/include/boolector_extensions.h

@@ -0,0 +1,30 @@
+/*********************                                                        */
+/*! \file boolector_extensions.h
+** \verbatim
+** Top contributors (to current version):
+**   Makai Mann
+** This file is part of the smt-switch project.
+** Copyright (c) 2020 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file LICENSE in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief Helper functions for certain operations in Boolector C API
+**
+**
+**/
+
+#pragma once
+
+#include "boolector.h"
+
+namespace smt {
+BoolectorNode * custom_boolector_rotate_left(Btor * btor,
+                                             BoolectorNode * node,
+                                             uint32_t n);
+
+BoolectorNode * custom_boolector_rotate_right(Btor * btor,
+                                              BoolectorNode * node,
+                                              uint32_t n);
+}  // namespace smt
+

ipasir/include/boolector_solver.h

@@ -0,0 +1,167 @@
+/*********************                                                        */
+/*! \file boolector_solver.h
+** \verbatim
+** Top contributors (to current version):
+**   Makai Mann
+** This file is part of the smt-switch project.
+** Copyright (c) 2020 by the authors listed in the file AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved.  See the file LICENSE in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief Boolector implementation of AbsSmtSolver
+**
+**
+**/
+
+#pragma once
+
+#include <memory>
+#include <string>
+#include <unordered_set>
+#include <vector>
+
+#include "boolector_extensions.h"
+#include "boolector_sort.h"
+#include "boolector_term.h"
+
+#include "exceptions.h"
+#include "result.h"
+#include "smt.h"
+#include "sort.h"
+
+namespace smt {
+/**
+   Boolector Solver
+ */
+class BoolectorSolver : public AbsSmtSolver
+{
+ public:
+  // might have to use std::unique_ptr<Btor>(boolector_new) and move it?
+  BoolectorSolver() : AbsSmtSolver(BTOR), btor(boolector_new())
+  {
+    // set termination function -- throw an exception
+    auto throw_exception = [](const char * msg) -> void {
+      throw InternalSolverException(msg);
+    };
+    boolector_set_abort(throw_exception);
+  };
+  BoolectorSolver(const BoolectorSolver &) = delete;
+  BoolectorSolver & operator=(const BoolectorSolver &) = delete;
+  ~BoolectorSolver()
+  {
+    boolector_delete(btor);
+  };
+  void set_opt(const std::string option, const std::string value) override;
+  void set_logic(const std::string logic) override;
+  void assert_formula(const Term & t) override;
+  Result check_sat() override;
+  Result check_sat_assuming(const TermVec & assumptions) override;
+  Result check_sat_assuming_list(const TermList & assumptions) override;
+  Result check_sat_assuming_set(const UnorderedTermSet & assumptions) override;
+  void push(uint64_t num = 1) override;
+  void pop(uint64_t num = 1) override;
+  Term get_value(const Term & t) const override;
+  UnorderedTermMap get_array_values(const Term & arr,
+                                    Term & out_const_base) const override;
+  void get_unsat_assumptions(UnorderedTermSet & out) override;
+  Sort make_sort(const std::string name, uint64_t arity) const override;
+  Sort make_sort(SortKind sk) const override;
+  Sort make_sort(SortKind sk, uint64_t size) const override;
+  Sort make_sort(SortKind sk, const Sort & sort1) const override;
+  Sort make_sort(SortKind sk,
+                 const Sort & sort1,
+                 const Sort & sort2) const override;
+  Sort make_sort(SortKind sk,
+                 const Sort & sort1,
+                 const Sort & sort2,
+                 const Sort & sort3) const override;
+  Sort make_sort(SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
+  Sort make_sort(const DatatypeDecl & d) const override;
+
+  DatatypeDecl make_datatype_decl(const std::string & s) override;
+  DatatypeConstructorDecl make_datatype_constructor_decl(
+      const std::string s) override;
+  void add_constructor(DatatypeDecl & dt, const DatatypeConstructorDecl & con) const override;
+  void add_selector(DatatypeConstructorDecl & dt, const std::string & name, const Sort & s) const override;
+  void add_selector_self(DatatypeConstructorDecl & dt, const std::string & name) const override;
+  Term get_constructor(const Sort & s, std::string name) const override;
+  Term get_tester(const Sort & s, std::string name) const override;
+  Term get_selector(const Sort & s, std::string con, std::string name) const override;
+
+  Term make_term(bool b) const override;
+  Term make_term(int64_t i, const Sort & sort) const override;
+  Term make_term(const std::string val,
+                 const Sort & sort,
+                 uint64_t base = 10) const override;
+  Term make_term(const Term & val, const Sort & sort) const override;
+  Term make_symbol(const std::string name, const Sort & sort) override;
+  Term make_param(const std::string name, const Sort & sort) override;
+  /* build a new term */
+  Term make_term(Op op, const Term & t) const override;
+  Term make_term(Op op, const Term & t0, const Term & t1) const override;
+  Term make_term(Op op,
+                 const Term & t0,
+                 const Term & t1,
+                 const Term & t2) const override;
+  Term make_term(Op op, const TermVec & terms) const override;
+  void reset() override;
+  void reset_assertions() override;
+  Term substitute(const Term term,
+                  const UnorderedTermMap & substitution_map) const override;
+  // helper methods for making a term with a primitive op
+  Term apply_prim_op(PrimOp op, Term t) const;
+  Term apply_prim_op(PrimOp op, Term t0, Term t1) const;
+  Term apply_prim_op(PrimOp op, Term t0, Term t1, Term t2) const;
+  Term apply_prim_op(PrimOp op, TermVec terms) const;
+  void dump_smt2(std::string filename) const override;
+
+  // getters for solver-specific objects
+  // for interacting with third-party Boolector-specific software
+
+  Btor * get_btor() const { return btor; };
+
+ protected:
+  Btor * btor;
+  // store the names of created symbols
+  std::unordered_set<std::string> symbol_names;
+
+  bool base_context_1 = false;
+  ///< if set to true, do all solving at context 1 in the solver
+  ///< this then supports reset_assertions by popping and re-pushing
+  ///< the context. Without it, boolector does not support
+  ///< reset_assertions yet
+  ///< set this flag with set_opt("base-context-1", "true")
+  size_t context_level = 0;  ///< tracks the current solving context level
+
+  // helper functions
+  template <class I>
+  inline Result check_sat_assuming(I it, const I & end)
+  {
+    std::shared_ptr<BoolectorTerm> bt;
+    while (it != end)
+    {
+      bt = std::static_pointer_cast<BoolectorTerm>(*it);
+      assert(boolector_get_width(bt->btor, bt->node) == 1);
+      boolector_assume(btor, bt->node);
+      ++it;
+    }
+
+    int32_t res = boolector_sat(btor);
+    if (res == BOOLECTOR_SAT)
+    {
+      return Result(SAT);
+    }
+    else if (res == BOOLECTOR_UNSAT)
+    {
+      return Result(UNSAT);
+    }
+    else
+    {
+      return Result(UNKNOWN);
+    }
+  }
+};
+}  // namespace smt
+