{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Crux.Config.Solver (
  parseSolverConfig,
  SolverConfig(..),
  SolverOnline(..),
  SolverOffline(..),
  HasDefaultFloatRepr(..),
  sameSolver
  ) where

import           Control.Applicative ( (<|>), empty, Alternative )
import           Data.List.Split (wordsBy)
import qualified Data.Foldable as F
import qualified Data.Traversable as T
import           Text.Printf ( printf )
import qualified What4.Expr.Builder as WEB
import qualified What4.InterpretedFloatingPoint as WIF

import qualified Crux.Config.Common as CCC

data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP
  deriving (SolverOnline -> SolverOnline -> Bool
(SolverOnline -> SolverOnline -> Bool)
-> (SolverOnline -> SolverOnline -> Bool) -> Eq SolverOnline
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SolverOnline -> SolverOnline -> Bool
== :: SolverOnline -> SolverOnline -> Bool
$c/= :: SolverOnline -> SolverOnline -> Bool
/= :: SolverOnline -> SolverOnline -> Bool
Eq, Eq SolverOnline
Eq SolverOnline =>
(SolverOnline -> SolverOnline -> Ordering)
-> (SolverOnline -> SolverOnline -> Bool)
-> (SolverOnline -> SolverOnline -> Bool)
-> (SolverOnline -> SolverOnline -> Bool)
-> (SolverOnline -> SolverOnline -> Bool)
-> (SolverOnline -> SolverOnline -> SolverOnline)
-> (SolverOnline -> SolverOnline -> SolverOnline)
-> Ord SolverOnline
SolverOnline -> SolverOnline -> Bool
SolverOnline -> SolverOnline -> Ordering
SolverOnline -> SolverOnline -> SolverOnline
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SolverOnline -> SolverOnline -> Ordering
compare :: SolverOnline -> SolverOnline -> Ordering
$c< :: SolverOnline -> SolverOnline -> Bool
< :: SolverOnline -> SolverOnline -> Bool
$c<= :: SolverOnline -> SolverOnline -> Bool
<= :: SolverOnline -> SolverOnline -> Bool
$c> :: SolverOnline -> SolverOnline -> Bool
> :: SolverOnline -> SolverOnline -> Bool
$c>= :: SolverOnline -> SolverOnline -> Bool
>= :: SolverOnline -> SolverOnline -> Bool
$cmax :: SolverOnline -> SolverOnline -> SolverOnline
max :: SolverOnline -> SolverOnline -> SolverOnline
$cmin :: SolverOnline -> SolverOnline -> SolverOnline
min :: SolverOnline -> SolverOnline -> SolverOnline
Ord, Int -> SolverOnline -> String -> String
[SolverOnline] -> String -> String
SolverOnline -> String
(Int -> SolverOnline -> String -> String)
-> (SolverOnline -> String)
-> ([SolverOnline] -> String -> String)
-> Show SolverOnline
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> SolverOnline -> String -> String
showsPrec :: Int -> SolverOnline -> String -> String
$cshow :: SolverOnline -> String
show :: SolverOnline -> String
$cshowList :: [SolverOnline] -> String -> String
showList :: [SolverOnline] -> String -> String
Show)
data SolverOffline = SolverOnline SolverOnline | Boolector | DReal
  deriving (SolverOffline -> SolverOffline -> Bool
(SolverOffline -> SolverOffline -> Bool)
-> (SolverOffline -> SolverOffline -> Bool) -> Eq SolverOffline
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SolverOffline -> SolverOffline -> Bool
== :: SolverOffline -> SolverOffline -> Bool
$c/= :: SolverOffline -> SolverOffline -> Bool
/= :: SolverOffline -> SolverOffline -> Bool
Eq, Eq SolverOffline
Eq SolverOffline =>
(SolverOffline -> SolverOffline -> Ordering)
-> (SolverOffline -> SolverOffline -> Bool)
-> (SolverOffline -> SolverOffline -> Bool)
-> (SolverOffline -> SolverOffline -> Bool)
-> (SolverOffline -> SolverOffline -> Bool)
-> (SolverOffline -> SolverOffline -> SolverOffline)
-> (SolverOffline -> SolverOffline -> SolverOffline)
-> Ord SolverOffline
SolverOffline -> SolverOffline -> Bool
SolverOffline -> SolverOffline -> Ordering
SolverOffline -> SolverOffline -> SolverOffline
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SolverOffline -> SolverOffline -> Ordering
compare :: SolverOffline -> SolverOffline -> Ordering
$c< :: SolverOffline -> SolverOffline -> Bool
< :: SolverOffline -> SolverOffline -> Bool
$c<= :: SolverOffline -> SolverOffline -> Bool
<= :: SolverOffline -> SolverOffline -> Bool
$c> :: SolverOffline -> SolverOffline -> Bool
> :: SolverOffline -> SolverOffline -> Bool
$c>= :: SolverOffline -> SolverOffline -> Bool
>= :: SolverOffline -> SolverOffline -> Bool
$cmax :: SolverOffline -> SolverOffline -> SolverOffline
max :: SolverOffline -> SolverOffline -> SolverOffline
$cmin :: SolverOffline -> SolverOffline -> SolverOffline
min :: SolverOffline -> SolverOffline -> SolverOffline
Ord, Int -> SolverOffline -> String -> String
[SolverOffline] -> String -> String
SolverOffline -> String
(Int -> SolverOffline -> String -> String)
-> (SolverOffline -> String)
-> ([SolverOffline] -> String -> String)
-> Show SolverOffline
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> SolverOffline -> String -> String
showsPrec :: Int -> SolverOffline -> String -> String
$cshow :: SolverOffline -> String
show :: SolverOffline -> String
$cshowList :: [SolverOffline] -> String -> String
showList :: [SolverOffline] -> String -> String
Show)

class HasDefaultFloatRepr solver where
  withDefaultFloatRepr ::
    st s ->
    solver ->
    (forall fm. (WIF.IsInterpretedFloatExprBuilder (WEB.ExprBuilder s st (WEB.Flags fm))) => WEB.FloatModeRepr fm -> a) ->
    a

instance HasDefaultFloatRepr SolverOnline where
  withDefaultFloatRepr :: forall (st :: * -> *) s a.
st s
-> SolverOnline
-> (forall (fm :: FloatMode).
    IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
    FloatModeRepr fm -> a)
-> a
withDefaultFloatRepr st s
_ SolverOnline
s forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k =
    case SolverOnline
s of
      SolverOnline
CVC4 -> FloatModeRepr 'FloatReal -> a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k FloatModeRepr 'FloatReal
WEB.FloatRealRepr
      SolverOnline
CVC5 -> FloatModeRepr 'FloatReal -> a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k FloatModeRepr 'FloatReal
WEB.FloatRealRepr
      SolverOnline
STP -> FloatModeRepr 'FloatReal -> a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k FloatModeRepr 'FloatReal
WEB.FloatRealRepr
      SolverOnline
Yices -> FloatModeRepr 'FloatReal -> a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k FloatModeRepr 'FloatReal
WEB.FloatRealRepr
      SolverOnline
Z3 -> FloatModeRepr 'FloatIEEE -> a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k FloatModeRepr 'FloatIEEE
WEB.FloatIEEERepr

instance HasDefaultFloatRepr SolverOffline where
  withDefaultFloatRepr :: forall (st :: * -> *) s a.
st s
-> SolverOffline
-> (forall (fm :: FloatMode).
    IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
    FloatModeRepr fm -> a)
-> a
withDefaultFloatRepr st s
st SolverOffline
s forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k =
    case SolverOffline
s of
      SolverOnline SolverOnline
s' -> st s
-> SolverOnline
-> (forall (fm :: FloatMode).
    IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
    FloatModeRepr fm -> a)
-> a
forall solver (st :: * -> *) s a.
HasDefaultFloatRepr solver =>
st s
-> solver
-> (forall (fm :: FloatMode).
    IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
    FloatModeRepr fm -> a)
-> a
forall (st :: * -> *) s a.
st s
-> SolverOnline
-> (forall (fm :: FloatMode).
    IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
    FloatModeRepr fm -> a)
-> a
withDefaultFloatRepr st s
st SolverOnline
s' FloatModeRepr fm -> a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k
      SolverOffline
Boolector -> FloatModeRepr 'FloatUninterpreted -> a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k FloatModeRepr 'FloatUninterpreted
WEB.FloatUninterpretedRepr
      SolverOffline
DReal -> FloatModeRepr 'FloatReal -> a
forall (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder s st (Flags fm)) =>
FloatModeRepr fm -> a
k FloatModeRepr 'FloatReal
WEB.FloatRealRepr

-- | Test to see if an online and offline solver are actually the same
sameSolver :: SolverOnline -> SolverOffline -> Bool
sameSolver :: SolverOnline -> SolverOffline -> Bool
sameSolver SolverOnline
o SolverOffline
f =
  case SolverOffline
f of
    SolverOnline SolverOnline
s' -> SolverOnline
o SolverOnline -> SolverOnline -> Bool
forall a. Eq a => a -> a -> Bool
== SolverOnline
s'
    SolverOffline
_ -> Bool
False

data SolverConfig = SingleOnlineSolver SolverOnline
                  -- ^ Use a single online solver for both path satisfiability
                  -- checking and goal discharge

                  | OnlineSolverWithOfflineGoals SolverOnline SolverOffline
                  -- ^ Use an online solver for path satisfiability checking and
                  -- use an offline solver for goal discharge

                  | OnlineSolverWithSeparateOnlineGoals SolverOnline SolverOnline
                  -- ^ Use one online solver connection for path satisfiability
                  -- checking and a separate online solver connection for goal
                  -- discharge.  INVARIANT: the solvers must be distinct.

                  | OnlyOfflineSolvers [SolverOffline]
                  -- ^ Try any of a number of offline solvers with no support
                  -- for path satisfiability checking

-- | A type that contains a validated instance of a value or a list of messages
-- describing why it was not valid
--
-- This is basically `Either [String] a` but with instances that accumulate
-- error messages across alternatives unless there is a success.
data Validated a = Invalid [String] | Validated a
  deriving (Int -> Validated a -> String -> String
[Validated a] -> String -> String
Validated a -> String
(Int -> Validated a -> String -> String)
-> (Validated a -> String)
-> ([Validated a] -> String -> String)
-> Show (Validated a)
forall a. Show a => Int -> Validated a -> String -> String
forall a. Show a => [Validated a] -> String -> String
forall a. Show a => Validated a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Validated a -> String -> String
showsPrec :: Int -> Validated a -> String -> String
$cshow :: forall a. Show a => Validated a -> String
show :: Validated a -> String
$cshowList :: forall a. Show a => [Validated a] -> String -> String
showList :: [Validated a] -> String -> String
Show, (forall a b. (a -> b) -> Validated a -> Validated b)
-> (forall a b. a -> Validated b -> Validated a)
-> Functor Validated
forall a b. a -> Validated b -> Validated a
forall a b. (a -> b) -> Validated a -> Validated 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) -> Validated a -> Validated b
fmap :: forall a b. (a -> b) -> Validated a -> Validated b
$c<$ :: forall a b. a -> Validated b -> Validated a
<$ :: forall a b. a -> Validated b -> Validated a
Functor, (forall m. Monoid m => Validated m -> m)
-> (forall m a. Monoid m => (a -> m) -> Validated a -> m)
-> (forall m a. Monoid m => (a -> m) -> Validated a -> m)
-> (forall a b. (a -> b -> b) -> b -> Validated a -> b)
-> (forall a b. (a -> b -> b) -> b -> Validated a -> b)
-> (forall b a. (b -> a -> b) -> b -> Validated a -> b)
-> (forall b a. (b -> a -> b) -> b -> Validated a -> b)
-> (forall a. (a -> a -> a) -> Validated a -> a)
-> (forall a. (a -> a -> a) -> Validated a -> a)
-> (forall a. Validated a -> [a])
-> (forall a. Validated a -> Bool)
-> (forall a. Validated a -> Int)
-> (forall a. Eq a => a -> Validated a -> Bool)
-> (forall a. Ord a => Validated a -> a)
-> (forall a. Ord a => Validated a -> a)
-> (forall a. Num a => Validated a -> a)
-> (forall a. Num a => Validated a -> a)
-> Foldable Validated
forall a. Eq a => a -> Validated a -> Bool
forall a. Num a => Validated a -> a
forall a. Ord a => Validated a -> a
forall m. Monoid m => Validated m -> m
forall a. Validated a -> Bool
forall a. Validated a -> Int
forall a. Validated a -> [a]
forall a. (a -> a -> a) -> Validated a -> a
forall m a. Monoid m => (a -> m) -> Validated a -> m
forall b a. (b -> a -> b) -> b -> Validated a -> b
forall a b. (a -> b -> b) -> b -> Validated a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Validated m -> m
fold :: forall m. Monoid m => Validated m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Validated a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Validated a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Validated a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Validated a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Validated a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Validated a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Validated a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Validated a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Validated a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Validated a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Validated a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Validated a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Validated a -> a
foldr1 :: forall a. (a -> a -> a) -> Validated a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Validated a -> a
foldl1 :: forall a. (a -> a -> a) -> Validated a -> a
$ctoList :: forall a. Validated a -> [a]
toList :: forall a. Validated a -> [a]
$cnull :: forall a. Validated a -> Bool
null :: forall a. Validated a -> Bool
$clength :: forall a. Validated a -> Int
length :: forall a. Validated a -> Int
$celem :: forall a. Eq a => a -> Validated a -> Bool
elem :: forall a. Eq a => a -> Validated a -> Bool
$cmaximum :: forall a. Ord a => Validated a -> a
maximum :: forall a. Ord a => Validated a -> a
$cminimum :: forall a. Ord a => Validated a -> a
minimum :: forall a. Ord a => Validated a -> a
$csum :: forall a. Num a => Validated a -> a
sum :: forall a. Num a => Validated a -> a
$cproduct :: forall a. Num a => Validated a -> a
product :: forall a. Num a => Validated a -> a
F.Foldable, Functor Validated
Foldable Validated
(Functor Validated, Foldable Validated) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Validated a -> f (Validated b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Validated (f a) -> f (Validated a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Validated a -> m (Validated b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Validated (m a) -> m (Validated a))
-> Traversable Validated
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Validated (m a) -> m (Validated a)
forall (f :: * -> *) a.
Applicative f =>
Validated (f a) -> f (Validated a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Validated a -> m (Validated b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Validated a -> f (Validated b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Validated a -> f (Validated b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Validated a -> f (Validated b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Validated (f a) -> f (Validated a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Validated (f a) -> f (Validated a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Validated a -> m (Validated b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Validated a -> m (Validated b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Validated (m a) -> m (Validated a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Validated (m a) -> m (Validated a)
T.Traversable)

validatedToEither :: Validated a -> Either [String] a
validatedToEither :: forall a. Validated a -> Either [String] a
validatedToEither Validated a
v =
  case Validated a
v of
    Invalid [String]
rsns -> [String] -> Either [String] a
forall a b. a -> Either a b
Left [String]
rsns
    Validated a
a -> a -> Either [String] a
forall a b. b -> Either a b
Right a
a

instance Applicative Validated where
  pure :: forall a. a -> Validated a
pure = a -> Validated a
forall a. a -> Validated a
Validated
  Validated a -> b
f <*> :: forall a b. Validated (a -> b) -> Validated a -> Validated b
<*> Validated a
a = b -> Validated b
forall a. a -> Validated a
Validated (a -> b
f a
a)
  Validated a -> b
_f <*> Invalid [String]
rsns = [String] -> Validated b
forall a. [String] -> Validated a
Invalid [String]
rsns
  Invalid [String]
rsns1 <*> Invalid [String]
rsns2 = [String] -> Validated b
forall a. [String] -> Validated a
Invalid ([String]
rsns1 [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String]
rsns2)
  Invalid [String]
rsns <*> Validated a
_ = [String] -> Validated b
forall a. [String] -> Validated a
Invalid [String]
rsns

instance Alternative Validated where
  empty :: forall a. Validated a
empty = [String] -> Validated a
forall a. [String] -> Validated a
Invalid []
  Validated a
a <|> :: forall a. Validated a -> Validated a -> Validated a
<|> Validated a
_ = a -> Validated a
forall a. a -> Validated a
Validated a
a
  Invalid [String]
rsns1 <|> Invalid [String]
rsns2 = [String] -> Validated a
forall a. [String] -> Validated a
Invalid ([String]
rsns1 [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String]
rsns2)
  Invalid [String]
_ <|> Validated a
a = a -> Validated a
forall a. a -> Validated a
Validated a
a

invalid :: String -> Validated a
invalid :: forall a. String -> Validated a
invalid String
rsn = [String] -> Validated a
forall a. [String] -> Validated a
Invalid [String
rsn]

-- | Boolector and DReal only support offline solving (for our purposes), so
-- attempt to parse them from the given string
asOnlyOfflineSolver :: String -> Validated SolverOffline
asOnlyOfflineSolver :: String -> Validated SolverOffline
asOnlyOfflineSolver String
s =
  case String
s of
    String
"dreal" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOffline
DReal
    String
"boolector" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOffline
Boolector
    String
_ -> String -> Validated SolverOffline
forall a. String -> Validated a
invalid (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s is not an offline-only solver (expected dreal or boolector)" String
s)

-- | Solvers that can be used in offline mode
asAnyOfflineSolver :: String -> Validated SolverOffline
asAnyOfflineSolver :: String -> Validated SolverOffline
asAnyOfflineSolver String
s = case String
s of
      String
"dreal" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOffline
DReal
      String
"boolector" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOffline
Boolector
      String
"z3" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverOnline -> SolverOffline
SolverOnline SolverOnline
Z3)
      String
"yices" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverOnline -> SolverOffline
SolverOnline SolverOnline
Yices)
      String
"cvc4" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverOnline -> SolverOffline
SolverOnline SolverOnline
CVC4)
      String
"cvc5" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverOnline -> SolverOffline
SolverOnline SolverOnline
CVC5)
      String
"stp" -> SolverOffline -> Validated SolverOffline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverOnline -> SolverOffline
SolverOnline SolverOnline
STP)
      String
_ -> String -> Validated SolverOffline
forall a. String -> Validated a
invalid (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, or stp)" String
s)

asManyOfflineSolvers :: String -> Validated [SolverOffline]
asManyOfflineSolvers :: String -> Validated [SolverOffline]
asManyOfflineSolvers String
s
  | String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"all"         = String -> Validated [SolverOffline]
asManyOfflineSolvers String
"dreal,boolector,z3,yices,cvc4,cvc5,stp"
  | [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
solvers Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 = (String -> Validated SolverOffline)
-> [String] -> Validated [SolverOffline]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse String -> Validated SolverOffline
asAnyOfflineSolver [String]
solvers
  | Bool
otherwise          = String -> Validated [SolverOffline]
forall a. String -> Validated a
invalid (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s is not a valid solver list (expected 'all' or a comma separated list of solvers)" String
s)
  where
    solvers :: [String]
solvers = (Char -> Bool) -> String -> [String]
forall a. (a -> Bool) -> [a] -> [[a]]
wordsBy (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
',') String
s

-- | Attempt to parse the string as one of our solvers that supports online mode
asOnlineSolver :: String -> Validated SolverOnline
asOnlineSolver :: String -> Validated SolverOnline
asOnlineSolver String
s =
  case String
s of
    String
"yices" -> SolverOnline -> Validated SolverOnline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOnline
Yices
    String
"cvc4" -> SolverOnline -> Validated SolverOnline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOnline
CVC4
    String
"cvc5" -> SolverOnline -> Validated SolverOnline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOnline
CVC5
    String
"z3" -> SolverOnline -> Validated SolverOnline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOnline
Z3
    String
"stp" -> SolverOnline -> Validated SolverOnline
forall a. a -> Validated a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SolverOnline
STP
    String
_ -> String -> Validated SolverOnline
forall a. String -> Validated a
invalid (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s is not a valid online solver (expected yices, cvc4, cvc5, z3, or stp)" String
s)

-- | Examine a 'CCC.CruxOptions' and determine what solver configuration to use for
-- symbolic execution.  This can fail if an invalid solver configuration is
-- requested by the user.
--
-- The high level logic is that:
--
--  * If a user specifies only a single solver with the --solver option, that is
--    used as an online solver if possible for path sat checking (if requested)
--    and goal discharge.
--  * If the user specifies an explicit --path-sat-solver, that solver is used
--    for path satisfiability checking (if requested) while the solver specified
--    with --solver is used for goal discharge.
--  * The goal solver can be entirely offline (if it doesn't support online
--    mode) or if the user requests that it be used in offline mode with the
--    --force-offline-goal-solving option.
parseSolverConfig :: CCC.CruxOptions -> Either [String] SolverConfig
parseSolverConfig :: CruxOptions -> Either [String] SolverConfig
parseSolverConfig CruxOptions
cruxOpts = Validated SolverConfig -> Either [String] SolverConfig
forall a. Validated a -> Either [String] a
validatedToEither (Validated SolverConfig -> Either [String] SolverConfig)
-> Validated SolverConfig -> Either [String] SolverConfig
forall a b. (a -> b) -> a -> b
$
  case (CruxOptions -> Maybe String
CCC.pathSatSolver CruxOptions
cruxOpts, CruxOptions -> Bool
CCC.checkPathSat CruxOptions
cruxOpts, CruxOptions -> Bool
CCC.forceOfflineGoalSolving CruxOptions
cruxOpts) of
    (Maybe String
Nothing, Bool
True, Bool
False) ->
      -- No separate path sat checker was requested, but we do have to check
      -- path satisfiability.  That means that we have to use the one solver
      -- specified and it must be one that supports online solving
      Validated SolverConfig
trySingleOnline
    (Maybe String
Nothing, Bool
True, Bool
True) ->
      -- The user requested path satisfiability checking (using an online
      -- solver), but also wants to force goals to be discharged using the same
      -- solver in offline mode.
      SolverOnline -> SolverOffline -> SolverConfig
OnlineSolverWithOfflineGoals (SolverOnline -> SolverOffline -> SolverConfig)
-> Validated SolverOnline
-> Validated (SolverOffline -> SolverConfig)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Validated SolverOnline
asOnlineSolver (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts) Validated (SolverOffline -> SolverConfig)
-> Validated SolverOffline -> Validated SolverConfig
forall a b. Validated (a -> b) -> Validated a -> Validated b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Validated SolverOffline
asAnyOfflineSolver (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts)
    (Just String
_, Bool
False, Bool
False) ->
      -- The user specified a separate path sat checking solver, but did not
      -- request path satisfiability checking; we'll treat that as not asking
      -- for path satisfiability checking and just use a single online solver
      Validated SolverConfig
tryOnlyOffline Validated SolverConfig
-> Validated SolverConfig -> Validated SolverConfig
forall a. Validated a -> Validated a -> Validated a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Validated SolverConfig
trySingleOnline
    (Just String
_, Bool
False, Bool
True) ->
      -- The user requested a separate path sat checking solver, but did not
      -- request path satisfiability checking.  They also requested that a
      -- separate solver be used for each goal (offline mode).  We'll use the
      -- specified solver as the only solver purely in offline mode.
      Validated SolverConfig
tryAnyOffline Validated SolverConfig
-> Validated SolverConfig -> Validated SolverConfig
forall a. Validated a -> Validated a -> Validated a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Validated SolverConfig
tryManyOffline
    (Maybe String
Nothing, Bool
False, Bool
False) ->
      -- This is currently the same as the previous case, but the user
      -- explicitly selected no path sat checking
      Validated SolverConfig
tryOnlyOffline Validated SolverConfig
-> Validated SolverConfig -> Validated SolverConfig
forall a. Validated a -> Validated a -> Validated a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Validated SolverConfig
trySingleOnline
    (Maybe String
Nothing, Bool
False, Bool
True) ->
      -- This is the same as the `(Just _, False, True)` case since we were just
      -- ignoring the unused path sat solver option.
      Validated SolverConfig
tryAnyOffline Validated SolverConfig
-> Validated SolverConfig -> Validated SolverConfig
forall a. Validated a -> Validated a -> Validated a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Validated SolverConfig
tryManyOffline
    (Just String
onSolver, Bool
True, Bool
False) ->
      -- The user requested path sat checking and specified a solver
      --
      -- NOTE: We can still use the goal solver in online mode if it is supported

      -- In this case, the user requested a goal solver that is only usable as
      -- an offline solver
      (SolverOnline -> SolverOffline -> SolverConfig
OnlineSolverWithOfflineGoals (SolverOnline -> SolverOffline -> SolverConfig)
-> Validated SolverOnline
-> Validated (SolverOffline -> SolverConfig)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Validated SolverOnline
asOnlineSolver String
onSolver Validated (SolverOffline -> SolverConfig)
-> Validated SolverOffline -> Validated SolverConfig
forall a b. Validated (a -> b) -> Validated a -> Validated b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Validated SolverOffline
asOnlyOfflineSolver (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts)) Validated SolverConfig
-> Validated SolverConfig -> Validated SolverConfig
forall a. Validated a -> Validated a -> Validated a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
        -- In this case, the requested solver can be used in online mode so we
        -- use it as such
        (SolverOnline -> SolverOnline -> SolverConfig
onlineWithOnlineGoals (SolverOnline -> SolverOnline -> SolverConfig)
-> Validated SolverOnline
-> Validated (SolverOnline -> SolverConfig)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Validated SolverOnline
asOnlineSolver String
onSolver Validated (SolverOnline -> SolverConfig)
-> Validated SolverOnline -> Validated SolverConfig
forall a b. Validated (a -> b) -> Validated a -> Validated b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Validated SolverOnline
asOnlineSolver (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts))

    (Just String
onSolver, Bool
True, Bool
True) ->
      -- In this case, the user requested separate solvers for path sat checking
      -- and goal discharge, but further requested that we force goals to be
      -- discharged with an offline solver.
      SolverOnline -> SolverOffline -> SolverConfig
OnlineSolverWithOfflineGoals (SolverOnline -> SolverOffline -> SolverConfig)
-> Validated SolverOnline
-> Validated (SolverOffline -> SolverConfig)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Validated SolverOnline
asOnlineSolver String
onSolver Validated (SolverOffline -> SolverConfig)
-> Validated SolverOffline -> Validated SolverConfig
forall a b. Validated (a -> b) -> Validated a -> Validated b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Validated SolverOffline
asAnyOfflineSolver (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts)
  where
    tryAnyOffline :: Validated SolverConfig
tryAnyOffline = [SolverOffline] -> SolverConfig
OnlyOfflineSolvers ([SolverOffline] -> SolverConfig)
-> (SolverOffline -> [SolverOffline])
-> SolverOffline
-> SolverConfig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverOffline -> [SolverOffline]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverOffline -> SolverConfig)
-> Validated SolverOffline -> Validated SolverConfig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Validated SolverOffline
asAnyOfflineSolver (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts)
    tryOnlyOffline :: Validated SolverConfig
tryOnlyOffline = [SolverOffline] -> SolverConfig
OnlyOfflineSolvers ([SolverOffline] -> SolverConfig)
-> (SolverOffline -> [SolverOffline])
-> SolverOffline
-> SolverConfig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverOffline -> [SolverOffline]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverOffline -> SolverConfig)
-> Validated SolverOffline -> Validated SolverConfig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Validated SolverOffline
asOnlyOfflineSolver (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts)
    trySingleOnline :: Validated SolverConfig
trySingleOnline = SolverOnline -> SolverConfig
SingleOnlineSolver (SolverOnline -> SolverConfig)
-> Validated SolverOnline -> Validated SolverConfig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Validated SolverOnline
asOnlineSolver (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts)
    tryManyOffline :: Validated SolverConfig
tryManyOffline = [SolverOffline] -> SolverConfig
OnlyOfflineSolvers ([SolverOffline] -> SolverConfig)
-> Validated [SolverOffline] -> Validated SolverConfig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Validated [SolverOffline]
asManyOfflineSolvers (CruxOptions -> String
CCC.solver CruxOptions
cruxOpts)

    onlineWithOnlineGoals :: SolverOnline -> SolverOnline -> SolverConfig
onlineWithOnlineGoals SolverOnline
s1 SolverOnline
s2
      | SolverOnline
s1 SolverOnline -> SolverOnline -> Bool
forall a. Eq a => a -> a -> Bool
== SolverOnline
s2  = SolverOnline -> SolverConfig
SingleOnlineSolver SolverOnline
s1
      | Bool
otherwise = SolverOnline -> SolverOnline -> SolverConfig
OnlineSolverWithSeparateOnlineGoals SolverOnline
s1 SolverOnline
s2