GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/quantifier_macros.cpp Lines: 289 337 85.8 %
Date: 2021-03-22 Branches: 595 1274 46.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifier_macros.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Yoni Zohar, Haniel Barbosa
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 Sort inference module
13
 **
14
 ** This class implements quantifiers macro definitions.
15
 **/
16
17
#include "preprocessing/passes/quantifier_macros.h"
18
19
#include <vector>
20
21
#include "options/quantifiers_options.h"
22
#include "options/smt_options.h"
23
#include "preprocessing/assertion_pipeline.h"
24
#include "preprocessing/preprocessing_pass_context.h"
25
#include "proof/proof_manager.h"
26
#include "smt/smt_engine.h"
27
#include "smt/smt_engine_scope.h"
28
#include "theory/arith/arith_msum.h"
29
#include "theory/quantifiers/ematching/pattern_term_selector.h"
30
#include "theory/quantifiers/quantifiers_registry.h"
31
#include "theory/quantifiers/term_database.h"
32
#include "theory/quantifiers/term_util.h"
33
#include "theory/quantifiers_engine.h"
34
#include "theory/rewriter.h"
35
#include "theory/theory_engine.h"
36
37
using namespace std;
38
using namespace CVC4::theory;
39
using namespace CVC4::theory::quantifiers;
40
using namespace CVC4::kind;
41
42
namespace CVC4 {
43
namespace preprocessing {
44
namespace passes {
45
46
8995
QuantifierMacros::QuantifierMacros(PreprocessingPassContext* preprocContext)
47
    : PreprocessingPass(preprocContext, "quantifier-macros"),
48
8995
      d_ground_macros(false)
49
{
50
8995
}
51
52
48
PreprocessingPassResult QuantifierMacros::applyInternal(
53
    AssertionPipeline* assertionsToPreprocess)
54
{
55
  bool success;
56
48
  do
57
  {
58
48
    success = simplify(assertionsToPreprocess, true);
59
  } while (success);
60
36
  finalizeDefinitions();
61
36
  clearMaps();
62
36
  return PreprocessingPassResult::NO_CONFLICT;
63
}
64
65
36
void QuantifierMacros::clearMaps()
66
{
67
36
  d_macro_basis.clear();
68
36
  d_macro_defs.clear();
69
36
  d_macro_defs_new.clear();
70
36
  d_macro_def_contains.clear();
71
36
  d_simplify_cache.clear();
72
36
  d_quant_macros.clear();
73
36
  d_ground_macros = false;
74
36
}
75
76
48
bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
77
{
78
48
  const std::vector<Node>& assertions = ap->ref();
79
  unsigned rmax =
80
108
      options::macrosQuantMode() == options::MacrosQuantMode::ALL ? 2 : 1;
81
84
  for( unsigned r=0; r<rmax; r++ ){
82
48
    d_ground_macros = (r==0);
83
48
    Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
84
    //first, collect macro definitions
85
84
    std::vector< Node > macro_assertions;
86
204
    for( int i=0; i<(int)assertions.size(); i++ ){
87
156
      Trace("macros-debug") << "  process assertion " << assertions[i] << std::endl;
88
156
      if( processAssertion( assertions[i] ) ){
89
36
        if (options::unsatCores() && !options::produceProofs()
90
24
            && std::find(macro_assertions.begin(),
91
                         macro_assertions.end(),
92
4
                         assertions[i])
93
24
                   == macro_assertions.end())
94
        {
95
2
          macro_assertions.push_back(assertions[i]);
96
        }
97
        //process this assertion again
98
16
        i--;
99
      }
100
    }
101
48
    Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl;
102
48
    if( doRewrite && !d_macro_defs_new.empty() ){
103
12
      bool retVal = false;
104
12
      Trace("macros") << "Do simplifications..." << std::endl;
105
      //now, rewrite based on macro definitions
106
47
      for( unsigned i=0; i<assertions.size(); i++ ){
107
70
        Node curr = simplify( assertions[i] );
108
35
        if( curr!=assertions[i] ){
109
16
          curr = Rewriter::rewrite( curr );
110
16
          Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl;
111
          // for now, it is dependent upon all assertions involving macros, this
112
          // is an over-approximation. a more fine-grained unsat core
113
          // computation would require caching dependencies for each subterm of
114
          // the formula, which is expensive.
115
16
          if (options::unsatCores() && !options::produceProofs())
116
          {
117
4
            ProofManager::currentPM()->addDependence(curr, assertions[i]);
118
8
            for (unsigned j = 0; j < macro_assertions.size(); j++)
119
            {
120
4
              if (macro_assertions[j] != assertions[i])
121
              {
122
4
                ProofManager::currentPM()->addDependence(curr,
123
2
                                                         macro_assertions[j]);
124
              }
125
            }
126
          }
127
16
          ap->replace(i, curr);
128
16
          retVal = true;
129
        }
130
      }
131
12
      d_macro_defs_new.clear();
132
12
      if( retVal ){
133
12
        return true;
134
      }
135
    }
136
  }
137
36
  if( Trace.isOn("macros-warn") ){
138
    for( unsigned i=0; i<assertions.size(); i++ ){
139
      debugMacroDefinition( assertions[i], assertions[i] );
140
    }
141
  }
142
36
  return false;
143
}
144
145
176
bool QuantifierMacros::processAssertion( Node n ) {
146
176
  if( n.getKind()==AND ){
147
24
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
148
20
      if( processAssertion( n[i] ) ){
149
8
        return true;
150
      }
151
    }
152
164
  }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){
153
36
    std::vector< Node > args;
154
54
    for( size_t j=0; j<n[0].getNumChildren(); j++ ){
155
28
      args.push_back( n[0][j] );
156
    }
157
36
    Node nproc = n[1];
158
26
    if( !d_macro_defs_new.empty() ){
159
4
      nproc = simplify( nproc );
160
4
      if( nproc!=n[1] ){
161
        nproc = Rewriter::rewrite( nproc );
162
      }
163
    }
164
    //look at the body of the quantifier for macro definition
165
26
    if( process( nproc, true, args, n ) ){
166
16
      d_quant_macros[n] = true;
167
16
      return true;
168
    }
169
  }
170
152
  return false;
171
}
172
173
72
bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){
174
72
  if( visited.find( n )==visited.end() ){
175
64
    visited[n] = true;
176
64
    if( n.getKind()==APPLY_UF ){
177
8
      Node nop = n.getOperator();
178
8
      if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end()  ){
179
8
        return true;
180
      }
181
      if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){
182
        opc.push_back( nop );
183
      }
184
56
    }else if( d_ground_macros && n.getKind()==FORALL ){
185
      return true;
186
    }
