Enable nl-cov-var-elim by default, but disable with proofs (#8310)

This changes our policy for --nl-cov-var-elim. It is now enabled by default (it is only used when the coverings solver is used, though), but then disabled when proofs are enabled. Before, it was forced to be enabled when coverings were enabled in set_defaults.

Fixes cvc5/cvc5-projects#489

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 0061b316e0d1677c5e4efc1b837a70ea1bd45f09..a5e8a8a98dffcd95da2d3b636148e3a1ee37925f 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -504,8 +504,8 @@ name   = "Arithmetic Theory"
   category   = "regular"
   long       = "nl-cov-var-elim"
   type       = "bool"
-  default    = "false"
-  help       = "whether to eliminate variables using equalities before going into the cylindrical algebraic coverings solver"
+  default    = "true"
+  help       = "whether to eliminate variables using equalities before going into the cylindrical algebraic coverings solver. It can not be used when producing proofs right now."
 
 [[option]]
   name       = "nlCovPrune"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 4c1df2d05c6a4bd2aa6be3b5c0aad21313b25de2..d5fc48f2a13177d0f673fc545b6f702c999d96be 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -800,7 +800,6 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser)
     {
       opts.arith.nlCov = true;
-      opts.arith.nlCovVarElim = true;
       if (!opts.arith.nlExtWasSetByUser)
       {
         opts.arith.nlExt = options::NlExtMode::LIGHT;
@@ -817,7 +816,6 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser)
     {
       opts.arith.nlCov = true;
-      opts.arith.nlCovVarElim = true;
       if (!opts.arith.nlExtWasSetByUser)
       {
         opts.arith.nlExt = options::NlExtMode::LIGHT;
@@ -939,6 +937,13 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
                << std::endl;
     opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
   }
+  if (opts.arith.nlCovVarElim && !opts.arith.nlCovVarElimWasSetByUser)
+  {
+    verbose(1)
+        << "Disabling nl-cov-var-elim since it is incompatible with proofs."
+        << std::endl;
+    opts.arith.nlCovVarElim = false;
+  }
   return false;
 }