假設我有以下 z3py 運算式：
import z3
x, y = z3.Ints("x y")
z3_expression = z3.Not(x<y)
此運算式以str()as保存和列印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
uj5u.com熱心網友回復：
在這種特殊情況下，是的：
from z3 import *
x, y = Ints("x y")
e = Not(x < y)
f = simplify(e)
print(f)
這列印：
y <= x
但重要的是要強調你認為“簡化”的人/數學和工具認為簡單的可能并不總是匹配。也就是說，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)
您可以根據需要使用這些。
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/362844.html
上一篇：Python回圈隨機整數函式
下一篇：將罪放在3d中的段上