diff options
Diffstat (limited to 'src/theory/quantifiers/extended_rewrite.h')
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.h | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 9a0ab6382..5ed6ee3f3 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -2,9 +2,9 @@ /*! \file extended_rewrite.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** 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 @@ -200,11 +200,17 @@ class ExtendedRewriter /** Partial substitute * * Applies the substitution specified by assign to n, recursing only beneath - * terms whose Kind appears in rec_kinds. + * terms whose Kind appears in rkinds (when rkinds is empty), and additionally + * never recursing beneath WITNESS. */ Node partialSubstitute(Node n, - std::map<Node, Node>& assign, - std::map<Kind, bool>& rkinds); + const std::map<Node, Node>& assign, + const std::map<Kind, bool>& rkinds); + /** same as above, with vectors */ + Node partialSubstitute(Node n, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + const std::map<Kind, bool>& rkinds); /** solve equality * * If this function returns a non-null node n', then n' is equivalent to n |