187
96
    for( size_t i=0; i<n.getNumChildren(); i++ ){
188
56
      if( containsBadOp( n[i], op, opc, visited ) ){
189
16
        return true;
190
      }
191
    }
192
  }
193
48
  return false;
194
}
195
196
18
bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
197
18
  return pol && n.getKind()==EQUAL;
198
}
199
200
6
bool QuantifierMacros::isGroundUfTerm(Node q, Node n)
201
{
202
6
  Node icn = d_preprocContext->getTheoryEngine()
203
                 ->getQuantifiersEngine()
204
6
                 ->getQuantifiersRegistry()
205
12
                 .substituteBoundVariablesToInstConstants(n, q);
206
6
  Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
207
12
  std::vector< Node > var;
208
6
  quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
209
6
  Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
210
12
  std::vector< Node > trigger_var;
211
6
  inst::PatternTermSelector::getTriggerVariables(icn, q, trigger_var);
212
6
  Trace("macros-debug2") << "Done." << std::endl;
213
  //only if all variables are also trigger variables
214
12
  return trigger_var.size()>=var.size();
215
}
216
217
26
bool QuantifierMacros::isBoundVarApplyUf( Node n ) {
218
26
  Assert(n.getKind() == APPLY_UF);
219
52
  TypeNode tno = n.getOperator().getType();
220
52
  std::map< Node, bool > vars;
221
  // allow if a vector of unique variables of the same type as UF arguments
222
52
  for( unsigned i=0; i<n.getNumChildren(); i++ ){
223
28
    if( n[i].getKind()!=BOUND_VARIABLE ){
224
      return false;
225
    }
226
28
    if( n[i].getType()!=tno[i] ){
227
2
      return false;
228
    }
229
26
    if( vars.find( n[i] )==vars.end() ){
230
26
      vars[n[i]] = true;
231
    }else{
232
      return false;
233
    }
234
  }
235
24
  return true;
236
}
237
238
42
void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){
239
42
  if( visited.find( n )==visited.end() ){
240
42
    visited[n] = true;
241
42
    if( n.getKind()==APPLY_UF ){
242
18
      if( isBoundVarApplyUf( n ) ){
243
16
        candidates.push_back( n );
244
      }
245
24
    }else if( n.getKind()==PLUS ){
246
6
      for( size_t i=0; i<n.getNumChildren(); i++ ){
247
4
        getMacroCandidates( n[i], candidates, visited );
248
      }
249
22
    }else if( n.getKind()==MULT ){
250
      //if the LHS is a constant
251
2
      if( n.getNumChildren()==2 && n[0].isConst() ){
252
2
        getMacroCandidates( n[1], candidates, visited );
253
      }
254
20
    }else if( n.getKind()==NOT ){
255
      getMacroCandidates( n[0], candidates, visited );
256
    }
257
  }
258
42
}
259
260
16
Node QuantifierMacros::solveInEquality( Node n, Node lit ){
261
16
  if( lit.getKind()==EQUAL ){
262
    //return the opposite side of the equality if defined that way
263
24
    for( int i=0; i<2; i++ ){
264
20
      if( lit[i]==n ){
265
28
        return lit[i==0 ? 1 : 0];
266
8
      }else if( lit[i].getKind()==NOT && lit[i][0]==n ){
267
        return lit[i==0 ? 1 : 0].negate();
268
      }
269
    }
270
4
    std::map<Node, Node> msum;
271
4
    if (ArithMSum::getMonomialSumLit(lit, msum))
272
    {
273
4
      Node veq_c;
274
4
      Node val;
275
4
      int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL);
276
4
      if (res != 0 && veq_c.isNull())
277
      {
278
4
        return val;
279
      }
280
    }
281
  }
