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