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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
/********************* */
/*! \file theory_uf_rewriter.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
#define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
#include "theory/rewriter.h"
#include "theory/substitutions.h"
namespace CVC4 {
namespace theory {
namespace uf {
class TheoryUfRewriter {
public:
static RewriteResponse postRewrite(TNode node) {
if(node.getKind() == kind::EQUAL) {
if(node[0] == node[1]) {
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
} else if(node[0].isConst() && node[1].isConst()) {
// uninterpreted constants are all distinct
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
}
if (node[0] > node[1]) {
Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
return RewriteResponse(REWRITE_DONE, newNode);
}
}
if(node.getKind() == kind::APPLY_UF) {
if( node.getOperator().getKind() == kind::LAMBDA ){
TNode lambda = node.getOperator();
std::vector<TNode> vars;
std::vector<TNode> subs;
for (const TNode& v : lambda[0])
{
vars.push_back(v);
}
for (const TNode& s : node)
{
subs.push_back(s);
}
Node ret = lambda[1].substitute(
vars.begin(), vars.end(), subs.begin(), subs.end());
return RewriteResponse(REWRITE_AGAIN_FULL, ret);
}else if( !canUseAsApplyUfOperator( node.getOperator() ) ){
return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
}
}else if( node.getKind() == kind::HO_APPLY ){
if( node[0].getKind() == kind::LAMBDA ){
// resolve one argument of the lambda
TNode arg = Rewriter::rewrite( node[1] );
TNode var = node[0][0][0];
Node new_body = node[0][1].substitute( var, arg );
if( node[0][0].getNumChildren()>1 ){
std::vector< Node > new_vars;
for( unsigned i=1; i<node[0][0].getNumChildren(); i++ ){
new_vars.push_back( node[0][0][i] );
}
std::vector< Node > largs;
largs.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, new_vars ) );
largs.push_back( new_body );
new_body = NodeManager::currentNM()->mkNode( kind::LAMBDA, largs );
}
return RewriteResponse( REWRITE_AGAIN_FULL, new_body );
}
}
return RewriteResponse(REWRITE_DONE, node);
}
static RewriteResponse preRewrite(TNode node) {
if(node.getKind() == kind::EQUAL) {
if(node[0] == node[1]) {
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
} else if(node[0].isConst() && node[1].isConst()) {
// uninterpreted constants are all distinct
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
}
}
return RewriteResponse(REWRITE_DONE, node);
}
static inline void init() {}
static inline void shutdown() {}
public: //conversion between HO_APPLY AND APPLY_UF
// converts an APPLY_UF to a curried HO_APPLY e.g. (f a b) becomes (@ (@ f a) b)
static Node getHoApplyForApplyUf(TNode n) {
Assert( n.getKind()==kind::APPLY_UF );
Node curr = n.getOperator();
for( unsigned i=0; i<n.getNumChildren(); i++ ){
curr = NodeManager::currentNM()->mkNode( kind::HO_APPLY, curr, n[i] );
}
return curr;
}
// converts a curried HO_APPLY into an APPLY_UF e.g. (@ (@ f a) b) becomes (f a b)
static Node getApplyUfForHoApply(TNode n) {
Assert( n.getType().getNumChildren()==2 );
std::vector< TNode > children;
TNode curr = decomposeHoApply( n, children, true );
// if operator is standard
if( canUseAsApplyUfOperator( curr ) ){
return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
}
// cannot construct APPLY_UF if operator is partially applied or is not standard
return Node::null();
}
/**
* Given a curried HO_APPLY term n, this method adds its arguments into args
* and returns its operator. If the argument opInArgs is true, then we add
* its operator to args.
*/
static Node decomposeHoApply(TNode n, std::vector<TNode>& args, bool opInArgs = false) {
TNode curr = n;
while( curr.getKind() == kind::HO_APPLY ){
args.push_back( curr[1] );
curr = curr[0];
}
if( opInArgs ){
args.push_back( curr );
}
std::reverse( args.begin(), args.end() );
return curr;
}
/** returns true if this node can be used as an operator of an APPLY_UF node. In higher-order logic,
* terms can have function types and not just variables.
* Currently, we want only free variables to be used as operators of APPLY_UF nodes. This is motivated by
* E-matching, ite-lifting among other things. For example:
* f: Int -> Int, g : Int -> Int
* forall x : ( Int -> Int ), y : Int. (x y) = (f 0)
* Then, f and g can be used as APPLY_UF operators, but (ite C f g), (lambda x1. (f x1)) as well as the variable x above are not.
*/
static inline bool canUseAsApplyUfOperator(TNode n){
return n.isVar();
}
};/* class TheoryUfRewriter */
}/* CVC4::theory::uf namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__UF__THEORY_UF_REWRITER_H */
|
