GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_relevance.cpp Lines: 19 20 95.0 %
Date: 2021-03-23 Branches: 21 36 58.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_relevance.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters
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 Implementation of quantifier relevance
13
 **/
14
15
#include "theory/quantifiers/quant_relevance.h"
16
17
using namespace std;
18
using namespace CVC4::kind;
19
using namespace CVC4::context;
20
21
namespace CVC4 {
22
namespace theory {
23
namespace quantifiers {
24
25
344
void QuantRelevance::registerQuantifier(Node f)
26
{
27
  // compute symbols in f
28
688
  std::vector<Node> syms;
29
344
  computeSymbols(f[1], syms);
30
344
  d_syms[f].insert(d_syms[f].begin(), syms.begin(), syms.end());
31
344
}
32
33
/** compute symbols */
34
49809
void QuantRelevance::computeSymbols(Node n, std::vector<Node>& syms)
35
{
36
49809
  if (n.getKind() == APPLY_UF)
37
  {
38
54554
    Node op = n.getOperator();
39
27277
    if (std::find(syms.begin(), syms.end(), op) == syms.end())
40
    {
41
1581
      syms.push_back(op);
42
    }
43
  }
44
49809
  if (n.getKind() != FORALL)
45
  {
46
99211
    for (int i = 0; i < (int)n.getNumChildren(); i++)
47
    {
48
49465
      computeSymbols(n[i], syms);
49
    }
50
  }
51
49809
}
52
53
1452
size_t QuantRelevance::getNumQuantifiersForSymbol(Node s) const
54
{
55
1452
  std::map<Node, std::vector<Node> >::const_iterator it = d_syms_quants.find(s);
56
1452
  if (it == d_syms_quants.end())
57
  {
58
1452
    return 0;
59
  }
60
  return it->second.size();
61
}
62
63
} /* CVC4::theory::quantifiers namespace */
64
} /* CVC4::theory namespace */
65
26685
} /* CVC4 namespace */