1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of quantifiers representative bound utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/quant_rep_bound_ext.h" |
17 |
|
|
18 |
|
#include "theory/quantifiers/first_order_model.h" |
19 |
|
#include "theory/quantifiers/quant_bound_inference.h" |
20 |
|
|
21 |
|
using namespace cvc5::kind; |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace quantifiers { |
26 |
|
|
27 |
5439 |
QRepBoundExt::QRepBoundExt(QuantifiersBoundInference& qbi, FirstOrderModel* m) |
28 |
5439 |
: d_qbi(qbi), d_model(m) |
29 |
|
{ |
30 |
5439 |
} |
31 |
|
|
32 |
5734 |
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 |
5734 |
if (owner.getKind() == FORALL) |
38 |
|
{ |
39 |
5734 |
BoundVarType bvt = d_qbi.getBoundVarType(owner, owner[0][i]); |
40 |
5734 |
if (bvt != BOUND_FINITE) |
41 |
|
{ |
42 |
2144 |
d_bound_int[i] = true; |
43 |
2144 |
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 |
3590 |
return ENUM_INVALID; |
50 |
|
} |
51 |
|
|
52 |
14585 |
bool QRepBoundExt::resetIndex(RepSetIterator* rsi, |
53 |
|
Node owner, |
54 |
|
unsigned i, |
55 |
|
bool initial, |
56 |
|
std::vector<Node>& elements) |
57 |
|
{ |
58 |
14585 |
if (d_bound_int.find(i) == d_bound_int.end()) |
59 |
|
{ |
60 |
|
// not bound |
61 |
11734 |
return true; |
62 |
|
} |
63 |
2851 |
Assert(owner.getKind() == FORALL); |
64 |
2851 |
if (!d_qbi.getBoundElements(rsi, initial, owner, owner[0][i], elements)) |
65 |
|
{ |
66 |
103 |
return false; |
67 |
|
} |
68 |
2748 |
return true; |
69 |
|
} |
70 |
|
|
71 |
7490 |
bool QRepBoundExt::initializeRepresentativesForType(TypeNode tn) |
72 |
|
{ |
73 |
7490 |
return d_model->initializeRepresentativesForType(tn); |
74 |
|
} |
75 |
|
|
76 |
5439 |
bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder) |
77 |
|
{ |
78 |
|
// must set a variable index order based on bounded integers |
79 |
5439 |
if (owner.getKind() != FORALL) |
80 |
|
{ |
81 |
|
return false; |
82 |
|
} |
83 |
5439 |
Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; |
84 |
5439 |
d_qbi.getBoundVarIndices(owner, varOrder); |
85 |
5439 |
return true; |
86 |
|
} |
87 |
|
|
88 |
|
} // namespace quantifiers |
89 |
|
} // namespace theory |
90 |
29577 |
} // namespace cvc5 |