GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_rep_bound_ext.cpp Lines: 25 26 96.2 %
Date: 2021-03-23 Branches: 25 58 43.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_rep_bound_ext.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 quantifiers representative bound utility
13
 **/
14
15
#include "theory/quantifiers/quant_rep_bound_ext.h"
16
17
#include "theory/quantifiers/first_order_model.h"
18
#include "theory/quantifiers/quant_bound_inference.h"
19
#include "theory/quantifiers_engine.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
27
4381
QRepBoundExt::QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m)
28
4381
    : d_qbi(qbi), d_model(m)
29
{
30
4381
}
31
32
5845
RsiEnumType QRepBoundExt::setBound(Node owner,
33
                                   unsigned i,
34
                                   std::vector<Node>& elements)
35
{
36
  // builtin: check if it is bound by bounded integer module
37
5845
  if (owner.getKind() == FORALL)
38
  {
39
5845
    BoundVarType bvt = d_qbi.getBoundVarType(owner, owner[0][i]);
40
5845
    if (bvt != BOUND_FINITE)
41
    {
42
1845
      d_bound_int[i] = true;
43
1845
      return ENUM_CUSTOM;
44
    }
45
    // indicates the variable is finitely bound due to
46
    // the (small) cardinality of its type,
47
    // will treat in default way
48
  }
49
4000
  return ENUM_INVALID;
50
}
51
52
13023
bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
53
                              Node owner,
54
                              unsigned i,
55
                              bool initial,
56
                              std::vector<Node>& elements)
57
{
58
13023
  if (d_bound_int.find(i) == d_bound_int.end())
59
  {
60
    // not bound
61
10430
    return true;
62
  }
63
2593
  Assert(owner.getKind() == FORALL);
64
2593
  if (!d_qbi.getBoundElements(rsi, initial, owner, owner[0][i], elements))
65
  {
66
68
    return false;
67
  }
68
2525
  return true;
69
}
70
71
6079
bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn)
72
{
73
6079
  return d_model->initializeRepresentativesForType(tn);
74
}
75
76
4381
bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
77
{
78
  // must set a variable index order based on bounded integers
79
4381
  if (owner.getKind() != FORALL)
80
  {
81
    return false;
82
  }
83
4381
  Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
84
4381
  d_qbi.getBoundVarIndices(owner, varOrder);
85
4381
  return true;
86
}
87
88
}  // namespace quantifiers
89
}  // namespace theory
90
26685
}  // namespace CVC4