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