packages feed

sop-satisfier-0.3.4.5: src/SoPSat/Internal/NewtonsMethod.hs

{-# LANGUAGE ScopedTypeVariables #-}

module SoPSat.Internal.NewtonsMethod
where

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

import SoPSat.Internal.SoP (
  Atom (..),
  Product (..),
  SoP (..),
  Symbol (..),
 )
import SoPSat.SoP (atoms)

-- | Evaluates SoP given atom bindings
evalSoP ::
  (Ord f, Ord c, Floating n) =>
  -- | Expression to evaluate
  SoP f c ->
  -- | Bindings from atoms to values
  Map (Atom f c) n ->
  -- | Evaluation result
  n
evalSoP (S []) _ = 0
evalSoP (S ps) binds = sum $ map (`evalProduct` binds) ps

{- | Evaluates product given atom bindings

Used by @evalSoP@
-}
evalProduct ::
  (Ord f, Ord c, Floating n) =>
  -- | Product to evalute
  Product f c ->
  -- | Atom bindings
  Map (Atom f c) n ->
  -- | Evaluation results
  n
evalProduct (P ss) binds = product $ map (`evalSymbol` binds) ss

{- | Evaluates symbol given atom bindings

Used by @evalProduct@
-}
evalSymbol ::
  (Ord f, Ord c, Floating n) =>
  -- | Symbol to evaluate
  Symbol f c ->
  -- | Atom bindings
  Map (Atom f c) n ->
  -- | Evaluation result
  n
evalSymbol (I i) _ = fromInteger i
evalSymbol (A a) binds = f $ M.lookup a binds
 where
  f (Just n) = n
  f Nothing = 0
evalSymbol (E b p) binds = exp (evalProduct p binds * log (evalSoP b binds))

{- | Analitically computes derivative of an expression
with respect to an atom

Returns function similar to @evalSoP@
-}
derivative ::
  (Ord f, Ord c, Floating n) =>
  -- | Expression to take a derivative of
  SoP f c ->
  -- | Atom to take a derivetive with respect to
  Atom f c ->
  -- | Function from bindings, representing point,
  -- to value of the derivative at that point
  (Map (Atom f c) n -> n)
derivative sop symb = \binds -> sum $ d <*> [binds]
 where
  d = map (`derivativeProduct` symb) $ unS sop

{- | Analitically computes derivative of a product
with respect to an atom

Used by @derivative@
-}
derivativeProduct ::
  (Ord f, Ord c, Floating n) =>
  -- | Product to take a derivative of
  Product f c ->
  -- | Atom to take a derivative with respect to
  Atom f c ->
  -- | Function from bindings to a value
  (Map (Atom f c) n -> n)
derivativeProduct (P []) _ = const 0
derivativeProduct (P (s : ss)) symb = \binds ->
  derivativeSymbol s symb binds * evalProduct ps binds
    + evalSymbol s binds * derivativeProduct ps symb binds
 where
  ps = P ss

{- | Analitically computes derivative of a symbol
with respect to an atom

Used by @derivativeProduct@
-}
derivativeSymbol ::
  (Ord f, Ord c, Floating n) =>
  -- | Symbol to take a derivate of
  Symbol f c ->
  -- | Atom to take a derivate with respect to
  Atom f c ->
  -- | Function from bindings to a value
  (Map (Atom f c) n -> n)
derivativeSymbol (I _) _ = const 0
derivativeSymbol (A a) atom
  | a == atom = const 1
  | otherwise = const 0
derivativeSymbol e@(E b p) atom = \binds ->
  expExpr binds
    * ( derivative b atom binds
          * evalProduct p binds
          / evalSoP b binds
          + logExpr binds
            * derivativeProduct p atom binds
      )
 where
  expExpr = evalSymbol e
  logExpr = log . evalSoP b

-- | Finds if an expression can be equal to zero
newtonMethod ::
  forall f c n.
  (Ord f, Ord c, Ord n, Floating n) =>
  -- | Expression to check
  SoP f c ->
  -- | @Right binds@ - Atom bindings when expression is equal to zero
  --   @Left binds@ - Last checked bindings
  Either (Map (Atom f c) n) (Map (Atom f c) n)
newtonMethod sop = go init_guess steps
 where
  consts = atoms sop
  derivs = M.fromSet (derivative sop) consts
  init_guess = M.fromSet (const 10) consts
  steps = 40

  go :: Map (Atom f c) n -> Word -> Either (Map (Atom f c) n) (Map (Atom f c) n)
  go guess 0 = Left guess
  go guess n
    | val <= 0.1 = Right guess
    | otherwise =
        let
          new_guess = foldl (\binds (c, x) -> M.insert c (x - val / dsdc c) binds) guess $ M.toList guess
         in
          go new_guess (n - 1)
   where
    val = evalSoP sop guess
    dsdc c = fromJust (M.lookup c derivs) guess