282
  Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;
283
  return Node::null();
284
}
285
286
122
bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){
287
122
  if( visited.find( n )==visited.end() ){
288
106
    visited[n] = true;
289
106
    if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
290
28
      if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
291
18
        if( retOnly ){
292
          return true;
293
        }else{
294
18
          vars.push_back( n );
295
        }
296
      }
297
    }
298
196
    for( size_t i=0; i<n.getNumChildren(); i++ ){
299
90
      if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){
300
        return true;
301
      }
302
    }
303
  }
304
122
  return false;
305
}
306
307
8
bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
308
                                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){
309
8
  bool success = true;
310
18
  for( size_t a=0; a<v_quant.size(); a++ ){
311
10
    if( !solved[ v_quant[a] ].isNull() ){
312
10
      vars.push_back( v_quant[a] );
313
10
      subs.push_back( solved[ v_quant[a] ] );
314
    }else{
315
      if( reqComplete ){
316
        success = false;
317
        break;
318
      }
319
    }
320
  }
321
8
  return success;
322
}
323
324
26
bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
325
26
  Trace("macros-debug") << "  process " << n << std::endl;
326
26
  if( n.getKind()==NOT ){
327
    return process( n[0], !pol, args, f );
328
26
  }else if( n.getKind()==AND || n.getKind()==OR ){
329
    //bool favorPol = (n.getKind()==AND)==pol;
330
    //conditional?
331
26
  }else if( n.getKind()==ITE ){
332
    //can not do anything
333
26
  }else if( n.getKind()==APPLY_UF ){
334
    //predicate case
335
8
    if( isBoundVarApplyUf( n ) ){
336
8
      Node op = n.getOperator();
337
8
      if( d_macro_defs.find( op )==d_macro_defs.end() ){
338
16
        Node n_def = NodeManager::currentNM()->mkConst( pol );
339
16
        for( unsigned i=0; i<n.getNumChildren(); i++ ){
340
16
          std::stringstream ss;
341
8
          ss << "mda_" << op << "";
342
16
          Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" );
343
8
          d_macro_basis[op].push_back( v );
344
        }
345
        //contains no ops
346
16
        std::vector< Node > op_contains;
347
        //add the macro
348
8
        addMacro( op, n_def, op_contains );
349
8
        return true;
350
      }
351
    }
352
  }else{
353
    //literal case
354
18
    if( isMacroLiteral( n, pol ) ){
355
18
      Trace("macros-debug") << "Check macro literal : " << n << std::endl;
356
28
      std::map< Node, bool > visited;
357
28
      std::vector< Node > candidates;
358
54
      for( size_t i=0; i<n.getNumChildren(); i++ ){
359
36
        getMacroCandidates( n[i], candidates, visited );
360
      }
361
26
      for( size_t i=0; i<candidates.size(); i++ ){
362
24
        Node m = candidates[i];
363
24
        Node op = m.getOperator();
364
16
        Trace("macros-debug") << "Check macro candidate : " << m << std::endl;
365
16
        if( d_macro_defs.find( op )==d_macro_defs.end() ){
366
24
          std::vector< Node > fvs;
367
16
          visited.clear();
368
16
          getFreeVariables( m, args, fvs, false, visited );
369
          //get definition and condition
370
24
          Node n_def = solveInEquality( m, n ); //definition for the macro
371
16
          if( !n_def.isNull() ){
372
16
            Trace("macros-debug") << m << " is possible macro in " << f << std::endl;
373
16
            Trace("macros-debug") << "  corresponding definition is : " << n_def << std::endl;
374
16
            visited.clear();
375
            //definition must exist and not contain any free variables apart from fvs
376
16
            if( !getFreeVariables( n_def, args, fvs, true, visited ) ){
377
16
              Trace("macros-debug") << "...free variables are contained." << std::endl;
378
16
              visited.clear();
379
              //cannot contain a defined operator, opc is list of functions it contains
380
24
              std::vector< Node > opc;
381
16
              if( !containsBadOp( n_def, op, opc, visited ) ){
382
8
                Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl;
383
                //must be ground UF term if mode is GROUND_UF
384
16
                if (options::macrosQuantMode()
385
                        != options::MacrosQuantMode::GROUND_UF
386
16
                    || isGroundUfTerm(f, n_def))
387
                {
388
8
                  Trace("macros-debug") << "...respects ground-uf constraint." << std::endl;
389
                  //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
390
                  // x1 ... xn are distinct variables
391
8
                  if( d_macro_basis[op].empty() ){
392
18
                    for( size_t a=0; a<m.getNumChildren(); a++ ){
393
20
                      std::stringstream ss;
394
10
                      ss << "mda_" << op << "";
395
20
                      Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
396
10
                      d_macro_basis[op].push_back( v );
397
                    }
398
                  }
399
8
                  std::map< Node, Node > solved;
400
18
                  for( size_t a=0; a<m.getNumChildren(); a++ ){
401
10
                    solved[m[a]] = d_macro_basis[op][a];
402
                  }
403
8
                  std::vector< Node > vars;
404
8
                  std::vector< Node > subs;
405
8
                  if( getSubstitution( fvs, solved, vars, subs, true ) ){
406
8
                    n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
407
8
                    addMacro( op, n_def, opc );
408
8
                    return true;
409
                  }
410
                }
411
              }
412
            }
413
          }
414
        }
415
      }
416
    }
417
  }
