Skip to content

JKind v1.5
Compare
Choose a tag to compare
@agacek agacek released this 08 Apr 13:38
· 459 commits to master since this release
v1.5
f3c96e6

Features

  • Detect (some) duplicate node calls and coalesce them for efficiency
  • From Lucas Wagner: support for tuples so that multi-return node calls can occur
    anywhere in an expression. For example:
  flag, value = if a > b then nodecall(x) else (true, 0)
  • Support for int/real casting using real(x) and floor(x)
  • Support for non-linear arithmetic when using Z3. This requires disabling the checks for division by zero, modulus by a negative integer, and integer division by a negative integer. The behavior under any of these conditions is left unspecified and subject to change in the future.
  • Added JKindApi.setSolver() (options: Yices, Z3, CVC4)

Feature: Record Updates

From Lucas Wagner: this release adds support for record updates using the syntax expr{field := value}. This is a functional update so it returns a new record with the updated value rather than changing the original record. The precedence of pre and record update may be initially confusing. Note the following equivalences

  pre expr{field := value} ==> (pre expr){field := (pre value)}
  pre(expr){field := value} ==> (pre expr){field := (pre value)}

Thus one should use (pre ...) to ensure the proper scope for pre expressions when using record updates.

Feature: Arrays

This release adds support for arrays. For example:

var
  A : int[5];
  sorted : bool;
let
  A = [0, 0, 0, 0, 0] -> (pre A)[i := v]
  sorted = A[0] <= A[1] and A[1] <= A[2] and ...;

Arrays are currently expanded to scalars, and dynamic indexing into
arrays for lookup or update is expanded to if-then-else expressions. Array updates are functional, just like record updates. Also, the precedence of pre and array lookup and update may be initially confusing. Note the following equivalences

  pre A[i := v] ==> (pre A)[(pre i) := (pre v)]
  pre(A)[i := v] ==> (pre A)[(pre i) := (pre v)]
  pre A[i] ==> (pre A)[pre i]
  pre(A)[i] ==> (pre A)[pre i]

Thus one should use (pre ...) to ensure the proper scope for pre expressions when using array operations.

Indexing outside of array bounds is discouraged. The current behavior for updates outside of array bounds is that they are ignored. The current behavior for lookups outside of arrays bound is that they return a default value. Both of these behaviors are subject to change in the future and should not be relied upon.

Fixes

  • Fixed bug in constant inlining which would cause some constants not be inlined
  • Fixed bug in checking for division by zero within constant declarations
  • Fixed bug in the options sent to CVC4 so that integer division by a constant is supported
  • Fixed bug in counterexample reconstruction which could crash JKind
Assets 3
Loading