Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Preprocessor for the theory of quantifiers.
14 : : */
15 : :
16 : : #include "theory/quantifiers/quantifiers_preprocess.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "options/quantifiers_options.h"
20 : : #include "theory/quantifiers/quant_util.h"
21 : : #include "theory/quantifiers/skolemize.h"
22 : :
23 : : using namespace cvc5::internal::kind;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace quantifiers {
28 : :
29 : 81768 : QuantifiersPreprocess::QuantifiersPreprocess(Env& env)
30 : 81768 : : EnvObj(env), d_qrew(nodeManager(), env.getRewriter(), options())
31 : : {
32 : 81768 : }
33 : :
34 : 9 : Node QuantifiersPreprocess::computePrenexAgg(
35 : : Node n, std::map<Node, Node>& visited) const
36 : : {
37 : 9 : std::map<Node, Node>::iterator itv = visited.find(n);
38 [ - + ]: 9 : if (itv != visited.end())
39 : : {
40 : 0 : return itv->second;
41 : : }
42 [ + + ]: 9 : if (!expr::hasClosure(n))
43 : : {
44 : : // trivial
45 : 4 : return n;
46 : : }
47 : 5 : NodeManager* nm = nodeManager();
48 : 10 : Node ret = n;
49 [ + + ]: 5 : if (n.getKind() == Kind::NOT)
50 : : {
51 : 1 : ret = computePrenexAgg(n[0], visited).negate();
52 : : }
53 [ + + ]: 4 : else if (n.getKind() == Kind::FORALL)
54 : : {
55 : 6 : std::vector<Node> children;
56 : 3 : children.push_back(computePrenexAgg(n[1], visited));
57 : 6 : std::vector<Node> args;
58 : 3 : args.insert(args.end(), n[0].begin(), n[0].end());
59 : : // only combine if standard
60 [ + + ]: 3 : if (d_qrew.isStandard(n, options()))
61 : : {
62 : : // for each child, strip top level quant
63 [ + + ]: 4 : for (unsigned i = 0; i < children.size(); i++)
64 : : {
65 [ - + ]: 2 : if (children[i].getKind() == Kind::FORALL)
66 : : {
67 : 0 : args.insert(args.end(), children[i][0].begin(), children[i][0].end());
68 : 0 : children[i] = children[i][1];
69 : : }
70 : : }
71 : : }
72 : : // keep the pattern
73 : 6 : std::vector<Node> iplc;
74 [ + - ]: 3 : if (n.getNumChildren() == 3)
75 : : {
76 : 3 : iplc.insert(iplc.end(), n[2].begin(), n[2].end());
77 : : }
78 : 3 : Node nb = nm->mkOr(children);
79 : 3 : ret = d_qrew.mkForall(args, nb, iplc, true);
80 : : }
81 : : else
82 : : {
83 : 2 : Node q;
84 : 2 : std::vector<Node> args, nargs;
85 : 3 : Node nn = d_qrew.computePrenex(q, n, args, nargs, true, true);
86 : 2 : std::unordered_set<Node> argsSet(args.begin(), args.end());
87 : 2 : std::unordered_set<Node> nargsSet(args.begin(), args.end());
88 [ - + ][ - - ]: 1 : Assert(n != nn || argsSet.empty());
[ - + ][ - - ]
89 [ - + ][ - - ]: 1 : Assert(n != nn || nargsSet.empty());
[ - + ][ - - ]
90 [ + - ]: 1 : if (n != nn)
91 : : {
92 : 2 : Node nnn = computePrenexAgg(nn, visited);
93 : : // merge prenex
94 [ - + ]: 1 : if (nnn.getKind() == Kind::FORALL)
95 : : {
96 : 0 : argsSet.insert(nnn[0].begin(), nnn[0].end());
97 : 0 : nnn = nnn[1];
98 : : // pos polarity variables are inner
99 [ - - ]: 0 : if (!argsSet.empty())
100 : : {
101 : 0 : nnn = d_qrew.mkForall({argsSet.begin(), argsSet.end()}, nnn, true);
102 : : }
103 : 0 : argsSet.clear();
104 : : }
105 [ - + ][ - - ]: 1 : else if (nnn.getKind() == Kind::NOT && nnn[0].getKind() == Kind::FORALL)
[ - + ][ - + ]
[ - - ]
106 : : {
107 : 0 : nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end());
108 : 0 : nnn = nnn[0][1].negate();
109 : : }
110 [ + - ]: 1 : if (!nargsSet.empty())
111 : : {
112 : : nnn = d_qrew
113 : 2 : .mkForall(
114 : 2 : {nargsSet.begin(), nargsSet.end()}, nnn.negate(), true)
115 : 1 : .negate();
116 : : }
117 [ + - ]: 1 : if (!argsSet.empty())
118 : : {
119 : 1 : nnn = d_qrew.mkForall({argsSet.begin(), argsSet.end()}, nnn, true);
120 : : }
121 : 1 : ret = nnn;
122 : : }
123 : : }
124 : 5 : visited[n] = ret;
125 : 5 : return ret;
126 : : }
127 : :
128 : 683 : Node QuantifiersPreprocess::preSkolemizeQuantifiers(
129 : : Node n,
130 : : bool polarity,
131 : : std::vector<TNode>& fvs,
132 : : std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>&
133 : : visited) const
134 : : {
135 [ - + ][ - + ]: 683 : Assert(options().quantifiers.preSkolemQuant
[ - - ]
136 : : != options::PreSkolemQuantMode::OFF);
137 : 1366 : std::pair<Node, bool> key(n, polarity);
138 : : std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>::
139 : 683 : iterator it = visited.find(key);
140 [ - + ]: 683 : if (it != visited.end())
141 : : {
142 : 0 : return it->second;
143 : : }
144 : 683 : NodeManager* nm = nodeManager();
145 [ + - ]: 1366 : Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size()
146 : 683 : << std::endl;
147 [ + + ]: 683 : if (n.getKind() == Kind::FORALL)
148 : : {
149 : 380 : Node ret = n;
150 [ + + ]: 190 : if (n.getNumChildren() == 3)
151 : : {
152 : : // Do not pre-skolemize quantified formulas with three children.
153 : : // This includes non-standard quantified formulas
154 : : // like recursive function definitions, or sygus conjectures, and
155 : : // quantified formulas with triggers.
156 : : }
157 [ + + ]: 78 : else if (polarity)
158 : : {
159 [ + + ]: 62 : if (options().quantifiers.preSkolemQuantNested)
160 : : {
161 : 80 : std::vector<Node> children;
162 : 40 : children.push_back(n[0]);
163 : : // add children to current scope
164 : 80 : std::vector<TNode> fvss;
165 : 40 : fvss.insert(fvss.end(), fvs.begin(), fvs.end());
166 : 40 : fvss.insert(fvss.end(), n[0].begin(), n[0].end());
167 : : // process body in a new context
168 : : std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>
169 : 80 : visitedSub;
170 : 40 : Node pbody = preSkolemizeQuantifiers(n[1], polarity, fvss, visitedSub);
171 : 40 : children.push_back(pbody);
172 : : // return processed quantifier
173 : 40 : ret = nm->mkNode(Kind::FORALL, children);
174 : : }
175 : : }
176 : : else
177 : : {
178 : : // will skolemize current, process body
179 : 32 : Node nn = preSkolemizeQuantifiers(n[1], polarity, fvs, visited);
180 : 32 : std::vector<Node> sk;
181 : 32 : Node sub;
182 : 16 : std::vector<unsigned> sub_vars;
183 : : // return skolemized body
184 : 32 : ret = Skolemize::mkSkolemizedBodyInduction(
185 : 16 : options(), n, nn, fvs, sk, sub, sub_vars);
186 : : }
187 : 190 : visited[key] = ret;
188 : 190 : return ret;
189 : : }
190 : : // check if it contains a quantifier as a subterm
191 : : // if so, we may preprocess this node
192 [ + + ]: 493 : if (!expr::hasClosure(n))
193 : : {
194 : 453 : visited[key] = n;
195 : 453 : return n;
196 : : }
197 : 40 : Kind k = n.getKind();
198 : 80 : Node ret = n;
199 [ - + ][ - + ]: 40 : Assert(n.getType().isBoolean());
[ - - ]
200 : 40 : if (k == Kind::ITE || (k == Kind::EQUAL && n[0].getType().isBoolean()))
201 : : {
202 : 6 : if (options().quantifiers.preSkolemQuant
203 [ - + ]: 6 : == options::PreSkolemQuantMode::AGG)
204 : : {
205 : 0 : Node nn;
206 : : // must remove structure
207 [ - - ]: 0 : if (k == Kind::ITE)
208 : : {
209 : 0 : nn = nm->mkNode(Kind::AND,
210 : 0 : nm->mkNode(Kind::OR, n[0].notNode(), n[1]),
211 : 0 : nm->mkNode(Kind::OR, n[0], n[2]));
212 : : }
213 [ - - ]: 0 : else if (k == Kind::EQUAL)
214 : : {
215 : 0 : nn = nm->mkNode(Kind::AND,
216 : 0 : nm->mkNode(Kind::OR, n[0].notNode(), n[1]),
217 : 0 : nm->mkNode(Kind::OR, n[0], n[1].notNode()));
218 : : }
219 : 0 : ret = preSkolemizeQuantifiers(nn, polarity, fvs, visited);
220 : : }
221 : : }
222 [ + + ][ + + ]: 34 : else if (k == Kind::AND || k == Kind::OR || k == Kind::NOT
[ + + ]
223 [ - + ]: 2 : || k == Kind::IMPLIES)
224 : : {
225 : 32 : std::vector<Node> children;
226 [ + + ]: 76 : for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
227 : : {
228 : : bool newHasPol;
229 : : bool newPol;
230 : 44 : QuantPhaseReq::getPolarity(n, i, true, polarity, newHasPol, newPol);
231 [ - + ][ - + ]: 44 : Assert(newHasPol);
[ - - ]
232 : 44 : children.push_back(preSkolemizeQuantifiers(n[i], newPol, fvs, visited));
233 : : }
234 : 32 : ret = nm->mkNode(k, children);
235 : : }
236 : 40 : visited[key] = ret;
237 : 40 : return ret;
238 : : }
239 : :
240 : 323243 : TrustNode QuantifiersPreprocess::preprocess(Node n, bool isInst) const
241 : : {
242 : 646486 : Node prev = n;
243 [ + + ]: 323243 : if (options().quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
244 : : {
245 [ + + ][ + + ]: 644 : if (!isInst || !options().quantifiers.preSkolemQuantNested)
[ + + ]
246 : : {
247 [ + - ]: 1166 : Trace("quantifiers-preprocess-debug")
248 : 583 : << "Pre-skolemize " << n << "..." << std::endl;
249 : : // apply pre-skolemization to existential quantifiers
250 : 1166 : std::vector<TNode> fvs;
251 : : std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>
252 : 583 : visited;
253 : 583 : n = preSkolemizeQuantifiers(prev, true, fvs, visited);
254 : : }
255 : : }
256 : : // pull all quantifiers globally
257 [ + + ]: 323243 : if (options().quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
258 : : {
259 [ + - ]: 4 : Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
260 : 4 : std::map<Node, Node> visited;
261 : 4 : n = computePrenexAgg(n, visited);
262 : 4 : n = rewrite(n);
263 [ + - ]: 4 : Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl;
264 : : }
265 [ + + ]: 323243 : if (n != prev)
266 : : {
267 [ + - ]: 17 : Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl;
268 [ + - ]: 17 : Trace("quantifiers-preprocess") << "..returned " << n << std::endl;
269 : 17 : return TrustNode::mkTrustRewrite(prev, n, nullptr);
270 : : }
271 : 323226 : return TrustNode::null();
272 : : }
273 : :
274 : : } // namespace quantifiers
275 : : } // namespace theory
276 : : } // namespace cvc5::internal
|
