diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-24 19:38:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-24 19:38:16 -0500 |
commit | e03d56b6de112cae8e9234fff16b985f0765740e (patch) | |
tree | 391fb3e8316e05c185e83623ce8fd770719a0c8f /src/options | |
parent | a33e9e4400b924f031100a9e498b2180bb025665 (diff) |
Cbqi bv ineq mode (#1273)
* Add mode for cbqi bv inequality handling.
* Implement the mode.
* Clang format
* Apply new clang format.
* Revert "Apply new clang format."
This reverts commit 1fec0ed999e45daacc4c756f11b5ecb4690f6561.
* Revert "Clang format"
This reverts commit 17042edb82d64c159aeddfe0264cd663998d0471.
* Clang format, second try.
* Revert "Clang format, second try."
This reverts commit f862c47c34bc313f5bc49a26b7586a4824e5aae0.
* Apply clang format, try 3.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/options_handler.cpp | 45 | ||||
-rw-r--r-- | src/options/options_handler.h | 3 | ||||
-rw-r--r-- | src/options/quantifiers_modes.h | 10 | ||||
-rw-r--r-- | src/options/quantifiers_options | 6 |
4 files changed, 60 insertions, 4 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index a3617ef6f..351c8b608 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -446,6 +446,23 @@ all \n\ \n\ "; +const std::string OptionsHandler::s_cbqiBvIneqModeHelp = + "\ +Modes for single invocation techniques, supported by --cbqi-bv-ineq:\n\ +\n\ +eq-slack (default) \n\ ++ Solve for the inequality using the slack value in the model, e.g.,\ + t > s becomes t = s + ( t-s )^M.\n\ +\n\ +eq-boundary \n\ ++ Solve for the boundary point of the inequality, e.g.,\ + t > s becomes t = s+1.\n\ +\n\ +keep \n\ ++ Solve for the inequality directly using side conditions for invertibility.\n\ +\n\ +"; + const std::string OptionsHandler::s_cegqiSingleInvHelp = "\ Modes for single invocation techniques, supported by --cegqi-si:\n\ \n\ @@ -772,6 +789,34 @@ theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(s } } +theory::quantifiers::CbqiBvIneqMode OptionsHandler::stringToCbqiBvIneqMode( + std::string option, std::string optarg) throw(OptionException) +{ + if (optarg == "eq-slack") + { + return theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK; + } + else if (optarg == "eq-boundary") + { + return theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY; + } + else if (optarg == "keep") + { + return theory::quantifiers::CBQI_BV_INEQ_KEEP; + } + else if (optarg == "help") + { + puts(s_cbqiBvIneqModeHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --cbqi-bv-ineq: `") + + optarg + + "'. Try --cbqi-bv-ineq help."); + } +} + theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException) { if(optarg == "none" ) { return theory::quantifiers::CEGQI_SI_MODE_NONE; diff --git a/src/options/options_handler.h b/src/options/options_handler.h index e534d8e58..c525c9e0e 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -98,6 +98,8 @@ public: theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::CbqiBvIneqMode stringToCbqiBvIneqMode( + std::string option, std::string optarg) throw(OptionException); theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); @@ -216,6 +218,7 @@ public: static const std::string s_qcfModeHelp; static const std::string s_qcfWhenModeHelp; static const std::string s_simplificationHelp; + static const std::string s_cbqiBvIneqModeHelp; static const std::string s_cegqiSingleInvHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_termDbModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 0b410e3fe..a19555987 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -149,6 +149,16 @@ enum IteLiftQuantMode { ITE_LIFT_QUANT_MODE_ALL, }; +enum CbqiBvIneqMode +{ + /** solve for inequalities using slack values in model */ + CBQI_BV_INEQ_EQ_SLACK, + /** solve for inequalities using boundary points */ + CBQI_BV_INEQ_EQ_BOUNDARY, + /** solve for inequalities directly, using side conditions */ + CBQI_BV_INEQ_KEEP, +}; + enum CegqiSingleInvMode { /** do not use single invocation techniques */ CEGQI_SI_MODE_NONE, diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 05c2512cd..0262012f6 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -337,10 +337,8 @@ option cbqiBv --cbqi-bv bool :read-write :default false use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false interleave model value instantiation with word-level inversion approach -option cbqiBvSlackIneq --cbqi-bv-slack-ineq bool :read-write :default true - use model slack values when solving inequalities with word-level inversion approach -option cbqiBvInvInDisEq --cbqi-bv-inv-in-dis-eq bool :read-write :default false - let bv inverter handle (un)signed less than nodes +option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode + choose mode for handling bit-vector inequalities with counterexample-guided instantiation ### local theory extensions options |