t>=1 or t>=2 => t>=1

Question

Using Z3, is it possible to somehow merge/simplify

t>=2 or t>=1

into

t>=1

where t is an integer?

We wish keep the constraint for t as simple as possible.

score 3 · Accepted Answer · answered Jul 16 '12 at 16:32

3

Z3 can do it by using the tactic ctx-solver-simplify. Note that this tactic may be quite expensive. The tactic ctx-simplify is cheaper by it only "propagates" equalities.

Here is a link for script using this tactic: http://rise4fun.com/Z3/F7Q

answered Jul 16 '12 at 16:32

Leonardo de Moura

21,065
2
47
53

Thanks! Seems to me (t>=0 and t<=1) or (t>=0 and t<=1) => (t>=0 and t<=1) But why it return false for the link here： http://rise4fun.com/Z3/aZFY – william007 Jul 16 '12 at 17:22
Sorry about that. This is bug. We will fix it for the next release. – Leonardo de Moura Jul 16 '12 at 18:03
Thanks, and also, seems to me (t>=2 and t<=2) => t==2 but link here http://rise4fun.com/Z3/NHlx doesn't seem to simplify that, is it possible for this simplification? – william007 Jul 16 '12 at 22:49
The tactic `propagate-ineqs` does the trick. However, this tactic only consider inequalities and equalities that are not nested inside the formula. So, it will not work for `(p or (t>=2 and t<=2))` – Leonardo de Moura Jul 17 '12 at 01:01
The link is broken (and web.archive doesn't record it). Could you paste this code snippet again? Very thanks! – chansey Sep 23 '21 at 12:44

t>=1 or t>=2 => t>=1

1 Answers1

Linked