Add option for using bound inference for relevant assertions (#7152)

The method for discarding assertions based on bound inference is quite expensive (40% of runtime) for some benchmarks with quantified formulas from Facebook. This adds an option to disable this, which is done by default for quantified logics.

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index ce6f2169d19f378633b39a5157459f09919336bc..97fab52a0bc662850203d8b9f39dfa91fec419f2 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -417,6 +417,14 @@ name   = "Arithmetic Theory"
   name = "full"
   help = "Use all lemma schemes"
 
+[[option]]
+  name       = "nlRlvAssertBounds"
+  category   = "regular"
+  long       = "nl-rlv-assert-bounds"
+  type       = "bool"
+  default    = "false"
+  help       = "use bound inference utility to prune when an assertion is entailed by another"
+
 [[option]]
   name       = "nlExtResBound"
   category   = "regular"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 034ca30e221f20e69e9839166468c2e990e9d00d..3c35c29610d57becb80067454c97d74a0e1eaa0f 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -649,6 +649,12 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       opts.arith.nlExtTangentPlanesInterleave = true;
     }
   }
+  if (!opts.arith.nlRlvAssertBoundsWasSetByUser)
+  {
+    // use bound inference to determine when bounds are irrelevant only when
+    // the logic is quantifier-free
+    opts.arith.nlRlvAssertBounds = !logic.isQuantified();
+  }
 
   // set the default decision mode
   setDefaultDecisionMode(logic, opts);

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index f437d5007afb8b79b422cb10ec2140899803d948..db92009f4b39b47312efc87217c8eddaf45b9e0c 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -140,7 +140,8 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
       // not relevant, skip
       continue;
     }
-    if (bounds.add(lit, false))
+    // if using the bound inference utility
+    if (options().arith.nlRlvAssertBounds && bounds.add(lit, false))
     {
       continue;
     }