如何更改 z3py 否定不等式的符号
How to change the sign of z3py negated inequalities
假设我有以下 z3py 表达式：
import z3
x, y = z3.Ints("x y")
z3_expression = z3.Not(x<y)
此表达式以str() 保存并打印为Not(x < y)。我想知道是否有任何方法可以将该 Not() 运算符应用于表达式并更改不等式的符号，即我想删除该否定运算符并使表达式看起来像这样： z3_expression = (x >= y) ，括号不是必须的，我只是为了更清楚地加上括号。
有没有最好使用 z3py 的方法？
编辑：
第一个 answear 解决了这个具体问题，但是如果我将表达式更改为：
z3_expression = z3.Not(x<=y)
z3_simplified_expression = z3.simplify(z3_expression)
print(z3_simplified_expression)
这会打印：
Not(x <= y)
而不是：
x > y
在这种特殊情况下，是的：
from z3 import *
x, y = Ints("x y")
e = Not(x < y)
f = simplify(e)
print(f)
这会打印：
y <= x
但重要的是要强调您认为“简化”的内容 person/mathematicial 以及工具认为简单的内容可能并不总是匹配。也就是说，z3 可能会转换表达式（或根本不更改它），具体取决于许多因素。
函数simplify有很多选项。要查看它们，运行:
help_simplify()
您将看到以下打印内容：
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)
您可以根据需要使用它们。
假设我有以下 z3py 表达式：
import z3
x, y = z3.Ints("x y")
z3_expression = z3.Not(x<y)
此表达式以str() 保存并打印为Not(x < y)。我想知道是否有任何方法可以将该 Not() 运算符应用于表达式并更改不等式的符号，即我想删除该否定运算符并使表达式看起来像这样： z3_expression = (x >= y) ，括号不是必须的，我只是为了更清楚地加上括号。
有没有最好使用 z3py 的方法？
编辑： 第一个 answear 解决了这个具体问题，但是如果我将表达式更改为：
z3_expression = z3.Not(x<=y)
z3_simplified_expression = z3.simplify(z3_expression)
print(z3_simplified_expression)
这会打印：
Not(x <= y)
而不是：
x > y
在这种特殊情况下，是的：
from z3 import *
x, y = Ints("x y")
e = Not(x < y)
f = simplify(e)
print(f)
这会打印：
y <= x
但重要的是要强调您认为“简化”的内容 person/mathematicial 以及工具认为简单的内容可能并不总是匹配。也就是说，z3 可能会转换表达式（或根本不更改它），具体取决于许多因素。
函数simplify有很多选项。要查看它们，运行:
help_simplify()
您将看到以下打印内容：
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)
您可以根据需要使用它们。