1 /********************* */
4 ** Top contributors (to current version):
5 ** Ying Sheng, Aina Niemetz, Yoni Zohar
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Ackermannization preprocessing pass.
14 ** This implements the Ackermannization preprocessing pass, which enables
15 ** very limited theory combination support for eager bit-blasting via
16 ** Ackermannization. It reduces constraints over the combination of the
17 ** theories of fixed-size bit-vectors and uninterpreted functions as
19 ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for
20 ** Bit-vectors in Satisfiability Modulo Theories.
21 ** https://cs.nyu.edu/media/publications/hadarean_liana.pdf
24 #include "cvc4_private.h"
26 #ifndef CVC4__PREPROCESSING__PASSES__ACKERMANN_H
27 #define CVC4__PREPROCESSING__PASSES__ACKERMANN_H
29 #include <unordered_map>
30 #include "expr/node.h"
31 #include "preprocessing/preprocessing_pass.h"
32 #include "preprocessing/preprocessing_pass_context.h"
35 namespace preprocessing
{
38 using TNodeSet
= std::unordered_set
<TNode
, TNodeHashFunction
>;
39 using FunctionToArgsMap
=
40 std::unordered_map
<TNode
, TNodeSet
, TNodeHashFunction
>;
41 using USortToBVSizeMap
=
42 std::unordered_map
<TypeNode
, size_t, TypeNode::HashFunction
>;
44 class Ackermann
: public PreprocessingPass
47 Ackermann(PreprocessingPassContext
* preprocContext
);
51 * Apply Ackermannization as follows:
53 * - For each application f(X) where X = (x1, . . . , xn), introduce a fresh
54 * variable f_X and use it to replace all occurrences of f(X).
56 * - For each f(X) and f(Y) with X = (x1, . . . , xn) and Y = (y1, . . . , yn)
57 * occurring in the input formula, add the following lemma:
58 * (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y
60 * - For each uninterpreted sort S, suppose k is the number of variables with
61 * sort S, then for each such variable X, introduce a fresh variable BV_X
62 * with BV with size log_2(k)+1 and use it to replace all occurrences of X.
64 PreprocessingPassResult
applyInternal(
65 AssertionPipeline
* assertionsToPreprocess
) override
;
68 /* Map each function to a set of terms associated with it */
69 FunctionToArgsMap d_funcToArgs
;
70 /* Map each function-application term to the new Skolem variable created by
72 theory::SubstitutionMap d_funcToSkolem
;
73 /* Map each variable with uninterpreted sort to the new Skolem BV variable
74 * created by ackermannization */
75 theory::SubstitutionMap d_usVarsToBVVars
;
76 /* Map each uninterpreted sort to the number of variables in this sort. */
77 USortToBVSizeMap d_usortCardinality
;
82 } // namespace preprocessing
85 #endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */