From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Sep 2021 16:33:40 +0000 (-0500)
Subject: Add option for using bound inference for relevant assertions (#7152)
X-Git-Tag: cvc5-1.0.0~1259
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ddce3af579b12b3eb8f69baec3806bc33f4ac23c;p=cvc5.git

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 ce6f2169d..97fab52a0 100644
--- 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 034ca30e2..3c35c2961 100644
--- 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 f437d5007..db92009f4 100644
--- 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;
     }