src/theory/arith/nl/cad/constraints.cpp

   1 /*********************                                                        */
   2 /*! \file constraints.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Gereon Kremer
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implements a container for CAD constraints.
  13  **
  14  ** Implements a container for CAD constraints.
  15  **/
  16
  17 #include "theory/arith/nl/cad/constraints.h"
  18
  19 #ifdef CVC4_POLY_IMP
  20
  21 #include <algorithm>
  22
  23 #include "theory/arith/nl/poly_conversion.h"
  24 #include "util/poly_util.h"
  25
  26 namespace CVC5 {
  27 namespace theory {
  28 namespace arith {
  29 namespace nl {
  30 namespace cad {
  31
  32 void Constraints::addConstraint(const poly::Polynomial& lhs,
  33                                 poly::SignCondition sc,
  34                                 Node n)
  35 {
  36   d_constraints.emplace_back(lhs, sc, n);
  37   sortConstraints();
  38 }
  39
  40 void Constraints::addConstraint(Node n)
  41 {
  42   auto c = as_poly_constraint(n, d_varMapper);
  43   addConstraint(c.first, c.second, n);
  44   sortConstraints();
  45 }
  46
  47 const Constraints::ConstraintVector& Constraints::getConstraints() const
  48 {
  49   return d_constraints;
  50 }
  51
  52 void Constraints::reset() { d_constraints.clear(); }
  53
  54 void Constraints::sortConstraints()
  55 {
  56   using Tpl = std::tuple<poly::Polynomial, poly::SignCondition, Node>;
  57   std::sort(d_constraints.begin(),
  58             d_constraints.end(),
  59             [](const Tpl& at, const Tpl& bt) {
  60               // Check if a is smaller than b
  61               const poly::Polynomial& a = std::get<0>(at);
  62               const poly::Polynomial& b = std::get<0>(bt);
  63               bool ua = is_univariate(a);
  64               bool ub = is_univariate(b);
  65               if (ua != ub) return ua;
  66               std::size_t tda = poly_utils::totalDegree(a);
  67               std::size_t tdb = poly_utils::totalDegree(b);
  68               if (tda != tdb) return tda < tdb;
  69               return degree(a) < degree(b);
  70             });
  71   for (auto& c : d_constraints)
  72   {
  73     auto* p = std::get<0>(c).get_internal();
  74     lp_polynomial_set_external(p);
  75   }
  76 }
  77
  78 }  // namespace cad
  79 }  // namespace nl
  80 }  // namespace arith
  81 }  // namespace theory
  82 }  // namespace CVC5
  83
  84 #endif