GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_bound_inference.cpp Lines: 50 50 100.0 %
Date: 2021-03-23 Branches: 83 146 56.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_bound_inference.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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 quantifiers bound inference
13
 **/
14
15
#include "theory/quantifiers/quant_bound_inference.h"
16
17
#include "theory/quantifiers/fmf/bounded_integers.h"
18
#include "theory/rewriter.h"
19
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace quantifiers {
25
26
8997
QuantifiersBoundInference::QuantifiersBoundInference(unsigned cardMax,
27
8997
                                                     bool isFmf)
28
8997
    : d_cardMax(cardMax), d_isFmf(isFmf), d_bint(nullptr)
29
{
30
8997
}
31
32
6054
void QuantifiersBoundInference::finishInit(BoundedIntegers* b) { d_bint = b; }
33
34
8213
bool QuantifiersBoundInference::mayComplete(TypeNode tn)
35
{
36
  std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
37
8213
      d_may_complete.find(tn);
38
8213
  if (it == d_may_complete.end())
39
  {
40
    // cache
41
407
    bool mc = mayComplete(tn, d_cardMax);
42
407
    d_may_complete[tn] = mc;
43
407
    return mc;
44
  }
45
7806
  return it->second;
46
}
47
48
407
bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
49
{
50
407
  bool mc = false;
51
407
  if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
52
  {
53
58
    Cardinality c = tn.getCardinality();
54
29
    if (!c.isLargeFinite())
55
    {
56
25
      NodeManager* nm = NodeManager::currentNM();
57
50
      Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
58
      // check if less than fixed upper bound
59
50
      Node oth = nm->mkConst(Rational(maxCard));
60
50
      Node eq = nm->mkNode(LEQ, card, oth);
61
25
      eq = Rewriter::rewrite(eq);
62
25
      mc = eq.isConst() && eq.getConst<bool>();
63
    }
64
  }
65
407
  return mc;
66
}
67
68
5551
bool QuantifiersBoundInference::isFiniteBound(Node q, Node v)
69
{
70
5551
  if (d_bint && d_bint->isBound(q, v))
71
  {
72
68
    return true;
73
  }
74
10966
  TypeNode tn = v.getType();
75
5483
  if (tn.isSort() && d_isFmf)
76
  {
77
1342
    return true;
78
  }
79
4141
  else if (mayComplete(tn))
80
  {
81
69
    return true;
82
  }
83
4072
  return false;
84
}
85
86
5845
BoundVarType QuantifiersBoundInference::getBoundVarType(Node q, Node v)
87
{
88
5845
  if (d_bint)
89
  {
90
4451
    return d_bint->getBoundVarType(q, v);
91
  }
92
1394
  return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
93
}
94
95
4381
void QuantifiersBoundInference::getBoundVarIndices(
96
    Node q, std::vector<unsigned>& indices) const
97
{
98
4381
  Assert(indices.empty());
99
  // we take the bounded variables first
100
4381
  if (d_bint)
101
  {
102
3373
    d_bint->getBoundVarIndices(q, indices);
103
  }
104
  // then get the remaining ones
105
10460
  for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
106
  {
107
6079
    if (std::find(indices.begin(), indices.end(), i) == indices.end())
108
    {
109
1642
      indices.push_back(i);
110
    }
111
  }
112
4381
}
113
114
2593
bool QuantifiersBoundInference::getBoundElements(
115
    RepSetIterator* rsi,
116
    bool initial,
117
    Node q,
118
    Node v,
119
    std::vector<Node>& elements) const
120
{
121
2593
  if (d_bint)
122
  {
123
2581
    return d_bint->getBoundElements(rsi, initial, q, v, elements);
124
  }
125
12
  return false;
126
}
127
128
}  // namespace quantifiers
129
}  // namespace theory
130
26685
}  // namespace CVC4