GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/theory_uf_rewriter.h Lines: 84 92 91.3 %
Date: 2021-03-23 Branches: 214 442 48.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_uf_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Dejan Jovanovic
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__UF__THEORY_UF_REWRITER_H
21
#define CVC4__THEORY__UF__THEORY_UF_REWRITER_H
22
23
#include "expr/node_algorithm.h"
24
#include "options/uf_options.h"
25
#include "theory/rewriter.h"
26
#include "theory/substitutions.h"
27
#include "theory/theory_rewriter.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace uf {
32
33
17991
class TheoryUfRewriter : public TheoryRewriter
34
{
35
 public:
36
810753
  RewriteResponse postRewrite(TNode node) override
37
  {
38
810753
    if(node.getKind() == kind::EQUAL) {
39
171430
      if(node[0] == node[1]) {
40
76
        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
41
171354
      } else if(node[0].isConst() && node[1].isConst()) {
42
        // uninterpreted constants are all distinct
43
26
        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
44
      }
45
171328
      if (node[0] > node[1]) {
46
63740
        Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
47
31870
        return RewriteResponse(REWRITE_DONE, newNode);
48
      }
49
    }
50
778781
    if(node.getKind() == kind::APPLY_UF) {
51
614543
      if( node.getOperator().getKind() == kind::LAMBDA ){
52
16736
        Trace("uf-ho-beta")
53
8368
          << "uf-ho-beta : beta-reducing all args of : " << node << "\n";
54
16736
        TNode lambda = node.getOperator();
55
16736
        Node ret;
56
        // build capture-avoiding substitution since in HOL shadowing may have
57
        // been introduced
58
8368
        if (options::ufHo())
59
        {
60
1186
          std::vector<Node> vars;
61
1186
          std::vector<Node> subs;
62
1631
          for (const Node& v : lambda[0])
63
          {
64
1038
            vars.push_back(v);
65
          }
66
1631
          for (const Node& s : node)
67
          {
68
1038
            subs.push_back(s);
69
          }
70
593
          if (Trace.isOn("uf-ho-beta"))
71
          {
72
            Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size()
73
                                << " vars into " << subs.size() << " terms :\n";
74
            for (unsigned i = 0, size = subs.size(); i < size; ++i)
75
            {
76
              Trace("uf-ho-beta") << "uf-ho-beta: .... " << vars[i] << " |-> "
77
                                  << subs[i] << "\n";
78
            }
79
          }
80
593
          ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs);
81
593
          Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n";
82
        }
83
        else
84
        {
85
15550
          std::vector<TNode> vars;
86
15550
          std::vector<TNode> subs;
87
21731
          for (const TNode& v : lambda[0])
88
          {
89
13956
            vars.push_back(v);
90
          }
91
21731
          for (const TNode& s : node)
92
          {
93
13956
            subs.push_back(s);
94
          }
95
7775
          ret = lambda[1].substitute(
96
              vars.begin(), vars.end(), subs.begin(), subs.end());
97
        }
98
8368
        return RewriteResponse(REWRITE_AGAIN_FULL, ret);
99
606175
      }else if( !canUseAsApplyUfOperator( node.getOperator() ) ){
100
113
        return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
101
      }
102
164238
    }else if( node.getKind() == kind::HO_APPLY ){
103
19968
      if( node[0].getKind() == kind::LAMBDA ){
104
        // resolve one argument of the lambda
105
728
        Trace("uf-ho-beta")
106
728
            << "uf-ho-beta : beta-reducing one argument of : " << node[0]
107
364
            << " with " << node[1] << "\n";
108
109
        // reconstruct the lambda first to avoid variable shadowing
110
728
        Node new_body = node[0][1];
111
364
        if( node[0][0].getNumChildren()>1 ){
112
586
          std::vector< Node > new_vars;
113
686
          for( unsigned i=1; i<node[0][0].getNumChildren(); i++ ){
114
393
            new_vars.push_back( node[0][0][i] );
115
          }
116
586
          std::vector< Node > largs;
117
293
          largs.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, new_vars ) );
118
293
          largs.push_back( new_body );
119
293
          new_body = NodeManager::currentNM()->mkNode( kind::LAMBDA, largs );
120
586
          Trace("uf-ho-beta")
121
293
            << "uf-ho-beta : ....new lambda : " << new_body << "\n";
122
        }
123
124
        // build capture-avoiding substitution since in HOL shadowing may have
125
        // been introduced
126
364
        if (options::ufHo())
127
        {
128
728
          Node arg = Rewriter::rewrite(node[1]);
129
728
          Node var = node[0][0][0];
130
364
          new_body = expr::substituteCaptureAvoiding(new_body, var, arg);
131
        }
132
        else
133
        {
134
          TNode arg = Rewriter::rewrite(node[1]);
135
          TNode var = node[0][0][0];
136
          new_body = new_body.substitute(var, arg);
137
        }
138
728
        Trace("uf-ho-beta")
139
364
            << "uf-ho-beta : ..new body : " << new_body << "\n";
140
364
        return RewriteResponse( REWRITE_AGAIN_FULL, new_body );
141
      }
