previous postでは、Z3Pyをオンラインで使用してオペアンプに関するいくつかの問題を解決しました。しかし、Z3Pyのオンラインサービスが中断されたので、私はZ3 SMT-LIBオンラインを使ってこのような問題を解決しようとしています。オペアンプの問題を解決するために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)
を、対応する出力であります:
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)))
0あなたがZ3からの出力は、xの二次方程式で見ることができるように
はオンラインhere
この例を実行します。それでは、問題は次のようなものです。Z3を使ってそのような方程式を解く方法は?
ドクターレオナルドには、すばらしいことがたくさんあります。 –