Don't like ads? PRO users don't see any ads ;-)
Public Pastes
Guest

Untitled

By: a guest on May 6th, 2012  |  syntax: None  |  size: 0.68 KB  |  hits: 10  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
  1. How to invoke Z3 on an input file
  2. (declare-const a Int)
  3. (declare-const b Int)
  4. (declare-const c Int)
  5. (declare-const d Real)
  6. (declare-const e Real)
  7. (assert (> a (+ b 2)))
  8. (assert (= a (+ (* 2 c) 10)))
  9. (assert (<= (+ c b) 1000))
  10. (assert (>= d e))
  11. (check-sat)
  12. (get-model)
  13.        
  14. sat
  15. (model
  16.     (define-fun c () Int
  17.         (- 5))
  18.     (define-fun a () Int
  19.         0)
  20.     (define-fun b () Int
  21.         (- 3))
  22.     (define-fun d ()
  23.         Real 0.0)
  24.     (define-fun e ()
  25.         Real 0.0)
  26. )
  27.        
  28. (benchmark file
  29.   :extrafuns ((a Int) (b Int) (c Int) (d Real) (e Real))
  30.   :assumption (> a (+ b 2))
  31.   :assumption (= a (+ (* 2 c) 10))
  32.   :assumption (<= (+ c b) 1000)
  33.   :assumption (>= d e)
  34.   :formula true)
create a new version of this paste RAW Paste Data