diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-11 12:15:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-11 12:15:44 -0600 |
commit | 74aad1b10d0ed716624abfadf9cccc4ae7e4ba96 (patch) | |
tree | bced7d6863a3fd8c651ca7171323892537bbe4f8 /src/expr/subs.h | |
parent | c28f040e3b8c4aba150a61f0e42b1da7376b350e (diff) |
Add simple substitution utility (#5397)
A few new algorithms for CEGQI and single invocation sygus will use this utility for managing transformations.
Diffstat (limited to 'src/expr/subs.h')
-rw-r--r-- | src/expr/subs.h | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/src/expr/subs.h b/src/expr/subs.h new file mode 100644 index 000000000..ac678d2ee --- /dev/null +++ b/src/expr/subs.h @@ -0,0 +1,85 @@ +/********************* */ +/*! \file subs.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Simple substitution utility + **/ + +#ifndef CVC4__EXPR__SUBS_H +#define CVC4__EXPR__SUBS_H + +#include <map> +#include <vector> +#include "expr/node.h" + +namespace CVC4 { + +/** + * Helper substitution class. Stores a substitution in parallel vectors + * d_vars and d_subs, both of which may be arbitrary terms, having the same + * types pairwise. + * + * Notice this class applies substitutions using Node::substitute. Furthermore, + * it does not insist that the terms in d_vars are unique. + */ +class Subs +{ + public: + /** Is the substitution empty? */ + bool empty() const; + /** The size of the substitution */ + size_t size() const; + /** Does the substitution contain v? */ + bool contains(Node v) const; + /** Get the substitution for v if it exists, or null otherwise */ + Node getSubs(Node v) const; + /** Add v -> k for fresh skolem of the same type as v */ + void add(Node v); + /** Add v -> k for fresh skolem of the same type as v for each v in vs */ + void add(const std::vector<Node>& vs); + /** Add v -> s to the substitution */ + void add(Node v, Node s); + /** Add vs -> ss to the substitution */ + void add(const std::vector<Node>& vs, const std::vector<Node>& ss); + /** Add eq[0] -> eq[1] to the substitution */ + void addEquality(Node eq); + /** Append the substitution s to this */ + void append(Subs& s); + /** Return the result of this substitution on n */ + Node apply(Node n, bool doRewrite = false) const; + /** Return the result of the reverse of this substitution on n */ + Node rapply(Node n, bool doRewrite = false) const; + /** Apply this substitution to all nodes in the range of s */ + void applyToRange(Subs& s, bool doRewrite = false) const; + /** Apply the reverse of this substitution to all nodes in the range of s */ + void rapplyToRange(Subs& s, bool doRewrite = false) const; + /** Get equality (= v s) where v -> s is the i^th position in the vectors */ + Node getEquality(size_t i) const; + /** Convert substitution to map */ + std::map<Node, Node> toMap() const; + /** Get string for this substitution */ + std::string toString() const; + /** The data */ + std::vector<Node> d_vars; + std::vector<Node> d_subs; +}; + +/** + * Serializes a given substitution to the given stream. + * + * @param out the output stream to use + * @param s the substitution to output to the stream + * @return the stream + */ +std::ostream& operator<<(std::ostream& out, const Subs& s); + +} // namespace CVC4 + +#endif /* CVC4__EXPR__SUBS_H */ |