{-# LANGUAGE RecordWildCards #-}

module SoPSat.Satisfier (
  -- * State
  SolverState,

  -- * State manipulation
  declare,
  assert,
  unify,

  -- * State information
  range,
  ranges,

  -- * State execution
  withState,
  runStatements,
  evalStatements,

  -- * Expressions
  evalSoP,
)
where

import Control.Applicative ((<|>))
import Control.Arrow (second)
import Control.Monad (unless, when, (>=>))

import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe (isNothing)

import SoPSat.Internal.NewtonsMethod
import SoPSat.Internal.Range
import SoPSat.Internal.SoP (
  Atom (..),
  Product (..),
  SoP (..),
  Symbol (..),
 )
import SoPSat.Internal.SolverMonad
import SoPSat.Internal.Unify
import SoPSat.SoP

parts :: [a] -> [[a]]
parts :: forall a. [a] -> [[a]]
parts [] = []
parts (a
x : [a]
xs) = [a]
xs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [[a]]
forall a. [a] -> [[a]]
parts [a]
xs)

{- | Declares atom in the state
ignores constants and only declare function arguments
-}
declareAtom :: (Ord f, Ord c) => Atom f c -> SolverState f c Bool
declareAtom :: forall f c. (Ord f, Ord c) => Atom f c -> SolverState f c Bool
declareAtom (C c
_) = Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
declareAtom (F f
_ [SoP f c]
args) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> StateT (State f c) Maybe [Bool] -> StateT (State f c) Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SoP f c -> StateT (State f c) Maybe Bool)
-> [SoP f c] -> StateT (State f c) Maybe [Bool]
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 SoP f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => SoP f c -> SolverState f c Bool
declareSoP [SoP f c]
args

{- | Declares symbol in the state with the default interval
If symbol exists preserves the old interval
-}
declareSymbol :: (Ord f, Ord c) => Symbol f c -> SolverState f c Bool
declareSymbol :: forall f c. (Ord f, Ord c) => Symbol f c -> SolverState f c Bool
declareSymbol (I Integer
_) = Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
declareSymbol (A Atom f c
a) = do
  Map (Atom f c) (Range f c)
existing <- SolverState f c (Map (Atom f c) (Range f c))
forall f c.
(Ord f, Ord c) =>
SolverState f c (Map (Atom f c) (Range f c))
getRanges
  Bool -> StateT (State f c) Maybe () -> StateT (State f c) Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe (Range f c) -> Bool
forall a. Maybe a -> Bool
isNothing (Atom f c -> Map (Atom f c) (Range f c) -> Maybe (Range f c)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Atom f c
a Map (Atom f c) (Range f c)
existing)) (Atom f c -> Range f c -> StateT (State f c) Maybe ()
forall f c.
(Ord f, Ord c) =>
Atom f c -> Range f c -> SolverState f c ()
putRange Atom f c
a Range f c
forall {f} {c}. Range f c
rangeNatural)
  Atom f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => Atom f c -> SolverState f c Bool
declareAtom Atom f c
a
 where
  rangeNatural :: Range f c
rangeNatural = Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range (SoP f c -> Bound f c
forall f c. SoP f c -> Bound f c
Bound (Integer -> SoP f c
forall f c. Integer -> SoP f c
int Integer
0)) Bound f c
forall f c. Bound f c
Inf
declareSymbol (E SoP f c
b Product f c
p) = Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> StateT (State f c) Maybe Bool
-> StateT (State f c) Maybe (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SoP f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => SoP f c -> SolverState f c Bool
declareSoP SoP f c
b StateT (State f c) Maybe (Bool -> Bool)
-> StateT (State f c) Maybe Bool -> StateT (State f c) Maybe Bool
forall a b.
StateT (State f c) Maybe (a -> b)
-> StateT (State f c) Maybe a -> StateT (State f c) Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Product f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => Product f c -> SolverState f c Bool
declareProduct Product f c
p

-- | Similar to @declareSoP@ but for @Product@
declareProduct :: (Ord f, Ord c) => Product f c -> SolverState f c Bool
declareProduct :: forall f c. (Ord f, Ord c) => Product f c -> SolverState f c Bool
declareProduct = ([Bool] -> Bool)
-> StateT (State f c) Maybe [Bool] -> StateT (State f c) Maybe Bool
forall a b.
(a -> b)
-> StateT (State f c) Maybe a -> StateT (State f c) Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (StateT (State f c) Maybe [Bool] -> StateT (State f c) Maybe Bool)
-> (Product f c -> StateT (State f c) Maybe [Bool])
-> Product f c
-> StateT (State f c) Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol f c -> StateT (State f c) Maybe Bool)
-> [Symbol f c] -> StateT (State f c) Maybe [Bool]
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 Symbol f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => Symbol f c -> SolverState f c Bool
declareSymbol ([Symbol f c] -> StateT (State f c) Maybe [Bool])
-> (Product f c -> [Symbol f c])
-> Product f c
-> StateT (State f c) Maybe [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product f c -> [Symbol f c]
forall f c. Product f c -> [Symbol f c]
unP

{- | Declare SoP in the state with default values
Creates range for free-variables
-}
declareSoP :: (Ord f, Ord c) => SoP f c -> SolverState f c Bool
declareSoP :: forall f c. (Ord f, Ord c) => SoP f c -> SolverState f c Bool
declareSoP s :: SoP f c
s@(S [Product f c]
ps)
  | SoP f c
left SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer -> SoP f c
forall f c. Integer -> SoP f c
int Integer
0 =
      Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> StateT (State f c) Maybe Bool
-> StateT (State f c) Maybe (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> StateT (State f c) Maybe [Bool] -> StateT (State f c) Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Product f c -> StateT (State f c) Maybe Bool)
-> [Product f c] -> StateT (State f c) Maybe [Bool]
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 Product f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => Product f c -> SolverState f c Bool
declareProduct [Product f c]
ps) StateT (State f c) Maybe (Bool -> Bool)
-> StateT (State f c) Maybe Bool -> StateT (State f c) Maybe Bool
forall a b.
StateT (State f c) Maybe (a -> b)
-> StateT (State f c) Maybe a -> StateT (State f c) Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SoPE f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
assert (SoP f c -> SoP f c -> OrdRel -> SoPE f c
forall f c. SoP f c -> SoP f c -> OrdRel -> SoPE f c
SoPE SoP f c
left SoP f c
right OrdRel
LeR)
  | Bool
