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(FunctionToArgsMap& fun_to_args,
149 : : SubstitutionMap& fun_to_skolem,
150 : : std::vector<TNode>* vec,
151 : : AssertionPipeline* assertions)
152 : : {
153 : 242 : TNodeSet seen;
154 : 121 : NodeManager* nm = NodeManager::currentNM();
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(const std::unordered_set<TNode>& vars,
207 : : const USortToBVSizeMap& usortCardinality,
208 : : SubstitutionMap& usVarsToBVVars)
209 : : {
210 : 17 : NodeManager* nm = NodeManager::currentNM();
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(const LogicInfo& d_logic,
257 : : AssertionPipeline* assertions,
258 : : USortToBVSizeMap& usortCardinality,
259 : : SubstitutionMap& usVarsToBVVars)
260 : : {
261 : 120 : std::unordered_set<TNode> toProcess = getVarsWithUSorts(assertions);
262 : :
263 [ + + ]: 120 : if (toProcess.size() > 0)
264 : : {
265 : : /* the current version only supports BV for removing uninterpreted sorts */
266 [ - + ]: 17 : if (!d_logic.isTheoryEnabled(theory::THEORY_BV))
267 : : {
268 : 0 : return;
269 : : }
270 : :
271 [ + + ]: 134 : for (TNode term : toProcess)
272 : : {
273 : 117 : TypeNode type = term.getType();
274 : : /* Update the counts for each uninterpreted sort.
275 : : * For non-existing keys, C++ will create a new element for it, which has
276 : : * a default 0 value, before incrementing by 1. */
277 : 117 : usortCardinality[type] = usortCardinality[type] + 1;
278 : : }
279 : :
280 : 17 : collectUSortsToBV(toProcess, usortCardinality, usVarsToBVVars);
281 : :
282 [ + + ]: 298 : for (size_t i = 0, size = assertions->size(); i < size; ++i)
283 : : {
284 : 562 : Node old = (*assertions)[i];
285 : 562 : Node newA = usVarsToBVVars.apply((*assertions)[i]);
286 [ + + ]: 281 : if (newA != old)
287 : : {
288 : 207 : assertions->replace(i, newA);
289 [ + - ]: 414 : Trace("uninterpretedSorts-to-bv")
290 : 207 : << " " << old << " => " << (*assertions)[i] << "\n";
291 : : }
292 : : }
293 : : }
294 : : }
295 : :
296 : : /* -------------------------------------------------------------------------- */
297 : :
298 : 49805 : Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
299 : : : PreprocessingPass(preprocContext, "ackermann"),
300 : 99610 : d_funcToSkolem(userContext()),
301 : 99610 : d_usVarsToBVVars(userContext()),
302 : 49805 : d_logic(logicInfo())
303 : : {
304 : 49805 : }
305 : :
306 : 121 : PreprocessingPassResult Ackermann::applyInternal(
307 : : AssertionPipeline* assertionsToPreprocess)
308 : : {
309 [ - + ][ - + ]: 121 : AlwaysAssert(!options().base.incrementalSolving);
[ - - ]
310 : :
311 : : /* collect all function applications and generate consistency lemmas
312 : : * accordingly */
313 : 122 : std::vector<TNode> to_process;
314 [ + + ]: 826 : for (const Node& a : assertionsToPreprocess->ref())
315 : : {
316 : 705 : to_process.push_back(a);
317 : : }
318 : 121 : collectFunctionsAndLemmas(
319 : 121 : d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess);
320 : :
321 : : /* replace applications of UF by skolems */
322 : : // FIXME for model building, github issue #1901
323 [ + + ]: 1712 : for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
324 : : {
325 : 1592 : assertionsToPreprocess->replace(
326 : 3184 : i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
327 : : }
328 : :
329 : : /* replace uninterpreted sorts with bit-vectors */
330 : 120 : usortsToBitVectors(
331 : 120 : d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars);
332 : :
333 : 240 : return PreprocessingPassResult::NO_CONFLICT;
334 : : }
335 : :
336 : : /* -------------------------------------------------------------------------- */
337 : :
338 : : } // namespace passes
339 : : } // namespace preprocessing
340 : : } // namespace cvc5::internal
|