{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module ToySolver.Data.FOL.Arith
(
Expr (..)
, var
, evalExpr
, module ToySolver.Data.OrdRel
, Atom (..)
, evalAtom
, module ToySolver.Data.FOL.Formula
, 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
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
var :: Var -> Expr r
var :: forall r. Var -> Expr r
var = forall r. Var -> Expr r
Var
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
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)
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)