Configured for linking against drat2er (#2754)

drat2er is a C/C++ project which includes support for
   * Checking DRAT proofs
   * Converting DRAT proofs to LRAT proofs
   * Converting DRAT proofs to ER proofs

It does the first 2 by using drat-trim under the hood.

I've modified our CMake configuration to allow drat2er to be linked into
CVC4, and I added a contrib script.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 099fc00fa1b0147f866945061985e9cb4aacf50c..3265830ccd1b454fd0c8cf9cfb0d583cc757eced 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -93,6 +93,7 @@ cvc4_option(USE_READLINE "Use readline for better interactive support")
 #    > for options where we don't need to detect if set by user (default: OFF)
 option(USE_CADICAL       "Use CaDiCaL SAT solver")
 option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
+option(USE_DRAT2ER       "Include drat2er for making eager BV proofs")
 option(USE_LFSC          "Use LFSC proof checker")
 option(USE_SYMFPU        "Use SymFPU for floating point support")
 option(USE_PYTHON2       "Prefer using Python 2 (for Python bindings)")
@@ -108,6 +109,7 @@ set(ANTLR_DIR         "" CACHE STRING "Set ANTLR3 install directory")
 set(CADICAL_DIR       "" CACHE STRING "Set CaDiCaL install directory")
 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
 set(CXXTEST_DIR       "" CACHE STRING "Set CxxTest install directory")
+set(DRAT2ER_DIR       "" CACHE STRING "Set drat2er install directory")
 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
 set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
@@ -410,6 +412,12 @@ if(USE_CRYPTOMINISAT)
   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 endif()
 
+if(USE_DRAT2ER)
+  set(Drat2Er_HOME ${DRAT2ER_DIR})
+  find_package(Drat2Er REQUIRED)
+  add_definitions(-DCVC4_USE_DRAT2ER)
+endif()
+
 if(USE_GLPK)
   set(GPL_LIBS "${GPL_LIBS} glpk")
   set(GLPK_HOME ${GLPK_DIR})
@@ -523,6 +531,7 @@ message("")
 print_config("ABC                  :" USE_ABC)
 print_config("CaDiCaL              :" USE_CADICAL)
 print_config("CryptoMiniSat        :" USE_CRYPTOMINISAT)
+print_config("drat2er              :" USE_DRAT2ER)
 print_config("GLPK                 :" USE_GLPK)
 print_config("LFSC                 :" USE_LFSC)
 
@@ -546,6 +555,9 @@ endif()
 if(CRYPTOMINISAT_DIR)
   message("CRYPTOMINISAT dir    : ${CRYPTOMINISAT_DIR}")
 endif()
+if(DRAT2ER_DIR)
+  message("DRAT2ER dir          : ${DRAT2ER_DIR}")
+endif()
 if(GLPK_DIR)
   message("GLPK dir             : ${GLPK_DIR}")
 endif()

diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake
new file mode 100644 (file)
index 0000000..e0bc8d4
--- /dev/null
+++ b/cmake/FindDrat2Er.cmake
@@ -0,0 +1,31 @@
+# Find drat2er
+# Drat2Er_FOUND - system has Drat2Er lib
+# Drat2Er_INCLUDE_DIR - the Drat2Er include directory
+# Drat2Er_LIBRARIES - Libraries needed to use Drat2Er
+
+
+# Check default location of Drat2Er built with contrib/get-drat2er.
+# If the user provides a directory we will not search the default paths and
+# fail if Drat2Er was not found in the specified directory.
+if(NOT Drat2Er_HOME)
+  set(Drat2Er_HOME ${PROJECT_SOURCE_DIR}/drat2er/build/install)
+endif()
+
+find_path(Drat2Er_INCLUDE_DIR
+          NAMES drat2er.h
+          PATHS ${Drat2Er_HOME}/include
+          NO_DEFAULT_PATH)
+find_library(Drat2Er_LIBRARIES
+             NAMES libdrat2er.a
+             PATHS ${Drat2Er_HOME}/lib
+             NO_DEFAULT_PATH)
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(Drat2Er
+  DEFAULT_MSG
+  Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES)
+
+mark_as_advanced(Drat2Er_INCLUDE_DIR Drat2Er_LIBRARIES)
+if(Drat2Er_LIBRARIES)
+  message(STATUS "Found Drat2Er libs: ${Drat2Er_LIBRARIES}")
+endif()

diff --git a/configure.sh b/configure.sh
index 7fa842f7086b1aefe701c3ef040fe4bc9c2d7055..e53d8caa73df42fcffcadb027328130594ff7dcf 100755 (executable)
--- a/configure.sh
+++ b/configure.sh
@@ -55,6 +55,7 @@ The following flags enable optional packages (disable with --no-<option name>).
   --abc                    use the ABC AIG library
   --cadical                use the CaDiCaL SAT solver
   --cryptominisat          use the CryptoMiniSat SAT solver
+  --drat2er                use drat2er (required for eager BV proofs)
   --lfsc                   use the LFSC proof checker
   --symfpu                 use SymFPU for floating point solver
   --portfolio              build the multithreaded portfolio version of CVC4
@@ -66,6 +67,7 @@ Optional Path to Optional Packages:
   --antlr-dir=PATH         path to ANTLR C headers and libraries
   --cadical-dir=PATH       path to top level of CaDiCaL source tree
   --cryptominisat-dir=PATH path to top level of CryptoMiniSat source tree
+  --drat2er-dir=PATH       path to the top level of the drat2er installation
   --cxxtest-dir=PATH       path to CxxTest installation
   --glpk-dir=PATH          path to top level of GLPK installation
   --gmp-dir=PATH           path to top level of GMP installation
@@ -112,6 +114,7 @@ coverage=default
 cryptominisat=default
 debug_symbols=default
 debug_context_mm=default
+drat2er=default
 dumping=default
 gpl=default
 win64=default
@@ -141,6 +144,7 @@ abc_dir=default
 antlr_dir=default
 cadical_dir=default
 cryptominisat_dir=default
+drat2er_dir=default
 cxxtest_dir=default
 glpk_dir=default
 gmp_dir=default
@@ -202,6 +206,9 @@ do
     --debug-context-mm) debug_context_mm=ON;;
     --no-debug-context-mm) debug_context_mm=OFF;;
 
