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