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 |
|
* Methods for counterexample-guided quantifier instantiation |
14 |
|
* based on nested quantifier elimination. |
15 |
|
*/ |
16 |
|
|
17 |
|
#include "theory/quantifiers/cegqi/nested_qe.h" |
18 |
|
|
19 |
|
#include "expr/node_algorithm.h" |
20 |
|
#include "expr/subs.h" |
21 |
|
#include "theory/smt_engine_subsolver.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace quantifiers { |
26 |
|
|
27 |
30 |
NestedQe::NestedQe(context::UserContext* u) : d_qnqe(u) {} |
28 |
|
|
29 |
58 |
bool NestedQe::process(Node q, std::vector<Node>& lems) |
30 |
|
{ |
31 |
58 |
NodeNodeMap::iterator it = d_qnqe.find(q); |
32 |
58 |
if (it != d_qnqe.end()) |
33 |
|
{ |
34 |
|
// already processed |
35 |
22 |
return (*it).second != q; |
36 |
|
} |
37 |
36 |
Trace("cegqi-nested-qe") << "Check nested QE on " << q << std::endl; |
38 |
72 |
Node qqe = doNestedQe(q, true); |
39 |
36 |
d_qnqe[q] = qqe; |
40 |
36 |
if (qqe == q) |
41 |
|
{ |
42 |
22 |
Trace("cegqi-nested-qe") << "...did not apply nested QE" << std::endl; |
43 |
22 |
return false; |
44 |
|
} |
45 |
14 |
Trace("cegqi-nested-qe") << "...applied nested QE" << std::endl; |
46 |
14 |
Trace("cegqi-nested-qe") << "Result is " << qqe << std::endl; |
47 |
|
|
48 |
|
// add as lemma |
49 |
14 |
lems.push_back(q.eqNode(qqe)); |
50 |
14 |
return true; |
51 |
|
} |
52 |
|
|
53 |
|
bool NestedQe::hasProcessed(Node q) const |
54 |
|
{ |
55 |
|
return d_qnqe.find(q) != d_qnqe.end(); |
56 |
|
} |
57 |
|
|
58 |
131 |
bool NestedQe::getNestedQuantification(Node q, std::unordered_set<Node>& nqs) |
59 |
|
{ |
60 |
131 |
expr::getKindSubterms(q[1], kind::FORALL, true, nqs); |
61 |
131 |
return !nqs.empty(); |
62 |
|
} |
63 |
|
|
64 |
46 |
bool NestedQe::hasNestedQuantification(Node q) |
65 |
|
{ |
66 |
92 |
std::unordered_set<Node> nqs; |
67 |
92 |
return getNestedQuantification(q, nqs); |
68 |
|
} |
69 |
|
|
70 |
85 |
Node NestedQe::doNestedQe(Node q, bool keepTopLevel) |
71 |
|
{ |
72 |
85 |
NodeManager* nm = NodeManager::currentNM(); |
73 |
170 |
Node qOrig = q; |
74 |
85 |
bool inputExists = false; |
75 |
85 |
if (q.getKind() == kind::EXISTS) |
76 |
|
{ |
77 |
23 |
q = nm->mkNode(kind::FORALL, q[0], q[1].negate()); |
78 |
23 |
inputExists = true; |
79 |
|
} |
80 |
85 |
Assert(q.getKind() == kind::FORALL); |
81 |
170 |
std::unordered_set<Node> nqs; |
82 |
85 |
if (!getNestedQuantification(q, nqs)) |
83 |
|
{ |
84 |
132 |
Trace("cegqi-nested-qe-debug") |
85 |
66 |
<< "...no nested quantification" << std::endl; |
86 |
66 |
if (keepTopLevel) |
87 |
|
{ |
88 |
51 |
return qOrig; |
89 |
|
} |
90 |
|
// just do ordinary quantifier elimination |
91 |
30 |
Node qqe = doQe(q); |
92 |
15 |
Trace("cegqi-nested-qe-debug") << "...did ordinary qe" << std::endl; |
93 |
15 |
return qqe; |
94 |
|
} |
95 |
38 |
Trace("cegqi-nested-qe-debug") |
96 |
19 |
<< "..." << nqs.size() << " nested quantifiers" << std::endl; |
97 |
|
// otherwise, skolemize the arguments of this and apply |
98 |
38 |
std::vector<Node> vars(q[0].begin(), q[0].end()); |
99 |
38 |
Subs sk; |
100 |
19 |
sk.add(vars); |
101 |
|
// do nested quantifier elimination on each nested quantifier, skolemizing the |
102 |
|
// free variables |
103 |
38 |
Subs snqe; |
104 |
38 |
for (const Node& nq : nqs) |
105 |
|
{ |
106 |
38 |
Node nqk = sk.apply(nq); |
107 |
38 |
Node nqqe = doNestedQe(nqk); |
108 |
19 |
if (nqqe == nqk) |
109 |
|
{ |
110 |
|
// failed |
111 |
|
Trace("cegqi-nested-qe-debug") |
112 |
|
<< "...failed to apply to nested" << std::endl; |
113 |
|
return q; |
114 |
|
} |
115 |
19 |
snqe.add(nqk, nqqe); |
116 |
|
} |
117 |
|
// get the result of nested quantifier elimination |
118 |
38 |
Node qeBody = sk.apply(q[1]); |
119 |
19 |
qeBody = snqe.apply(qeBody); |
120 |
|
// undo the skolemization |
121 |
19 |
qeBody = sk.rapply(qeBody, true); |
122 |
|
// reconstruct the body |
123 |
38 |
std::vector<Node> qargs; |
124 |
19 |
qargs.push_back(q[0]); |
125 |
19 |
qargs.push_back(inputExists ? qeBody.negate() : qeBody); |
126 |
19 |
if (q.getNumChildren() == 3) |
127 |
|
{ |
128 |
|
qargs.push_back(q[2]); |
129 |
|
} |
130 |
19 |
return nm->mkNode(inputExists ? kind::EXISTS : kind::FORALL, qargs); |
131 |
|
} |
132 |
|
|
133 |
15 |
Node NestedQe::doQe(Node q) |
134 |
|
{ |
135 |
15 |
Assert(q.getKind() == kind::FORALL); |
136 |
15 |
Trace("cegqi-nested-qe") << " Apply qe to " << q << std::endl; |
137 |
15 |
NodeManager* nm = NodeManager::currentNM(); |
138 |
15 |
q = nm->mkNode(kind::EXISTS, q[0], q[1].negate()); |
139 |
30 |
std::unique_ptr<SmtEngine> smt_qe; |
140 |
15 |
initializeSubsolver(smt_qe); |
141 |
30 |
Node qqe = smt_qe->getQuantifierElimination(q, true, false); |
142 |
15 |
if (expr::hasBoundVar(qqe)) |
143 |
|
{ |
144 |
|
Trace("cegqi-nested-qe") << " ...failed QE" << std::endl; |
145 |
|
//...failed to apply |
146 |
|
return q; |
147 |
|
} |
148 |
30 |
Node res = qqe.negate(); |
149 |
15 |
Trace("cegqi-nested-qe") << " ...success, result = " << res << std::endl; |
150 |
15 |
return res; |
151 |
|
} |
152 |
|
|
153 |
|
} // namespace quantifiers |
154 |
|
} // namespace theory |
155 |
28194 |
} // namespace cvc5 |