418
10
  return false;
419
}
420
421
209
Node QuantifierMacros::simplify( Node n ){
422
209
  if( n.getNumChildren()==0 ){
423
92
    return n;
424
  }else{
425
117
    std::map< Node, Node >::iterator itn = d_simplify_cache.find( n );
426
117
    if( itn!=d_simplify_cache.end() ){
427
4
      return itn->second;
428
    }else{
429
226
      Node ret = n;
430
113
      Trace("macros-debug") << "  simplify " << n << std::endl;
431
226
      std::vector< Node > children;
432
113
      bool childChanged = false;
433
283
      for( size_t i=0; i<n.getNumChildren(); i++ ){
434
340
        Node nn = simplify( n[i] );
435
170
        children.push_back( nn );
436
170
        childChanged = childChanged || nn!=n[i];
437
      }
438
113
      bool retSet = false;
439
113
      if( n.getKind()==APPLY_UF ){
440
60
        Node op = n.getOperator();
441
30
        std::map< Node, Node >::iterator it = d_macro_defs.find( op );
442
30
        if( it!=d_macro_defs.end() && !it->second.isNull() ){
443
          //only apply if children are subtypes of arguments
444
24
          bool success = true;
445
          // FIXME : this can be eliminated when we have proper typing rules
446
48
          std::vector< Node > cond;
447
48
          TypeNode tno = op.getType();
448
50
          for( unsigned i=0; i<children.size(); i++ ){
449
52
            Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] );
450
26
            if( etc.isNull() ){
451
              // if this does fail, we are incomplete, since we are eliminating
452
              // quantified formula corresponding to op,
453
              //  and not ensuring it applies to n when its types are correct.
454
              success = false;
455
              break;
456
26
            }else if( !etc.isConst() ){
457
              cond.push_back( etc );
458
            }
459
26
            Assert(children[i].getType().isSubtypeOf(tno[i]));
460
          }
461
24
          if( success ){
462
            //do substitution if necessary
463
24
            ret = it->second;
464
24
            std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op );
465
24
            if( itb!=d_macro_basis.end() ){
466
24
              ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() );
467
            }
468
24
            if( !cond.empty() ){
469
              Node cc = cond.size()==1 ? cond[0] : NodeManager::currentNM()->mkNode( kind::AND, cond );
470
              ret = NodeManager::currentNM()->mkNode( kind::ITE, cc, ret, n );
471
            }
472
24
            retSet = true;
473
          }
474
        }
