{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE KindSignatures #-}
module Test.IOTasks.Z3 (
  findPathInput, printPathScript, evalPathScript,
  satPaths, satPathsQ, isSatPath, SatResult(..), Timeout,
  PathInjector(..), mkPathInjector,
  ) where

import Test.IOTasks.Constraints
import Test.IOTasks.Internal.ValueSet
import Test.IOTasks.Internal.Term
import Test.IOTasks.Var (Var(..), SomeVar, pattern SomeVar, pattern Var, VarExp(..), someVar, Embeddable (..), varname)
import Test.IOTasks.ValueMap

import Z3.Monad
import Z3.Base (Goal)

import Test.QuickCheck (generate, vectorOf, elements)

import Control.Applicative (liftA2) -- not redundant for base-4.17.x.x and below!
import Control.Concurrent.STM

import Control.Monad
import Control.Monad.State

import Data.Maybe (catMaybes, fromMaybe, mapMaybe, fromJust)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Tuple.Extra (fst3, thd3)

import Data.List as List
import Test.QuickCheck.Gen (Gen)
import Type.Reflection
import Type.Match
import Data.List.Extra
import Control.Monad.Reader
import Data.Kind (Type)
import Data.Some (Some(Some))

type Z3R = ReaderT ImplicitParameters Z3

data ImplicitParameters = ImplicitParameter { ImplicitParameters -> Integer
valueSizeParameter :: Integer, ImplicitParameters -> Int
maxSeqLengthParameter :: Int }

type Timeout = Int

findPathInput :: Timeout -> Path -> Integer -> Int -> Bool -> IO (SatResult [String])
findPathInput :: Int -> Path -> Integer -> Int -> Bool -> IO (SatResult [String])
findPathInput Int
t Path
p Integer
bound Int
maxSeqLength Bool
checkOverflows = (SatResult [String], String) -> SatResult [String]
forall a b. (a, b) -> a
fst ((SatResult [String], String) -> SatResult [String])
-> IO (SatResult [String], String) -> IO (SatResult [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Path
-> Integer
-> Int
-> Bool
-> IO (SatResult [String], String)
evalPathScript Int
t Path
p Integer
bound Int
maxSeqLength Bool
checkOverflows

printPathScript :: Timeout -> Path -> Integer -> Int -> Bool -> IO String
printPathScript :: Int -> Path -> Integer -> Int -> Bool -> IO String
printPathScript Int
t Path
p Integer
bound Int
maxSeqLength Bool
checkOverflows = (SatResult [String], String) -> String
forall a b. (a, b) -> b
snd ((SatResult [String], String) -> String)
-> IO (SatResult [String], String) -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Path
-> Integer
-> Int
-> Bool
-> IO (SatResult [String], String)
evalPathScript Int
t Path
p Integer
bound Int
maxSeqLength Bool
checkOverflows

evalPathScript :: Timeout -> Path -> Integer -> Int -> Bool -> IO (SatResult [String],String)
evalPathScript :: Int
-> Path
-> Integer
-> Int
-> Bool
-> IO (SatResult [String], String)
evalPathScript Int
t Path
p Integer
bound Int
maxSeqLength Bool
checkOverflows = do
  Maybe Logic
-> Opts
-> Z3 (SatResult [String], String)
-> IO (SatResult [String], String)
forall a. Maybe Logic -> Opts -> Z3 a -> IO a
evalZ3With Maybe Logic
forall a. Maybe a
Nothing (Opts
stdOpts Opts -> Opts -> Opts
+? String -> String -> Opts
forall val. OptValue val => String -> val -> Opts
opt String
"timeout" (Int -> String
forall a. Show a => a -> String
show Int
t)) (Z3 (SatResult [String], String)
 -> IO (SatResult [String], String))
-> Z3 (SatResult [String], String)
-> IO (SatResult [String], String)
forall a b. (a -> b) -> a -> b
$ ReaderT ImplicitParameters Z3 (SatResult [String], String)
-> ImplicitParameters -> Z3 (SatResult [String], String)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Path
-> ScriptMode
-> Bool
-> ReaderT ImplicitParameters Z3 (SatResult [String], String)
pathScript Path
p ScriptMode
WithSoft Bool
checkOverflows) ImplicitParameters
implicits
  where implicits :: ImplicitParameters
implicits = ImplicitParameter {valueSizeParameter :: Integer
valueSizeParameter=Integer
bound, maxSeqLengthParameter :: Int
maxSeqLengthParameter=Int
maxSeqLength}

data SatResult a = SAT a | NotSAT | Timeout deriving (SatResult a -> SatResult a -> Bool
(SatResult a -> SatResult a -> Bool)
-> (SatResult a -> SatResult a -> Bool) -> Eq (SatResult a)
forall a. Eq a => SatResult a -> SatResult a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => SatResult a -> SatResult a -> Bool
== :: SatResult a -> SatResult a -> Bool
$c/= :: forall a. Eq a => SatResult a -> SatResult a -> Bool
/= :: SatResult a -> SatResult a -> Bool
Eq, Int -> SatResult a -> ShowS
[SatResult a] -> ShowS
SatResult a -> String
(Int -> SatResult a -> ShowS)
-> (SatResult a -> String)
-> ([SatResult a] -> ShowS)
-> Show (SatResult a)
forall a. Show a => Int -> SatResult a -> ShowS
forall a. Show a => [SatResult a] -> ShowS
forall a. Show a => SatResult a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> SatResult a -> ShowS
showsPrec :: Int -> SatResult a -> ShowS
$cshow :: forall a. Show a => SatResult a -> String
show :: SatResult a -> String
$cshowList :: forall a. Show a => [SatResult a] -> ShowS
showList :: [SatResult a] -> ShowS
Show, (forall a b. (a -> b) -> SatResult a -> SatResult b)
-> (forall a b. a -> SatResult b -> SatResult a)
-> Functor SatResult
forall a b. a -> SatResult b -> SatResult a
forall a b. (a -> b) -> SatResult a -> SatResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SatResult a -> SatResult b
fmap :: forall a b. (a -> b) -> SatResult a -> SatResult b
$c<$ :: forall a b. a -> SatResult b -> SatResult a
<$ :: forall a b. a -> SatResult b -> SatResult a
Functor)

isSatPath :: Timeout -> Path-> Int -> Bool -> IO (SatResult ())
isSatPath :: Int -> Path -> Int -> Bool -> IO (SatResult ())
isSatPath Int
t Path
p Int
maxSeqLength Bool
checkOverflows = do
  (SatResult [String]
mRes,String
_) <- Maybe Logic
-> Opts
-> Z3 (SatResult [String], String)
-> IO (SatResult [String], String)
forall a. Maybe Logic -> Opts -> Z3 a -> IO a
evalZ3With Maybe Logic
forall a. Maybe a
Nothing (Opts
stdOpts Opts -> Opts -> Opts
+? String -> String -> Opts
forall val. OptValue val => String -> val -> Opts
opt String
"timeout" (Int -> String
forall a. Show a => a -> String
show Int
t)) (Z3 (SatResult [String], String)
 -> IO (SatResult [String], String))
-> Z3 (SatResult [String], String)
-> IO (SatResult [String], String)
forall a b. (a -> b) -> a -> b
$ ReaderT ImplicitParameters Z3 (SatResult [String], String)
-> ImplicitParameters -> Z3 (SatResult [String], String)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Path
-> ScriptMode
-> Bool
-> ReaderT ImplicitParameters Z3 (SatResult [String], String)
pathScript Path
p ScriptMode
WithoutSoft Bool
checkOverflows) ImplicitParameters
implicits
  SatResult () -> IO (SatResult ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SatResult () -> IO (SatResult ()))
-> SatResult () -> IO (SatResult ())
forall a b. (a -> b) -> a -> b
$ SatResult [String] -> SatResult ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void SatResult [String]
mRes
  where implicits :: ImplicitParameters
implicits = ImplicitParameter {valueSizeParameter :: Integer
valueSizeParameter= String -> Integer
forall a. HasCallStack => String -> a
error String
"isSatPath: valueSize not available in isSatPath", maxSeqLengthParameter :: Int
maxSeqLengthParameter=Int
maxSeqLength}

data ScriptMode = WithSoft | WithoutSoft

data SearchContext = NoContext | LastNotSAT Int | RequirePruningCheck

-- depth is currently not used to trigger pruning
updateContext :: SatResult a -> Int -> SearchContext -> SearchContext
updateContext :: forall a. SatResult a -> Int -> SearchContext -> SearchContext
updateContext (SAT a
_) Int
_ SearchContext
_ = SearchContext
NoContext
updateContext SatResult a
Timeout Int
_ SearchContext
_ = SearchContext
NoContext
updateContext SatResult a
NotSAT Int
d SearchContext
NoContext = Int -> SearchContext
LastNotSAT Int
d
updateContext SatResult a
NotSAT Int
_ (LastNotSAT Int
_) = SearchContext
RequirePruningCheck
updateContext SatResult a
_ Int
_ SearchContext
RequirePruningCheck = String -> SearchContext
forall a. HasCallStack => String -> a
error String
"updateContext: should not happen"

type PrefixPath = [Some SimpleConstraint]
satPaths :: Int -> Int -> ConstraintTree -> Int -> Bool -> IO [SimplePath]
satPaths :: Int -> Int -> ConstraintTree -> Int -> Bool -> IO [SimplePath]
satPaths Int
maxUnfolds Int
to ConstraintTree
t Int
maxSeqLength Bool
checkOverflows = do
  TQueue (Maybe SimplePath)
q <- STM (TQueue (Maybe SimplePath)) -> IO (TQueue (Maybe SimplePath))
forall a. STM a -> IO a
atomically STM (TQueue (Maybe SimplePath))
forall a. STM (TQueue a)
newTQueue
  TVar (Maybe Int)
nVar <- Maybe Int -> IO (TVar (Maybe Int))
forall a. a -> IO (TVar a)
newTVarIO Maybe Int
forall a. Maybe a
Nothing
  TVar (Maybe Int)
-> Int
-> ConstraintTree
-> Int
-> Int
-> Bool
-> TQueue (Maybe SimplePath)
-> IO ()
satPathsQ TVar (Maybe Int)
nVar Int
to ConstraintTree
t Int
maxUnfolds Int
maxSeqLength Bool
checkOverflows TQueue (Maybe SimplePath)
q
  (Maybe SimplePath -> SimplePath)
-> [Maybe SimplePath] -> [SimplePath]
forall a b. (a -> b) -> [a] -> [b]
map Maybe SimplePath -> SimplePath
forall a. HasCallStack => Maybe a -> a
fromJust ([Maybe SimplePath] -> [SimplePath])
-> ([Maybe SimplePath] -> [Maybe SimplePath])
-> [Maybe SimplePath]
-> [SimplePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe SimplePath] -> [Maybe SimplePath]
forall a. HasCallStack => [a] -> [a]
init ([Maybe SimplePath] -> [SimplePath])
-> IO [Maybe SimplePath] -> IO [SimplePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM [Maybe SimplePath] -> IO [Maybe SimplePath]
forall a. STM a -> IO a
atomically (TQueue (Maybe SimplePath) -> STM [Maybe SimplePath]
forall a. TQueue a -> STM [a]
flushTQueue TQueue (Maybe SimplePath)
q)

satPathsQ :: TVar (Maybe Int) -> Int -> ConstraintTree -> Int -> Int -> Bool -> TQueue (Maybe SimplePath) -> IO ()
satPathsQ :: TVar (Maybe Int)
-> Int
-> ConstraintTree
-> Int
-> Int
-> Bool
-> TQueue (Maybe SimplePath)
-> IO ()
satPathsQ TVar (Maybe Int)
nVar Int
to ConstraintTree
t Int
maxUnfolds Int
maxSeqLength Bool
checkOverflows TQueue (Maybe SimplePath)
q = do
  StateT SearchContext IO () -> SearchContext -> IO ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
0 Int
0 Int
to ConstraintTree
t ([],PrefixPath -> SimplePath
ClosedPath [],Int
0) TQueue (Maybe SimplePath)
q) SearchContext
NoContext
  STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TQueue (Maybe SimplePath) -> Maybe SimplePath -> STM ()
forall a. TQueue a -> a -> STM ()
writeTQueue TQueue (Maybe SimplePath)
q Maybe SimplePath
forall a. Maybe a
Nothing
  where
    -- nUnfolds: number of Unfolds on current path
    -- nInputs: number of inputs on current path (path length)
    -- to: solver timeout
    -- (s,d,e): current prefix path, depth of current position in the tree (d =/= path length), current symbolic environment
    satPaths' :: Int -> Int -> Int -> ConstraintTree -> (PrefixPath,SimplePath,Int) -> TQueue (Maybe SimplePath) -> StateT SearchContext IO ()
    satPaths' :: Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
_ Int
_ Int
to ConstraintTree
Empty (PrefixPath
_,SimplePath
p,Int
d) TQueue (Maybe SimplePath)
q = do
      let basePath :: Path
basePath = [Int] -> SimplePath -> Path
completePath [] SimplePath
p
      SatResult ()
res <- IO (SatResult ()) -> StateT SearchContext IO (SatResult ())
forall (m :: * -> *) a. Monad m => m a -> StateT SearchContext m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (SatResult ()) -> StateT SearchContext IO (SatResult ()))
-> IO (SatResult ()) -> StateT SearchContext IO (SatResult ())
forall a b. (a -> b) -> a -> b
$ Int -> Path -> Int -> Bool -> IO (SatResult ())
isSatPath Int
to Path
basePath Int
maxSeqLength Bool
checkOverflows
      (SearchContext -> SearchContext) -> StateT SearchContext IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SearchContext -> SearchContext) -> StateT SearchContext IO ())
