diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-05-24 22:30:41 -0700 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-05-24 22:30:48 -0700 |
commit | 2591fc4f57030b31c2c49d5c2dae9e96d3ce3afa (patch) | |
tree | 0296cb4f8194aef27813ef5251e88f475c9a6ffb /src/options | |
parent | beaf8b212dfadb47328942c23a7649ab44a014cb (diff) |
Merged cryptominisat from experimental branch.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/bv_bitblast_mode.cpp | 15 | ||||
-rw-r--r-- | src/options/bv_bitblast_mode.h | 7 | ||||
-rw-r--r-- | src/options/bv_options | 3 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 66 | ||||
-rw-r--r-- | src/options/options_handler.h | 6 |
5 files changed, 97 insertions, 0 deletions
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; |