+    --drat2er) drat2er=ON;;
+    --no-drat2er) drat2er=OFF;;
+
     --dumping) dumping=ON;;
     --no-dumping) dumping=OFF;;
 
@@ -297,6 +304,9 @@ do
     --cxxtest-dir) die "missing argument to $1 (try -h)" ;;
     --cxxtest-dir=*) cxxtest_dir=${1##*=} ;;
 
+    --drat2er-dir) die "missing argument to $1 (try -h)" ;;
+    --drat2er-dir=*) drat2er_dir=${1##*=} ;;
+
     --glpk-dir) die "missing argument to $1 (try -h)" ;;
     --glpk-dir=*) glpk_dir=${1##*=} ;;
 
@@ -386,6 +396,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_CLN=$cln"
 [ $cryptominisat != default ] \
   && cmake_opts="$cmake_opts -DUSE_CRYPTOMINISAT=$cryptominisat"
+[ $drat2er != default ] \
+  && cmake_opts="$cmake_opts -DUSE_DRAT2ER=$drat2er"
 [ $glpk != default ] \
   && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk"
 [ $lfsc != default ] \
@@ -408,6 +420,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DCRYPTOMINISAT_DIR=$cryptominisat_dir"
 [ "$cxxtest_dir" != default ] \
   && cmake_opts="$cmake_opts -DCXXTEST_DIR=$cxxtest_dir"
+[ "$drat2er_dir" != default ] \
+  && cmake_opts="$cmake_opts -DDRAT2ER_DIR=$drat2er_dir"
 [ "$glpk_dir" != default ] \
   && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
 [ "$gmp_dir" != default ] \

diff --git a/contrib/get-drat2er b/contrib/get-drat2er
new file mode 100755 (executable)
index 0000000..e465ab3
--- /dev/null
+++ b/contrib/get-drat2er
@@ -0,0 +1,25 @@
+#!/bin/bash
+#
+source "$(dirname "$0")/get-script-header.sh"
+if [ -e drat2er ]; then
+  echo 'error: file or directory "drat2er" exists; please move it out of the way.' >&2
+  exit 1
+fi
+
+git clone https://github.com/alex-ozdemir/drat2er.git
+
+cd drat2er
+
+git checkout api
+
+mkdir build
+
+cd build
+
+cmake .. -DCMAKE_INSTALL_PREFIX=$(pwd)/install
+
+make install
+
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure.sh --drat2er

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7ecee2dee9f5e17d0d3c8236a2089d875c19723f..889260045fb1bf0b54b2bb1a6ae57b91644b11ae 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -739,6 +739,10 @@ if(USE_CRYPTOMINISAT)
   target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
   target_include_directories(cvc4 PUBLIC ${CryptoMiniSat_INCLUDE_DIR})
 endif()
+if(USE_DRAT2ER)
+  target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
+  target_include_directories(cvc4 PUBLIC ${Drat2Er_INCLUDE_DIR})
+endif()
 if(USE_GLPK)
   target_link_libraries(cvc4 ${GLPK_LIBRARIES})
   target_include_directories(cvc4 PUBLIC ${GLPK_INCLUDE_DIR})

diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 5164d46bcafd04b7fa64ddf1e6c6f4bddd145731..77f3f5e778dd5c2a0a1dd742e4464ca92a0481a4 100644 (file)
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -126,6 +126,12 @@ namespace CVC4 {
 #  define IS_CRYPTOMINISAT_BUILD false
 #endif /* CVC4_USE_CRYPTOMINISAT */
 
+#if CVC4_USE_DRAT2ER
+#  define IS_DRAT2ER_BUILD true
+#else /* CVC4_USE_DRAT2ER */
+#  define IS_DRAT2ER_BUILD false
+#endif /* CVC4_USE_DRAT2ER */
+
 #if CVC4_USE_LFSC
 #define IS_LFSC_BUILD true
 #else /* CVC4_USE_LFSC */