otherwise = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> StateT (State f c) Maybe [Bool] -> StateT (State f c) Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Product f c -> StateT (State f c) Maybe Bool)
-> [Product f c] -> StateT (State f c) Maybe [Bool]
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 Product f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => Product f c -> SolverState f c Bool
declareProduct [Product f c]
ps
 where
  (SoP f c
left, SoP f c
right) = SoP f c -> SoP f c -> (SoP f c, SoP f c)
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> (SoP f c, SoP f c)
splitSoP (Integer -> SoP f c
forall f c. Integer -> SoP f c
int Integer
0) SoP f c
s

{- | Declare expression to state, returns normalised expression

Common for @declare@, @assert@, and @unify@
-}
declareToState :: (Ord f, Ord c) => SoPE f c -> SolverState f c (SoPE f c)
declareToState :: forall f c.
(Ord f, Ord c) =>
SoPE f c -> SolverState f c (SoPE f c)
declareToState SoPE{SoP f c
OrdRel
lhs :: SoP f c
rhs :: SoP f c
op :: OrdRel
op :: forall f c. SoPE f c -> OrdRel
rhs :: forall f c. SoPE f c -> SoP f c
lhs :: forall f c. SoPE f c -> SoP f c
..} = do
  Bool
r1 <- SoP f c -> SolverState f c Bool
forall f c. (Ord f, Ord c) => SoP f c -> SolverState f c Bool
declareSoP SoP f c
lhs
  Bool
r2 <- SoP f c -> SolverState f c Bool
forall f c. (Ord f, Ord c) => SoP f c -> SolverState f c Bool
declareSoP SoP f c
rhs
  [Unifier f c]
us <- SolverState f c [Unifier f c]
forall f c. (Ord f, Ord c) => SolverState f c [Unifier f c]
getUnifiers
  let
    lhs' :: SoP f c
lhs' = [Unifier f c] -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => [Unifier f c] -> SoP f c -> SoP f c
substsSoP [Unifier f c]
us SoP f c
lhs
    rhs' :: SoP f c
rhs' = [Unifier f c] -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => [Unifier f c] -> SoP f c -> SoP f c
substsSoP [Unifier f c]
us SoP f c
rhs
  Bool -> StateT (State f c) Maybe () -> StateT (State f c) Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
r1 Bool -> Bool -> Bool
&& Bool
r2) (String -> StateT (State f c) Maybe ()
forall a. String -> StateT (State f c) Maybe a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"")
  SoPE f c -> SolverState f c (SoPE f c)
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SoP f c -> SoP f c -> OrdRel -> SoPE f c
forall f c. SoP f c -> SoP f c -> OrdRel -> SoPE f c
SoPE SoP f c
lhs' SoP f c
rhs' OrdRel
op)

{- | Declare equality of two expressions
Adds new unifiers to the state
-}
declareEq ::
  (Ord f, Ord c) =>
  -- | First expression
  SoP f c ->
  -- | Second expression
  SoP f c ->
  -- | Similar to @declare@ but handles only equalities
  SolverState f c Bool
declareEq :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
declareEq SoP f c
u SoP f c
v =
  do
    (Range Bound f c
low1 Bound f c
up1) <- SoP f c -> SolverState f c (Range f c)
forall f c.
(Ord f, Ord c) =>
SoP f c -> SolverState f c (Range f c)
getRangeSoP SoP f c
u
    (Range Bound f c
low2 Bound f c
up2) <- SoP f c -> SolverState f c (Range f c)
forall f c.
(Ord f, Ord c) =>
SoP f c -> SolverState f c (Range f c)
getRangeSoP SoP f c
v
    Bool
lowRes <- Bound f c -> Bound f c -> SolverState f c Bool
forall {f} {c}.
(Ord f, Ord c) =>
Bound f c -> Bound f c -> StateT (State f c) Maybe Bool
boundComp Bound f c
low1 Bound f c
low2
    Bool
upRes <- Bound f c -> Bound f c -> SolverState f c Bool
forall {f} {c}.
(Ord f, Ord c) =>
Bound f c -> Bound f c -> StateT (State f c) Maybe Bool
boundComp Bound f c
up1 Bound f c
up2

    -- Declaration and assertions of expression is done on the whole domain
    -- if two expressions are equal, their domains will intersect
    --
    -- g(x) in [1,5] and forall x  g(x) = f(x) then f(x) in [1,5]
    Bool
