Skip to content

Instantly share code, notes, and snippets.

@LeventErkok

LeventErkok/gist:e08a65ac190da3ba88a2989a146a407e

Created April 22, 2019 14:24
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save LeventErkok/e08a65ac190da3ba88a2989a146a407e to your computer and use it in GitHub Desktop.
Save LeventErkok/e08a65ac190da3ba88a2989a146a407e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
(set-logic ALL)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(declare-fun v3 () Int)
(assert (distinct v1 v2))
(assert (>= 10 v1 0))
(assert (>= 10 v2 0))
(assert (>= 10 v3 0))
(declare-fun empty () (Array Int Bool))
(define-fun set () (Array Int Bool) (store (store (store empty v1 true) v2 true) v3 true))
(declare-fun cost () Int)
(assert (set-has-size set cost))
(minimize cost)
(check-sat)
(get-model)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment