Let's say I have the following z3py expression:

import z3
x, y = z3.Ints("x y")
z3_expression = z3.Not(x<y)

This expression is saved and printed with str() as Not(x < y). I want to know if there is any way to apply that Not() operator to the expression and change the sign of the inequality, i.e. I want to remove that negation operator and make the expression look like this: z3_expression = (x >= y), the parenthesis is not neccesary, I just put it to make it clearer.

Is there a way to do it preferably using z3py?

EDIT: The first answear solves this concrete problem, but if I change the expression to:

z3_expression = z3.Not(x<=y)
z3_simplified_expression = z3.simplify(z3_expression)
print(z3_simplified_expression)

This prints:

Not(x <= y)

Instead of:

x > y

CodePudding user response：

In this particular case, yes:

from z3 import *

x, y = Ints("x y")
e = Not(x < y)
f = simplify(e)

print(f)

This prints:

y <= x

But it's important to emphasize what you'd consider "simplified" as a person/mathematicial and what the tool will consider simple may not always match. That is, z3 might convert the expression (or not change it at all), depending on many factors.

The function simplify takes many options. To see them, run:

help_simplify()

You'll see the following printed:

algebraic_number_evaluator (bool) simplify/evaluate expressions containing (algebraic) irrational numbers. (default: true)
arith_ineq_lhs (bool) rewrite inequalities so that right-hand-side is a constant. (default: false)
arith_lhs (bool) all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. (default: false)
bit2bool (bool) try to convert bit-vector terms of size 1 into Boolean terms (default: true)
blast_distinct (bool) expand a distinct predicate into a quadratic number of disequalities (default: false)
blast_distinct_threshold (unsigned int) when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted (default: 4294967295)
blast_eq_value (bool) blast (some) Bit-vector equalities into bits (default: false)
bv_extract_prop (bool) attempt to partially propagate extraction inwards (default: false)
bv_ineq_consistency_test_max (unsigned int) max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. (default: 0)
bv_ite2id (bool) rewrite ite that can be simplified to identity (default: false)
bv_le_extra (bool) additional bu_(u/s)le simplifications (default: false)
bv_not_simpl (bool) apply simplifications for bvnot (default: false)
bv_sort_ac (bool) sort the arguments of all AC operators (default: false)
bv_trailing (bool) lean removal of trailing zeros (default: false)
bv_urem_simpl (bool) additional simplification for bvurem (default: false)
bvnot2arith (bool) replace (bvnot x) with (bvsub -1 x) (default: false)
cache_all (bool) cache all intermediate results. (default: false)
elim_and (bool) conjunctions are rewritten using negation and disjunctions (default: false)
elim_ite (bool) eliminate ite in favor of and/or (default: true)
elim_rem (bool) replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). (default: false)
elim_sign_ext (bool) expand sign-ext operator using concat and extract (default: true)
elim_to_real (bool) eliminate to_real from arithmetic predicates that contain only integers. (default: false)
eq2ineq (bool) expand equalities into two inequalities (default: false)
expand_power (bool) expand (^ t k) into (* t ... t) if  1 < k <= max_degree. (default: false)
expand_select_store (bool) replace a (select (store ...) ...) term by an if-then-else term (default: false)
expand_store_eq (bool) reduce (store ...) = (store ...) with a common base into selects (default: false)
expand_tan (bool) replace (tan x) with (/ (sin x) (cos x)). (default: false)
flat (bool) create nary applications for and,or, ,*,bvadd,bvmul,bvand,bvor,bvxor (default: true)
gcd_rounding (bool) use gcd rounding on integer arithmetic atoms. (default: false)
hi_div0 (bool) use the 'hardware interpretation' for division by zero (for bit-vector terms) (default: true)
hoist_cmul (bool) hoist constant multiplication over summation to minimize number of multiplications (default: false)
hoist_ite (bool) hoist shared summands under ite expressions (default: false)
hoist_mul (bool) hoist multiplication over summation to minimize number of multiplications (default: false)
ignore_patterns_on_ground_qbody (bool) ignores patterns on quantifiers that don't mention their bound variables. (default: true)
ite_extra_rules (bool) extra ite simplifications, these additional simplifications may reduce size locally but increase globally (default: false)
local_ctx (bool) perform local (i.e., cheap) context simplifications (default: false)
local_ctx_limit (unsigned int) limit for applying local context simplifier (default: 4294967295)
max_degree (unsigned int) max degree of algebraic numbers (and power operators) processed by simplifier. (default: 64)
max_memory (unsigned int) maximum amount of memory in megabytes (default: 4294967295)
max_steps (unsigned int) maximum number of steps (default: 4294967295)
mul2concat (bool) replace multiplication by a power of two into a concatenation (default: false)
mul_to_power (bool) collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. (default: false)
pull_cheap_ite (bool) pull if-then-else terms when cheap. (default: false)
push_ite_arith (bool) push if-then-else over arithmetic terms. (default: false)
push_ite_bv (bool) push if-then-else over bit-vector terms. (default: false)
push_to_real (bool) distribute to_real over * and  . (default: true)
rewrite_patterns (bool) rewrite patterns. (default: false)
som (bool) put polynomials in som-of-monomials form (default: false)
som_blowup (unsigned int) maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form (default: 10)
sort_store (bool) sort nested stores when the indices are known to be different (default: false)
sort_sums (bool) sort the arguments of   application. (default: false)
split_concat_eq (bool) split equalities of the form (= (concat t1 t2) t3) (default: false)
udiv2mul (bool) convert constant udiv to mul (default: false)

You can use these as you see fit.