lowerUpdate <-
      case (Bool
lowRes, Bound f c
low1, Bound f c
low2) of
        (Bool
True, Bound f c
_, Bound SoP f c
lowB2) -> SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
u OrdRel
GeR SoP f c
lowB2
        (Bool
False, Bound SoP f c
lowB1, Bound f c
_) -> SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
v OrdRel
GeR SoP f c
lowB1
        (Bool
_, Bound f c
_, Bound f c
_) -> Bool -> SolverState f c Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    Bool
upperUpdate <-
      case (Bool
upRes, Bound f c
up1, Bound f c
up2) of
        (Bool
True, Bound f c
_, Bound SoP f c
upB2) -> SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
u OrdRel
LeR SoP f c
upB2
        (Bool
False, Bound SoP f c
upB1, Bound f c
_) -> SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
v OrdRel
LeR SoP f c
upB1
        (Bool
_, Bound f c
_, Bound f c
_) -> Bool -> SolverState f c Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    SoP f c -> SoP f c -> SolverState f c ()
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c ()
declareEq' SoP f c
u SoP f c
v
    Bool -> SolverState f c Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
lowerUpdate Bool -> Bool -> Bool
&& Bool
upperUpdate)
 where
  boundComp :: Bound f c -> Bound f c -> StateT (State f c) Maybe Bool
boundComp Bound f c
Inf Bound f c
_ = Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  boundComp Bound f c
_ Bound f c
Inf = Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  boundComp (Bound SoP f c
a) (Bound SoP f c
b) = SoPE f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
assert (SoP f c -> SoP f c -> OrdRel -> SoPE f c
forall f c. SoP f c -> SoP f c -> OrdRel -> SoPE f c
SoPE SoP f c
a SoP f c
b OrdRel
LeR)

declareEq' :: (Ord f, Ord c) => SoP f c -> SoP f c -> SolverState f c ()
declareEq' :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c ()
declareEq' (S [P [A Atom f c
a]]) SoP f c
v = [Unifier f c] -> SolverState f c ()
forall f c. (Ord f, Ord c) => [Unifier f c] -> SolverState f c ()
putUnifiers [Atom f c -> SoP f c -> Unifier f c
forall f c. Atom f c -> SoP f c -> Unifier f c
Subst Atom f c
a SoP f c
v]
declareEq' SoP f c
u (S [P [A Atom f c
a]]) = [Unifier f c] -> SolverState f c ()
forall f c. (Ord f, Ord c) => [Unifier f c] -> SolverState f c ()
putUnifiers [Atom f c -> SoP f c -> Unifier f c
forall f c. Atom f c -> SoP f c -> Unifier f c
Subst Atom f c
a SoP f c
u]
declareEq' SoP f c
u SoP f c
v = [Unifier f c] -> SolverState f c ()
forall f c. (Ord f, Ord c) => [Unifier f c] -> SolverState f c ()
putUnifiers ([Unifier f c] -> SolverState f c ())
-> [Unifier f c] -> SolverState f c ()
forall a b. (a -> b) -> a -> b
$ SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers SoP f c
u SoP f c
v

-- | Updates interval information for a symbol
propagateInEqSymbol ::
  (Ord f, Ord c) =>
  -- | Updated symbol
  Symbol f c ->
  -- | Relationship between the symbol and target
  OrdRel ->
  -- | Target Boundary
  SoP f c ->
  -- | Similat to @declareInEq@
  SolverState f c Bool
propagateInEqSymbol :: forall f c.
(Ord f, Ord c) =>
Symbol f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSymbol (I Integer
_) OrdRel
_ SoP f c
_ =
  Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- No need to update numbers
propagateInEqSymbol (A Atom f c
a) OrdRel
rel SoP f c
bound = do
  (Range Bound f c
low Bound f c
up) <- Atom f c -> SolverState f c (Range f c)
forall f c.
(Ord f, Ord c) =>
Atom f c -> SolverState f c (Range f c)
getRange Atom f c
a
  -- New bound is less/greater than the old one
  -- The check is done before propagation
  -- This assumption is potentially wrong
  case OrdRel
rel of
    OrdRel
LeR ->
      Atom f c -> Range f c -> StateT (State f c) Maybe ()
forall f c.
(Ord f, Ord c) =>
Atom f c -> Range f c -> SolverState f c ()
putRange Atom f c
a (Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range Bound f c
low Bound f c
rangeBound)
    OrdRel
GeR ->
      Atom f c -> Range f c -> StateT (State f c) Maybe ()
forall f c.
(Ord f, Ord c) =>
Atom f c -> Range f c -> SolverState f c ()
putRange Atom f c
a (Bound f c -> Bound f c -> Range f c
forall f c. Bound f c -> Bound f c -> Range f c
Range Bound f c
rangeBound Bound f c
up)
    OrdRel
EqR -> String -> StateT (State f c) Maybe ()
forall a. HasCallStack => String -> a
error String
"propagateInEqSymbol:EqR: unreachable"
  Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
 where
  rangeBound :: Bound f c
rangeBound = SoP f c -> Bound f c
forall f c. SoP f c -> Bound f c
Bound SoP f c
bound
propagateInEqSymbol (E SoP f c
b (P [I Integer
i])) OrdRel
rel (S [P [I Integer
j]])
  | (Just Integer
p) <- Integer -> Integer -> Maybe Integer
integerRt Integer
i Integer
j =
      SoP f c -> OrdRel -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
