From 95ad09bc87bc0d61ea6523d408e335b6b6935f80 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 18 Nov 2021 11:15:34 -0800 Subject: [PATCH] Refactor CAD option for linear model seed (#7657) This PR implements another strategy for using the linear model in the CAD-based nonlinear solver. It stays disabled by default. --- src/options/arith_options.toml | 22 ++++++++++++++++------ src/theory/arith/nl/cad/cdcac.cpp | 9 ++++++--- 2 files changed, 22 insertions(+), 9 deletions(-) diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 3c1840455..e5f65684b 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -497,7 +497,7 @@ name = "Arithmetic Theory" long = "nl-cad" type = "bool" default = "false" - help = "whether to use the cylindrical algebraic decomposition solver for non-linear arithmetic" + help = "whether to use the cylindrical algebraic coverings solver for non-linear arithmetic" [[option]] name = "nlCadPrune" @@ -508,12 +508,22 @@ name = "Arithmetic Theory" help = "whether to prune intervals more agressively" [[option]] - name = "nlCadUseInitial" + name = "nlCadLinearModel" category = "regular" - long = "nl-cad-initial" - type = "bool" - default = "false" - help = "whether to use the linear model as initial guess for the cylindrical algebraic decomposition solver" + long = "nl-cad-linear-model=MODE" + type = "NlCadLinearModelMode" + default = "NONE" + help = "whether to use the linear model as initial guess for the cylindrical algebraic coverings solver" + help_mode = "Modes for the usage of the linear model in non-linear arithmetic." +[[option.mode.NONE]] + name = "none" + help = "Do not use linear model to seed nonlinear model" +[[option.mode.INITIAL]] + name = "initial" + help = "Use linear model to seed nonlinear model initially, discard it when it does not work" +[[option.mode.PERSISTENT]] + name = "persistent" + help = "Use linear model to seed nonlinear model whenever possible" [[option]] name = "nlCadProjection" diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 7c0f4b892..2fc77be1b 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -79,7 +79,7 @@ void CDCAC::computeVariableOrdering() void CDCAC::retrieveInitialAssignment(NlModel& model, const Node& ran_variable) { - if (!options().arith.nlCadUseInitial) return; + if (options().arith.nlCadLinearModel == options::NlCadLinearModelMode::NONE) return; d_initialAssignment.clear(); Trace("cdcac") << "Retrieving initial assignment:" << std::endl; for (const auto& var : d_variableOrdering) @@ -176,7 +176,7 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector& infeasible, poly::Value& sample, std::size_t cur_variable) { - if (options().arith.nlCadUseInitial + if (options().arith.nlCadLinearModel != options::NlCadLinearModelMode::NONE && cur_variable < d_initialAssignment.size()) { const poly::Value& suggested = d_initialAssignment[cur_variable]; @@ -184,7 +184,10 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector& infeasible, { if (poly::contains(i.d_interval, suggested)) { - d_initialAssignment.clear(); + if (options().arith.nlCadLinearModel == options::NlCadLinearModelMode::INITIAL) + { + d_initialAssignment.clear(); + } return sampleOutside(infeasible, sample); } } -- 2.30.2