6

In a previous post some problems involving operational amplifiers were solved using Z3Py online. But now that Z3Py online is out of service I am trying to solve such problems using Z3 SMT-LIB online.

Example 1:

Find the value of R in the following circuit

enter image description here

This problem is solved using the following 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)

and the corresponding output is:

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

Run this example online here

As you can see the output from Z3 is a quadratic equation on x. Then the question is: How such equation could be solved using Z3?

Community
  • 1
  • 1
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15

1 Answers1

8

The output contains three algebraic numbers. For example, R is assigned to the 2nd root/zero of the polynomial x^2 - 130 x - 2000. This is a precise representation for irrational numbers that are zeros of polynomials. It may be hard to interpret. Thus, we can also ask Z3 to display the result using decimal notation. 

(set-option :pp-decimal true)

Z3 will append a ? to denote that the output is truncated. Here is the same problem with this option. With this option, we get the following output:

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))
)
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53