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.

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index a3617ef6fcd5e29b1df26bbdc3d2d461417abb4b..351c8b608153b817e7bac00c5b52f6505fef1f87 100644 (file)
--- 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 e534d8e588c4c2fd20564a5bcbcd2753ef325185..c525c9e0e7c1053f77ff0dd42c1a77a64ad7a1b6 100644 (file)
--- 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 0b410e3fe1c2f44eabb516b421676a9ba13a13e7..a195559872b28d6ff8d4fd8538cb8c063b04ee60 100644 (file)
--- 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 05c2512cdb17ae6fdfd45487db9a83603f291705..0262012f691ce12bbb67f7db9dd17036eeba756d 100644 (file)
--- 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 7620dcbc8126847977fdb8a6fd6ddbbbb7c6c50a..ad4c839196dc7c0f9a66dbc1859b36d22e2dc404 100644 (file)
--- 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