-> (SearchContext -> SearchContext) -> StateT SearchContext IO ()
forall a b. (a -> b) -> a -> b
$ SatResult () -> Int -> SearchContext -> SearchContext
forall a. SatResult a -> Int -> SearchContext -> SearchContext
updateContext SatResult ()
res Int
d
      Bool -> StateT SearchContext IO () -> StateT SearchContext IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SatResult ()
res SatResult () -> SatResult () -> Bool
forall a. Eq a => a -> a -> Bool
== () -> SatResult ()
forall a. a -> SatResult a
SAT ()) (StateT SearchContext IO () -> StateT SearchContext IO ())
-> StateT SearchContext IO () -> StateT SearchContext IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> StateT SearchContext IO ()
forall (m :: * -> *) a. Monad m => m a -> StateT SearchContext m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT SearchContext IO ())
-> IO () -> StateT SearchContext IO ()
forall a b. (a -> b) -> a -> b
$ STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TQueue (Maybe SimplePath) -> Maybe SimplePath -> STM ()
forall a. TQueue a -> a -> STM ()
writeTQueue TQueue (Maybe SimplePath)
q (Maybe SimplePath -> STM ()) -> Maybe SimplePath -> STM ()
forall a b. (a -> b) -> a -> b
$ SimplePath -> Maybe SimplePath
forall a. a -> Maybe a
Just SimplePath
p
    satPaths' Int
nUnfolds Int
nInputs Int
to (Choice ConstraintTree
l ConstraintTree
r) (PrefixPath
s,SimplePath
p,Int
d) TQueue (Maybe SimplePath)
q = do
      Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
nUnfolds Int
nInputs Int
to ConstraintTree
l (PrefixPath
s,SimplePath
p,Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) TQueue (Maybe SimplePath)
q
      SearchContext
ctx <- StateT SearchContext IO SearchContext
forall s (m :: * -> *). MonadState s m => m s
get
      case SearchContext
ctx of
        SearchContext
RequirePruningCheck -> do
          let prefix :: Path
prefix = PrefixPath -> Path
addEnvToPath (PrefixPath -> Path) -> PrefixPath -> Path
forall a b. (a -> b) -> a -> b
$ PrefixPath -> PrefixPath
forall a. [a] -> [a]
reverse PrefixPath
s
          SatResult ()
res <- IO (SatResult ()) -> StateT SearchContext IO (SatResult ())
forall (m :: * -> *) a. Monad m => m a -> StateT SearchContext m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (SatResult ()) -> StateT SearchContext IO (SatResult ()))
-> IO (SatResult ()) -> StateT SearchContext IO (SatResult ())
forall a b. (a -> b) -> a -> b
$ Int -> Path -> Int -> Bool -> IO (SatResult ())
isSatPath Int
to Path
prefix Int
maxSeqLength Bool
checkOverflows
          case SatResult ()
res of
            SatResult ()
NotSAT -> () -> StateT SearchContext IO ()
forall a. a -> StateT SearchContext IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            SatResult ()
Timeout -> do
              SearchContext -> StateT SearchContext IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SearchContext
NoContext
              Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
nUnfolds Int
nInputs Int
to ConstraintTree
r (PrefixPath
s,SimplePath
p,Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) TQueue (Maybe SimplePath)
q
            SAT () -> do
              SearchContext -> StateT SearchContext IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put SearchContext
NoContext
              Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
nUnfolds Int
nInputs Int
to ConstraintTree
r (PrefixPath
s,SimplePath
p,Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) TQueue (Maybe SimplePath)
q
        SearchContext
_ -> do
          Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
nUnfolds Int
nInputs Int
to ConstraintTree
r (PrefixPath
s,SimplePath
p,Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) TQueue (Maybe SimplePath)
q
    satPaths' Int
nUnfolds Int
nInputs Int
to (Assert c :: SimpleConstraint t
c@SimpleInput{} ConstraintTree
t) (PrefixPath
s,SimplePath
p,Int
d) TQueue (Maybe SimplePath)
q = do
      Maybe Int
currentMaxPathLength <- IO (Maybe Int) -> StateT SearchContext IO (Maybe Int)
forall (m :: * -> *) a. Monad m => m a -> StateT SearchContext m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe Int) -> StateT SearchContext IO (Maybe Int))
-> IO (Maybe Int) -> StateT SearchContext IO (Maybe Int)
forall a b. (a -> b) -> a -> b
$ TVar (Maybe Int) -> IO (Maybe Int)
forall a. TVar a -> IO a
readTVarIO TVar (Maybe Int)
nVar
      case Maybe Int
currentMaxPathLength of
        Just Int
len | Int
nInputs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len -> () -> StateT SearchContext IO ()
forall a. a -> StateT SearchContext IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Maybe Int
_ -> Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
nUnfolds (Int
nInputsInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
to ConstraintTree
t (SimpleConstraint t -> Some SimpleConstraint
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some SimpleConstraint t
cSome SimpleConstraint -> PrefixPath -> PrefixPath
forall a. a -> [a] -> [a]
:PrefixPath
s,SimplePath
p SimplePath -> SimplePath -> SimplePath
`appendPath` PrefixPath -> SimplePath
ClosedPath [SimpleConstraint t -> Some SimpleConstraint
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some SimpleConstraint t
c],Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) TQueue (Maybe SimplePath)
q -- stores constraints in reversed order
    satPaths' Int
nUnfolds Int
nInputs Int
to (Assert SimpleConstraint t
c ConstraintTree
t) (PrefixPath
s,SimplePath
p,Int
d) TQueue (Maybe SimplePath)
q = Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
nUnfolds Int
nInputs Int
to ConstraintTree
t (SimpleConstraint t -> Some SimpleConstraint
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some SimpleConstraint t
cSome SimpleConstraint -> PrefixPath -> PrefixPath
forall a. a -> [a] -> [a]
:PrefixPath
s,SimplePath
p SimplePath -> SimplePath -> SimplePath
`appendPath` PrefixPath -> SimplePath
ClosedPath [SimpleConstraint t -> Some SimpleConstraint
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some SimpleConstraint t
c],Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) TQueue (Maybe SimplePath)
q -- stores constraints in reversed order
    satPaths' Int
nUnfolds Int
nInputs Int
to (Unfold ConstraintTree
t) (PrefixPath
s,SimplePath
p,Int
d) TQueue (Maybe SimplePath)
q
      | Int
nUnfolds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxUnfolds = Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' (Int
nUnfoldsInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
nInputs Int
to ConstraintTree
t (PrefixPath
s,SimplePath
p,Int
d) TQueue (Maybe SimplePath)
q
      | Bool
otherwise = () -> StateT SearchContext IO ()
forall a. a -> StateT SearchContext IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    satPaths' Int
nUnfolds Int
nInputs Int
to (InjectionPoint SimpleConstraint 'Input
c ConstraintTree
t) (PrefixPath
s,SimplePath
p,Int
d) TQueue (Maybe SimplePath)
q = Int
-> Int
-> Int
-> ConstraintTree
-> (PrefixPath, SimplePath, Int)
-> TQueue (Maybe SimplePath)
-> StateT SearchContext IO ()
satPaths' Int
nUnfolds Int
nInputs Int
to ConstraintTree
t (PrefixPath
s,SimplePath
p SimplePath -> SimplePath -> SimplePath
`appendPath` PrefixPath -> SimpleConstraint 'Input -> SimplePath -> SimplePath
forall (t :: ConstraintType).
PrefixPath -> SimpleConstraint t -> SimplePath -> SimplePath
OpenPath [] SimpleConstraint 'Input
c (PrefixPath -> SimplePath
ClosedPath []),Int
d) TQueue (Maybe SimplePath)
q

newtype PathInjector = PathInjector { PathInjector -> Int -> Gen Path
injectNegatives :: Int -> Gen Path }

mkPathInjector :: SimplePath -> Timeout -> Int -> Bool -> IO PathInjector
mkPathInjector :: SimplePath -> Int -> Int -> Bool -> IO PathInjector
mkPathInjector (ClosedPath PrefixPath
cs) Int
_ Int
_ Bool
_ = PathInjector -> IO PathInjector
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PathInjector -> IO PathInjector)
-> (Path -> PathInjector) -> Path -> IO PathInjector
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Gen Path) -> PathInjector
PathInjector ((Int -> Gen Path) -> PathInjector)
-> (Path -> Int -> Gen Path) -> Path -> PathInjector
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen Path -> Int -> Gen Path
forall a b. a -> b -> a
const (Gen Path -> Int -> Gen Path)
-> (Path -> Gen Path) -> Path -> Int -> Gen Path
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Path -> Gen Path
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Path -> IO PathInjector) -> Path -> IO PathInjector
forall a b. (a -> b) -> a -> b
$ PrefixPath -> Path
addEnvToPath PrefixPath
cs
mkPathInjector p :: SimplePath
p@OpenPath{} Int
to Int
maxSeqLength Bool
checkOverflows = do
  [Int]
validPoints <- Int -> SimplePath -> Int -> Bool -> IO [Int]
validInjectionPoints Int
to SimplePath
p Int
maxSeqLength Bool
checkOverflows
  PathInjector -> IO PathInjector
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PathInjector -> IO PathInjector)
-> PathInjector -> IO PathInjector
forall a b. (a -> b) -> a -> b
$ (Int -> Gen Path) -> PathInjector
PathInjector ((Int -> Gen Path) -> PathInjector)
-> (Int -> Gen Path) -> PathInjector
forall a b. (a -> b) -> a -> b
$ \Int
n -> do
    [Int]
is <- [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Int]) -> Gen [Int] -> Gen [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen Int -> Gen [Int]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n ([Int] -> Gen Int
forall a. [a] -> Gen a
elements [Int]
validPoints)
    Path -> Gen Path
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Path -> Gen Path) -> Path -> Gen Path
forall a b. (a -> b) -> a -> b
$ [Int] -> SimplePath -> Path
completePath [Int]
is SimplePath
p

validInjectionPoints :: Timeout -> SimplePath -> Int -> Bool -> IO [Int]
validInjectionPoints :: Int -> SimplePath -> Int -> Bool -> IO [Int]
validInjectionPoints Int
to SimplePath
p Int
maxSeqLength Bool
checkOverflows = [Int] -> IO [Int]
searchPoints [Int
1..SimplePath -> Int
injectionPoints SimplePath
p]
  where
    searchPoints :: [Int] -> IO [Int]
