#lang rosette (define-symbolic a b c d e f g y z boolean?) (define deps (&& (=> a b) (=> a c) (=> a z) (=> b d) (=> c (|| d e)) (=> c (|| f g)) (! (&& d e)) (=> y z))) (define (int b) (if b 1 0)) (define obj (+ (int a) (int b) (int c) (int d) (int d) (int e) (* 5 (int f)) (* 2 (int g)) (int y) (* 0 (int z)))) (define (install deps new . given) ; installation (solve (assert (apply && deps new given)))) (define (optimal-install obj deps new . given) ; optimal installation (optimize #:minimize (list obj) #:guarantee (assert (&& deps a z)))) (define (show sol) (and (sat? sol) (sort (for/list ([(k v) (model sol)] #:when v) k) string