From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 1 Oct 2020 16:24:55 +0000 (+0200)
Subject: Allow to use the initial assignment for CAD (#5177)
X-Git-Tag: cvc5-1.0.0~2774
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25aaeabe85f8c3f2c6701fcd48f00f221f8dfccf;p=cvc5.git

Allow to use the initial assignment for CAD (#5177)

While the CAD subsolver already provided for a way to use the linear model to seed the model search, it was not actually used yet.
This PR now does use it, though it is disabled by a Boolean flag.
---

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index fde48d3f7..da3a8dc88 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -568,6 +568,14 @@ header = "options/arith_options.h"
   default    = "false"
   help       = "whether to use the cylindrical algebraic decomposition solver for non-linear arithmetic"
 
+[[option]]
+  name       = "nlCadUseInitial"
+  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"
+
 [[option]]
   name       = "nlICP"
   category   = "regular"
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index e1c752cd4..57a8b51df 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -19,6 +19,7 @@
 
 #ifdef CVC4_POLY_IMP
 
+#include "options/arith_options.h"
 #include "theory/arith/nl/cad/projections.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
 
@@ -80,6 +81,7 @@ void CDCAC::computeVariableOrdering()
 
 void CDCAC::retrieveInitialAssignment(NlModel& model, const Node& ran_variable)
 {
+  if (!options::nlCadUseInitial()) return;
   d_initialAssignment.clear();
   Trace("cdcac") << "Retrieving initial assignment:" << std::endl;
   for (const auto& var : d_variableOrdering)
@@ -138,7 +140,7 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector<CACInterval>& infeasible,
                                      poly::Value& sample,
                                      std::size_t cur_variable)
 {
-  if (cur_variable < d_initialAssignment.size())
+  if (options::nlCadUseInitial() && cur_variable < d_initialAssignment.size())
   {
     const poly::Value& suggested = d_initialAssignment[cur_variable];
     for (const auto& i : infeasible)
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 6ae75a837..b63a8398c 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -59,6 +59,7 @@ void CadSolver::initLastCall(const std::vector<Node>& assertions)
     d_CAC.getConstraints().addConstraint(a);
   }
   d_CAC.computeVariableOrdering();
+  d_CAC.retrieveInitialAssignment(d_model, d_ranVariable);
 #else
   Warning() << "Tried to use CadSolver but libpoly is not available. Compile "
                "with --poly."