{-# OPTIONS_GHC -Wall #-}
module ToySolver.Arith.FourierMotzkin.FOL
( solveFormula
, eliminateQuantifiers
, eliminateQuantifiers'
)
where
import Control.Monad
import Data.Maybe
import Data.VectorSpace hiding (project)
import ToySolver.Data.OrdRel
import ToySolver.Data.Boolean
import ToySolver.Data.DNF
import qualified ToySolver.Data.FOL.Arith as FOL
import qualified ToySolver.Data.LA.FOL as LAFOL
import ToySolver.Data.IntVar
import ToySolver.Arith.FourierMotzkin.Base
solveFormula :: VarSet -> FOL.Formula (FOL.Atom Rational) -> FOL.SatResult Rational
solveFormula :: VarSet -> Formula (Atom Rational) -> SatResult Rational
solveFormula VarSet
vs Formula (Atom Rational)
formula =
case Formula (Atom Rational) -> Maybe (DNF Constr)
eliminateQuantifiers' Formula (Atom Rational)
formula of
Maybe (DNF Constr)
Nothing -> forall r. SatResult r
FOL.Unknown
Just DNF Constr
dnf ->
case forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [VarSet -> [Constr] -> Maybe (Model Rational)
solve' VarSet
vs [Constr]
xs | [Constr]
xs <- forall lit. DNF lit -> [[lit]]
unDNF DNF Constr
dnf] of
Maybe (Model Rational)
Nothing -> forall r. SatResult r
FOL.Unsat
Just Model Rational
m -> forall r. Model r -> SatResult r
FOL.Sat Model Rational
m
eliminateQuantifiers :: FOL.Formula (FOL.Atom Rational) -> Maybe (FOL.Formula (FOL.Atom Rational))
eliminateQuantifiers :: Formula (Atom Rational) -> Maybe (Formula (Atom Rational))
eliminateQuantifiers Formula (Atom Rational)
phi = do
DNF Constr
dnf <- Formula (Atom Rational) -> Maybe (DNF Constr)
eliminateQuantifiers' Formula (Atom Rational)
phi
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. MonotoneBoolean a => [a] -> a
orB forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. MonotoneBoolean a => [a] -> a
andB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall r. Real r => Atom r -> Formula (Atom r)
LAFOL.toFOLFormula forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constr -> Atom Rational
toLAAtom)) forall a b. (a -> b) -> a -> b
$ forall lit. DNF lit -> [[lit]]
unDNF DNF Constr
dnf
eliminateQuantifiers' :: FOL.Formula (FOL.Atom Rational) -> Maybe (DNF Constr)
eliminateQuantifiers' :: Formula (Atom Rational) -> Maybe (DNF Constr)
eliminateQuantifiers' = Formula (Atom Rational) -> Maybe (DNF Constr)
f
where
f :: Formula (Atom Rational) -> Maybe (DNF Constr)
f Formula (Atom Rational)
FOL.T = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. MonotoneBoolean a => a
true
f Formula (Atom Rational)
FOL.F = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. MonotoneBoolean a => a
false
f (FOL.Atom (OrdRel Expr Rational
a RelOp
op Expr Rational
b)) = do
Expr Rational
a' <- forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
LAFOL.fromFOLExpr Expr Rational
a
Expr Rational
b' <- forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
LAFOL.fromFOLExpr Expr Rational
b
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Atom Rational -> DNF Constr
fromLAAtom forall a b. (a -> b) -> a -> b
$ forall e. e -> RelOp -> e -> OrdRel e
OrdRel Expr Rational
a' RelOp
op Expr Rational
b'
f (FOL.And Formula (Atom Rational)
a Formula (Atom Rational)
b) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. MonotoneBoolean a => a -> a -> a
(.&&.) (Formula (Atom Rational) -> Maybe (DNF Constr)
f Formula (Atom Rational)
a) (Formula (Atom Rational) -> Maybe (DNF Constr)
f Formula (Atom Rational)
b)
f (FOL.Or Formula (Atom Rational)
a Formula (Atom Rational)
b) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. MonotoneBoolean a => a -> a -> a
(.||.) (Formula (Atom Rational) -> Maybe (DNF Constr)
f Formula (Atom Rational)
a) (Formula (Atom Rational) -> Maybe (DNF Constr)
f Formula (Atom Rational)
b)
f (FOL.Not Formula (Atom Rational)
a) = Formula (Atom Rational) -> Maybe (DNF Constr)
f (forall a. Complement a => Formula a -> Formula a
FOL.pushNot Formula (Atom Rational)
a)
f (FOL.Imply Formula (Atom Rational)
a Formula (Atom Rational)
b) = Formula (Atom Rational) -> Maybe (DNF Constr)
f (forall a. Complement a => a -> a
notB Formula (Atom Rational)
a forall a. MonotoneBoolean a => a -> a -> a
.||. Formula (Atom Rational)
b)
f (FOL.Equiv Formula (Atom Rational)
a Formula (Atom Rational)
b) = Formula (Atom Rational) -> Maybe (DNF Constr)
f ((Formula (Atom Rational)
a forall a. Boolean a => a -> a -> a
.=>. Formula (Atom Rational)
b) forall a. MonotoneBoolean a => a -> a -> a
.&&. (Formula (Atom Rational)
b forall a. Boolean a => a -> a -> a
.=>.Formula (Atom Rational)
a))
f (FOL.Forall Var
v Formula (Atom Rational)
a) = do
DNF Constr
dnf <- Formula (Atom Rational) -> Maybe (DNF Constr)
f (forall a. Var -> Formula a -> Formula a
FOL.Exists Var
v (forall a. Complement a => Formula a -> Formula a
FOL.pushNot Formula (Atom Rational)
a))
forall (m :: * -> *) a. Monad m => a -> m a
return (DNF Constr -> DNF Constr
negateDNFConstr DNF Constr
dnf)
f (FOL.Exists Var
v Formula (Atom Rational)
a) = do
DNF Constr
dnf <- Formula (Atom Rational) -> Maybe (DNF Constr)
f Formula (Atom Rational)
a
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. MonotoneBoolean a => [a] -> a
orB [forall lit. [[lit]] -> DNF lit
DNF forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Var
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
project' Var
v [Constr]
xs | [Constr]
xs <- forall lit. DNF lit -> [[lit]]
unDNF DNF Constr
dnf]
negateDNFConstr :: DNF Constr -> DNF Constr
negateDNFConstr :: DNF Constr -> DNF Constr
negateDNFConstr (DNF [[Constr]]
xs) = forall a. MonotoneBoolean a => [a] -> a
orB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. MonotoneBoolean a => [a] -> a
andB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Constr -> DNF Constr
f) forall a b. (a -> b) -> a -> b
$ [[Constr]]
xs
where
f :: Constr -> DNF Constr
f :: Constr -> DNF Constr
f (IsPos ExprZ
t) = forall lit. [[lit]] -> DNF lit
DNF [[ExprZ -> Constr
IsNonneg (forall v. AdditiveGroup v => v -> v
negateV ExprZ
t)]]
f (IsNonneg ExprZ
t) = forall lit. [[lit]] -> DNF lit
DNF [[ExprZ -> Constr
IsPos (forall v. AdditiveGroup v => v -> v
negateV ExprZ
t)]]
f (IsZero ExprZ
t) = forall lit. [[lit]] -> DNF lit
DNF [[ExprZ -> Constr
IsPos ExprZ
t], [ExprZ -> Constr
IsPos (forall v. AdditiveGroup v => v -> v
negateV ExprZ
t)]]