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 |
3796 |
void DatatypesProofRuleChecker::registerTo(ProofChecker* pc) |
27 |
|
{ |
28 |
3796 |
pc->registerChecker(PfRule::DT_UNIF, this); |
29 |
3796 |
pc->registerChecker(PfRule::DT_INST, this); |
30 |
3796 |
pc->registerChecker(PfRule::DT_COLLAPSE, this); |
31 |
3796 |
pc->registerChecker(PfRule::DT_SPLIT, this); |
32 |
3796 |
pc->registerChecker(PfRule::DT_CLASH, this); |
33 |
3796 |
} |
34 |
|
|
35 |
1987 |
Node DatatypesProofRuleChecker::checkInternal(PfRule id, |
36 |
|
const std::vector<Node>& children, |
37 |
|
const std::vector<Node>& args) |
38 |
|
{ |
39 |
1987 |
NodeManager* nm = NodeManager::currentNM(); |
40 |
1987 |
if (id == PfRule::DT_UNIF) |
41 |
|
{ |
42 |
75 |
Assert(children.size() == 1); |
43 |
75 |
Assert(args.size() == 1); |
44 |
|
uint32_t i; |
45 |
150 |
if (children[0].getKind() != kind::EQUAL |
46 |
150 |
|| children[0][0].getKind() != kind::APPLY_CONSTRUCTOR |
47 |
150 |
|| children[0][1].getKind() != kind::APPLY_CONSTRUCTOR |
48 |
150 |
|| children[0][0].getOperator() != children[0][1].getOperator() |
49 |
225 |
|| !getUInt32(args[0], i)) |
50 |
|
{ |
51 |
|
return Node::null(); |
52 |
|
} |
53 |
75 |
if (i >= children[0][0].getNumChildren()) |
54 |
|
{ |
55 |
|
return Node::null(); |
56 |
|
} |
57 |
75 |
Assert(children[0][0].getNumChildren() == children[0][1].getNumChildren()); |
58 |
75 |
return children[0][0][i].eqNode(children[0][1][i]); |
59 |
|
} |
60 |
1912 |
else if (id == PfRule::DT_INST) |
61 |
|
{ |
62 |
534 |
Assert(children.empty()); |
63 |
534 |
Assert(args.size() == 2); |
64 |
1068 |
Node t = args[0]; |
65 |
1068 |
TypeNode tn = t.getType(); |
66 |
|
uint32_t i; |
67 |
534 |
if (!tn.isDatatype() || !getUInt32(args[1], i)) |
68 |
|
{ |
69 |
|
return Node::null(); |
70 |
|
} |
71 |
534 |
const DType& dt = tn.getDType(); |
72 |
534 |
if (i >= dt.getNumConstructors()) |
73 |
|
{ |
74 |
|
return Node::null(); |
75 |
|
} |
76 |
1068 |
Node tester = utils::mkTester(t, i, dt); |
77 |
1068 |
Node ticons = Rewriter::rewrite(utils::getInstCons(t, dt, i)); |
78 |
534 |
return tester.eqNode(t.eqNode(ticons)); |
79 |
|
} |
80 |
1378 |
else if (id == PfRule::DT_COLLAPSE) |
81 |
|
{ |
82 |
119 |
Assert(children.empty()); |
83 |
119 |
Assert(args.size() == 1); |
84 |
238 |
Node t = args[0]; |
85 |
238 |
if (t.getKind() != kind::APPLY_SELECTOR_TOTAL |
86 |
238 |
|| t[0].getKind() != kind::APPLY_CONSTRUCTOR) |
87 |
|
{ |
88 |
|
return Node::null(); |
89 |
|
} |
90 |
238 |
Node selector = t.getOperator(); |
91 |
119 |
size_t constructorIndex = utils::indexOf(t[0].getOperator()); |
92 |
119 |
const DType& dt = utils::datatypeOf(selector); |
93 |
119 |
const DTypeConstructor& dtc = dt[constructorIndex]; |
94 |
119 |
int selectorIndex = dtc.getSelectorIndexInternal(selector); |
95 |
|
Node r = |
96 |
238 |
selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex]; |
97 |
119 |
return t.eqNode(r); |
98 |
|
} |
99 |
1259 |
else if (id == PfRule::DT_SPLIT) |
100 |
|
{ |
101 |
1259 |
Assert(children.empty()); |
102 |
1259 |
Assert(args.size() == 1); |
103 |
2518 |
TypeNode tn = args[0].getType(); |
104 |
1259 |
if (!tn.isDatatype()) |
105 |
|
{ |
106 |
|
return Node::null(); |
107 |
|
} |
108 |
1259 |
const DType& dt = tn.getDType(); |
109 |
1259 |
return utils::mkSplit(args[0], dt); |
110 |
|
} |
111 |
|
else if (id == PfRule::DT_CLASH) |
112 |
|
{ |
113 |
|
Assert(children.size() == 2); |
114 |
|
Assert(args.empty()); |
115 |
|
if (children[0].getKind() != kind::APPLY_TESTER |
116 |
|
|| children[1].getKind() != kind::APPLY_TESTER |
117 |
|
|| children[0][0] != children[1][0] || children[0] == children[1]) |
118 |
|
{ |
119 |
|
return Node::null(); |
120 |
|
} |
121 |
|
return nm->mkConst(false); |
122 |
|
} |
123 |
|
// no rule |
124 |
|
return Node::null(); |
125 |
|
} |
126 |
|
|
127 |
|
} // namespace datatypes |
128 |
|
} // namespace theory |
129 |
29577 |
} // namespace cvc5 |