diff options
Diffstat (limited to 'src/preprocessing/passes/bv_ackermann.h')
-rw-r--r-- | src/preprocessing/passes/bv_ackermann.h | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h new file mode 100644 index 000000000..dbac79d21 --- /dev/null +++ b/src/preprocessing/passes/bv_ackermann.h @@ -0,0 +1,68 @@ +/********************* */ +/*! \file bv_ackermann.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Ackermannization preprocessing pass. + ** + ** This implements the Ackermannization preprocessing pass, which enables + ** very limited theory combination support for eager bit-blasting via + ** Ackermannization. It reduces constraints over the combination of the + ** theories of fixed-size bit-vectors and uninterpreted functions as + ** described in + ** Liana Hadarean, An Efficient and Trustworthy Theory Solver for + ** Bit-vectors in Satisfiability Modulo Theories. +** https://cs.nyu.edu/media/publications/hadarean_liana.pdf + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +#include <unordered_map> + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgsMap; + +class BVAckermann : public PreprocessingPass +{ + public: + BVAckermann(PreprocessingPassContext* preprocContext); + + protected: + /** + * Apply Ackermannization as follows: + * + * - For each application f(X) where X = (x1, . . . , xn), introduce a fresh + * variable f_X and use it to replace all occurrences of f(X). + * + * - For each f(X) and f(Y) with X = (x1, . . . , xn) and Y = (y1, . . . , yn) + * occurring in the input formula, add the following lemma: + * (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y + */ + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + FunctionToArgsMap d_funcToArgs; + theory::SubstitutionMap d_funcToSkolem; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif |