From 9f57f4613dd273b0ef1a531cc72fc418cf4b1af0 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 30 Jul 2020 18:16:25 +0200 Subject: [PATCH] Adds the interface for the CAD-based arithmetic solver. (#4773) This PR adds some utilities and, most importantly, the interface of the new CAD-based solver. The approach is based on https://arxiv.org/pdf/2003.05633.pdf and the code structure follows the paper rather closely. --- src/CMakeLists.txt | 4 + src/theory/arith/nl/cad/cdcac.cpp | 89 ++++++ src/theory/arith/nl/cad/cdcac.h | 138 +++++++++ src/theory/arith/nl/cad/cdcac_utils.cpp | 269 ++++++++++++++++++ src/theory/arith/nl/cad/cdcac_utils.h | 100 +++++++ src/theory/arith/nl/cad/constraints.cpp | 62 ++-- src/theory/arith/nl/cad/constraints.h | 51 ++-- src/theory/arith/nl/cad/projections.cpp | 38 ++- src/theory/arith/nl/cad/projections.h | 26 +- src/theory/arith/nl/cad/variable_ordering.cpp | 41 ++- src/theory/arith/nl/cad/variable_ordering.h | 12 +- src/theory/arith/nl/poly_conversion.cpp | 6 - src/theory/arith/nl/poly_conversion.h | 6 - 13 files changed, 697 insertions(+), 145 deletions(-) create mode 100644 src/theory/arith/nl/cad/cdcac.cpp create mode 100644 src/theory/arith/nl/cad/cdcac.h create mode 100644 src/theory/arith/nl/cad/cdcac_utils.cpp create mode 100644 src/theory/arith/nl/cad/cdcac_utils.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 992da9a85..59b559cb2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -306,6 +306,10 @@ libcvc4_add_sources( theory/arith/linear_equality.h theory/arith/matrix.cpp theory/arith/matrix.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/projections.cpp diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp new file mode 100644 index 000000000..18b16bbe8 --- /dev/null +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -0,0 +1,89 @@ +/********************* */ +/*! \file cdcac.cpp + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implements the CDCAC approach. + ** + ** Implements the CDCAC approach as described in + ** https://arxiv.org/pdf/2003.05633.pdf. + **/ + +#include "theory/arith/nl/cad/cdcac.h" + +#include "theory/arith/nl/cad/projections.h" +#include "theory/arith/nl/cad/variable_ordering.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace cad { + +CDCAC::CDCAC() {} + +CDCAC::CDCAC(const std::vector& ordering) + : d_variableOrdering(ordering) +{ +} + +void CDCAC::reset() +{ + d_constraints.reset(); + d_assignment.clear(); +} + +void CDCAC::computeVariableOrdering() {} + +Constraints& CDCAC::getConstraints() { return d_constraints; } +const Constraints& CDCAC::getConstraints() const { return d_constraints; } + +const poly::Assignment& CDCAC::getModel() const { return d_assignment; } + +const std::vector& CDCAC::getVariableOrdering() const +{ + return d_variableOrdering; +} + +std::vector CDCAC::getUnsatIntervals( + std::size_t cur_variable) const +{ + return {}; +} + +std::vector CDCAC::requiredCoefficients( + const poly::Polynomial& p) const +{ + return {}; +} + +std::vector CDCAC::constructCharacterization( + std::vector& intervals) +{ + return {}; +} + +CACInterval CDCAC::intervalFromCharacterization( + const std::vector& characterization, + std::size_t cur_variable, + const poly::Value& sample) +{ + return {}; +} + +std::vector CDCAC::getUnsatCover(std::size_t cur_variable) +{ + return {}; +} + +} // namespace cad +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h new file mode 100644 index 000000000..88e260ada --- /dev/null +++ b/src/theory/arith/nl/cad/cdcac.h @@ -0,0 +1,138 @@ +/********************* */ +/*! \file cdcac.h + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implements the CDCAC approach. + ** + ** Implements the CDCAC approach as described in + ** https://arxiv.org/pdf/2003.05633.pdf. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_H +#define CVC4__THEORY__ARITH__NL__CAD__CDCAC_H + +#include + +#include + +#include "theory/arith/nl/cad/cdcac_utils.h" +#include "theory/arith/nl/cad/constraints.h" +#include "theory/arith/nl/cad/variable_ordering.h" +#include "theory/arith/nl/nl_model.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace cad { + +/** + * This class implements Cylindrical Algebraic Coverings as presented in + * https://arxiv.org/pdf/2003.05633.pdf + */ +class CDCAC +{ + public: + /** Initialize without a variable ordering. */ + CDCAC(); + /** Initialize this method with the given variable ordering. */ + CDCAC(const std::vector& ordering); + + /** Reset this instance. */ + void reset(); + + /** Collect variables from the constraints and compute a variable ordering. */ + void computeVariableOrdering(); + + /** + * Returns the constraints as a non-const reference. Can be used to add new + * constraints. + */ + Constraints& getConstraints(); + /** Returns the constraints as a const reference. */ + const Constraints& getConstraints() const; + + /** + * Returns the current assignment. This is a satisfying model if + * get_unsat_cover() returned an empty vector. + */ + const poly::Assignment& getModel() const; + + /** Returns the current variable ordering. */ + const std::vector& getVariableOrdering() const; + + /** + * Collect all unsatisfiable intervals for the given variable. + * Combines unsatisfiable regions from d_constraints evaluated over + * d_assignment. Implements Algorithm 2. + */ + std::vector getUnsatIntervals(std::size_t cur_variable) const; + + /** + * Collects the coefficients required for projection from the given + * polynomial. Implements Algorithm 6. + */ + std::vector requiredCoefficients( + const poly::Polynomial& p) const; + + /** + * Constructs a characterization of the given covering. + * A characterization contains polynomials whose roots bound the region around + * the current assignment. Implements Algorithm 4. + */ + std::vector constructCharacterization( + std::vector& intervals); + + /** + * Constructs an infeasible interval from a characterization. + * Implements Algorithm 5. + */ + CACInterval intervalFromCharacterization( + const std::vector& characterization, + std::size_t cur_variable, + const poly::Value& sample); + + /** + * Main method that checks for the satisfiability of the constraints. + * Recursively explores possible assignments and excludes regions based on the + * coverings. Returns either a covering for the lowest dimension or an empty + * vector. If the covering is empty, the result is SAT and an assignment can + * be obtained from d_assignment. If the covering is not empty, the result is + * UNSAT and an infeasible subset can be extracted from the returned covering. + * Implements Algorithm 2. + */ + std::vector getUnsatCover(std::size_t cur_variable = 0); + + private: + /** + * The current assignment. When the method terminates with SAT, it contains a + * model for the input constraints. + */ + poly::Assignment d_assignment; + + /** The set of input constraints to be checked for consistency. */ + Constraints d_constraints; + + /** The computed variable ordering used for this method. */ + std::vector d_variableOrdering; + + /** The object computing the variable ordering. */ + VariableOrdering d_varOrder; +}; + +} // namespace cad +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp new file mode 100644 index 000000000..02df1a323 --- /dev/null +++ b/src/theory/arith/nl/cad/cdcac_utils.cpp @@ -0,0 +1,269 @@ +/********************* */ +/*! \file cdcac_utils.cpp + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implements utilities for cdcac. + ** + ** Implements utilities for cdcac. + **/ + +#include "theory/arith/nl/cad/cdcac_utils.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace cad { + +using namespace poly; + +bool operator==(const CACInterval& lhs, const CACInterval& rhs) +{ + return lhs.d_interval == rhs.d_interval; +} +bool operator<(const CACInterval& lhs, const CACInterval& rhs) +{ + return lhs.d_interval < rhs.d_interval; +} + +/** + * Induces an ordering on poly intervals that is suitable for redundancy + * removal as implemented in clean_intervals. + */ +inline bool compareForCleanup(const Interval& lhs, const Interval& rhs) +{ + const lp_value_t* ll = &(lhs.get_internal()->a); + const lp_value_t* lu = + lhs.get_internal()->is_point ? ll : &(lhs.get_internal()->b); + const lp_value_t* rl = &(rhs.get_internal()->a); + const lp_value_t* ru = + rhs.get_internal()->is_point ? rl : &(rhs.get_internal()->b); + + int lc = lp_value_cmp(ll, rl); + // Lower bound is smaller + if (lc < 0) return true; + // Lower bound is larger + if (lc > 0) return false; + // Lower bound type is smaller + if (!lhs.get_internal()->a_open && rhs.get_internal()->a_open) return true; + // Lower bound type is larger + if (lhs.get_internal()->a_open && !rhs.get_internal()->a_open) return false; + + // Attention: Here it differs from the regular interval ordering! + int uc = lp_value_cmp(lu, ru); + // Upper bound is smaller + if (uc < 0) return false; + // Upper bound is larger + if (uc > 0) return true; + // Upper bound type is smaller + if (lhs.get_internal()->b_open && !rhs.get_internal()->b_open) return false; + // Upper bound type is larger + if (!lhs.get_internal()->b_open && rhs.get_internal()->b_open) return true; + + // Identical + return false; +} + +bool intervalCovers(const Interval& lhs, const Interval& rhs) +{ + const lp_value_t* ll = &(lhs.get_internal()->a); + const lp_value_t* lu = + lhs.get_internal()->is_point ? ll : &(lhs.get_internal()->b); + const lp_value_t* rl = &(rhs.get_internal()->a); + const lp_value_t* ru = + rhs.get_internal()->is_point ? rl : &(rhs.get_internal()->b); + + int lc = lp_value_cmp(ll, rl); + int uc = lp_value_cmp(lu, ru); + + // Lower bound is smaller and upper bound is larger + if (lc < 0 && uc > 0) return true; + // Lower bound is larger or upper bound is smaller + if (lc > 0 || uc < 0) return false; + + // Now both bounds are identical. + Assert(lc <= 0 && uc >= 0); + Assert(lc == 0 || uc == 0); + + // Lower bound is the same and the bound type is stricter + if (lc == 0 && lhs.get_internal()->a_open && !rhs.get_internal()->a_open) + return false; + // Upper bound is the same and the bound type is stricter + if (uc == 0 && lhs.get_internal()->b_open && !rhs.get_internal()->b_open) + return false; + + // Both bounds are weaker + return true; +} + +bool intervalConnect(const Interval& lhs, const Interval& rhs) +{ + Assert(lhs < rhs) << "Can only check for a connection if lhs < rhs."; + const lp_value_t* lu = lhs.get_internal()->is_point + ? &(lhs.get_internal()->a) + : &(lhs.get_internal()->b); + const lp_value_t* rl = &(rhs.get_internal()->a); + int c = lp_value_cmp(lu, rl); + if (c < 0) + { + Trace("libpoly::interval_connect") + << lhs << " and " << rhs << " are separated." << std::endl; + return false; + } + if (c > 0) + { + Trace("libpoly::interval_connect") + << lhs << " and " << rhs << " overlap." << std::endl; + return true; + } + Assert(c == 0); + if (lhs.get_internal()->is_point || rhs.get_internal()->is_point + || !lhs.get_internal()->b_open || !rhs.get_internal()->a_open) + { + Trace("libpoly::interval_connect") + << lhs << " and " << rhs + << " touch and the intermediate point is covered." << std::endl; + return true; + } + return false; +} + +void cleanIntervals(std::vector& intervals) +{ + // Simplifies removal of redundancies later on. + if (intervals.size() < 2) return; + + // Sort intervals. + std::sort(intervals.begin(), + intervals.end(), + [](const CACInterval& lhs, const CACInterval& rhs) { + return compareForCleanup(lhs.d_interval, rhs.d_interval); + }); + + // Remove intervals that are covered by others. + // Implementation roughly follows + // https://en.cppreference.com/w/cpp/algorithm/remove Find first interval that + // covers the next one. + std::size_t first = 0; + for (std::size_t n = intervals.size(); first < n - 1; ++first) + { + if (intervalCovers(intervals[first].d_interval, + intervals[first + 1].d_interval)) + { + break; + } + } + // If such an interval exists, remove accordingly. + if (first < intervals.size() - 1) + { + for (std::size_t i = first + 2, n = intervals.size(); i < n; ++i) + { + if (!intervalCovers(intervals[first].d_interval, intervals[i].d_interval)) + { + // Interval is not covered. Move it to the front and bump front. + ++first; + intervals[first] = std::move(intervals[i]); + } + // Else: Interval is covered as well. + } + // Erase trailing values + while (intervals.size() > first + 1) + { + intervals.pop_back(); + } + } +} + +std::vector collectConstraints(const std::vector& intervals) +{ + std::vector res; + for (const auto& i : intervals) + { + res.insert(res.end(), i.d_origins.begin(), i.d_origins.end()); + } + std::sort(res.begin(), res.end()); + auto it = std::unique(res.begin(), res.end()); + res.erase(it, res.end()); + return res; +} + +bool sampleOutside(const std::vector& infeasible, Value& sample) +{ + if (infeasible.empty()) + { + // No infeasible region, just take anything: zero + sample = poly::Integer(); + return true; + } + if (!is_minus_infinity(get_lower(infeasible.front().d_interval))) + { + // First does not cover -oo, just take sufficiently low value + Trace("cdcac") << "Sample before " << infeasible.front().d_interval + << std::endl; + const auto* i = infeasible.front().d_interval.get_internal(); + sample = value_between( + Value::minus_infty().get_internal(), true, &i->a, !i->a_open); + return true; + } + for (std::size_t i = 0, n = infeasible.size(); i < n - 1; ++i) + { + // Search for two subsequent intervals that do not connect + if (!intervalConnect(infeasible[i].d_interval, + infeasible[i + 1].d_interval)) + { + // Two intervals do not connect, take something from the gap + const auto* l = infeasible[i].d_interval.get_internal(); + const auto* r = infeasible[i + 1].d_interval.get_internal(); + + Trace("cdcac") << "Sample between " << infeasible[i].d_interval << " and " + << infeasible[i + 1].d_interval << std::endl; + + if (l->is_point) + { + sample = value_between(&l->a, true, &r->a, !r->a_open); + } + else + { + sample = value_between(&l->b, !l->b_open, &r->a, !r->a_open); + } + return true; + } + else + { + Trace("cdcac") << infeasible[i].d_interval << " and " + << infeasible[i + 1].d_interval << " connect" << std::endl; + } + } + if (!is_plus_infinity(get_upper(infeasible.back().d_interval))) + { + // Last does not cover oo, just take something sufficiently large + Trace("cdcac") << "Sample above " << infeasible.back().d_interval + << std::endl; + const auto* i = infeasible.back().d_interval.get_internal(); + if (i->is_point) + { + sample = + value_between(&i->a, true, Value::plus_infty().get_internal(), true); + } + else + { + sample = value_between( + &i->b, !i->b_open, Value::plus_infty().get_internal(), true); + } + return true; + } + return false; +} + +} // namespace cad +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 \ No newline at end of file diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h new file mode 100644 index 000000000..d5fa70bd9 --- /dev/null +++ b/src/theory/arith/nl/cad/cdcac_utils.h @@ -0,0 +1,100 @@ +/********************* */ +/*! \file cdcac_utils.h + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implements utilities for cdcac. + ** + ** Implements utilities for cdcac. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H +#define CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H + +#include + +#include + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace cad { + +/** + * An interval as specified in section 4.1 of + * https://arxiv.org/pdf/2003.05633.pdf. + * + * It consists of + * - the actual interval, either an open or a point interal, + * - the characterizing polynomials of the lower and upper bound, + * - the characterizing polynomials in the main variable, + * - the characterizing polynomials in lower variables and + * - the constraints used to derive this interval. + */ +struct CACInterval +{ + /** The actual interval. */ + poly::Interval d_interval; + /** The polynomials characterizing the lower bound. */ + std::vector d_lowerPolys; + /** The polynomials characterizing the upper bound. */ + std::vector d_upperPolys; + /** The characterizing polynomials in the main variable. */ + std::vector d_mainPolys; + /** The characterizing polynomials in lower variables. */ + std::vector d_downPolys; + /** The constraints used to derive this interval. */ + std::vector d_origins; +}; +/** Check whether to intervals are the same. */ +bool operator==(const CACInterval& lhs, const CACInterval& rhs); +/** Compare two intervals. */ +bool operator<(const CACInterval& lhs, const CACInterval& rhs); + +/** Check whether lhs covers rhs. */ +bool intervalCovers(const poly::Interval& lhs, const poly::Interval& rhs); +/** + * Check whether two intervals connect, assuming lhs < rhs. + * They connect, if their union has no gap. + */ +bool intervalConnect(const poly::Interval& lhs, const poly::Interval& rhs); + +/** + * Sort intervals according to section 4.4.1. + * Also removes fully redundant intervals as in 4.5. 1. + */ +void cleanIntervals(std::vector& intervals); + +/** + * Collect all origins from the list of intervals to construct the origins for a + * whole covering. + */ +std::vector collectConstraints(const std::vector& intervals); + +/** + * Sample a point outside of the infeasible intervals. + * Stores the sample in sample, returns whether such a sample exists. + * If false is returned, the infeasible intervals cover the real line. + * Implements sample_outside() from section 4.3 + */ +bool sampleOutside(const std::vector& infeasible, + poly::Value& sample); + +} // namespace cad +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp index b1b9edccc..1e6ca9b5e 100644 --- a/src/theory/arith/nl/cad/constraints.cpp +++ b/src/theory/arith/nl/cad/constraints.cpp @@ -9,24 +9,18 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Implements a container for CAD constraints. ** ** Implements a container for CAD constraints. **/ -#include "constraints.h" +#include "theory/arith/nl/cad/constraints.h" #ifdef CVC4_POLY_IMP #include -#include "../poly_conversion.h" +#include "theory/arith/nl/poly_conversion.h" #include "util/poly_util.h" namespace CVC4 { @@ -35,13 +29,33 @@ namespace arith { namespace nl { namespace cad { -using namespace poly; +void Constraints::addConstraint(const poly::Polynomial& lhs, + poly::SignCondition sc, + Node n) +{ + d_constraints.emplace_back(lhs, sc, n); + sortConstraints(); +} + +void Constraints::addConstraint(Node n) +{ + auto c = as_poly_constraint(n, d_varMapper); + addConstraint(c.first, c.second, n); + sortConstraints(); +} -void Constraints::sort_constraints() +const Constraints::ConstraintVector& Constraints::getConstraints() const +{ + return d_constraints; +} + +void Constraints::reset() { d_constraints.clear(); } + +void Constraints::sortConstraints() { using Tpl = std::tuple; - std::sort(mConstraints.begin(), - mConstraints.end(), + std::sort(d_constraints.begin(), + d_constraints.end(), [](const Tpl& at, const Tpl& bt) { // Check if a is smaller than b const poly::Polynomial& a = std::get<0>(at); @@ -54,35 +68,13 @@ void Constraints::sort_constraints() if (tda != tdb) return tda < tdb; return degree(a) < degree(b); }); - for (auto& c : mConstraints) + for (auto& c : d_constraints) { auto* p = std::get<0>(c).get_internal(); lp_polynomial_set_external(p); } } -void Constraints::add_constraint(const Polynomial& lhs, - SignCondition sc, - Node n) -{ - mConstraints.emplace_back(lhs, sc, n); - sort_constraints(); -} - -void Constraints::add_constraint(Node n) -{ - auto c = as_poly_constraint(n, mVarMapper); - add_constraint(c.first, c.second, n); - sort_constraints(); -} - -const Constraints::ConstraintVector& Constraints::get_constraints() const -{ - return mConstraints; -} - -void Constraints::reset() { mConstraints.clear(); } - } // namespace cad } // namespace nl } // namespace arith diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index eda785d8e..a7989fcb6 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -9,17 +9,13 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Implements a container for CAD constraints. ** ** Implements a container for CAD constraints. **/ +#include "cvc4_private.h" + #ifndef CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H #define CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H @@ -33,9 +29,9 @@ #include #include -#include "../poly_conversion.h" #include "expr/kind.h" #include "expr/node_manager_attributes.h" +#include "theory/arith/nl/poly_conversion.h" namespace CVC4 { namespace theory { @@ -50,47 +46,46 @@ class Constraints using Constraint = std::tuple; using ConstraintVector = std::vector; - private: - /** - * A list of constraints, each comprised of a polynomial and a sign - * condition. - */ - ConstraintVector mConstraints; - - /** - * A mapping from CVC4 variables to poly variables. - */ - VariableMapper mVarMapper; - - void sort_constraints(); - - public: - VariableMapper& var_mapper() { return mVarMapper; } + VariableMapper& varMapper() { return d_varMapper; } /** * Add a constraint (represented by a polynomial and a sign condition) to the * list of constraints. */ - void add_constraint(const poly::Polynomial& lhs, - poly::SignCondition sc, - Node n); + void addConstraint(const poly::Polynomial& lhs, + poly::SignCondition sc, + Node n); /** * Add a constraints (represented by a node) to the list of constraints. * The given node can either be a negation (NOT) or a suitable relation symbol * as checked by is_suitable_relation(). */ - void add_constraint(Node n); + void addConstraint(Node n); /** * Gives the list of added constraints. */ - const ConstraintVector& get_constraints() const; + const ConstraintVector& getConstraints() const; /** * Remove all constraints. */ void reset(); + + private: + /** + * A list of constraints, each comprised of a polynomial and a sign + * condition. + */ + ConstraintVector d_constraints; + + /** + * A mapping from CVC4 variables to poly variables. + */ + VariableMapper d_varMapper; + + void sortConstraints(); }; } // namespace cad diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp index 87d8a3945..488a1f1c6 100644 --- a/src/theory/arith/nl/cad/projections.cpp +++ b/src/theory/arith/nl/cad/projections.cpp @@ -9,18 +9,12 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Implements utilities for CAD projection operators. ** ** Implements utilities for CAD projection operators. **/ -#include "projections.h" +#include "theory/arith/nl/cad/projections.h" #ifdef CVC4_POLY_IMP @@ -32,14 +26,14 @@ namespace cad { using namespace poly; -void reduce_projection_polynomials(std::vector& polys) +void reduceProjectionPolynomials(std::vector& polys) { std::sort(polys.begin(), polys.end()); auto it = std::unique(polys.begin(), polys.end()); polys.erase(it, polys.end()); } -void add_polynomial(std::vector& polys, const Polynomial& poly) +void addPolynomial(std::vector& polys, const Polynomial& poly) { for (const auto& p : square_free_factors(poly)) { @@ -48,13 +42,13 @@ void add_polynomial(std::vector& polys, const Polynomial& poly) } } -void add_polynomials(std::vector& polys, - const std::vector& p) +void addPolynomials(std::vector& polys, + const std::vector& p) { - for (const auto& q : p) add_polynomial(polys, q); + for (const auto& q : p) addPolynomial(polys, q); } -void make_finest_square_free_basis(std::vector& polys) +void makeFinestSquareFreeBasis(std::vector& polys) { for (std::size_t i = 0, n = polys.size(); i < n; ++i) { @@ -73,11 +67,11 @@ void make_finest_square_free_basis(std::vector& polys) return is_constant(p); }); polys.erase(it, polys.end()); - reduce_projection_polynomials(polys); + reduceProjectionPolynomials(polys); } -void make_finest_square_free_basis(std::vector& lhs, - std::vector& rhs) +void makeFinestSquareFreeBasis(std::vector& lhs, + std::vector& rhs) { for (std::size_t i = 0, ln = lhs.size(); i < ln; ++i) { @@ -94,8 +88,8 @@ void make_finest_square_free_basis(std::vector& lhs, } } } - reduce_projection_polynomials(lhs); - reduce_projection_polynomials(rhs); + reduceProjectionPolynomials(lhs); + reduceProjectionPolynomials(rhs); } std::vector projection_mccallum( @@ -107,19 +101,19 @@ std::vector projection_mccallum( { for (const auto& coeff : coefficients(p)) { - add_polynomial(res, coeff); + addPolynomial(res, coeff); } - add_polynomial(res, discriminant(p)); + addPolynomial(res, discriminant(p)); } for (std::size_t i = 0, n = polys.size(); i < n; ++i) { for (std::size_t j = i + 1; j < n; ++j) { - add_polynomial(res, resultant(polys[i], polys[j])); + addPolynomial(res, resultant(polys[i], polys[j])); } } - reduce_projection_polynomials(res); + reduceProjectionPolynomials(res); return res; } diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index 39d2b1221..c4a34ee56 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -9,17 +9,13 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Implements utilities for CAD projection operators. ** ** Implements utilities for CAD projection operators. **/ +#include "cvc4_private.h" + #ifndef CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H #define CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H @@ -40,33 +36,33 @@ namespace nl { namespace cad { /** Sort and remove duplicates from the list of polynomials. */ -void reduce_projection_polynomials(std::vector& polys); +void reduceProjectionPolynomials(std::vector& polys); /** * Adds a polynomial to the list of projection polynomials. * Before adding, it factorizes the polynomials and removed constant factors. */ -void add_polynomial(std::vector& polys, - const poly::Polynomial& poly); +void addPolynomial(std::vector& polys, + const poly::Polynomial& poly); /** Adds a list of polynomials using add_polynomial(). */ -void add_polynomials(std::vector& polys, - const std::vector& p); +void addPolynomials(std::vector& polys, + const std::vector& p); /** Make a set of polynomials a finest square-free basis. */ -void make_finest_square_free_basis(std::vector& polys); +void makeFinestSquareFreeBasis(std::vector& polys); /** * Ensure that two sets of polynomials are finest square-free basis relative to * each other. */ -void make_finest_square_free_basis(std::vector& lhs, - std::vector& rhs); +void makeFinestSquareFreeBasis(std::vector& lhs, + std::vector& rhs); /** * Computes McCallum's projection operator. */ -std::vector projection_mccallum( +std::vector projectionMcCallum( const std::vector& polys); } // namespace cad diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp index efb2e6350..ca87f8a83 100644 --- a/src/theory/arith/nl/cad/variable_ordering.cpp +++ b/src/theory/arith/nl/cad/variable_ordering.cpp @@ -9,18 +9,12 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Implements variable orderings tailored to CAD. ** ** Implements variable orderings tailored to CAD. **/ -#include "variable_ordering.h" +#include "theory/arith/nl/cad/variable_ordering.h" #ifdef CVC4_POLY_IMP @@ -32,12 +26,10 @@ namespace arith { namespace nl { namespace cad { -using namespace poly; - -std::vector collect_information( +std::vector collectInformation( const Constraints::ConstraintVector& polys, bool with_totals) { - VariableCollector vc; + poly::VariableCollector vc; for (const auto& c : polys) { vc(std::get<0>(c)); @@ -63,7 +55,7 @@ std::vector collect_information( return res; } -std::vector get_variables( +std::vector getVariables( const std::vector& vi) { std::vector res; @@ -74,22 +66,21 @@ std::vector get_variables( return res; } -std::vector sort_byid( - const Constraints::ConstraintVector& polys) +std::vector sortByid(const Constraints::ConstraintVector& polys) { - auto vi = collect_information(polys); + auto vi = collectInformation(polys); std::sort( vi.begin(), vi.end(), [](const poly_utils::VariableInformation& a, const poly_utils::VariableInformation& b) { return a.var < b.var; }); - return get_variables(vi); + return getVariables(vi); }; -std::vector sort_brown( +std::vector sortBrown( const Constraints::ConstraintVector& polys) { - auto vi = collect_information(polys); + auto vi = collectInformation(polys); std::sort(vi.begin(), vi.end(), [](const poly_utils::VariableInformation& a, @@ -100,13 +91,13 @@ std::vector sort_brown( return a.max_terms_tdegree > b.max_terms_tdegree; return a.num_terms > b.num_terms; }); - return get_variables(vi); + return getVariables(vi); }; -std::vector sort_triangular( +std::vector sortTriangular( const Constraints::ConstraintVector& polys) { - auto vi = collect_information(polys); + auto vi = collectInformation(polys); std::sort(vi.begin(), vi.end(), [](const poly_utils::VariableInformation& a, @@ -117,7 +108,7 @@ std::vector sort_triangular( return a.max_lc_degree > b.max_lc_degree; return a.sum_poly_degree > b.sum_poly_degree; }); - return get_variables(vi); + return getVariables(vi); }; VariableOrdering::VariableOrdering() {} @@ -129,9 +120,9 @@ std::vector VariableOrdering::operator()( { switch (vos) { - case VariableOrderingStrategy::BYID: return sort_byid(polys); - case VariableOrderingStrategy::BROWN: return sort_brown(polys); - case VariableOrderingStrategy::TRIANGULAR: return sort_triangular(polys); + case VariableOrderingStrategy::BYID: return sortByid(polys); + case VariableOrderingStrategy::BROWN: return sortBrown(polys); + case VariableOrderingStrategy::TRIANGULAR: return sortTriangular(polys); default: Assert(false) << "Unsupported variable ordering."; } return {}; diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h index 3d4bee861..8973003f7 100644 --- a/src/theory/arith/nl/cad/variable_ordering.h +++ b/src/theory/arith/nl/cad/variable_ordering.h @@ -9,17 +9,13 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Implements variable orderings tailored to CAD. ** ** Implements variable orderings tailored to CAD. **/ +#include "cvc4_private.h" + #ifndef CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H #define CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H @@ -29,7 +25,7 @@ #include -#include "constraints.h" +#include "theory/arith/nl/cad/constraints.h" #include "util/poly_util.h" namespace CVC4 { @@ -64,7 +60,7 @@ class VariableOrdering * If with_totals is set, the last element of the vector contains totals as * computed by get_variable_information if no variable is specified. */ -std::vector collect_information( +std::vector collectInformation( const Constraints::ConstraintVector& polys, bool with_totals = false); } // namespace cad diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 8292380f9..8345fc5a1 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -9,12 +9,6 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Utilities for converting to and from LibPoly objects. ** ** Utilities for converting to and from LibPoly objects. diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 73509f83c..82ae565d2 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -9,12 +9,6 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** ** \brief Utilities for converting to and from LibPoly objects. ** ** Utilities for converting to and from LibPoly objects. -- 2.30.2