z3
by Microsoft Research
Is this formula satisfiable?
Ask z3!
; This example illustrates basic arithmetic and ; uninterpreted functions (declare-fun x () Int) (declare-fun y () Int) (declare-fun z () Int) (assert (>= (* 2 x) (+ y z))) (declare-fun f (Int) Int) (declare-fun g (Int Int) Int) (assert (< (f x) (g x x))) (assert (> (f y) (g x x))) (check-sat) (get-model) (push) (assert (= x y)) (check-sat) (pop) (exit)
home
tutorial
video
permalink
More samples
doc_examples
smtc_core
smtc_datatypes
smtc_arrays
smtc_bv
bit-count
About Z3 - Efficient Theorem Prover
Z3 is a high-performance theorem prover. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers.
home
tutorials
project map
live
developer
about
© 2012 Microsoft Corporation -
terms of use
-
privacy