Z3 unsigned variables - simplify

Question

I have the following constraint (constr) I want to simplify:

4p+3q<=-10+r AND 4p+3q<=-12+r

p (and similar for r) is created as follows:

Z3_ast p;
Z3_sort ty = Z3_mk_int_sort(ctx)
Z3_symbol s = Z3_mk_string_symbol(ctx, "p");
p = Z3_mk_const(ctx, s, ty)

If i do

Z3_simplify(ctx, constr)

Nothing changes as p and r are integers.

How can I encode the knowledge that p an r are natural numbers (unsigned)?

Simply adding the constraint p >= 0 AND r >= 0 will not help in the context of simplifying my constraint (but of course helps when seeking a solution).

To clarify,

4p+3q<=-10+r AND 4p+3q<=-12+r

should be reduced to:

4p+3q<=-12+r

As it is the hardest to fulfill (implies the other).

UPDATE: Tried the solution by Taylor on the constraint and it works. When I try to use the same technique for the following different (somewhat)-pretty-printed constraint:

(([(false AND (0<=5+0epsilon+0q+0p AND false)) OR (0<=5+0epsilon+0q+0p AND [(0+0epsilon+q+0p<=5+0epsilon+0q+0p AND (0+0epsilon+q+0p<=5+0epsilon+0q+0p AND [false OR 0+0epsilon+0q+p<=7+0epsilon+0q+0p])) OR (false AND false) OR (false AND false)])] AND [(false AND (0<=5+0epsilon+0q+0p AND false)) OR (0<=5+0epsilon+0q+0p AND [(0+0epsilon+q+0p<=5+0epsilon+0q+0p AND (0+0epsilon+q+0p<=5+0epsilon+0q+0p AND [false OR 0+0epsilon+0q+p<=7+0epsilon+0q+0p])) OR (false AND false) OR (false AND false)])]) AND epsilon>=0 AND q>=0 AND p>=0)

By Z3_simplify this is reduced to

(q<=5 AND p<=7 AND epsilon>=0 AND q>=0 AND p>=0)

If I create a tactic using ctx-solver-simplify together with a goal and use Z3_apply_result_to_string, I get the following:

(goals
(goal
  (let ((a!1 (+ 5 (* 0 epsilon) (* 0 q) (* 0 p)))
        (a!3 (or false
                 (<= (+ 0 (* 0 epsilon) (* 0 q) p)
                     (+ 7 (* 0 epsilon) (* 0 q) (* 0 p))))))
  (let ((a!2 (<= (+ 0 (* 0 epsilon) q (* 0 p)) a!1)))
    (or (and false (<= 0 a!1) false)
        (and (<= 0 a!1)
             (or (and a!2 a!2 a!3) (and false false) (and false false))))))
  (>= epsilon 0)
  (>= q 0)
  (>= p 0))
)

What can I do to get a simple representation like the one for Z3_simplify?

Answer 1

For this example, this can be done using the strongest simplifier, ctx-solver-simplify, although note that in general this could transform your equations. Here is your example (rise4fun link: http://rise4fun.com/Z3/tw0t ):

(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun r () Int)

(assert (and (<= (+ (* 4 p) (* 3 q)) (- r 10)) (<= (+ (* 4 p) (* 3 q)) (- r 12))))

(apply ctx-solver-simplify)

(apply (then simplify ctx-simplify ctx-solver-simplify))

; (help-tactic)

Output:

(goals
(goal
  (<= (+ (* 4 p) (* 3 q)) (+ r (* (- 1) 12)))
  :precision precise :depth 1)
)
(goals
(goal
  (<= (+ (* 4 p) (* 3 q)) (+ (- 12) r))
  :precision precise :depth 3)
)

You can use the tactics via the C API as well.

You can add the natural number constraint as well:

(assert (and (<= (+ (* 4 p) (* 3 q)) (- r 10)) (<= (+ (* 4 p) (* 3 q)) (- r 12))))
(assert (>= p 0))
(assert (>= r 0))
(apply ctx-solver-simplify)
(apply (then simplify ctx-simplify ctx-solver-simplify))

Output:

(goals
(goal
  (<= (+ (* 4 p) (* 3 q)) (+ r (* (- 1) 12)))
  (>= p 0)
  (>= r 0)
  :precision precise :depth 1)
)
(goals
(goal
  (<= (+ (* 4 p) (* 3 q)) (+ (- 12) r))
  (>= p 0)
  (>= r 0)
  :precision precise :depth 3)
)

UPDATE:

You probably just need to iterate over the appropriate subgoals after applying the simplification tactics to get the formulas out if you need the simplified ones for something, see, e.g. Z3_apply_result_get_subgoal:

http://z3prover.github.io/api/html/group__capi.html#ga63813eb4cc7865f0cf714e1eff0e0c64

When I tried this tactic on your new constraint, it also returns the simplified answer you stated (rise4fun link: http://rise4fun.com/Z3/T1TZ ):

(declare-fun epsilon () Int)
(declare-fun q () Int)
(declare-fun p () Int)

(assert (and  (let ((a!1 (+ 5 (* 0 epsilon) (* 0 q) (* 0 p)))
        (a!3 (or false
                 (<= (+ 0 (* 0 epsilon) (* 0 q) p)
                     (+ 7 (* 0 epsilon) (* 0 q) (* 0 p))))))
  (let ((a!2 (<= (+ 0 (* 0 epsilon) q (* 0 p)) a!1)))
    (or (and false (<= 0 a!1) false)
        (and (<= 0 a!1)
             (or (and a!2 a!2 a!3) (and false false) (and false false))))))
  (>= epsilon 0)
  (>= q 0)
  (>= p 0)))

(apply (then simplify ctx-simplify ctx-solver-simplify))

which yields

(goals
(goal
  (<= q 5)
  (>= epsilon 0)
  (>= q 0)
  (>= p 0)
  (<= p 7)
  :precision precise :depth 3)
)