475
      }
476
113
      if( !retSet && childChanged ){
477
44
        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
478
          children.insert( children.begin(), n.getOperator() );
479
        }
480
44
        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
481
      }
482
113
      d_simplify_cache[n] = ret;
483
113
      return ret;
484
    }
485
  }
486
}
487
488
void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) {
489
  //for debugging, ensure that all previous definitions have been eliminated
490
  if( n.getKind()==APPLY_UF ){
491
    Node op = n.getOperator();
492
    if( d_macro_defs.find( op )!=d_macro_defs.end() ){
493
      if( d_macro_defs.find( oo )!=d_macro_defs.end() ){
494
        Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl;
495
      }else{
496
        Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl;
497
      }
498
      Trace("macros-warn") << "  contains defined function " << op << "!!!" << std::endl;
499
    }
500
  }
501
  for( unsigned i=0; i<n.getNumChildren(); i++ ){
502
    debugMacroDefinition( oo, n[i] );
503
  }
504
}
505
506
36
void QuantifierMacros::finalizeDefinitions() {
507
36
  bool doDefs = false;
508
36
  if( Trace.isOn("macros-warn") ){
509
    doDefs = true;
510
  }
511
36
  if( options::incrementalSolving() || options::produceModels() || doDefs ){
512
30
    Trace("macros") << "Store as defined functions..." << std::endl;
513
    //also store as defined functions
514
30
    SmtEngine* smt = d_preprocContext->getSmt();
515
37
    for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
516
7
      Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl;
517
7
      Trace("macros-def") << "  basis is : ";
518
14
      std::vector< Node > nargs;
519
14
      std::vector<Node> args;
520
15
      for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){
521
16
        Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() );
522
8
        Trace("macros-def") << d_macro_basis[it->first][i] << " ";
523
8
        nargs.push_back( bv );
524
8
        args.push_back(bv);
525
      }
526
7
      Trace("macros-def") << std::endl;
527
14
      Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() );
528
7
      smt->defineFunction(it->first, args, sbody);
529
530
7
      if( Trace.isOn("macros-warn") ){
531
        debugMacroDefinition( it->first, sbody );
532
      }
533
    }
534
30
    Trace("macros") << "done." << std::endl;
535
  }
536
36
}
537
538
16
void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
539
16
  Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl;
540
16
  d_simplify_cache.clear();
541
16
  d_macro_defs[op] = n;
542
16
  d_macro_defs_new[op] = n;
543
  //substitute into all previous
544
32
  std::vector< Node > dep_ops;
545
16
  dep_ops.push_back( op );
546
16
  Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl;
547
16
  for( unsigned i=0; i<d_macro_def_contains[op].size(); i++ ){
548
    Node cop = d_macro_def_contains[op][i];
549
    Node def = d_macro_defs[cop];
550
    def = simplify( def );
551
    d_macro_defs[cop] = def;
552
    if( d_macro_defs_new.find( cop )!=d_macro_defs_new.end() ){
553
      d_macro_defs_new[cop] = def;
554
    }
555
    dep_ops.push_back( cop );
556
  }
557
  //store the contains op information
558
16
  for( unsigned i=0; i<opc.size(); i++ ){
559
    for( unsigned j=0; j<dep_ops.size(); j++ ){
560
      Node dop = dep_ops[j];
561
      if( std::find( d_macro_def_contains[opc[i]].begin(), d_macro_def_contains[opc[i]].end(), dop )==d_macro_def_contains[opc[i]].end() ){
562
        d_macro_def_contains[opc[i]].push_back( dop );
563
      }
564
    }
565
  }
566
16
}
567
568
569
}  // passes
570
}  // preprocessing
571
26736
}  // CVC4