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>;
46 return std::holds_alternative<SymbolLookupResult<component::FieldDefOp>>(index) ||
47 std::holds_alternative<component::FieldDefOp>(index);
50 ensure(
isField(),
"ConstrainRefIndex: field requested but not contained");
51 if (std::holds_alternative<component::FieldDefOp>(index)) {
52 return std::get<component::FieldDefOp>(index);
54 return std::get<SymbolLookupResult<component::FieldDefOp>>(index).get();
57 bool isIndex()
const {
return std::holds_alternative<mlir::APInt>(index); }
59 ensure(
isIndex(),
"ConstrainRefIndex: index requested but not contained");
60 return std::get<mlir::APInt>(index);
63 bool isIndexRange()
const {
return std::holds_alternative<IndexRange>(index); }
66 return std::get<IndexRange>(index);
70 void print(mlir::raw_ostream &os)
const;
78 return index == rhs.index;
103static inline mlir::raw_ostream &
operator<<(mlir::raw_ostream &os,
const ConstrainRefIndex &rhs) {
124 static std::vector<ConstrainRef> getAllConstrainRefs(
126 mlir::BlockArgument blockArg, std::vector<ConstrainRefIndex> fields
133 static std::vector<ConstrainRef> getAllConstrainRefs(
134 mlir::SymbolTableCollection &tables, mlir::ModuleOp
mod,
136 std::vector<ConstrainRefIndex> fields
141 static std::vector<ConstrainRef> getAllConstrainRefs(
142 mlir::SymbolTableCollection &tables, mlir::ModuleOp
mod, mlir::BlockArgument arg,
143 std::vector<ConstrainRefIndex> fields = {}
152 static std::vector<ConstrainRef>
156 : blockArg(b), fieldRefs(), constantVal(std::nullopt) {}
158 : blockArg(b), fieldRefs(std::move(f)), constantVal(std::nullopt) {}
161 : blockArg(nullptr), fieldRefs(), constantVal(c) {}
163 : blockArg(nullptr), fieldRefs(), constantVal(c) {}
168 return constantVal.has_value() && std::holds_alternative<felt::FeltConstantOp>(*constantVal);
171 return constantVal.has_value() &&
172 std::holds_alternative<mlir::arith::ConstantIndexOp>(*constantVal);
175 return constantVal.has_value() &&
176 std::holds_alternative<polymorphic::ConstReadOp>(*constantVal);
198 return std::get<felt::FeltConstantOp>(*constantVal).getValueAttr().getValue();
202 return toAPInt(std::get<mlir::arith::ConstantIndexOp>(*constantVal).value());
207 __FUNCTION__ + mlir::Twine(
" requires a constant int type!")
227 mlir::FailureOr<ConstrainRef>
234 return mlir::failure();
237 copy.fieldRefs.pop_back();
243 copy.fieldRefs.push_back(r);
254 const std::vector<ConstrainRefIndex> &
getPieces()
const {
return fieldRefs; }
256 void print(mlir::raw_ostream &os)
const;
277 mlir::BlockArgument blockArg;
279 std::vector<ConstrainRefIndex> fieldRefs;
281 mutable std::optional<
282 std::variant<felt::FeltConstantOp, mlir::arith::ConstantIndexOp, polymorphic::ConstReadOp>>
291 using Base = std::unordered_set<ConstrainRef, ConstrainRef::Hash>;
303 "ConstrainRefSet must satisfy the ScalarLatticeValue requirements"
310template <>
struct DenseMapInfo<
llzk::ConstrainRef> {
312 return llzk::ConstrainRef(mlir::BlockArgument(
reinterpret_cast<mlir::detail::ValueImpl *
>(1)));
315 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)
ConstrainRefIndex(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)
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
mlir::APInt getConstantValue() 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