From 8f1ecaaef1ce13533a7dd8b19a3373a64f9edab4 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Mar 2022 01:37:13 +0100 Subject: [PATCH] Rename cad to coverings (#8187) The nonlinear subsolver that implements cylindrical algebraic coverings is still called cad in many places, which really was a misnomer from the beginning. This PR renames it everywhere. --- src/CMakeLists.txt | 36 +++--- src/options/arith_options.toml | 38 +++--- src/proof/lazy_tree_proof_generator.h | 12 +- src/proof/proof_rule.cpp | 4 +- src/proof/proof_rule.h | 10 +- src/smt/set_defaults.cpp | 22 ++-- .../arith/nl/{cad => coverings}/cdcac.cpp | 40 +++---- .../arith/nl/{cad => coverings}/cdcac.h | 22 ++-- .../nl/{cad => coverings}/cdcac_utils.cpp | 8 +- .../arith/nl/{cad => coverings}/cdcac_utils.h | 10 +- .../nl/{cad => coverings}/constraints.cpp | 8 +- .../arith/nl/{cad => coverings}/constraints.h | 10 +- .../{cad => coverings}/lazard_evaluation.cpp | 108 +++++++++--------- .../nl/{cad => coverings}/lazard_evaluation.h | 8 +- .../nl/{cad => coverings}/projections.cpp | 8 +- .../arith/nl/{cad => coverings}/projections.h | 10 +- .../nl/{cad => coverings}/proof_checker.cpp | 22 ++-- .../nl/{cad => coverings}/proof_checker.h | 22 ++-- .../nl/{cad => coverings}/proof_generator.cpp | 34 +++--- .../nl/{cad => coverings}/proof_generator.h | 22 ++-- .../{cad => coverings}/variable_ordering.cpp | 8 +- .../nl/{cad => coverings}/variable_ordering.h | 14 +-- .../{cad_solver.cpp => coverings_solver.cpp} | 78 ++++++------- .../nl/{cad_solver.h => coverings_solver.h} | 24 ++-- src/theory/arith/nl/nonlinear_extension.cpp | 10 +- src/theory/arith/nl/nonlinear_extension.h | 6 +- src/theory/arith/nl/poly_conversion.cpp | 12 +- src/theory/arith/nl/poly_conversion.h | 2 +- src/theory/arith/nl/strategy.cpp | 10 +- src/theory/arith/nl/strategy.h | 8 +- src/theory/inference_id.cpp | 6 +- src/theory/inference_id.h | 8 +- .../regress0/nl/issue5726-downpolys.smt2 | 2 +- .../regress0/nl/issue5726-sqfactor.smt2 | 2 +- test/unit/api/cpp/theory_arith_nl_black.cpp | 4 +- test/unit/theory/CMakeLists.txt | 2 +- ...e.cpp => theory_arith_coverings_white.cpp} | 63 +++++----- 37 files changed, 356 insertions(+), 357 deletions(-) rename src/theory/arith/nl/{cad => coverings}/cdcac.cpp (95%) rename src/theory/arith/nl/{cad => coverings}/cdcac.h (93%) rename src/theory/arith/nl/{cad => coverings}/cdcac_utils.cpp (98%) rename src/theory/arith/nl/{cad => coverings}/cdcac_utils.h (94%) rename src/theory/arith/nl/{cad => coverings}/constraints.cpp (93%) rename src/theory/arith/nl/{cad => coverings}/constraints.h (90%) rename src/theory/arith/nl/{cad => coverings}/lazard_evaluation.cpp (89%) rename src/theory/arith/nl/{cad => coverings}/lazard_evaluation.h (94%) rename src/theory/arith/nl/{cad => coverings}/projections.cpp (93%) rename src/theory/arith/nl/{cad => coverings}/projections.h (90%) rename src/theory/arith/nl/{cad => coverings}/proof_checker.cpp (67%) rename src/theory/arith/nl/{cad => coverings}/proof_checker.h (69%) rename src/theory/arith/nl/{cad => coverings}/proof_generator.cpp (87%) rename src/theory/arith/nl/{cad => coverings}/proof_generator.h (88%) rename src/theory/arith/nl/{cad => coverings}/variable_ordering.cpp (95%) rename src/theory/arith/nl/{cad => coverings}/variable_ordering.h (81%) rename src/theory/arith/nl/{cad_solver.cpp => coverings_solver.cpp} (68%) rename src/theory/arith/nl/{cad_solver.h => coverings_solver.h} (85%) rename test/unit/theory/{theory_arith_cad_white.cpp => theory_arith_coverings_white.cpp} (89%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ac8b64293..e29b234ba 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -410,24 +410,24 @@ libcvc5_add_sources( theory/arith/linear_equality.h theory/arith/matrix.cpp theory/arith/matrix.h - theory/arith/nl/cad_solver.cpp - theory/arith/nl/cad_solver.h - theory/arith/nl/cad/cdcac.cpp - theory/arith/nl/cad/cdcac.h - theory/arith/nl/cad/cdcac_utils.cpp - theory/arith/nl/cad/cdcac_utils.h - theory/arith/nl/cad/constraints.cpp - theory/arith/nl/cad/constraints.h - theory/arith/nl/cad/lazard_evaluation.cpp - theory/arith/nl/cad/lazard_evaluation.h - theory/arith/nl/cad/projections.cpp - theory/arith/nl/cad/projections.h - theory/arith/nl/cad/proof_checker.cpp - theory/arith/nl/cad/proof_checker.h - theory/arith/nl/cad/proof_generator.cpp - theory/arith/nl/cad/proof_generator.h - theory/arith/nl/cad/variable_ordering.cpp - theory/arith/nl/cad/variable_ordering.h + theory/arith/nl/coverings_solver.cpp + theory/arith/nl/coverings_solver.h + theory/arith/nl/coverings/cdcac.cpp + theory/arith/nl/coverings/cdcac.h + theory/arith/nl/coverings/cdcac_utils.cpp + theory/arith/nl/coverings/cdcac_utils.h + theory/arith/nl/coverings/constraints.cpp + theory/arith/nl/coverings/constraints.h + theory/arith/nl/coverings/lazard_evaluation.cpp + theory/arith/nl/coverings/lazard_evaluation.h + theory/arith/nl/coverings/projections.cpp + theory/arith/nl/coverings/projections.h + theory/arith/nl/coverings/proof_checker.cpp + theory/arith/nl/coverings/proof_checker.h + theory/arith/nl/coverings/proof_generator.cpp + theory/arith/nl/coverings/proof_generator.h + theory/arith/nl/coverings/variable_ordering.cpp + theory/arith/nl/coverings/variable_ordering.h theory/arith/nl/equality_substitution.cpp theory/arith/nl/equality_substitution.h theory/arith/nl/ext/constraint.cpp diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 5ec842f1a..d76f6c973 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -492,34 +492,34 @@ name = "Arithmetic Theory" help = "whether to use simple rounding, similar to a unit-cube test, for integers" [[option]] - name = "nlCad" + name = "nlCov" category = "regular" - long = "nl-cad" + long = "nl-cov" type = "bool" default = "false" help = "whether to use the cylindrical algebraic coverings solver for non-linear arithmetic" [[option]] - name = "nlCadVarElim" + name = "nlCovVarElim" category = "regular" - long = "nl-cad-var-elim" + long = "nl-cov-var-elim" type = "bool" default = "false" help = "whether to eliminate variables using equalities before going into the cylindrical algebraic coverings solver" [[option]] - name = "nlCadPrune" + name = "nlCovPrune" category = "regular" - long = "nl-cad-prune" + long = "nl-cov-prune" type = "bool" default = "false" help = "whether to prune intervals more agressively" [[option]] - name = "nlCadLinearModel" + name = "nlCovLinearModel" category = "regular" - long = "nl-cad-linear-model=MODE" - type = "NlCadLinearModelMode" + long = "nl-cov-linear-model=MODE" + type = "nlCovLinearModelMode" default = "NONE" help = "whether to use the linear model as initial guess for the cylindrical algebraic coverings solver" help_mode = "Modes for the usage of the linear model in non-linear arithmetic." @@ -534,13 +534,13 @@ name = "Arithmetic Theory" help = "Use linear model to seed nonlinear model whenever possible" [[option]] - name = "nlCadProjection" + name = "nlCovProjection" category = "expert" - long = "nl-cad-proj=MODE" - type = "NlCadProjectionMode" + long = "nl-cov-proj=MODE" + type = "nlCovProjectionMode" default = "MCCALLUM" - help = "choose the CAD projection operator" - help_mode = "Modes for the CAD projection operator in non-linear arithmetic." + help = "choose the Coverings projection operator" + help_mode = "Modes for the Coverings projection operator in non-linear arithmetic." [[option.mode.MCCALLUM]] name = "mccallum" help = "McCallum's projection operator." @@ -552,13 +552,13 @@ name = "Arithmetic Theory" help = "A modification of Lazard's projection operator." [[option]] - name = "nlCadLifting" + name = "nlCovLifting" category = "expert" - long = "nl-cad-lift=MODE" - type = "NlCadLiftingMode" + long = "nl-cov-lift=MODE" + type = "nlCovLiftingMode" default = "REGULAR" - help = "choose the CAD lifting mode" - help_mode = "Modes for the CAD lifting in non-linear arithmetic." + help = "choose the Coverings lifting mode" + help_mode = "Modes for the Coverings lifting in non-linear arithmetic." [[option.mode.REGULAR]] name = "regular" help = "Regular lifting." diff --git a/src/proof/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h index 1863c739f..4f603fc2d 100644 --- a/src/proof/lazy_tree_proof_generator.h +++ b/src/proof/lazy_tree_proof_generator.h @@ -71,13 +71,13 @@ struct TreeProofNode * * Consider the example x*x<1 and x>2 and the intended proof * (SCOPE - * (ARITH_NL_CAD_SPLIT + * (ARITH_NL_COVERING_RECURSIVE * (SCOPE - * (ARITH_NL_CAD_DIRECT (x<=2 and x>2) ==> false) + * (ARITH_NL_COVERING_DIRECT (x<=2 and x>2) ==> false) * :args [x<=2] * ) * (SCOPE - * (ARITH_NL_CAD_DIRECT (x>=1 and x*x<1) ==> false) + * (ARITH_NL_COVERING_DIRECT (x>=1 and x*x<1) ==> false) * :args [x>=1] * ) * ) @@ -104,7 +104,7 @@ struct TreeProofNode * openChild(); * setCurrent(SCOPE, {}, {}, false); * openChild(); - * setCurrent(CAD_DIRECT, {x>2}, {}, false); + * setCurrent(ARITH_NL_COVERING_DIRECT, {x>2}, {}, false); * closeChild(); * getCurrent().args = {x<=2}; * closeChild(); @@ -112,12 +112,12 @@ struct TreeProofNode * openChild(); * setCurrent(SCOPE, {}, {}, false); * openChild(); - * setCurrent(CAD_DIRECT, {x*x<1}, {}, false); + * setCurrent(ARITH_NL_COVERING_DIRECT, {x*x<1}, {}, false); * closeChild(); * getCurrent().args = {x>=1}; * closeChild(); * // Finish split - * setCurrent(CAD_SPLIT, {}, {}, false); + * setCurrent(ARITH_NL_COVERING_RECURSIVE, {}, {}, false); * closeChild(); * closeChild(); * diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 9bd714161..fd143350c 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -200,8 +200,8 @@ const char* toString(PfRule id) return "ARITH_TRANS_SINE_APPROX_BELOW_NEG"; case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS: return "ARITH_TRANS_SINE_APPROX_BELOW_POS"; - case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT"; - case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; + case PfRule::ARITH_NL_COVERING_DIRECT: return "ARITH_NL_COVERING_DIRECT"; + case PfRule::ARITH_NL_COVERING_RECURSIVE: return "ARITH_NL_COVERING_RECURSIVE"; //================================================= External rules case PfRule::LFSC_RULE: return "LFSC_RULE"; case PfRule::ALETHE_RULE: return "ALETHE_RULE"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index eaa92c02c..5028cba1b 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -1379,7 +1379,7 @@ enum class PfRule : uint32_t // secant of p from l to u. ARITH_TRANS_SINE_APPROX_BELOW_POS, - // ================ CAD Lemmas + // ================ Coverings Lemmas // We use IRP for IndexedRootPredicate. // // A formula "Interval" describes that a variable (xn is none is given) is @@ -1396,7 +1396,7 @@ enum class PfRule : uint32_t // A formula "Covering" is a set of Intervals, implying that xn can be in // neither of these intervals. To be a covering (of the real line), the union // of these intervals should be the real numbers. - // ======== CAD direct conflict + // ======== Coverings direct conflict // Children (Cell, A) // --------------------- // Conclusion: (false) @@ -1404,15 +1404,15 @@ enum class PfRule : uint32_t // over a Cell (in variables x1...xn). It derives that A evaluates to false // over the Cell. In the actual algorithm, it means that xn can not be in the // topmost interval of the Cell. - ARITH_NL_CAD_DIRECT, - // ======== CAD recursive interval + ARITH_NL_COVERING_DIRECT, + // ======== Coverings recursive interval // Children (Cell, Covering) // --------------------- // Conclusion: (false) // A recursive interval is generated from a Covering (for xn) over a Cell // (in variables x1...xn-1). It generates the conclusion that no xn exists // that extends the Cell and satisfies all assumptions. - ARITH_NL_CAD_RECURSIVE, + ARITH_NL_COVERING_RECURSIVE, //================================================ Place holder for Lfsc rules // ======== Lfsc rule diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index c3008f2dd..bc5ab5f08 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -798,10 +798,10 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const #ifdef CVC5_USE_POLY if (logic == LogicInfo("QF_UFNRA")) { - if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) + if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser) { - opts.arith.nlCad = true; - opts.arith.nlCadVarElim = true; + opts.arith.nlCov = true; + opts.arith.nlCovVarElim = true; if (!opts.arith.nlExtWasSetByUser) { opts.arith.nlExt = options::NlExtMode::LIGHT; @@ -815,10 +815,10 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const else if (logic.isQuantified() && logic.isTheoryEnabled(theory::THEORY_ARITH) && logic.areRealsUsed() && !logic.areIntegersUsed()) { - if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser) + if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser) { - opts.arith.nlCad = true; - opts.arith.nlCadVarElim = true; + opts.arith.nlCov = true; + opts.arith.nlCovVarElim = true; if (!opts.arith.nlExtWasSetByUser) { opts.arith.nlExt = options::NlExtMode::LIGHT; @@ -826,18 +826,18 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } } #else - if (opts.arith.nlCad) + if (opts.arith.nlCov) { - if (opts.arith.nlCadWasSetByUser) + if (opts.arith.nlCovWasSetByUser) { throw OptionException( - "Cannot use --nl-cad without configuring with --poly."); + "Cannot use --nl-cov without configuring with --poly."); } else { - verbose(1) << "Cannot use --nl-cad without configuring with --poly." + verbose(1) << "Cannot use --nl-cov without configuring with --poly." << std::endl; - opts.arith.nlCad = false; + opts.arith.nlCov = false; opts.arith.nlExt = options::NlExtMode::FULL; } } diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/coverings/cdcac.cpp similarity index 95% rename from src/theory/arith/nl/cad/cdcac.cpp rename to src/theory/arith/nl/coverings/cdcac.cpp index 989144729..8091964d7 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/coverings/cdcac.cpp @@ -14,14 +14,14 @@ * https://arxiv.org/pdf/2003.05633.pdf. */ -#include "theory/arith/nl/cad/cdcac.h" +#include "theory/arith/nl/coverings/cdcac.h" #ifdef CVC5_POLY_IMP #include "options/arith_options.h" -#include "theory/arith/nl/cad/lazard_evaluation.h" -#include "theory/arith/nl/cad/projections.h" -#include "theory/arith/nl/cad/variable_ordering.h" +#include "theory/arith/nl/coverings/lazard_evaluation.h" +#include "theory/arith/nl/coverings/projections.h" +#include "theory/arith/nl/coverings/variable_ordering.h" #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" @@ -41,7 +41,7 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { CDCAC::CDCAC(Env& env, const std::vector& ordering) : EnvObj(env), d_variableOrdering(ordering) @@ -49,7 +49,7 @@ CDCAC::CDCAC(Env& env, const std::vector& ordering) if (d_env.isTheoryProofProducing()) { d_proof.reset( - new CADProofGenerator(userContext(), d_env.getProofNodeManager())); + new CoveringsProofGenerator(userContext(), d_env.getProofNodeManager())); } } @@ -79,7 +79,7 @@ void CDCAC::computeVariableOrdering() void CDCAC::retrieveInitialAssignment(NlModel& model, const Node& ran_variable) { - if (options().arith.nlCadLinearModel == options::NlCadLinearModelMode::NONE) return; + if (options().arith.nlCovLinearModel == options::nlCovLinearModelMode::NONE) return; d_initialAssignment.clear(); Trace("cdcac") << "Retrieving initial assignment:" << std::endl; for (const auto& var : d_variableOrdering) @@ -121,8 +121,8 @@ std::vector CDCAC::getUnsatIntervals(std::size_t cur_variable) Trace("cdcac") << "Infeasible intervals for " << p << " " << sc << " 0 over " << d_assignment << std::endl; std::vector intervals; - if (options().arith.nlCadLifting - == options::NlCadLiftingMode::LAZARD) + if (options().arith.nlCovLifting + == options::nlCovLiftingMode::LAZARD) { intervals = le.infeasibleRegions(p, sc); if (Trace.isOn("cdcac")) @@ -167,7 +167,7 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector& infeasible, poly::Value& sample, std::size_t cur_variable) { - if (options().arith.nlCadLinearModel != options::NlCadLinearModelMode::NONE + if (options().arith.nlCovLinearModel != options::nlCovLinearModelMode::NONE && cur_variable < d_initialAssignment.size()) { const poly::Value& suggested = d_initialAssignment[cur_variable]; @@ -175,7 +175,7 @@ bool CDCAC::sampleOutsideWithInitial(const std::vector& infeasible, { if (poly::contains(i.d_interval, suggested)) { - if (options().arith.nlCadLinearModel == options::NlCadLinearModelMode::INITIAL) + if (options().arith.nlCovLinearModel == options::nlCovLinearModelMode::INITIAL) { d_initialAssignment.clear(); } @@ -308,13 +308,13 @@ PolyVector CDCAC::requiredCoefficients(const poly::Polynomial& p) << "Original: " << requiredCoefficientsOriginal(p, d_assignment) << std::endl; } - switch (options().arith.nlCadProjection) + switch (options().arith.nlCovProjection) { - case options::NlCadProjectionMode::MCCALLUM: + case options::nlCovProjectionMode::MCCALLUM: return requiredCoefficientsOriginal(p, d_assignment); - case options::NlCadProjectionMode::LAZARD: + case options::nlCovProjectionMode::LAZARD: return requiredCoefficientsLazard(p, d_assignment); - case options::NlCadProjectionMode::LAZARDMOD: + case options::nlCovProjectionMode::LAZARDMOD: return requiredCoefficientsLazardModified( p, d_assignment, d_constraints.varMapper(), d_env.getRewriter()); default: @@ -331,7 +331,7 @@ PolyVector CDCAC::constructCharacterization(std::vector& intervals) for (std::size_t i = 0, n = intervals.size(); i < n - 1; ++i) { - cad::makeFinestSquareFreeBasis(intervals[i], intervals[i + 1]); + coverings::makeFinestSquareFreeBasis(intervals[i], intervals[i + 1]); } for (const auto& i : intervals) @@ -702,7 +702,7 @@ bool CDCAC::hasRootBelow(const poly::Polynomial& p, void CDCAC::pruneRedundantIntervals(std::vector& intervals) { cleanIntervals(intervals); - if (options().arith.nlCadPrune) + if (options().arith.nlCovPrune) { if (Trace.isOn("cdcac")) { @@ -738,7 +738,7 @@ void CDCAC::pruneRedundantIntervals(std::vector& intervals) void CDCAC::prepareRootIsolation(LazardEvaluation& le, size_t cur_variable) const { - if (options().arith.nlCadLifting == options::NlCadLiftingMode::LAZARD) + if (options().arith.nlCovLifting == options::nlCovLiftingMode::LAZARD) { for (size_t vid = 0; vid < cur_variable; ++vid) { @@ -752,14 +752,14 @@ void CDCAC::prepareRootIsolation(LazardEvaluation& le, std::vector CDCAC::isolateRealRoots( LazardEvaluation& le, const poly::Polynomial& p) const { - if (options().arith.nlCadLifting == options::NlCadLiftingMode::LAZARD) + if (options().arith.nlCovLifting == options::nlCovLiftingMode::LAZARD) { return le.isolateRealRoots(p); } return poly::isolate_real_roots(p, d_assignment); } -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/coverings/cdcac.h similarity index 93% rename from src/theory/arith/nl/cad/cdcac.h rename to src/theory/arith/nl/coverings/cdcac.h index 8317c0813..e7f57095d 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/coverings/cdcac.h @@ -16,8 +16,8 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_H -#define CVC5__THEORY__ARITH__NL__CAD__CDCAC_H +#ifndef CVC5__THEORY__ARITH__NL__COVERINGS__CDCAC_H +#define CVC5__THEORY__ARITH__NL__COVERINGS__CDCAC_H #ifdef CVC5_POLY_IMP @@ -27,11 +27,11 @@ #include "smt/env.h" #include "smt/env_obj.h" -#include "theory/arith/nl/cad/cdcac_utils.h" -#include "theory/arith/nl/cad/constraints.h" -#include "theory/arith/nl/cad/lazard_evaluation.h" -#include "theory/arith/nl/cad/proof_generator.h" -#include "theory/arith/nl/cad/variable_ordering.h" +#include "theory/arith/nl/coverings/cdcac_utils.h" +#include "theory/arith/nl/coverings/constraints.h" +#include "theory/arith/nl/coverings/lazard_evaluation.h" +#include "theory/arith/nl/coverings/proof_generator.h" +#include "theory/arith/nl/coverings/variable_ordering.h" namespace cvc5 { namespace theory { @@ -40,7 +40,7 @@ namespace nl { class NlModel; -namespace cad { +namespace coverings { /** * This class implements Cylindrical Algebraic Coverings as presented in @@ -159,7 +159,7 @@ class CDCAC : protected EnvObj ProofGenerator* closeProof(const std::vector& assertions); /** Get the proof generator */ - CADProofGenerator* getProof() { return d_proof.get(); } + CoveringsProofGenerator* getProof() { return d_proof.get(); } private: /** Check whether proofs are enabled */ @@ -229,13 +229,13 @@ class CDCAC : protected EnvObj std::vector d_initialAssignment; /** The proof generator */ - std::unique_ptr d_proof; + std::unique_ptr d_proof; /** The next interval id */ size_t d_nextIntervalId = 1; }; -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/coverings/cdcac_utils.cpp similarity index 98% rename from src/theory/arith/nl/cad/cdcac_utils.cpp rename to src/theory/arith/nl/coverings/cdcac_utils.cpp index f5723a634..ae1abe9d0 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.cpp +++ b/src/theory/arith/nl/coverings/cdcac_utils.cpp @@ -13,19 +13,19 @@ * Implements utilities for cdcac. */ -#include "theory/arith/nl/cad/cdcac_utils.h" +#include "theory/arith/nl/coverings/cdcac_utils.h" #ifdef CVC5_POLY_IMP #include -#include "theory/arith/nl/cad/projections.h" +#include "theory/arith/nl/coverings/projections.h" namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { using namespace poly; @@ -457,7 +457,7 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs) rhs.d_downPolys.reduce(); } -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/coverings/cdcac_utils.h similarity index 94% rename from src/theory/arith/nl/cad/cdcac_utils.h rename to src/theory/arith/nl/coverings/cdcac_utils.h index c53e8fbce..16c01fe62 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.h +++ b/src/theory/arith/nl/coverings/cdcac_utils.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H -#define CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H +#ifndef CVC5__THEORY__ARITH__NL__COVERINGS__CDCAC_UTILS_H +#define CVC5__THEORY__ARITH__NL__COVERINGS__CDCAC_UTILS_H #ifdef CVC5_POLY_IMP @@ -25,13 +25,13 @@ #include #include "expr/node.h" -#include "theory/arith/nl/cad/projections.h" +#include "theory/arith/nl/coverings/projections.h" namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { /** * An interval as specified in section 4.1 of @@ -104,7 +104,7 @@ bool sampleOutside(const std::vector& infeasible, */ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs); -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/coverings/constraints.cpp similarity index 93% rename from src/theory/arith/nl/cad/constraints.cpp rename to src/theory/arith/nl/coverings/constraints.cpp index 628859a8f..d857113a3 100644 --- a/src/theory/arith/nl/cad/constraints.cpp +++ b/src/theory/arith/nl/coverings/constraints.cpp @@ -10,10 +10,10 @@ * directory for licensing information. * **************************************************************************** * - * Implements a container for CAD constraints. + * Implements a container for coverings constraints. */ -#include "theory/arith/nl/cad/constraints.h" +#include "theory/arith/nl/coverings/constraints.h" #ifdef CVC5_POLY_IMP @@ -26,7 +26,7 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { void Constraints::addConstraint(const poly::Polynomial& lhs, poly::SignCondition sc, @@ -74,7 +74,7 @@ void Constraints::sortConstraints() } } -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/coverings/constraints.h similarity index 90% rename from src/theory/arith/nl/cad/constraints.h rename to src/theory/arith/nl/coverings/constraints.h index 4321800f2..7fe521a1e 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/coverings/constraints.h @@ -10,13 +10,13 @@ * directory for licensing information. * **************************************************************************** * - * Implements a container for CAD constraints. + * Implements a container for coverings constraints. */ #include "cvc5_private.h" -#ifndef CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H -#define CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H +#ifndef CVC5__THEORY__ARITH__NL__COVERINGS__CONSTRAINTS_H +#define CVC5__THEORY__ARITH__NL__COVERINGS__CONSTRAINTS_H #ifdef CVC5_POLY_IMP @@ -31,7 +31,7 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { class Constraints { @@ -82,7 +82,7 @@ class Constraints void sortConstraints(); }; -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/lazard_evaluation.cpp b/src/theory/arith/nl/coverings/lazard_evaluation.cpp similarity index 89% rename from src/theory/arith/nl/cad/lazard_evaluation.cpp rename to src/theory/arith/nl/coverings/lazard_evaluation.cpp index 91d775d16..3d60e8677 100644 --- a/src/theory/arith/nl/cad/lazard_evaluation.cpp +++ b/src/theory/arith/nl/coverings/lazard_evaluation.cpp @@ -1,4 +1,4 @@ -#include "theory/arith/nl/cad/lazard_evaluation.h" +#include "theory/arith/nl/coverings/lazard_evaluation.h" #ifdef CVC5_POLY_IMP @@ -13,18 +13,18 @@ #include -namespace cvc5::theory::arith::nl::cad { +namespace cvc5::theory::arith::nl::coverings { struct LazardEvaluationStats { IntStat d_directAssignments = - smtStatisticsRegistry().registerInt("theory::arith::cad::lazard-direct"); + smtStatisticsRegistry().registerInt("theory::arith::coverings::lazard-direct"); IntStat d_ranAssignments = - smtStatisticsRegistry().registerInt("theory::arith::cad::lazard-rans"); + smtStatisticsRegistry().registerInt("theory::arith::coverings::lazard-rans"); IntStat d_evaluations = - smtStatisticsRegistry().registerInt("theory::arith::cad::lazard-evals"); + smtStatisticsRegistry().registerInt("theory::arith::coverings::lazard-evals"); IntStat d_reductions = - smtStatisticsRegistry().registerInt("theory::arith::cad::lazard-reduce"); + smtStatisticsRegistry().registerInt("theory::arith::coverings::lazard-reduce"); }; struct LazardEvaluationState; @@ -263,7 +263,7 @@ struct LazardEvaluationState */ CoCoA::RingElem pushDownJ(const CoCoA::RingElem& p, size_t i) const { - Trace("cad::lazard") << "Push " << p << " from " << d_J[i] << " to " + Trace("nl-cov::lazard") << "Push " << p << " from " << d_J[i] << " to " << d_J[i - 1] << std::endl; Assert(CoCoA::owner(p) == d_J[i]); CoCoA::RingElem res(d_J[i - 1]); @@ -307,7 +307,7 @@ struct LazardEvaluationState CoCoA::RingElem res = p; for (; i > 0; --i) { - Trace("cad::lazard") << "Pushing " << p << " from J" << i << " to J" + Trace("nl-cov::lazard") << "Pushing " << p << " from J" << i << " to J" << i - 1 << std::endl; res = pushDownJ(res, i); } @@ -324,7 +324,7 @@ struct LazardEvaluationState void addR(const poly::Variable& var) { d_variables.emplace_back(var); - if (Trace.isOn("cad::lazard")) + if (Trace.isOn("nl-cov::lazard")) { std::string vname = lp_variable_db_get_name( poly::Context::get_context().get_variable_db(), var.get_internal()); @@ -334,7 +334,7 @@ struct LazardEvaluationState { d_R.emplace_back(CoCoA::NewPolyRing(d_K.back(), {CoCoA::NewSymbol()})); } - Trace("cad::lazard") << "R" << d_R.size() - 1 << " = " << d_R.back() + Trace("nl-cov::lazard") << "R" << d_R.size() - 1 << " = " << d_R.back() << std::endl; d_varCoCoA.emplace(std::make_pair(CoCoA::RingID(d_R.back()), 0), var); } @@ -349,10 +349,10 @@ struct LazardEvaluationState { d_direct.emplace_back(); d_p.emplace_back(p); - Trace("cad::lazard") << "p" << d_p.size() - 1 << " = " << d_p.back() + Trace("nl-cov::lazard") << "p" << d_p.size() - 1 << " = " << d_p.back() << std::endl; d_K.emplace_back(CoCoA::NewQuotientRing(d_R.back(), CoCoA::ideal(p))); - Trace("cad::lazard") << "K" << d_K.size() - 1 << " = " << d_K.back() + Trace("nl-cov::lazard") << "K" << d_K.size() - 1 << " = " << d_K.back() << std::endl; } @@ -366,9 +366,9 @@ struct LazardEvaluationState { d_direct.emplace_back(r); d_p.emplace_back(); - Trace("cad::lazard") << "x" << d_p.size() - 1 << " = " << r << std::endl; + Trace("nl-cov::lazard") << "x" << d_p.size() - 1 << " = " << r << std::endl; d_K.emplace_back(d_K.back()); - Trace("cad::lazard") << "K" << d_K.size() - 1 << " = " << d_K.back() + Trace("nl-cov::lazard") << "K" << d_K.size() - 1 << " = " << d_K.back() << std::endl; } @@ -384,7 +384,7 @@ struct LazardEvaluationState */ void addFreeVariable(const poly::Variable& var) { - Trace("cad::lazard") << "Add free variable " << var << std::endl; + Trace("nl-cov::lazard") << "Add free variable " << var << std::endl; addR(var); std::vector symbols; for (size_t i = 0; i < d_R.size(); ++i) @@ -394,23 +394,23 @@ struct LazardEvaluationState for (size_t i = 0; i < d_R.size(); ++i) { d_J.emplace_back(CoCoA::NewPolyRing(d_K[i], symbols, CoCoA::lex)); - Trace("cad::lazard") << "J" << d_J.size() - 1 << " = " << d_J.back() + Trace("nl-cov::lazard") << "J" << d_J.size() - 1 << " = " << d_J.back() << std::endl; symbols.erase(symbols.begin()); // R_i --> J_i d_phom.emplace_back( CoCoA::PolyAlgebraHom(d_R[i], d_J[i], {CoCoA::indet(d_J[i], 0)})); - Trace("cad::lazard") << "R" << i << " --> J" << i << ": " << d_phom.back() + Trace("nl-cov::lazard") << "R" << i << " --> J" << i << ": " << d_phom.back() << std::endl; if (i > 0) { - Trace("cad::lazard") + Trace("nl-cov::lazard") << "Constructing J" << i - 1 << " --> J" << i << ": " << std::endl; - Trace("cad::lazard") << "Constructing " << d_J[i - 1] << " --> " + Trace("nl-cov::lazard") << "Constructing " << d_J[i - 1] << " --> " << d_J[i] << ": " << std::endl; if (d_direct[i - 1]) { - Trace("cad::lazard") << "Using " << d_variables[i - 1] << " for " + Trace("nl-cov::lazard") << "Using " << d_variables[i - 1] << " for " << CoCoA::indet(d_J[i - 1], 0) << std::endl; Assert(CoCoA::CoeffRing(d_J[i]) == CoCoA::owner(*d_direct[i - 1])); std::vector indets = { @@ -449,7 +449,7 @@ struct LazardEvaluationState d_qhom.emplace_back( CoCoA::PolyRingHom(d_J[i - 1], d_J[i], R2K(K2R), indets)); } - Trace("cad::lazard") << "J" << i - 1 << " --> J" << i << ": " + Trace("nl-cov::lazard") << "J" << i - 1 << " --> J" << i << ": " << d_qhom.back() << std::endl; } } @@ -467,12 +467,12 @@ struct LazardEvaluationState for (size_t i = 0; i < d_p.size(); ++i) { if (d_direct[i]) continue; - Trace("cad::lazard") << "Apply " << d_phom[i] << " to " << d_p[i] + Trace("nl-cov::lazard") << "Apply " << d_phom[i] << " to " << d_p[i] << " from " << CoCoA::owner(d_p[i]) << std::endl; d_GBBaseIdeal.emplace_back(pushDownJ0(d_phom[i](d_p[i]), i)); } - Trace("cad::lazard") << "Finished construction" << std::endl + Trace("nl-cov::lazard") << "Finished construction" << std::endl << *this << std::endl; } @@ -521,7 +521,7 @@ struct LazardEvaluationState poly::Polynomial convertImpl(const CoCoA::RingElem& p, poly::Integer& denominator) const { - Trace("cad::lazard") << "Converting " << p << std::endl; + Trace("nl-cov::lazard") << "Converting " << p << std::endl; denominator = poly::Integer(1); poly::Polynomial res; for (CoCoA::SparsePolyIter i = CoCoA::BeginIter(p); !CoCoA::IsEnded(i); ++i) @@ -563,7 +563,7 @@ struct LazardEvaluationState res += coeff; } } - Trace("cad::lazard") << "-> " << res << std::endl; + Trace("nl-cov::lazard") << "-> " << res << std::endl; return res; } /** @@ -597,20 +597,20 @@ struct LazardEvaluationState { d_stats.d_evaluations++; std::vector res; - Trace("cad::lazard") << "Reducing " << qpoly << std::endl; + Trace("nl-cov::lazard") << "Reducing " << qpoly << std::endl; auto input = convertQ(qpoly); Assert(CoCoA::owner(input) == d_J[0]); auto factorization = CoCoA::factor(input); for (const auto& f : factorization.myFactors()) { - Trace("cad::lazard") << "-> factor " << f << std::endl; + Trace("nl-cov::lazard") << "-> factor " << f << std::endl; CoCoA::RingElem q = f; for (size_t i = 0; i < d_J.size() - 1; ++i) { - Trace("cad::lazard") << "i = " << i << std::endl; + Trace("nl-cov::lazard") << "i = " << i << std::endl; if (d_direct[i]) { - Trace("cad::lazard") + Trace("nl-cov::lazard") << "Substitute " << d_variables[i] << " = " << *d_direct[i] << " into " << q << " from " << CoCoA::owner(q) << std::endl; auto indets = CoCoA::indets(d_J[i]); @@ -625,7 +625,7 @@ struct LazardEvaluationState } // substitute x_i -> a_i q = hom(q); - Trace("cad::lazard") + Trace("nl-cov::lazard") << "-> " << q << " from " << CoCoA::owner(q) << std::endl; } else @@ -639,18 +639,18 @@ struct LazardEvaluationState } q = d_qhom[i](q); } - Trace("cad::lazard") << "-> reduced to " << q << std::endl; + Trace("nl-cov::lazard") << "-> reduced to " << q << std::endl; Assert(CoCoA::owner(q) == d_J.back()); std::vector ideal = d_GBBaseIdeal; ideal.emplace_back(pushDownJ0(q, d_J.size() - 1)); - Trace("cad::lazard") << "-> ideal " << ideal << std::endl; + Trace("nl-cov::lazard") << "-> ideal " << ideal << std::endl; auto basis = CoCoA::ReducedGBasis(CoCoA::ideal(ideal)); - Trace("cad::lazard") << "-> basis " << basis << std::endl; + Trace("nl-cov::lazard") << "-> basis " << basis << std::endl; for (const auto& belem : basis) { - Trace("cad::lazard") << "-> retrieved " << belem << std::endl; + Trace("nl-cov::lazard") << "-> retrieved " << belem << std::endl; auto pres = convert(belem); - Trace("cad::lazard") << "-> converted " << pres << std::endl; + Trace("nl-cov::lazard") << "-> converted " << pres << std::endl; // These checks are orthogonal! if (poly::is_univariate(pres) && poly::is_univariate_over_assignment(pres, d_assignment)) @@ -702,7 +702,7 @@ LazardEvaluation::~LazardEvaluation() {} */ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val) { - Trace("cad::lazard") << "Adding " << var << " -> " << val << std::endl; + Trace("nl-cov::lazard") << "Adding " << var << " -> " << val << std::endl; try { d_state->d_assignment.set(var, val); @@ -720,7 +720,7 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val) } else { - Trace("cad::lazard") << "\tis proper ran" << std::endl; + Trace("nl-cov::lazard") << "\tis proper ran" << std::endl; polymipo = poly::get_defining_polynomial(ran); } } @@ -749,12 +749,12 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val) d_state->d_stats.d_directAssignments++; return; } - Trace("cad::lazard") << "Got mipo " << polymipo << std::endl; + Trace("nl-cov::lazard") << "Got mipo " << polymipo << std::endl; auto mipo = d_state->convertMiPo(polymipo, var); - Trace("cad::lazard") << "Factoring " << mipo << " from " + Trace("nl-cov::lazard") << "Factoring " << mipo << " from " << CoCoA::owner(mipo) << std::endl; auto factorization = CoCoA::factor(mipo); - Trace("cad::lazard") << "-> " << factorization << std::endl; + Trace("nl-cov::lazard") << "-> " << factorization << std::endl; bool used_factor = false; for (const auto& f : factorization.myFactors()) { @@ -764,14 +764,14 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val) if (CoCoA::deg(f) == 1) { auto rat = -CoCoA::ConstantCoeff(f) / CoCoA::LC(f); - Trace("cad::lazard") << "Using linear factor " << f << " -> " << var + Trace("nl-cov::lazard") << "Using linear factor " << f << " -> " << var << " = " << rat << std::endl; d_state->addKRational(var, rat); d_state->d_stats.d_directAssignments++; } else { - Trace("cad::lazard") << "Using nonlinear factor " << f << std::endl; + Trace("nl-cov::lazard") << "Using nonlinear factor " << f << std::endl; d_state->addK(var, f); d_state->d_stats.d_ranAssignments++; } @@ -780,7 +780,7 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val) } else { - Trace("cad::lazard") << "Skipping " << f << std::endl; + Trace("nl-cov::lazard") << "Skipping " << f << std::endl; } } Assert(used_factor); @@ -829,7 +829,7 @@ std::vector LazardEvaluation::isolateRealRoots( for (const auto& p : reducePolynomial(q)) { // collect all real roots except for -infty, none, +infty - Trace("cad::lazard") << "Isolating roots of " << p << std::endl; + Trace("nl-cov::lazard") << "Isolating roots of " << p << std::endl; Assert(poly::is_univariate(p) && poly::is_univariate_over_assignment(p, a)); std::vector proots = poly::isolate_real_roots(p, a); for (const auto& r : proots) @@ -890,10 +890,10 @@ std::vector LazardEvaluation::infeasibleRegions( // clean up assignment d_state->d_assignment.unset(d_state->d_variables.back()); - Trace("cad::lazard") << "Shrinking:" << std::endl; + Trace("nl-cov::lazard") << "Shrinking:" << std::endl; for (const auto& i : res) { - Trace("cad::lazard") << "-> " << i << std::endl; + Trace("nl-cov::lazard") << "-> " << i << std::endl; } std::vector combined; if (res.empty()) @@ -919,7 +919,7 @@ std::vector LazardEvaluation::infeasibleRegions( continue; } // combine them into res[i+1], do not copy res[i] over to combined - Trace("cad::lazard") << "Combine " << res[i] << " and " << res[i + 1] + Trace("nl-cov::lazard") << "Combine " << res[i] << " and " << res[i + 1] << std::endl; Assert(poly::get_lower(res[i]) <= poly::get_lower(res[i + 1])); res[i + 1].set_lower(poly::get_lower(res[i]), poly::get_lower_open(res[i])); @@ -927,19 +927,19 @@ std::vector LazardEvaluation::infeasibleRegions( // always use the last one, it is never dropped combined.emplace_back(res.back()); - Trace("cad::lazard") << "To:" << std::endl; + Trace("nl-cov::lazard") << "To:" << std::endl; for (const auto& i : combined) { - Trace("cad::lazard") << "-> " << i << std::endl; + Trace("nl-cov::lazard") << "-> " << i << std::endl; } return combined; } -} // namespace cvc5::theory::arith::nl::cad +} // namespace cvc5::theory::arith::nl::coverings #else -namespace cvc5::theory::arith::nl::cad { +namespace cvc5::theory::arith::nl::coverings { /** * Do a very simple wrapper around the regular poly::infeasible_regions. @@ -974,7 +974,7 @@ std::vector LazardEvaluation::isolateRealRoots( const poly::Polynomial& q) const { WarningOnce() - << "CAD::LazardEvaluation is disabled because CoCoA is not available. " + << "nl-cov::LazardEvaluation is disabled because CoCoA is not available. " "Falling back to regular real root isolation." << std::endl; return poly::isolate_real_roots(q, d_state->d_assignment); @@ -983,13 +983,13 @@ std::vector LazardEvaluation::infeasibleRegions( const poly::Polynomial& q, poly::SignCondition sc) const { WarningOnce() - << "CAD::LazardEvaluation is disabled because CoCoA is not available. " + << "nl-cov::LazardEvaluation is disabled because CoCoA is not available. " "Falling back to regular calculation of infeasible regions." << std::endl; return poly::infeasible_regions(q, d_state->d_assignment, sc); } -} // namespace cvc5::theory::arith::nl::cad +} // namespace cvc5::theory::arith::nl::coverings #endif #endif diff --git a/src/theory/arith/nl/cad/lazard_evaluation.h b/src/theory/arith/nl/coverings/lazard_evaluation.h similarity index 94% rename from src/theory/arith/nl/cad/lazard_evaluation.h rename to src/theory/arith/nl/coverings/lazard_evaluation.h index 2afccb462..a03630d89 100644 --- a/src/theory/arith/nl/cad/lazard_evaluation.h +++ b/src/theory/arith/nl/coverings/lazard_evaluation.h @@ -16,8 +16,8 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H -#define CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H +#ifndef CVC5__THEORY__ARITH__NL__COVERINGS__LAZARD_EVALUATION_H +#define CVC5__THEORY__ARITH__NL__COVERINGS__LAZARD_EVALUATION_H #ifdef CVC5_POLY_IMP @@ -25,7 +25,7 @@ #include -namespace cvc5::theory::arith::nl::cad { +namespace cvc5::theory::arith::nl::coverings { struct LazardEvaluationState; /** @@ -111,7 +111,7 @@ class LazardEvaluation std::unique_ptr d_state; }; -} // namespace cvc5::theory::arith::nl::cad +} // namespace cvc5::theory::arith::nl::coverings #endif #endif diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/coverings/projections.cpp similarity index 93% rename from src/theory/arith/nl/cad/projections.cpp rename to src/theory/arith/nl/coverings/projections.cpp index 896d8da89..4340f99b4 100644 --- a/src/theory/arith/nl/cad/projections.cpp +++ b/src/theory/arith/nl/coverings/projections.cpp @@ -10,10 +10,10 @@ * directory for licensing information. * **************************************************************************** * - * Implements utilities for CAD projection operators. + * Implements utilities for coverings projection operators. */ -#include "theory/arith/nl/cad/projections.h" +#include "theory/arith/nl/coverings/projections.h" #ifdef CVC5_POLY_IMP @@ -23,7 +23,7 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { using namespace poly; @@ -101,7 +101,7 @@ PolyVector projectionMcCallum(const std::vector& polys) return res; } -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/coverings/projections.h similarity index 90% rename from src/theory/arith/nl/cad/projections.h rename to src/theory/arith/nl/coverings/projections.h index 129c3515a..7df36a607 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/coverings/projections.h @@ -10,13 +10,13 @@ * directory for licensing information. * **************************************************************************** * - * Implements utilities for CAD projection operators. + * Implements utilities for coverings projection operators. */ #include "cvc5_private.h" -#ifndef CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H -#define CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H +#ifndef CVC5__THEORY__ARITH__NL__COVERINGS_PROJECTIONS_H +#define CVC5__THEORY__ARITH__NL__COVERINGS_PROJECTIONS_H #ifdef CVC5_USE_POLY @@ -28,7 +28,7 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { /** * A simple wrapper around std::vector that ensures that all @@ -71,7 +71,7 @@ class PolyVector : public std::vector */ PolyVector projectionMcCallum(const std::vector& polys); -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/coverings/proof_checker.cpp similarity index 67% rename from src/theory/arith/nl/cad/proof_checker.cpp rename to src/theory/arith/nl/coverings/proof_checker.cpp index 562b57722..d4f8c6f50 100644 --- a/src/theory/arith/nl/cad/proof_checker.cpp +++ b/src/theory/arith/nl/coverings/proof_checker.cpp @@ -13,7 +13,7 @@ * Implementation of CAD proof checker. */ -#include "theory/arith/nl/cad/proof_checker.h" +#include "theory/arith/nl/coverings/proof_checker.h" #include "expr/sequence.h" #include "theory/rewriter.h" @@ -24,30 +24,30 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { -void CADProofRuleChecker::registerTo(ProofChecker* pc) +void CoveringsProofRuleChecker::registerTo(ProofChecker* pc) { // trusted rules - pc->registerTrustedChecker(PfRule::ARITH_NL_CAD_DIRECT, this, 2); - pc->registerTrustedChecker(PfRule::ARITH_NL_CAD_RECURSIVE, this, 2); + pc->registerTrustedChecker(PfRule::ARITH_NL_COVERING_DIRECT, this, 2); + pc->registerTrustedChecker(PfRule::ARITH_NL_COVERING_RECURSIVE, this, 2); } -Node CADProofRuleChecker::checkInternal(PfRule id, +Node CoveringsProofRuleChecker::checkInternal(PfRule id, const std::vector& children, const std::vector& args) { - Trace("nl-cad-checker") << "Checking " << id << std::endl; + Trace("nl-cov-checker") << "Checking " << id << std::endl; for (const auto& c : children) { - Trace("nl-cad-checker") << "\t" << c << std::endl; + Trace("nl-cov-checker") << "\t" << c << std::endl; } - if (id == PfRule::ARITH_NL_CAD_DIRECT) + if (id == PfRule::ARITH_NL_COVERING_DIRECT) { Assert(args.size() == 1); return args[0]; } - if (id == PfRule::ARITH_NL_CAD_RECURSIVE) + if (id == PfRule::ARITH_NL_COVERING_RECURSIVE) { Assert(args.size() == 1); return args[0]; @@ -55,7 +55,7 @@ Node CADProofRuleChecker::checkInternal(PfRule id, return Node::null(); } -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/coverings/proof_checker.h similarity index 69% rename from src/theory/arith/nl/cad/proof_checker.h rename to src/theory/arith/nl/coverings/proof_checker.h index 8cc544fc4..cc33787f7 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/coverings/proof_checker.h @@ -10,13 +10,13 @@ * directory for licensing information. * **************************************************************************** * - * CAD proof checker utility. + * Coverings proof checker utility. */ #include "cvc5_private.h" -#ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H -#define CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H +#ifndef CVC5__THEORY__ARITH__NL__COVERINGS__PROOF_CHECKER_H +#define CVC5__THEORY__ARITH__NL__COVERINGS__PROOF_CHECKER_H #include "expr/node.h" #include "proof/proof_checker.h" @@ -25,20 +25,20 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { /** - * A checker for CAD proofs + * A checker for coverings proofs * - * This proof checker takes care of the two CAD proof rules ARITH_NL_CAD_DIRECT - * and ARITH_NL_CAD_RECURSIVE. It does not do any actual proof checking yet, but + * This proof checker takes care of the two coverings proof rules ARITH_NL_COVERING_DIRECT + * and ARITH_NL_COVERING_RECURSIVE. It does not do any actual proof checking yet, but * considers them to be trusted rules. */ -class CADProofRuleChecker : public ProofRuleChecker +class CoveringsProofRuleChecker : public ProofRuleChecker { public: - CADProofRuleChecker() {} - ~CADProofRuleChecker() {} + CoveringsProofRuleChecker() {} + ~CoveringsProofRuleChecker() {} /** Register all rules owned by this rule checker in pc. */ void registerTo(ProofChecker* pc) override; @@ -50,7 +50,7 @@ class CADProofRuleChecker : public ProofRuleChecker const std::vector& args) override; }; -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/coverings/proof_generator.cpp similarity index 87% rename from src/theory/arith/nl/cad/proof_generator.cpp rename to src/theory/arith/nl/coverings/proof_generator.cpp index 1e3c52202..b91af55a8 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/coverings/proof_generator.cpp @@ -10,10 +10,10 @@ * directory for licensing information. * **************************************************************************** * - * Implementation of CAD proof generator. + * Implementation of coverings proof generator. */ -#include "theory/arith/nl/cad/proof_generator.h" +#include "theory/arith/nl/coverings/proof_generator.h" #ifdef CVC5_POLY_IMP @@ -27,7 +27,7 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { namespace { /** @@ -91,7 +91,7 @@ Node mkIRP(const Node& var, } // namespace -CADProofGenerator::CADProofGenerator(context::Context* ctx, +CoveringsProofGenerator::CoveringsProofGenerator(context::Context* ctx, ProofNodeManager* pnm) : d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr) { @@ -99,34 +99,34 @@ CADProofGenerator::CADProofGenerator(context::Context* ctx, d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); } -void CADProofGenerator::startNewProof() +void CoveringsProofGenerator::startNewProof() { d_current = d_proofs.allocateProof(); } -void CADProofGenerator::startRecursive() { d_current->openChild(); } -void CADProofGenerator::endRecursive(size_t intervalId) +void CoveringsProofGenerator::startRecursive() { d_current->openChild(); } +void CoveringsProofGenerator::endRecursive(size_t intervalId) { d_current->setCurrent( - intervalId, PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false); + intervalId, PfRule::ARITH_NL_COVERING_RECURSIVE, {}, {d_false}, d_false); d_current->closeChild(); } -void CADProofGenerator::startScope() +void CoveringsProofGenerator::startScope() { d_current->openChild(); d_current->getCurrent().d_rule = PfRule::SCOPE; } -void CADProofGenerator::endScope(const std::vector& args) +void CoveringsProofGenerator::endScope(const std::vector& args) { d_current->setCurrent(0, PfRule::SCOPE, {}, args, d_false); d_current->closeChild(); } -ProofGenerator* CADProofGenerator::getProofGenerator() const +ProofGenerator* CoveringsProofGenerator::getProofGenerator() const { return d_current; } -void CADProofGenerator::addDirect(Node var, +void CoveringsProofGenerator::addDirect(Node var, VariableMapper& vm, const poly::Polynomial& poly, const poly::Assignment& a, @@ -141,7 +141,7 @@ void CADProofGenerator::addDirect(Node var, // "Full conflict", constraint excludes (-inf,inf) d_current->openChild(); d_current->setCurrent(intervalId, - PfRule::ARITH_NL_CAD_DIRECT, + PfRule::ARITH_NL_COVERING_DIRECT, {constraint}, {d_false}, d_false); @@ -181,7 +181,7 @@ void CADProofGenerator::addDirect(Node var, startScope(); d_current->openChild(); d_current->setCurrent(intervalId, - PfRule::ARITH_NL_CAD_DIRECT, + PfRule::ARITH_NL_COVERING_DIRECT, {constraint}, {d_false}, d_false); @@ -189,7 +189,7 @@ void CADProofGenerator::addDirect(Node var, endScope(res); } -std::vector CADProofGenerator::constructCell(Node var, +std::vector CoveringsProofGenerator::constructCell(Node var, const CACInterval& i, const poly::Assignment& a, const poly::Value& s, @@ -233,12 +233,12 @@ std::vector CADProofGenerator::constructCell(Node var, return res; } -std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof) +std::ostream& operator<<(std::ostream& os, const CoveringsProofGenerator& proof) { return os << *proof.d_current; } -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/coverings/proof_generator.h similarity index 88% rename from src/theory/arith/nl/cad/proof_generator.h rename to src/theory/arith/nl/coverings/proof_generator.h index 521d5aa45..46d3843ed 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/coverings/proof_generator.h @@ -10,13 +10,13 @@ * directory for licensing information. * **************************************************************************** * - * Implements the proof generator for CAD. + * Implements the proof generator for coverings. */ #include "cvc5_private.h" -#ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H -#define CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H +#ifndef CVC5__THEORY__ARITH__NL__COVERINGS__PROOF_GENERATOR_H +#define CVC5__THEORY__ARITH__NL__COVERINGS__PROOF_GENERATOR_H #ifdef CVC5_POLY_IMP @@ -27,7 +27,7 @@ #include "expr/node.h" #include "proof/lazy_tree_proof_generator.h" #include "proof/proof_set.h" -#include "theory/arith/nl/cad/cdcac_utils.h" +#include "theory/arith/nl/coverings/cdcac_utils.h" namespace cvc5 { @@ -39,10 +39,10 @@ namespace nl { struct VariableMapper; -namespace cad { +namespace coverings { /** - * This class manages the proof creation during a run of the CAD solver. + * This class manages the proof creation during a run of the coverings solver. * * Though it implements the ProofGenerator interface getProofFor(Node), it only * gives a proof for a single node. @@ -50,12 +50,12 @@ namespace cad { * It uses a LazyTreeProofGenerator internally to manage the tree-based proof * construction. */ -class CADProofGenerator +class CoveringsProofGenerator { public: friend std::ostream& operator<<(std::ostream& os, - const CADProofGenerator& proof); - CADProofGenerator(context::Context* ctx, ProofNodeManager* pnm); + const CoveringsProofGenerator& proof); + CoveringsProofGenerator(context::Context* ctx, ProofNodeManager* pnm); /** Start a new proof in this proof generator */ void startNewProof(); @@ -147,9 +147,9 @@ class CADProofGenerator * Prints the underlying LazyTreeProofGenerator. Please check the documentation * of std::ostream& operator<<(std::ostream&, const LazyTreeProofGenerator&) */ -std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof); +std::ostream& operator<<(std::ostream& os, const CoveringsProofGenerator& proof); -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/coverings/variable_ordering.cpp similarity index 95% rename from src/theory/arith/nl/cad/variable_ordering.cpp rename to src/theory/arith/nl/coverings/variable_ordering.cpp index daf3f48a8..58a42d13d 100644 --- a/src/theory/arith/nl/cad/variable_ordering.cpp +++ b/src/theory/arith/nl/coverings/variable_ordering.cpp @@ -10,10 +10,10 @@ * directory for licensing information. * **************************************************************************** * - * Implements variable orderings tailored to CAD. + * Implements variable orderings tailored to coverings. */ -#include "theory/arith/nl/cad/variable_ordering.h" +#include "theory/arith/nl/coverings/variable_ordering.h" #ifdef CVC5_POLY_IMP @@ -23,7 +23,7 @@ namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { std::vector collectInformation( const Constraints::ConstraintVector& polys, bool with_totals) @@ -127,7 +127,7 @@ std::vector VariableOrdering::operator()( return {}; } -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/coverings/variable_ordering.h similarity index 81% rename from src/theory/arith/nl/cad/variable_ordering.h rename to src/theory/arith/nl/coverings/variable_ordering.h index 2de262089..e3f287f06 100644 --- a/src/theory/arith/nl/cad/variable_ordering.h +++ b/src/theory/arith/nl/coverings/variable_ordering.h @@ -10,28 +10,28 @@ * directory for licensing information. * **************************************************************************** * - * Implements variable orderings tailored to CAD. + * Implements variable orderings tailored to coverings. */ #include "cvc5_private.h" -#ifndef CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H -#define CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H +#ifndef CVC5__THEORY__ARITH__NL__COVERINGS__VARIABLE_ORDERING_H +#define CVC5__THEORY__ARITH__NL__COVERINGS__VARIABLE_ORDERING_H #ifdef CVC5_POLY_IMP #include -#include "theory/arith/nl/cad/constraints.h" +#include "theory/arith/nl/coverings/constraints.h" #include "util/poly_util.h" namespace cvc5 { namespace theory { namespace arith { namespace nl { -namespace cad { +namespace coverings { -/** Variable orderings for real variables in the context of CAD. */ +/** Variable orderings for real variables in the context of coverings. */ enum class VariableOrderingStrategy { /** Dummy ordering by variable ID. */ @@ -60,7 +60,7 @@ class VariableOrdering std::vector collectInformation( const Constraints::ConstraintVector& polys, bool with_totals = false); -} // namespace cad +} // namespace coverings } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/coverings_solver.cpp similarity index 68% rename from src/theory/arith/nl/cad_solver.cpp rename to src/theory/arith/nl/coverings_solver.cpp index 57ea8c8ba..2ec366d2a 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/coverings_solver.cpp @@ -13,13 +13,13 @@ * Implementation of new non-linear solver. */ -#include "theory/arith/nl/cad_solver.h" +#include "theory/arith/nl/coverings_solver.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" #include "smt/env.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/cad/cdcac.h" +#include "theory/arith/nl/coverings/cdcac.h" #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/poly_conversion.h" #include "theory/inference_id.h" @@ -30,7 +30,7 @@ namespace theory { namespace arith { namespace nl { -CadSolver::CadSolver(Env& env, InferenceManager& im, NlModel& model) +CoveringsSolver::CoveringsSolver(Env& env, InferenceManager& im, NlModel& model) : EnvObj(env), #ifdef CVC5_POLY_IMP @@ -54,38 +54,38 @@ CadSolver::CadSolver(Env& env, InferenceManager& im, NlModel& model) #endif } -CadSolver::~CadSolver() {} +CoveringsSolver::~CoveringsSolver() {} -void CadSolver::initLastCall(const std::vector& assertions) +void CoveringsSolver::initLastCall(const std::vector& assertions) { #ifdef CVC5_POLY_IMP - if (Trace.isOn("nl-cad")) + if (Trace.isOn("nl-cov")) { - Trace("nl-cad") << "CadSolver::initLastCall" << std::endl; - Trace("nl-cad") << "* Assertions: " << std::endl; + Trace("nl-cov") << "CoveringsSolver::initLastCall" << std::endl; + Trace("nl-cov") << "* Assertions: " << std::endl; for (const Node& a : assertions) { - Trace("nl-cad") << " " << a << std::endl; + Trace("nl-cov") << " " << a << std::endl; } } - if (options().arith.nlCadVarElim) + if (options().arith.nlCovVarElim) { d_eqsubs.reset(); std::vector processed = d_eqsubs.eliminateEqualities(assertions); if (d_eqsubs.hasConflict()) { Node lem = NodeManager::currentNM()->mkAnd(d_eqsubs.getConflict()).negate(); - d_im.addPendingLemma(lem, InferenceId::ARITH_NL_CAD_CONFLICT, nullptr); - Trace("nl-cad") << "Found conflict: " << lem << std::endl; + d_im.addPendingLemma(lem, InferenceId::ARITH_NL_COVERING_CONFLICT, nullptr); + Trace("nl-cov") << "Found conflict: " << lem << std::endl; return; } - if (Trace.isOn("nl-cad")) + if (Trace.isOn("nl-cov")) { - Trace("nl-cad") << "After simplifications" << std::endl; - Trace("nl-cad") << "* Assertions: " << std::endl; + Trace("nl-cov") << "After simplifications" << std::endl; + Trace("nl-cov") << "* Assertions: " << std::endl; for (const Node& a : processed) { - Trace("nl-cad") << " " << a << std::endl; + Trace("nl-cov") << " " << a << std::endl; } } d_CAC.reset(); @@ -107,18 +107,18 @@ void CadSolver::initLastCall(const std::vector& assertions) d_CAC.computeVariableOrdering(); d_CAC.retrieveInitialAssignment(d_model, d_ranVariable); #else - warning() << "Tried to use CadSolver but libpoly is not available. Compile " + warning() << "Tried to use CoveringsSolver but libpoly is not available. Compile " "with --poly." << std::endl; #endif } -void CadSolver::checkFull() +void CoveringsSolver::checkFull() { #ifdef CVC5_POLY_IMP if (d_CAC.getConstraints().getConstraints().empty()) { d_foundSatisfiability = true; - Trace("nl-cad") << "No constraints. Return." << std::endl; + Trace("nl-cov") << "No constraints. Return." << std::endl; return; } d_CAC.startNewProof(); @@ -126,40 +126,40 @@ void CadSolver::checkFull() if (covering.empty()) { d_foundSatisfiability = true; - Trace("nl-cad") << "SAT: " << d_CAC.getModel() << std::endl; + Trace("nl-cov") << "SAT: " << d_CAC.getModel() << std::endl; } else { d_foundSatisfiability = false; auto mis = collectConstraints(covering); - Trace("nl-cad") << "Collected MIS: " << mis << std::endl; + Trace("nl-cov") << "Collected MIS: " << mis << std::endl; Assert(!mis.empty()) << "Infeasible subset can not be empty"; - Trace("nl-cad") << "UNSAT with MIS: " << mis << std::endl; + Trace("nl-cov") << "UNSAT with MIS: " << mis << std::endl; d_eqsubs.postprocessConflict(mis); - Trace("nl-cad") << "After postprocessing: " << mis << std::endl; + Trace("nl-cov") << "After postprocessing: " << mis << std::endl; Node lem = NodeManager::currentNM()->mkAnd(mis).notNode(); ProofGenerator* proof = d_CAC.closeProof(mis); - d_im.addPendingLemma(lem, InferenceId::ARITH_NL_CAD_CONFLICT, proof); + d_im.addPendingLemma(lem, InferenceId::ARITH_NL_COVERING_CONFLICT, proof); } #else - warning() << "Tried to use CadSolver but libpoly is not available. Compile " + warning() << "Tried to use CoveringsSolver but libpoly is not available. Compile " "with --poly." << std::endl; #endif } -void CadSolver::checkPartial() +void CoveringsSolver::checkPartial() { #ifdef CVC5_POLY_IMP if (d_CAC.getConstraints().getConstraints().empty()) { - Trace("nl-cad") << "No constraints. Return." << std::endl; + Trace("nl-cov") << "No constraints. Return." << std::endl; return; } auto covering = d_CAC.getUnsatCover(true); if (covering.empty()) { d_foundSatisfiability = true; - Trace("nl-cad") << "SAT: " << d_CAC.getModel() << std::endl; + Trace("nl-cov") << "SAT: " << d_CAC.getModel() << std::endl; } else { @@ -183,22 +183,22 @@ void CadSolver::checkPartial() if (!conclusion.isNull()) { Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion); - Trace("nl-cad") << "Excluding " << first_var << " -> " + Trace("nl-cov") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl; d_im.addPendingLemma(lemma, - InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL); + InferenceId::ARITH_NL_COVERING_EXCLUDED_INTERVAL); } } } #else - warning() << "Tried to use CadSolver but libpoly is not available. Compile " + warning() << "Tried to use CoveringsSolver but libpoly is not available. Compile " "with --poly." << std::endl; #endif } -bool CadSolver::constructModelIfAvailable(std::vector& assertions) +bool CoveringsSolver::constructModelIfAvailable(std::vector& assertions) { #ifdef CVC5_POLY_IMP if (!d_foundSatisfiability) @@ -211,7 +211,7 @@ bool CadSolver::constructModelIfAvailable(std::vector& assertions) Node variable = d_CAC.getConstraints().varMapper()(v); if (!Theory::isLeafOf(variable, TheoryId::THEORY_ARITH)) { - Trace("nl-cad") << "Not a variable: " << variable << std::endl; + Trace("nl-cov") << "Not a variable: " << variable << std::endl; foundNonVariable = true; } Node value = value_to_node(d_CAC.getModel().get(v), variable); @@ -219,32 +219,32 @@ bool CadSolver::constructModelIfAvailable(std::vector& assertions) } for (const auto& sub : d_eqsubs.getSubstitutions()) { - Trace("nl-cad") << "EqSubs: " << sub.first << " -> " << sub.second + Trace("nl-cov") << "EqSubs: " << sub.first << " -> " << sub.second << std::endl; addToModel(sub.first, sub.second); } if (foundNonVariable) { - Trace("nl-cad") + Trace("nl-cov") << "Some variable was an extended term, don't clear list of assertions." << std::endl; return false; } - Trace("nl-cad") << "Constructed a full assignment, clear list of assertions." + Trace("nl-cov") << "Constructed a full assignment, clear list of assertions." << std::endl; assertions.clear(); return true; #else - warning() << "Tried to use CadSolver but libpoly is not available. Compile " + warning() << "Tried to use CoveringsSolver but libpoly is not available. Compile " "with --poly." << std::endl; return false; #endif } -void CadSolver::addToModel(TNode var, TNode value) const +void CoveringsSolver::addToModel(TNode var, TNode value) const { - Trace("nl-cad") << "-> " << var << " = " << value << std::endl; + Trace("nl-cov") << "-> " << var << " = " << value << std::endl; Assert(value.getType().isRealOrInt()); d_model.addSubstitution(var, value); } diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/coverings_solver.h similarity index 85% rename from src/theory/arith/nl/cad_solver.h rename to src/theory/arith/nl/coverings_solver.h index d72c92a8a..73ba352f5 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/coverings_solver.h @@ -13,16 +13,16 @@ * CAD-based solver based on https://arxiv.org/pdf/2003.05633.pdf. */ -#ifndef CVC5__THEORY__ARITH__CAD_SOLVER_H -#define CVC5__THEORY__ARITH__CAD_SOLVER_H +#ifndef CVC5__THEORY__ARITH__COVERINGS_SOLVER_H +#define CVC5__THEORY__ARITH__COVERINGS_SOLVER_H #include #include "context/context.h" #include "expr/node.h" #include "smt/env_obj.h" -#include "theory/arith/nl/cad/cdcac.h" -#include "theory/arith/nl/cad/proof_checker.h" +#include "theory/arith/nl/coverings/cdcac.h" +#include "theory/arith/nl/coverings/proof_checker.h" #include "theory/arith/nl/equality_substitution.h" namespace cvc5 { @@ -42,11 +42,11 @@ class NlModel; * A solver for nonlinear arithmetic that implements the CAD-based method * described in https://arxiv.org/pdf/2003.05633.pdf. */ -class CadSolver: protected EnvObj +class CoveringsSolver: protected EnvObj { public: - CadSolver(Env& env, InferenceManager& im, NlModel& model); - ~CadSolver(); + CoveringsSolver(Env& env, InferenceManager& im, NlModel& model); + ~CoveringsSolver(); /** * This is called at the beginning of last call effort check, where @@ -97,9 +97,9 @@ class CadSolver: protected EnvObj /** * The object implementing the actual decision procedure. */ - cad::CDCAC d_CAC; - /** The proof checker for cad proofs */ - cad::CADProofRuleChecker d_proofChecker; + coverings::CDCAC d_CAC; + /** The proof checker for coverings proofs */ + coverings::CoveringsProofRuleChecker d_proofChecker; #endif /** * Indicates whether we found satisfiability in the last call to @@ -114,11 +114,11 @@ class CadSolver: protected EnvObj /** Utility to eliminate variables from simple equalities before going into * the actual coverings solver */ EqualitySubstitution d_eqsubs; -}; /* class CadSolver */ +}; /* class CoveringsSolver */ } // namespace nl } // namespace arith } // namespace theory } // namespace cvc5 -#endif /* CVC5__THEORY__ARITH__CAD_SOLVER_H */ +#endif /* CVC5__THEORY__ARITH__COVERINGS_SOLVER_H */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index a26dbf173..43004c21e 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -56,7 +56,7 @@ NonlinearExtension::NonlinearExtension(Env& env, d_monomialSlv(d_env, &d_extState), d_splitZeroSlv(d_env, &d_extState), d_tangentPlaneSlv(d_env, &d_extState), - d_cadSlv(d_env, d_im, d_model), + d_covSlv(d_env, d_im, d_model), d_icpSlv(d_env, d_im), d_iandSlv(env, d_im, state, d_model), d_pow2Slv(env, d_im, state, d_model) @@ -223,9 +223,9 @@ bool NonlinearExtension::checkModel(const std::vector& assertions) return false; } } - if (options().arith.nlCad) + if (options().arith.nlCov) { - d_cadSlv.constructModelIfAvailable(passertions); + d_covSlv.constructModelIfAvailable(passertions); } Trace("nl-ext-cm") << "-----" << std::endl; @@ -442,8 +442,8 @@ void NonlinearExtension::runStrategy(Theory::Effort effort, { case InferStep::BREAK: stop = d_im.hasPendingLemma(); break; case InferStep::FLUSH_WAITING_LEMMAS: d_im.flushWaitingLemmas(); break; - case InferStep::CAD_FULL: d_cadSlv.checkFull(); break; - case InferStep::CAD_INIT: d_cadSlv.initLastCall(assertions); break; + case InferStep::COVERINGS_FULL: d_covSlv.checkFull(); break; + case InferStep::COVERINGS_INIT: d_covSlv.initLastCall(assertions); break; case InferStep::NL_FACTORING: d_factoringSlv.check(assertions, false_asserts); break; diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 0c94bbc08..0080f8948 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "smt/env_obj.h" -#include "theory/arith/nl/cad_solver.h" +#include "theory/arith/nl/coverings_solver.h" #include "theory/arith/nl/ext/ext_state.h" #include "theory/arith/nl/ext/factoring_check.h" #include "theory/arith/nl/ext/monomial_bounds_check.h" @@ -242,8 +242,8 @@ class NonlinearExtension : EnvObj SplitZeroCheck d_splitZeroSlv; /** Solver for tangent plane lemmas. */ TangentPlaneCheck d_tangentPlaneSlv; - /** The CAD-based solver */ - CadSolver d_cadSlv; + /** The coverings-based solver */ + CoveringsSolver d_covSlv; /** The ICP-based solver */ icp::ICPSolver d_icpSlv; /** The integer and solver diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 43c3d152d..0327af22c 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -567,7 +567,7 @@ Node excluding_interval_to_lemma(const Node& variable, const poly::AlgebraicNumber& alg = as_algebraic_number(lv); if (poly::is_rational(alg)) { - Trace("nl-cad") << "Rational point interval: " << interval << std::endl; + Trace("nl-cov") << "Rational point interval: " << interval << std::endl; return nm->mkNode( Kind::DISTINCT, variable, @@ -575,7 +575,7 @@ Node excluding_interval_to_lemma(const Node& variable, CONST_RATIONAL, poly_utils::toRational(poly::to_rational_approximation(alg)))); } - Trace("nl-cad") << "Algebraic point interval: " << interval << std::endl; + Trace("nl-cov") << "Algebraic point interval: " << interval << std::endl; // p(x) != 0 or x <= lb or ub <= x if (allowNonlinearLemma) { @@ -597,7 +597,7 @@ Node excluding_interval_to_lemma(const Node& variable, } else { - Trace("nl-cad") << "Rational point interval: " << interval << std::endl; + Trace("nl-cov") << "Rational point interval: " << interval << std::endl; return nm->mkNode( Kind::DISTINCT, variable, @@ -606,17 +606,17 @@ Node excluding_interval_to_lemma(const Node& variable, } if (li) { - Trace("nl-cad") << "Only upper bound: " << interval << std::endl; + Trace("nl-cov") << "Only upper bound: " << interval << std::endl; return upper_bound_as_node( variable, uv, poly::get_upper_open(interval), allowNonlinearLemma); } if (ui) { - Trace("nl-cad") << "Only lower bound: " << interval << std::endl; + Trace("nl-cov") << "Only lower bound: " << interval << std::endl; return lower_bound_as_node( variable, lv, poly::get_lower_open(interval), allowNonlinearLemma); } - Trace("nl-cad") << "Proper interval: " << interval << std::endl; + Trace("nl-cov") << "Proper interval: " << interval << std::endl; Node lb = lower_bound_as_node( variable, lv, poly::get_lower_open(interval), allowNonlinearLemma); Node ub = upper_bound_as_node( diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index dddde3c0f..f9c82fa1f 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -68,7 +68,7 @@ poly::UPolynomial as_poly_upolynomial(const cvc5::Node& n, * Once the polynomial has been fully constructed, we can oftentimes ignore the * denominator (except for its sign, which is always positive, though). * This is the case if we are solely interested in the roots of the polynomials - * (like in the context of CAD). If we need the actual polynomial (for example + * (like in the context of coverings). If we need the actual polynomial (for example * in the context of ICP) the second overload provides the denominator in the * third argument. */ diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index a14841f67..8ea46099c 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -31,8 +31,8 @@ std::ostream& operator<<(std::ostream& os, InferStep step) { case InferStep::BREAK: return os << "BREAK"; case InferStep::FLUSH_WAITING_LEMMAS: return os << "FLUSH_WAITING_LEMMAS"; - case InferStep::CAD_INIT: return os << "CAD_INIT"; - case InferStep::CAD_FULL: return os << "CAD_FULL"; + case InferStep::COVERINGS_INIT: return os << "COVERINGS_INIT"; + case InferStep::COVERINGS_FULL: return os << "COVERINGS_FULL"; case InferStep::NL_FACTORING: return os << "NL_FACTORING"; case InferStep::IAND_INIT: return os << "IAND_INIT"; case InferStep::IAND_FULL: return os << "IAND_FULL"; @@ -170,10 +170,10 @@ void Strategy::initializeStrategy(const Options& options) } one << InferStep::IAND_FULL << InferStep::BREAK; one << InferStep::POW2_FULL << InferStep::BREAK; - if (options.arith.nlCad) + if (options.arith.nlCov) { - one << InferStep::CAD_INIT << InferStep::BREAK; - one << InferStep::CAD_FULL << InferStep::BREAK; + one << InferStep::COVERINGS_INIT << InferStep::BREAK; + one << InferStep::COVERINGS_FULL << InferStep::BREAK; } d_interleaving.add(one); diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index d50108851..a0d257d2a 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -34,10 +34,10 @@ enum class InferStep /** Flush waiting lemmas to be pending */ FLUSH_WAITING_LEMMAS, - /** Initialize the CAD solver */ - CAD_INIT, - /** A full CAD check */ - CAD_FULL, + /** Initialize the coverings solver */ + COVERINGS_INIT, + /** A full coverings check */ + COVERINGS_FULL, /** Initialize the IAND solver */ IAND_INIT, diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index b0d218e81..5968a2ff2 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -100,9 +100,9 @@ const char* toString(InferenceId i) return "ARITH_NL_POW2_MONOTONE_REFINE"; case InferenceId::ARITH_NL_POW2_TRIVIAL_CASE_REFINE: return "ARITH_NL_POW2_TRIVIAL_CASE_REFINE"; - case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT"; - case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: - return "ARITH_NL_CAD_EXCLUDED_INTERVAL"; + case InferenceId::ARITH_NL_COVERING_CONFLICT: return "ARITH_NL_COVERING_CONFLICT"; + case InferenceId::ARITH_NL_COVERING_EXCLUDED_INTERVAL: + return "ARITH_NL_COVERING_EXCLUDED_INTERVAL"; case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT"; case InferenceId::ARITH_NL_ICP_PROPAGATION: return "ARITH_NL_ICP_PROPAGATION"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index a34b40661..76c330cae 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -158,11 +158,11 @@ enum class InferenceId ARITH_NL_POW2_MONOTONE_REFINE, // trivial refinements (Pow2Solver::checkFullRefine) ARITH_NL_POW2_TRIVIAL_CASE_REFINE, - //-------------------- nonlinear cad solver - // conflict / infeasible subset obtained from cad - ARITH_NL_CAD_CONFLICT, + //-------------------- nonlinear coverings solver + // conflict / infeasible subset obtained from coverings + ARITH_NL_COVERING_CONFLICT, // excludes an interval for a single variable - ARITH_NL_CAD_EXCLUDED_INTERVAL, + ARITH_NL_COVERING_EXCLUDED_INTERVAL, //-------------------- nonlinear icp solver // conflict obtained from icp ARITH_NL_ICP_CONFLICT, diff --git a/test/regress/regress0/nl/issue5726-downpolys.smt2 b/test/regress/regress0/nl/issue5726-downpolys.smt2 index b9b204198..4a663ebe0 100644 --- a/test/regress/regress0/nl/issue5726-downpolys.smt2 +++ b/test/regress/regress0/nl/issue5726-downpolys.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext=none --nl-cad +; COMMAND-LINE: --nl-ext=none --nl-cov ; REQUIRES: poly ; EXPECT: unsat (set-logic QF_NRA) diff --git a/test/regress/regress0/nl/issue5726-sqfactor.smt2 b/test/regress/regress0/nl/issue5726-sqfactor.smt2 index bfe8d31a6..07f1b7f6d 100644 --- a/test/regress/regress0/nl/issue5726-sqfactor.smt2 +++ b/test/regress/regress0/nl/issue5726-sqfactor.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext=none --nl-cad +; COMMAND-LINE: --nl-ext=none --nl-cov ; REQUIRES: poly ; EXPECT: sat (set-logic QF_NRA) diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/unit/api/cpp/theory_arith_nl_black.cpp index 0b9b9f119..de33a3f3d 100644 --- a/test/unit/api/cpp/theory_arith_nl_black.cpp +++ b/test/unit/api/cpp/theory_arith_nl_black.cpp @@ -55,8 +55,8 @@ TEST_F(TestTheoryBlackArithNl, cvc5Projects388Min) return; } Solver slv; - slv.setOption("nl-cad", "true"); - slv.setOption("nl-cad-var-elim", "true"); + slv.setOption("nl-cov", "true"); + slv.setOption("nl-cov-var-elim", "true"); slv.setOption("nl-ext", "none"); slv.setLogic("QF_NIRA"); Sort s = slv.getRealSort(); diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 82e191d83..82cd3cb58 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -22,7 +22,7 @@ cvc5_add_unit_test_white(sequences_rewriter_white theory) cvc5_add_unit_test_white(strings_rewriter_white theory) cvc5_add_unit_test_white(theory_arith_pow2_white theory) cvc5_add_unit_test_white(theory_arith_white theory) -cvc5_add_unit_test_white(theory_arith_cad_white theory) +cvc5_add_unit_test_white(theory_arith_coverings_white theory) cvc5_add_unit_test_black(theory_arith_rewriter_black theory) cvc5_add_unit_test_white(theory_bags_normal_form_white theory) cvc5_add_unit_test_white(theory_bags_rewriter_white theory) diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp similarity index 89% rename from test/unit/theory/theory_arith_cad_white.cpp rename to test/unit/theory/theory_arith_coverings_white.cpp index aef2189ba..864402eed 100644 --- a/test/unit/theory/theory_arith_cad_white.cpp +++ b/test/unit/theory/theory_arith_coverings_white.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Unit tests for the CAD module for nonlinear arithmetic. + * Unit tests for the coverings module for nonlinear arithmetic. */ #ifdef CVC5_USE_POLY @@ -26,10 +26,10 @@ #include "options/proof_options.h" #include "options/smt_options.h" #include "smt/proof_manager.h" -#include "theory/arith/nl/cad/cdcac.h" -#include "theory/arith/nl/cad/lazard_evaluation.h" -#include "theory/arith/nl/cad/projections.h" -#include "theory/arith/nl/cad_solver.h" +#include "theory/arith/nl/coverings/cdcac.h" +#include "theory/arith/nl/coverings/lazard_evaluation.h" +#include "theory/arith/nl/coverings/projections.h" +#include "theory/arith/nl/coverings_solver.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/poly_conversion.h" #include "theory/arith/theory_arith.h" @@ -47,7 +47,7 @@ using namespace cvc5::theory::arith; using namespace cvc5::theory::arith::nl; NodeManager* nodeManager; -class TestTheoryWhiteArithCAD : public TestSmt +class TestTheoryWhiteArithCoverings : public TestSmt { protected: void SetUp() override @@ -55,7 +55,6 @@ class TestTheoryWhiteArithCAD : public TestSmt TestSmt::SetUp(); d_realType.reset(new TypeNode(d_nodeManager->realType())); d_intType.reset(new TypeNode(d_nodeManager->integerType())); - Trace.on("cad-check"); nodeManager = d_nodeManager; } @@ -125,7 +124,7 @@ Node make_int_variable(const std::string& s) s, nodeManager->integerType(), "", SkolemManager::SKOLEM_EXACT_NAME); } -TEST_F(TestTheoryWhiteArithCAD, test_univariate_isolation) +TEST_F(TestTheoryWhiteArithCoverings, test_univariate_isolation) { poly::UPolynomial poly({-2, 2, 3, -3, -1, 1}); auto roots = poly::isolate_real_roots(poly); @@ -137,7 +136,7 @@ TEST_F(TestTheoryWhiteArithCAD, test_univariate_isolation) EXPECT_TRUE(roots[3] == get_ran({-2, 0, 1}, 1, 2)); } -TEST_F(TestTheoryWhiteArithCAD, test_multivariate_isolation) +TEST_F(TestTheoryWhiteArithCoverings, test_multivariate_isolation) { poly::Variable x("x"); poly::Variable y("y"); @@ -155,7 +154,7 @@ TEST_F(TestTheoryWhiteArithCAD, test_multivariate_isolation) EXPECT_TRUE(roots[0] == get_ran({-8, 0, 1}, 2, 3)); } -TEST_F(TestTheoryWhiteArithCAD, test_univariate_factorization) +TEST_F(TestTheoryWhiteArithCoverings, test_univariate_factorization) { poly::UPolynomial poly({-24, 44, -18, -1, 1, -3, 1}); @@ -165,7 +164,7 @@ TEST_F(TestTheoryWhiteArithCAD, test_univariate_factorization) EXPECT_EQ(factors[1], poly::UPolynomial({-24, -4, -2, -1, 1})); } -TEST_F(TestTheoryWhiteArithCAD, test_projection) +TEST_F(TestTheoryWhiteArithCoverings, test_projection) { // Gereon's thesis, Ex 5.1 poly::Variable x("x"); @@ -174,7 +173,7 @@ TEST_F(TestTheoryWhiteArithCAD, test_projection) poly::Polynomial p = (y + 1) * (y + 1) - x * x * x + 3 * x - 2; poly::Polynomial q = (x + 1) * y - 3; - auto res = cad::projectionMcCallum({p, q}); + auto res = coverings::projectionMcCallum({p, q}); std::sort(res.begin(), res.end()); EXPECT_EQ(res[0], x - 1); EXPECT_EQ(res[1], x + 1); @@ -200,7 +199,7 @@ poly::Polynomial up_to_poly(const poly::UPolynomial& p, poly::Variable var) return res; } -TEST_F(TestTheoryWhiteArithCAD, lazard_simp) +TEST_F(TestTheoryWhiteArithCoverings, lazard_simp) { Rewriter* rewriter = d_slvEngine->getRewriter(); Node a = d_nodeManager->mkVar(*d_realType); @@ -227,7 +226,7 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_simp) } #ifdef CVC5_USE_COCOA -TEST_F(TestTheoryWhiteArithCAD, lazard_eval) +TEST_F(TestTheoryWhiteArithCoverings, lazard_eval) { poly::Variable x("x"); poly::Variable y("y"); @@ -237,7 +236,7 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_eval) poly::AlgebraicNumber ay = get_ran({-2, 0, 0, 0, 1}, 1, 2); poly::AlgebraicNumber az = get_ran({-3, 0, 1}, 1, 2); - cad::LazardEvaluation lazard; + coverings::LazardEvaluation lazard; lazard.add(x, ax); lazard.add(y, ay); lazard.add(z, az); @@ -249,11 +248,11 @@ TEST_F(TestTheoryWhiteArithCAD, lazard_eval) } #endif -TEST_F(TestTheoryWhiteArithCAD, test_cdcac_1) +TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_1) { Options opts; Env env(NodeManager::currentNM(), &opts); - cad::CDCAC cac(env, {}); + coverings::CDCAC cac(env, {}); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y")); @@ -271,11 +270,11 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_1) std::cout << "SAT: " << cac.getModel() << std::endl; } -TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2) +TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_2) { Options opts; Env env(NodeManager::currentNM(), &opts); - cad::CDCAC cac(env, {}); + coverings::CDCAC cac(env, {}); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y")); @@ -297,18 +296,18 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2) auto cover = cac.getUnsatCover(); EXPECT_TRUE(!cover.empty()); - auto nodes = cad::collectConstraints(cover); + auto nodes = coverings::collectConstraints(cover); std::vector ref{dummy(1), dummy(2), dummy(3), dummy(4), dummy(5)}; std::sort(nodes.begin(), nodes.end()); std::sort(ref.begin(), ref.end()); EXPECT_EQ(nodes, ref); } -TEST_F(TestTheoryWhiteArithCAD, test_cdcac_3) +TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_3) { Options opts; Env env(NodeManager::currentNM(), &opts); - cad::CDCAC cac(env, {}); + coverings::CDCAC cac(env, {}); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y")); poly::Variable z = cac.getConstraints().varMapper()(make_real_variable("z")); @@ -327,11 +326,11 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_3) std::cout << "SAT: " << cac.getModel() << std::endl; } -TEST_F(TestTheoryWhiteArithCAD, test_cdcac_4) +TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_4) { Options opts; Env env(NodeManager::currentNM(), &opts); - cad::CDCAC cac(env, {}); + coverings::CDCAC cac(env, {}); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y")); poly::Variable z = cac.getConstraints().varMapper()(make_real_variable("z")); @@ -356,7 +355,7 @@ void test_delta(const std::vector& a) { Options opts; Env env(NodeManager::currentNM(), &opts); - cad::CDCAC cac(env, {}); + coverings::CDCAC cac(env, {}); cac.reset(); for (const Node& n : a) { @@ -373,7 +372,7 @@ void test_delta(const std::vector& a) } else { - auto mis = cad::collectConstraints(covering); + auto mis = coverings::collectConstraints(covering); std::cout << "Collected MIS: " << mis << std::endl; Assert(!mis.empty()) << "Infeasible subset can not be empty"; Node lem = NodeManager::currentNM()->mkAnd(mis).negate(); @@ -381,7 +380,7 @@ void test_delta(const std::vector& a) } } -TEST_F(TestTheoryWhiteArithCAD, test_cdcac_proof_1) +TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1) { Options opts; // enable proofs @@ -394,10 +393,10 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_proof_1) // register checkers that we need builtin::BuiltinProofRuleChecker btchecker(env); btchecker.registerTo(env.getProofNodeManager()->getChecker()); - cad::CADProofRuleChecker checker; + coverings::CoveringsProofRuleChecker checker; checker.registerTo(env.getProofNodeManager()->getChecker()); // do the coverings problem - cad::CDCAC cac(env, {}); + coverings::CDCAC cac(env, {}); EXPECT_TRUE(cac.getProof() != nullptr); cac.startNewProof(); poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x")); @@ -424,7 +423,7 @@ TEST_F(TestTheoryWhiteArithCAD, test_cdcac_proof_1) EXPECT_TRUE(pg != nullptr); } -TEST_F(TestTheoryWhiteArithCAD, test_delta_one) +TEST_F(TestTheoryWhiteArithCoverings, test_delta_one) { std::vector a; Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); @@ -447,7 +446,7 @@ TEST_F(TestTheoryWhiteArithCAD, test_delta_one) test_delta(a); } -TEST_F(TestTheoryWhiteArithCAD, test_delta_two) +TEST_F(TestTheoryWhiteArithCoverings, test_delta_two) { std::vector a; Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)); @@ -470,7 +469,7 @@ TEST_F(TestTheoryWhiteArithCAD, test_delta_two) test_delta(a); } -TEST_F(TestTheoryWhiteArithCAD, test_ran_conversion) +TEST_F(TestTheoryWhiteArithCoverings, test_ran_conversion) { RealAlgebraicNumber ran( std::vector({-2, 0, 1}), Rational(1, 3), Rational(7, 3)); -- 2.30.2