Array.branch()

• << Z3 Home
• Z3 Language Documentation
• Listing of Z3 Array Manipulation Member Functions

Array.branch(fns)

fns can be any arbitrary array of functions. The result will be a similar array as functions evaluated for the array itself.

Split values into [negative, zero and positive] values by default. Returns the true/false of the match result.

[[1,-2],[3,3],[0,44,-44]].branch(true).print()

[ [ [false,true ],

[false,false ],

[false,false,true ] ],

[ [false,false ],

[false,false ],

[true,false,false ] ],

[ [true,false ],

[true,true ],

[false,true,false ] ] ]

[-5..5].branch(true)

true true true true true false false false false false false

false false false false false true false false false false false

false false false false false false true true true true true

[-5..5].branchvalues(true)

branchvalues splits it based on neg, zero and positive, and OnlyMatches will filtered if unmatched.

-5 -4 -3 -2 -1

0

1 2 3 4 5

-10..10.branch([LT,[EQ,GT]]) .print()

See Also

branchvalues