View Source cure_smt_array (cure v0.7.0)
SMT Array Theory for Lists and Vectors
This module provides SMT array theory support for reasoning about lists and vectors with constraints like:
- All elements satisfy a property (forall i. arr[i] > 0)
- Sorted sequences (forall i j. i < j => arr[i] <= arr[j])
- Length-indexed vectors (length(arr) == n)
SMT-LIB Array Theory
Arrays in SMT-LIB are maps from indices to values:
(declare-const arr (Array Int Int)) ; Array from Int to Int
(assert (= (select arr 0) 42)) ; arr[0] = 42
(assert (= (store arr 1 10) arr2)) ; arr2 = arr with arr2[1] = 10Usage
% Check if all elements are positive
Constraint = all_elements_satisfy(arr, n,
fun(i, v) -> #binary_op_expr{op = '>', left = v, right = lit(0)} end),
Query = generate_array_query(Constraint, #{arr => {array, int, int}, n => {type, int}}).Summary
Types
-type expr() :: #literal_expr{value :: term(), location :: term()} | #identifier_expr{name :: term(), location :: term()} | #function_call_expr{function :: term(), args :: term(), location :: term()} | #match_expr{expr :: term(), patterns :: term(), location :: term()} | #let_expr{bindings :: term(), body :: term(), location :: term()} | #binary_op_expr{op :: term(), left :: term(), right :: term(), location :: term()} | #unary_op_expr{op :: term(), operand :: term(), location :: term()} | #list_expr{elements :: term(), location :: term()} | #vector_expr{elements :: term(), location :: term()} | #tuple_expr{elements :: term(), location :: term()} | #record_expr{name :: term(), fields :: term(), location :: term()} | #field_access_expr{record :: term(), field :: term(), location :: term()} | #record_update_expr{name :: term(), base :: term(), fields :: term(), location :: term()} | #lambda_expr{params :: term(), body :: term(), location :: term()} | #forall_expr{variables :: term(), body :: term(), location :: term()} | #exists_expr{variables :: term(), body :: term(), location :: term()} | #fsm_spawn_expr{fsm_name :: term(), init_args :: term(), init_state :: term(), location :: term()} | #fsm_send_expr{target :: term(), message :: term(), location :: term()} | #fsm_receive_expr{patterns :: term(), timeout :: term(), location :: term()} | #fsm_state_expr{location :: term()} | #melquiades_send_expr{message :: term(), target :: term(), location :: term()} | #qualified_call_expr{trait_name :: term(), type_args :: term(), method_name :: term(), receiver :: term(), args :: term(), location :: term()}.