Skip to content

Instantly share code, notes, and snippets.

@Garciat
Last active August 10, 2017 17:37
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Garciat/3bf24dc94abe1f842f343ecf0dc95f1d to your computer and use it in GitHub Desktop.
Save Garciat/3bf24dc94abe1f842f343ecf0dc95f1d to your computer and use it in GitHub Desktop.
import Data.SBV
fruits :: SInteger -> SInteger -> SInteger -> SBool
fruits a b c = equation &&& positive
where
x = sFromIntegral a :: SReal
y = sFromIntegral b :: SReal
z = sFromIntegral c :: SReal
equation = x / (y + z) + y / (x + z) + z / (x + y) .== 4
positive = a .> 0 &&& b .> 0 &&& c .> 0
main :: IO ()
main = sat fruits >>= print
$ ghci Fruits.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Fruits.hs, interpreted )
Ok, 1 module loaded.
*Main> sat fruits
Unknown.
Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment