Используйте Z3 и SMT-LIB для определения функции sqrt с вещественным числом.

Предположим, что ваша формула не содержит квантификаторов, тогда вы можете неявно определить квадратные корни, введя новые переменные и добавив ограничения. Например, вы можете написать:

  (define-fun is_sqrt ((x Real) (y Real)) Bool (= y (* x x)))

Тогда «х» — это квадратный корень из «у»; и если вам просто нужны неотрицательные квадратные корни, то:

  (define-fun is_sqrt ((x Real) (y Real)) Bool (and (>= x 0) (= y (* x x))))

Для каждого случая в вашем утверждении, где у вас есть квадратный корень, введите новую переменную и вставьте новую переменную в это место. Затем добавьте утверждение

   (assert (is_sqrt fresh-variable sub-term))

Z3 также предоставляет встроенный оператор для возведения терминов в степень. Вы можете использовать это, чтобы получить квадратный корень. Таким образом, чтобы записать квадратный корень из «x», вы можете написать термин:

   (^ x 0.5)

Вывод с использованием степеней в Z3 несколько ограничен, поэтому действительно зависит от того, что говорит ваша формула, будет ли эта формулировка обрабатываться так же, как реляционное кодирование.

Если вам на самом деле не нужна функция, то самый простой способ определить y как квадратный корень из x — это утверждать, что y * y = x , то есть:

; This will cause Z3 to return a decimal answer instead of a root-obj
(set-option :pp.decimal true)

; Option 1: inverse of multiplication. This works fine if you don't actually
; need to define a custom function. This will find y = 1.414... or y = -1.414...
(declare-fun y () Real)
(assert (= 2.0 (* y y)))

; Do this if you want to find the positive root y = 1.414...
(assert (>= y 0.0))

(check-sat)
(get-value (y))
(reset)

Другой способ, которым я пытался использовать неинтерпретируемые функции, выглядит следующим образом:

; Option 2: uninterpreted functions. Unfortunately Z3 seems to always return
; 'unknown' when sqrt is defined this way. Here we ignore the possibility that
; x < 0.0; fixing this doesn't help the situation, though.
(declare-fun sqrt (Real) Real)
(assert (forall ((x Real)) (= x (* (sqrt x) (sqrt x)))))
(declare-fun y () Real)
(assert (= y (sqrt 2.0)))
(check-sat)
(reset)

Наконец, самое простое, если вы используете Z3, — это использовать встроенный оператор мощности, предложенный Николаем. Вы можете использовать функцию, основанную на этой идее:

; Option 3: built-in power operator. This is not standard SMT-LIB, but works
; well with Z3.
(define-fun sqrt ((x Real)) Real (^ x 0.5))
(declare-fun y () Real)
(assert (= y (sqrt 2.0)))
(check-sat)
(get-value (y))
(reset)

Идея Николая по определению функции is_sqrt также является интересной и имеет то преимущество, что она не содержит кванторов, поэтому она будет работать с nlsat (самый мощный нелинейный решатель в Z3).