z3 - z3py expression simplification

Question

I am trying to simplify an expression using z3py but am unable to find any documentation on what different tactics do. The best resource I have found is a stack overflow question that lists all the tactics by name.

Is someone able to link me to detailed documentation on the tactics available? The on line python tutorials are not sufficient.

Or can someone recommend a better way to accomplish this.

An example of the problems is an expression such as:

x < 5, x < 4, x < 3, x = 1 I would like this to simplify down to x = 1.

Using the tactic unit-subsume-simplify appears works for this example.

But when I try a more complicated example such as x > 1, x < 5, x != 3, x != 4 I get x > 1, x < 5, x ≠ 3, x ≠ 4 as the result. When I would like x = 2.

What is the best approach to achieve this type of simplification using z3py?

My current solution.

Thanks Matt

Answer 1

Example with Redlog of Reduce. Please let me know what do you think.

Answer 2

可能的解决方案：

x = Int('x')
s = Solver()
s.add(x < 5, x < 4, x < 3, x == 1)
print s.check()
m = s.model()
print m
s1 = Solver()
s1.add(x > 1, x < 5, x != 3, x != 4)
print s1.check()
m1 = s1.model()
print m1

输出：

sat
[x = 1]
sat
[x = 2]

在此处在线运行此解决方案