20#include <mlir/Analysis/DataFlowFramework.h>
21#include <mlir/Dialect/Arith/IR/Arith.h>
22#include <mlir/Pass/AnalysisManager.h>
24#include <llvm/ADT/EquivalenceClasses.h>
26#include <unordered_set>
35 using IndexRange = std::pair<mlir::APInt, mlir::APInt>;
45 return std::holds_alternative<SymbolLookupResult<component::FieldDefOp>>(index);
48 ensure(
isField(),
"ConstrainRefIndex: field requested but not contained");
49 return std::get<SymbolLookupResult<component::FieldDefOp>>(index).get();
52 bool isIndex()
const {
return std::holds_alternative<mlir::APInt>(index); }
54 ensure(
isIndex(),
"ConstrainRefIndex: index requested but not contained");
55 return std::get<mlir::APInt>(index);
58 bool isIndexRange()
const {
return std::holds_alternative<IndexRange>(index); }
61 return std::get<IndexRange>(index);
65 void print(mlir::raw_ostream &os)
const;
76 return llvm::hash_value(c.
getIndex());
79 return llvm::hash_value(std::get<0>(r)) ^ llvm::hash_value(std::get<1>(r));
94 std::variant<SymbolLookupResult<component::FieldDefOp>, mlir::APInt, IndexRange> index;
97static inline mlir::raw_ostream &
operator<<(mlir::raw_ostream &os,
const ConstrainRefIndex &rhs) {
118 static std::vector<ConstrainRef> getAllConstrainRefs(
120 mlir::BlockArgument blockArg, std::vector<ConstrainRefIndex> fields
127 static std::vector<ConstrainRef> getAllConstrainRefs(
128 mlir::SymbolTableCollection &tables, mlir::ModuleOp
mod,
130 std::vector<ConstrainRefIndex> fields
134 static std::vector<ConstrainRef> getAllConstrainRefs(
135 mlir::SymbolTableCollection &tables, mlir::ModuleOp
mod, mlir::BlockArgument arg
143 : blockArg(b), fieldRefs(), constantVal(std::nullopt) {}
145 : blockArg(b), fieldRefs(std::move(f)), constantVal(std::nullopt) {}
148 : blockArg(nullptr), fieldRefs(), constantVal(c) {}
150 : blockArg(nullptr), fieldRefs(), constantVal(c) {}
155 return constantVal.has_value() && std::holds_alternative<felt::FeltConstantOp>(*constantVal);
158 return constantVal.has_value() &&
159 std::holds_alternative<mlir::arith::ConstantIndexOp>(*constantVal);
162 return constantVal.has_value() &&
163 std::holds_alternative<polymorphic::ConstReadOp>(*constantVal);
185 return std::get<felt::FeltConstantOp>(*constantVal).getValueAttr().getValue();
189 return toAPInt(std::get<mlir::arith::ConstantIndexOp>(*constantVal).value());
194 __FUNCTION__ + mlir::Twine(
" requires a constant int type!")
214 mlir::FailureOr<ConstrainRef>
221 return mlir::failure();
224 copy.fieldRefs.pop_back();
230 copy.fieldRefs.push_back(r);
241 const std::vector<ConstrainRefIndex> &
getPieces()
const {
return fieldRefs; }
243 void print(mlir::raw_ostream &os)
const;
264 mlir::BlockArgument blockArg;
266 std::vector<ConstrainRefIndex> fieldRefs;
268 mutable std::optional<
269 std::variant<felt::FeltConstantOp, mlir::arith::ConstantIndexOp, polymorphic::ConstReadOp>>
278 using Base = std::unordered_set<ConstrainRef, ConstrainRef::Hash>;
290 "ConstrainRefSet must satisfy the ScalarLatticeValue requirements"
297template <>
struct DenseMapInfo<
llzk::ConstrainRef> {
299 return llzk::ConstrainRef(mlir::BlockArgument(
reinterpret_cast<mlir::detail::ValueImpl *
>(1)));
302 return llzk::ConstrainRef(mlir::BlockArgument(
reinterpret_cast<mlir::detail::ValueImpl *
>(2)));
Defines an index into an LLZK object.
component::FieldDefOp getField() const
void print(mlir::raw_ostream &os) const
bool isIndexRange() const
ConstrainRefIndex(int64_t i)
ConstrainRefIndex(mlir::APInt i)
bool operator<(const ConstrainRefIndex &rhs) const
bool operator==(const ConstrainRefIndex &rhs) const
ConstrainRefIndex(SymbolLookupResult< component::FieldDefOp > f)
IndexRange getIndexRange() const
mlir::APInt getIndex() const
ConstrainRefIndex(IndexRange r)
ConstrainRefIndex(mlir::APInt low, mlir::APInt high)
bool operator>(const ConstrainRefIndex &rhs) const
ConstrainRefSet & join(const ConstrainRefSet &rhs)
friend mlir::raw_ostream & operator<<(mlir::raw_ostream &os, const ConstrainRefSet &rhs)
Defines a reference to a llzk object within a constrain function call.
mlir::APInt getConstantFeltValue() const
bool isTypeVarVal() const
const std::vector< ConstrainRefIndex > & getPieces() const
bool operator<(const ConstrainRef &rhs) const
ConstrainRef(felt::FeltConstantOp c)
bool isValidPrefix(const ConstrainRef &prefix) const
Returns true iff prefix is a valid prefix of this reference.
bool isIntegerVal() const
void print(mlir::raw_ostream &os) const
bool isConstantFelt() const
ConstrainRef createChild(ConstrainRef other) const
ConstrainRef(polymorphic::ConstReadOp c)
bool isTemplateConstant() const
ConstrainRef(mlir::BlockArgument b, std::vector< ConstrainRefIndex > f)
mlir::APInt getConstantIndexValue() const
bool isConstantIndex() const
ConstrainRef(mlir::BlockArgument b)
mlir::APInt getConstantInt() const
bool operator==(const ConstrainRef &rhs) const
mlir::FailureOr< ConstrainRef > getParentPrefix() const
Create a new reference that is the immediate prefix of this reference if possible.
ConstrainRef(mlir::arith::ConstantIndexOp c)
bool isBlockArgument() const
mlir::BlockArgument getBlockArgument() const
ConstrainRef createChild(ConstrainRefIndex r) const
bool operator!=(const ConstrainRef &rhs) const
mlir::FailureOr< ConstrainRef > translate(const ConstrainRef &prefix, const ConstrainRef &other) const
Create a new reference with prefix replaced with other iff prefix is a valid prefix for this referenc...
mlir::Type getType() const
bool operator>(const ConstrainRef &rhs) const
mlir::FailureOr< std::vector< ConstrainRefIndex > > getSuffix(const ConstrainRef &prefix) const
If prefix is a valid prefix of this reference, return the suffix that remains after removing the pref...
unsigned getInputNum() const
mlir::raw_ostream & operator<<(mlir::raw_ostream &os, const ConstrainRef &rhs)
llvm::APInt toAPInt(int64_t i)
void ensure(bool condition, llvm::Twine errMsg)
bool isSignalType(Type type)
ExpressionValue mod(llvm::SMTSolverRef solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
static bool isEqual(const llzk::ConstrainRef &lhs, const llzk::ConstrainRef &rhs)
static llzk::ConstrainRef getTombstoneKey()
static llzk::ConstrainRef getEmptyKey()
static unsigned getHashValue(const llzk::ConstrainRef &ref)
size_t operator()(const ConstrainRefIndex &c) const
size_t operator()(const ConstrainRef &val) const