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

Line Exec Source
1
/*********************                                                        */
2
/*! \file ho_elim.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli
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 The HoElim preprocessing pass
13
 **
14
 ** Eliminates higher-order constraints.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H
20
#define __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H
21
22
#include <map>
23
#include <unordered_map>
24
#include <unordered_set>
25
26
#include "expr/node.h"
27
#include "preprocessing/preprocessing_pass.h"
28
29
namespace CVC4 {
30
namespace preprocessing {
31
namespace passes {
32
33
/** Higher-order elimination.
34
 *
35
 * This preprocessing pass eliminates all occurrences of higher-order
36
 * constraints in the input, and replaces the entire input problem with
37
 * an equisatisfiable one. This is based on the following steps.
38
 *
39
 * [1] Eliminate all occurrences of lambdas via lambda lifting. This includes
40
 * lambdas with free variables that occur in quantifier bodies (see
41
 * documentation for eliminateLambdaComplete).
42
 *
43
 * [2] Eliminate all occurrences of partial applications and constraints
44
 * involving functions as first-class members. This is done by first
45
 * turning all function applications into an applicative encoding involving the
46
 * parametric binary operator @ (of kind HO_APPLY). Then we introduce:
47
 * - An uninterpreted sort U(T) for each function type T,
48
 * - A function H(f) of sort U(T1) x .. x U(Tn) -> U(T) for each function f
49
 * of sort T1 x ... x Tn -> T.
50
 * - A function App_{T1 x T2 ... x Tn -> T} of type
51
 *   U(T1 x T2 ... x Tn -> T) x U(T1) -> U(T2 ... x Tn -> T)
52
 * for each occurrence of @ applied to arguments of types T1 x T2 ... x Tn -> T
53
 * and T1.
54
 *
55
 * [3] Add additional axioms to ensure the correct interpretation of
56
 * the sorts U(...), and functions App_{...}. This includes:
57
 *
58
 * - The "extensionality" axiom for App_{...} terms, stating that functions
59
 * that behave the same according to App for all inputs must be equal:
60
 *   forall x : U(T1->T2), y : U(T1->T2).
61
 *      ( forall z : T1. App_{T1->T2}( x, z ) = App_{T1->T2}( y, z ) ) =>
62
 *        x = y
63
 *
64
 * - The "store" axiom, which effectively states that for all (encoded)
65
 * functions f, there exists a function g that behaves identically to f, except
66
 * that g for argument i is e:
67
 *   forall x : U(T1->T2), i : U(T1), e : U(T2).
68
 *     exists g : U(T1->T2).
69
 *       forall z: T1.
70
 *         App_{T1->T2}( g, z ) = ite( z = i, e, App_{T1->T2}( f, z ) ).
71
 *
72
 *
73
 * Based on options, this preprocessing pass may apply a subset o the above
74
 * steps. In particular:
75
 * * If options::hoElim() is true, then step [2] is taken and extensionality
76
 * axioms are added in step [3].
77
 * * If options::hoElimStoreAx() is true, then store axioms are added in step 3.
78
 * The form of these axioms depends on whether options::hoElim() is true. If it
79
 * is true, the axiom is given in terms of the uninterpreted functions that
80
 * encode function sorts. If it is false, then the store axiom is given in terms
81
 * of the original function sorts.
82
 */
83
17984
class HoElim : public PreprocessingPass
84
{
85
 public:
86
  HoElim(PreprocessingPassContext* preprocContext);
87
88
 protected:
89
  PreprocessingPassResult applyInternal(
90
      AssertionPipeline* assertionsToPreprocess) override;
91
  /**
92
   * Eliminate all occurrences of lambdas in term n, return the result. This
93
   * is step [1] mentioned at the header of this class.
94
   *
95
   * The map newLambda maps newly introduced function skolems with their
96
   * (lambda) definition, which is a closed term.
97
   *
98
   * Notice that to ensure that all lambda definitions are closed, we
99
   * introduce extra bound arguments to the lambda, for example:
100
   *    forall x. (lambda y. x+y) != f
101
   * becomes
102
   *    forall x. g(x) != f
103
   * where g is mapped to the (closed) term ( lambda xy. x+y ).
104
   *
105
   * Notice that the definitions in newLambda may themselves contain lambdas,
106
   * hence, this method is run until a fix point is reached.
107
   */
108
  Node eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda);
109
110
  /**
111
   * Eliminate all higher-order constraints in n, return the result. This is
112
   * step [2] mentioned at the header of this class.
113
   */
114
  Node eliminateHo(Node n);
115
  /**
116
   * Stores the set of nodes we have current visited and their results
117
   * in steps [1] and [2] of this pass.
118
   */
119
  std::unordered_map<Node, Node, NodeHashFunction> d_visited;
120
  /**
121
   * Stores the mapping from functions f to their corresponding function H(f)
122
   * in the encoding for step [2] of this pass.
123
   */
124
  std::unordered_map<TNode, Node, TNodeHashFunction> d_visited_op;
125
  /** The set of all function types encountered in assertions. */
126
  std::unordered_set<TypeNode, TypeNodeHashFunction> d_funTypes;
127
128
  /**
129
   * Get ho apply uf, this returns App_{@_{T1 x T2 ... x Tn -> T}}
130
   */
131
  Node getHoApplyUf(TypeNode tn);
132
  /**
133
   * Get ho apply uf, where:
134
   *   tn is T1 x T2 ... x Tn -> T,
135
   *   tna is T1,
136
   *   tnr is T2 ... x Tn -> T
137
   * This returns App_{@_{T1 x T2 ... x Tn -> T}}.
138
   */
139
  Node getHoApplyUf(TypeNode tn, TypeNode tna, TypeNode tnr);
140
  /** cache of getHoApplyUf */
141
  std::map<TypeNode, Node> d_hoApplyUf;
142
  /**
143
   * Get uninterpreted sort for function sort. This returns U(T) for function
144
   * type T for step [2] of this pass.
145
   */
146
  TypeNode getUSort(TypeNode tn);
147
  /** cache of the above function */
148
  std::map<TypeNode, TypeNode> d_ftypeMap;
149
};
150
151
}  // namespace passes
152
}  // namespace preprocessing
153
}  // namespace CVC4
154
155
#endif /* __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H */