module System.Process.Quick.Sbv.Arbitrary where

import System.Process.Quick.Prelude
import Data.SBV -- (Satisfiable, SymVal, Modelable (..), SString, sat, (.==), (.&&), literal)
import Data.SBV.String qualified as S
-- import Data.SBV.Control qualified as C
import System.IO.Unsafe (unsafePerformIO)
import Data.SBV.RegExp

getSingleValue :: (SymVal b, Modelable m) => m -> Maybe b
getSingleValue :: forall b m. (SymVal b, Modelable m) => m -> Maybe b
getSingleValue m
m
  | m -> Bool
forall a. Modelable a => a -> Bool
modelExists m
m =
    case Map String CV -> [(String, CV)]
forall t a b. (IsList t, Item t ~ (a, b)) => t -> [(a, b)]
toPairs (Map String CV -> [(String, CV)])
-> Map String CV -> [(String, CV)]
forall a b. (a -> b) -> a -> b
$ m -> Map String CV
forall a. Modelable a => a -> Map String CV
getModelDictionary m
m of
      [(String
k, CV
_)] -> String -> m -> Maybe b
forall b. SymVal b => String -> m -> Maybe b
forall a b. (Modelable a, SymVal b) => String -> a -> Maybe b
getModelValue String
k m
m
      [(String, CV)]
_ -> Maybe b
forall a. Maybe a
Nothing
  | Bool
otherwise = Maybe b
forall a. Maybe a
Nothing

-- models
satOne :: (Satisfiable a, SymVal b) => Int -> a -> Maybe b
satOne :: forall a b. (Satisfiable a, SymVal b) => Int -> a -> Maybe b
satOne Int
_n a
p = IO (Maybe b) -> Maybe b
forall a. IO a -> a
unsafePerformIO (SatResult -> Maybe b
forall b m. (SymVal b, Modelable m) => m -> Maybe b
getSingleValue (SatResult -> Maybe b) -> IO SatResult -> IO (Maybe b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat a
p)

satN :: (Satisfiable a, SymVal b) => Int -> a -> [b]
satN :: forall a b. (Satisfiable a, SymVal b) => Int -> a -> [b]
satN Int
n a
p = IO [b] -> [b]
forall a. IO a -> a
unsafePerformIO ((SMTResult -> Maybe b) -> [SMTResult] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SMTResult -> Maybe b
forall b m. (SymVal b, Modelable m) => m -> Maybe b
getSingleValue ([SMTResult] -> [b])
-> (AllSatResult -> [SMTResult]) -> AllSatResult -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AllSatResult -> [SMTResult]
allSatResults (AllSatResult -> [b]) -> IO AllSatResult -> IO [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO AllSatResult
asat)
  where
    asat :: IO AllSatResult
asat = SMTConfig -> a -> IO AllSatResult
forall a. Satisfiable a => SMTConfig -> a -> IO AllSatResult
allSatWith SMTConfig
defaultSMTCfg { allSatMaxModelCount = Just n } a
p

-- satStateless :: SymVal a => Int -> a -> Symbolic (Either String b)
-- satStateless seed p = unsafePerformIO go
--   where
--     solve ::
--     go = runSMT solve

findStringByRegex :: (SymVal b) => RegExp -> Gen b
findStringByRegex :: forall b. SymVal b => RegExp -> Gen b
findStringByRegex RegExp
r = Int -> Gen b
go (Int
3 :: Int)
  where
    go :: Int -> Gen b
go Int
t = (Int -> Gen b) -> Gen b
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen b) -> Gen b) -> (Int -> Gen b) -> Gen b
forall a b. (a -> b) -> a -> b
$ \Int
l ->
      if Int
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
        then do
          n <- (Int, Int) -> Gen Int
chooseInt (Int
0, Int
l)
          case trySat n of
            Just b
y -> b -> Gen b
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
y
            Maybe b
Nothing -> Int -> Gen b
go (Int -> Gen b) -> Int -> Gen b
forall a b. (a -> b) -> a -> b
$ Int
t Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
        else do
          case Int -> (SString -> SBool) -> [b]
forall a b. (Satisfiable a, SymVal b) => Int -> a -> [b]
satN Int
l SString -> SBool
matchRx of
            [] -> Text -> Gen b
forall a t. (HasCallStack, IsText t) => t -> a
error (Text -> Gen b) -> Text -> Gen b
forall a b. (a -> b) -> a -> b
$ Text
"No solution for regex: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RegExp -> Text
forall b a. (Show a, IsString b) => a -> b
show RegExp
r
            [b]
ss -> [b] -> Gen b
forall a. [a] -> Gen a
elements [b]
ss

    matchRx :: SString -> SBool
matchRx (SString
x :: SString) = SString -> RegExp -> SBool
forall a. RegExpMatchable a => a -> RegExp -> SBool
match SString
x RegExp
r

    trySat :: Int -> Maybe b
trySat Int
n =
      Int -> (SString -> SBool) -> Maybe b
forall a b. (Satisfiable a, SymVal b) => Int -> a -> Maybe b
satOne Int
n (\SString
x -> SString -> SBool
matchRx SString
x
                 SBool -> SBool -> SBool
.&& SString -> SInteger
S.length SString
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n))