Jak używać Z3 SMT-LIB online do rozwiązywania problemów ze wzmacniaczami operacyjnymi

Question

Niektóre problemy związane z wzmacniaczami operacyjnymi zostały rozwiązane za pomocą Z3Py online. Ale teraz, gdy Z3Py online jest nieczynny, próbuję rozwiązać takie problemy za pomocą Z3 SMT-LIB online.

Przykład 1:

Znajdź wartość R w następującym układzie

Ten problem jest rozwiązany za pomocą następującego kodu:

(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) 

i odpowiednie wyjście :

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

uruchomić ten przykład w Internecie here

Jak widać wyjście z Z3 to równanie kwadratowe na x. Następnie pytanie brzmi: Jak takie równanie można rozwiązać za pomocą Z3?

Answer 1

Dane wyjściowe zawierają trzy liczby algebraiczne. Na przykład R jest przypisany do drugiego korzenia/zera wielomianu x^2 - 130 x - 2000. Jest to dokładna reprezentacja liczb irracjonalnych, które są zerami wielomianów. Może to być trudne do zinterpretowania. W związku z tym możemy poprosić Z3 o wyświetlenie wyniku za pomocą zapisu dziesiętnego.

(set-option :pp-decimal true) 

Z3 dołączania ? oznaczać, że wyjście jest obcinane. Here to ten sam problem z tą opcją. Z tą opcją uzyskujemy następujące dane wyjściowe:

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