diff options
| -rw-r--r-- | configure.ac | 14 | ||||
| -rw-r--r-- | src/prop/sat_solver_factory.cpp | 2 | ||||
| -rw-r--r-- | src/theory/bv/options_handlers.h | 42 |
3 files changed, 23 insertions, 35 deletions
diff --git a/configure.ac b/configure.ac index 9ec2bb41f..f24d284aa 100644 --- a/configure.ac +++ b/configure.ac @@ -789,18 +789,6 @@ AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1]) AC_SUBST([ABC_LDFLAGS]) AC_SUBST([ABC_LIBS]) -dnl AC_ARG_WITH( -dnl [cryptominisat], -dnl AS_HELP_STRING( -dnl [--with-cryptominisat], -dnl [use CRYPTOMINISAT sat solver] -dnl ), -dnl [case "$withval" in -dnl y|ye|yes|Y|YE|YES) cvc4_use_cryptominisat=1 ;; -dnl n|no|N|NO) cvc4_use_cryptominisat=0 ;; -dnl esac -dnl ] -dnl ) # Build with libcryptominisat AC_ARG_WITH([cryptominisat], @@ -817,7 +805,7 @@ elif test -n "$with_cryptominisat"; then AC_LINK_IFELSE( [AC_LANG_PROGRAM([#include <cryptominisat4/cryptominisat.h>], [CMSat::SATSolver test()])], - [LIBS="$LIBS -lcryptominisat4"] [have_libcryptominisat=1], + [LIBS="$LIBS -lcryptominisat4 -lm4ri"] [have_libcryptominisat=1], [AC_MSG_ERROR([libcryptominisat is not installed.])]) LDFLAGS=$SAVED_LDFLAGS else diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 02efc69d6..8409be6c2 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -15,10 +15,10 @@ **/ #include "prop/cryptominisat.h" +#include "prop/minisat/minisat.h" #include "prop/riss.h" #include "prop/glucose.h" #include "prop/sat_solver_factory.h" -#include "prop/minisat/minisat.h" #include "prop/bvminisat/bvminisat.h" diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h index e9812d9fc..b23225e2b 100644 --- a/src/theory/bv/options_handlers.h +++ b/src/theory/bv/options_handlers.h @@ -122,12 +122,12 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, if (!options::bitvectorToBool.wasSetByUser()) { options::bitvectorToBool.set(true); } - - if (!options::bvAbstraction.wasSetByUser() && - !options::skolemizeArguments.wasSetByUser()) { - options::bvAbstraction.set(true); - options::skolemizeArguments.set(true); - } + // broken currently + // if (!options::bvAbstraction.wasSetByUser() && + // !options::skolemizeArguments.wasSetByUser()) { + // options::bvAbstraction.set(true); + // options::skolemizeArguments.set(true); + // } return BITBLAST_MODE_EAGER; } else if(optarg == "help") { puts(bitblastingModeHelp.c_str()); @@ -217,11 +217,11 @@ inline SatSolverMode stringToSatSolver(std::string option, options::bitvectorToBool.set(true); } - if (!options::bvAbstraction.wasSetByUser() && - !options::skolemizeArguments.wasSetByUser()) { - options::bvAbstraction.set(true); - options::skolemizeArguments.set(true); - } + // if (!options::bvAbstraction.wasSetByUser() && + // !options::skolemizeArguments.wasSetByUser()) { + // options::bvAbstraction.set(true); + // options::skolemizeArguments.set(true); + // } return SAT_SOLVER_CRYPTOMINISAT; } else if(optarg == "riss") { @@ -240,11 +240,11 @@ inline SatSolverMode stringToSatSolver(std::string option, options::bitvectorToBool.set(true); } - if (!options::bvAbstraction.wasSetByUser() && - !options::skolemizeArguments.wasSetByUser()) { - options::bvAbstraction.set(true); - options::skolemizeArguments.set(true); - } + // if (!options::bvAbstraction.wasSetByUser() && + // !options::skolemizeArguments.wasSetByUser()) { + // options::bvAbstraction.set(true); + // options::skolemizeArguments.set(true); + // } return SAT_SOLVER_RISS; }else if(optarg == "glucose") { @@ -263,11 +263,11 @@ inline SatSolverMode stringToSatSolver(std::string option, options::bitvectorToBool.set(true); } - if (!options::bvAbstraction.wasSetByUser() && - !options::skolemizeArguments.wasSetByUser()) { - options::bvAbstraction.set(true); - options::skolemizeArguments.set(true); - } + // if (!options::bvAbstraction.wasSetByUser() && + // !options::skolemizeArguments.wasSetByUser()) { + // options::bvAbstraction.set(true); + // options::skolemizeArguments.set(true); + // } return SAT_SOLVER_GLUCOSE; } else if(optarg == "help") { puts(bvSatSolverHelp.c_str()); |