小编Jua*_*ina的帖子

在之前的文章中,使用Z3Py在线解决了涉及运算放大器的一些问题.但是现在Z3Py在线无法使用我试图在线使用Z3 SMT-LIB来解决这些问题.

例1:

在以下电路中找到R的值

使用以下代码解决此问题:

(declare-const R Real)
(declare-const V1 Real)
(declare-const V2 Real)
(declare-const Vo Real)
(declare-const I1 Real)
(declare-const I2 Real)
(declare-const g Real)
(assert (= (/ V1 (+ R -50)) I1))
(assert (= (/ V2 (+ R  10)) I2))
(assert (= (* (* R (+ I1 I2)) -1) g))
(assert (= Vo g))
(assert (= Vo -2))
(assert (= V1 1))
(assert (= V2 0.5))
(assert (> R 0))
(assert (> R 50))
(check-sat)
(get-model) …

证明的代码是

x, d = Reals('x d')
t = (simplify(simplify(((x + d)**2 - x**2)/d, som = True), mul_to_power=True))
print t
prove(Implies(d != 0, t == 2*x + d))
prove(Implies(d == 0, 2 * x + d == 2*x))

而输出是

(2·d·x + d2)/d
proved
proved

如果你知道使用Z3Py的更紧凑的证据,请告诉我.非常感谢.