GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/match_trie.h Lines: 3 3 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file match_trie.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Andres Noetzli
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 Implements a match trie, also known as a discrimination tree.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__MATCH_TRIE_H
18
#define CVC4__EXPR__MATCH_TRIE_H
19
20
#include <map>
21
#include <vector>
22
23
#include "expr/node.h"
24
25
namespace CVC4 {
26
namespace expr {
27
28
/** A virtual class for notifications regarding matches. */
29
12
class NotifyMatch
30
{
31
 public:
32
12
  virtual ~NotifyMatch() {}
33
  /**
34
   * A notification that s is equal to n * { vars -> subs }. This function
35
   * should return false if we do not wish to be notified of further matches.
36
   */
37
  virtual bool notify(Node s,
38
                      Node n,
39
                      std::vector<Node>& vars,
40
                      std::vector<Node>& subs) = 0;
41
};
42
43
/**
44
 * A trie (discrimination tree) storing a set of terms S, that can be used to
45
 * query, for a given term t, all terms s from S that are matchable with t,
46
 * that is s*sigma = t for some substitution sigma.
47
 */
48
1212
class MatchTrie
49
{
50
 public:
51
  /** Get matches
52
   *
53
   * This calls ntm->notify( n, s, vars, subs ) for each term s stored in this
54
   * trie that is matchable with n where s = n * { vars -> subs } for some
55
   * vars, subs. This function returns false if one of these calls to notify
56
   * returns false.
57
   */
58
  bool getMatches(Node n, NotifyMatch* ntm);
59
  /** Adds node n to this trie */
60
  void addTerm(Node n);
61
  /** Clear this trie */
62
  void clear();
63
64
 private:
65
  /**
66
   * The children of this node in the trie. Terms t are indexed by a
67
   * depth-first (right to left) traversal on its subterms, where the
68
   * top-symbol of t is indexed by:
69
   * - (operator, #children) if t has an operator, or
70
   * - (t, 0) if t does not have an operator.
71
   */
72
  std::map<Node, std::map<unsigned, MatchTrie> > d_children;
73
  /** The set of variables in the domain of d_children */
74
  std::vector<Node> d_vars;
75
  /** The data of this node in the trie */
76
  Node d_data;
77
};
78
79
}  // namespace expr
80
}  // namespace CVC4
81
82
#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */