diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-02 09:46:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-02 09:46:15 -0500 |
commit | 9720e341d9cda3de7e7b2b0c25afe190cc2021e4 (patch) | |
tree | cb44e6cd092956a05ac00d4104d19bd0e1f36eb4 /src/theory/arith/nl_lemma_utils.h | |
parent | 796703fc72cfd67dc05357b10a5f0311200f2865 (diff) | |
parent | aa6fb6fa3df0b1519e6763e72541c022396ab1dc (diff) |
Merge branch 'master' into rmAliasesrmAliases
Diffstat (limited to 'src/theory/arith/nl_lemma_utils.h')
-rw-r--r-- | src/theory/arith/nl_lemma_utils.h | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/src/theory/arith/nl_lemma_utils.h b/src/theory/arith/nl_lemma_utils.h index 74886a1fb..9ad9f2ca5 100644 --- a/src/theory/arith/nl_lemma_utils.h +++ b/src/theory/arith/nl_lemma_utils.h @@ -23,6 +23,8 @@ namespace CVC4 { namespace theory { namespace arith { +class NlModel; + /** * A side effect of adding a lemma in the non-linear solver. This is used * to specify how the state of the non-linear solver should update. This @@ -46,6 +48,56 @@ struct NlLemmaSideEffect std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint; }; +struct SortNlModel +{ + SortNlModel() + : d_nlm(nullptr), + d_isConcrete(true), + d_isAbsolute(false), + d_reverse_order(false) + { + } + /** pointer to the model */ + NlModel* d_nlm; + /** are we comparing concrete model values? */ + bool d_isConcrete; + /** are we comparing absolute values? */ + bool d_isAbsolute; + /** are we in reverse order? */ + bool d_reverse_order; + /** the comparison */ + bool operator()(Node i, Node j); +}; + +struct SortNonlinearDegree +{ + SortNonlinearDegree(std::map<Node, unsigned>& m) : d_mdegree(m) {} + /** pointer to the non-linear extension */ + std::map<Node, unsigned>& d_mdegree; + /** Get the degree of n in d_mdegree */ + unsigned getDegree(Node n) const; + /** + * Sorts by degree of the monomials, where lower degree monomials come + * first. + */ + bool operator()(Node i, Node j); +}; + +/** An argument trie, for computing congruent terms */ +class ArgTrie +{ + public: + /** children of this node */ + std::map<Node, ArgTrie> d_children; + /** the data of this node */ + Node d_data; + /** + * Set d as the data on the node whose path is [args], return either d if + * that node has no data, or the data that already occurs there. + */ + Node add(Node d, const std::vector<Node>& args); +}; + } // namespace arith } // namespace theory } // namespace CVC4 |