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 | |
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.
-rw-r--r-- | src/expr/subs.cpp | 177 | ||||
-rw-r--r-- | src/expr/subs.h | 85 |
2 files changed, 262 insertions, 0 deletions
diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp new file mode 100644 index 000000000..541db1ac5 --- /dev/null +++ b/src/expr/subs.cpp @@ -0,0 +1,177 @@ +/********************* */ +/*! \file subs.cpp + ** \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 + **/ + +#include "expr/subs.h" + +#include "theory/rewriter.h" + +namespace CVC4 { + +bool Subs::empty() const { return d_vars.empty(); } + +size_t Subs::size() const { return d_vars.size(); } + +bool Subs::contains(Node v) const +{ + return std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end(); +} + +Node Subs::getSubs(Node v) const +{ + std::vector<Node>::const_iterator it = + std::find(d_vars.begin(), d_vars.end(), v); + if (it == d_vars.end()) + { + return Node::null(); + } + size_t i = std::distance(d_vars.begin(), it); + Assert(i < d_subs.size()); + return d_subs[i]; +} + +void Subs::add(Node v) +{ + // default, use a fresh skolem of the same type + Node s = NodeManager::currentNM()->mkSkolem("sk", v.getType()); + add(v, s); +} + +void Subs::add(const std::vector<Node>& vs) +{ + for (const Node& v : vs) + { + add(v); + } +} + +void Subs::add(Node v, Node s) +{ + Assert(v.getType().isComparableTo(s.getType())); + d_vars.push_back(v); + d_subs.push_back(s); +} + +void Subs::add(const std::vector<Node>& vs, const std::vector<Node>& ss) +{ + Assert(vs.size() == ss.size()); + for (size_t i = 0, nvs = vs.size(); i < nvs; i++) + { + add(vs[i], ss[i]); + } +} + +void Subs::addEquality(Node eq) +{ + Assert(eq.getKind() == kind::EQUAL); + add(eq[0], eq[1]); +} + +void Subs::append(Subs& s) +{ + // add the substitution list + add(s.d_vars, s.d_subs); +} + +Node Subs::apply(Node n, bool doRewrite) const +{ + if (d_vars.empty()) + { + return n; + } + Node ns = + n.substitute(d_vars.begin(), d_vars.end(), d_subs.begin(), d_subs.end()); + if (doRewrite) + { + ns = theory::Rewriter::rewrite(ns); + } + return ns; +} +Node Subs::rapply(Node n, bool doRewrite) const +{ + if (d_vars.empty()) + { + return n; + } + Node ns = + n.substitute(d_subs.begin(), d_subs.end(), d_vars.begin(), d_vars.end()); + if (doRewrite) + { + ns = theory::Rewriter::rewrite(ns); + } + return ns; +} + +void Subs::applyToRange(Subs& s, bool doRewrite) const +{ + if (d_vars.empty()) + { + return; + } + for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++) + { + s.d_subs[i] = apply(s.d_subs[i], doRewrite); + } +} + +void Subs::rapplyToRange(Subs& s, bool doRewrite) const +{ + if (d_vars.empty()) + { + return; + } + for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++) + { + s.d_subs[i] = rapply(s.d_subs[i], doRewrite); + } +} + +Node Subs::getEquality(size_t i) const +{ + Assert(i < d_vars.size()); + return d_vars[i].eqNode(d_subs[i]); +} + +std::map<Node, Node> Subs::toMap() const +{ + std::map<Node, Node> ret; + for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++) + { + ret[d_vars[i]] = d_subs[i]; + } + return ret; +} + +std::string Subs::toString() const +{ + std::stringstream ss; + ss << "["; + for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++) + { + if (i > 0) + { + ss << " "; + } + ss << d_vars[i] << " -> " << d_subs[i]; + } + ss << "]"; + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, const Subs& s) +{ + out << s.toString(); + return out; +} + +} // namespace CVC4 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 */ |