MCPcopy Create free account
hub / github.com/Z3Prover/z3 / ToBitVecExprArray

Method ToBitVecExprArray

src/api/java/ASTVector.java:144–151  ·  view source on GitHub ↗

Translates the AST vector into an BitVecExpr[]

()

Source from the content-addressed store, hash-verified

142 * Translates the AST vector into an BitVecExpr[]
143 * */
144 public BitVecExpr[] ToBitVecExprArray()
145 {
146 int n = size();
147 BitVecExpr[] res = new BitVecExpr[n];
148 for (int i = 0; i < n; i++)
149 res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
150 return res;
151 }
152
153 /**
154 * Translates the AST vector into an ArithExpr[]

Callers

nothing calls this directly

Calls 5

sizeMethod · 0.95
createMethod · 0.95
getMethod · 0.95
getContextMethod · 0.80
getNativeObjectMethod · 0.80

Tested by

no test coverage detected