6

在之前的一篇文章中，使用 Z3Py 在线解决了一些涉及运算放大器的问题。但是现在 Z3Py online 已停止服务，我正在尝试使用 Z3 SMT-LIB online 解决此类问题。

示例 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)

相应的输出是：

sat 
(model (define-fun R () Real (root-obj (+ (^ x 2) (* (- 130) x) (- 2000)) 2)) 
       (define-fun I1 () Real (root-obj (+ (* 6000 (^ x 2)) (* 30 x) (- 1)) 2)) 
       (define-fun I2 () Real (root-obj (+ (* 2400 (^ x 2)) (* 300 x) (- 1)) 2)) 
       (define-fun V2 () Real (/ 1.0 2.0)) 
       (define-fun V1 () Real 1.0) 
       (define-fun Vo () Real (- 2.0)) 
       (define-fun g () Real (- 2.0)) )

在此处在线运行此示例

如您所见，Z3 的输出是 x 上的二次方程。那么问题是：如何使用 Z3 求解这样的方程？

4

1 回答 1

8

输出包含三个代数数。例如，R分配给多项式的第二个根/零x^2 - 130 x - 2000。这是多项式零的无理数的精确表示。可能很难解释。因此，我们也可以要求 Z3 使用十进制表示法显示结果。

(set-option :pp-decimal true)

Z3 将附加一个?以表示输出被截断。 这个选项也有同样的问题。使用此选项，我们得到以下输出：

sat
(model 
  (define-fun R () Real
    143.8986691902?)
  (define-fun I1 () Real
    0.0106497781?)
  (define-fun I2 () Real
    0.0032488909?)
  (define-fun V2 () Real
    0.5)
  (define-fun V1 () Real
    1.0)
  (define-fun Vo () Real
    (- 2.0))
  (define-fun g () Real
    (- 2.0))
)
于 2013-10-12T19:09:09.817 回答