I am new to Z3, so excuse me if the question sounds too easy. I have two questions regrading constants in Z3 Java API.
- How does creation of constants happen internally? To understand that I started by tracking
public BitVecExpr mkBVConst(String, int)
down topublic StringSymbol mkSymbol(String)
which eventually callsNative.mkStringSymbol(var1.nCtx(), var2)
which generates the variable invar3
in this linelong var3 = INTERNALmkStringSymbol(var0, var2);
now because `INTERNALmkStringSymbol' is native I can't see its source. I am wondering about how does it operate. Does anyone know how does it work? Where to view its source?
- Another thing I am confused about is the scoping of constants using the API. In the interactive Z3, it is maintained through matching push and pop but through the API, I am not sure how scoping is defined and managed.
Any insights or guidance is much appreciated.!