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