Skip to content

Conversation

@Shoooooon
Copy link
Contributor

  • Partial support for ArraysEX theory added
  • JSON output for parametric sorts defined:
    • Sorts are identifiers or objects of the form { "sortKind": (identifier), "sortParams": [sort...] }
    • e.g., Int, [Bitvec, 32], { "sortKind": Array, "sortParams": [Int, Int]}
    • Nonterminals are handled/printed as sorts as well, so I opted to avoid changing the representation of unparametrized identifiers.

@kjcjohnson
Copy link
Collaborator

I am, in general, fine with this PR - looks good to me.

I do want to be a bit pedantic about naming on the JSON format changes.

  • sortKind and sortParams should just be kind and params. We're already inside of a sort object, so it's redundant to have sort in the name! In most places it's used, it will be as a parameter called sort: or returnSort: or similar.
  • Why kind? The SMT-LIB docs seem to mostly call it the "sort symbol", and we use "name" and "id" in other similar places. It's fine if you have a justification, but just want to be intentional about it. It will be difficult to change in the future :)

@Shoooooon
Copy link
Contributor Author

  • I agree about changing sortKind and sortParams to kind and params.
  • I tried to stay away from "name" and "id" because the kind is not unique to a given sort (e.g., one might have (Set Int) and (Set Bool), in which case name and id are a little misleading). The phrase "symbol" misses the point that the kind defines the overarching type of the object.

@kjcjohnson kjcjohnson merged commit 884868e into SemGuS-git:main Feb 23, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants