model-sns-swap-participations.smt2

(define-fun e8s ((x Int)) Int (* x 100000000))

; Example values based on parameterf from here:
; https://nns.ic0.app/proposal/?u=qoctq-giaaa-aaaaa-aaaea-cai&proposal=131075
(define-const minimum_participants Int 50)
(define-const minimum_direct_participation_icp Int (e8s 50000))
(define-const maximum_direct_participation_icp Int (e8s 250000))
(define-const minimum_participant_icp Int (e8s 10))
(define-const maximum_participant_icp Int (e8s 50000))

; Helper functions
(define-fun is_valid_participation ((x Int)) Bool (
    and (>= x minimum_participant_icp)
        (<= x maximum_participant_icp)
))

; General facts about arrays
(declare-fun len ((Array Int Int)) Int)
(assert (forall ((xs (Array Int Int))) (>= (len xs) 0)))

(define-fun in_range ((p Int) (xs (Array Int Int))) Bool
    (and (>= p 0) (< p (len xs))))

(define-fun-rec sum ((xs (Array Int Int)) (till Int)) Int
    (ite (not (in_range (- till 1) xs))
        0
        (+ (select xs (- till 1)) (sum xs (- till 1)))
    )
)
(define-fun total ((xs (Array Int Int))) Int
    (sum xs (len xs))
)

; Modeling direct participants
(declare-const direct_participant_e8s (Array Int Int))

; Each participation is within bounds
(assert (forall ((p Int))
    (implies (in_range p direct_participant_e8s)
        (is_valid_participation (select direct_participant_e8s p)))
))

; These constraints convenient for testing
(assert (= (total direct_participant_e8s) maximum_direct_participation_icp))
(assert (= (len direct_participant_e8s) minimum_participants))

(get-info :version) 
(check-sat)

; If satisfiability has been established, fetch the relevant bits from the model
(get-value ((select direct_participant_e8s 0)))
(get-value ((select direct_participant_e8s 1)))
(get-value ((select direct_participant_e8s 2)))
; ditto
(get-value ((select direct_participant_e8s (- (len direct_participant_e8s) 1))))

; Example output from z3
; ----------------------
; (:version "4.8.10")
; sat
; (((select direct_participant_e8s 0) 4999999996417))
; (((select direct_participant_e8s 1) 4999999997744))
; (((select direct_participant_e8s 2) 1000007854))
; (((select direct_participant_e8s (- (len direct_participant_e8s) 1)) 1000000000))