b OrdRel
rel (Integer -> SoP f c
forall f c. Integer -> SoP f c
int Integer
p)
propagateInEqSymbol (E (S [P [I Integer
i]]) Product f c
p) OrdRel
rel (S [P [I Integer
j]])
  | (Just Integer
e) <- Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j =
      Product f c -> OrdRel -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
Product f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqProduct Product f c
p OrdRel
rel (Integer -> SoP f c
forall f c. Integer -> SoP f c
int Integer
e)
propagateInEqSymbol Symbol f c
_ OrdRel
_ SoP f c
_ = String -> StateT (State f c) Maybe Bool
forall a. String -> StateT (State f c) Maybe a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
""

-- | Propagates interval information down the Product
propagateInEqProduct ::
  (Ord f, Ord c) =>
  -- | Updates expression
  Product f c ->
  -- | Relationship between the expression and target
  OrdRel ->
  -- | Target boundary
  SoP f c ->
  -- | Similar to @declareInEq@
  SolverState f c Bool
propagateInEqProduct :: forall f c.
(Ord f, Ord c) =>
Product f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqProduct (P [Symbol f c
symb]) OrdRel
rel SoP f c
target_bound = Symbol f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
Symbol f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSymbol Symbol f c
symb OrdRel
rel SoP f c
target_bound
propagateInEqProduct (P [Symbol f c]
ss) OrdRel
rel SoP f c
target_bound =
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> StateT (State f c) Maybe [Bool] -> SolverState f c Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol f c, Product f c) -> SolverState f c Bool)
-> [(Symbol f c, Product f c)] -> StateT (State f c) Maybe [Bool]
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 ((Symbol f c -> Product f c -> SolverState f c Bool)
-> (Symbol f c, Product f c) -> SolverState f c Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol f c -> Product f c -> SolverState f c Bool
forall {p}. Symbol f c -> p -> SolverState f c Bool
propagate) ((Symbol f c -> [Symbol f c] -> (Symbol f c, Product f c))
-> [Symbol f c] -> [[Symbol f c]] -> [(Symbol f c, Product f c)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (((Symbol f c, [Symbol f c]) -> (Symbol f c, Product f c))
-> Symbol f c -> [Symbol f c] -> (Symbol f c, Product f c)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (([Symbol f c] -> Product f c)
-> (Symbol f c, [Symbol f c]) -> (Symbol f c, Product f c)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P)) [Symbol f c]
ss ([Symbol f c] -> [[Symbol f c]]
forall a. [a] -> [[a]]
parts [Symbol f c]
ss))
 where
  -- a <= x * y => a/y <= x and a/x <= y
  -- Currently simply propagating the bound further
  -- a <= x * y => a <= x and a <= y
  propagate :: Symbol f c -> p -> SolverState f c Bool
propagate Symbol f c
symb p
_prod =
    Symbol f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
Symbol f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSymbol
      Symbol f c
symb
      OrdRel
rel
      SoP f c
target_bound

-- (target_bound |/| prod)

-- | Propagates interval information down the SoP
propagateInEqSoP ::
  (Ord f, Ord c) =>
  -- | Updated expression
  SoP f c ->
  -- | Relationship between the expression and target
  OrdRel ->
  -- | Target boundary
  SoP f c ->
  -- | Similar to @declareInEq@
  SolverState f c Bool
propagateInEqSoP :: forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP (S [P [Symbol f c
symb]]) OrdRel
rel SoP f c
target_bound = Symbol f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
Symbol f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSymbol Symbol f c
symb OrdRel
rel SoP f c
target_bound
propagateInEqSoP (S [Product f c]
ps) OrdRel
rel SoP f c
target_bound =
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> StateT (State f c) Maybe [Bool] -> SolverState f c Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Product f c, SoP f c) -> SolverState f c Bool)
-> [(Product f c, SoP f c)] -> StateT (State f c) Maybe [Bool]
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 ((Product f c -> SoP f c -> SolverState f c Bool)
-> (Product f c, SoP f c) -> SolverState f c Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Product f c -> SoP f c -> SolverState f c Bool
propagate) ((Product f c -> [Product f c] -> (Product f c, SoP f c))
-> [Product f c] -> [[Product f c]] -> [(Product f c, SoP f c)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (((Product f c, [Product f c]) -> (Product f c, SoP f c))
-> Product f c -> [Product f c] -> (Product f c, SoP f c)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (([Product f c] -> SoP f c)
-> (Product f c, [Product f c]) -> (Product f c, SoP f c)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S)) [Product f c]
ps ([Product f c] -> [[Product f c]]
forall a. [a] -> [[a]]
parts [Product f c]
ps))
 where
  -- a <= x + y => a - y <= x and a - x <= y
  propagate :: Product f c -> SoP f c -> SolverState f c Bool
propagate Product f c
prod SoP f c
sm =
    Product f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
Product f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqProduct
      Product f c
prod
      OrdRel
rel
      (SoP f c
target_bound SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
|-| SoP f c
sm)

{- | Declare inequality of two expressions
Updates interval information in the state
-}
declareInEq ::
  (Ord f, Ord c) =>
  -- | Relationship between expressions
  OrdRel ->
  -- | Left-hand side expression
  SoP f c ->
  -- | Right-hand side expression
  SoP f c ->
  -- | Similar to @declare@ but handles only inequalities
  SolverState f c Bool
declareInEq :: forall f c.
(Ord f, Ord c) =>
OrdRel -> SoP f c -> SoP f c -> SolverState f c Bool
declareInEq OrdRel
EqR SoP f c
u SoP f c
v = SoP f c -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
declareEq SoP f c
u SoP f c
v SolverState f c Bool
-> SolverState f c Bool -> SolverState f c Bool
forall a b.
StateT (State f c) Maybe a
-> StateT (State f c) Maybe b -> StateT (State f c) Maybe b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> SolverState f c Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
declareInEq OrdRel
op SoP f c
u SoP f c
v =
  let
    (SoP f c
u', SoP f c
v') = SoP f c -> SoP f c -> (SoP f c, SoP f c)
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> (SoP f c, SoP f c)
splitSoP SoP f c
u SoP f c
v
   in
    -- If inequality holds with current interval information
    -- then no need to update it
    do
      Bool
res <- SoPE f c -> SolverState f c Bool
forall f c. (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
assert (SoP f c -> SoP f c -> OrdRel -> SoPE f c
forall f c. SoP f c -> SoP f c -> OrdRel -> SoPE f c
SoPE SoP f c
u' SoP f c
v' OrdRel
op)
      if Bool
res
        then Bool -> SolverState f c Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else case OrdRel
op of
          OrdRel
LeR -> do
            Bool
a1 <- SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
u' OrdRel
LeR SoP f c
v'
            Bool
a2 <- SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
v' OrdRel
GeR SoP f c
u'
            Bool -> SolverState f c Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
a1 Bool -> Bool -> Bool
&& Bool
a2)
          OrdRel
GeR -> do
            Bool
a1 <- SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
u' OrdRel
GeR SoP f c
v'
            Bool
a2 <- SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> OrdRel -> SoP f c -> SolverState f c Bool
propagateInEqSoP SoP f c
v' OrdRel
LeR SoP f c
u'
            Bool -> SolverState f c Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
a1 Bool -> Bool -> Bool
&& Bool
a2)

-- | Declare expression to the state
declare ::
  (Ord f, Ord c) =>
  -- | Expression to declare
  SoPE f c ->
  -- | - True - if expression was declared
  --   - False - if expression contradicts current state
  --
  -- State will become @Nothing@ if it cannot reason about these kind of expressions
  SolverState f c Bool
declare :: forall f c. (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
declare =
  SoPE f c -> SolverState f c (SoPE f c)
forall f c.
(Ord f, Ord c) =>
SoPE f c -> SolverState f c (SoPE f c)
declareToState (SoPE f c -> SolverState f c (SoPE f c))
-> (SoPE f c -> StateT (State f c) Maybe Bool)
-> SoPE f c
-> StateT (State f c) Maybe Bool
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \SoPE{SoP f c
OrdRel
op :: forall f c. SoPE f c -> OrdRel
rhs :: forall f c. SoPE f c -> SoP f c
lhs :: forall f c. SoPE f c -> SoP f c
lhs :: SoP f c
rhs :: SoP f c
op :: OrdRel
..} ->
    case OrdRel
op of
      OrdRel
EqR -> SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
declareEq SoP f c
lhs SoP f c
rhs
      OrdRel
_ -> OrdRel -> SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
OrdRel -> SoP f c -> SoP f c -> SolverState f c Bool
declareInEq OrdRel
op SoP f c
lhs SoP f c
rhs

-- | Assert that two expressions are equal using unifiers from the state
assertEq ::
  (Ord f, Ord c) =>
  -- | Left-hand side expression
  SoP f c ->
  -- | Right-hand size expression
  SoP f c ->
  -- | Similar to assert but only checks for equality @lhs = rhs@
  SolverState f c Bool
assertEq :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertEq SoP f c
lhs SoP f c
rhs = Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SoP f c
lhs SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
rhs)

-- | Assert using only ranges stores in the state
assertRange ::
  (Ord f, Ord c) =>
  -- | Left-hand side expression
  SoP f c ->
  -- | Right-hand size expression
  SoP f c ->
  -- | Similar to @assert@ but uses only intervals from the state to check @lhs <= rhs@
  SolverState f c Bool
assertRange :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertRange SoP f c
lhs SoP f c
rhs = (SoP f c -> SoP f c -> SolverState f c Bool)
-> (SoP f c, SoP f c) -> SolverState f c Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SoP f c -> SoP f c -> SolverState f c Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertRange' ((SoP f c, SoP f c) -> SolverState f c Bool)
-> (SoP f c, SoP f c) -> SolverState f c Bool
forall a b. (a -> b) -> a -> b
$ SoP f c -> SoP f c -> (SoP f c, SoP f c)
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> (SoP f c, SoP f c)
splitSoP SoP f c
lhs SoP f c
rhs

assertRange' :: (Ord f, Ord c) => SoP f c -> SoP f c -> SolverState f c Bool
assertRange' :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertRange' (S [P [I Integer
i]]) (S [P [I Integer
j]]) = Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
j)
assertRange' SoP f c
lhs SoP f c
rhs = do
  (Range Bound f c
_ Bound f c
up1) <- SoP f c -> SolverState f c (Range f c)
forall f c.
(Ord f, Ord c) =>
SoP f c -> SolverState f c (Range f c)
getRangeSoP SoP f c
lhs
  (Range Bound f c
low2 Bound f c
up2) <- SoP f c -> SolverState f c (Range f c)
forall f c.
(Ord f, Ord c) =>
SoP f c -> SolverState f c (Range f c)
getRangeSoP SoP f c
rhs
  -- If both sides increase infinitely, fail to use Newton's method
  -- Information about rate of growth is required
  -- to check inequality on the whole domain
  if Bound f c
