search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
121 stars 33 forks source link

Where is mkEnumType/EnumSort? #77

Open delenius opened 3 years ago

delenius commented 3 years ago

The current version of Z3Context has no mkEnumType method, or EnumSort class. The Java API has a corresponding method, and so does the underlying Native class used by ScalaZ3 (at least when I compiled it):

    protected static native long INTERNALmkEnumerationSort(long var0, long var2, int var4, long[] var5, long[] var6, long[] var7);

Is there another preferred way to create an enum type?

romac commented 3 years ago

We are likely missing some bindings here, would gladly accept a PR for this :)