Value classes instead of Longs in Z3 API

Open
#44 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
5/5
Estimated time
Over a week
Newbie friendliness
25/100
Issue type
Refactor
Clarity
Mostly clear
Activity status
Stale
Tech stack
kotlin
Domain
backend-api-design

Research direction

Start by reading the Z3.Native methods and how native objects such as sorts, expressions, and declarations are represented throughout the Kotlin API. Identify the distinct object kinds and the methods that accept raw longs. Done means the API uses value classes that distinguish these native objects instead of ambiguous longs.

Written by the indexing model from the issue text.

Description

enhancement

Currently, we use long to represent all Z3 native objects: sorts, expressions, declarations.
Also, all Z3.Native methods accept raw longs without any clarification whether it is sort, expr, or whatever else.

The idea is to provide wrappers for Z3.native methods with different value classes for different object kinds.

Dominant language
Kotlin
Stars
42
Forks
17
No merged PRs in 30d

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from UnitTestBot/ksmt

All issues in UnitTestBot/ksmt

Similar issues

More Kotlin issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.