--- /dev/null
+# 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 <cryptominisat4/cryptominisat.h>],
+ [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
+
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
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])
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<uint64_t> or not. Some do, some don't.
# See src/util/hash.h.
--- /dev/null
+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)
--- /dev/null
+#!/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`
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 \
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 \
return IS_ABC_BUILD;
}
+bool Configuration::isBuiltWithCryptominisat() {
+ return IS_CRYPTOMINISAT_BUILD;
+}
+
bool Configuration::isBuiltWithReadline() {
return IS_READLINE_BUILD;
}
static bool isBuiltWithAbc();
+ static bool isBuiltWithCryptominisat();
+
static bool isBuiltWithReadline();
static bool isBuiltWithCudd();
# 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 */
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 */
};/* 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 */
# 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
#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\
// 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);
/* 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;
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);
--- /dev/null
+/********************* */
+/*! \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<CMSat::Lit> 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<CMSat::Var> 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<CMSat::Lit> 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<CMSat::lbool> 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<CMSat::Lit>& 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<CMSat::Lit>& 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
--- /dev/null
+/********************* */
+/*! \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 <cryptominisat4/cryptominisat.h>
+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<CMSat::Lit>& internal_clause);
+ static void toSatClause (std::vector<CMSat::Lit>& 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
+
+
+
+
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(); }
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
/** Check if the solver is in an inconsistent state */
virtual bool ok() const = 0;
-
+
+ virtual void setProofLog( BitVectorProof * bvp ) {}
};/* class SatSolver */
#include "prop/sat_solver_factory.h"
+#include "prop/cryptominisat.h"
#include "prop/minisat/minisat.h"
#include "prop/bvminisat/bvminisat.h"
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);
}
StatisticsRegistry* registry,
const std::string& name = "");
static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry);
+ static SatSolver* createCryptoMinisat(StatisticsRegistry* registry,
+ const std::string& name = "");
};/* class SatSolverFactory */
, 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() {
class EagerBitblaster : public TBitblaster<Node> {
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> 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;
{
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;
}
projects / cvc5.git / commitdiff