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                 :            :  * A substitution mapping for theory simplification.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__THEORY__SUBSTITUTIONS_H
      16                 :            : #define CVC5__THEORY__SUBSTITUTIONS_H
      17                 :            : 
      18                 :            : // #include <algorithm>
      19                 :            : #include <unordered_map>
      20                 :            : #include <utility>
      21                 :            : #include <vector>
      22                 :            : 
      23                 :            : #include "context/cdhashmap.h"
      24                 :            : #include "context/cdo.h"
      25                 :            : #include "context/context.h"
      26                 :            : #include "expr/node.h"
      27                 :            : #include "util/hash.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : namespace theory {
      31                 :            : 
      32                 :            : class Rewriter;
      33                 :            : 
      34                 :            : /**
      35                 :            :  * The type for the Substitutions mapping output by
      36                 :            :  * Theory::simplify(), TheoryEngine::simplify(), and
      37                 :            :  * Valuation::simplify().  This is in its own header to
      38                 :            :  * avoid circular dependences between those three.
      39                 :            :  *
      40                 :            :  * This map is context-dependent.
      41                 :            :  */
      42                 :            : class SubstitutionMap
      43                 :            : {
      44                 :            :  public:
      45                 :            :   typedef context::CDHashMap<Node, Node> NodeMap;
      46                 :            : 
      47                 :            :   typedef NodeMap::iterator iterator;
      48                 :            :   typedef NodeMap::const_iterator const_iterator;
      49                 :            : 
      50                 :            :   struct ShouldTraverseCallback
      51                 :            :   {
      52                 :            :     virtual bool operator()(TNode n) const = 0;
      53                 :        165 :     virtual ~ShouldTraverseCallback() {}
      54                 :            :   };
      55                 :            : 
      56                 :            :  private:
      57                 :            :   typedef std::unordered_map<Node, Node> NodeCache;
      58                 :            :   /** A dummy context used by this class if none is provided */
      59                 :            :   context::Context d_context;
      60                 :            : 
      61                 :            :   /** The variables, in order of addition */
      62                 :            :   NodeMap d_substitutions;
      63                 :            : 
      64                 :            :   /** Cache of the already performed substitutions */
      65                 :            :   NodeCache d_substitutionCache;
      66                 :            : 
      67                 :            :   /** Has the cache been invalidated? */
      68                 :            :   bool d_cacheInvalidated;
      69                 :            : 
      70                 :            :   /** Are we using substitution compression */
      71                 :            :   bool d_compress;
      72                 :            : 
      73                 :            :   /** Internal method that performs substitution */
      74                 :            :   Node internalSubstitute(TNode t,
      75                 :            :                           NodeCache& cache,
      76                 :            :                           std::set<TNode>* tracker,
      77                 :            :                           const ShouldTraverseCallback* stc);
      78                 :            : 
      79                 :            :   /** Helper class to invalidate cache on user pop */
      80                 :            :   class CacheInvalidator : public context::ContextNotifyObj
      81                 :            :   {
      82                 :            :     bool& d_cacheInvalidated;
      83                 :            : 
      84                 :            :    protected:
      85                 :    8997971 :     void contextNotifyPop() override { d_cacheInvalidated = true; }
      86                 :            : 
      87                 :            :    public:
      88                 :     268385 :     CacheInvalidator(context::Context* context, bool& cacheInvalidated)
      89                 :     268385 :         : context::ContextNotifyObj(context),
      90                 :     268385 :           d_cacheInvalidated(cacheInvalidated)
      91                 :            :     {
      92                 :     268385 :     }
      93                 :            : 
      94                 :            :   }; /* class SubstitutionMap::CacheInvalidator */
      95                 :            : 
      96                 :            :   /**
      97                 :            :    * This object is notified on user pop and marks the SubstitutionMap's
      98                 :            :    * cache as invalidated.
      99                 :            :    */
     100                 :            :   CacheInvalidator d_cacheInvalidator;
     101                 :            : 
     102                 :            :  public:
     103                 :            :   /**
     104                 :            :    * @param context The context this substitution depends on.
     105                 :            :    * @param compress If true, we may update the range of substitutions based
     106                 :            :    * on further substitutions. For example, if we add {y -> f(x)} and later
     107                 :            :    * add {x -> a}, then we may update the substitution to {y -> f(a), x -> a}.
     108                 :            :    */
     109                 :            :   SubstitutionMap(context::Context* context = nullptr, bool compress = true);
     110                 :            : 
     111                 :            :   /** Get substitutions in this object as a raw map */
     112                 :            :   std::unordered_map<Node, Node> getSubstitutions() const;
     113                 :            :   /**
     114                 :            :    * Return a formula that is equivalent to this substitution, e.g. for
     115                 :            :    * [x -> t, y -> s], we return (and (= x t) (= y s)).
     116                 :            :    */
     117                 :            :   Node toFormula(NodeManager* nm) const;
     118                 :            :   /**
     119                 :            :    * Adds a substitution from x to t.
     120                 :            :    */
     121                 :            :   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
     122                 :            : 
     123                 :            :   /**
     124                 :            :    * Merge subMap into current set of substitutions
     125                 :            :    */
     126                 :            :   void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true);
     127                 :            : 
     128                 :            :   /**
     129                 :            :    * Erase substitution. This erases x from the domain of this substitution.
     130                 :            :    * This method should only be called if compression is disabled, since
     131                 :            :    * if compression is enabled, then the substituion of x may have been
     132                 :            :    * applied to the range of other substitutions in this class, and erasing
     133                 :            :    * the entry for x would not undo those changes.
     134                 :            :    * @param x The variable to erase.
     135                 :            :    * @param invalidateCache If true, we clear the cache.
     136                 :            :    */
     137                 :            :   void eraseSubstitution(TNode x, bool invalidateCache = true);
     138                 :            : 
     139                 :            :   /** Size of the substitutions */
     140                 :          0 :   size_t size() const { return d_substitutions.size(); }
     141                 :            :   /**
     142                 :            :    * Returns true iff x is in the substitution map
     143                 :            :    */
     144                 :      30368 :   bool hasSubstitution(TNode x) const
     145                 :            :   {
     146                 :      30368 :     return d_substitutions.find(x) != d_substitutions.end();
     147                 :            :   }
     148                 :            : 
     149                 :            :   /**
     150                 :            :    * Returns the substitution mapping that was given for x via
     151                 :            :    * addSubstitution().  Note that the returned value might itself
     152                 :            :    * be in the map; for the actual substitution that would be
     153                 :            :    * performed for x, use .apply(x).  This getSubstitution() function
     154                 :            :    * is mainly intended for constructing assertions about what has
     155                 :            :    * already been put in the map.
     156                 :            :    */
     157                 :          0 :   TNode getSubstitution(TNode x) const
     158                 :            :   {
     159         [ -  - ]:          0 :     AssertArgument(
     160                 :            :         hasSubstitution(x), x, "element not in this substitution map");
     161                 :          0 :     return (*d_substitutions.find(x)).second;
     162                 :            :   }
     163                 :            : 
     164                 :            :   /**
     165                 :            :    * Apply the substitutions to the node, optionally rewrite if a non-null
     166                 :            :    * Rewriter pointer is passed.
     167                 :            :    */
     168                 :            :   Node apply(TNode t,
     169                 :            :              Rewriter* r = nullptr,
     170                 :            :              std::set<TNode>* tracker = nullptr,
     171                 :            :              const ShouldTraverseCallback* stc = nullptr);
     172                 :            : 
     173                 :            :   /**
     174                 :            :    * Apply the substitutions to the node.
     175                 :            :    */
     176                 :         56 :   Node apply(TNode t, Rewriter* r = nullptr) const
     177                 :            :   {
     178                 :         56 :     return const_cast<SubstitutionMap*>(this)->apply(t, r);
     179                 :            :   }
     180                 :            : 
     181                 :      95031 :   iterator begin() { return d_substitutions.begin(); }
     182                 :            : 
     183                 :     175389 :   iterator end() { return d_substitutions.end(); }
     184                 :            : 
     185                 :        121 :   const_iterator begin() const { return d_substitutions.begin(); }
     186                 :            : 
     187                 :        121 :   const_iterator end() const { return d_substitutions.end(); }
     188                 :            : 
     189                 :        188 :   bool empty() const { return d_substitutions.empty(); }
     190                 :            : 
     191                 :            :   /**
     192                 :            :    * Print to the output stream
     193                 :            :    */
     194                 :            :   void print(std::ostream& out) const;
     195                 :            :   /** To string */
     196                 :            :   std::string toString() const;
     197                 :            : 
     198                 :       9565 :   void invalidateCache() { d_cacheInvalidated = true; }
     199                 :            : 
     200                 :            : }; /* class SubstitutionMap */
     201                 :            : 
     202                 :            : inline std::ostream& operator<<(std::ostream& out, const SubstitutionMap& subst)
     203                 :            : {
     204                 :            :   subst.print(out);
     205                 :            :   return out;
     206                 :            : }
     207                 :            : 
     208                 :            : }  // namespace theory
     209                 :            : 
     210                 :            : std::ostream& operator<<(std::ostream& out,
     211                 :            :                          const theory::SubstitutionMap::iterator& i);
     212                 :            : 
     213                 :            : }  // namespace cvc5::internal
     214                 :            : 
     215                 :            : #endif /* CVC5__THEORY__SUBSTITUTIONS_H */