1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* dynamic_rewriter |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H |
19 |
|
#define CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H |
20 |
|
|
21 |
|
#include <map> |
22 |
|
|
23 |
|
#include "context/cdlist.h" |
24 |
|
#include "theory/uf/equality_engine.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace quantifiers { |
29 |
|
|
30 |
|
/** DynamicRewriter |
31 |
|
* |
32 |
|
* This class is given a stream of equalities in calls to addRewrite(...). |
33 |
|
* The goal is to show that a subset of these can be inferred from previously |
34 |
|
* asserted equalities. For example, a possible set of return values for |
35 |
|
* add rewrite on successive calls is the following: |
36 |
|
* |
37 |
|
* addRewrite( x, y ) ---> true |
38 |
|
* addRewrite( f( x ), f( y ) ) ---> false, since we already know x=y |
39 |
|
* addRewrite( x, z ) ---> true |
40 |
|
* addRewrite( x+y, x+z ) ---> false, since we already know y=x=z. |
41 |
|
* |
42 |
|
* This class can be used to filter out redundant candidate rewrite rules |
43 |
|
* when using the option sygusRewSynth(). |
44 |
|
* |
45 |
|
* Currently, this class infers that an equality is redundant using |
46 |
|
* an instance of the equality engine that does congruence over all |
47 |
|
* operators by mapping all operators to uninterpreted ones and doing |
48 |
|
* congruence on APPLY_UF. |
49 |
|
* |
50 |
|
* TODO (#1591): Add more advanced technique, e.g. by theory rewriting |
51 |
|
* to show when terms can already be inferred equal. |
52 |
|
*/ |
53 |
|
class DynamicRewriter |
54 |
|
{ |
55 |
|
typedef context::CDList<Node> NodeList; |
56 |
|
|
57 |
|
public: |
58 |
|
DynamicRewriter(const std::string& name, context::UserContext* u); |
59 |
7 |
~DynamicRewriter() {} |
60 |
|
/** inform this class that the equality a = b holds. */ |
61 |
|
void addRewrite(Node a, Node b); |
62 |
|
/** |
63 |
|
* Check whether this class knows that the equality a = b holds. |
64 |
|
*/ |
65 |
|
bool areEqual(Node a, Node b); |
66 |
|
/** |
67 |
|
* Convert node a to its internal representation, which replaces all |
68 |
|
* interpreted operators in a by a unique uninterpreted symbol. |
69 |
|
*/ |
70 |
|
Node toInternal(Node a); |
71 |
|
/** |
72 |
|
* Convert internal node ai to its original representation. It is the case |
73 |
|
* that toExternal(toInternal(a))=a. If ai is not a term returned by |
74 |
|
* toInternal, this method returns null. |
75 |
|
*/ |
76 |
|
Node toExternal(Node ai); |
77 |
|
|
78 |
|
private: |
79 |
|
/** index over argument types to function skolems |
80 |
|
* |
81 |
|
* The purpose of this trie is to associate a class of interpreted operator |
82 |
|
* with uninterpreted symbols. It is necessary to introduce multiple |
83 |
|
* uninterpreted symbols per interpreted operator since they may be |
84 |
|
* polymorphic. For example, for array select, its associate trie may look |
85 |
|
* like this: |
86 |
|
* d_children[array_type_1] |
87 |
|
* d_children[index_type_1] : k1 |
88 |
|
* d_children[index_type_2] : k2 |
89 |
|
* d_children[array_type_2] |
90 |
|
* d_children[index_type_1] : k3 |
91 |
|
*/ |
92 |
222 |
class OpInternalSymTrie |
93 |
|
{ |
94 |
|
public: |
95 |
|
/** |
96 |
|
* Get the uninterpreted function corresponding to the top-most symbol |
97 |
|
* of the internal representation of term n. This will return a skolem |
98 |
|
* of the same type as n.getOperator() if it has one, or of the same type |
99 |
|
* as n itself otherwise. |
100 |
|
*/ |
101 |
|
Node getSymbol(Node n); |
102 |
|
|
103 |
|
private: |
104 |
|
/** the symbol at this node in the trie */ |
105 |
|
Node d_sym; |
106 |
|
/** the children of this node in the trie */ |
107 |
|
std::map<TypeNode, OpInternalSymTrie> d_children; |
108 |
|
}; |
109 |
|
/** the internal operator symbol trie for this class */ |
110 |
|
std::map<Node, OpInternalSymTrie> d_ois_trie; |
111 |
|
/** cache of the above function */ |
112 |
|
std::map<Node, Node> d_term_to_internal; |
113 |
|
/** inverse of the above map */ |
114 |
|
std::map<Node, Node> d_internal_to_term; |
115 |
|
/** stores congruence closure over terms given to this class. */ |
116 |
|
eq::EqualityEngine d_equalityEngine; |
117 |
|
/** list of all equalities asserted to equality engine */ |
118 |
|
NodeList d_rewrites; |
119 |
|
}; |
120 |
|
|
121 |
|
} // namespace quantifiers |
122 |
|
} // namespace theory |
123 |
|
} // namespace cvc5 |
124 |
|
|
125 |
|
#endif /* CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */ |