GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/ackermann.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
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-2021 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
31
#include "expr/node.h"
32
#include "preprocessing/preprocessing_pass.h"
33
#include "theory/logic_info.h"
34
#include "theory/substitutions.h"
35
36
namespace CVC4 {
37
namespace preprocessing {
38
namespace passes {
39
40
using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
41
using FunctionToArgsMap =
42
    std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
43
using USortToBVSizeMap =
44
    std::unordered_map<TypeNode, size_t, TypeNode::HashFunction>;
45
46
17988
class Ackermann : public PreprocessingPass
47
{
48
 public:
49
  Ackermann(PreprocessingPassContext* preprocContext);
50
51
 protected:
52
  /**
53
   * Apply Ackermannization as follows:
54
   *
55
   * - For each application f(X) where X = (x1, . . . , xn), introduce a fresh
56
   *   variable f_X and use it to replace all occurrences of f(X).
57
   *
58
   * - For each f(X) and f(Y) with X = (x1, . . . , xn) and Y = (y1, . . . , yn)
59
   *   occurring in the input formula, add the following lemma:
60
   *     (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y
61
   *
62
   * - For each uninterpreted sort S, suppose k is the number of variables with
63
   *   sort S, then for each such variable X, introduce a fresh variable BV_X
64
   *   with BV with size log_2(k)+1 and use it to replace all occurrences of X.
65
   */
66
  PreprocessingPassResult applyInternal(
67
      AssertionPipeline* assertionsToPreprocess) override;
68
69
 private:
70
  /* Map each function to a set of terms associated with it */
71
  FunctionToArgsMap d_funcToArgs;
72
  /* Map each function-application term to the new Skolem variable created by
73
   * ackermannization */
74
  theory::SubstitutionMap d_funcToSkolem;
75
  /* Map each variable with uninterpreted sort to the new Skolem BV variable
76
   * created by ackermannization */
77
  theory::SubstitutionMap d_usVarsToBVVars;
78
  /* Map each uninterpreted sort to the number of variables in this sort. */
79
  USortToBVSizeMap d_usortCardinality;
80
  LogicInfo d_logic;
81
};
82
83
}  // namespace passes
84
}  // namespace preprocessing
85
}  // namespace CVC4
86
87
#endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */