src/theory/arith/nl/nl_lemma_utils.cpp

   1 /*********************                                                        */
   2 /*! \file nl_lemma_utils.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, 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 Implementation of utilities for the non-linear solver
  13  **/
  14
  15 #include "theory/arith/nl/nl_lemma_utils.h"
  16
  17 #include "theory/arith/nl/nl_model.h"
  18 #include "theory/arith/nl/nonlinear_extension.h"
  19
  20 namespace CVC5 {
  21 namespace theory {
  22 namespace arith {
  23 namespace nl {
  24
  25 TrustNode NlLemma::processLemma(LemmaProperty& p)
  26 {
  27   if (d_nlext != nullptr)
  28   {
  29     d_nlext->processSideEffect(*this);
  30   }
  31   return SimpleTheoryLemma::processLemma(p);
  32 }
  33
  34 std::ostream& operator<<(std::ostream& out, NlLemma& n)
  35 {
  36   out << n.d_node;
  37   return out;
  38 }
  39
  40 bool SortNlModel::operator()(Node i, Node j)
  41 {
  42   int cv = d_nlm->compare(i, j, d_isConcrete, d_isAbsolute);
  43   if (cv == 0)
  44   {
  45     return i < j;
  46   }
  47   return d_reverse_order ? cv < 0 : cv > 0;
  48 }
  49
  50 bool SortNonlinearDegree::operator()(Node i, Node j)
  51 {
  52   unsigned i_count = getDegree(i);
  53   unsigned j_count = getDegree(j);
  54   return i_count == j_count ? (i < j) : (i_count < j_count ? true : false);
  55 }
  56
  57 unsigned SortNonlinearDegree::getDegree(Node n) const
  58 {
  59   std::map<Node, unsigned>::const_iterator it = d_mdegree.find(n);
  60   Assert(it != d_mdegree.end());
  61   return it->second;
  62 }
  63
  64 Node ArgTrie::add(Node d, const std::vector<Node>& args)
  65 {
  66   ArgTrie* at = this;
  67   for (const Node& a : args)
  68   {
  69     at = &(at->d_children[a]);
  70   }
  71   if (at->d_data.isNull())
  72   {
  73     at->d_data = d;
  74   }
  75   return at->d_data;
  76 }
  77
  78 }  // namespace nl
  79 }  // namespace arith
  80 }  // namespace theory
  81 }  // namespace CVC5