{-# LANGUAGE TemplateHaskell #-}

module Language.Hasmtlib.Type.Solution where

import Language.Hasmtlib.Type.Expr
import Data.IntMap
import Control.Lens

-- | Function that turns a state into a result and a solution.
type Solver s m = s -> m (Result, Solution)

-- | Results of check-sat commands.
data Result = Unsat | Unknown | Sat deriving (Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Result -> ShowS
showsPrec :: Int -> Result -> ShowS
$cshow :: Result -> String
show :: Result -> String
$cshowList :: [Result] -> ShowS
showList :: [Result] -> ShowS
Show, Result -> Result -> Bool
(Result -> Result -> Bool)
-> (Result -> Result -> Bool) -> Eq Result
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
/= :: Result -> Result -> Bool
Eq, Eq Result
Eq Result =>
(Result -> Result -> Ordering)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Result)
-> (Result -> Result -> Result)
-> Ord Result
Result -> Result -> Bool
Result -> Result -> Ordering
Result -> Result -> Result
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 :: Result -> Result -> Ordering
compare :: Result -> Result -> Ordering
$c< :: Result -> Result -> Bool
< :: Result -> Result -> Bool
$c<= :: Result -> Result -> Bool
<= :: Result -> Result -> Bool
$c> :: Result -> Result -> Bool
> :: Result -> Result -> Bool
$c>= :: Result -> Result -> Bool
>= :: Result -> Result -> Bool
$cmax :: Result -> Result -> Result
max :: Result -> Result -> Result
$cmin :: Result -> Result -> Result
min :: Result -> Result -> Result
Ord)

-- | A Solution is a Map from the variable-identifier to some solution for it.
type Solution = IntMap (SomeKnownSMTSort SMTVarSol)

-- | A solution for a single variable.
data SMTVarSol (t :: SMTSort) = SMTVarSol 
  { forall (t :: SMTSort). SMTVarSol t -> SMTVar t
_solVar :: SMTVar t                       -- ^ A variable in the SMT-Problem
  , forall (t :: SMTSort). SMTVarSol t -> Value t
_solVal :: Value t                        -- ^ An assignment for this variable in a solution
  } deriving (Int -> SMTVarSol t -> ShowS
[SMTVarSol t] -> ShowS
SMTVarSol t -> String
(Int -> SMTVarSol t -> ShowS)
-> (SMTVarSol t -> String)
-> ([SMTVarSol t] -> ShowS)
-> Show (SMTVarSol t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: SMTSort). Int -> SMTVarSol t -> ShowS
forall (t :: SMTSort). [SMTVarSol t] -> ShowS
forall (t :: SMTSort). SMTVarSol t -> String
$cshowsPrec :: forall (t :: SMTSort). Int -> SMTVarSol t -> ShowS
showsPrec :: Int -> SMTVarSol t -> ShowS
$cshow :: forall (t :: SMTSort). SMTVarSol t -> String
show :: SMTVarSol t -> String
$cshowList :: forall (t :: SMTSort). [SMTVarSol t] -> ShowS
showList :: [SMTVarSol t] -> ShowS
Show, SMTVarSol t -> SMTVarSol t -> Bool
(SMTVarSol t -> SMTVarSol t -> Bool)
-> (SMTVarSol t -> SMTVarSol t -> Bool) -> Eq (SMTVarSol t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Bool
$c== :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Bool
== :: SMTVarSol t -> SMTVarSol t -> Bool
$c/= :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Bool
/= :: SMTVarSol t -> SMTVarSol t -> Bool
Eq, Eq (SMTVarSol t)
Eq (SMTVarSol t) =>
(SMTVarSol t -> SMTVarSol t -> Ordering)
-> (SMTVarSol t -> SMTVarSol t -> Bool)
-> (SMTVarSol t -> SMTVarSol t -> Bool)
-> (SMTVarSol t -> SMTVarSol t -> Bool)
-> (SMTVarSol t -> SMTVarSol t -> Bool)
-> (SMTVarSol t -> SMTVarSol t -> SMTVarSol t)
-> (SMTVarSol t -> SMTVarSol t -> SMTVarSol t)
-> Ord (SMTVarSol t)
SMTVarSol t -> SMTVarSol t -> Bool
SMTVarSol t -> SMTVarSol t -> Ordering
SMTVarSol t -> SMTVarSol t -> SMTVarSol t
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
forall (t :: SMTSort). Eq (SMTVarSol t)
forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Bool
forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Ordering
forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> SMTVarSol t
$ccompare :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Ordering
compare :: SMTVarSol t -> SMTVarSol t -> Ordering
$c< :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Bool
< :: SMTVarSol t -> SMTVarSol t -> Bool
$c<= :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Bool
<= :: SMTVarSol t -> SMTVarSol t -> Bool
$c> :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Bool
> :: SMTVarSol t -> SMTVarSol t -> Bool
$c>= :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> Bool
>= :: SMTVarSol t -> SMTVarSol t -> Bool
$cmax :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> SMTVarSol t
max :: SMTVarSol t -> SMTVarSol t -> SMTVarSol t
$cmin :: forall (t :: SMTSort). SMTVarSol t -> SMTVarSol t -> SMTVarSol t
min :: SMTVarSol t -> SMTVarSol t -> SMTVarSol t
Ord)
$(makeLenses ''SMTVarSol)