I just learn something about the[ operational amplifier knowledge.And I have know more about this amplifier like following:
What is operation amplifier
An operational amplifier (often op-amp or opamp) is a DC-coupled high-gain electronic voltage amplifier with a differential input and, usually, a single-ended output.[1] In this configuration, an op-amp produces an output potential (relative to circuit ground) that is typically hundreds of thousands of times larger than the potential difference between its input terminals. Operational amplifiers had their origins in analog computers, where they were used to perform mathematical operations in many linear, non-linear, and frequency-dependent circuits.
The popularity of the op-amp as a building block in analog circuits is due to its versatility. By using negative feedback, the characteristics of an op-amp circuit, its gain, input and output impedance, bandwidth etc. are determined by external components and have little dependence on temperature coefficients or engineering tolerance in the op-amp itself.
operation amplifiers working principle
The center of operational speaker is a differential intensifier. Two transistors are associated consecutive. Offer the current of a transverse current source. One transistor is the forward contribution of the operational speaker and the other is the turn around information. The forward info transistor is intensified and sent to a power intensifier circuit to intensify the yield. Along these lines, if the voltage of the forward info rises, the yield will normally increment. In the event that the reversed info voltage rises, the transformed and forward three-arrange cylinders share a steady current source. On the off chance that the current of the turn around three-arrange transistor is bigger, the forward one will be littler, so the yield will be lower. So it’s called invert input. Obviously, there are numerous other useful segments in the circuit, however the center is this.
However I still met trouble when I uses Z3Py online. But now that Z3Py online is out of service I am trying to solve such problems using Z3 SMT-LIB online.
This problem is solved using the following code:
(define-fun g_place ((state (State (Set Int) Bool Bool ))(b Int)) Bool
(= (open state) true)
)
<CODE> (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)
<CODE>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)) )
<CODE>(define-sort Set (T) (Array T Bool))
(declare-const x (Set Int) )
(declare-const y (Set Int) )
(define-fun set-union ((a1 (Set Int)) (a Int)) (Set Int)
(store a1 a true)
)
(define-fun union-sets ((a1 (Set Int)) (a2 (Set Int))) (Set Int)
((_ map or) a1 a2)
)
(declare-datatypes (T1 T2 T3)
(
(State
(payload
(bids T1)
(open T2)
(empty T3)
)
)
)
)(declare-const state (State (Set Int) Bool Bool))
(define-fun place ((state (State (Set Int) Bool Bool ))(b Int)) (State (Set Int) Bool Bool )
(payload (set-union (bids state) b) (open state) false )
)
(define-fun close ((state (State (Set Int) Bool Bool ))) (State (Set Int) Bool Bool )
(payload (bids state) false false )
)
(define-fun g_close ((state (State (Set Int) Bool Bool ))) Bool
(and (= (open state) true) (not (empty state)))
)
(def_close (close state))
)
)
))
(check-sat)
(get-model)