1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
/********************* */
/*! \file quant_rep_bound_ext.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Implementation of quantifiers representative bound utility
**/
#include "theory/quantifiers/quant_rep_bound_ext.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quant_bound_inference.h"
using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
namespace quantifiers {
QRepBoundExt::QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m)
: d_qbi(qbi), d_model(m)
{
}
RsiEnumType QRepBoundExt::setBound(Node owner,
unsigned i,
std::vector<Node>& elements)
{
// builtin: check if it is bound by bounded integer module
if (owner.getKind() == FORALL)
{
BoundVarType bvt = d_qbi.getBoundVarType(owner, owner[0][i]);
if (bvt != BOUND_FINITE)
{
d_bound_int[i] = true;
return ENUM_CUSTOM;
}
// indicates the variable is finitely bound due to
// the (small) cardinality of its type,
// will treat in default way
}
return ENUM_INVALID;
}
bool QRepBoundExt::resetIndex(RepSetIterator* rsi,
Node owner,
unsigned i,
bool initial,
std::vector<Node>& elements)
{
if (d_bound_int.find(i) == d_bound_int.end())
{
// not bound
return true;
}
Assert(owner.getKind() == FORALL);
if (!d_qbi.getBoundElements(rsi, initial, owner, owner[0][i], elements))
{
return false;
}
return true;
}
bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn)
{
return d_model->initializeRepresentativesForType(tn);
}
bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
{
// must set a variable index order based on bounded integers
if (owner.getKind() != FORALL)
{
return false;
}
Trace("bound-int-rsi") << "Calculating variable order..." << std::endl;
d_qbi.getBoundVarIndices(owner, varOrder);
return true;
}
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
|