up1 Bound f c -> Bound f c -> Bool
forall a. Eq a => a -> a -> Bool
== Bound f c
up2 Bool -> Bool -> Bool
&& Bound f c
up2 Bound f c -> Bound f c -> Bool
forall a. Eq a => a -> a -> Bool
== Bound f c
forall f c. Bound f c
Inf
    then String -> StateT (State f c) Maybe Bool
forall a. String -> StateT (State f c) Maybe a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
""
    else case (Bound f c
up1, Bound f c
low2) of
      (Bound f c
Inf, Bound f c
_) -> Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      (Bound f c
_, Bound f c
Inf) -> Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      (Bound SoP f c
ub1, Bound SoP f c
lb2) ->
        -- Orders of recursive checks matters
        -- @runLemma2@ in the tests loops indefinitely
        -- possibly other test cases too
        do
          Bool
r1 <-
            if SoP f c
ub1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
/= SoP f c
lhs
              then SoPE f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
assert (SoP f c -> SoP f c -> OrdRel -> SoPE f c
forall f c. SoP f c -> SoP f c -> OrdRel -> SoPE f c
SoPE SoP f c
ub1 SoP f c
rhs OrdRel
LeR)
              else Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          Bool
r2 <-
            if SoP f c
lb2 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
/= SoP f c
rhs
              then SoPE f c -> StateT (State f c) Maybe Bool
