src/expr/subs.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * Simple substitution utility.
  14  */
  15
  16 #ifndef CVC5__EXPR__SUBS_H
  17 #define CVC5__EXPR__SUBS_H
  18
  19 #include <map>
  20 #include <vector>
  21 #include "expr/node.h"
  22
  23 namespace cvc5 {
  24
  25 /**
  26  * Helper substitution class. Stores a substitution in parallel vectors
  27  * d_vars and d_subs, both of which may be arbitrary terms, having the same
  28  * types pairwise.
  29  *
  30  * Notice this class applies substitutions using Node::substitute. Furthermore,
  31  * it does not insist that the terms in d_vars are unique.
  32  */
  33 class Subs
  34 {
  35  public:
  36   /** Is the substitution empty? */
  37   bool empty() const;
  38   /** The size of the substitution */
  39   size_t size() const;
  40   /** Does the substitution contain v? */
  41   bool contains(Node v) const;
  42   /** Get the substitution for v if it exists, or null otherwise */
  43   Node getSubs(Node v) const;
  44   /** Add v -> k for fresh skolem of the same type as v */
  45   void add(Node v);
  46   /** Add v -> k for fresh skolem of the same type as v for each v in vs */
  47   void add(const std::vector<Node>& vs);
  48   /** Add v -> s to the substitution */
  49   void add(Node v, Node s);
  50   /** Add vs -> ss to the substitution */
  51   void add(const std::vector<Node>& vs, const std::vector<Node>& ss);
  52   /** Add eq[0] -> eq[1] to the substitution */
  53   void addEquality(Node eq);
  54   /** Append the substitution s to this */
  55   void append(Subs& s);
  56   /** Return the result of this substitution on n */
  57   Node apply(Node n, bool doRewrite = false) const;
  58   /** Return the result of the reverse of this substitution on n */
  59   Node rapply(Node n, bool doRewrite = false) const;
  60   /** Apply this substitution to all nodes in the range of s */
  61   void applyToRange(Subs& s, bool doRewrite = false) const;
  62   /** Apply the reverse of this substitution to all nodes in the range of s */
  63   void rapplyToRange(Subs& s, bool doRewrite = false) const;
  64   /** Get equality (= v s) where v -> s is the i^th position in the vectors */
  65   Node getEquality(size_t i) const;
  66   /** Convert substitution to map */
  67   std::map<Node, Node> toMap() const;
  68   /** Get string for this substitution */
  69   std::string toString() const;
  70   /** The data */
  71   std::vector<Node> d_vars;
  72   std::vector<Node> d_subs;
  73 };
  74
  75 /**
  76  * Serializes a given substitution to the given stream.
  77  *
  78  * @param out the output stream to use
  79  * @param s the substitution to output to the stream
  80  * @return the stream
  81  */
  82 std::ostream& operator<<(std::ostream& out, const Subs& s);
  83
  84 }  // namespace cvc5
  85
  86 #endif /* CVC5__EXPR__SUBS_H */