From 25aaeabe85f8c3f2c6701fcd48f00f221f8dfccf Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 1 Oct 2020 18:24:55 +0200 Subject: [PATCH] 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. --- src/options/arith_options.toml | 8 ++++++++ src/theory/arith/nl/cad/cdcac.cpp | 4 +++- src/theory/arith/nl/cad_solver.cpp | 1 + 3 files changed, 12 insertions(+), 1 deletion(-) 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& 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& 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." -- 2.30.2