La seule solution que je peux trouver est de faire une approximation de la racine carrée, mais cela ne fonctionne pas symboliquement, donc je ne peux pas l'utiliser pour prouver.Comment obtenir des fonctions de racine carrée et de logarithme symboliques dans SBV?
SBV soutient déjà la racine carrée pour les types à virgule flottante:
simple précision:
Prelude Data.SBV> sat $ \x -> x .== fpSqrt sRNE (4.2::SFloat)
Satisfiable. Model:
s0 = 2.04939 :: Float
double précision:
Prelude Data.SBV> sat $ \x -> x .== fpSqrt sRNE (4.2::SDouble)
Satisfiable. Model:
s0 = 2.04939015319192 :: Double
Notez que vous devez fournir un rounding- mode, dans ce qui précède, j'ai utilisé sRNE qui signifie round-nearest-towards-even qui est le mode d'arrondi par défaut utilisé dans Haskell. SBV prend en charge les 5 modes d'arrondi IEEE, si nécessaire.
Vous pouvez également utiliser reals (nombres réels algébriques-précision arbitraire):
Prelude Data.SBV> sat $ \x -> x * x .== (4.2::SReal)
Satisfiable. Model:
s0 = root(1, 5x^2 = 21) = -2.0493901531919196... :: Real
Dans ce cas, vous obtenez une équation algébrique, et une approximation du résultat réel-. (Notez dans ce qui précède que x*x == 4.2 est le même que 5*x^2 = 21). Les deux formulaires sont disponibles à partir de l'API programmatique.
Il n'y a pas de fonction unique pour les entiers-racines carrées; ni pour les logarithmes. Ces derniers peuvent être exprimés en utilisant des quantificateurs, mais les solveurs SMT sont peu susceptibles de produire de bons résultats car ils impliqueront à la fois l'arithmétique non linéaire et la quantification.
Notez en général que ni les solveurs SBV ni SMT ne sont bons pour "simplifier" les expressions symboliques. Vous obtiendrez toujours une réponse concrète pour votre requête: Si vous demandez sqrt 50, vous obtiendrez 7.07106 (dans le bon type/précision), au lieu de choses comme 5 * sqrt 2, par exemple.
Racine carrée à point flottant ou racine carrée réelle exacte ou racine carrée entière ou quoi? En outre, pour la racine carrée, ne pouvez-vous pas simplement ajouter une variable 'y' avec' y.> = 0' et 'y * y. == x'? –
@ReidBarton Idéalement, il agirait comme la fonction sqrt de Sage, de sorte que si je fais sqrt 50, cela me donne quelque chose comme 5 * sqrt 2. – Kytuzian