1/*
2 * Licensed to the Apache Software Foundation (ASF) under one
3 * or more contributor license agreements. See the NOTICE file
4 * distributed with this work for additional information
5 * regarding copyright ownership. The ASF licenses this file
6 * to you under the Apache License, Version 2.0 (the
7 * "License"); you may not use this file except in compliance
8 * with the License. You may obtain a copy of the License at
9 *
10 * http://www.apache.org/licenses/LICENSE-2.0
11 *
12 * Unless required by applicable law or agreed to in writing,
13 * software distributed under the License is distributed on an
14 * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
15 * KIND, either express or implied. See the License for the
16 * specific language governing permissions and limitations
17 * under the License.
18 */
19
20/*!
21 * \file contraint_extract.h
22 *
23 * \brief Centralized location for extraction of constraints from a boolean expression.
24 */
25
26#ifndef TVM_ARITH_CONSTRAINT_EXTRACT_H_
27#define TVM_ARITH_CONSTRAINT_EXTRACT_H_
28
29#include <tvm/tir/expr.h>
30
31#include <vector>
32
33namespace tvm {
34namespace arith {
35
36/* \brief Returns constraints that are true if the expression is true.
37 *
38 * Utility to break up a boolean expression into independent
39 * constraints.
40 *
41 * Example: `i==5 && j==3` => `[i==5 && j==3, i==5, j==3]`
42 * Example: `i==5 || j==3` => `[i==5 || j==3]`
43 * Example: `!(i>5 || j==3)` => `[!(i==5 || j==3), i<=5, j!=3]`
44 *
45 * If `keep_composite_constraints` is true (default), a constraint
46 * that can be decomposed will be included in the output. If false,
47 * they will be excluded.
48 *
49 * Example, removing composite: `!(i>5 || j==3)` => `[i<=5, j!=3]`
50 *
51 * Intended for use in bounds analysis or simplification within a
52 * conditional, or identifying independent conditionals that may be
53 * hoisted.
54 *
55 * \param expr The expression to be analyzers
56 *
57 * \param keep_composite_constraints Whether to include composite
58 * constraints in the output.
59 *
60 * \returns A vector of independent constraints
61 */
62std::vector<PrimExpr> ExtractConstraints(const PrimExpr& expr,
63 bool keep_composite_constraints = true);
64
65/* \brief Returns components that are false if the expression is false.
66 *
67 * Utility to break up a boolean expression into independent
68 * components.
69 *
70 * Example: `i==5 || j==3` => `[i==5, j==3]`
71 * Example: `i==5 && j==3` => `[i==5 && j==3]`
72 * Example: `!(i>5 && j==3)` => `[i<=5, j!=3]`
73 *
74 * Intended for use in bounds analysis or simplification within a
75 * conditional, or identifying independent conditionals that may be
76 * hoisted.
77 *
78 * \param expr The expression to be analyzers
79 *
80 * \returns A vector of independent constraints
81 */
82std::vector<PrimExpr> ExtractComponents(const PrimExpr& expr);
83
84} // namespace arith
85} // namespace tvm
86
87#endif // TVM_ARITH_CONSTRAINT_EXTRACT_H_
88