GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/subs.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

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