1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 datatypes proof checker. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/datatypes/proof_checker.h" |
17 |
|
|
18 |
|
#include "expr/dtype_cons.h" |
19 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
20 |
|
#include "theory/rewriter.h" |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace theory { |
24 |
|
namespace datatypes { |
25 |
|
|
26 |
3769 |
void DatatypesProofRuleChecker::registerTo(ProofChecker* pc) |
27 |
|
{ |
28 |
3769 |
pc->registerChecker(PfRule::DT_UNIF, this); |
29 |
3769 |
pc->registerChecker(PfRule::DT_INST, this); |
30 |
3769 |
pc->registerChecker(PfRule::DT_COLLAPSE, this); |
31 |
3769 |
pc->registerChecker(PfRule::DT_SPLIT, this); |
32 |
3769 |
pc->registerChecker(PfRule::DT_CLASH, this); |
33 |
|
// trusted rules |
34 |
3769 |
pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2); |
35 |
3769 |
} |
36 |
|
|
37 |
7102 |
Node DatatypesProofRuleChecker::checkInternal(PfRule id, |
38 |
|
const std::vector<Node>& children, |
39 |
|
const std::vector<Node>& args) |
40 |
|
{ |
41 |
7102 |
NodeManager* nm = NodeManager::currentNM(); |
42 |
7102 |
if (id == PfRule::DT_UNIF) |
43 |
|
{ |
44 |
780 |
Assert(children.size() == 1); |
45 |
780 |
Assert(args.size() == 1); |
46 |
|
uint32_t i; |
47 |
1560 |
if (children[0].getKind() != kind::EQUAL |
48 |
1560 |
|| children[0][0].getKind() != kind::APPLY_CONSTRUCTOR |
49 |
1560 |
|| children[0][1].getKind() != kind::APPLY_CONSTRUCTOR |
50 |
1560 |
|| children[0][0].getOperator() != children[0][1].getOperator() |
51 |
2340 |
|| !getUInt32(args[0], i)) |
52 |
|
{ |
53 |
|
return Node::null(); |
54 |
|
} |
55 |
780 |
if (i >= children[0][0].getNumChildren()) |
56 |
|
{ |
57 |
|
return Node::null(); |
58 |
|
} |
59 |
780 |
Assert(children[0][0].getNumChildren() == children[0][1].getNumChildren()); |
60 |
780 |
return children[0][0][i].eqNode(children[0][1][i]); |
61 |
|
} |
62 |
6322 |
else if (id == PfRule::DT_INST) |
63 |
|
{ |
64 |
2673 |
Assert(children.empty()); |
65 |
2673 |
Assert(args.size() == 2); |
66 |
5346 |
Node t = args[0]; |
67 |
5346 |
TypeNode tn = t.getType(); |
68 |
|
uint32_t i; |
69 |
2673 |
if (!tn.isDatatype() || !getUInt32(args[1], i)) |
70 |
|
{ |
71 |
|
return Node::null(); |
72 |
|
} |
73 |
2673 |
const DType& dt = tn.getDType(); |
74 |
2673 |
if (i >= dt.getNumConstructors()) |
75 |
|
{ |
76 |
|
return Node::null(); |
77 |
|
} |
78 |
5346 |
Node tester = utils::mkTester(t, i, dt); |
79 |
5346 |
Node ticons = Rewriter::rewrite(utils::getInstCons(t, dt, i)); |
80 |
2673 |
return tester.eqNode(t.eqNode(ticons)); |
81 |
|
} |
82 |
3649 |
else if (id == PfRule::DT_COLLAPSE) |
83 |
|
{ |
84 |
1202 |
Assert(children.empty()); |
85 |
1202 |
Assert(args.size() == 1); |
86 |
2404 |
Node t = args[0]; |
87 |
2404 |
if (t.getKind() != kind::APPLY_SELECTOR_TOTAL |
88 |
2404 |
|| t[0].getKind() != kind::APPLY_CONSTRUCTOR) |
89 |
|
{ |
90 |
|
return Node::null(); |
91 |
|
} |
92 |
2404 |
Node selector = t.getOperator(); |
93 |
1202 |
size_t constructorIndex = utils::indexOf(t[0].getOperator()); |
94 |
1202 |
const DType& dt = utils::datatypeOf(selector); |
95 |
1202 |
const DTypeConstructor& dtc = dt[constructorIndex]; |
96 |
1202 |
int selectorIndex = dtc.getSelectorIndexInternal(selector); |
97 |
|
Node r = |
98 |
2404 |
selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex]; |
99 |
1202 |
return t.eqNode(r); |
100 |
|
} |
101 |
2447 |
else if (id == PfRule::DT_SPLIT) |
102 |
|
{ |
103 |
2018 |
Assert(children.empty()); |
104 |
2018 |
Assert(args.size() == 1); |
105 |
4036 |
TypeNode tn = args[0].getType(); |
106 |
2018 |
if (!tn.isDatatype()) |
107 |
|
{ |
108 |
|
return Node::null(); |
109 |
|
} |
110 |
2018 |
const DType& dt = tn.getDType(); |
111 |
2018 |
return utils::mkSplit(args[0], dt); |
112 |
|
} |
113 |
429 |
else if (id == PfRule::DT_CLASH) |
114 |
|
{ |
115 |
|
Assert(children.size() == 2); |
116 |
|
Assert(args.empty()); |
117 |
|
if (children[0].getKind() != kind::APPLY_TESTER |
118 |
|
|| children[1].getKind() != kind::APPLY_TESTER |
119 |
|
|| children[0][0] != children[1][0] || children[0] == children[1]) |
120 |
|
{ |
121 |
|
return Node::null(); |
122 |
|
} |
123 |
|
return nm->mkConst(false); |
124 |
|
} |
125 |
429 |
else if (id == PfRule::DT_TRUST) |
126 |
|
{ |
127 |
429 |
Assert(!args.empty()); |
128 |
429 |
Assert(args[0].getType().isBoolean()); |
129 |
429 |
return args[0]; |
130 |
|
} |
131 |
|
// no rule |
132 |
|
return Node::null(); |
133 |
|
} |
134 |
|
|
135 |
|
} // namespace datatypes |
136 |
|
} // namespace theory |
137 |
29349 |
} // namespace cvc5 |