kdrag.theories.real.arb.z3_of_exact_arb

kdrag.theories.real.arb.z3_of_exact_arb(x: arb) → ArithRef

Get exact arb as z3 value

>>> z3_of_exact_arb(arb(1))
1
>>> z3_of_exact_arb(arb(1) + arb(2))
3
>>> z3_of_exact_arb(arb(2**1000))
2**1000

Parameters:

x (arb)

Return type:

ArithRef