diff options
Diffstat (limited to 'src/expr/node_algorithm.h')
-rw-r--r-- | src/expr/node_algorithm.h | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h new file mode 100644 index 000000000..61e81c4c2 --- /dev/null +++ b/src/expr/node_algorithm.h @@ -0,0 +1,59 @@ +/********************* */ +/*! \file node_algorithm.h + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Common algorithms on nodes + ** + ** This file implements common algorithms applied to nodes, such as checking if + ** a node contains a free or a bound variable. This file should generally only + ** be included in source files. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__EXPR__NODE_ALGORITHM_H +#define __CVC4__EXPR__NODE_ALGORITHM_H + +#include <unordered_map> +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +/** + * Check if the node n has a subterm t. + * @param n The node to search in + * @param t The subterm to search for + * @param strict If true, a term is not considered to be a subterm of itself + * @return true iff t is a subterm in n + */ +bool hasSubterm(TNode n, TNode t, bool strict = false); + +/** + * Returns true iff the node n contains a bound variable. This bound + * variable may or may not be free. + * @param n The node under investigation + * @return true iff this node contains a bound variable + */ +bool hasBoundVar(TNode n); + +/** + * Returns true iff the node n contains a free variable. + * @param n The node under investigation + * @return true iff this node contains a free variable. + */ +bool hasFreeVar(TNode n); + +} // namespace expr +} // namespace CVC4 + +#endif |