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
--- /dev/null
+/********************* */
+/*! \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<poly::Variable>& 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<poly::Variable>& CDCAC::getVariableOrdering() const
+{
+ return d_variableOrdering;
+}
+
+std::vector<CACInterval> CDCAC::getUnsatIntervals(
+ std::size_t cur_variable) const
+{
+ return {};
+}
+
+std::vector<poly::Polynomial> CDCAC::requiredCoefficients(
+ const poly::Polynomial& p) const
+{
+ return {};
+}
+
+std::vector<poly::Polynomial> CDCAC::constructCharacterization(
+ std::vector<CACInterval>& intervals)
+{
+ return {};
+}
+
+CACInterval CDCAC::intervalFromCharacterization(
+ const std::vector<poly::Polynomial>& characterization,
+ std::size_t cur_variable,
+ const poly::Value& sample)
+{
+ return {};
+}
+
+std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
+{
+ return {};
+}
+
+} // namespace cad
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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 <poly/polyxx.h>
+
+#include <vector>
+
+#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<poly::Variable>& 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<poly::Variable>& 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<CACInterval> getUnsatIntervals(std::size_t cur_variable) const;
+
+ /**
+ * Collects the coefficients required for projection from the given
+ * polynomial. Implements Algorithm 6.
+ */
+ std::vector<poly::Polynomial> 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<poly::Polynomial> constructCharacterization(
+ std::vector<CACInterval>& intervals);
+
+ /**
+ * Constructs an infeasible interval from a characterization.
+ * Implements Algorithm 5.
+ */
+ CACInterval intervalFromCharacterization(
+ const std::vector<poly::Polynomial>& 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<CACInterval> 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<poly::Variable> d_variableOrdering;
+
+ /** The object computing the variable ordering. */
+ VariableOrdering d_varOrder;
+};
+
+} // namespace cad
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \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<CACInterval>& 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<Node> collectConstraints(const std::vector<CACInterval>& intervals)
+{
+ std::vector<Node> 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<CACInterval>& 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
--- /dev/null
+/********************* */
+/*! \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 <poly/polyxx.h>
+
+#include <vector>
+
+#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<poly::Polynomial> d_lowerPolys;
+ /** The polynomials characterizing the upper bound. */
+ std::vector<poly::Polynomial> d_upperPolys;
+ /** The characterizing polynomials in the main variable. */
+ std::vector<poly::Polynomial> d_mainPolys;
+ /** The characterizing polynomials in lower variables. */
+ std::vector<poly::Polynomial> d_downPolys;
+ /** The constraints used to derive this interval. */
+ std::vector<Node> 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<CACInterval>& intervals);
+
+/**
+ * Collect all origins from the list of intervals to construct the origins for a
+ * whole covering.
+ */
+std::vector<Node> collectConstraints(const std::vector<CACInterval>& 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<CACInterval>& infeasible,
+ poly::Value& sample);
+
+} // namespace cad
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif
** 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 <algorithm>
-#include "../poly_conversion.h"
+#include "theory/arith/nl/poly_conversion.h"
#include "util/poly_util.h"
namespace CVC4 {
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<poly::Polynomial, poly::SignCondition, Node>;
- 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);
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
** 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
#include <tuple>
#include <vector>
-#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 {
using Constraint = std::tuple<poly::Polynomial, poly::SignCondition, Node>;
using ConstraintVector = std::vector<Constraint>;
- 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
** 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
using namespace poly;
-void reduce
_projection_polynomials(std::vector<Polynomial>& polys)
+void reduce
ProjectionPolynomials(std::vector<Polynomial>& 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<Polynomial>& polys, const Polynomial& poly)
+void add
Polynomial(std::vector<Polynomial>& polys, const Polynomial& poly)
{
for (const auto& p : square_free_factors(poly))
{
}
}
-void add
_polynomials(std::vector<Polynomial>& polys,
-
const std::vector<Polynomial>& p)
+void add
Polynomials(std::vector<Polynomial>& polys,
+ const std::vector<Polynomial>& 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<Polynomial>& polys)
+void make
FinestSquareFreeBasis(std::vector<Polynomial>& polys)
{
for (std::size_t i = 0, n = polys.size(); i < n; ++i)
{
return is_constant(p);
});
polys.erase(it, polys.end());
- reduce_projection_polynomials(polys);
+ reduceProjectionPolynomials(polys);
}
-void make
_finest_square_free_basis(std::vector<poly::Polynomial>& lhs,
-
std::vector<poly::Polynomial>& rhs)
+void make
FinestSquareFreeBasis(std::vector<poly::Polynomial>& lhs,
+ std::vector<poly::Polynomial>& rhs)
{
for (std::size_t i = 0, ln = lhs.size(); i < ln; ++i)
{
}
}
}
- reduce_projection_polynomials(lhs);
- reduce_projection_polynomials(rhs);
+ reduceProjectionPolynomials(lhs);
+ reduceProjectionPolynomials(rhs);
}
std::vector<Polynomial> 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;
}
** 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
namespace cad {
/** Sort and remove duplicates from the list of polynomials. */
-void reduce
_projection_polynomials(std::vector<poly::Polynomial>& polys);
+void reduce
ProjectionPolynomials(std::vector<poly::Polynomial>& 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<poly::Polynomial>& polys,
- const poly::Polynomial& poly);
+void add
Polynomial(std::vector<poly::Polynomial>& polys,
+ const poly::Polynomial& poly);
/** Adds a list of polynomials using add_polynomial(). */
-void add
_polynomials(std::vector<poly::Polynomial>& polys,
-
const std::vector<poly::Polynomial>& p);
+void add
Polynomials(std::vector<poly::Polynomial>& polys,
+ const std::vector<poly::Polynomial>& p);
/** Make a set of polynomials a finest square-free basis. */
-void make
_finest_square_free_basis(std::vector<poly::Polynomial>& polys);
+void make
FinestSquareFreeBasis(std::vector<poly::Polynomial>& polys);
/**
* Ensure that two sets of polynomials are finest square-free basis relative to
* each other.
*/
-void make
_finest_square_free_basis(std::vector<poly::Polynomial>& lhs,
-
std::vector<poly::Polynomial>& rhs);
+void make
FinestSquareFreeBasis(std::vector<poly::Polynomial>& lhs,
+ std::vector<poly::Polynomial>& rhs);
/**
* Computes McCallum's projection operator.
*/
-std::vector<poly::Polynomial> projection_mccallum(
+std::vector<poly::Polynomial> projectionMcCallum(
const std::vector<poly::Polynomial>& polys);
} // namespace cad
** 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
namespace nl {
namespace cad {
-using namespace poly;
-
-std::vector<poly_utils::VariableInformation> collect_information(
+std::vector<poly_utils::VariableInformation> collectInformation(
const Constraints::ConstraintVector& polys, bool with_totals)
{
- VariableCollector vc;
+ poly::VariableCollector vc;
for (const auto& c : polys)
{
vc(std::get<0>(c));
return res;
}
-std::vector<poly::Variable> get_variables(
+std::vector<poly::Variable> getVariables(
const std::vector<poly_utils::VariableInformation>& vi)
{
std::vector<poly::Variable> res;
return res;
}
-std::vector<poly::Variable> sort_byid(
- const Constraints::ConstraintVector& polys)
+std::vector<poly::Variable> 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<poly::Variable> sort_brown(
+std::vector<poly::Variable> 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,
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<poly::Variable> sort_triangular(
+std::vector<poly::Variable> 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,
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() {}
{
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 {};
** 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
#include <poly/polyxx.h>
-#include "constraints.h"
+#include "theory/arith/nl/cad/constraints.h"
#include "util/poly_util.h"
namespace CVC4 {
* 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<poly_utils::VariableInformation> collect_information(
+std::vector<poly_utils::VariableInformation> collectInformation(
const Constraints::ConstraintVector& polys, bool with_totals = false);
} // namespace cad
** 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.
** 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.
projects / cvc5.git / commitdiff