{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.FOL.Arith
-- Copyright   :  (c) Masahiro Sakai 2011-2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Arithmetic language (not limited to linear ones).
--
-----------------------------------------------------------------------------
module ToySolver.Data.FOL.Arith
  (
  -- * Arithmetic expressions
    Expr (..)
  , var
  , evalExpr

  -- * Atomic formula
  , module ToySolver.Data.OrdRel
  , Atom (..)
  , evalAtom

  -- * Arithmetic formula
  , module ToySolver.Data.FOL.Formula

  -- * Misc
  , SatResult (..)
  ) where

import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.Ratio

import ToySolver.Data.OrdRel
import ToySolver.Data.FOL.Formula
import ToySolver.Data.IntVar

-- ---------------------------------------------------------------------------

-- | Arithmetic expressions
data Expr r
  = Const r
  | Var Var
  | Expr r :+: Expr r
  | Expr r :*: Expr r
  | Expr r :/: Expr r
  deriving (Expr r -> Expr r -> Bool
(Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Bool) -> Eq (Expr r)
forall r. Eq r => Expr r -> Expr r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr r -> Expr r -> Bool
$c/= :: forall r. Eq r => Expr r -> Expr r -> Bool
== :: Expr r -> Expr r -> Bool
$c== :: forall r. Eq r => Expr r -> Expr r -> Bool
Eq, Eq (Expr r)
Eq (Expr r)
-> (Expr r -> Expr r -> Ordering)
-> (Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Bool)
-> (Expr r -> Expr r -> Expr r)
-> (Expr r -> Expr r -> Expr r)
-> Ord (Expr r)
Expr r -> Expr r -> Bool
Expr r -> Expr r -> Ordering
Expr r -> Expr r -> Expr r
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 r. Ord r => Eq (Expr r)
forall r. Ord r => Expr r -> Expr r -> Bool
forall r. Ord r => Expr r -> Expr r -> Ordering
forall r. Ord r => Expr r -> Expr r -> Expr r
min :: Expr r -> Expr r -> Expr r
$cmin :: forall r. Ord r => Expr r -> Expr r -> Expr r
max :: Expr r -> Expr r -> Expr r
$cmax :: forall r. Ord r => Expr r -> Expr r -> Expr r
>= :: Expr r -> Expr r -> Bool
$c>= :: forall r. Ord r => Expr r -> Expr r -> Bool
> :: Expr r -> Expr r -> Bool
$c> :: forall r. Ord r => Expr r -> Expr r -> Bool
<= :: Expr r -> Expr r -> Bool
$c<= :: forall r. Ord r => Expr r -> Expr r -> Bool
< :: Expr r -> Expr r -> Bool
$c< :: forall r. Ord r => Expr r -> Expr r -> Bool
compare :: Expr r -> Expr r -> Ordering
$ccompare :: forall r. Ord r => Expr r -> Expr r -> Ordering
$cp1Ord :: forall r. Ord r => Eq (Expr r)
Ord, Int -> Expr r -> ShowS
[Expr r] -> ShowS
Expr r -> String
(Int -> Expr r -> ShowS)
-> (Expr r -> String) -> ([Expr r] -> ShowS) -> Show (Expr r)
forall r. Show r => Int -> Expr r -> ShowS
forall r. Show r => [Expr r] -> ShowS
forall r. Show r => Expr r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr r] -> ShowS
$cshowList :: forall r. Show r => [Expr r] -> ShowS
show :: Expr r -> String
$cshow :: forall r. Show r => Expr r -> String
showsPrec :: Int -> Expr r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> Expr r -> ShowS
Show)

instance Num r => Num (Expr r) where
  Expr r
a + :: Expr r -> Expr r -> Expr r
+ Expr r
b = Expr r
a Expr r -> Expr r -> Expr r
forall r. Expr r -> Expr r -> Expr r
:+: Expr r
b
  Expr r
a * :: Expr r -> Expr r -> Expr r
* Expr r
b = Expr r
a Expr r -> Expr r -> Expr r
forall r. Expr r -> Expr r -> Expr r
:*: Expr r
b
  Expr r
a - :: Expr r -> Expr r -> Expr r
- Expr r
b = Expr r
a Expr r -> Expr r -> Expr r
forall a. Num a => a -> a -> a
+ Expr r -> Expr r
forall a. Num a => a -> a
negate Expr r
b
  negate :: Expr r -> Expr r
negate Expr r
a = r -> Expr r
forall r. r -> Expr r
Const (-r
1) Expr r -> Expr r -> Expr r
forall r. Expr r -> Expr r -> Expr r
:*: Expr r
a
  abs :: Expr r -> Expr r
abs Expr r
a = Expr r
a
  signum :: Expr r -> Expr r
signum Expr r
_ = Expr r
1
  fromInteger :: Integer -> Expr r