forall f c. (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
assert (SoP f c -> SoP f c -> OrdRel -> SoPE f c
forall f c. SoP f c -> SoP f c -> OrdRel -> SoPE f c
SoPE SoP f c
lhs SoP f c
lb2 OrdRel
LeR)
              else Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
          Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
r1 Bool -> Bool -> Bool
|| Bool
r2)

-- | Assert using only Newton's method
assertNewton ::
  (Ord f, Ord c) =>
  -- | Left-hand side expression
  SoP f c ->
  -- | Right-hand side expression
  SoP f c ->
  -- | Similar to @assert@ but uses only Newton's method to check @lhs <= rhs@
  SolverState f c Bool
assertNewton :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertNewton SoP f c
lhs SoP f c
rhs =
  let
    expr :: SoP f c
expr = SoP f c
rhs SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
|-| SoP f c
lhs SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
|+| Integer -> SoP f c
forall f c. Integer -> SoP f c
int Integer
1
   in
    SoP f c -> SolverState f c Bool
forall f c. (Ord f, Ord c) => SoP f c -> SolverState f c Bool
checkExpr SoP f c
expr
 where
  -- hasFunction :: (Ord f, Ord c) => SoP f c -> Bool
  -- hasFunction = any isFunction . atoms

  checkExpr :: (Ord f, Ord c) => SoP f c -> SolverState f c Bool
  checkExpr :: forall f c. (Ord f, Ord c) => SoP f c -> SolverState f c Bool
checkExpr SoP f c
expr
    | (Right Map (Atom f c) Double
binds) <- SoP f c -> Either (Map (Atom f c) Double) (Map (Atom f c) Double)
forall f c n.
(Ord f, Ord c, Ord n, Floating n) =>
SoP f c -> Either (Map (Atom f c) n) (Map (Atom f c) n)
newtonMethod SoP f c
expr =
        Bool -> Bool
not (Bool -> Bool)
-> StateT (State f c) Maybe Bool -> StateT (State f c) Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Atom f c) Double -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
Map (Atom f c) Double -> SolverState f c Bool
checkBinds Map (Atom f c) Double
binds
    | Bool
otherwise =
        Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

  checkBinds :: (Ord f, Ord c) => Map (Atom f c) Double -> SolverState f c Bool
  checkBinds :: forall f c.
(Ord f, Ord c) =>
Map (Atom f c) Double -> SolverState f c Bool
checkBinds Map (Atom f c) Double
binds = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> StateT (State f c) Maybe [Bool] -> StateT (State f c) Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Atom f c, Double) -> StateT (State f c) Maybe Bool)
-> [(Atom f c, Double)] -> StateT (State f c) Maybe [Bool]
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 ((Atom f c -> Double -> StateT (State f c) Maybe Bool)
-> (Atom f c, Double) -> StateT (State f c) Maybe Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Map (Atom f c) Double
-> Atom f c -> Double -> StateT (State f c) Maybe Bool
forall f c n.
(Ord f, Ord c, Ord n, Floating n) =>
Map (Atom f c) n -> Atom f c -> n -> SolverState f c Bool
checkBind Map (Atom f c) Double
binds)) (Map (Atom f c) Double -> [(Atom f c, Double)]
forall k a. Map k a -> [(k, a)]
M.toList Map (Atom f c) Double
binds)

  checkBind ::
    (Ord f, Ord c, Ord n, Floating n) =>
    Map (Atom f c) n -> Atom f c -> n -> SolverState f c Bool
  checkBind :: forall f c n.
(Ord f, Ord c, Ord n, Floating n) =>
Map (Atom f c) n -> Atom f c -> n -> SolverState f c Bool
checkBind Map (Atom f c) n
binds Atom f c
c n
v = do
    (Range Bound f c
left Bound f c
right) <- Atom f c -> SolverState f c (Range f c)
forall f c.
(Ord f, Ord c) =>
Atom f c -> SolverState f c (Range f c)
getRange Atom f c
c
    Bool -> SolverState f c Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map (Atom f c) n -> n -> Bound f c -> Bool
