diff options
Diffstat (limited to 'src/theory/arith/nl/nl_lemma_utils.cpp')
-rw-r--r-- | src/theory/arith/nl/nl_lemma_utils.cpp | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp new file mode 100644 index 000000000..ca34d91a9 --- /dev/null +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -0,0 +1,65 @@ +/********************* */ +/*! \file nl_lemma_utils.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implementation of utilities for the non-linear solver + **/ + +#include "theory/arith/nl/nl_lemma_utils.h" + +#include "theory/arith/nl/nl_model.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +bool SortNlModel::operator()(Node i, Node j) +{ + int cv = d_nlm->compare(i, j, d_isConcrete, d_isAbsolute); + if (cv == 0) + { + return i < j; + } + return d_reverse_order ? cv < 0 : cv > 0; +} + +bool SortNonlinearDegree::operator()(Node i, Node j) +{ + unsigned i_count = getDegree(i); + unsigned j_count = getDegree(j); + return i_count == j_count ? (i < j) : (i_count < j_count ? true : false); +} + +unsigned SortNonlinearDegree::getDegree(Node n) const +{ + std::map<Node, unsigned>::const_iterator it = d_mdegree.find(n); + Assert(it != d_mdegree.end()); + return it->second; +} + +Node ArgTrie::add(Node d, const std::vector<Node>& args) +{ + ArgTrie* at = this; + for (const Node& a : args) + { + at = &(at->d_children[a]); + } + if (at->d_data.isNull()) + { + at->d_data = d; + } + return at->d_data; +} + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 |