From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Tue, 15 Mar 2022 18:25:21 +0000 (+0100)
Subject: Enable nl-cov-var-elim by default, but disable with proofs (#8310)
X-Git-Tag: cvc5-1.0.0~255
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aedccbd629c5af0cbc960a170fad47f10f332da9;p=cvc5.git

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 0061b316e..a5e8a8a98 100644
--- 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 4c1df2d05..d5fc48f2a 100644
--- 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;
 }