fromInteger = r -> Expr r
forall r. r -> Expr r
Const (r -> Expr r) -> (Integer -> r) -> Integer -> Expr r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> r
forall a. Num a => Integer -> a
fromInteger

instance Fractional r => Fractional (Expr r) where
  Expr r
a / :: Expr r -> Expr r -> Expr r
/ Expr r
b = Expr r
a Expr r -> Expr r -> Expr r
forall r. Expr r -> Expr r -> Expr r
:/: Expr r
b
  fromRational :: Rational -> Expr r
fromRational Rational
x = Integer -> Expr r
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x) Expr r -> Expr r -> Expr r
forall a. Fractional a => a -> a -> a
/ Integer -> Expr r
forall a. Num a => Integer -> a
fromInteger (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x)

instance Functor Expr where
  fmap :: (a -> b) -> Expr a -> Expr b
fmap a -> b
f = Expr a -> Expr b
g
    where
      g :: Expr a -> Expr b
g (Const a
c) = b -> Expr b
forall r. r -> Expr r
Const (a -> b
f a
c)
      g (Var Int
v)   = Int -> Expr b
forall r. Int -> Expr r
Var Int
v
      g (Expr a
a :+: Expr a
b) = Expr a -> Expr b
g Expr a
a Expr b -> Expr b -> Expr b
forall r. Expr r -> Expr r -> Expr r
:+: Expr a -> Expr b
g Expr a
b
      g (Expr a
a :*: Expr a
b) = Expr a -> Expr b
g Expr a
a Expr b -> Expr b -> Expr b
forall r. Expr r -> Expr r -> Expr r
:*: Expr a -> Expr b
g Expr a
b
      g (Expr a
a :/: Expr a
b) = Expr a -> Expr b
g Expr a
a Expr b -> Expr b -> Expr b
forall r. Expr r -> Expr r -> Expr r
:/: Expr a -> Expr b
g Expr a
b

instance Variables (Expr r) where
  vars :: Expr r -> VarSet
vars (Const r
_) = VarSet
IS.empty
  vars (Var Int
v)   = Int -> VarSet
IS.singleton Int
v
  vars (Expr r
a :+: Expr r
b) = Expr r -> VarSet
forall a. Variables a => a -> VarSet
vars Expr r
a VarSet -> VarSet -> VarSet
`IS.union` Expr r -> VarSet
forall a. Variables a => a -> VarSet
vars Expr r
b
  vars (Expr r
a :*: Expr r
b) = Expr r -> VarSet
forall a. Variables a => a -> VarSet
vars Expr r
a VarSet -> VarSet -> VarSet
`IS.union` Expr r -> VarSet
forall a. Variables a => a -> VarSet
vars Expr r
b
  vars (Expr r
a :/: Expr r
b) = Expr r -> VarSet
forall a. Variables a => a -> VarSet
vars Expr r
a VarSet -> VarSet -> VarSet
`IS.union` Expr r -> VarSet
forall a. Variables a => a -> VarSet
vars Expr r
b

-- | single variable expression
var :: Var -> Expr r
var :: Int -> Expr r
var = Int -> Expr r
forall r. Int -> Expr r
Var

-- | evaluate an 'Expr' with respect to a 'Model'
evalExpr :: Fractional r => Model r -> Expr r -> r
evalExpr :: Model r -> Expr r -> r
evalExpr Model r
m = Expr r -> r
f
  where
    f :: Expr r -> r
f (Const r
x) = r
x
    f (Var Int
v) = Model r
m Model r -> Int -> r
forall a. IntMap a -> Int -> a
IM.! Int
v
    f (Expr r
a :+: Expr r
b) = Expr r -> r
f Expr r
a r -> r -> r
forall a. Num a => a -> a -> a
+ Expr r -> r
f Expr r
b
    f (Expr r
a :*: Expr r
b) = Expr r -> r
f Expr r
a r -> r -> r
forall a. Num a => a -> a -> a
* Expr r -> r
f Expr r
b
    f (Expr r
a :/: Expr r
b) = Expr r -> r
f Expr r
a r -> r -> r
forall a. Fractional a => a -> a -> a
/ Expr r -> r
f Expr r
b

instance Fractional r => Eval (Model r) (Expr r) r where
  eval :: Model r -> Expr r -> r
eval = Model r -> Expr r -> r
forall r. Fractional r => Model r -> Expr r -> r
evalExpr

-- ---------------------------------------------------------------------------

-- | Atomic formula
type Atom c = OrdRel (Expr c)

