Branch data     Line data    Source code

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