2013-10-11 15 views
5

previous postでは、Z3Pyをオンラインで使用してオペアンプに関するいくつかの問題を解決しました。しかし、Z3Pyのオンラインサービスが中断されたので、私はZ3 SMT-LIBオンラインを使ってこのような問題を解決しようとしています。オペアンプの問題を解決するためにZ3 SMT-LIBをオンラインで使用する方法

例1:

enter image description here

は、この問題は次のコードを使用して解決され、以下の回路に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を使ってそのような方程式を解く方法は?

答えて

7

出力には3つの代数が含まれています。たとえば、Rは、多項式x^2 - 130 x - 2000の2番目のルート/ゼロに割り当てられます。これは多項式のゼロである不合理な数の正確な表現です。解釈が難しいかもしれません。したがって、Z3に10進表記を使用して結果を表示するよう依頼することもできます。

(set-option :pp-decimal true) 

Z3は、出力が切り捨てられていることを示すために?を付加します。 Hereは、このオプションで同じ問題です。このオプションを使用すると、次のような結果が得られます。

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)) 
) 
+1

ドクターレオナルドには、すばらしいことがたくさんあります。 –

関連する問題