From: Liana Hadarean Date: Wed, 25 May 2016 05:30:41 +0000 (-0700) Subject: Merged cryptominisat from experimental branch. X-Git-Tag: cvc5-1.0.0~6049^2~36 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2591fc4f57030b31c2c49d5c2dae9e96d3ce3afa;p=cvc5.git Merged cryptominisat from experimental branch. --- diff --git a/config/cryptominisat.m4 b/config/cryptominisat.m4 new file mode 100644 index 000000000..f7d3a1544 --- /dev/null +++ b/config/cryptominisat.m4 @@ -0,0 +1,87 @@ +# CVC4_CHECK_FOR_CRYPTOMINISAT +# ------------------ +# Look for cryptominisat and link it in, but only if user requested. +AC_DEFUN([CVC4_CHECK_FOR_CRYPTOMINISAT], [ +AC_MSG_CHECKING([whether user requested cryptominisat support]) + +have_libcryptominisat=0 +CRYPTOMINISAT_LIBS= +CRYPTOMINISAT_LDFLAGS= + +have_libcryptominisat=0 +if test "$with_cryptominisat" = no; then + AC_MSG_RESULT([no, cryptominisat disabled by user]) +elif test -n "$with_cryptominisat"; then + AC_MSG_RESULT([yes, cryptominisat requested by user]) + AC_ARG_VAR(CRYPTOMINISAT_HOME, [path to top level of cryptominisat source tree]) + AC_ARG_WITH( + [cryptominisat-dir], + AS_HELP_STRING( + [--with-cryptominisat-dir=PATH], + [path to top level of cryptominisat source tree] + ), + [CRYPTOMINISAT_HOME="$withval"], + [ if test -z "$CRYPTOMINISAT_HOME"; then + AC_MSG_FAILURE([must give --with-cryptominisat-dir=PATH or define environment variable CRYPTOMINISAT_HOME!]) + fi + ] + ) + + if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat" ; then + AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built]) + fi + + CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include" + + AC_MSG_CHECKING([how to link cryptominisat]) + + dnl TODO FIXME: + dnl For some reason the CVC4_TRY_CRYPTOMINISAT is not working correctly + CVC4_TRY_CRYPTOMINISAT_WITH([]) + CVC4_TRY_CRYPTOMINISAT_WITH([-lm4ri]) + + if test -z "$CRYPTOMINISAT_LIBS"; then + AC_MSG_FAILURE([cannot link against libcryptominisat!]) + else + AC_MSG_RESULT([$CRYPTOMINISAT_LIBS]) + have_libcryptominisat=1 + fi + + CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib" + CRYPTOMINISAT_LIBS="-lcryptominisat4 -lm4ri" + +else + AC_MSG_RESULT([no, user didn't request cryptominisat]) + with_cryptominisat=no +fi + +])# CVC4_CHECK_FOR_CRYPTOMINISAT + +# CVC4_TRY_STATIC_CRYPTOMINISAT_WITH(LIBS) +# ------------------------------ +# Try AC_CHECK_LIB(cryptominisat) with the given linking libraries +AC_DEFUN([CVC4_TRY_CRYPTOMINISAT_WITH], [ +if test -z "$CRYPTOMINISAT_LIBS"; then + AC_LANG_PUSH([C++]) + + cvc4_save_LIBS="$LIBS" + cvc4_save_LDFLAGS="$LDFLAGS" + cvc4_save_CPPFLAGS="$CPPFLAGS" + + LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib" + LIBS="-lcryptominisat4 $1" + + + AC_LINK_IFELSE( + [AC_LANG_PROGRAM([#include ], + [CMSat::SATSolver test()])], [CRYPTOMINISAT_LIBS="-lcryptominisat4 $1"], + [CRYPTOMINISAT_LIBS=]) + + LDFLAGS="$cvc4_save_LDFLAGS" + CPPFLAGS="$cvc4_save_CPPFLAGS" + LIBS="$cvc4_save_LIBS" + + AC_LANG_POP([C++]) +fi +])# CVC4_TRY_CRYPTOMINISAT_WITH + diff --git a/configure.ac b/configure.ac index c3c29db38..2f343368a 100644 --- a/configure.ac +++ b/configure.ac @@ -113,7 +113,7 @@ AC_ARG_WITH([build], if test -z "${with_build+set}"; then with_build=production fi -if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}"; then +if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}" -a -z "${with_cryptominisat+set}"; then custom_build_profile=no else custom_build_profile=yes @@ -217,6 +217,12 @@ if test -n "${with_abc+set}"; then btargs="$btargs abc" fi fi +if test -n "${with_cryptominisat+set}"; then + if test "$with_cryptominisat" = yes; then + btargs="$btargs cryptominisat" + fi +fi + AC_MSG_RESULT([$with_build]) AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects]) @@ -775,6 +781,21 @@ AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1]) AC_SUBST([ABC_LDFLAGS]) AC_SUBST([ABC_LIBS]) + +# Build with libcryptominisat +AC_ARG_WITH([cryptominisat], + [AS_HELP_STRING([--with-cryptominisat], + [use the CRYPTOMINISAT sat solver])], [], [with_cryptominisat=]) +CVC4_CHECK_FOR_CRYPTOMINISAT +if test $have_libcryptominisat -eq 1; then + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT" + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/install/include" +fi +AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1]) +AC_SUBST([CRYPTOMINISAT_LDFLAGS]) +AC_SUBST([CRYPTOMINISAT_LIBS]) + + # Check to see if this version/architecture of GNU C++ explicitly # instantiates __gnu_cxx::hash or not. Some do, some don't. # See src/util/hash.h. diff --git a/contrib/cryptominisat-4.2.0.patch b/contrib/cryptominisat-4.2.0.patch new file mode 100644 index 000000000..30b24a3cc --- /dev/null +++ b/contrib/cryptominisat-4.2.0.patch @@ -0,0 +1,12 @@ +diff -ruN orig/CMakeLists.txt new/CMakeLists.txt +--- CMakeLists.txt 2016-05-24 22:05:50.702570824 -0700 ++++ patched.txt 2016-05-24 22:05:57.778570529 -0700 +@@ -132,7 +132,7 @@ + set(CMAKE_FIND_LIBRARY_SUFFIXES ".a") + SET(Boost_USE_STATIC_LIBS ON) + set(CMAKE_EXE_LINKER_FLAGS "-static -Wl,--whole-archive -lpthread -Wl,--no-whole-archive") +- ++ add_cxx_flag_if_supported("-fPIC") + set(NOMYSQL ON) + else() + add_definitions(-DBOOST_TEST_DYN_LINK) diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4 new file mode 100755 index 000000000..a1a8cb786 --- /dev/null +++ b/contrib/get-cryptominisat4 @@ -0,0 +1,57 @@ +#!/bin/bash +# +set -e + +version="4.2.0" + +cd "$(dirname "$0")/.." + +if ! [ -e src/parser/cvc/Cvc.g ]; then + echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 + echo "but apparently:" >&2 + echo >&2 + echo " $(pwd)" >&2 + echo >&2 + echo "is not a CVC4 source tree ?!" >&2 + exit 1 +fi + +function webget { + if which wget &>/dev/null; then + wget -c -O "$2" "$1" + elif which curl &>/dev/null; then + curl "$1" >"$2" + else + echo "Can't figure out how to download from web. Please install wget or curl." >&2 + exit 1 + fi +} + +if [ -e cryptominisat4 ]; then + echo 'error: file or directory "cryptominisat4" exists; please move it out of the way.' >&2 + exit 1 +fi + +mkdir cryptominisat4 +cd cryptominisat4 +CRYPTOMINISAT_PATH=`pwd` + +webget https://github.com/msoos/cryptominisat/archive/$version.tar.gz cryptominisat-$version.tar.gz +gunzip -f cryptominisat-$version.tar.gz +tar xfv cryptominisat-$version.tar +cd cryptominisat-$version + +patch -p0 < ../../contrib/cryptominisat-4.2.0.patch +patch -p0 < ../../contrib/cryptominisat-4.2.0.second.patch + +mkdir ../build +cd ../build + +cmake -DCMAKE_INSTALL_PREFIX:PATH=$CRYPTOMINISAT_PATH/install -DSTATICCOMPILE="ON" ../cryptominisat-$version +make install -j2 + +cd ../ + +echo +echo ===================== Now configure CVC4 with ===================== +echo ./configure --with-cryptominisat --with-cryptominisat-dir=`pwd` diff --git a/src/Makefile.am b/src/Makefile.am index 908245e63..a3580989c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -109,6 +109,8 @@ libcvc4_la_SOURCES = \ prop/sat_solver_factory.cpp \ prop/sat_solver_factory.h \ prop/sat_solver_types.h \ + prop/cryptominisat.h \ + prop/cryptominisat.cpp \ prop/theory_proxy.cpp \ prop/theory_proxy.h \ smt/boolean_terms.cpp \ @@ -474,6 +476,12 @@ libcvc4_la_LIBADD += $(ABC_LIBS) libcvc4_la_LDFLAGS += $(ABC_LDFLAGS) endif +if CVC4_USE_CRYPTOMINISAT +libcvc4_la_LIBADD += $(CRYPTOMINISAT_LIBS) +libcvc4_la_LDFLAGS += $(CRYPTOMINISAT_LDFLAGS) +endif + + BUILT_SOURCES = \ theory/rewriter_tables.h \ theory/theory_traits.h \ diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index ce8967a18..db19469fd 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -134,6 +134,10 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } +bool Configuration::isBuiltWithCryptominisat() { + return IS_CRYPTOMINISAT_BUILD; +} + bool Configuration::isBuiltWithReadline() { return IS_READLINE_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 498337c4c..5d499174f 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -93,6 +93,8 @@ public: static bool isBuiltWithAbc(); + static bool isBuiltWithCryptominisat(); + static bool isBuiltWithReadline(); static bool isBuiltWithCudd(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 74ce00bdf..f0ef1a795 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -114,6 +114,12 @@ namespace CVC4 { # define IS_ABC_BUILD false #endif /* CVC4_USE_ABC */ +#if CVC4_USE_CRYPTOMINISAT +# define IS_CRYPTOMINISAT_BUILD true +#else /* CVC4_USE_CRYPTOMINISAT */ +# define IS_CRYPTOMINISAT_BUILD false +#endif /* CVC4_USE_CRYPTOMINISAT */ + #ifdef HAVE_LIBREADLINE # define IS_READLINE_BUILD true #else /* HAVE_LIBREADLINE */ diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp index 9cf47fe33..f331345f7 100644 --- a/src/options/bv_bitblast_mode.cpp +++ b/src/options/bv_bitblast_mode.cpp @@ -53,4 +53,19 @@ std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) { return out; } +std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode solver) { + switch(solver) { + case theory::bv::SAT_SOLVER_MINISAT: + out << "SAT_SOLVER_MINISAT"; + break; + case theory::bv::SAT_SOLVER_CRYPTOMINISAT: + out << "SAT_SOLVER_CRYPTOMINISAT"; + break; + default: + out << "SatSolverMode:UNKNOWN![" << unsigned(solver) << "]"; + } + + return out; +} + }/* CVC4 namespace */ diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h index 4c8c4f626..3a6474104 100644 --- a/src/options/bv_bitblast_mode.h +++ b/src/options/bv_bitblast_mode.h @@ -60,12 +60,19 @@ enum BvSlicerMode { };/* enum BvSlicerMode */ +/** Enumeration of sat solvers that can be used. */ +enum SatSolverMode { + SAT_SOLVER_MINISAT, + SAT_SOLVER_CRYPTOMINISAT, +};/* enum SatSolver */ + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode); std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode); +std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode); }/* CVC4 namespace */ diff --git a/src/options/bv_options b/src/options/bv_options index 8edc809e3..2e6fa2e7a 100644 --- a/src/options/bv_options +++ b/src/options/bv_options @@ -7,6 +7,9 @@ module BV "options/bv_options.h" Bitvector theory # Option to set the bit-blasting mode (lazy, eager) +expert-option bvSatSolver bv-sat-solver --bv-sat-solver=MODE CVC4::theory::bv::SatSolverMode :predicate satSolverEnabledBuild :handler stringToSatSolver :default CVC4::theory::bv::SAT_SOLVER_MINISAT :read-write :include "options/bv_bitblast_mode.h" + choose which sat solver to use, see --bv-sat-solver=help + option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h" choose bitblasting mode, see --bitblast=help diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 867feef6e..6a5f6cd39 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -821,6 +821,72 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) thro #endif /* CVC4_USE_ABC */ } +void OptionsHandler::satSolverEnabledBuild(std::string option, + bool value) throw(OptionException) { +#ifndef CVC4_USE_CRYPTOMINISAT + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_CRYPTOMINISAT */ +} + +void OptionsHandler::satSolverEnabledBuild(std::string option, + std::string value) throw(OptionException) { +#ifndef CVC4_USE_CRYPTOMINISAT + if(!value.empty()) { + std::stringstream ss; + ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_USE_CRYPTOMINISAT */ +} + +const std::string OptionsHandler::s_bvSatSolverHelp = "\ +Sat solvers currently supported by the --bv-sat-solver option:\n\ +\n\ +minisat (default)\n\ +\n\ +cryptominisat\n\ +"; + +theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, + std::string optarg) throw(OptionException) { + if(optarg == "minisat") { + return theory::bv::SAT_SOLVER_MINISAT; + } else if(optarg == "cryptominisat") { + + if (options::incrementalSolving() && + options::incrementalSolving.wasSetByUser()) { + throw OptionException(std::string("Cryptominsat does not support incremental mode. \n\ + Try --bv-sat-solver=minisat")); + } + + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && + options::bitblastMode.wasSetByUser()) { + throw OptionException(std::string("Cryptominsat does not support lazy bit-blsating. \n\ + Try --bv-sat-solver=minisat")); + } + if (!options::bitvectorToBool.wasSetByUser()) { + options::bitvectorToBool.set(true); + } + + // if (!options::bvAbstraction.wasSetByUser() && + // !options::skolemizeArguments.wasSetByUser()) { + // options::bvAbstraction.set(true); + // options::skolemizeArguments.set(true); + // } + return theory::bv::SAT_SOLVER_CRYPTOMINISAT; + } else if(optarg == "help") { + puts(s_bvSatSolverHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bv-sat-solver: `") + + optarg + "'. Try --bv-sat-solver=help."); + } +} + const std::string OptionsHandler::s_bitblastingModeHelp = "\ Bit-blasting modes currently supported by the --bitblast option:\n\ \n\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 8f23219eb..5db2887c0 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -107,10 +107,15 @@ public: // theory/bv/options_handlers.h void abcEnabledBuild(std::string option, bool value) throw(OptionException); void abcEnabledBuild(std::string option, std::string value) throw(OptionException); + void satSolverEnabledBuild(std::string option, bool value) throw(OptionException); + void satSolverEnabledBuild(std::string option, std::string optarg) throw(OptionException); + theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException); theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException); void setBitblastAig(std::string option, bool arg) throw(OptionException); + theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException); + // theory/booleans/options_handlers.h theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException); @@ -193,6 +198,7 @@ public: /* Help strings */ static const std::string s_bitblastingModeHelp; + static const std::string s_bvSatSolverHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; static const std::string s_cegqiFairModeHelp; diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 20724efd2..56a7c61e2 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -78,6 +78,10 @@ public: ClauseId addClause(SatClause& clause, bool removable); + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + Unreachable("Minisat does not support native XOR reasoning"); + } + SatValue propagate(); SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp new file mode 100644 index 000000000..d8f25a786 --- /dev/null +++ b/src/prop/cryptominisat.cpp @@ -0,0 +1,230 @@ +/********************* */ +/*! \file cryptominisat.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the cryptominisat for cvc4 (bitvectors). + **/ + +#include "prop/cryptominisat.h" + +#include "proof/clause_id.h" +#include "proof/sat_proof.h" + +using namespace CVC4; +using namespace prop; + +#ifdef CVC4_USE_CRYPTOMINISAT + +CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry, + const std::string& name) +: d_solver(new CMSat::SATSolver()) +, d_numVariables(0) +, d_okay(true) +, d_statistics(registry, name) +{ + d_true = newVar(); + d_false = newVar(); + + std::vector clause(1); + clause[0] = CMSat::Lit(d_true, false); + d_solver->add_clause(clause); + + clause[0] = CMSat::Lit(d_false, true); + d_solver->add_clause(clause); +} + + +CryptoMinisatSolver::~CryptoMinisatSolver() throw(AssertionException) { + delete d_solver; +} + +ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, + bool rhs, + bool removable) { + Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n"; + + if (!d_okay) { + Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n"; + return ClauseIdError; + } + + ++(d_statistics.d_xorClausesAdded); + + // ensure all sat literals have positive polarity by pushing + // the negation on the result + std::vector xor_clause; + for (unsigned i = 0; i < clause.size(); ++i) { + xor_clause.push_back(toInternalLit(clause[i]).var()); + rhs ^= clause[i].isNegated(); + } + bool res = d_solver->add_xor_clause(xor_clause, rhs); + d_okay &= res; + return ClauseIdError; +} + +ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){ + Debug("sat::cryptominisat") << "Add clause " << clause <<"\n"; + + if (!d_okay) { + Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n"; + return ClauseIdError; + } + + ++(d_statistics.d_clausesAdded); + + std::vector internal_clause; + toInternalClause(clause, internal_clause); + bool res = d_solver->add_clause(internal_clause); + d_okay &= res; + return ClauseIdError; +} + +bool CryptoMinisatSolver::ok() const { + return d_okay; +} + + +SatVariable CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ + d_solver->new_var(); + ++d_numVariables; + Assert (d_numVariables == d_solver->nVars()); + return d_numVariables - 1; +} + +SatVariable CryptoMinisatSolver::trueVar() { + return d_true; +} + +SatVariable CryptoMinisatSolver::falseVar() { + return d_false; +} + +void CryptoMinisatSolver::markUnremovable(SatLiteral lit) { + // cryptominisat supports dynamically adding back variables (?) + // so this is a no-op + return; +} + +void CryptoMinisatSolver::interrupt(){ + d_solver->interrupt_asap(); +} + +SatValue CryptoMinisatSolver::solve(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + ++d_statistics.d_statCallsToSolve; + return toSatLiteralValue(d_solver->solve()); +} + +SatValue CryptoMinisatSolver::solve(long unsigned int& resource) { + // CMSat::SalverConf conf = d_solver->getConf(); + Unreachable("Not sure how to set different limits for calls to solve in Cryptominisat"); + return solve(); +} + +SatValue CryptoMinisatSolver::value(SatLiteral l){ + const std::vector model = d_solver->get_model(); + CMSat::Var var = l.getSatVariable(); + Assert (var < model.size()); + CMSat::lbool value = model[var]; + return toSatLiteralValue(value); +} + +SatValue CryptoMinisatSolver::modelValue(SatLiteral l){ + return value(l); +} + +unsigned CryptoMinisatSolver::getAssertionLevel() const { + Unreachable("No interface to get assertion level in Cryptominisat"); + return -1; +} + +// converting from internal sat solver representation + +SatVariable CryptoMinisatSolver::toSatVariable(CMSat::Var var) { + if (var == CMSat::var_Undef) { + return undefSatVariable; + } + return SatVariable(var); +} + +CMSat::Lit CryptoMinisatSolver::toInternalLit(SatLiteral lit) { + if (lit == undefSatLiteral) { + return CMSat::lit_Undef; + } + return CMSat::Lit(lit.getSatVariable(), lit.isNegated()); +} + +SatLiteral CryptoMinisatSolver::toSatLiteral(CMSat::Lit lit) { + Assert (lit != CMSat::lit_Error); + if (lit == CMSat::lit_Undef) { + return undefSatLiteral; + } + + return SatLiteral(SatVariable(lit.var()), + lit.sign()); +} + +SatValue CryptoMinisatSolver::toSatLiteralValue(CMSat::lbool res) { + if(res == CMSat::l_True) return SAT_VALUE_TRUE; + if(res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN; + Assert(res == CMSat::l_False); + return SAT_VALUE_FALSE; +} + +void CryptoMinisatSolver::toInternalClause(SatClause& clause, + std::vector& internal_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + internal_clause.push_back(toInternalLit(clause[i])); + } + Assert(clause.size() == internal_clause.size()); +} + +void CryptoMinisatSolver::toSatClause(std::vector& clause, + SatClause& sat_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert(clause.size() == sat_clause.size()); +} + + +// Satistics for CryptoMinisatSolver + +CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry, + const std::string& prefix) : + d_registry(registry), + d_statCallsToSolve("theory::bv::"+prefix+"::cryptominisat::calls_to_solve", 0), + d_xorClausesAdded("theory::bv::"+prefix+"::cryptominisat::xor_clauses", 0), + d_clausesAdded("theory::bv::"+prefix+"::cryptominisat::clauses", 0), + d_solveTime("theory::bv::"+prefix+"::cryptominisat::solve_time"), + d_registerStats(!prefix.empty()) +{ + if (!d_registerStats) + return; + + d_registry->registerStat(&d_statCallsToSolve); + d_registry->registerStat(&d_xorClausesAdded); + d_registry->registerStat(&d_clausesAdded); + d_registry->registerStat(&d_solveTime); +} + +CryptoMinisatSolver::Statistics::~Statistics() { + if (!d_registerStats) + return; + d_registry->unregisterStat(&d_statCallsToSolve); + d_registry->unregisterStat(&d_xorClausesAdded); + d_registry->unregisterStat(&d_clausesAdded); + d_registry->unregisterStat(&d_solveTime); +} +#endif diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h new file mode 100644 index 000000000..29f8b7a2a --- /dev/null +++ b/src/prop/cryptominisat.h @@ -0,0 +1,137 @@ +/********************* */ +/*! \file cryptominisat.h + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the cryptominisat sat solver for cvc4 (bitvectors). + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "prop/sat_solver.h" + +#ifdef CVC4_USE_CRYPTOMINISAT +#include +namespace CVC4 { +namespace prop { + +class CryptoMinisatSolver : public SatSolver { + +private: + CMSat::SATSolver* d_solver; + unsigned d_numVariables; + bool d_okay; + SatVariable d_true; + SatVariable d_false; +public: + CryptoMinisatSolver(StatisticsRegistry* registry, + const std::string& name = ""); + ~CryptoMinisatSolver() throw(AssertionException); + + ClauseId addClause(SatClause& clause, bool removable); + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable); + + bool nativeXor() { return true; } + + SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); + + SatVariable trueVar(); + SatVariable falseVar(); + + void markUnremovable(SatLiteral lit); + + void interrupt(); + + SatValue solve(); + SatValue solve(long unsigned int&); + bool ok() const; + SatValue value(SatLiteral l); + SatValue modelValue(SatLiteral l); + + unsigned getAssertionLevel() const; + + + // helper methods for converting from the internal Minisat representation + + static SatVariable toSatVariable(CMSat::Var var); + static CMSat::Lit toInternalLit(SatLiteral lit); + static SatLiteral toSatLiteral(CMSat::Lit lit); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(CMSat::lbool res); + + static void toInternalClause(SatClause& clause, std::vector& internal_clause); + static void toSatClause (std::vector& clause, SatClause& sat_clause); + + class Statistics { + public: + StatisticsRegistry* d_registry; + IntStat d_statCallsToSolve; + IntStat d_xorClausesAdded; + IntStat d_clausesAdded; + TimerStat d_solveTime; + bool d_registerStats; + Statistics(StatisticsRegistry* registry, + const std::string& prefix); + ~Statistics(); + }; + + Statistics d_statistics; +}; +} // CVC4::prop +} // CVC4 + +#else // CVC4_USE_CRYPTOMINISAT + +namespace CVC4 { +namespace prop { + +class CryptoMinisatSolver : public SatSolver { + +public: + CryptoMinisatSolver(const std::string& name = "") { Unreachable(); } + /** Assert a clause in the solver. */ + ClauseId addClause(SatClause& clause, bool removable) { + Unreachable(); + } + + /** Return true if the solver supports native xor resoning */ + bool nativeXor() { Unreachable(); } + + /** Add a clause corresponding to rhs = l1 xor .. xor ln */ + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + Unreachable(); + } + + SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); } + SatVariable trueVar() { Unreachable(); } + SatVariable falseVar() { Unreachable(); } + SatValue solve() { Unreachable(); } + SatValue solve(long unsigned int&) { Unreachable(); } + void interrupt() { Unreachable(); } + SatValue value(SatLiteral l) { Unreachable(); } + SatValue modelValue(SatLiteral l) { Unreachable(); } + unsigned getAssertionLevel() const { Unreachable(); } + bool ok() const { return false;}; + + +};/* class CryptoMinisatSolver */ +} // CVC4::prop +} // CVC4 + +#endif // CVC4_USE_CRYPTOMINISAT + + + + diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 535ce1a47..ec5297bb7 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -44,6 +44,9 @@ public: void initialize(context::Context* context, TheoryProxy* theoryProxy); ClauseId addClause(SatClause& clause, bool removable); + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + Unreachable("Minisat does not support native XOR reasoning"); + } SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 92696ae25..81fb94242 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -49,6 +49,12 @@ public: virtual ClauseId addClause(SatClause& clause, bool removable) = 0; + /** Return true if the solver supports native xor resoning */ + virtual bool nativeXor() { return false; } + + /** Add a clause corresponding to rhs = l1 xor .. xor ln */ + virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0; + /** * Create a new boolean variable in the solver. * @param isTheoryAtom is this a theory atom that needs to be asserted to theory @@ -84,7 +90,8 @@ public: /** Check if the solver is in an inconsistent state */ virtual bool ok() const = 0; - + + virtual void setProofLog( BitVectorProof * bvp ) {} };/* class SatSolver */ diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 092ec72f2..7fdc44e66 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -16,6 +16,7 @@ #include "prop/sat_solver_factory.h" +#include "prop/cryptominisat.h" #include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" @@ -26,6 +27,12 @@ BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatC return new BVMinisatSatSolver(registry, mainSatContext, name); } +SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry, + const std::string& name) { +return new CryptoMinisatSolver(registry, name); +} + + DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) { return new MinisatSatSolver(registry); } diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 7cc23a8e8..a04bcaaf4 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -35,6 +35,8 @@ public: StatisticsRegistry* registry, const std::string& name = ""); static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry); + static SatSolver* createCryptoMinisat(StatisticsRegistry* registry, + const std::string& name = ""); };/* class SatSolverFactory */ diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 887daa1bd..80a9396ac 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -140,10 +140,23 @@ AigBitblaster::AigBitblaster() , d_bbAtoms() , d_aigOutputNode(NULL) { - d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); + d_nullContext = new context::Context(); + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext, + "AigBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), + "AigBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } } AigBitblaster::~AigBitblaster() { diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 5fdc549d0..f9f5361d3 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -257,7 +257,7 @@ public: class EagerBitblaster : public TBitblaster { typedef __gnu_cxx::hash_set TNodeSet; // sat solver used for bitblasting and associated CnfStream - prop::BVSatSolverInterface* d_satSolver; + prop::SatSolver* d_satSolver; BitblastingRegistrar* d_bitblastingRegistrar; context::Context* d_nullContext; prop::CnfStream* d_cnfStream; diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index a103d1f63..53fb4f94b 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -47,15 +47,30 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) { d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - - d_satSolver = prop::SatSolverFactory::createMinisat( - d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); + + switch(options::bvSatSolver()) { + case SAT_SOLVER_MINISAT: { + prop::BVSatSolverInterface* minisat = + prop::SatSolverFactory::createMinisat(d_nullContext, + smtStatisticsRegistry(), + "EagerBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + minisat->setNotify(notify); + d_satSolver = minisat; + break; + } + case SAT_SOLVER_CRYPTOMINISAT: + d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), + "EagerBitblaster"); + break; + default: + Unreachable("Unknown SAT solver type"); + } d_cnfStream = new prop::TseitinCnfStream( d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(), "EagerBitblaster"); - d_satSolver->setNotify(&d_notify); d_bvp = NULL; }