142
    }
143
769936
    return RewriteResponse(REWRITE_DONE, node);
144
  }
145
146
424637
  RewriteResponse preRewrite(TNode node) override
147
  {
148
424637
    if(node.getKind() == kind::EQUAL) {
149
95933
      if(node[0] == node[1]) {
150
2671
        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
151
93262
      } else if(node[0].isConst() && node[1].isConst()) {
152
        // uninterpreted constants are all distinct
153
6259
        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
154
      }
155
    }
156
415707
    return RewriteResponse(REWRITE_DONE, node);
157
  }
158
159
public: //conversion between HO_APPLY AND APPLY_UF
160
  // converts an APPLY_UF to a curried HO_APPLY e.g. (f a b) becomes (@ (@ f a) b)
161
8966
  static Node getHoApplyForApplyUf(TNode n) {
162
8966
    Assert(n.getKind() == kind::APPLY_UF);
163
8966
    Node curr = n.getOperator();
164
23731
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
165
14765
      curr = NodeManager::currentNM()->mkNode( kind::HO_APPLY, curr, n[i] );
166
    }
167
8966
    return curr;
168
  }
169
  // converts a curried HO_APPLY into an APPLY_UF e.g. (@ (@ f a) b) becomes (f a b)
170
  static Node getApplyUfForHoApply(TNode n) {
171
    Assert(n.getType().getNumChildren() == 2);
172
    std::vector< TNode > children;
173
    TNode curr = decomposeHoApply( n, children, true );
174
    // if operator is standard
175
    if( canUseAsApplyUfOperator( curr ) ){
176
      return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
177
    }
178
    // cannot construct APPLY_UF if operator is partially applied or is not standard
179
    return Node::null();
180
  }
181
  /**
182
   * Given a curried HO_APPLY term n, this method adds its arguments into args
183
   * and returns its operator. If the argument opInArgs is true, then we add
184
   * its operator to args.
185
   */
186
296
  static Node decomposeHoApply(TNode n, std::vector<TNode>& args, bool opInArgs = false) {
187
592
    TNode curr = n;
188
1300
    while( curr.getKind() == kind::HO_APPLY ){
189
502
      args.push_back( curr[1] );
190
502
      curr = curr[0];
191
    }
192
296
    if( opInArgs ){
193
120
      args.push_back( curr );
194
    }
195
296
    std::reverse( args.begin(), args.end() );
196
592
    return curr;
197
  }
198
  /** returns true if this node can be used as an operator of an APPLY_UF node.  In higher-order logic,
199
   * terms can have function types and not just variables.
200
   * Currently, we want only free variables to be used as operators of APPLY_UF nodes. This is motivated by
201
   * E-matching, ite-lifting among other things.  For example:
202
   * f: Int -> Int, g : Int -> Int
203
   * forall x : ( Int -> Int ), y : Int. (x y) = (f 0)
204
   * 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.
205
   */
206
606415
  static inline bool canUseAsApplyUfOperator(TNode n){
207
606415
    return n.isVar();
208
  }
209
}; /* class TheoryUfRewriter */
210
211
}/* CVC4::theory::uf namespace */
212
}/* CVC4::theory namespace */
213
}/* CVC4 namespace */
214
215
#endif /* CVC4__THEORY__UF__THEORY_UF_REWRITER_H */