Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Yoni Zohar, Ying Sheng, Aina Niemetz
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 : : * Ackermannization preprocessing pass.
14 : : *
15 : : * This implements the Ackermannization preprocessing pass, which enables
16 : : * very limited theory combination support for eager bit-blasting via
17 : : * Ackermannization. It reduces constraints over the combination of the
18 : : * theories of fixed-size bit-vectors and uninterpreted functions as
19 : : * described in
20 : : * Liana Hadarean, An Efficient and Trustworthy Theory Solver for
21 : : * Bit-vectors in Satisfiability Modulo Theories.
22 : : * https://cs.nyu.edu/media/publications/hadarean_liana.pdf
23 : : */
24 : :
25 : : #include "preprocessing/passes/ackermann.h"
26 : :
27 : : #include <cmath>
28 : :
29 : : #include "base/check.h"
30 : : #include "expr/node_algorithm.h"
31 : : #include "expr/skolem_manager.h"
32 : : #include "smt/logic_exception.h"
33 : : #include "options/base_options.h"
34 : : #include "options/options.h"
35 : : #include "preprocessing/assertion_pipeline.h"
36 : : #include "preprocessing/preprocessing_pass_context.h"
37 : :
38 : : using namespace cvc5::internal;
39 : : using namespace cvc5::internal::theory;
40 : :
41 : : namespace cvc5::internal {
42 : : namespace preprocessing {
43 : : namespace passes {
44 : :
45 : : /* -------------------------------------------------------------------------- */
46 : :
47 : : namespace {
48 : :
49 : 891 : void addLemmaForPair(TNode args1,
50 : : TNode args2,
51 : : const TNode func,
52 : : AssertionPipeline* assertionsToPreprocess,
53 : : NodeManager* nm)
54 : : {
55 : 1782 : Node args_eq;
56 : :
57 [ + + ]: 891 : if (args1.getKind() == Kind::APPLY_UF)
58 : : {
59 [ - + ][ - + ]: 680 : Assert(args1.getOperator() == func);
[ - - ]
60 : 1360 : Assert(args2.getKind() == Kind::APPLY_UF && args2.getOperator() == func);
61 [ - + ][ - + ]: 680 : Assert(args1.getNumChildren() == args2.getNumChildren());
[ - - ]
62 [ - + ][ - + ]: 680 : Assert(args1.getNumChildren() >= 1);
[ - - ]
63 : :
64 : 1360 : std::vector<Node> eqs(args1.getNumChildren());
65 : :
66 [ + + ]: 1360 : for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
67 : : {
68 : 680 : eqs[i] = nm->mkNode(Kind::EQUAL, args1[i], args2[i]);
69 : : }
70 [ - + ]: 680 : if (eqs.size() >= 2)
71 : : {
72 : 0 : args_eq = nm->mkNode(Kind::AND, eqs);
73 : : }
74 : : else
75 : : {
76 : 680 : args_eq = eqs[0];
77 : : }
78 : : }
79 : : else
80 : : {
81 : 422 : Assert(args1.getKind() == Kind::SELECT && args1.getOperator() == func);
82 : 422 : Assert(args2.getKind() == Kind::SELECT && args2.getOperator() == func);
83 [ - + ][ - + ]: 211 : Assert(args1.getNumChildren() == 2);
[ - - ]
84 [ - + ][ - + ]: 211 : Assert(args2.getNumChildren() == 2);
[ - - ]
85 : 633 : args_eq = nm->mkNode(Kind::AND,
86 : 422 : nm->mkNode(Kind::EQUAL, args1[0], args2[0]),
87 : 633 : nm->mkNode(Kind::EQUAL, args1[1], args2[1]));
88 : : }
89 : 2673 : Node func_eq = nm->mkNode(Kind::EQUAL, args1, args2);
90 : 1782 : Node lemma = nm->mkNode(Kind::IMPLIES, args_eq, func_eq);
91 : 891 : assertionsToPreprocess->push_back(lemma);
92 : 891 : }
93 : :
94 : 570 : void storeFunctionAndAddLemmas(TNode func,
95 : : TNode term,
96 : : FunctionToArgsMap& fun_to_args,
97 : : SubstitutionMap& fun_to_skolem,
98 : : AssertionPipeline* assertions,
99 : : NodeManager* nm,
100 : : std::vector<TNode>* vec)
101 : : {
102 [ + + ]: 570 : if (fun_to_args.find(func) == fun_to_args.end())
103 : : {
104 : 177 : fun_to_args.insert(make_pair(func, TNodeSet()));
105 : : }
106 : 570 : TNodeSet& set = fun_to_args[func];
107 [ + - ]: 570 : if (set.find(term) == set.end())
108 : : {
109 : 570 : SkolemManager* sm = nm->getSkolemManager();
110 : 1140 : Node skolem = sm->mkPurifySkolem(term);
111 [ + + ]: 1461 : for (const auto& t : set)
112 : : {
113 : 891 : addLemmaForPair(t, term, func, assertions, nm);
114 : : }
115 : 570 : fun_to_skolem.addSubstitution(term, skolem);
116 : 570 : set.insert(term);
117 : : /* Add the arguments of term (newest element in set) to the vector, so that
118 : : * collectFunctionsAndLemmas will process them as well.
119 : : * This is only needed if the set has at least two elements
120 : : * (otherwise, no lemma is generated).
121 : : * Therefore, we defer this for term in case it is the first element in the
122 : : * set*/
123 [ + + ]: 570 : if (set.size() == 2)
124 : : {
125 [ + + ]: 489 : for (TNode elem : set)
126 : : {
127 : 326 : vec->insert(vec->end(), elem.begin(), elem.end());
128 : : }
129 : : }
130 [ + + ]: 407 : else if (set.size() > 2)
131 : : {
132 : 230 : vec->insert(vec->end(), term.begin(), term.end());
133 : : }
134 : : }
135 : 570 : }
136 : :
137 : : /* We only add top-level applications of functions.
138 : : * For example: when we see "f(g(x))", we do not add g as a function and x as a
139 : : * parameter.
140 : : * Instead, we only include f as a function and g(x) as a parameter.
141 : : * However, if we see g(x) later on as a top-level application, we will add it
142 : : * as well.
143 : : * Another example: for the formula f(g(x))=f(g(y)),
144 : : * we first only add f as a function and g(x),g(y) as arguments.
145 : : * storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) ->
146 : : * f(g(x))=f(g(y)).
147 : : * Now that we see g(x) and g(y), we explicitly add them as well. */
148 : 121 : void collectFunctionsAndLemmas(NodeManager* nm,
149 : : FunctionToArgsMap& fun_to_args,
150 : : SubstitutionMap& fun_to_skolem,
151 : : std::vector<TNode>* vec,
152 : : AssertionPipeline* assertions)
153 : : {
154 : 242 : TNodeSet seen;
155 : 242 : TNode term;
156 [ + + ]: 6186 : while (!vec->empty())
157 : : {
158 : 6066 : term = vec->back();
159 : 6066 : vec->pop_back();
160 [ + + ]: 6066 : if (seen.find(term) == seen.end())
161 : : {
162 : 6984 : TNode func;
163 [ + + ][ + + ]: 3492 : if (term.getKind() == Kind::APPLY_UF || term.getKind() == Kind::SELECT)
[ + + ]
164 : : {
165 : 570 : storeFunctionAndAddLemmas(term.getOperator(),
166 : : term,
167 : : fun_to_args,
168 : : fun_to_skolem,
169 : : assertions,
170 : : nm,
171 : : vec);
172 : : }
173 [ + + ]: 2922 : else if (term.getKind() == Kind::STORE)
174 : : {
175 : : throw LogicException("Ackermannization is not supported for kind: "
176 : 1 : + kindToString(term.getKind()));
177 : : }
178 : : else
179 : : {
180 : : /* add children to the vector, so that they are processed later */
181 [ + + ]: 7642 : for (TNode n : term)
182 : : {
183 : 4721 : vec->push_back(n);
184 : : }
185 : : }
186 : 3491 : seen.insert(term);
187 : : }
188 : : }
189 : 120 : }
190 : :
191 : : } // namespace
192 : :
193 : : /* -------------------------------------------------------------------------- */
194 : :
195 : : /* Given a minimum capacity for an uninterpreted sort, return the size of the
196 : : * new BV type */
197 : 117 : size_t getBVSkolemSize(size_t capacity)
198 : : {
199 : 117 : return static_cast<size_t>(log2(capacity)) + 1;
200 : : }
201 : :
202 : : /* Given the lowest capacity requirements for each uninterpreted sort, assign
203 : : * a sufficient bit-vector size.
204 : : * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
205 : : * the fresh skolem BV variables. variables */
206 : 17 : void collectUSortsToBV(NodeManager* nm,
207 : : const std::unordered_set<TNode>& vars,
208 : : const USortToBVSizeMap& usortCardinality,
209 : : SubstitutionMap& usVarsToBVVars)
210 : : {
211 : 17 : SkolemManager* sm = nm->getSkolemManager();
212 : :
213 [ + + ]: 134 : for (TNode var : vars)
214 : : {
215 : 234 : TypeNode type = var.getType();
216 : 117 : size_t size = getBVSkolemSize(usortCardinality.at(type));
217 : : Node skolem = sm->mkDummySkolem(
218 : : "ackermann.bv",
219 : 234 : nm->mkBitVectorType(size),
220 : : "a variable created by the ackermannization "
221 : : "preprocessing pass, representing a variable with uninterpreted sort "
222 : 468 : + type.toString() + ".");
223 : 117 : usVarsToBVVars.addSubstitution(var, skolem);
224 : : }
225 : 17 : }
226 : :
227 : : /* This function returns the list of terms with uninterpreted sort in the
228 : : * formula represented by assertions. */
229 : 120 : std::unordered_set<TNode> getVarsWithUSorts(AssertionPipeline* assertions)
230 : : {
231 : 120 : std::unordered_set<TNode> res;
232 : :
233 [ + + ]: 1712 : for (const Node& assertion : assertions->ref())
234 : : {
235 : 3184 : std::unordered_set<Node> vars;
236 : 1592 : expr::getVariables(assertion, vars);
237 : :
238 [ + + ]: 6404 : for (const Node& var : vars)
239 : : {
240 [ + + ]: 4812 : if (var.getType().isUninterpretedSort())
241 : : {
242 : 468 : res.insert(var);
243 : : }
244 : : }
245 : : }
246 : :
247 : 120 : return res;
248 : : }
249 : :
250 : : /* This is the top level of converting uninterpreted sorts to bit-vectors.
251 : : * We count the number of different variables for each uninterpreted sort.
252 : : * Then for each sort, we will assign a new bit-vector type with a sufficient
253 : : * size. The size is calculated to have enough capacity, that can accommodate
254 : : * the variables occured in the original formula. At the end, all variables of
255 : : * uninterpreted sorts will be converted into Skolem variables of BV */
256 : 120 : void usortsToBitVectors(NodeManager* nm,
257 : : const LogicInfo& d_logic,
258 : : AssertionPipeline* assertions,
259 : : USortToBVSizeMap& usortCardinality,
260 : : SubstitutionMap& usVarsToBVVars)
261 : : {
262 : 120 : std::unordered_set<TNode> toProcess = getVarsWithUSorts(assertions);
263 : :
264 [ + + ]: 120 : if (toProcess.size() > 0)
265 : : {
266 : : /* the current version only supports BV for removing uninterpreted sorts */
267 [ - + ]: 17 : if (!d_logic.isTheoryEnabled(theory::THEORY_BV))
268 : : {
269 : 0 : return;
270 : : }
271 : :
272 [ + + ]: 134 : for (TNode term : toProcess)
273 : : {
274 : 117 : TypeNode type = term.getType();
275 : : /* Update the counts for each uninterpreted sort.
276 : : * For non-existing keys, C++ will create a new element for it, which has
277 : : * a default 0 value, before incrementing by 1. */
278 : 117 : usortCardinality[type] = usortCardinality[type] + 1;
279 : : }
280 : :
281 : 17 : collectUSortsToBV(nm, toProcess, usortCardinality, usVarsToBVVars);
282 : :
283 [ + + ]: 298 : for (size_t i = 0, size = assertions->size(); i < size; ++i)
284 : : {
285 : 562 : Node old = (*assertions)[i];
286 : 562 : Node newA = usVarsToBVVars.apply((*assertions)[i]);
287 [ + + ]: 281 : if (newA != old)
288 : : {
289 : 207 : assertions->replace(i, newA);
290 [ + - ]: 414 : Trace("uninterpretedSorts-to-bv")
291 : 207 : << " " << old << " => " << (*assertions)[i] << "\n";
292 : : }
293 : : }
294 : : }
295 : : }
296 : :
297 : : /* -------------------------------------------------------------------------- */
298 : :
299 : 49866 : Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
300 : : : PreprocessingPass(preprocContext, "ackermann"),
301 : 99732 : d_funcToSkolem(userContext()),
302 : 99732 : d_usVarsToBVVars(userContext()),
303 : 49866 : d_logic(logicInfo())
304 : : {
305 : 49866 : }
306 : :
307 : 121 : PreprocessingPassResult Ackermann::applyInternal(
308 : : AssertionPipeline* assertionsToPreprocess)
309 : : {
310 [ - + ][ - + ]: 121 : AlwaysAssert(!options().base.incrementalSolving);
[ - - ]
311 : :
312 : : /* collect all function applications and generate consistency lemmas
313 : : * accordingly */
314 : 122 : std::vector<TNode> to_process;
315 [ + + ]: 826 : for (const Node& a : assertionsToPreprocess->ref())
316 : : {
317 : 705 : to_process.push_back(a);
318 : : }
319 : 121 : collectFunctionsAndLemmas(nodeManager(),
320 : 121 : d_funcToArgs,
321 : 121 : d_funcToSkolem,
322 : : &to_process,
323 : : assertionsToPreprocess);
324 : :
325 : : /* replace applications of UF by skolems */
326 : : // FIXME for model building, github issue #1901
327 [ + + ]: 1712 : for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
328 : : {
329 : 1592 : assertionsToPreprocess->replace(
330 : 3184 : i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
331 : : }
332 : :
333 : : /* replace uninterpreted sorts with bit-vectors */
334 : 120 : usortsToBitVectors(nodeManager(),
335 : 120 : d_logic,
336 : : assertionsToPreprocess,
337 : 120 : d_usortCardinality,
338 : 120 : d_usVarsToBVVars);
339 : :
340 : 240 : return PreprocessingPassResult::NO_CONFLICT;
341 : : }
342 : :
343 : : /* -------------------------------------------------------------------------- */
344 : :
345 : : } // namespace passes
346 : : } // namespace preprocessing
347 : : } // namespace cvc5::internal
|
