{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.FourierMotzkin.FOL
-- Copyright   :  (c) Masahiro Sakai 2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
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' {x1,…,xm} φ@ returns @'Sat' M@ such that @M ⊧_LRA φ@ when such @M@ exists,
--
-- * returns @'Unsat'@ when such @M@ does not exists, and
--
-- * returns @'Unknown'@ when @φ@ is beyond LRA.
--
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

-- | Eliminate quantifiers and returns equivalent quantifier-free formula.
--
-- @'eliminateQuantifiers' φ@ returns @(ψ, lift)@ such that:
--
-- * ψ is a quantifier-free formula and @LRA ⊢ ∀y1, …, yn. φ ↔ ψ@ where @{y1, …, yn} = FV(φ) ⊇ FV(ψ)@, and
--
-- * if @M ⊧_LRA ψ@ then @lift M ⊧_LRA φ@.
--
-- φ may or may not be a closed formula.
--
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)]]

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