From ddce3af579b12b3eb8f69baec3806bc33f4ac23c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Sep 2021 11:33:40 -0500 Subject: [PATCH] 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. --- src/options/arith_options.toml | 8 ++++++++ src/smt/set_defaults.cpp | 6 ++++++ src/theory/arith/nl/nonlinear_extension.cpp | 3 ++- 3 files changed, 16 insertions(+), 1 deletion(-) 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& 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; } -- 2.30.2