From: Gereon Kremer <gkremer@stanford.edu>
Date: Thu, 18 Nov 2021 19:15:34 +0000 (-0800)
Subject: Refactor CAD option for linear model seed (#7657)
X-Git-Tag: cvc5-1.0.0~798
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=95ad09bc87bc0d61ea6523d408e335b6b6935f80;p=cvc5.git

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.
---

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<CACInterval>& 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<CACInterval>& 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);
       }
     }