GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/monomial.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file monomial.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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 Utilities for monomials
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_H
16
#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_H
17
18
#include <map>
19
#include <vector>
20
21
#include "expr/node.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace arith {
26
namespace nl {
27
28
class MonomialDb;
29
class NlModel;
30
31
typedef std::map<Node, unsigned> NodeMultiset;
32
typedef std::map<Node, NodeMultiset> MonomialExponentMap;
33
34
/** An index data structure for node multisets (monomials) */
35
15421
class MonomialIndex
36
{
37
 public:
38
  /**
39
   * Add term to this trie. The argument status indicates what the status
40
   * of n is with respect to the current node in the trie, where:
41
   *   0 : n is equal, -1 : n is superset, 1 : n is subset
42
   * of the node described by the current path in the trie.
43
   */
44
  void addTerm(Node n,
45
               const std::vector<Node>& reps,
46
               MonomialDb* nla,
47
               int status = 0,
48
               unsigned argIndex = 0);
49
50
 private:
51
  /** The children of this node */
52
  std::map<Node, MonomialIndex> d_data;
53
  /** The monomials at this node */
54
  std::vector<Node> d_monos;
55
}; /* class MonomialIndex */
56
57
/** Context-independent database for monomial information */
58
class MonomialDb
59
{
60
 public:
61
  MonomialDb();
62
4386
  ~MonomialDb() {}
63
  /** register monomial */
64
  void registerMonomial(Node n);
65
  /**
66
   * Register monomial subset. This method is called when we infer that b is
67
   * a subset of monomial a, e.g. x*y^2 is a subset of x^3*y^2*z.
68
   */
69
  void registerMonomialSubset(Node a, Node b);
70
  /**
71
   * returns true if the multiset containing the
72
   * factors of monomial a is a subset of the multiset
73
   * containing the factors of monomial b.
74
   */
75
  bool isMonomialSubset(Node a, Node b) const;
76
  /** Returns the NodeMultiset for a registered monomial. */
77
  const NodeMultiset& getMonomialExponentMap(Node monomial) const;
78
  /** Returns the exponent of variable v in the given monomial */
79
  unsigned getExponent(Node monomial, Node v) const;
80
  /** Get the list of unique variables is the monomial */
81
  const std::vector<Node>& getVariableList(Node monomial) const;
82
  /** Get degree of monomial, e.g. the degree of x^2*y^2 = 4 */
83
  unsigned getDegree(Node monomial) const;
84
  /** Sort monomials in ms by their degree
85
   *
86
   * Updates ms so that degree(ms[i]) <= degree(ms[j]) for i <= j.
87
   */
88
  void sortByDegree(std::vector<Node>& ms) const;
89
  /** Sort the variable lists based on model values
90
   *
91
   * This updates the variable lists of monomials in ms based on the absolute
92
   * value of their current model values in m.
93
   *
94
   * In other words, for each i, getVariableList(ms[i]) returns
95
   * v1, ..., vn where |m(v1)| <= ... <= |m(vn)| after this method is invoked.
96
   */
97
  void sortVariablesByModel(std::vector<Node>& ms, NlModel& m);
98
  /** Get monomial contains children map
99
   *
100
   * This maps monomials to other monomials that are contained in them, e.g.
101
   * x^2 * y may map to { x, x^2, y } if these three terms exist have been
102
   * registered to this class.
103
   */
104
  const std::map<Node, std::vector<Node> >& getContainsChildrenMap();
105
  /** Get monomial contains parent map, reverse of above */
106
  const std::map<Node, std::vector<Node> >& getContainsParentMap();
107
  /**
108
   * Get contains difference. Return the difference of a and b or null if it
109
   * does not exist. In other words, this returns a term equivalent to a/b
110
   * that does not contain division.
111
   */
112
  Node getContainsDiff(Node a, Node b) const;
113
  /**
114
   * Get contains difference non-linear. Same as above, but stores terms of kind
115
   * NONLINEAR_MULT instead of MULT.
116
   */
117
  Node getContainsDiffNl(Node a, Node b) const;
118
  /** Make monomial remainder factor */
119
  Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const;
120
121
 private:
122
  /** commonly used terms */
123
  Node d_one;
124
  /** list of all monomials */
125
  std::vector<Node> d_monomials;
126
  /** Map from monomials to var^index. */
127
  MonomialExponentMap d_m_exp;
128
  /**
129
   * Mapping from monomials to the list of variables that occur in it. For
130
   * example, x*x*y*z -> { x, y, z }.
131
   */
132
  std::map<Node, std::vector<Node> > d_m_vlist;
133
  /** Degree information */
134
  std::map<Node, unsigned> d_m_degree;
135
  /** monomial index, by sorted variables */
136
  MonomialIndex d_m_index;
137
  /** containment ordering */
138
  std::map<Node, std::vector<Node> > d_m_contain_children;
139
  std::map<Node, std::vector<Node> > d_m_contain_parent;
140
  std::map<Node, std::map<Node, Node> > d_m_contain_mult;
141
  std::map<Node, std::map<Node, Node> > d_m_contain_umult;
142
};
143
144
}  // namespace nl
145
}  // namespace arith
146
}  // namespace theory
147
}  // namespace CVC4
148
149
#endif /* CVC4__THEORY__ARITH__NL_MONOMIAL_H */