forall f c n.
(Ord f, Ord c, Ord n, Floating n) =>
Map (Atom f c) n -> n -> Bound f c -> Bool
checkLeft Map (Atom f c) n
binds n
v Bound f c
left Bool -> Bool -> Bool
&& Map (Atom f c) n -> n -> Bound f c -> Bool
forall f c n.
(Ord f, Ord c, Ord n, Floating n) =>
Map (Atom f c) n -> n -> Bound f c -> Bool
checkRight Map (Atom f c) n
binds n
v Bound f c
right)

  checkLeft ::
    (Ord f, Ord c, Ord n, Floating n) => Map (Atom f c) n -> n -> Bound f c -> Bool
  checkLeft :: forall f c n.
(Ord f, Ord c, Ord n, Floating n) =>
Map (Atom f c) n -> n -> Bound f c -> Bool
checkLeft Map (Atom f c) n
_ n
_ Bound f c
Inf = Bool
True
  checkLeft Map (Atom f c) n
binds n
v (Bound SoP f c
sop) = SoP f c -> Map (Atom f c) n -> n
forall f c n.
(Ord f, Ord c, Floating n) =>
SoP f c -> Map (Atom f c) n -> n
evalSoP SoP f c
sop Map (Atom f c) n
binds n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= n
v

  checkRight ::
    (Ord f, Ord c, Ord n, Floating n) => Map (Atom f c) n -> n -> Bound f c -> Bool
  checkRight :: forall f c n.
(Ord f, Ord c, Ord n, Floating n) =>
Map (Atom f c) n -> n -> Bound f c -> Bool
checkRight Map (Atom f c) n
_ n
_ Bound f c
Inf = Bool
True
  checkRight Map (Atom f c) n
binds n
v (Bound SoP f c
sop) = n
v n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= SoP f c -> Map (Atom f c) n -> n
forall f c n.
(Ord f, Ord c, Floating n) =>
SoP f c -> Map (Atom f c) n -> n
evalSoP SoP f c
sop Map (Atom f c) n
binds

-- | Assert if given expression holds in the current environment
assert ::
  (Ord f, Ord c) =>
  -- | Asserted expression
  SoPE f c ->
  -- | - True - if expressions holds
  --   - False - otherwise
  --
  -- State will become @Nothing@ if it cannot reason about these kind of expressions
  SolverState f c Bool