searchPoints [Int]
xs
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
8 = ([(Int, SatResult ())] -> [Int])
-> IO [(Int, SatResult ())] -> IO [Int]
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Int, SatResult ())] -> [Int]
filterSATs (IO [(Int, SatResult ())] -> IO [Int])
-> IO [(Int, SatResult ())] -> IO [Int]
forall a b. (a -> b) -> a -> b
$ [Int]
-> (Int -> IO (Int, SatResult ())) -> IO [(Int, SatResult ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
xs ((Int -> IO (Int, SatResult ())) -> IO [(Int, SatResult ())])
-> (Int -> IO (Int, SatResult ())) -> IO [(Int, SatResult ())]
forall a b. (a -> b) -> a -> b
$ \Int
i -> (Int
i,) (SatResult () -> (Int, SatResult ()))
-> IO (SatResult ()) -> IO (Int, SatResult ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Path -> Int -> Bool -> IO (SatResult ())
isSatPath Int
to ([Int] -> SimplePath -> Path
completePath [Int
i] SimplePath
p) Int
maxSeqLength Bool
checkOverflows
      | Bool
otherwise = do
        SatResult ()
res <- Int -> Path -> Int -> Bool -> IO (SatResult ())
isSatPath Int
to ([Int] -> SimplePath -> Path
completePath [Int]
xs SimplePath
p) Int
maxSeqLength Bool
checkOverflows
        case SatResult ()
res of
          SAT () -> [Int] -> IO [Int]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Int]
xs
          SatResult ()
_ ->
            let ([Int]
l,[Int]
r) = Int -> [Int] -> ([Int], [Int])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [Int]
xs
            in ([Int] -> [Int] -> [Int]) -> IO [Int] -> IO [Int] -> IO [Int]
forall a b c. (a -> b -> c) -> IO a -> IO b -> IO c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
(++) ([Int] -> IO [Int]
searchPoints [Int]
l) ([Int] -> IO [Int]
searchPoints [Int]
r)
      where n :: Int
n = [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs

    filterSATs :: [(Int,SatResult ())] -> [Int]
    filterSATs :: [(Int, SatResult ())] -> [Int]
filterSATs [(Int, SatResult ())]
xs = [ Int
i | (Int
i,SatResult ()
r) <- [(Int, SatResult ())]
xs, SatResult ()
r SatResult () -> SatResult () -> Bool
forall a. Eq a => a -> a -> Bool
== () -> SatResult ()
forall a. a -> SatResult a
SAT () ]


data ValueGenerator where
  ValueGenerator :: Typeable v => (ValueMap -> Size -> Gen v) -> ValueGenerator

withGeneratedValue :: (forall v. Typeable v => v -> r) -> ValueGenerator -> ValueMap -> Size -> IO r
withGeneratedValue :: forall r.
(forall v. Typeable v => v -> r)
-> ValueGenerator -> ValueMap -> Size -> IO r
withGeneratedValue forall v. Typeable v => v -> r
f (ValueGenerator ValueMap -> Size -> Gen v
g) ValueMap
m Size
sz = v -> r
forall v. Typeable v => v -> r
f (v -> r) -> IO v -> IO r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen v -> IO v
forall a. Gen a -> IO a
generate (ValueMap -> Size -> Gen v
g ValueMap
m Size
sz)

pathScript :: Path -> ScriptMode -> Bool -> Z3R (SatResult [String], String)
pathScript :: Path
-> ScriptMode
-> Bool
-> ReaderT ImplicitParameters Z3 (SatResult [String], String)
pathScript Path
path ScriptMode
mode Bool
checkOverflows = do
  let ([Constraint 'Input]
tyConstr,[Constraint 'Condition]
predConstr,[Constraint 'Overflow]
overflowConstr) = Path
-> ([Constraint 'Input], [Constraint 'Condition],
    [Constraint 'Overflow])
partitionPath Path
path

  Goal
goal <- Bool -> Bool -> Bool -> ReaderT ImplicitParameters Z3 Goal
forall (z3 :: * -> *).
MonadZ3 z3 =>
Bool -> Bool -> Bool -> z3 Goal
mkGoal Bool
True Bool
False Bool
False
  [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars <- [Constraint 'Input]
-> (Constraint 'Input
    -> ReaderT
         ImplicitParameters Z3 (((SomeVar, Int), AST, Int), ValueGenerator))
-> ReaderT
     ImplicitParameters
     Z3
     [(((SomeVar, Int), AST, Int), ValueGenerator)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Constraint 'Input]
tyConstr ((Constraint 'Input
  -> ReaderT
       ImplicitParameters Z3 (((SomeVar, Int), AST, Int), ValueGenerator))
 -> ReaderT
      ImplicitParameters
      Z3
      [(((SomeVar, Int), AST, Int), ValueGenerator)])
-> (Constraint 'Input
    -> ReaderT
         ImplicitParameters Z3 (((SomeVar, Int), AST, Int), ValueGenerator))
-> ReaderT
     ImplicitParameters
     Z3
     [(((SomeVar, Int), AST, Int), ValueGenerator)]
forall a b. (a -> b) -> a -> b
$
    \(InputConstraint (iVar :: Var v
iVar@(Var (String
x,TypeRep v
_)),Int
i) (ValueSet v
vs :: ValueSet v) Map SomeVar SymbolicInfo
e) -> do
      AST
var <- String -> Sort -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => String -> Sort -> z3 AST
mkFreshVar (String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) (Sort -> ReaderT ImplicitParameters Z3 AST)
-> ReaderT ImplicitParameters Z3 Sort
-> ReaderT ImplicitParameters Z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Var v -> ReaderT ImplicitParameters Z3 Sort
forall (z3 :: * -> *) a. MonadZ3 z3 => Var a -> z3 Sort
mkSortFor Var v
iVar
      let r :: Int
r = Int -> (SymbolicInfo -> Int) -> Maybe SymbolicInfo -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 ([Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> (SymbolicInfo -> [Int]) -> SymbolicInfo -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolicInfo -> [Int]
chronology) (Maybe SymbolicInfo -> Int) -> Maybe SymbolicInfo -> Int
forall a b. (a -> b) -> a -> b
$ SomeVar -> Map SomeVar SymbolicInfo -> Maybe SymbolicInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var v -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var v
iVar) Map SomeVar SymbolicInfo
e
      (((SomeVar, Int), AST, Int), ValueGenerator)
-> ReaderT
     ImplicitParameters Z3 (((SomeVar, Int), AST, Int), ValueGenerator)
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((Var v -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var v
iVar,Int
i),AST
var,Int
r),(ValueMap -> Size -> Gen v) -> ValueGenerator
forall v.
Typeable v =>
(ValueMap -> Size -> Gen v) -> ValueGenerator
ValueGenerator ((ValueMap -> Size -> Gen v) -> ValueGenerator)
-> (ValueMap -> Size -> Gen v) -> ValueGenerator
forall a b. (a -> b) -> a -> b
$ \ValueMap
m -> Var v -> ValueMap -> ValueSet v -> Size -> Gen v
forall a. Var a -> ValueMap -> ValueSet a -> Size -> Gen a
valueOf Var v
iVar ValueMap
m ValueSet v
vs)

  [Constraint 'Input]
-> (Constraint 'Input -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Constraint 'Input]
tyConstr ((Constraint 'Input -> ReaderT ImplicitParameters Z3 ())
 -> ReaderT ImplicitParameters Z3 ())
-> (Constraint 'Input -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall a b. (a -> b) -> a -> b
$
    \(InputConstraint (Var v
iVar,Int
i) (ValueSet v
vs :: ValueSet v) Map SomeVar SymbolicInfo
e) -> do
      let varASTs :: Map SomeVar [AST]
varASTs = ([AST] -> [AST] -> [AST])
-> [(SomeVar, [AST])] -> Map SomeVar [AST]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [AST] -> [AST] -> [AST]
forall a. [a] -> [a] -> [a]
(++) ([(SomeVar, [AST])] -> Map SomeVar [AST])
-> [(SomeVar, [AST])] -> Map SomeVar [AST]
forall a b. (a -> b) -> a -> b
$ ((((SomeVar, Int), AST, Int), ValueGenerator)
 -> [(SomeVar, [AST])])
-> [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> [(SomeVar, [AST])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(((SomeVar
var,Int
j),AST
ast,Int
_),ValueGenerator
_) -> [ (SomeVar
var,[AST
ast]) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= SomeVar -> Map SomeVar SymbolicInfo -> Int
ix SomeVar
var Map SomeVar SymbolicInfo
e]) [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars
      let var :: AST
var = AST -> Maybe AST -> AST
forall a. a -> Maybe a -> a
fromMaybe (String -> AST
forall a. HasCallStack => String -> a
error String
"impossible") (Maybe AST -> AST) -> Maybe AST -> AST
forall a b. (a -> b) -> a -> b
$ (SomeVar, Int) -> [((SomeVar, Int), AST)] -> Maybe AST
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup (Var v -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var v
iVar, Int
i) ([((SomeVar, Int), AST)] -> Maybe AST)
-> [((SomeVar, Int), AST)] -> Maybe AST
forall a b. (a -> b) -> a -> b
$ ((((SomeVar, Int), AST, Int), ValueGenerator)
 -> ((SomeVar, Int), AST))
-> [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> [((SomeVar, Int), AST)]
forall a b. (a -> b) -> [a] -> [b]
map (((SomeVar, Int), AST, Int) -> ((SomeVar, Int), AST)
forall a b c. (a, b, c) -> (a, b)
dropThd (((SomeVar, Int), AST, Int) -> ((SomeVar, Int), AST))
-> ((((SomeVar, Int), AST, Int), ValueGenerator)
    -> ((SomeVar, Int), AST, Int))
-> (((SomeVar, Int), AST, Int), ValueGenerator)
-> ((SomeVar, Int), AST)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((SomeVar, Int), AST, Int), ValueGenerator)
-> ((SomeVar, Int), AST, Int)
forall a b. (a, b) -> a
fst) [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars
      AST
constraint <- Var v
-> Map SomeVar [AST]
-> ValueSet v
-> AST
-> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *) a.
(MonadZ3 z3, Typeable a) =>
Var a -> Map SomeVar [AST] -> ValueSet a -> AST -> z3 AST
z3ValueSetConstraint Var v
iVar Map SomeVar [AST]
varASTs ValueSet v
vs AST
var
      Goal -> AST -> ReaderT ImplicitParameters Z3 ()
forall (z3 :: * -> *). MonadZ3 z3 => Goal -> AST -> z3 ()
goalAssert Goal
goal AST
constraint
  [Constraint 'Condition]
-> (Constraint 'Condition -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Constraint 'Condition]
predConstr ((Constraint 'Condition -> ReaderT ImplicitParameters Z3 ())
 -> ReaderT ImplicitParameters Z3 ())
-> (Constraint 'Condition -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall a b. (a -> b) -> a -> b
$
    \(ConditionConstraint Term 'Transparent Bool
t Map SomeVar SymbolicInfo
e) ->
        Goal -> AST -> ReaderT ImplicitParameters Z3 ()
forall (z3 :: * -> *). MonadZ3 z3 => Goal -> AST -> z3 ()
goalAssert Goal
goal (AST -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 AST
-> ReaderT ImplicitParameters Z3 ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Goal
-> Term 'Transparent Bool
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
forall x.
Typeable x =>
Goal
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
z3Predicate Goal
goal Term 'Transparent Bool
t Map SomeVar SymbolicInfo
e (((((SomeVar, Int), AST, Int), ValueGenerator)
 -> ((SomeVar, Int), AST))
-> [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> [((SomeVar, Int), AST)]
forall a b. (a -> b) -> [a] -> [b]
map (((SomeVar, Int), AST, Int) -> ((SomeVar, Int), AST)
forall a b c. (a, b, c) -> (a, b)
dropThd (((SomeVar, Int), AST, Int) -> ((SomeVar, Int), AST))
-> ((((SomeVar, Int), AST, Int), ValueGenerator)
    -> ((SomeVar, Int), AST, Int))
-> (((SomeVar, Int), AST, Int), ValueGenerator)
-> ((SomeVar, Int), AST)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((SomeVar, Int), AST, Int), ValueGenerator)
-> ((SomeVar, Int), AST, Int)
forall a b. (a, b) -> a
fst) [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars)

  Bool
-> ReaderT ImplicitParameters Z3 ()
-> ReaderT ImplicitParameters Z3 ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
checkOverflows (ReaderT ImplicitParameters Z3 ()
 -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
-> ReaderT ImplicitParameters Z3 ()
forall a b. (a -> b) -> a -> b
$
    [Constraint 'Overflow]
-> (Constraint 'Overflow -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Constraint 'Overflow]
overflowConstr ((Constraint 'Overflow -> ReaderT ImplicitParameters Z3 ())
 -> ReaderT ImplicitParameters Z3 ())
-> (Constraint 'Overflow -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall a b. (a -> b) -> a -> b
$
      \(OverflowConstraints [Term 'Transparent Integer]
ts Map SomeVar SymbolicInfo
e) ->
        [Term 'Transparent Integer]
-> (Term 'Transparent Integer -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Term 'Transparent Integer]
ts (\Term 'Transparent Integer
t -> Goal
-> Term 'Transparent Integer
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 ()
assertOverflowChecks Goal
goal Term 'Transparent Integer
t Map SomeVar SymbolicInfo
e (((((SomeVar, Int), AST, Int), ValueGenerator)
 -> ((SomeVar, Int), AST))
-> [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> [((SomeVar, Int), AST)]
forall a b. (a -> b) -> [a] -> [b]
map (((SomeVar, Int), AST, Int) -> ((SomeVar, Int), AST)
forall a b c. (a, b, c) -> (a, b)
dropThd (((SomeVar, Int), AST, Int) -> ((SomeVar, Int), AST))
-> ((((SomeVar, Int), AST, Int), ValueGenerator)
    -> ((SomeVar, Int), AST, Int))
-> (((SomeVar, Int), AST, Int), ValueGenerator)
-> ((SomeVar, Int), AST)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((SomeVar, Int), AST, Int), ValueGenerator)
-> ((SomeVar, Int), AST, Int)
forall a b. (a, b) -> a
fst) [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars))

  -- simplify and assert goal
  Tactic
simplifyTactic <- String -> ReaderT ImplicitParameters Z3 Tactic
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 Tactic
mkTactic String
"simplify"
  ApplyResult
tacticResult <- Tactic -> Goal -> ReaderT ImplicitParameters Z3 ApplyResult
forall (z3 :: * -> *).
MonadZ3 z3 =>
Tactic -> Goal -> z3 ApplyResult
applyTactic Tactic
simplifyTactic Goal
goal
  [Goal
newGoal] <- ApplyResult -> ReaderT ImplicitParameters Z3 [Goal]
forall (z3 :: * -> *). MonadZ3 z3 => ApplyResult -> z3 [Goal]
getApplyResultSubgoals ApplyResult
tacticResult
  [AST]
fs <- Goal -> ReaderT ImplicitParameters Z3 [AST]
forall (z3 :: * -> *). MonadZ3 z3 => Goal -> z3 [AST]
getGoalFormulas Goal
newGoal
  [AST]
-> (AST -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [AST]
fs ((AST -> ReaderT ImplicitParameters Z3 ())
 -> ReaderT ImplicitParameters Z3 ())
-> (AST -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall a b. (a -> b) -> a -> b
$ \AST
f -> Z3 () -> ReaderT ImplicitParameters Z3 ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Z3 () -> ReaderT ImplicitParameters Z3 ())
-> Z3 () -> ReaderT ImplicitParameters Z3 ()
forall a b. (a -> b) -> a -> b
$ AST -> Z3 ()
forall (z3 :: * -> *). MonadOptimize z3 => AST -> z3 ()
optimizeAssert AST
f

  case ScriptMode
mode of
    ScriptMode
WithSoft -> do
      [(AST, Value)]
vs <- [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> Z3R [(AST, Value)]
generateSuggestions [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars
      [(AST, Value)]
-> ((AST, Value) -> ReaderT ImplicitParameters Z3 [Int])
-> ReaderT ImplicitParameters Z3 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(AST, Value)]
vs (((AST, Value) -> ReaderT ImplicitParameters Z3 [Int])
 -> ReaderT ImplicitParameters Z3 ())
-> ((AST, Value) -> ReaderT ImplicitParameters Z3 [Int])
-> ReaderT ImplicitParameters Z3 ()
forall a b. (a -> b) -> a -> b
$ \(AST
ast,Value
v) -> do
        [(AST, Symbol)]
cs <- AST -> Value -> ReaderT ImplicitParameters Z3 [(AST, Symbol)]
forall (z3 :: * -> *).
MonadZ3 z3 =>
AST -> Value -> z3 [(AST, Symbol)]
mkValueRep AST
ast Value
v
        [(AST, Symbol)]
-> ((AST, Symbol) -> ReaderT ImplicitParameters Z3 Int)
-> ReaderT ImplicitParameters Z3 [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(AST, Symbol)]
cs (((AST, Symbol) -> ReaderT ImplicitParameters Z3 Int)
 -> ReaderT ImplicitParameters Z3 [Int])
-> ((AST, Symbol) -> ReaderT ImplicitParameters Z3 Int)
-> ReaderT ImplicitParameters Z3 [Int]
forall a b. (a -> b) -> a -> b
$ \(AST
c,Symbol
l) -> Z3 Int -> ReaderT ImplicitParameters Z3 Int
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Z3 Int -> ReaderT ImplicitParameters Z3 Int)
-> Z3 Int -> ReaderT ImplicitParameters Z3 Int
forall a b. (a -> b) -> a -> b
$ AST -> String -> Symbol -> Z3 Int
forall (z3 :: * -> *).
MonadOptimize z3 =>
AST -> String -> Symbol -> z3 Int
optimizeAssertSoft AST
c String
"1" Symbol
l -- soft assert with weight 1 and id "default"
    ScriptMode
WithoutSoft -> () -> ReaderT ImplicitParameters Z3 ()
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  String
str <- Z3 String -> ReaderT ImplicitParameters Z3 String
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Z3 String
forall (z3 :: * -> *). MonadOptimize z3 => z3 String
optimizeToString
  Result
result <- Z3 Result -> ReaderT ImplicitParameters Z3 Result
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Z3 Result -> ReaderT ImplicitParameters Z3 Result)
-> Z3 Result -> ReaderT ImplicitParameters Z3 Result
forall a b. (a -> b) -> a -> b
$ [AST] -> Z3 Result
forall (z3 :: * -> *). MonadOptimize z3 => [AST] -> z3 Result
optimizeCheck []
  SatResult [String]
mRes <- case Result
result of
    Result
Sat -> do
      Model
model <- Z3 Model -> ReaderT ImplicitParameters Z3 Model
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Z3 Model
forall (z3 :: * -> *). MonadOptimize z3 => z3 Model
optimizeGetModel
      [String] -> SatResult [String]
forall a. a -> SatResult a
SAT ([String] -> SatResult [String])
-> ([Maybe String] -> [String])
-> [Maybe String]
-> SatResult [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe String] -> SatResult [String])
-> ReaderT ImplicitParameters Z3 [Maybe String]
-> ReaderT ImplicitParameters Z3 (SatResult [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((((SomeVar, Int), AST, Int), ValueGenerator)
 -> ReaderT ImplicitParameters Z3 (Maybe String))
-> [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> ReaderT ImplicitParameters Z3 [Maybe String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(((SomeVar
var,Int
_),AST
ast,Int
_),ValueGenerator
_) -> Model
-> (SomeVar, AST) -> ReaderT ImplicitParameters Z3 (Maybe String)
forall (z3 :: * -> *).
MonadZ3 z3 =>
Model -> (SomeVar, AST) -> z3 (Maybe String)
evalAST Model
model (SomeVar
var,AST
ast)) [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars
    Result
Unsat -> do
      SatResult [String]
-> ReaderT ImplicitParameters Z3 (SatResult [String])
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SatResult [String]
forall a. SatResult a
NotSAT
    Result
Undef -> SatResult [String]
-> ReaderT ImplicitParameters Z3 (SatResult [String])
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SatResult [String]
forall a. SatResult a
Timeout
  (SatResult [String], String)
-> ReaderT ImplicitParameters Z3 (SatResult [String], String)
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SatResult [String]
mRes,String
str)

dropThd :: (a,b,c) -> (a,b)
dropThd :: forall a b c. (a, b, c) -> (a, b)
dropThd (a
x,b
y,c
_) = (a
x,b
y)

generateSuggestions :: [(((SomeVar, Int), AST, Int), ValueGenerator)] -> Z3R [(AST, Value)]
generateSuggestions :: [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> Z3R [(AST, Value)]
generateSuggestions [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars = do
  -- make sure variables are ordered correctly, otherwise we construct the wrong ValueMap
  let
    sortedVars :: [(((SomeVar, Int), AST, Int), ValueGenerator)]
sortedVars = ((((SomeVar, Int), AST, Int), ValueGenerator) -> Int)
-> [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> [(((SomeVar, Int), AST, Int), ValueGenerator)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (((SomeVar, Int), AST, Int) -> Int
forall a b c. (a, b, c) -> c
thd3 (((SomeVar, Int), AST, Int) -> Int)
-> ((((SomeVar, Int), AST, Int), ValueGenerator)
    -> ((SomeVar, Int), AST, Int))
-> (((SomeVar, Int), AST, Int), ValueGenerator)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((SomeVar, Int), AST, Int), ValueGenerator)
-> ((SomeVar, Int), AST, Int)
forall a b. (a, b) -> a
fst) [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars
    baseVars :: [SomeVar]
baseVars = ((((SomeVar, Int), AST, Int), ValueGenerator) -> SomeVar)
-> [(((SomeVar, Int), AST, Int), ValueGenerator)] -> [SomeVar]
forall a b. (a -> b) -> [a] -> [b]
map ((SomeVar, Int) -> SomeVar
forall a b. (a, b) -> a
fst ((SomeVar, Int) -> SomeVar)
-> ((((SomeVar, Int), AST, Int), ValueGenerator) -> (SomeVar, Int))
-> (((SomeVar, Int), AST, Int), ValueGenerator)
-> SomeVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SomeVar, Int), AST, Int) -> (SomeVar, Int)
forall a b c. (a, b, c) -> a
fst3 (((SomeVar, Int), AST, Int) -> (SomeVar, Int))
-> ((((SomeVar, Int), AST, Int), ValueGenerator)
    -> ((SomeVar, Int), AST, Int))
-> (((SomeVar, Int), AST, Int), ValueGenerator)
-> (SomeVar, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((SomeVar, Int), AST, Int), ValueGenerator)
-> ((SomeVar, Int), AST, Int)
forall a b. (a, b) -> a
fst) [(((SomeVar, Int), AST, Int), ValueGenerator)]
sortedVars
  ImplicitParameter {Int
Integer
valueSizeParameter :: ImplicitParameters -> Integer
maxSeqLengthParameter :: ImplicitParameters -> Int
valueSizeParameter :: Integer
maxSeqLengthParameter :: Int
..} <- ReaderT ImplicitParameters Z3 ImplicitParameters
forall r (m :: * -> *). MonadReader r m => m r
ask
  (StateT ValueMap (ReaderT ImplicitParameters Z3) [(AST, Value)]
 -> ValueMap -> Z3R [(AST, Value)])
-> ValueMap
-> StateT ValueMap (ReaderT ImplicitParameters Z3) [(AST, Value)]
-> Z3R [(AST, Value)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT ValueMap (ReaderT ImplicitParameters Z3) [(AST, Value)]
-> ValueMap -> Z3R [(AST, Value)]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ([SomeVar] -> ValueMap
emptyValueMap [SomeVar]
baseVars) (StateT ValueMap (ReaderT ImplicitParameters Z3) [(AST, Value)]
 -> Z3R [(AST, Value)])
-> StateT ValueMap (ReaderT ImplicitParameters Z3) [(AST, Value)]
-> Z3R [(AST, Value)]
forall a b. (a -> b) -> a -> b
$
    [(((SomeVar, Int), AST, Int), ValueGenerator)]
-> ((((SomeVar, Int), AST, Int), ValueGenerator)
    -> StateT ValueMap (ReaderT ImplicitParameters Z3) (AST, Value))
-> StateT ValueMap (ReaderT ImplicitParameters Z3) [(AST, Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(((SomeVar, Int), AST, Int), ValueGenerator)]
vars (((((SomeVar, Int), AST, Int), ValueGenerator)
  -> StateT ValueMap (ReaderT ImplicitParameters Z3) (AST, Value))
 -> StateT ValueMap (ReaderT ImplicitParameters Z3) [(AST, Value)])
-> ((((SomeVar, Int), AST, Int), ValueGenerator)
    -> StateT ValueMap (ReaderT ImplicitParameters Z3) (AST, Value))
-> StateT ValueMap (ReaderT ImplicitParameters Z3) [(AST, Value)]
forall a b. (a -> b) -> a -> b
$ \(((SomeVar
var,Int
_),AST
ast,Int
_),ValueGenerator
gen) -> do
      ValueMap
vMap <- StateT ValueMap (ReaderT ImplicitParameters Z3) ValueMap
forall s (m :: * -> *). MonadState s m => m s
get
      (AST
ast,Value
val) <- IO (AST, Value)
-> StateT ValueMap (ReaderT ImplicitParameters Z3) (AST, Value)
forall a. IO a -> StateT ValueMap (ReaderT ImplicitParameters Z3) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (AST, Value)
 -> StateT ValueMap (ReaderT ImplicitParameters Z3) (AST, Value))
-> IO (AST, Value)
-> StateT ValueMap (ReaderT ImplicitParameters Z3) (AST, Value)
forall a b. (a -> b) -> a -> b
$ (forall v. Typeable v => v -> (AST, Value))
-> ValueGenerator -> ValueMap -> Size -> IO (AST, Value)
forall r.
(forall v. Typeable v => v -> r)
-> ValueGenerator -> ValueMap -> Size -> IO r
withGeneratedValue (\v
v -> (AST
ast,v -> Value
forall a. Typeable a => a -> Value
wrapValue v
v)) ValueGenerator
gen ValueMap
vMap (Integer -> Int -> Size
Size Integer
valueSizeParameter (Int
maxSeqLengthParameter Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2))
      (ValueMap -> ValueMap)
-> StateT ValueMap (ReaderT ImplicitParameters Z3) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Value -> SomeVar -> ValueMap -> ValueMap
insertValue Value
val SomeVar
var)
      (AST, Value)
-> StateT ValueMap (ReaderT ImplicitParameters Z3) (AST, Value)
forall a. a -> StateT ValueMap (ReaderT ImplicitParameters Z3) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AST
ast,Value
val)

evalAST :: MonadZ3 z3 => Model -> (SomeVar, AST) -> z3 (Maybe String)
evalAST :: forall (z3 :: * -> *).
MonadZ3 z3 =>
Model -> (SomeVar, AST) -> z3 (Maybe String)
evalAST Model
m (SomeVar StringVar{},AST
x) = do
  Bool
isS <- Sort -> z3 Bool
forall (z3 :: * -> *). MonadZ3 z3 => Sort -> z3 Bool
isStringSort (Sort -> z3 Bool) -> z3 Sort -> z3 Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> z3 Sort
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 Sort
getSort AST
x
  if Bool
isS
    then do
      Maybe AST
mR <- Model -> AST -> Bool -> z3 (Maybe AST)
forall (z3 :: * -> *).
MonadZ3 z3 =>
Model -> AST -> Bool -> z3 (Maybe AST)
modelEval Model
m AST
x Bool
True
      case Maybe AST
mR of
        Just AST
r -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> z3 String -> z3 (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AST -> z3 String
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 String
getString AST
r
        Maybe AST
Nothing -> Maybe String -> z3 (Maybe String)
forall a. a -> z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
    else Maybe String -> z3 (Maybe String)
forall a. a -> z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
evalAST Model
m (SomeVar IntVar{},AST
x) = (Integer -> String) -> Maybe Integer -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> String
forall a. Show a => a -> String
show (Maybe Integer -> Maybe String)
-> z3 (Maybe Integer) -> z3 (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EvalAst z3 Integer
forall (z3 :: * -> *). MonadZ3 z3 => EvalAst z3 Integer
evalInt Model
m AST
x
evalAST Model
m (SomeVar BoolVar{},AST
x) = (Bool -> String) -> Maybe Bool -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> String
forall a. Show a => a -> String
show (Maybe Bool -> Maybe String)
-> z3 (Maybe Bool) -> z3 (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EvalAst z3 Bool
forall (z3 :: * -> *). MonadZ3 z3 => EvalAst z3 Bool
evalBool Model
m AST
x
evalAST Model
m (SomeVar (EmbeddedVar (TypeRep a1
_ :: TypeRep a) String
_),AST
x) = (Integer -> String) -> Maybe Integer -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a1 -> String
forall a. Show a => a -> String
show (a1 -> String) -> (Integer -> a1) -> Integer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Embeddable a => Integer -> a
asOriginal @a) (Maybe Integer -> Maybe String)
-> z3 (Maybe Integer) -> z3 (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EvalAst z3 Integer
forall (z3 :: * -> *). MonadZ3 z3 => EvalAst z3 Integer
evalInt Model
m AST
x

mkSortFor :: MonadZ3 z3 => Var a -> z3 Sort
mkSortFor :: forall (z3 :: * -> *) a. MonadZ3 z3 => Var a -> z3 Sort
mkSortFor IntVar{} = z3 Sort
forall (z3 :: * -> *). MonadZ3 z3 => z3 Sort
mkIntSort
mkSortFor BoolVar{} = z3 Sort
forall (z3 :: * -> *). MonadZ3 z3 => z3 Sort
mkBoolSort
mkSortFor StringVar{} = z3 Sort
forall (z3 :: * -> *). MonadZ3 z3 => z3 Sort
mkStringSort
mkSortFor EmbeddedVar{} = z3 Sort
forall (z3 :: * -> *). MonadZ3 z3 => z3 Sort
mkIntSort

mkValueRep :: MonadZ3 z3 => AST -> Value -> z3 [(AST,Symbol)]
mkValueRep :: forall (z3 :: * -> *).
MonadZ3 z3 =>
AST -> Value -> z3 [(AST, Symbol)]
mkValueRep AST
x (IntegerValue Integer
n) = do
  Symbol
def <- String -> z3 Symbol
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 Symbol
mkStringSymbol String
"default"
  (AST, Symbol) -> [(AST, Symbol)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((AST, Symbol) -> [(AST, Symbol)])
-> (AST -> (AST, Symbol)) -> AST -> [(AST, Symbol)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Symbol
def) (AST -> [(AST, Symbol)]) -> z3 AST -> z3 [(AST, Symbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
x (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Integer -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => Integer -> z3 AST
mkInteger Integer
n)
mkValueRep AST
x (BoolValue Bool
b) = do
  Symbol
def <- String -> z3 Symbol
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 Symbol
mkStringSymbol String
"default"
  (AST, Symbol) -> [(AST, Symbol)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((AST, Symbol) -> [(AST, Symbol)])
-> (AST -> (AST, Symbol)) -> AST -> [(AST, Symbol)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,Symbol
def) (AST -> [(AST, Symbol)]) -> z3 AST -> z3 [(AST, Symbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
x (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bool -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => Bool -> z3 AST
mkBool Bool
b)
mkValueRep AST
x (StringValue String
s) = do
  String
xStr <- AST -> z3 String
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 String
astToString AST
x
  -- length constraint
  Symbol
lenSym <- String -> z3 Symbol
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 Symbol
mkStringSymbol (String -> z3 Symbol) -> String -> z3 Symbol
forall a b. (a -> b) -> a -> b
$ String
xStr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_len"
  AST
len <- Int -> z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum (Int -> z3 AST) -> Int -> z3 AST
forall a b. (a -> b) -> a -> b
$ String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s
  AST
lenEq <- AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
len (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkSeqLength AST
x
  -- character range constraint
  Symbol
rangeSym <- String -> z3 Symbol
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 Symbol
mkStringSymbol (String -> z3 Symbol) -> String -> z3 Symbol
forall a b. (a -> b) -> a -> b
$ String
xStr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_range"
  AST
r1 <- Char -> Char -> z3 AST
forall {m :: * -> *}. MonadZ3 m => Char -> Char -> m AST
reRange Char
'a' Char
'z'
  AST
r2 <- Char -> Char -> z3 AST
forall {m :: * -> *}. MonadZ3 m => Char -> Char -> m AST
reRange Char
'A' Char
'Z'
  AST
rangeEq <- AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkSeqInRe AST
x (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkReStar (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Integer -> [AST] -> z3 AST
forall int (z3 :: * -> *).
(Integral int, MonadZ3 z3) =>
int -> [AST] -> z3 AST
mkReUnion (Integer
2 :: Integer) [AST
r1,AST
r2]
  -- value constraints
  [(AST, Symbol)]
vals <- ((Char, Integer) -> z3 (AST, Symbol))
-> [(Char, Integer)] -> z3 [(AST, Symbol)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (String -> (Char, Integer) -> z3 (AST, Symbol)
positionConstraint String
xStr) (String
s String -> [Integer] -> [(Char, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Integer
1..])
  [(AST, Symbol)] -> z3 [(AST, Symbol)]
forall a. a -> z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(AST, Symbol)] -> z3 [(AST, Symbol)])
-> [(AST, Symbol)] -> z3 [(AST, Symbol)]
forall a b. (a -> b) -> a -> b
$ (AST
lenEq,Symbol
lenSym) (AST, Symbol) -> [(AST, Symbol)] -> [(AST, Symbol)]
forall a. a -> [a] -> [a]
: (AST
rangeEq,Symbol
rangeSym) (AST, Symbol) -> [(AST, Symbol)] -> [(AST, Symbol)]
forall a. a -> [a] -> [a]
: [(AST, Symbol)]
vals
  where
    reRange :: Char -> Char -> m AST
reRange Char
a Char
b = do
      AST
aStr <- String -> m AST
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 AST
mkString [Char
a]
      AST
bStr <- String -> m AST
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 AST
mkString [Char
b]
      AST -> AST -> m AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkReRange AST
aStr AST
bStr
    positionConstraint :: String -> (Char, Integer) -> z3 (AST, Symbol)
positionConstraint String
xStr (Char
c,Integer
i) = do
      AST
xi <- AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkSeqAt AST
x (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Integer -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => Integer -> z3 AST
mkInteger Integer
i
      AST
eq <- AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
xi (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 AST
mkString [Char
c]
      Symbol
sym <- String -> z3 Symbol
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 Symbol
mkStringSymbol (String -> z3 Symbol) -> String -> z3 Symbol
forall a b. (a -> b) -> a -> b
$ String
xStr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_val"
      (AST, Symbol) -> z3 (AST, Symbol)
forall a. a -> z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AST
eq,Symbol
sym)


      -- binNoList (:&&:) = \a b -> mkAnd [a,b]
      -- binNoList (:||:) = \a b -> mkOr [a,b]

forStringElse :: forall (a :: Type) z3. (Typeable a, MonadZ3 z3) => (AST -> AST -> z3 AST) -> (AST -> AST -> z3 AST) -> AST -> AST -> z3 AST
forStringElse :: forall a (z3 :: * -> *).
(Typeable a, MonadZ3 z3) =>
(AST -> AST -> z3 AST)
-> (AST -> AST -> z3 AST) -> AST -> AST -> z3 AST
forStringElse AST -> AST -> z3 AST
string AST -> AST -> z3 AST
normal = forall {k} (a :: k) r. Typeable a => [Case a r] -> r
forall a r. Typeable a => [Case a r] -> r
matchType @a
  [ forall {k1} {k2} (a :: k1) (x :: k2) r. Typeable a => r -> Case x r
forall a x r. Typeable a => r -> Case x r
inCaseOf' @String AST -> AST -> z3 AST
string
  , (AST -> AST -> z3 AST) -> Case a (AST -> AST -> z3 AST)
forall {k} r (x :: k). r -> Case x r
fallbackCase' AST -> AST -> z3 AST
normal
  ]

z3Predicate :: Typeable x => Goal -> Term 'Transparent x -> Map SomeVar SymbolicInfo -> [((SomeVar, Int), AST)] -> Z3R AST
z3Predicate :: forall x.
Typeable x =>
Goal
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
z3Predicate Goal
goal (Add Term 'Transparent x
x Term 'Transparent x
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent x
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent x
x Term 'Transparent x
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = \AST
a AST
b -> [AST] -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkAdd [AST
a,AST
b]
}
z3Predicate Goal
goal (Sub Term 'Transparent x
x Term 'Transparent x
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent x
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent x
x Term 'Transparent x
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = \AST
a AST
b -> [AST] -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkSub [AST
a,AST
b]
}
z3Predicate Goal
goal (Mul Term 'Transparent x
x Term 'Transparent x
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent x
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent x
x Term 'Transparent x
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = \AST
a AST
b -> [AST] -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkMul [AST
a,AST
b]
}
z3Predicate Goal
goal (Equals Term 'Transparent a1
x Term 'Transparent a1
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent a1
-> Term 'Transparent a1
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent a1
x Term 'Transparent a1
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = mkEq,
  binaryListAB = compareSymbolic (Strict EQ)
  }
z3Predicate Goal
goal (Gt (Term 'Transparent a1
x :: Term k a) Term 'Transparent a1
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent a1
-> Term 'Transparent a1
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent a1
x Term 'Transparent a1
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = forStringElse @a (\AST
a AST
b -> AST -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkNot (AST -> ReaderT ImplicitParameters Z3 AST)
-> ReaderT ImplicitParameters Z3 AST
-> ReaderT ImplicitParameters Z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkStrLe AST
a AST
b) mkGt,
  binaryListAB = compareSymbolic (Strict GT)
  }
z3Predicate Goal
goal (Ge (Term 'Transparent a1
x :: Term k a) Term 'Transparent a1
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent a1
-> Term 'Transparent a1
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent a1
x Term 'Transparent a1
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = forStringElse @a (\AST
a AST
b -> AST -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkNot (AST -> ReaderT ImplicitParameters Z3 AST)
-> ReaderT ImplicitParameters Z3 AST
-> ReaderT ImplicitParameters Z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkStrLt AST
a AST
b) mkGe,
  binaryListAB = compareSymbolic (ReflexiveClosure GT)
  }
z3Predicate Goal
goal (Lt (Term 'Transparent a1
x :: Term k a) Term 'Transparent a1
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent a1
-> Term 'Transparent a1
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent a1
x Term 'Transparent a1
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = forStringElse @a mkStrLt mkLt,
  binaryListAB = compareSymbolic (Strict LT)
  }
z3Predicate Goal
goal (Le (Term 'Transparent a1
x :: Term k a) Term 'Transparent a1
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent a1
-> Term 'Transparent a1
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent a1
x Term 'Transparent a1
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = forStringElse @a mkStrLe mkLe,
  binaryListAB = compareSymbolic (ReflexiveClosure LT)
  }
z3Predicate Goal
goal (And Term 'Transparent Bool
x Term 'Transparent Bool
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent Bool
-> Term 'Transparent Bool
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent Bool
x Term 'Transparent Bool
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList = \AST
a AST
b -> [AST] -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkAnd [AST
a,AST
b]
  }
z3Predicate Goal
goal (Or Term 'Transparent Bool
x Term 'Transparent Bool
y) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent Bool
-> Term 'Transparent Bool
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent Bool
x Term 'Transparent Bool
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryNoList =  \AST
a AST
b -> [AST] -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkOr [AST
a,AST
b]
  }
z3Predicate Goal
goal (IsIn Term 'Transparent a1
x Term 'Transparent [a1]
xs) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent a1
-> Term 'Transparent [a1]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent a1
x Term 'Transparent [a1]
xs Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Bin (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Bin (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Bin z3
binary {
  binaryListB = \AST
x [AST]
xs -> [AST] -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkOr ([AST] -> ReaderT ImplicitParameters Z3 AST)
-> ReaderT ImplicitParameters Z3 [AST]
-> ReaderT ImplicitParameters Z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (AST -> ReaderT ImplicitParameters Z3 AST)
-> [AST] -> ReaderT ImplicitParameters Z3 [AST]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (AST -> AST -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
x) [AST]
xs
  }
z3Predicate Goal
goal (Not Term 'Transparent Bool
x) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent Bool
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a.
Typeable a =>
Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateUnary Goal
goal Term 'Transparent Bool
x Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Un (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Un (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Un z3
unary {
  unaryNoList = mkNot
  }
z3Predicate Goal
goal (Sum Term 'Transparent [x]
xs) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent [x]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a.
Typeable a =>
Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateUnary Goal
goal Term 'Transparent [x]
xs Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Un (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Un (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Un z3
unary {
  unaryList = mkAdd
  }
z3Predicate Goal
goal (Product Term 'Transparent [x]
xs) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent [x]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a.
Typeable a =>
Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateUnary Goal
goal Term 'Transparent [x]
xs Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Un (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Un (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Un z3
unary {
  unaryList = mkMul
  }
z3Predicate Goal
_ (Length (Current e [a1]
x Int
n)) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = AST -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkSeqLength (AST -> ReaderT ImplicitParameters Z3 AST)
-> ([(SomeVar, Int)] -> AST)
-> [(SomeVar, Int)]
-> ReaderT ImplicitParameters Z3 AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe AST -> AST
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe AST -> AST)
-> ([(SomeVar, Int)] -> Maybe AST) -> [(SomeVar, Int)] -> AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SomeVar, Int) -> [((SomeVar, Int), AST)] -> Maybe AST
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`List.lookup` [((SomeVar, Int), AST)]
vars) ((SomeVar, Int) -> Maybe AST)
-> ([(SomeVar, Int)] -> (SomeVar, Int))
-> [(SomeVar, Int)]
-> Maybe AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SomeVar, Int)] -> (SomeVar, Int)
forall a. HasCallStack => [a] -> a
last ([(SomeVar, Int)] -> ReaderT ImplicitParameters Z3 AST)
-> [(SomeVar, Int)] -> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ e [a1] -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
weaveVariables e [a1]
x Int
n Map SomeVar SymbolicInfo
e --special case for string variables
z3Predicate Goal
goal (Length Term 'Transparent [a1]
xs) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent [a1]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a.
Typeable a =>
Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateUnary Goal
goal Term 'Transparent [a1]
xs Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Un (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Un (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Un z3
unary {
  unaryList = mkIntNum . length
  }
z3Predicate Goal
goal (Reverse Term 'Transparent [a1]
xs) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent [a1]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a.
Typeable a =>
Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateUnary Goal
goal Term 'Transparent [a1]
xs Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars (Un (ReaderT ImplicitParameters Z3)
 -> ReaderT ImplicitParameters Z3 AST)
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ Un (ReaderT ImplicitParameters Z3)
forall (z3 :: * -> *). Un z3
unary {
  unaryList = error "z3Predicate: top level reverse should not happen"
  }
z3Predicate Goal
_ (IntLit Integer
n) Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = Integer -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum Integer
n
z3Predicate Goal
_ (ListLit [a1]
_) Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = String -> ReaderT ImplicitParameters Z3 AST
forall a. HasCallStack => String -> a
error String
"z3Predicate: top level list literal should not happen"
z3Predicate Goal
_ (EmbeddedLit a1
x) Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = Integer -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum (Integer -> ReaderT ImplicitParameters Z3 AST)
-> Integer -> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ a1 -> Integer
forall a. Embeddable a => a -> Integer
asInteger a1
x
z3Predicate Goal
_ (BoolLit Bool
b) Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = Bool -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => Bool -> z3 AST
mkBool Bool
b
z3Predicate Goal
_ (Current e x
x Int
n) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = AST -> ReaderT ImplicitParameters Z3 AST
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AST -> ReaderT ImplicitParameters Z3 AST)
-> AST -> ReaderT ImplicitParameters Z3 AST
forall a b. (a -> b) -> a -> b
$ AST -> Maybe AST -> AST
forall a. a -> Maybe a -> a
fromMaybe (e x -> AST
forall (e :: * -> *) a b. VarExp e => e a -> b
unknownVariablesError e x
x) (Maybe AST -> AST) -> Maybe AST -> AST
forall a b. (a -> b) -> a -> b
$ ((SomeVar, Int) -> [((SomeVar, Int), AST)] -> Maybe AST
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`List.lookup` [((SomeVar, Int), AST)]
vars) ((SomeVar, Int) -> Maybe AST)
-> ([(SomeVar, Int)] -> (SomeVar, Int))
-> [(SomeVar, Int)]
-> Maybe AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SomeVar, Int)] -> (SomeVar, Int)
forall a. HasCallStack => [a] -> a
last ([(SomeVar, Int)] -> Maybe AST) -> [(SomeVar, Int)] -> Maybe AST
forall a b. (a -> b) -> a -> b
$ e x -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
weaveVariables e x
x Int
n Map SomeVar SymbolicInfo
e
z3Predicate Goal
_ All{} Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = String -> ReaderT ImplicitParameters Z3 AST
forall a. HasCallStack => String -> a
error String
"z3Predicate: top level list should not happen"

data Un z3 = Un
  { forall (z3 :: * -> *). Un z3 -> AST -> z3 AST
unaryNoList :: AST -> z3 AST
  , forall (z3 :: * -> *). Un z3 -> [AST] -> z3 AST
unaryList :: [AST] -> z3 AST
  }
unary :: Un z3
unary :: forall (z3 :: * -> *). Un z3
unary = (AST -> z3 AST) -> ([AST] -> z3 AST) -> Un z3
forall (z3 :: * -> *).
(AST -> z3 AST) -> ([AST] -> z3 AST) -> Un z3
Un AST -> z3 AST
forall {a}. a
err [AST] -> z3 AST
forall {a}. a
err
  where err :: a
err = String -> a
forall a. HasCallStack => String -> a
error String
"does not happen with currently supported functions"

data Bin z3 = Bin
  { forall (z3 :: * -> *). Bin z3 -> AST -> AST -> z3 AST
binaryNoList :: AST -> AST -> z3 AST
  , forall (z3 :: * -> *). Bin z3 -> [AST] -> AST -> z3 AST
binaryListA :: [AST] -> AST -> z3 AST
  , forall (z3 :: * -> *). Bin z3 -> AST -> [AST] -> z3 AST
binaryListB :: AST -> [AST] -> z3 AST
  , forall (z3 :: * -> *). Bin z3 -> [AST] -> [AST] -> z3 AST
binaryListAB :: [AST] -> [AST] ->  z3 AST
  }
binary :: Bin z3
binary :: forall (z3 :: * -> *). Bin z3
binary = (AST -> AST -> z3 AST)
-> ([AST] -> AST -> z3 AST)
-> (AST -> [AST] -> z3 AST)
-> ([AST] -> [AST] -> z3 AST)
-> Bin z3
forall (z3 :: * -> *).
(AST -> AST -> z3 AST)
-> ([AST] -> AST -> z3 AST)
-> (AST -> [AST] -> z3 AST)
-> ([AST] -> [AST] -> z3 AST)
-> Bin z3
Bin AST -> AST -> z3 AST
forall {a}. a
err [AST] -> AST -> z3 AST
forall {a}. a
err AST -> [AST] -> z3 AST
forall {a}. a
err [AST] -> [AST] -> z3 AST
forall {a}. a
err
  where err :: a
err = String -> a
forall a. HasCallStack => String -> a
error String
"does not happen with currently supported functions"

z3PredicateUnary :: forall a. Typeable a => Goal -> Term 'Transparent a ->  Map SomeVar SymbolicInfo -> [((SomeVar, Int), AST)] -> Un Z3R -> Z3R AST
z3PredicateUnary :: forall a.
Typeable a =>
Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Un (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateUnary Goal
goal Term 'Transparent a
x Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars Un{[AST] -> ReaderT ImplicitParameters Z3 AST
AST -> ReaderT ImplicitParameters Z3 AST
unaryNoList :: forall (z3 :: * -> *). Un z3 -> AST -> z3 AST
unaryList :: forall (z3 :: * -> *). Un z3 -> [AST] -> z3 AST
unaryNoList :: AST -> ReaderT ImplicitParameters Z3 AST
unaryList :: [AST] -> ReaderT ImplicitParameters Z3 AST
..} = case forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a of
  App TypeRep a
c TypeRep b
_ -> case TypeRep a -> TypeRep [] -> Maybe (a :~~: [])
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
c (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> *). Typeable a => TypeRep a
typeRep @[]) of
    Just a :~~: []
HRefl -> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
forall a.
Typeable [a] =>
Term 'Transparent [a] -> ReaderT ImplicitParameters Z3 AST
case1 Term 'Transparent a
Term 'Transparent [b]
x -- a ~ [a1]
    Maybe (a :~~: [])
Nothing -> Term 'Transparent a -> ReaderT ImplicitParameters Z3 AST
forall a.
Typeable a =>
Term 'Transparent a -> ReaderT ImplicitParameters Z3 AST
case2 Term 'Transparent a
x -- a ~ f a1
  TypeRep a
_ -> Term 'Transparent a -> ReaderT ImplicitParameters Z3 AST
forall a.
Typeable a =>
Term 'Transparent a -> ReaderT ImplicitParameters Z3 AST
case2 Term 'Transparent a
x --
  where
    case1 :: forall a. Typeable [a] => Term 'Transparent [a] -> Z3R AST
    case1 :: forall a.
Typeable [a] =>
Term 'Transparent [a] -> ReaderT ImplicitParameters Z3 AST
case1 Term 'Transparent [a]
x = do
      Either AST [AST]
rx <- Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
forall a.
Typeable [a] =>
Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
listASTs Goal
goal Term 'Transparent [a]
x Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
      case Either AST [AST]
rx of
        Right [AST]
xs -> [AST] -> ReaderT ImplicitParameters Z3 AST
unaryList [AST]
xs
        Left AST
x -> AST -> ReaderT ImplicitParameters Z3 AST
unaryNoList AST
x
    case2 :: forall a. Typeable a => Term 'Transparent a -> Z3R AST
    case2 :: forall a.
Typeable a =>
Term 'Transparent a -> ReaderT ImplicitParameters Z3 AST
case2 Term 'Transparent a
x = AST -> ReaderT ImplicitParameters Z3 AST
unaryNoList (AST -> ReaderT ImplicitParameters Z3 AST)
-> ReaderT ImplicitParameters Z3 AST
-> ReaderT ImplicitParameters Z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
forall x.
Typeable x =>
Goal
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
z3Predicate Goal
goal Term 'Transparent a
x Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars

z3PredicateBinary :: forall a b. (Typeable a, Typeable b) => Goal -> Term 'Transparent a -> Term 'Transparent b ->  Map SomeVar SymbolicInfo -> [((SomeVar, Int), AST)] -> Bin Z3R -> Z3R AST
z3PredicateBinary :: forall a b.
(Typeable a, Typeable b) =>
Goal
-> Term 'Transparent a
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Bin (ReaderT ImplicitParameters Z3)
-> ReaderT ImplicitParameters Z3 AST
z3PredicateBinary Goal
goal Term 'Transparent a
x Term 'Transparent b
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars Bin{[AST] -> [AST] -> ReaderT ImplicitParameters Z3 AST
[AST] -> AST -> ReaderT ImplicitParameters Z3 AST
AST -> [AST] -> ReaderT ImplicitParameters Z3 AST
AST -> AST -> ReaderT ImplicitParameters Z3 AST
binaryNoList :: forall (z3 :: * -> *). Bin z3 -> AST -> AST -> z3 AST
binaryListAB :: forall (z3 :: * -> *). Bin z3 -> [AST] -> [AST] -> z3 AST
binaryListB :: forall (z3 :: * -> *). Bin z3 -> AST -> [AST] -> z3 AST
binaryListA :: forall (z3 :: * -> *). Bin z3 -> [AST] -> AST -> z3 AST
binaryNoList :: AST -> AST -> ReaderT ImplicitParameters Z3 AST
binaryListA :: [AST] -> AST -> ReaderT ImplicitParameters Z3 AST
binaryListB :: AST -> [AST] -> ReaderT ImplicitParameters Z3 AST
binaryListAB :: [AST] -> [AST] -> ReaderT ImplicitParameters Z3 AST
..} = case forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a of
  App TypeRep a
ca TypeRep b
_ -> case TypeRep a -> TypeRep [] -> Maybe (a :~~: [])
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
ca (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> *). Typeable a => TypeRep a
typeRep @[]) of
    Just a :~~: []
HRefl -> case forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b of
      App TypeRep a
cb TypeRep b
_ -> case TypeRep a -> TypeRep [] -> Maybe (a :~~: [])
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
cb (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> *). Typeable a => TypeRep a
typeRep @[]) of
        Just a :~~: []
HRefl ->  Term 'Transparent [b]
-> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable [a], Typeable [b]) =>
Term 'Transparent [a]
-> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
case1 Term 'Transparent a
Term 'Transparent [b]
x Term 'Transparent b
Term 'Transparent [b]
y -- a ~ [a1], b ~ [b1]
        Maybe (a :~~: [])
Nothing -> Term 'Transparent [b]
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable [a], Typeable b) =>
Term 'Transparent [a]
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
case2 Term 'Transparent a
Term 'Transparent [b]
x Term 'Transparent b
y -- a ~ [a1], b ~ f b1
      TypeRep b
_ -> Term 'Transparent [b]
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable [a], Typeable b) =>
Term 'Transparent [a]
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
case2 Term 'Transparent a
Term 'Transparent [b]
x Term 'Transparent b
y -- a ~ [a1]
    Maybe (a :~~: [])
Nothing -> case forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b of
      App TypeRep a
cb TypeRep b
_ -> case TypeRep a -> TypeRep [] -> Maybe (a :~~: [])
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
cb (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> *). Typeable a => TypeRep a
typeRep @[]) of
        Just a :~~: []
HRefl ->  Term 'Transparent a
-> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable [b]) =>
Term 'Transparent a
-> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
case3 Term 'Transparent a
x Term 'Transparent b
Term 'Transparent [b]
y -- a ~ f a1, b ~ [b1]
        Maybe (a :~~: [])
Nothing -> Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
case4 Term 'Transparent a
x Term 'Transparent b
y -- a ~ f a1, b ~ f b1
      TypeRep b
_ -> Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
case4 Term 'Transparent a
x Term 'Transparent b
y-- a ~ f a1
  TypeRep a
_ -> case forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b of
    App TypeRep a
cb TypeRep b
_ -> case TypeRep a -> TypeRep [] -> Maybe (a :~~: [])
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
cb (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> *). Typeable a => TypeRep a
typeRep @[]) of
      Just a :~~: []
HRefl ->  Term 'Transparent a
-> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable [b]) =>
Term 'Transparent a
-> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
case3 Term 'Transparent a
x Term 'Transparent b
Term 'Transparent [b]
y -- b ~ [b1]
      Maybe (a :~~: [])
Nothing -> Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
case4 Term 'Transparent a
x Term 'Transparent b
y -- b ~ f b1
    TypeRep b
_ -> Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
forall a b.
(Typeable a, Typeable b) =>
Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
case4 Term 'Transparent a
x Term 'Transparent b
y --
  where
  case1 :: forall a b. (Typeable [a], Typeable [b]) => Term 'Transparent [a] -> Term 'Transparent [b] -> Z3R AST
  case1 :: forall a b.
(Typeable [a], Typeable [b]) =>
Term 'Transparent [a]
-> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
case1 Term 'Transparent [a]
x Term 'Transparent [b]
y = do
    Either AST [AST]
rx <- Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
forall a.
Typeable [a] =>
Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
listASTs Goal
goal Term 'Transparent [a]
x Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
    Either AST [AST]
ry <- Goal
-> Term 'Transparent [b]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
forall a.
Typeable [a] =>
Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
listASTs Goal
goal Term 'Transparent [b]
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
    case (Either AST [AST]
rx,Either AST [AST]
ry) of
      (Right [AST]
xs,Right [AST]
ys) -> [AST] -> [AST] -> ReaderT ImplicitParameters Z3 AST
binaryListAB [AST]
xs [AST]
ys
      (Right [AST]
xs,Left AST
y) -> [AST] -> AST -> ReaderT ImplicitParameters Z3 AST
binaryListA [AST]
xs AST
y
      (Left AST
x,Right [AST]
ys) -> AST -> [AST] -> ReaderT ImplicitParameters Z3 AST
binaryListB AST
x [AST]
ys
      (Left AST
x,Left AST
y) -> AST -> AST -> ReaderT ImplicitParameters Z3 AST
binaryNoList AST
x AST
y
  case2 :: forall a b. (Typeable [a], Typeable b) => Term 'Transparent [a] -> Term 'Transparent b -> Z3R AST
  case2 :: forall a b.
(Typeable [a], Typeable b) =>
Term 'Transparent [a]
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
case2 Term 'Transparent [a]
x Term 'Transparent b
y = do
    Either AST [AST]
exs <- Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
forall a.
Typeable [a] =>
Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
listASTs Goal
goal Term 'Transparent [a]
x Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
    AST
y' <- Goal
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
forall x.
Typeable x =>
Goal
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
z3Predicate Goal
goal Term 'Transparent b
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
    case Either AST [AST]
exs of
      Right [AST]
xs -> [AST] -> AST -> ReaderT ImplicitParameters Z3 AST
binaryListA [AST]
xs AST
y'
      Left AST
x -> AST -> AST -> ReaderT ImplicitParameters Z3 AST
binaryNoList AST
x AST
y'
  case3 :: forall a b. (Typeable a, Typeable [b]) => Term 'Transparent a -> Term 'Transparent [b] -> Z3R AST
  case3 :: forall a b.
(Typeable a, Typeable [b]) =>
Term 'Transparent a
-> Term 'Transparent [b] -> ReaderT ImplicitParameters Z3 AST
case3 Term 'Transparent a
x Term 'Transparent [b]
y = do
    AST
x' <- Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
forall x.
Typeable x =>
Goal
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
z3Predicate Goal
goal Term 'Transparent a
x Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
    Either AST [AST]
eys <- Goal
-> Term 'Transparent [b]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
forall a.
Typeable [a] =>
Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
listASTs Goal
goal Term 'Transparent [b]
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
    case Either AST [AST]
eys of
      Right [AST]
ys -> AST -> [AST] -> ReaderT ImplicitParameters Z3 AST
binaryListB AST
x' [AST]
ys
      Left AST
y -> AST -> AST -> ReaderT ImplicitParameters Z3 AST
binaryNoList AST
x' AST
y
  case4 :: forall a b. (Typeable a, Typeable b) => Term 'Transparent a -> Term 'Transparent b -> Z3R AST
  case4 :: forall a b.
(Typeable a, Typeable b) =>
Term 'Transparent a
-> Term 'Transparent b -> ReaderT ImplicitParameters Z3 AST
case4 Term 'Transparent a
x Term 'Transparent b
y = do
    AST
xP <- Goal
-> Term 'Transparent a
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
forall x.
Typeable x =>
Goal
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
z3Predicate Goal
goal Term 'Transparent a
x Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
    AST
yP <- Goal
-> Term 'Transparent b
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
forall x.
Typeable x =>
Goal
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
z3Predicate Goal
goal Term 'Transparent b
y Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
    AST -> AST -> ReaderT ImplicitParameters Z3 AST
binaryNoList AST
xP AST
yP

data CompareOp = Strict Ordering | ReflexiveClosure Ordering

compareSymbolic :: MonadZ3 z3 => CompareOp -> [AST] -> [AST] -> z3 AST
compareSymbolic :: forall (z3 :: * -> *).
MonadZ3 z3 =>
CompareOp -> [AST] -> [AST] -> z3 AST
compareSymbolic CompareOp
cmpOp [AST]
xs [AST]
ys = do
  let (AST -> AST -> z3 AST
mkCmp,z3 AST
mkConstShort,z3 AST
mkConstLong) = CompareOp -> (AST -> AST -> z3 AST, z3 AST, z3 AST)
forall (z3 :: * -> *).
MonadZ3 z3 =>
CompareOp -> (AST -> AST -> z3 AST, z3 AST, z3 AST)
compareParams CompareOp
cmpOp
  [AST]
strictComps <- ([AST] -> z3 AST) -> [[AST]] -> z3 [AST]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkAnd ([[AST]] -> z3 [AST]) -> z3 [[AST]] -> z3 [AST]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [AST] -> z3 [[AST]]
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 [[AST]]
clauses ([AST] -> z3 [[AST]]) -> z3 [AST] -> z3 [[AST]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (AST -> AST -> z3 AST) -> z3 AST -> z3 AST -> z3 [AST]
forall (z3 :: * -> *).
MonadZ3 z3 =>
(AST -> AST -> z3 AST) -> z3 AST -> z3 AST -> z3 [AST]
compareASTLists AST -> AST -> z3 AST
mkCmp z3 AST
mkConstShort z3 AST
mkConstLong
  case CompareOp
cmpOp of
    Strict{} -> [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkOr [AST]
strictComps
    ReflexiveClosure{} -> do
      AST
eqComp <- [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkAnd ([AST] -> z3 AST) -> z3 [AST] -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (AST -> AST -> z3 AST) -> z3 AST -> z3 AST -> z3 [AST]
forall (z3 :: * -> *).
MonadZ3 z3 =>
(AST -> AST -> z3 AST) -> z3 AST -> z3 AST -> z3 [AST]
compareASTLists AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkFalse z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkFalse
      [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkOr ([AST] -> z3 AST) -> [AST] -> z3 AST
forall a b. (a -> b) -> a -> b
$ AST
eqComp AST -> [AST] -> [AST]
forall a. a -> [a] -> [a]
: [AST]
strictComps
  where
    compareParams :: MonadZ3 z3 => CompareOp -> (AST -> AST -> z3 AST, z3 AST, z3 AST)
    compareParams :: forall (z3 :: * -> *).
MonadZ3 z3 =>
CompareOp -> (AST -> AST -> z3 AST, z3 AST, z3 AST)
compareParams (Strict Ordering
EQ) = (AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq,z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkFalse,z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkFalse)
    compareParams (Strict Ordering
LT) = (AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkLt,z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkTrue,z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkFalse)
    compareParams (Strict Ordering
GT) = (AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkGt,z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkFalse,z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => z3 AST
mkTrue)
    compareParams (ReflexiveClosure Ordering
x) = CompareOp -> (AST -> AST -> z3 AST, z3 AST, z3 AST)
forall (z3 :: * -> *).
MonadZ3 z3 =>
CompareOp -> (AST -> AST -> z3 AST, z3 AST, z3 AST)
compareParams (CompareOp -> (AST -> AST -> z3 AST, z3 AST, z3 AST))
-> CompareOp -> (AST -> AST -> z3 AST, z3 AST, z3 AST)
forall a b. (a -> b) -> a -> b
$ Ordering -> CompareOp
Strict Ordering
x
    compareASTLists :: MonadZ3 z3 => (AST -> AST -> z3 AST) -> z3 AST -> z3 AST -> z3 [AST]
    compareASTLists :: forall (z3 :: * -> *).
MonadZ3 z3 =>
(AST -> AST -> z3 AST) -> z3 AST -> z3 AST -> z3 [AST]
compareASTLists AST -> AST -> z3 AST
mkCmp z3 AST
mkConstShort z3 AST
mkConstLong = [z3 AST] -> z3 [AST]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ((Maybe AST -> Maybe AST -> z3 AST) -> [AST] -> [AST] -> [z3 AST]
forall a b c. (Maybe a -> Maybe b -> c) -> [a] -> [b] -> [c]
zipWithLongest ((AST -> AST -> z3 AST)
-> z3 AST -> z3 AST -> Maybe AST -> Maybe AST -> z3 AST
forall (z3 :: * -> *).
MonadZ3 z3 =>
(AST -> AST -> z3 AST)
-> z3 AST -> z3 AST -> Maybe AST -> Maybe AST -> z3 AST
comparePositions AST -> AST -> z3 AST
mkCmp z3 AST
mkConstShort z3 AST
mkConstLong) [AST]
xs [AST]
ys)
    comparePositions :: MonadZ3 z3 => (AST -> AST -> z3 AST) -> z3 AST -> z3 AST -> Maybe AST -> Maybe AST -> z3 AST
    comparePositions :: forall (z3 :: * -> *).
MonadZ3 z3 =>
(AST -> AST -> z3 AST)
-> z3 AST -> z3 AST -> Maybe AST -> Maybe AST -> z3 AST
comparePositions AST -> AST -> z3 AST
mkCmp z3 AST
_ z3 AST
_ (Just AST
x) (Just AST
y) = AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkIntermediateBoolean (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> z3 AST
mkCmp AST
x AST
y
    comparePositions AST -> AST -> z3 AST
_ z3 AST
mkConstShort z3 AST
_ Maybe AST
Nothing (Just AST
_) = z3 AST
mkConstShort
    comparePositions AST -> AST -> z3 AST
_ z3 AST
_ z3 AST
mkConstLong (Just AST
_) Maybe AST
Nothing = z3 AST
mkConstLong
    comparePositions AST -> AST -> z3 AST
_ z3 AST
_ z3 AST
_ Maybe AST
Nothing Maybe AST
Nothing = String -> z3 AST
forall a. HasCallStack => String -> a
error String
"impossible: invariant of zipWithLongest"
    clauses :: MonadZ3 z3 => [AST] -> z3 [[AST]]
    clauses :: forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 [[AST]]
clauses [] = [[AST]] -> z3 [[AST]]
forall a. a -> z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    clauses [AST
b1] = [[AST]] -> z3 [[AST]]
forall a. a -> z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[AST
b1]]
    clauses (AST
b:[AST]
bs) = do
      AST
nb <- AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkNot AST
b
      [[AST]]
r <- [AST] -> z3 [[AST]]
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 [[AST]]
clauses [AST]
bs
      [[AST]] -> z3 [[AST]]
forall a. a -> z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([[AST]] -> z3 [[AST]]) -> [[AST]] -> z3 [[AST]]
forall a b. (a -> b) -> a -> b
$ [AST
b] [AST] -> [[AST]] -> [[AST]]
forall a. a -> [a] -> [a]
: ((AST
nb :) ([AST] -> [AST]) -> [[AST]] -> [[AST]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[AST]]
r)

mkIntermediateBoolean :: MonadZ3 z3 => AST -> z3 AST
mkIntermediateBoolean :: forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkIntermediateBoolean AST
x = do
  AST
b <- String -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 AST
mkFreshBoolVar String
"b"
  AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
b AST
x

listASTs :: forall a. Typeable [a] => Goal -> Term 'Transparent [a] -> Map SomeVar SymbolicInfo -> [((SomeVar, Int), AST)] -> Z3R (Either AST [AST])
listASTs :: forall a.
Typeable [a] =>
Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
listASTs Goal
goal (Reverse (Reverse Term 'Transparent [a1]
t)) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Goal
-> Term 'Transparent [a1]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
forall a.
Typeable [a] =>
Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
listASTs Goal
goal Term 'Transparent [a1]
t Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
listASTs Goal
goal (Reverse Term 'Transparent [a1]
t) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = do
  Either AST [AST]
r <- Goal
-> Term 'Transparent [a1]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
forall a.
Typeable [a] =>
Goal
-> Term 'Transparent [a]
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> Z3R (Either AST [AST])
listASTs Goal
goal Term 'Transparent [a1]
t Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
  case Either AST [AST]
r of
    Right [AST]
as -> Either AST [AST] -> Z3R (Either AST [AST])
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either AST [AST] -> Z3R (Either AST [AST]))
-> Either AST [AST] -> Z3R (Either AST [AST])
forall a b. (a -> b) -> a -> b
$ [AST] -> Either AST [AST]
forall a b. b -> Either a b
Right ([AST] -> Either AST [AST]) -> [AST] -> Either AST [AST]
forall a b. (a -> b) -> a -> b
$ [AST] -> [AST]
forall a. [a] -> [a]
reverse [AST]
as
    Left AST
a -> AST -> Either AST [AST]
forall a b. a -> Either a b
Left (AST -> Either AST [AST])
-> ReaderT ImplicitParameters Z3 AST -> Z3R (Either AST [AST])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Goal -> AST -> ReaderT ImplicitParameters Z3 AST
reverseSequence Goal
goal AST
a
listASTs Goal
_ (ListLit [a1]
xs) Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ =
  forall {k} (a :: k) r. Typeable a => [Case a r] -> r
forall a r. Typeable a => [Case a r] -> r
matchType @a
    [ forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @Integer (((Integer :~~: a) -> Z3R (Either AST [AST]))
 -> Case a (Z3R (Either AST [AST])))
-> ((Integer :~~: a) -> Z3R (Either AST [AST]))
-> Case a (Z3R (Either AST [AST]))
forall a b. (a -> b) -> a -> b
$ \Integer :~~: a
HRefl -> [AST] -> Either AST [AST]
forall a b. b -> Either a b
Right ([AST] -> Either AST [AST])
-> ReaderT ImplicitParameters Z3 [AST] -> Z3R (Either AST [AST])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a1 -> ReaderT ImplicitParameters Z3 AST)
-> [a1] -> ReaderT ImplicitParameters Z3 [AST]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Integer -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum (Integer -> ReaderT ImplicitParameters Z3 AST)
-> (a1 -> Integer) -> a1 -> ReaderT ImplicitParameters Z3 AST
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a1 -> Integer
forall a. Integral a => a -> Integer
toInteger) [a1]
xs
    , forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @Char (((Char :~~: a) -> Z3R (Either AST [AST]))
 -> Case a (Z3R (Either AST [AST])))
-> ((Char :~~: a) -> Z3R (Either AST [AST]))
-> Case a (Z3R (Either AST [AST]))
forall a b. (a -> b) -> a -> b
$ \Char :~~: a
HRefl -> AST -> Either AST [AST]
forall a b. a -> Either a b
Left (AST -> Either AST [AST])
-> ReaderT ImplicitParameters Z3 AST -> Z3R (Either AST [AST])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => String -> z3 AST
mkString [a1]
String
xs
    , Z3R (Either AST [AST]) -> Case a (Z3R (Either AST [AST]))
forall {k} r (x :: k). r -> Case x r
fallbackCase' (Z3R (Either AST [AST]) -> Case a (Z3R (Either AST [AST])))
-> Z3R (Either AST [AST]) -> Case a (Z3R (Either AST [AST]))
forall a b. (a -> b) -> a -> b
$ String -> Z3R (Either AST [AST])
forall a. HasCallStack => String -> a
error (String -> Z3R (Either AST [AST]))
-> String -> Z3R (Either AST [AST])
forall a b. (a -> b) -> a -> b
$ String
"list literal of unsupported type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep [a] -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[a])
    ]
listASTs Goal
_ (All e a1
x Int
n) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Either AST [AST] -> Z3R (Either AST [AST])
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either AST [AST] -> Z3R (Either AST [AST]))
-> ([AST] -> Either AST [AST]) -> [AST] -> Z3R (Either AST [AST])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AST] -> Either AST [AST]
forall a b. b -> Either a b
Right ([AST] -> Z3R (Either AST [AST]))
-> [AST] -> Z3R (Either AST [AST])
forall a b. (a -> b) -> a -> b
$ [(SomeVar, Int)] -> [((SomeVar, Int), AST)] -> [AST]
forall a b. Eq a => [a] -> [(a, b)] -> [b]
lookupList (e a1 -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
weaveVariables e a1
x Int
n Map SomeVar SymbolicInfo
e) [((SomeVar, Int), AST)]
vars
listASTs Goal
_ (Current e [a]
x Int
n) Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = Either AST [AST] -> Z3R (Either AST [AST])
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either AST [AST] -> Z3R (Either AST [AST]))
-> ([AST] -> Either AST [AST]) -> [AST] -> Z3R (Either AST [AST])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST -> Either AST [AST]
forall a b. a -> Either a b
Left (AST -> Either AST [AST])
-> ([AST] -> AST) -> [AST] -> Either AST [AST]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AST] -> AST
forall a. HasCallStack => [a] -> a
head ([AST] -> Z3R (Either AST [AST]))
-> [AST] -> Z3R (Either AST [AST])
forall a b. (a -> b) -> a -> b
$ [(SomeVar, Int)] -> [((SomeVar, Int), AST)] -> [AST]
forall a b. Eq a => [a] -> [(a, b)] -> [b]
lookupList (e [a] -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
weaveVariables e [a]
x Int
n Map SomeVar SymbolicInfo
e) [((SomeVar, Int), AST)]
vars
listASTs Goal
_ Add{} Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = String -> Z3R (Either AST [AST])
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
listASTs Goal
_ Sub{} Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = String -> Z3R (Either AST [AST])
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
listASTs Goal
_ Mul{} Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = String -> Z3R (Either AST [AST])
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
listASTs Goal
_ Sum{} Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = String -> Z3R (Either AST [AST])
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
listASTs Goal
_ Product{} Map SomeVar SymbolicInfo
_ [((SomeVar, Int), AST)]
_ = String -> Z3R (Either AST [AST])
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"

reverseSequence :: Goal -> AST -> Z3R AST
reverseSequence :: Goal -> AST -> ReaderT ImplicitParameters Z3 AST
reverseSequence Goal
goal AST
x = do
  AST
y <- String -> Sort -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => String -> Sort -> z3 AST
mkFreshVar String
"reversed" (Sort -> ReaderT ImplicitParameters Z3 AST)
-> ReaderT ImplicitParameters Z3 Sort
-> ReaderT ImplicitParameters Z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> ReaderT ImplicitParameters Z3 Sort
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 Sort
getSort AST
x
  AST
lx <- AST -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkSeqLength AST
x
  AST
ly <- AST -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> z3 AST
mkSeqLength AST
y
  Z3 () -> ReaderT ImplicitParameters Z3 ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Goal -> AST -> Z3 ()
forall (z3 :: * -> *). MonadZ3 z3 => Goal -> AST -> z3 ()
goalAssert Goal
goal (AST -> Z3 ()) -> Z3 AST -> Z3 ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
lx AST
ly)
  Int
m <- (ImplicitParameters -> Int) -> ReaderT ImplicitParameters Z3 Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ImplicitParameters -> Int
maxSeqLengthParameter
  Z3 () -> ReaderT ImplicitParameters Z3 ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Goal -> AST -> Z3 ()
forall (z3 :: * -> *). MonadZ3 z3 => Goal -> AST -> z3 ()
goalAssert Goal
goal (AST -> Z3 ()) -> Z3 AST -> Z3 ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkLe AST
lx (AST -> Z3 AST) -> Z3 AST -> Z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> Z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum Int
m)
  [Int]
-> (Int -> ReaderT ImplicitParameters Z3 ())
-> ReaderT ImplicitParameters Z3 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0 .. Int
m] (Z3 () -> ReaderT ImplicitParameters Z3 ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Z3 () -> ReaderT ImplicitParameters Z3 ())
-> (AST -> Z3 ()) -> AST -> ReaderT ImplicitParameters Z3 ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> AST -> Z3 ()
forall (z3 :: * -> *). MonadZ3 z3 => Goal -> AST -> z3 ()
goalAssert Goal
goal (AST -> ReaderT ImplicitParameters Z3 ())
-> (Int -> ReaderT ImplicitParameters Z3 AST)
-> Int
-> ReaderT ImplicitParameters Z3 ()
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (AST, AST)
-> (AST, AST) -> Int -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *).
MonadZ3 z3 =>
(AST, AST) -> (AST, AST) -> Int -> z3 AST
pos (AST
x,AST
lx) (AST
y,AST
ly))
  AST -> ReaderT ImplicitParameters Z3 AST
forall a. a -> ReaderT ImplicitParameters Z3 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AST
y
  where
    pos :: MonadZ3 z3 => (AST,AST) -> (AST,AST) -> Int -> z3 AST
    pos :: forall (z3 :: * -> *).
MonadZ3 z3 =>
(AST, AST) -> (AST, AST) -> Int -> z3 AST
pos (AST
x,AST
lx) (AST
y,AST
ly) Int
i = do
      AST
index <- Int -> z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum Int
i
      AST
pre <- AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkGe AST
lx AST
index
      AST
xi <- AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkSeqAt AST
x AST
index
      AST
index' <- Int -> z3 AST
forall (z3 :: * -> *) a. (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
      AST
yj <- AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkSeqAt AST
y (AST -> z3 AST) -> z3 AST -> z3 AST
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [AST] -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => [AST] -> z3 AST
mkSub [AST
ly,AST
index']
      AST
con <- AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkEq AST
xi AST
yj
      AST -> AST -> z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkImplies AST
pre AST
con

unknownVariablesError :: VarExp e => e a -> b
unknownVariablesError :: forall (e :: * -> *) a b. VarExp e => e a -> b
unknownVariablesError e a
x = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"unknown variable(s) {" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var a -> String) -> [Var a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> String
forall a. Var a -> String
varname ([Var a] -> [String]) -> [Var a] -> [String]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
x) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"

weaveVariables :: (VarExp e, Typeable a) => e a -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar,Int)]
weaveVariables :: forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Map SomeVar SymbolicInfo -> [(SomeVar, Int)]
weaveVariables e a
vs Int
n Map SomeVar SymbolicInfo
e =
  [(SomeVar, Int)] -> [(SomeVar, Int)]
forall a. [a] -> [a]
reverse ([(SomeVar, Int)] -> [(SomeVar, Int)])
-> ([Var a] -> [(SomeVar, Int)]) -> [Var a] -> [(SomeVar, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [(SomeVar, Int)] -> [(SomeVar, Int)]
forall a. Int -> [a] -> [a]
drop Int
n ([(SomeVar, Int)] -> [(SomeVar, Int)])
-> ([Var a] -> [(SomeVar, Int)]) -> [Var a] -> [(SomeVar, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SomeVar, Int)] -> [(SomeVar, Int)]
forall a. [a] -> [a]
reverse -- drop last n variables
  ([(SomeVar, Int)] -> [(SomeVar, Int)])
-> ([Var a] -> [(SomeVar, Int)]) -> [Var a] -> [(SomeVar, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SomeVar, Int, Int) -> (SomeVar, Int))
-> [(SomeVar, Int, Int)] -> [(SomeVar, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeVar
x,Int
y,Int
_) -> (SomeVar
x,Int
y))
  ([(SomeVar, Int, Int)] -> [(SomeVar, Int)])
-> ([Var a] -> [(SomeVar, Int, Int)])
-> [Var a]
-> [(SomeVar, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SomeVar, Int, Int) -> Int)
-> [(SomeVar, Int, Int)] -> [(SomeVar, Int, Int)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (SomeVar, Int, Int) -> Int
forall a b c. (a, b, c) -> c
thd3
  ([(SomeVar, Int, Int)] -> [(SomeVar, Int, Int)])
-> ([Var a] -> [(SomeVar, Int, Int)])
-> [Var a]
-> [(SomeVar, Int, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SomeVar, [(Int, Int)]) -> [(SomeVar, Int, Int)])
-> [(SomeVar, [(Int, Int)])] -> [(SomeVar, Int, Int)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(SomeVar
x,[(Int, Int)]
jks) -> ((Int, Int) -> (SomeVar, Int, Int))
-> [(Int, Int)] -> [(SomeVar, Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
j,Int
k) -> (SomeVar
x,Int
j,Int
k)) [(Int, Int)]
jks)
  ([(SomeVar, [(Int, Int)])] -> [(SomeVar, Int, Int)])
-> ([Var a] -> [(SomeVar, [(Int, Int)])])
-> [Var a]
-> [(SomeVar, Int, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var a -> Maybe (SomeVar, [(Int, Int)]))
-> [Var a] -> [(SomeVar, [(Int, Int)])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((\SomeVar
v -> ((SomeVar
v,) ([(Int, Int)] -> (SomeVar, [(Int, Int)]))
-> (SymbolicInfo -> [(Int, Int)])
-> SymbolicInfo
-> (SomeVar, [(Int, Int)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolicInfo -> [(Int, Int)]
storedValues) (SymbolicInfo -> (SomeVar, [(Int, Int)]))
-> Maybe SymbolicInfo -> Maybe (SomeVar, [(Int, Int)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeVar -> Map SomeVar SymbolicInfo -> Maybe SymbolicInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeVar
v Map SomeVar SymbolicInfo
e) (SomeVar -> Maybe (SomeVar, [(Int, Int)]))
-> (Var a -> SomeVar) -> Var a -> Maybe (SomeVar, [(Int, Int)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar)
  ([Var a] -> [(SomeVar, Int)]) -> [Var a] -> [(SomeVar, Int)]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
vs

lookupList :: Eq a => [a] -> [(a, b)] -> [b]
lookupList :: forall a b. Eq a => [a] -> [(a, b)] -> [b]
lookupList [a]
vs [(a, b)]
vars = (a -> Maybe b) -> [a] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (a -> [(a, b)] -> Maybe b
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`List.lookup` [(a, b)]
vars) [a]
vs

assertOverflowChecks :: Goal -> Term 'Transparent Integer ->  Map SomeVar SymbolicInfo -> [((SomeVar, Int), AST)] -> Z3R ()
assertOverflowChecks :: Goal
-> Term 'Transparent Integer
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 ()
assertOverflowChecks Goal
goal Term 'Transparent Integer
t Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars = do
  AST
ast <- Goal
-> Term 'Transparent Integer
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
forall x.
Typeable x =>
Goal
-> Term 'Transparent x
-> Map SomeVar SymbolicInfo
-> [((SomeVar, Int), AST)]
-> ReaderT ImplicitParameters Z3 AST
z3Predicate Goal
goal Term 'Transparent Integer
t Map SomeVar SymbolicInfo
e [((SomeVar, Int), AST)]
vars
  Goal -> AST -> ReaderT ImplicitParameters Z3 ()
overflowConstraints Goal
goal AST
ast

overflowConstraints :: Goal -> AST -> Z3R ()
overflowConstraints :: Goal -> AST -> ReaderT ImplicitParameters Z3 ()
overflowConstraints Goal
goal AST
x = do
  AST
minInt <- Integer -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => Integer -> z3 AST
mkInteger (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ forall a. Bounded a => a
minBound @Int)
  AST
maxInt <- Integer -> ReaderT ImplicitParameters Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => Integer -> z3 AST
mkInteger (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ forall a. Bounded a => a
maxBound @Int)
  Z3 () -> ReaderT ImplicitParameters Z3 ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Goal -> AST -> Z3 ()
forall (z3 :: * -> *). MonadZ3 z3 => Goal -> AST -> z3 ()
goalAssert Goal
goal (AST -> Z3 ()) -> Z3 AST -> Z3 ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkGe AST
x AST
minInt)
  Z3 () -> ReaderT ImplicitParameters Z3 ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT ImplicitParameters m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Goal -> AST -> Z3 ()
forall (z3 :: * -> *). MonadZ3 z3 => Goal -> AST -> z3 ()
goalAssert Goal
goal (AST -> Z3 ()) -> Z3 AST -> Z3 ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< AST -> AST -> Z3 AST
forall (z3 :: * -> *). MonadZ3 z3 => AST -> AST -> z3 AST
mkLe AST
x AST
maxInt)