From e03d56b6de112cae8e9234fff16b985f0765740e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 24 Oct 2017 19:38:16 -0500 Subject: [PATCH] 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. --- src/options/options_handler.cpp | 45 +++++++++++++++++++ src/options/options_handler.h | 3 ++ src/options/quantifiers_modes.h | 10 +++++ src/options/quantifiers_options | 6 +-- src/theory/quantifiers/ceg_t_instantiator.cpp | 24 +++++++--- 5 files changed, 78 insertions(+), 10 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 diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 7620dcbc8..ad4c83919 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -917,23 +917,35 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node atom = lit.getKind() == NOT ? lit[0] : lit; bool pol = lit.getKind() != NOT; Kind k = atom.getKind(); - if ((pol && k == EQUAL) || (options::cbqiBvInvInDisEq())) { - // positively asserted equalities between bitvector terms we leave unmodifed + if (pol && k == EQUAL) + { + // positively asserted equalities between bitvector terms we always leave + // unmodified if (atom[0].getType().isBitVector()) { return lit; } + } + else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP) + { + // if option is set, disequalities and inequalities we leave unmodified + if ((k == EQUAL && atom[0].getType().isBitVector()) || k == BITVECTOR_ULT + || k == BITVECTOR_SLT) + { + return lit; + } } else { bool useSlack = false; - if (k == EQUAL) { + if (k == EQUAL && atom[0].getType().isBitVector()) + { // always use slack for disequalities useSlack = true; } else if (k == BITVECTOR_ULT || k == BITVECTOR_SLT) { - if (options::cbqiBvSlackIneq()) { + if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK) + { useSlack = true; } } else { - // others should be rewritten - Assert(false); + // others are not unhandled return Node::null(); } // for all other predicates, we convert them to a positive equality based on -- 2.30.2