14 auto testOperation = createIndexOperation();
19 mlirOperationDestroy(testOperation);
25 auto testOp = createIndexOperation();
31 MlirLocation location = mlirLocationUnknownGet(context);
32 auto dummyValue = mlirOperationGetResult(testOp, 0);
38 mlirOperationDestroy(testOp);
46 static std::unique_ptr<ContractEndOpBuildFuncHelper>
get();
58 auto testOperation = createIndexOperation();
63 mlirOperationDestroy(testOperation);
67 auto testOp = createIndexOperation();
73 mlirOperationDestroy(testOp);
77 auto testOp = createIndexOperation();
83 mlirOperationDestroy(testOp);
87 auto testOp = createIndexOperation();
93 mlirOperationDestroy(testOp);
97 auto testOp = createIndexOperation();
103 mlirOperationDestroy(testOp);
107 auto testOp = createIndexOperation();
113 mlirOperationDestroy(testOp);
117 auto testOp = createIndexOperation();
123 mlirOperationDestroy(testOp);
127 auto testOp = createIndexOperation();
133 mlirOperationDestroy(testOp);
137 auto testOp = createIndexOperation();
143 mlirOperationDestroy(testOp);
147 auto testOp = createIndexOperation();
153 mlirOperationDestroy(testOp);
158 auto testOperation = createIndexOperation();
165 mlirOperationDestroy(testOperation);
170 auto testOperation = createIndexOperation();
178 mlirOperationDestroy(testOperation);
183 auto testOperation = createIndexOperation();
190 mlirOperationDestroy(testOperation);
195 auto testOperation = createIndexOperation();
202 mlirOperationDestroy(testOperation);
207 auto testOperation = createIndexOperation();
214 mlirOperationDestroy(testOperation);
219 auto testOperation = createIndexOperation();
227 mlirOperationDestroy(testOperation);
232 auto testOperation = createIndexOperation();
235 bool requireParent =
false;
240 mlirOperationDestroy(testOperation);
245 auto testOperation = createIndexOperation();
250 mlirOperationDestroy(testOperation);
256 auto testOp = createIndexOperation();
262 MlirLocation location = mlirLocationUnknownGet(context);
263 auto dummyValue = mlirOperationGetResult(testOp, 0);
269 mlirOperationDestroy(testOp);
277 static std::unique_ptr<DecreasesOpBuildFuncHelper>
get();
288 auto testOp = createIndexOperation();
294 mlirOperationDestroy(testOp);
298 auto testOp = createIndexOperation();
301 auto dummyValue = mlirOperationGetResult(testOp, 0);
305 mlirOperationDestroy(testOp);
310 auto testOperation = createIndexOperation();
315 mlirOperationDestroy(testOperation);
321 auto testOp = createIndexOperation();
327 MlirLocation location = mlirLocationUnknownGet(context);
328 auto dummyValue = mlirOperationGetResult(testOp, 0);
334 mlirOperationDestroy(testOp);
342 static std::unique_ptr<EnsureComputeOpBuildFuncHelper>
get();
353 auto testOp = createIndexOperation();
359 mlirOperationDestroy(testOp);
363 auto testOp = createIndexOperation();
366 auto dummyValue = mlirOperationGetResult(testOp, 0);
370 mlirOperationDestroy(testOp);
375 auto testOperation = createIndexOperation();
380 mlirOperationDestroy(testOperation);
386 auto testOp = createIndexOperation();
392 MlirLocation location = mlirLocationUnknownGet(context);
393 auto dummyValue = mlirOperationGetResult(testOp, 0);
399 mlirOperationDestroy(testOp);
407 static std::unique_ptr<EnsureConstrainOpBuildFuncHelper>
get();
418 auto testOp = createIndexOperation();
424 mlirOperationDestroy(testOp);
428 auto testOp = createIndexOperation();
431 auto dummyValue = mlirOperationGetResult(testOp, 0);
435 mlirOperationDestroy(testOp);
440 auto testOperation = createIndexOperation();
445 mlirOperationDestroy(testOperation);
449 auto testOp = createIndexOperation();
455 mlirOperationDestroy(testOp);
459 auto testOp = createIndexOperation();
465 mlirOperationDestroy(testOp);
469 auto testOp = createIndexOperation();
472 auto dummyValue = mlirOperationGetResult(testOp, 0);
473 MlirValue values[] = {dummyValue};
477 mlirOperationDestroy(testOp);
481 auto testOp = createIndexOperation();
487 mlirOperationDestroy(testOp);
491 auto testOp = createIndexOperation();
497 mlirOperationDestroy(testOp);
501 auto testOp = createIndexOperation();
504 auto dummyValue = mlirOperationGetResult(testOp, 0);
506 groups[0].
values = &dummyValue;
511 mlirOperationDestroy(testOp);
515 auto testOp = createIndexOperation();
521 mlirOperationDestroy(testOp);
525 auto testOp = createIndexOperation();
531 mlirOperationDestroy(testOp);
535 auto testOp = createIndexOperation();
541 mlirOperationDestroy(testOp);
545 auto testOp = createIndexOperation();
551 mlirOperationDestroy(testOp);
555 auto testOp = createIndexOperation();
561 mlirOperationDestroy(testOp);
565 auto testOp = createIndexOperation();
571 mlirOperationDestroy(testOp);
575 auto testOp = createIndexOperation();
581 mlirOperationDestroy(testOp);
585 auto testOp = createIndexOperation();
591 mlirOperationDestroy(testOp);
596 auto testOperation = createIndexOperation();
603 mlirOperationDestroy(testOperation);
608 auto testOperation = createIndexOperation();
615 mlirOperationDestroy(testOperation);
620 auto testOperation = createIndexOperation();
627 mlirOperationDestroy(testOperation);
632 auto testOperation = createIndexOperation();
639 mlirOperationDestroy(testOperation);
644 auto testOperation = createIndexOperation();
649 mlirOperationDestroy(testOperation);
655 auto testOp = createIndexOperation();
661 MlirLocation location = mlirLocationUnknownGet(context);
662 auto dummyValue = mlirOperationGetResult(testOp, 0);
668 mlirOperationDestroy(testOp);
676 static std::unique_ptr<IncreasesOpBuildFuncHelper>
get();
687 auto testOp = createIndexOperation();
693 mlirOperationDestroy(testOp);
697 auto testOp = createIndexOperation();
700 auto dummyValue = mlirOperationGetResult(testOp, 0);
704 mlirOperationDestroy(testOp);
709 auto testOperation = createIndexOperation();
714 mlirOperationDestroy(testOperation);
718 auto testOp = createIndexOperation();
724 mlirOperationDestroy(testOp);
728 auto testOp = createIndexOperation();
734 mlirOperationDestroy(testOp);
738 auto testOp = createIndexOperation();
744 mlirOperationDestroy(testOp);
748 auto testOp = createIndexOperation();
754 mlirOperationDestroy(testOp);
758 auto testOp = createIndexOperation();
764 mlirOperationDestroy(testOp);
769 auto testOperation = createIndexOperation();
776 mlirOperationDestroy(testOperation);
781 auto testOperation = createIndexOperation();
786 mlirOperationDestroy(testOperation);
792 auto testOp = createIndexOperation();
798 MlirLocation location = mlirLocationUnknownGet(context);
799 auto dummyValue = mlirOperationGetResult(testOp, 0);
805 mlirOperationDestroy(testOp);
813 static std::unique_ptr<OldOpBuildFuncHelper>
get();
824 auto testOp = createIndexOperation();
830 mlirOperationDestroy(testOp);
834 auto testOp = createIndexOperation();
837 auto dummyValue = mlirOperationGetResult(testOp, 0);
841 mlirOperationDestroy(testOp);
845 auto testOp = createIndexOperation();
851 mlirOperationDestroy(testOp);
856 auto testOperation = createIndexOperation();
861 mlirOperationDestroy(testOperation);
867 auto testOp = createIndexOperation();
873 MlirLocation location = mlirLocationUnknownGet(context);
874 auto dummyValue = mlirOperationGetResult(testOp, 0);
880 mlirOperationDestroy(testOp);
888 static std::unique_ptr<RequireComputeOpBuildFuncHelper>
get();
899 auto testOp = createIndexOperation();
905 mlirOperationDestroy(testOp);
909 auto testOp = createIndexOperation();
912 auto dummyValue = mlirOperationGetResult(testOp, 0);
916 mlirOperationDestroy(testOp);
921 auto testOperation = createIndexOperation();
926 mlirOperationDestroy(testOperation);
932 auto testOp = createIndexOperation();
938 MlirLocation location = mlirLocationUnknownGet(context);
939 auto dummyValue = mlirOperationGetResult(testOp, 0);
945 mlirOperationDestroy(testOp);
953 static std::unique_ptr<RequireConstrainOpBuildFuncHelper>
get();
964 auto testOp = createIndexOperation();
970 mlirOperationDestroy(testOp);
974 auto testOp = createIndexOperation();
977 auto dummyValue = mlirOperationGetResult(testOp, 0);
981 mlirOperationDestroy(testOp);
986 auto testOperation = createIndexOperation();
991 mlirOperationDestroy(testOperation);
997 auto testOp = createIndexOperation();
1003 MlirLocation location = mlirLocationUnknownGet(context);
1004 auto dummyValue = mlirOperationGetResult(testOp, 0);
1010 mlirOperationDestroy(testOp);
1018 static std::unique_ptr<StepOpBuildFuncHelper>
get();
1029 auto testOp = createIndexOperation();
1035 mlirOperationDestroy(testOp);
1040 auto testOperation = createIndexOperation();
1045 mlirOperationDestroy(testOperation);
1051 auto testOp = createIndexOperation();
1057 MlirLocation location = mlirLocationUnknownGet(context);
1058 auto dummyValue = mlirOperationGetResult(testOp, 0);
1064 mlirOperationDestroy(testOp);
1072 static std::unique_ptr<StepYieldOpBuildFuncHelper>
get();
1083 auto testOp = createIndexOperation();
1089 mlirOperationDestroy(testOp);
1093 auto testOp = createIndexOperation();
1096 auto dummyValue = mlirOperationGetResult(testOp, 0);
1100 mlirOperationDestroy(testOp);
1105 auto testOperation = createIndexOperation();
1110 mlirOperationDestroy(testOperation);
1116 auto testOp = createIndexOperation();
1122 MlirLocation location = mlirLocationUnknownGet(context);
1123 auto dummyValue = mlirOperationGetResult(testOp, 0);
1129 mlirOperationDestroy(testOp);
1137 static std::unique_ptr<VerifAssertOpBuildFuncHelper>
get();
1148 auto testOp = createIndexOperation();
1154 mlirOperationDestroy(testOp);
1158 auto testOp = createIndexOperation();
1161 auto dummyValue = mlirOperationGetResult(testOp, 0);
1165 mlirOperationDestroy(testOp);
1170 auto testOperation = createIndexOperation();
1175 mlirOperationDestroy(testOperation);
1181 auto testOp = createIndexOperation();
1187 MlirLocation location = mlirLocationUnknownGet(context);
1188 auto dummyValue = mlirOperationGetResult(testOp, 0);
1194 mlirOperationDestroy(testOp);
1202 static std::unique_ptr<VerifProveOpBuildFuncHelper>
get();
1213 auto testOp = createIndexOperation();
1219 mlirOperationDestroy(testOp);
1223 auto testOp = createIndexOperation();
1226 auto dummyValue = mlirOperationGetResult(testOp, 0);
1230 mlirOperationDestroy(testOp);
1235 auto testOperation = createIndexOperation();
1240 mlirOperationDestroy(testOperation);
1246 auto testOp = createIndexOperation();
1252 MlirLocation location = mlirLocationUnknownGet(context);
1253 auto dummyValue = mlirOperationGetResult(testOp, 0);
1259 mlirOperationDestroy(testOp);
1267 static std::unique_ptr<VerifSMTProveOpBuildFuncHelper>
get();
1278 auto testOp = createIndexOperation();
1284 mlirOperationDestroy(testOp);
1288 auto testOp = createIndexOperation();
1291 auto dummyValue = mlirOperationGetResult(testOp, 0);
1295 mlirOperationDestroy(testOp);
TEST_F(ArrayOperationLinkTests, IsA_Array_ArrayLengthOp)
This test ensures llzkOperationIsA_Array_ArrayLengthOp links properly.
MlirOpBuilder mlirOpBuilderCreate(MlirContext ctx)
Creates a new OpBuilder for the given MLIR context.
MlirValue llzkVerif_OldOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::OldOp Operation.
MlirAttribute llzkVerif_IncludeOpGetNumDimsPerMap(MlirOperation op)
Get NumDimsPerMap attribute from llzk::verif::IncludeOp Operation.
intptr_t llzkVerif_IncludeOpGetMapOperandsCount(MlirOperation op)
Get number of MapOperands operands in llzk::verif::IncludeOp Operation.
void llzkVerif_StepYieldOpSetValue(MlirOperation op, MlirValue value)
Set Value operand of llzk::verif::StepYieldOp Operation.
void llzkVerif_VerifAssertOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::VerifAssertOp Operation.
void llzkVerif_IncludeOpSetTemplateParams(MlirOperation op, MlirAttribute attr)
Set TemplateParams attribute of llzk::verif::IncludeOp Operation.
void llzkVerif_IncludeOpSetMapOpGroupSizes(MlirOperation op, MlirAttribute attr)
Set MapOpGroupSizes attribute of llzk::verif::IncludeOp Operation.
MlirValue llzkVerif_VerifProveOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::VerifProveOp Operation.
void llzkVerif_VerifProveOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::VerifProveOp Operation.
MlirOperation llzkVerif_RequireComputeOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::RequireComputeOp Operation.
void llzkVerif_IncludeOpSetCallee(MlirOperation op, MlirAttribute attr)
Set Callee attribute of llzk::verif::IncludeOp Operation.
MlirOperation llzkVerif_RequireConstrainOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::RequireConstrainOp Operation.
bool llzkVerif_ContractOpHasStructTarget(MlirOperation inp)
Return true iff the contract targets a struct type.
void llzkVerif_RequireConstrainOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::RequireConstrainOp Operation.
MlirValue llzkVerif_VerifSMTProveOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::VerifSMTProveOp Operation.
MlirRegion llzkVerif_ContractOpGetBody(MlirOperation op)
Get Body region from llzk::verif::ContractOp Operation.
MlirAttribute llzkVerif_IncludeOpGetTemplateParams(MlirOperation op)
Get TemplateParams attribute from llzk::verif::IncludeOp Operation.
MlirOperation llzkVerif_StepOpBuild(MlirOpBuilder builder, MlirLocation location)
Build a llzk::verif::StepOp Operation.
bool llzkOperationIsA_Verif_RequireConstrainOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::RequireConstrainOp.
MlirOperation llzkVerif_EnsureConstrainOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::EnsureConstrainOp Operation.
MlirAttribute llzkVerif_IncludeOpGetMapOpGroupSizes(MlirOperation op)
Get MapOpGroupSizes attribute from llzk::verif::IncludeOp Operation.
bool llzkOperationIsA_Verif_VerifSMTProveOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::VerifSMTProveOp.
MlirOperation llzkVerif_ContractEndOpBuild(MlirOpBuilder builder, MlirLocation location)
Build a llzk::verif::ContractEndOp Operation.
void llzkVerif_EnsureComputeOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::EnsureComputeOp Operation.
MlirValue llzkVerif_StepYieldOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::StepYieldOp Operation.
MlirOperation llzkVerif_VerifProveOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::VerifProveOp Operation.
MlirOperation llzkVerif_VerifSMTProveOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::VerifSMTProveOp Operation.
MlirAttribute llzkVerif_InvariantOpGetLoopName(MlirOperation op)
Get LoopName attribute from llzk::verif::InvariantOp Operation.
bool llzkVerif_ContractOpHasArgPublicAttr(MlirOperation inp, unsigned index)
Return true iff the argument at the given index has pub attribute.
bool llzkOperationIsA_Verif_ContractEndOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::ContractEndOp.
MlirRegion llzkVerif_StepOpGetRegion(MlirOperation op)
Get Region region from llzk::verif::StepOp Operation.
intptr_t llzkVerif_IncludeOpGetArgOperandsCount(MlirOperation op)
Get number of ArgOperands operands in llzk::verif::IncludeOp Operation.
bool llzkOperationIsA_Verif_DecreasesOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::DecreasesOp.
bool llzkOperationIsA_Verif_StepYieldOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::StepYieldOp.
bool llzkOperationIsA_Verif_InvariantOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::InvariantOp.
MlirAttribute llzkVerif_ContractOpGetSymName(MlirOperation op)
Get SymName attribute from llzk::verif::ContractOp Operation.
void llzkVerif_IncreasesOpSetValue(MlirOperation op, MlirValue value)
Set Value operand of llzk::verif::IncreasesOp Operation.
MlirValue llzkVerif_VerifAssertOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::VerifAssertOp Operation.
MlirOperation llzkVerif_IncreasesOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value)
Build a llzk::verif::IncreasesOp Operation.
MlirAttribute llzkVerif_InvariantOpGetLoopArgTypes(MlirOperation op)
Get LoopArgTypes attribute from llzk::verif::InvariantOp Operation.
MlirOperation llzkVerif_OldOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value)
Build a llzk::verif::OldOp Operation.
void llzkVerif_VerifSMTProveOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::VerifSMTProveOp Operation.
bool llzkVerif_ContractOpHasArgName(MlirOperation inp, unsigned index)
Return true iff the argument at the given index has a function.arg_name attribute.
bool llzkVerif_IncludeOpContractTargetsStruct(MlirOperation inp)
Return true iff the contract targets a struct type.
bool llzkOperationIsA_Verif_RequireComputeOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::RequireComputeOp.
MlirAttribute llzkVerif_ContractOpGetTarget(MlirOperation op)
Get Target attribute from llzk::verif::ContractOp Operation.
MlirAttribute llzkVerif_ContractOpGetFunctionType(MlirOperation op)
Get FunctionType attribute from llzk::verif::ContractOp Operation.
bool llzkOperationIsA_Verif_EnsureConstrainOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::EnsureConstrainOp.
MlirAttribute llzkVerif_ContractOpGetArgAttrs(MlirOperation op)
Get ArgAttrs attribute from llzk::verif::ContractOp Operation.
bool llzkOperationIsA_Verif_EnsureComputeOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::EnsureComputeOp.
void llzkVerif_IncludeOpSetArgOperands(MlirOperation op, intptr_t count, MlirValue const *values)
Set ArgOperands operands of llzk::verif::IncludeOp Operation.
MlirOperation llzkVerif_DecreasesOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value)
Build a llzk::verif::DecreasesOp Operation.
void llzkVerif_IncludeOpSetNumDimsPerMap(MlirOperation op, MlirAttribute attr)
Set NumDimsPerMap attribute of llzk::verif::IncludeOp Operation.
void llzkVerif_ContractOpSetTarget(MlirOperation op, MlirAttribute attr)
Set Target attribute of llzk::verif::ContractOp Operation.
void llzkVerif_EnsureConstrainOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::EnsureConstrainOp Operation.
MlirAttribute llzkVerif_IncludeOpGetCallee(MlirOperation op)
Get Callee attribute from llzk::verif::IncludeOp Operation.
bool llzkVerif_ContractOpIsDeclaration(MlirOperation inp)
Required by SymbolOpInterface.
MlirOperation llzkVerif_InvariantOpGetParentContract(MlirOperation inp)
Returns the contract operation that contains this invariant.
MlirOperation llzkVerif_StepYieldOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue value)
Build a llzk::verif::StepYieldOp Operation.
MlirValue llzkVerif_IncludeOpGetMapOperandsAt(MlirOperation op, intptr_t index)
Get MapOperands operand at index from llzk::verif::IncludeOp Operation.
void llzkVerif_ContractOpSetArgAttrs(MlirOperation op, MlirAttribute attr)
Set ArgAttrs attribute of llzk::verif::ContractOp Operation.
void llzkVerif_InvariantOpSetLoopName(MlirOperation op, MlirAttribute attr)
Set LoopName attribute of llzk::verif::InvariantOp Operation.
MlirOperation llzkVerif_EnsureComputeOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::EnsureComputeOp Operation.
MlirValue llzkVerif_RequireComputeOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::RequireComputeOp Operation.
bool llzkOperationIsA_Verif_IncludeOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::IncludeOp.
void llzkVerif_InvariantOpSetLoopArgTypes(MlirOperation op, MlirAttribute attr)
Set LoopArgTypes attribute of llzk::verif::InvariantOp Operation.
MlirValue llzkVerif_IncludeOpGetArgOperandsAt(MlirOperation op, intptr_t index)
Get ArgOperands operand at index from llzk::verif::IncludeOp Operation.
void llzkVerif_RequireComputeOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::RequireComputeOp Operation.
void llzkVerif_IncludeOpSetMapOperands(MlirOperation op, intptr_t groupCount, MlirValueRange const *groups)
Set MapOperands operand groups of llzk::verif::IncludeOp Operation.
bool llzkOperationIsA_Verif_IncreasesOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::IncreasesOp.
bool llzkOperationIsA_Verif_StepOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::StepOp.
void llzkVerif_DecreasesOpSetValue(MlirOperation op, MlirValue value)
Set Value operand of llzk::verif::DecreasesOp Operation.
MlirRegion llzkVerif_InvariantOpGetRegion(MlirOperation op)
Get Region region from llzk::verif::InvariantOp Operation.
MlirValue llzkVerif_IncludeOpGetSelfValue(MlirOperation inp)
Return the "self" value (i.e.
MlirValue llzkVerif_IncreasesOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::IncreasesOp Operation.
MlirType llzkVerif_IncludeOpGetTypeSignature(MlirOperation inp)
Return the FunctionType inferred from the arg operands of this CallOp.
void llzkVerif_OldOpSetValue(MlirOperation op, MlirValue value)
Set Value operand of llzk::verif::OldOp Operation.
MlirValue llzkVerif_EnsureComputeOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::EnsureComputeOp Operation.
bool llzkOperationIsA_Verif_VerifAssertOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::VerifAssertOp.
MlirValue llzkVerif_EnsureConstrainOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::EnsureConstrainOp Operation.
MlirRegion llzkVerif_ContractOpGetCallableRegion(MlirOperation inp)
Required by FunctionOpInterface.
bool llzkOperationIsA_Verif_VerifProveOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::VerifProveOp.
MlirValue llzkVerif_RequireConstrainOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::RequireConstrainOp Operation.
bool llzkVerif_ContractOpHasFuncTarget(MlirOperation inp)
Return true iff the contract targets a function.
MlirOperation llzkVerif_VerifAssertOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::VerifAssertOp Operation.
bool llzkOperationIsA_Verif_ContractOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::ContractOp.
MlirAttribute llzkVerif_ContractOpGetFullyQualifiedName(MlirOperation inp, bool requireParent)
Return the full name for this contract from the root module, including all surrounding symbol table n...
MlirValue llzkVerif_OldOpGetResult(MlirOperation op)
Get Result result from llzk::verif::OldOp Operation.
void llzkVerif_ContractOpSetFunctionType(MlirOperation op, MlirAttribute attr)
Set FunctionType attribute of llzk::verif::ContractOp Operation.
MlirValue llzkVerif_DecreasesOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::DecreasesOp Operation.
void llzkVerif_ContractOpSetSymName(MlirOperation op, MlirAttribute attr)
Set SymName attribute of llzk::verif::ContractOp Operation.
bool llzkOperationIsA_Verif_OldOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::OldOp.
MlirOperation llzkVerif_IncludeOpResolveCallable(MlirOperation inp)
Required by CallOpInterface.
static std::unique_ptr< ContractEndOpBuildFuncHelper > get()
This method must be implemented to return a subclass of ContractEndOpBuildFuncHelper that at least im...
virtual bool callIsA(MlirOperation op) override
ContractEndOpBuildFuncHelper()=default
DecreasesOpBuildFuncHelper()=default
virtual bool callIsA(MlirOperation op) override
static std::unique_ptr< DecreasesOpBuildFuncHelper > get()
This method must be implemented to return a subclass of DecreasesOpBuildFuncHelper that at least impl...
static std::unique_ptr< EnsureComputeOpBuildFuncHelper > get()
This method must be implemented to return a subclass of EnsureComputeOpBuildFuncHelper that at least ...
virtual bool callIsA(MlirOperation op) override
EnsureComputeOpBuildFuncHelper()=default
EnsureConstrainOpBuildFuncHelper()=default
virtual bool callIsA(MlirOperation op) override
static std::unique_ptr< EnsureConstrainOpBuildFuncHelper > get()
This method must be implemented to return a subclass of EnsureConstrainOpBuildFuncHelper that at leas...
virtual bool callIsA(MlirOperation op) override
IncreasesOpBuildFuncHelper()=default
static std::unique_ptr< IncreasesOpBuildFuncHelper > get()
This method must be implemented to return a subclass of IncreasesOpBuildFuncHelper that at least impl...
Representation of an mlir::ValueRange
MlirValue const * values
Pointer to the first value in the range.
intptr_t size
Number of values in the range.
OldOpBuildFuncHelper()=default
virtual bool callIsA(MlirOperation op) override
static std::unique_ptr< OldOpBuildFuncHelper > get()
This method must be implemented to return a subclass of OldOpBuildFuncHelper that at least implements...
virtual bool callIsA(MlirOperation op) override
RequireComputeOpBuildFuncHelper()=default
static std::unique_ptr< RequireComputeOpBuildFuncHelper > get()
This method must be implemented to return a subclass of RequireComputeOpBuildFuncHelper that at least...
RequireConstrainOpBuildFuncHelper()=default
virtual bool callIsA(MlirOperation op) override
static std::unique_ptr< RequireConstrainOpBuildFuncHelper > get()
This method must be implemented to return a subclass of RequireConstrainOpBuildFuncHelper that at lea...
static std::unique_ptr< StepOpBuildFuncHelper > get()
This method must be implemented to return a subclass of StepOpBuildFuncHelper that at least implement...
StepOpBuildFuncHelper()=default
virtual bool callIsA(MlirOperation op) override
static std::unique_ptr< StepYieldOpBuildFuncHelper > get()
This method must be implemented to return a subclass of StepYieldOpBuildFuncHelper that at least impl...
virtual bool callIsA(MlirOperation op) override
StepYieldOpBuildFuncHelper()=default
virtual bool callIsA(MlirOperation op) override
VerifAssertOpBuildFuncHelper()=default
static std::unique_ptr< VerifAssertOpBuildFuncHelper > get()
This method must be implemented to return a subclass of VerifAssertOpBuildFuncHelper that at least im...
static std::unique_ptr< VerifProveOpBuildFuncHelper > get()
This method must be implemented to return a subclass of VerifProveOpBuildFuncHelper that at least imp...
VerifProveOpBuildFuncHelper()=default
virtual bool callIsA(MlirOperation op) override
VerifSMTProveOpBuildFuncHelper()=default
virtual bool callIsA(MlirOperation op) override
static std::unique_ptr< VerifSMTProveOpBuildFuncHelper > get()
This method must be implemented to return a subclass of VerifSMTProveOpBuildFuncHelper that at least ...