assert :: forall f c. (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
assert =
  SoPE f c -> SolverState f c (SoPE f c)
forall f c.
(Ord f, Ord c) =>
SoPE f c -> SolverState f c (SoPE f c)
declareToState (SoPE f c -> SolverState f c (SoPE f c))
-> (SoPE f c -> StateT (State f c) Maybe Bool)
-> SoPE f c
-> StateT (State f c) Maybe Bool
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \SoPE{SoP f c
OrdRel
op :: forall f c. SoPE f c -> OrdRel
rhs :: forall f c. SoPE f c -> SoP f c
lhs :: forall f c. SoPE f c -> SoP f c
lhs :: SoP f c
rhs :: SoP f c
op :: OrdRel
..} ->
    case OrdRel
op of
      OrdRel
EqR -> SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertEq SoP f c
lhs SoP f c
rhs
      OrdRel
LeR -> do
        Bool
r1 <- SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertEq SoP f c
lhs SoP f c
rhs
        if Bool
r1
          then Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          else do
            SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertRange SoP f c
lhs SoP f c
rhs StateT (State f c) Maybe Bool
-> StateT (State f c) Maybe Bool -> StateT (State f c) Maybe Bool
forall a.
StateT (State f c) Maybe a
-> StateT (State f c) Maybe a -> StateT (State f c) Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertNewton SoP f c
lhs SoP f c
rhs
      OrdRel
GeR -> do
        Bool
r1 <- SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertEq SoP f c
lhs SoP f c
rhs
        if Bool
r1
          then Bool -> StateT (State f c) Maybe Bool
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
          else do
            SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertRange SoP f c
rhs SoP f c
lhs StateT (State f c) Maybe Bool
-> StateT (State f c) Maybe Bool -> StateT (State f c) Maybe Bool
forall a.
StateT (State f c) Maybe a
-> StateT (State f c) Maybe a -> StateT (State f c) Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SoP f c -> SoP f c -> StateT (State f c) Maybe Bool
forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> SolverState f c Bool
assertNewton SoP f c
rhs SoP f c
lhs

{- | Get unifiers for an expression
minimal set of expressions that should hold for the expression to hold
-}
unify ::
  (Ord f, Ord c) =>
  -- | Unified expression
  SoPE f c ->
  -- | List of unifiers - Minimal list of unifiers for the expression to hold.
  -- The list is empty, if it never holds
  --
  -- State will always be valid after a call
  SolverState f c [SoPE f c]
unify :: forall f c.
(Ord f, Ord c) =>
SoPE f c -> SolverState f c [SoPE f c]
unify =
  SoPE f c -> SolverState f c (SoPE f c)
forall f c.
(Ord f, Ord c) =>
SoPE f c -> SolverState f c (SoPE f c)
declareToState (SoPE f c -> SolverState f c (SoPE f c))
-> (SoPE f c -> StateT (State f c) Maybe [SoPE f c])
-> SoPE f c
-> StateT (State f c) Maybe [SoPE f c]
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \expr :: SoPE f c
expr@SoPE{SoP f c
OrdRel
op :: forall f c. SoPE f c -> OrdRel
rhs :: forall f c. SoPE f c -> SoP f c
lhs :: forall f c. SoPE f c -> SoP f c
lhs :: SoP f c
rhs :: SoP f c
op :: OrdRel
..} ->
    case OrdRel
op of
      OrdRel
EqR -> [SoPE f c] -> StateT (State f c) Maybe [SoPE f c]
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((SoPE f c -> Bool) -> [SoPE f c] -> [SoPE f c]
forall a. (a -> Bool) -> [a] -> [a]
filter (SoPE f c -> SoPE f c -> Bool
forall a. Eq a => a -> a -> Bool
/= SoPE f c
expr) ([SoPE f c] -> [SoPE f c]) -> [SoPE f c] -> [SoPE f c]
forall a b. (a -> b) -> a -> b
$ (Unifier f c -> SoPE f c) -> [Unifier f c] -> [SoPE f c]
forall a b. (a -> b) -> [a] -> [b]
map Unifier f c -> SoPE f c
forall {f} {c}. Unifier f c -> SoPE f c
unifier2SoPE (SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers SoP f c
lhs SoP f c
rhs))
      OrdRel
_ -> [SoPE f c] -> StateT (State f c) Maybe [SoPE f c]
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
 where
  unifier2SoPE :: Unifier f c -> SoPE f c
unifier2SoPE Subst{SoP f c
Atom f c
sConst :: Atom f c
sSoP :: SoP f c
sSoP :: forall f c. Unifier f c -> SoP f c
sConst :: forall f c. Unifier f c -> Atom f c
..} = SoP f c -> SoP f c -> OrdRel -> SoPE f c
forall f c. SoP f c -> SoP f c -> OrdRel -> SoPE f c
SoPE (Atom f c -> SoP f c
forall f c. Atom f c -> SoP f c
symbol Atom f c
sConst) SoP f c
sSoP OrdRel
EqR

-- | Get range of possible values for an expression
range ::
  (Ord f, Ord c) =>
  -- | Expression
  SoP f c ->
  -- | (lower bound, upper bound) - Range for an expression
  --
  -- @Nothing@ means that the expression is unbounded
  -- from that side
  SolverState f c (Maybe (SoP f c), Maybe (SoP f c))
range :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SolverState f c (Maybe (SoP f c), Maybe (SoP f c))
range SoP f c
sop = do
  Bool
_ <- SoP f c -> SolverState f c Bool
forall f c. (Ord f, Ord c) => SoP f c -> SolverState f c Bool
declareSoP SoP f c
sop
  (Range Bound f c
low Bound f c
up) <- SoP f c -> SolverState f c (Range f c)
forall f c.
(Ord f, Ord c) =>
SoP f c -> SolverState f c (Range f c)
getRangeSoP SoP f c
sop
  (Maybe (SoP f c), Maybe (SoP f c))
-> SolverState f c (Maybe (SoP f c), Maybe (SoP f c))
forall a. a -> StateT (State f c) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bound f c -> Maybe (SoP f c)
forall f c. Bound f c -> Maybe (SoP f c)
boundSoP Bound f c
low, Bound f c -> Maybe (SoP f c)
forall f c. Bound f c -> Maybe (SoP f c)
boundSoP Bound f c
up)

-- | Get list of all ranges stored in a state
ranges ::
  (Ord f, Ord c) =>
  -- | (lower bound, symbol, upper bound) - Similar to @range@
  --     but also provides expression
  SolverState f c [(Maybe (SoP f c), SoP f c, Maybe (SoP f c))]
ranges :: forall f c.
(Ord f, Ord c) =>
SolverState f c [(Maybe (SoP f c), SoP f c, Maybe (SoP f c))]
ranges =
  ((Atom f c, Range f c)
 -> (Maybe (SoP f c), SoP f c, Maybe (SoP f c)))
-> [(Atom f c, Range f c)]
-> [(Maybe (SoP f c), SoP f c, Maybe (SoP f c))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Atom f c
a, Range Bound f c
low Bound f c
up) -> (Bound f c -> Maybe (SoP f c)
forall f c. Bound f c -> Maybe (SoP f c)
boundSoP Bound f c
low, Atom f c -> SoP f c
forall f c. Atom f c -> SoP f c
symbol Atom f c
a, Bound f c -> Maybe (SoP f c)
forall f c. Bound f c -> Maybe (SoP f c)
boundSoP Bound f c
up)) ([(Atom f c, Range f c)]
 -> [(Maybe (SoP f c), SoP f c, Maybe (SoP f c))])
-> (Map (Atom f c) (Range f c) -> [(Atom f c, Range f c)])
-> Map (Atom f c) (Range f c)
-> [(Maybe (SoP f c), SoP f c, Maybe (SoP f c))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Atom f c) (Range f c) -> [(Atom f c, Range f c)]
forall k a. Map k a -> [(k, a)]
M.toList (Map (Atom f c) (Range f c)
 -> [(Maybe (SoP f c), SoP f c, Maybe (SoP f c))])
-> StateT (State f c) Maybe (Map (Atom f c) (Range f c))
-> StateT
     (State f c) Maybe [(Maybe (SoP f c), SoP f c, Maybe (SoP f c))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (State f c) Maybe (Map (Atom f c) (Range f c))
forall f c.
(Ord f, Ord c) =>
SolverState f c (Map (Atom f c) (Range f c))
getRanges