{-# 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
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, Expr r -> Expr r -> Ordering
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
Ord, Var -> Expr r -> ShowS
forall r. Show r => Var -> Expr r -> ShowS
forall r. Show r => [Expr r] -> ShowS
forall r. Show r => Expr r -> String
forall a.
(Var -> 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 :: Var -> Expr r -> ShowS
$cshowsPrec :: forall r. Show r => Var -> 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 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 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 forall a. Num a => a -> a -> a
+ forall a. Num a => a -> a
negate Expr r
b
  negate :: Expr r -> Expr r
negate Expr r
a = forall r. r -> Expr r
Const (-r
1) 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 = forall r. r -> Expr r
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall r. Expr r -> Expr r -> Expr r
:/: Expr r
b
  fromRational :: Rational -> Expr r
fromRational Rational
x = forall a. Num a => Integer -> a
fromInteger (forall a. Ratio a -> a
numerator Rational
x) forall a. Fractional a => a -> a -> a
/ forall a. Num a => Integer -> a
fromInteger (forall a. Ratio a -> a
denominator Rational
x)

instance Functor Expr where
  fmap :: forall a b. (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) = forall r. r -> Expr r
Const (a -> b
f a
c)
      g (Var Var
v)   = forall r. Var -> Expr r
Var Var
v
      g (Expr a
a :+: Expr a
b) = Expr a -> Expr b
g Expr a
a 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 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 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 Var
v)   = Var -> VarSet
IS.singleton Var
v
  vars (Expr r
a :+: Expr r
b) = forall a. Variables a => a -> VarSet
vars Expr r
a VarSet -> VarSet -> VarSet
`IS.union` forall a. Variables a => a -> VarSet
vars Expr r
b
  vars (Expr r
a :*: Expr r
b) = forall a. Variables a => a -> VarSet
vars Expr r
a VarSet -> VarSet -> VarSet
`IS.union` forall a. Variables a => a -> VarSet
vars Expr r
b
  vars (Expr r
a :/: Expr r
b) = forall a. Variables a => a -> VarSet
vars Expr r
a VarSet -> VarSet -> VarSet
`IS.union` forall a. Variables a => a -> VarSet
vars Expr r
b

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

-- | evaluate an 'Expr' with respect to a 'Model'
evalExpr :: Fractional r => Model r -> Expr r -> r
evalExpr :: forall r. Fractional r => 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 Var
v) = Model r
m forall a. IntMap a -> Var -> a
IM.! Var
v
    f (Expr r
a :+: Expr r
b) = Expr r -> r
f Expr r
a 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 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 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 = 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 :: forall r. (Real r, Fractional r) => Model r -> Atom r -> Bool
evalAtom Model r
m (OrdRel Expr r
a RelOp
op Expr r
b) = forall a. Ord a => RelOp -> a -> a -> Bool
evalOp RelOp
op (forall r. Fractional r => Model r -> Expr r -> r
evalExpr Model r
m Expr r
a) (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 = forall a. a -> Formula a
Atom (Expr c
a 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 = forall a. a -> Formula a
Atom (Expr c
a 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 = forall a. a -> Formula a
Atom (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 (Var -> SatResult r -> ShowS
forall r. Show r => Var -> SatResult r -> ShowS
forall r. Show r => [SatResult r] -> ShowS
forall r. Show r => SatResult r -> String
forall a.
(Var -> 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 :: Var -> SatResult r -> ShowS
$cshowsPrec :: forall r. Show r => Var -> SatResult r -> ShowS
Show, SatResult r -> SatResult r -> Bool
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, SatResult r -> SatResult r -> Bool
SatResult r -> SatResult r -> Ordering
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
Ord)

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