src/preprocessing/passes/ackermann.h

   1 /*********************                                                        */
   2 /*! \file ackermann.h
   3  ** \verbatim
   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
  11  **
  12  ** \brief Ackermannization preprocessing pass.
  13  **
  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
  18  ** described in
  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
  22  **/
  23
  24 #include "cvc4_private.h"
  25
  26 #ifndef CVC4__PREPROCESSING__PASSES__ACKERMANN_H
  27 #define CVC4__PREPROCESSING__PASSES__ACKERMANN_H
  28
  29 #include <unordered_map>
  30 #include "expr/node.h"
  31 #include "preprocessing/preprocessing_pass.h"
  32 #include "preprocessing/preprocessing_pass_context.h"
  33
  34 namespace CVC4 {
  35 namespace preprocessing {
  36 namespace passes {
  37
  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>;
  43
  44 class Ackermann : public PreprocessingPass
  45 {
  46  public:
  47   Ackermann(PreprocessingPassContext* preprocContext);
  48
  49  protected:
  50   /**
  51    * Apply Ackermannization as follows:
  52    *
  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).
  55    *
  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
  59    *
  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.
  63    */
  64   PreprocessingPassResult applyInternal(
  65       AssertionPipeline* assertionsToPreprocess) override;
  66
  67  private:
  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
  71    * ackermannization */
  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;
  78   LogicInfo d_logic;
  79 };
  80
  81 }  // namespace passes
  82 }  // namespace preprocessing
  83 }  // namespace CVC4
  84
  85 #endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */