Want more features on Pastebin? Sign Up, it's FREE!
Guest

Untitled

By: a guest on Jun 20th, 2012  |  syntax: None  |  size: 1.36 KB  |  views: 48  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
This paste has a previous version, view the difference. Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
  1. ; header
  2.  
  3. (set-logic QF_LIA)
  4.  
  5. ; initial variable declarations
  6.  
  7. (declare-fun var1 () Int)
  8. (assert     (and
  9.       (>= var1 0)
  10.       (<= var1 7)
  11.     ))
  12. (declare-fun var1_post () Int)
  13. (assert     (and
  14.       (>= var1_post 0)
  15.       (<= var1_post 7)
  16.     ))
  17. (declare-fun var2 () Int)
  18. (assert     (and
  19.       (>= var2 0)
  20.       (<= var2 4)
  21.     ))
  22. (declare-fun var2_post () Int)
  23. (assert     (and
  24.       (>= var2_post 0)
  25.       (<= var2_post 4)
  26.     ))
  27. (declare-fun var3 () Int)
  28. (assert     (and
  29.       (>= var3 0)
  30.       (<= var3 4)
  31.     ))
  32. (declare-fun var3_post () Int)
  33. (assert     (and
  34.       (>= var3_post 0)
  35.       (<= var3_post 4)
  36.     ))
  37. (declare-fun var4 () Int)
  38. (assert     (and
  39.       (>= var4 0)
  40.       (<= var4 1)
  41.     ))
  42. (declare-fun var4_post () Int)
  43. (assert     (and
  44.       (>= var4_post 0)
  45.       (<= var4_post 1)
  46.     ))
  47.  
  48. (assert (not
  49. (and
  50.   (=
  51.     var1
  52.     7
  53.   )
  54.   (=
  55.     var2
  56.     0
  57.   )
  58.   (=
  59.     var1_post
  60.     2
  61.   )
  62.   (=
  63.     var4_post
  64.     1
  65.   )
  66.   (=
  67.     var2_post
  68.       var2
  69.   )
  70.   (=
  71.     var3_post
  72.       var3
  73.   )
  74. )
  75. ))
  76.  
  77. (assert
  78.   (and
  79.     (=
  80.       var1
  81.       0
  82.     )
  83.     (=
  84.         var2
  85.       0
  86.     )
  87.     (=
  88.       var1_post
  89.       2
  90.     )
  91.     (=
  92.       var4_post
  93.       1
  94.     )
  95.     (=
  96.       var2_post
  97.         var2
  98.     )
  99.     (=
  100.       var3_post
  101.         var3
  102.     )
  103.  
  104.   )
  105. )
  106.  
  107. ; start check
  108. (check-sat)
  109. (get-model)
  110. (exit)
clone this paste RAW Paste Data