1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Andres Noetzli, 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 |
|
* [[ Add one-line brief description here ]] |
14 |
|
* |
15 |
|
* [[ Add lengthier description here ]] |
16 |
|
* \todo document this file |
17 |
|
*/ |
18 |
|
|
19 |
|
#include "cvc5_private.h" |
20 |
|
|
21 |
|
#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H |
22 |
|
#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H |
23 |
|
|
24 |
|
#include "theory/theory_rewriter.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace builtin { |
29 |
|
|
30 |
19881 |
class TheoryBuiltinRewriter : public TheoryRewriter |
31 |
|
{ |
32 |
|
static Node blastDistinct(TNode node); |
33 |
|
|
34 |
|
public: |
35 |
|
|
36 |
|
RewriteResponse postRewrite(TNode node) override; |
37 |
|
|
38 |
436172 |
RewriteResponse preRewrite(TNode node) override { return doRewrite(node); } |
39 |
|
|
40 |
|
// conversions between lambdas and arrays |
41 |
|
private: |
42 |
|
/** recursive helper for getLambdaForArrayRepresentation */ |
43 |
|
static Node getLambdaForArrayRepresentationRec( |
44 |
|
TNode a, |
45 |
|
TNode bvl, |
46 |
|
unsigned bvlIndex, |
47 |
|
std::unordered_map<TNode, Node>& visited); |
48 |
|
/** recursive helper for getArrayRepresentationForLambda */ |
49 |
|
static Node getArrayRepresentationForLambdaRec(TNode n, TypeNode retType); |
50 |
|
|
51 |
|
public: |
52 |
|
/** |
53 |
|
* The default rewriter for rewrites that occur at both pre and post rewrite. |
54 |
|
*/ |
55 |
|
static RewriteResponse doRewrite(TNode node); |
56 |
|
/** |
57 |
|
* Main entry point for rewriting terms of the form (witness ((x T)) (P x)). |
58 |
|
* Returns the rewritten form of node. |
59 |
|
*/ |
60 |
|
static Node rewriteWitness(TNode node); |
61 |
|
/** Get function type for array type |
62 |
|
* |
63 |
|
* This returns the function type of terms returned by the function |
64 |
|
* getLambdaForArrayRepresentation( t, bvl ), |
65 |
|
* where t.getType()=atn. |
66 |
|
* |
67 |
|
* bvl should be a bound variable list whose variables correspond in-order |
68 |
|
* to the index types of the (curried) Array type. For example, a bound |
69 |
|
* variable list bvl whose variables have types (Int, Real) can be given as |
70 |
|
* input when paired with atn = (Array Int (Array Real Bool)), or (Array Int |
71 |
|
* (Array Real (Array Bool Bool))). This function returns (-> Int Real Bool) |
72 |
|
* and (-> Int Real (Array Bool Bool)) respectively in these cases. |
73 |
|
* On the other hand, the above bvl is not a proper input for |
74 |
|
* atn = (Array Int (Array Bool Bool)) or (Array Int Int). |
75 |
|
* If the types of bvl and atn do not match, we throw an assertion failure. |
76 |
|
*/ |
77 |
|
static TypeNode getFunctionTypeForArrayType(TypeNode atn, Node bvl); |
78 |
|
/** Get array type for function type |
79 |
|
* |
80 |
|
* This returns the array type of terms returned by |
81 |
|
* getArrayRepresentationForLambda( t ), where t.getType()=ftn. |
82 |
|
*/ |
83 |
|
static TypeNode getArrayTypeForFunctionType(TypeNode ftn); |
84 |
|
/** |
85 |
|
* Given an array constant a, returns a lambda expression that it corresponds |
86 |
|
* to, with bound variable list bvl. |
87 |
|
* Examples: |
88 |
|
* |
89 |
|
* (store (storeall (Array Int Int) 2) 0 1) |
90 |
|
* becomes |
91 |
|
* ((lambda x. (ite (= x 0) 1 2)) |
92 |
|
* |
93 |
|
* (store (storeall (Array Int (Array Int Int)) (storeall (Array Int Int) 4)) |
94 |
|
* 0 (store (storeall (Array Int Int) 3) 1 2)) becomes (lambda xy. (ite (= x |
95 |
|
* 0) (ite (= x 1) 2 3) 4)) |
96 |
|
* |
97 |
|
* (store (store (storeall (Array Int Bool) false) 2 true) 1 true) |
98 |
|
* becomes |
99 |
|
* (lambda x. (ite (= x 1) true (ite (= x 2) true false))) |
100 |
|
* |
101 |
|
* Notice that the return body of the lambda is rewritten to ensure that the |
102 |
|
* representation is canonical. Hence the last |
103 |
|
* example will in fact be returned as: |
104 |
|
* (lambda x. (ite (= x 1) true (= x 2))) |
105 |
|
*/ |
106 |
|
static Node getLambdaForArrayRepresentation(TNode a, TNode bvl); |
107 |
|
/** |
108 |
|
* Given a lambda expression n, returns an array term that corresponds to n. |
109 |
|
* This does the opposite direction of the examples described above. |
110 |
|
* |
111 |
|
* We limit the return values of this method to be almost constant functions, |
112 |
|
* that is, arrays of the form: |
113 |
|
* (store ... (store (storeall _ b) i1 e1) ... in en) |
114 |
|
* where b, i1, e1, ..., in, en are constants. |
115 |
|
* Notice however that the return value of this form need not be a (canonical) |
116 |
|
* array constant. |
117 |
|
* |
118 |
|
* If it is not possible to construct an array of this form that corresponds |
119 |
|
* to n, this method returns null. |
120 |
|
*/ |
121 |
|
static Node getArrayRepresentationForLambda(TNode n); |
122 |
|
}; /* class TheoryBuiltinRewriter */ |
123 |
|
|
124 |
|
} // namespace builtin |
125 |
|
} // namespace theory |
126 |
|
} // namespace cvc5 |
127 |
|
|
128 |
|
#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ |