From aedccbd629c5af0cbc960a170fad47f10f332da9 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 15 Mar 2022 19:25:21 +0100 Subject: [PATCH] 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 --- src/options/arith_options.toml | 4 ++-- src/smt/set_defaults.cpp | 9 +++++++-- 2 files changed, 9 insertions(+), 4 deletions(-) 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; } -- 2.30.2