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

Method getBoundVariableSorts

src/api/java/Lambda.java:57–65  ·  view source on GitHub ↗

The sorts of the bound variables. @throws Z3Exception

()

Source from the content-addressed store, hash-verified

55 * @throws Z3Exception
56 **/
57 public Sort[] getBoundVariableSorts()
58 {
59 int n = getNumBound();
60 Sort[] res = new Sort[n];
61 for (int i = 0; i < n; i++)
62 res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
63 getContext().nCtx(), getNativeObject(), i));
64 return res;
65 }
66
67 /**
68 * The body of the quantifier.

Callers

nothing calls this directly

Calls 5

getNumBoundMethod · 0.95
createMethod · 0.95
getContextMethod · 0.80
nCtxMethod · 0.80
getNativeObjectMethod · 0.80

Tested by

no test coverage detected