Array.branch()

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

Array.branch(SomeOnlyMatches)

Split values into negative, zero and positive values. Return the true/false of the match result. Show all (with null for non-matches) or matches only based on SomeOnlyMatches.

[[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)

-5 -4 -3 -2 -1

0

1 2 3 4 5