1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz, Andres Noetzli |
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 ceg_dt_instantiator. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" |
17 |
|
|
18 |
|
#include "expr/dtype.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "expr/node_algorithm.h" |
21 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
22 |
|
|
23 |
|
using namespace std; |
24 |
|
using namespace cvc5::kind; |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace quantifiers { |
29 |
|
|
30 |
39 |
void DtInstantiator::reset(CegInstantiator* ci, |
31 |
|
SolvedForm& sf, |
32 |
|
Node pv, |
33 |
|
CegInstEffort effort) |
34 |
|
{ |
35 |
39 |
} |
36 |
|
|
37 |
39 |
bool DtInstantiator::hasProcessEqualTerm(CegInstantiator* ci, |
38 |
|
SolvedForm& sf, |
39 |
|
Node pv, |
40 |
|
CegInstEffort effort) |
41 |
|
{ |
42 |
39 |
return true; |
43 |
|
} |
44 |
|
|
45 |
30 |
bool DtInstantiator::processEqualTerms(CegInstantiator* ci, |
46 |
|
SolvedForm& sf, |
47 |
|
Node pv, |
48 |
|
std::vector<Node>& eqc, |
49 |
|
CegInstEffort effort) |
50 |
|
{ |
51 |
60 |
Trace("cegqi-dt-debug") << "try based on constructors in equivalence class." |
52 |
30 |
<< std::endl; |
53 |
|
// look in equivalence class for a constructor |
54 |
30 |
NodeManager* nm = NodeManager::currentNM(); |
55 |
60 |
for (unsigned k = 0, size = eqc.size(); k < size; k++) |
56 |
|
{ |
57 |
82 |
Node n = eqc[k]; |
58 |
52 |
if (n.getKind() == APPLY_CONSTRUCTOR) |
59 |
|
{ |
60 |
44 |
Trace("cegqi-dt-debug") |
61 |
22 |
<< "...try based on constructor term " << n << std::endl; |
62 |
22 |
std::vector<Node> children; |
63 |
22 |
children.push_back(n.getOperator()); |
64 |
22 |
const DType& dt = d_type.getDType(); |
65 |
22 |
unsigned cindex = datatypes::utils::indexOf(n.getOperator()); |
66 |
|
// now must solve for selectors applied to pv |
67 |
58 |
for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++) |
68 |
|
{ |
69 |
|
Node c = nm->mkNode(APPLY_SELECTOR_TOTAL, |
70 |
72 |
dt[cindex].getSelectorInternal(d_type, j), |
71 |
144 |
pv); |
72 |
36 |
ci->pushStackVariable(c); |
73 |
36 |
children.push_back(c); |
74 |
|
} |
75 |
22 |
Node val = nm->mkNode(kind::APPLY_CONSTRUCTOR, children); |
76 |
22 |
TermProperties pv_prop_dt; |
77 |
22 |
if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf)) |
78 |
|
{ |
79 |
22 |
return true; |
80 |
|
} |
81 |
|
// cleanup |
82 |
|
for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++) |
83 |
|
{ |
84 |
|
ci->popStackVariable(); |
85 |
|
} |
86 |
|
break; |
87 |
|
} |
88 |
|
} |
89 |
8 |
return false; |
90 |
|
} |
91 |
|
|
92 |
8 |
bool DtInstantiator::hasProcessEquality(CegInstantiator* ci, |
93 |
|
SolvedForm& sf, |
94 |
|
Node pv, |
95 |
|
CegInstEffort effort) |
96 |
|
{ |
97 |
8 |
return true; |
98 |
|
} |
99 |
|
|
100 |
11 |
bool DtInstantiator::processEquality(CegInstantiator* ci, |
101 |
|
SolvedForm& sf, |
102 |
|
Node pv, |
103 |
|
std::vector<TermProperties>& term_props, |
104 |
|
std::vector<Node>& terms, |
105 |
|
CegInstEffort effort) |
106 |
|
{ |
107 |
22 |
Node val = solve_dt(pv, terms[0], terms[1], terms[0], terms[1]); |
108 |
11 |
if (!val.isNull()) |
109 |
|
{ |
110 |
2 |
TermProperties pv_prop; |
111 |
2 |
if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) |
112 |
|
{ |
113 |
2 |
return true; |
114 |
|
} |
115 |
|
} |
116 |
9 |
return false; |
117 |
|
} |
118 |
|
|
119 |
33 |
Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb) |
120 |
|
{ |
121 |
66 |
Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b |
122 |
33 |
<< " " << sa << " " << sb << std::endl; |
123 |
66 |
Node ret; |
124 |
33 |
if (!a.isNull() && a == v) |
125 |
|
{ |
126 |
11 |
ret = sb; |
127 |
|
} |
128 |
22 |
else if (!b.isNull() && b == v) |
129 |
|
{ |
130 |
|
ret = sa; |
131 |
|
} |
132 |
22 |
else if (!a.isNull() && a.getKind() == APPLY_CONSTRUCTOR) |
133 |
|
{ |
134 |
12 |
if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR) |
135 |
|
{ |
136 |
10 |
if (a.getOperator() == b.getOperator()) |
137 |
|
{ |
138 |
30 |
for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++) |
139 |
|
{ |
140 |
40 |
Node s = solve_dt(v, a[i], b[i], sa[i], sb[i]); |
141 |
20 |
if (!s.isNull()) |
142 |
|
{ |
143 |
|
return s; |
144 |
|
} |
145 |
|
} |
146 |
|
} |
147 |
|
} |
148 |
|
else |
149 |
|
{ |
150 |
2 |
NodeManager* nm = NodeManager::currentNM(); |
151 |
2 |
unsigned cindex = DType::indexOf(a.getOperator()); |
152 |
2 |
TypeNode tn = a.getType(); |
153 |
2 |
const DType& dt = tn.getDType(); |
154 |
2 |
for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++) |
155 |
|
{ |
156 |
|
Node nn = nm->mkNode( |
157 |
2 |
APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), sb); |
158 |
2 |
Node s = solve_dt(v, a[i], Node::null(), sa[i], nn); |
159 |
2 |
if (!s.isNull()) |
160 |
|
{ |
161 |
2 |
return s; |
162 |
|
} |
163 |
|
} |
164 |
|
} |
165 |
|
} |
166 |
10 |
else if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR) |
167 |
|
{ |
168 |
|
// flip sides |
169 |
|
return solve_dt(v, b, a, sb, sa); |
170 |
|
} |
171 |
31 |
if (!ret.isNull()) |
172 |
|
{ |
173 |
|
// ensure does not contain v |
174 |
11 |
if (expr::hasSubterm(ret, v)) |
175 |
|
{ |
176 |
9 |
ret = Node::null(); |
177 |
|
} |
178 |
|
} |
179 |
31 |
return ret; |
180 |
|
} |
181 |
|
|
182 |
|
} // namespace quantifiers |
183 |
|
} // namespace theory |
184 |
29502 |
} // namespace cvc5 |