5

How do I get the maximum of a formula using smt-lib2?

I want something like this:

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= x 2))
(assert (= y 4))
(assert (= z (max x y))
(check-sat)
(get-model)
(exit)

Of course, 'max' is unknown to smtlibv2. So, how can this be done?

John Smith
  • 771
  • 8
  • 25

2 Answers2

10

In Z3, you can easily define a macro max and use it for getting maximum of two values:

(define-fun max ((x Int) (y Int)) Int
  (ite (< x y) y x))

There is another trick to model max using uninterpreted functions, which will be helpful to use with Z3 API:

(declare-fun max (Int Int) Int)
(assert (forall ((x Int) (y Int))
    (= (max x y) (ite (< x y) y x))))

Note that you have to set (set-option :macro-finder true), so Z3 is able to replace universal quantifiers with body of the function when checking satisfiability.

pad
  • 41,040
  • 7
  • 92
  • 166
  • Quick note: `define-fun` is part of the SMT-LIB v2 standard. – Leonardo de Moura Nov 28 '11 at 17:18
  • Thank You... this is very good indeed. Next problem would be to make a max function which takes n arguments (like +). I can't get it to work with "List Int". How is that done? – John Smith Nov 30 '11 at 13:27
  • 2
    max for lists is more complicated. define-fun is just macro, and recursion is not allowed. The option `:macro-finder` will not detect "recursive macros". You can still write a "forall" axiom for max-int-list. However, Z3 will not be complete. That is, it may return "unknown". More precisely, it will return "unknown" for any satisfiable problem, and for some unsatisfiable problems that can be solved by the default search limits used in Z3. In future versions of Z3, we may extend the inductive datatype procedure to handle fold like definitions. – Leonardo de Moura Nov 30 '11 at 19:04
3

You've got abs, and per basic math max(a,b) = (a+b+abs(a-b))/2

MSalters
  • 173,980
  • 10
  • 155
  • 350
  • I see where this is going... but in the end I want to use max() on more than two parameters(floating point) without doing this kind of workarounds. Hope there are easier solutions to this ;) Thanks. – John Smith Nov 28 '11 at 15:10