evalAtom :: (Real r, Fractional r) => Model r -> Atom r -> Bool
evalAtom :: Model r -> Atom r -> Bool
evalAtom Model r
m (OrdRel Expr r
a RelOp
op Expr r
b) = RelOp -> r -> r -> Bool
forall a. Ord a => RelOp -> a -> a -> Bool
evalOp RelOp
op (Model r -> Expr r -> r
forall r. Fractional r => Model r -> Expr r -> r
evalExpr Model r
m Expr r
a) (Model r -> Expr r -> r
forall r. Fractional r => Model r -> Expr r -> r
evalExpr Model r
m Expr r
b)

instance IsEqRel (Expr c) (Formula (Atom c)) where
  Expr c
a .==. :: Expr c -> Expr c -> Formula (Atom c)
.==. Expr c
b = Atom c -> Formula (Atom c)
forall a. a -> Formula a
Atom (Expr c
a Expr c -> Expr c -> Atom c
forall e r. IsEqRel e r => e -> e -> r
.==. Expr c
b)
  Expr c
a ./=. :: Expr c -> Expr c -> Formula (Atom c)
./=. Expr c
b = Atom c -> Formula (Atom c)
forall a. a -> Formula a
Atom (Expr c
a Expr c -> Expr c -> Atom c
forall e r. IsEqRel e r => e -> e -> r
./=. Expr c
b)

instance IsOrdRel (Expr c) (Formula (Atom c)) where
  ordRel :: RelOp -> Expr c -> Expr c -> Formula (Atom c)
ordRel RelOp
op Expr c
a Expr c
b = Atom c -> Formula (Atom c)
forall a. a -> Formula a
Atom (RelOp -> Expr c -> Expr c -> Atom c
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
op Expr c
a Expr c
b)

-- ---------------------------------------------------------------------------

-- | results of satisfiability checking
data SatResult r = Unknown | Unsat | Sat (Model r)
  deriving (Int -> SatResult r -> ShowS
[SatResult r] -> ShowS
SatResult r -> String
(Int -> SatResult r -> ShowS)
-> (SatResult r -> String)
-> ([SatResult r] -> ShowS)
-> Show (SatResult r)
forall r. Show r => Int -> SatResult r -> ShowS
forall r. Show r => [SatResult r] -> ShowS
forall r. Show r => SatResult r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SatResult r] -> ShowS
$cshowList :: forall r. Show r => [SatResult r] -> ShowS
show :: SatResult r -> String
$cshow :: forall r. Show r => SatResult r -> String
showsPrec :: Int -> SatResult r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> SatResult r -> ShowS
Show, SatResult r -> SatResult r -> Bool
(SatResult r -> SatResult r -> Bool)
-> (SatResult r -> SatResult r -> Bool) -> Eq (SatResult r)
forall r. Eq r => SatResult r -> SatResult r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SatResult r -> SatResult r -> Bool
$c/= :: forall r. Eq r => SatResult r -> SatResult r -> Bool
== :: SatResult r -> SatResult r -> Bool
$c== :: forall r. Eq r => SatResult r -> SatResult r -> Bool
Eq, Eq (SatResult r)
Eq (SatResult r)
-> (SatResult r -> SatResult r -> Ordering)
-> (SatResult r -> SatResult r -> Bool)
-> (SatResult r -> SatResult r -> Bool)
-> (SatResult r -> SatResult r -> Bool)
-> (SatResult r -> SatResult r -> Bool)
-> (SatResult r -> SatResult r -> SatResult r)
-> (SatResult r -> SatResult r -> SatResult r)
-> Ord (SatResult r)
SatResult r -> SatResult r -> Bool
SatResult r -> SatResult r -> Ordering
SatResult r -> SatResult r -> SatResult r
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 r. Ord r => Eq (SatResult r)
forall r. Ord r => SatResult r -> SatResult r -> Bool
forall r. Ord r => SatResult r -> SatResult r -> Ordering
forall r. Ord r => SatResult r -> SatResult r -> SatResult r
min :: SatResult r -> SatResult r -> SatResult r
$cmin :: forall r. Ord r => SatResult r -> SatResult r -> SatResult r
max :: SatResult r -> SatResult r -> SatResult r
$cmax :: forall r. Ord r => SatResult r -> SatResult r -> SatResult r
>= :: SatResult r -> SatResult r -> Bool
$c>= :: forall r. Ord r => SatResult r -> SatResult r -> Bool
> :: SatResult r -> SatResult r -> Bool
$c> :: forall r. Ord r => SatResult r -> SatResult r -> Bool
<= :: SatResult r -> SatResult r -> Bool
$c<= :: forall r. Ord r => SatResult r -> SatResult r -> Bool
< :: SatResult r -> SatResult r -> Bool
$c< :: forall r. Ord r => SatResult r -> SatResult r -> Bool
compare :: SatResult r -> SatResult r -> Ordering
$ccompare :: forall r. Ord r => SatResult r -> SatResult r -> Ordering
$cp1Ord :: forall r. Ord r => Eq (SatResult r)
Ord)

-- ---------------------------------------------------------------------------