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<AssumeDetOpBuildFuncHelper>
get();
57 auto testOp = createIndexOperation();
63 mlirOperationDestroy(testOp);
67 auto testOp = createIndexOperation();
70 auto dummyValue = mlirOperationGetResult(testOp, 0);
74 mlirOperationDestroy(testOp);
79 auto testOperation = createIndexOperation();
84 mlirOperationDestroy(testOperation);
90 auto testOp = createIndexOperation();
96 MlirLocation location = mlirLocationUnknownGet(context);
97 auto dummyValue = mlirOperationGetResult(testOp, 0);
103 mlirOperationDestroy(testOp);
111 static std::unique_ptr<ContractEndOpBuildFuncHelper>
get();
123 auto testOperation = createIndexOperation();
128 mlirOperationDestroy(testOperation);
132 auto testOp = createIndexOperation();
138 mlirOperationDestroy(testOp);
142 auto testOp = createIndexOperation();
148 mlirOperationDestroy(testOp);
152 auto testOp = createIndexOperation();
158 mlirOperationDestroy(testOp);
162 auto testOp = createIndexOperation();
168 mlirOperationDestroy(testOp);
172 auto testOp = createIndexOperation();
178 mlirOperationDestroy(testOp);
182 auto testOp = createIndexOperation();
188 mlirOperationDestroy(testOp);
192 auto testOp = createIndexOperation();
198 mlirOperationDestroy(testOp);
202 auto testOp = createIndexOperation();
208 mlirOperationDestroy(testOp);
212 auto testOp = createIndexOperation();
218 mlirOperationDestroy(testOp);
222 auto testOp = createIndexOperation();
228 mlirOperationDestroy(testOp);
232 auto testOp = createIndexOperation();
238 mlirOperationDestroy(testOp);
243 auto testOperation = createIndexOperation();
250 mlirOperationDestroy(testOperation);
255 auto testOperation = createIndexOperation();
263 mlirOperationDestroy(testOperation);
268 auto testOperation = createIndexOperation();
275 mlirOperationDestroy(testOperation);
280 auto testOperation = createIndexOperation();
287 mlirOperationDestroy(testOperation);
292 auto testOperation = createIndexOperation();
299 mlirOperationDestroy(testOperation);
304 auto testOperation = createIndexOperation();
312 mlirOperationDestroy(testOperation);
317 auto testOperation = createIndexOperation();
320 bool requireParent =
false;
325 mlirOperationDestroy(testOperation);
330 auto testOperation = createIndexOperation();
335 mlirOperationDestroy(testOperation);
341 auto testOp = createIndexOperation();
347 MlirLocation location = mlirLocationUnknownGet(context);
348 auto dummyValue = mlirOperationGetResult(testOp, 0);
354 mlirOperationDestroy(testOp);
362 static std::unique_ptr<DecreasesOpBuildFuncHelper>
get();
373 auto testOp = createIndexOperation();
379 mlirOperationDestroy(testOp);
383 auto testOp = createIndexOperation();
386 auto dummyValue = mlirOperationGetResult(testOp, 0);
390 mlirOperationDestroy(testOp);
395 auto testOperation = createIndexOperation();
400 mlirOperationDestroy(testOperation);
406 auto testOp = createIndexOperation();
412 MlirLocation location = mlirLocationUnknownGet(context);
413 auto dummyValue = mlirOperationGetResult(testOp, 0);
419 mlirOperationDestroy(testOp);
427 static std::unique_ptr<EnsureComputeOpBuildFuncHelper>
get();
438 auto testOp = createIndexOperation();
444 mlirOperationDestroy(testOp);
448 auto testOp = createIndexOperation();
451 auto dummyValue = mlirOperationGetResult(testOp, 0);
455 mlirOperationDestroy(testOp);
460 auto testOperation = createIndexOperation();
465 mlirOperationDestroy(testOperation);
471 auto testOp = createIndexOperation();
477 MlirLocation location = mlirLocationUnknownGet(context);
478 auto dummyValue = mlirOperationGetResult(testOp, 0);
484 mlirOperationDestroy(testOp);
492 static std::unique_ptr<EnsureConstrainOpBuildFuncHelper>
get();
503 auto testOp = createIndexOperation();
509 mlirOperationDestroy(testOp);
513 auto testOp = createIndexOperation();
516 auto dummyValue = mlirOperationGetResult(testOp, 0);
520 mlirOperationDestroy(testOp);
525 auto testOperation = createIndexOperation();
530 mlirOperationDestroy(testOperation);
534 auto testOp = createIndexOperation();
540 mlirOperationDestroy(testOp);
544 auto testOp = createIndexOperation();
550 mlirOperationDestroy(testOp);
554 auto testOp = createIndexOperation();
557 auto dummyValue = mlirOperationGetResult(testOp, 0);
558 MlirValue values[] = {dummyValue};
562 mlirOperationDestroy(testOp);
566 auto testOp = createIndexOperation();
572 mlirOperationDestroy(testOp);
576 auto testOp = createIndexOperation();
582 mlirOperationDestroy(testOp);
586 auto testOp = createIndexOperation();
589 auto dummyValue = mlirOperationGetResult(testOp, 0);
591 groups[0].
values = &dummyValue;
596 mlirOperationDestroy(testOp);
600 auto testOp = createIndexOperation();
606 mlirOperationDestroy(testOp);
610 auto testOp = createIndexOperation();
616 mlirOperationDestroy(testOp);
620 auto testOp = createIndexOperation();
626 mlirOperationDestroy(testOp);
630 auto testOp = createIndexOperation();
636 mlirOperationDestroy(testOp);
640 auto testOp = createIndexOperation();
646 mlirOperationDestroy(testOp);
650 auto testOp = createIndexOperation();
656 mlirOperationDestroy(testOp);
660 auto testOp = createIndexOperation();
666 mlirOperationDestroy(testOp);
670 auto testOp = createIndexOperation();
676 mlirOperationDestroy(testOp);
680 auto testOp = createIndexOperation();
686 mlirOperationDestroy(testOp);
690 auto testOp = createIndexOperation();
696 mlirOperationDestroy(testOp);
700 auto testOp = createIndexOperation();
706 mlirOperationDestroy(testOp);
710 auto testOp = createIndexOperation();
716 mlirOperationDestroy(testOp);
721 auto testOperation = createIndexOperation();
728 mlirOperationDestroy(testOperation);
733 auto testOperation = createIndexOperation();
740 mlirOperationDestroy(testOperation);
745 auto testOperation = createIndexOperation();
752 mlirOperationDestroy(testOperation);
757 auto testOperation = createIndexOperation();
762 mlirOperationDestroy(testOperation);
768 auto testOp = createIndexOperation();
774 MlirLocation location = mlirLocationUnknownGet(context);
775 auto dummyValue = mlirOperationGetResult(testOp, 0);
781 mlirOperationDestroy(testOp);
789 static std::unique_ptr<IncreasesOpBuildFuncHelper>
get();
800 auto testOp = createIndexOperation();
806 mlirOperationDestroy(testOp);
810 auto testOp = createIndexOperation();
813 auto dummyValue = mlirOperationGetResult(testOp, 0);
817 mlirOperationDestroy(testOp);
822 auto testOperation = createIndexOperation();
827 mlirOperationDestroy(testOperation);
831 auto testOp = createIndexOperation();
837 mlirOperationDestroy(testOp);
841 auto testOp = createIndexOperation();
847 mlirOperationDestroy(testOp);
851 auto testOp = createIndexOperation();
857 mlirOperationDestroy(testOp);
861 auto testOp = createIndexOperation();
867 mlirOperationDestroy(testOp);
871 auto testOp = createIndexOperation();
877 mlirOperationDestroy(testOp);
882 auto testOperation = createIndexOperation();
889 mlirOperationDestroy(testOperation);
894 auto testOperation = createIndexOperation();
899 mlirOperationDestroy(testOperation);
905 auto testOp = createIndexOperation();
911 MlirLocation location = mlirLocationUnknownGet(context);
912 auto dummyValue = mlirOperationGetResult(testOp, 0);
918 mlirOperationDestroy(testOp);
926 static std::unique_ptr<OldOpBuildFuncHelper>
get();
937 auto testOp = createIndexOperation();
943 mlirOperationDestroy(testOp);
947 auto testOp = createIndexOperation();
950 auto dummyValue = mlirOperationGetResult(testOp, 0);
954 mlirOperationDestroy(testOp);
958 auto testOp = createIndexOperation();
964 mlirOperationDestroy(testOp);
969 auto testOperation = createIndexOperation();
974 mlirOperationDestroy(testOperation);
980 auto testOp = createIndexOperation();
986 MlirLocation location = mlirLocationUnknownGet(context);
987 auto dummyValue = mlirOperationGetResult(testOp, 0);
993 mlirOperationDestroy(testOp);
1001 static std::unique_ptr<ProveDetOpBuildFuncHelper>
get();
1012 auto testOp = createIndexOperation();
1018 mlirOperationDestroy(testOp);
1022 auto testOp = createIndexOperation();
1025 auto dummyValue = mlirOperationGetResult(testOp, 0);
1029 mlirOperationDestroy(testOp);
1033 auto testOp = createIndexOperation();
1039 mlirOperationDestroy(testOp);
1044 auto testOperation = createIndexOperation();
1049 mlirOperationDestroy(testOperation);
1055 auto testOp = createIndexOperation();
1061 MlirLocation location = mlirLocationUnknownGet(context);
1062 auto dummyValue = mlirOperationGetResult(testOp, 0);
1068 mlirOperationDestroy(testOp);
1076 static std::unique_ptr<RequireComputeOpBuildFuncHelper>
get();
1087 auto testOp = createIndexOperation();
1093 mlirOperationDestroy(testOp);
1097 auto testOp = createIndexOperation();
1100 auto dummyValue = mlirOperationGetResult(testOp, 0);
1104 mlirOperationDestroy(testOp);
1109 auto testOperation = createIndexOperation();
1114 mlirOperationDestroy(testOperation);
1120 auto testOp = createIndexOperation();
1126 MlirLocation location = mlirLocationUnknownGet(context);
1127 auto dummyValue = mlirOperationGetResult(testOp, 0);
1133 mlirOperationDestroy(testOp);
1141 static std::unique_ptr<RequireConstrainOpBuildFuncHelper>
get();
1152 auto testOp = createIndexOperation();
1158 mlirOperationDestroy(testOp);
1162 auto testOp = createIndexOperation();
1165 auto dummyValue = mlirOperationGetResult(testOp, 0);
1169 mlirOperationDestroy(testOp);
1174 auto testOperation = createIndexOperation();
1179 mlirOperationDestroy(testOperation);
1185 auto testOp = createIndexOperation();
1191 MlirLocation location = mlirLocationUnknownGet(context);
1192 auto dummyValue = mlirOperationGetResult(testOp, 0);
1198 mlirOperationDestroy(testOp);
1206 static std::unique_ptr<StepOpBuildFuncHelper>
get();
1217 auto testOp = createIndexOperation();
1223 mlirOperationDestroy(testOp);
1228 auto testOperation = createIndexOperation();
1233 mlirOperationDestroy(testOperation);
1239 auto testOp = createIndexOperation();
1245 MlirLocation location = mlirLocationUnknownGet(context);
1246 auto dummyValue = mlirOperationGetResult(testOp, 0);
1252 mlirOperationDestroy(testOp);
1260 static std::unique_ptr<StepYieldOpBuildFuncHelper>
get();
1271 auto testOp = createIndexOperation();
1277 mlirOperationDestroy(testOp);
1281 auto testOp = createIndexOperation();
1284 auto dummyValue = mlirOperationGetResult(testOp, 0);
1288 mlirOperationDestroy(testOp);
1293 auto testOperation = createIndexOperation();
1298 mlirOperationDestroy(testOperation);
1304 auto testOp = createIndexOperation();
1310 MlirLocation location = mlirLocationUnknownGet(context);
1311 auto dummyValue = mlirOperationGetResult(testOp, 0);
1317 mlirOperationDestroy(testOp);
1325 static std::unique_ptr<VerifAssertOpBuildFuncHelper>
get();
1336 auto testOp = createIndexOperation();
1342 mlirOperationDestroy(testOp);
1346 auto testOp = createIndexOperation();
1349 auto dummyValue = mlirOperationGetResult(testOp, 0);
1353 mlirOperationDestroy(testOp);
1358 auto testOperation = createIndexOperation();
1363 mlirOperationDestroy(testOperation);
1369 auto testOp = createIndexOperation();
1375 MlirLocation location = mlirLocationUnknownGet(context);
1376 auto dummyValue = mlirOperationGetResult(testOp, 0);
1382 mlirOperationDestroy(testOp);
1390 static std::unique_ptr<VerifProveOpBuildFuncHelper>
get();
1401 auto testOp = createIndexOperation();
1407 mlirOperationDestroy(testOp);
1411 auto testOp = createIndexOperation();
1414 auto dummyValue = mlirOperationGetResult(testOp, 0);
1418 mlirOperationDestroy(testOp);
1423 auto testOperation = createIndexOperation();
1428 mlirOperationDestroy(testOperation);
1434 auto testOp = createIndexOperation();
1440 MlirLocation location = mlirLocationUnknownGet(context);
1441 auto dummyValue = mlirOperationGetResult(testOp, 0);
1447 mlirOperationDestroy(testOp);
1455 static std::unique_ptr<VerifSMTProveOpBuildFuncHelper>
get();
1466 auto testOp = createIndexOperation();
1472 mlirOperationDestroy(testOp);
1476 auto testOp = createIndexOperation();
1479 auto dummyValue = mlirOperationGetResult(testOp, 0);
1483 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_AssumeDetOpSetHint(MlirOperation op, MlirValue value)
Set Hint operand of llzk::verif::AssumeDetOp 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_ContractOpGetResAttrs(MlirOperation op)
Get ResAttrs attribute 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.
bool llzkOperationIsA_Verif_ProveDetOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::ProveDetOp.
MlirAttribute llzkVerif_IncludeOpGetResAttrs(MlirOperation op)
Get ResAttrs attribute from llzk::verif::IncludeOp Operation.
MlirAttribute llzkVerif_IncludeOpGetArgAttrs(MlirOperation op)
Get ArgAttrs attribute from llzk::verif::IncludeOp 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.
void llzkVerif_ProveDetOpSetCondition(MlirOperation op, MlirValue value)
Set Condition operand of llzk::verif::ProveDetOp 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.
MlirOperation llzkVerif_AssumeDetOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue hint)
Build a llzk::verif::AssumeDetOp 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.
void llzkVerif_IncludeOpSetResAttrs(MlirOperation op, MlirAttribute attr)
Set ResAttrs attribute of llzk::verif::IncludeOp Operation.
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.
void llzkVerif_IncludeOpSetArgAttrs(MlirOperation op, MlirAttribute attr)
Set ArgAttrs attribute of llzk::verif::IncludeOp Operation.
MlirValue llzkVerif_ProveDetOpGetResult(MlirOperation op)
Get Result result from llzk::verif::ProveDetOp Operation.
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.
MlirValue llzkVerif_ProveDetOpGetCondition(MlirOperation op)
Get Condition operand from llzk::verif::ProveDetOp 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.
MlirOperation llzkVerif_ProveDetOpBuild(MlirOpBuilder builder, MlirLocation location, MlirValue condition)
Build a llzk::verif::ProveDetOp 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)
getSelfValue
MlirValue llzkVerif_IncreasesOpGetValue(MlirOperation op)
Get Value operand from llzk::verif::IncreasesOp Operation.
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.
MlirValue llzkVerif_AssumeDetOpGetHint(MlirOperation op)
Get Hint operand from llzk::verif::AssumeDetOp 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...
bool llzkOperationIsA_Verif_AssumeDetOp(MlirOperation inp)
Returns true if the Operation is a llzk::verif::AssumeDetOp.
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.
void llzkVerif_ContractOpSetResAttrs(MlirOperation op, MlirAttribute attr)
Set ResAttrs attribute of llzk::verif::ContractOp Operation.
MlirOperation llzkVerif_IncludeOpResolveCallable(MlirOperation inp)
resolveCallable
virtual bool callIsA(MlirOperation op) override
static std::unique_ptr< AssumeDetOpBuildFuncHelper > get()
This method must be implemented to return a subclass of AssumeDetOpBuildFuncHelper that at least impl...
AssumeDetOpBuildFuncHelper()=default
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
static std::unique_ptr< ProveDetOpBuildFuncHelper > get()
This method must be implemented to return a subclass of ProveDetOpBuildFuncHelper that at least imple...
ProveDetOpBuildFuncHelper()=default
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 ...