Z3支持平方根 [英] Z3 support for square root
本文介绍了Z3支持平方根的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
我一直在搜索Z3提供的平方根功能。例如,对于添加关于实数x的约束,即x*x=2,对其进行编码的最佳方式是什么?
我已尝试:
(declare-const x Real)
(assert (= 2 (* x x)))
(check-sat)
结果未知。该模型也不可用。
然而,我相信应该有一种方法来满足这一点。我指的是SMT-lib 2.0语言的扩展版本,而不是pythonAPI。
推荐答案
您需要使用非线性求解器。您的示例没有自动检测和使用它的原因是因为常量2
:它被解析为整数而不是实数,因此从技术上讲,它是整数和实数的组合理论,而非线性求解器可能只涉及实数,除非您强制它。要强制使用它,可以使用check-sat-using
和非线性求解器qfnra-nlsat
(rise4un link:http://rise4fun.com/Z3/fXDp):
(declare-const x Real)
(push)
(assert (= 2 (* x x)))
(check-sat-using qfnra-nlsat) ; sat
(get-model)
; may have to play with printing options as this is irrational (or this may be a bug)
; (model
; (define-fun x () Real
; (/ 5.0 4.0))
;)
(pop)
; the reason you need to use check-sat-using is because the 2 gets parsed into an integer; to force it to be a real, use a decimal:
(push)
(assert (= 2.0 (* x x)))
(check-sat) ; sat
(get-model)
;(model
; (define-fun x () Real
; (root-obj (+ (^ x 2) (- 2)) 1))
;)
(pop)
对于一般指数(平方根等),可以使用^进行求幂:
; you can also use ^ for exponentiation
(push)
(assert (= 2.0 (^ x 2.0)))
(check-sat) ; sat
(get-model)
; (model
; (define-fun x () Real
; (root-obj (+ (^ x 2) (- 2)) 1))
;)
(pop)
; to represent square root, etc., you may use fractional or decimal exponents
(push)
(assert (= 25.0 (^ x 0.5))) ; square root: 2 = sqrt(x)
(check-sat) ; sat
(get-model)
; maybe a bug or have to tune the model printer
;(model
; (define-fun x () Real
; (- 1.0))
;)
(pop)
(push)
(assert (= 2.0 (^ x (/ 1.0 3.0))))
(check-sat) ; sat
(get-model)
;(model
; (define-fun x () Real
; 8.0)
;)
(pop)
(push)
(assert (= 10.0 (^ x 0.2)))
(check-sat) ; sat
(get-model)
;(model
; (define-fun x () Real
; 100000.0)
;)
(pop)
这是一个古老但相关的帖子:z3/python reals
某些打印问题,例如,如果您需要小数近似值,可以使用以下命令修复:
(set-option :pp.decimal true)
这篇关于Z3支持平方根的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文