{-# 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 -> SatResult Rational
forall r. SatResult r
FOL.Unknown
    Just DNF Constr
dnf ->
      case [Maybe (Model Rational)] -> Maybe (Model Rational)
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 <- DNF Constr -> [[Constr]]
forall lit. DNF lit -> [[lit]]
unDNF DNF Constr
dnf] of
        Maybe (Model Rational)
Nothing -> SatResult Rational
forall r. SatResult r
FOL.Unsat
        Just Model Rational
m -> Model Rational -> SatResult Rational
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
  Formula (Atom Rational) -> Maybe (Formula (Atom Rational))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula (Atom Rational) -> Maybe (Formula (Atom Rational)))
-> Formula (Atom Rational) -> Maybe (Formula (Atom Rational))
forall a b. (a -> b) -> a -> b
$ [Formula (Atom Rational)] -> Formula (Atom Rational)
forall a. MonotoneBoolean a => [a] -> a
orB ([Formula (Atom Rational)] -> Formula (Atom Rational))
-> [Formula (Atom Rational)] -> Formula (Atom Rational)
forall a b. (a -> b) -> a -> b
$ ([Constr] -> Formula (Atom Rational))
-> [[Constr]] -> [Formula (Atom Rational)]
forall a b. (a -> b) -> [a] -> [b]
map ([Formula (Atom Rational)] -> Formula (Atom Rational)
forall a. MonotoneBoolean a => [a] -> a
andB ([Formula (Atom Rational)] -> Formula (Atom Rational))
-> ([Constr] -> [Formula (Atom Rational)])
-> [Constr]
-> Formula (Atom Rational)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constr -> Formula (Atom Rational))
-> [Constr] -> [Formula (Atom Rational)]
forall a b. (a -> b) -> [a] -> [b]
map (Atom Rational -> Formula (Atom Rational)
forall r. Real r => Atom r -> Formula (Atom r)
LAFOL.toFOLFormula (Atom Rational -> Formula (Atom Rational))
-> (Constr -> Atom Rational) -> Constr -> Formula (Atom Rational)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constr -> Atom Rational
toLAAtom)) ([[Constr]] -> [Formula (Atom Rational)])
-> [[Constr]] -> [Formula (Atom Rational)]
forall a b. (a -> b) -> a -> b
$ DNF Constr -> [[Constr]]
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 = DNF Constr -> Maybe (DNF Constr)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return DNF Constr
forall a. MonotoneBoolean a => a
true
    f Formula (Atom Rational)
FOL.F = DNF Constr -> Maybe (DNF Constr)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return DNF Constr
forall a. MonotoneBoolean a => a
false
    f (FOL.Atom (OrdRel Expr Rational
a RelOp
op Expr Rational
b)) = do
       Expr Rational
a' <- Expr Rational -> Maybe (Expr Rational)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
LAFOL.fromFOLExpr Expr Rational
a
       Expr Rational
b' <- Expr Rational -> Maybe (Expr Rational)
forall r. (Real r, Fractional r) => Expr r -> Maybe (Expr r)
LAFOL.fromFOLExpr Expr Rational
b
       DNF Constr -> Maybe (DNF Constr)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (DNF Constr -> Maybe (DNF Constr))
-> DNF Constr -> Maybe (DNF Constr)
forall a b. (a -> b) -> a -> b
$ Atom Rational -> DNF Constr
fromLAAtom (Atom Rational -> DNF Constr) -> Atom Rational -> DNF Constr
forall a b. (a -> b) -> a -> b
$ Expr Rational -> RelOp -> Expr Rational -> Atom Rational
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) = (DNF Constr -> DNF Constr -> DNF Constr)
-> Maybe (DNF Constr) -> Maybe (DNF Constr) -> Maybe (DNF Constr)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 DNF Constr -> DNF Constr -> DNF Constr
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) = (DNF Constr -> DNF Constr -> DNF Constr)
-> Maybe (DNF Constr) -> Maybe (DNF Constr) -> Maybe (DNF Constr)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 DNF Constr -> DNF Constr -> DNF Constr
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 (Formula (Atom Rational) -> Formula (Atom Rational)
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 (Formula (Atom Rational) -> Formula (Atom Rational)
forall a. Complement a => a -> a
notB Formula (Atom Rational)
a Formula (Atom Rational)
-> Formula (Atom Rational) -> Formula (Atom Rational)
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 Formula (Atom Rational)
-> Formula (Atom Rational) -> Formula (Atom Rational)
forall a. Boolean a => a -> a -> a
.=>. Formula (Atom Rational)
b) Formula (Atom Rational)
-> Formula (Atom Rational) -> Formula (Atom Rational)
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Formula (Atom Rational)
b Formula (Atom Rational)
-> Formula (Atom Rational) -> Formula (Atom Rational)
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 (Var -> Formula (Atom Rational) -> Formula (Atom Rational)
forall a. Var -> Formula a -> Formula a
FOL.Exists Var
v (Formula (Atom Rational) -> Formula (Atom Rational)
forall a. Complement a => Formula a -> Formula a
FOL.pushNot Formula (Atom Rational)
a))
      DNF Constr -> Maybe (DNF Constr)
forall a. a -> Maybe 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
      DNF Constr -> Maybe (DNF Constr)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (DNF Constr -> Maybe (DNF Constr))
-> DNF Constr -> Maybe (DNF Constr)
forall a b. (a -> b) -> a -> b
$ [DNF Constr] -> DNF Constr
forall a. MonotoneBoolean a => [a] -> a
orB [[[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF ([[Constr]] -> DNF Constr) -> [[Constr]] -> DNF Constr
forall a b. (a -> b) -> a -> b
$ Maybe [Constr] -> [[Constr]]
forall a. Maybe a -> [a]
maybeToList (Maybe [Constr] -> [[Constr]]) -> Maybe [Constr] -> [[Constr]]
forall a b. (a -> b) -> a -> b
$ (([Constr], Model Rational -> Model Rational) -> [Constr])
-> Maybe ([Constr], Model Rational -> Model Rational)
-> Maybe [Constr]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Constr], Model Rational -> Model Rational) -> [Constr]
forall a b. (a, b) -> a
fst (Maybe ([Constr], Model Rational -> Model Rational)
 -> Maybe [Constr])
-> Maybe ([Constr], Model Rational -> Model Rational)
-> Maybe [Constr]
forall a b. (a -> b) -> a -> b
$ Var
-> [Constr] -> Maybe ([Constr], Model Rational -> Model Rational)
project' Var
v [Constr]
xs | [Constr]
xs <- DNF Constr -> [[Constr]]
forall lit. DNF lit -> [[lit]]
unDNF DNF Constr
dnf]

negateDNFConstr :: DNF Constr -> DNF Constr
negateDNFConstr :: DNF Constr -> DNF Constr
negateDNFConstr (DNF [[Constr]]
xs) = [DNF Constr] -> DNF Constr
forall a. MonotoneBoolean a => [a] -> a
orB ([DNF Constr] -> DNF Constr)
-> ([[Constr]] -> [DNF Constr]) -> [[Constr]] -> DNF Constr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Constr] -> DNF Constr) -> [[Constr]] -> [DNF Constr]
forall a b. (a -> b) -> [a] -> [b]
map ([DNF Constr] -> DNF Constr
forall a. MonotoneBoolean a => [a] -> a
andB ([DNF Constr] -> DNF Constr)
-> ([Constr] -> [DNF Constr]) -> [Constr] -> DNF Constr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constr -> DNF Constr) -> [Constr] -> [DNF Constr]
forall a b. (a -> b) -> [a] -> [b]
map Constr -> DNF Constr
f) ([[Constr]] -> DNF Constr) -> [[Constr]] -> DNF Constr
forall a b. (a -> b) -> a -> b
$ [[Constr]]
xs
  where
    f :: Constr -> DNF Constr
    f :: Constr -> DNF Constr
f (IsPos ExprZ
t)    = [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ -> Constr
IsNonneg (ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
t)]]
    f (IsNonneg ExprZ
t) = [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ -> Constr
IsPos (ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
t)]]
    f (IsZero ExprZ
t)   = [[Constr]] -> DNF Constr
forall lit. [[lit]] -> DNF lit
DNF [[ExprZ -> Constr
IsPos ExprZ
t], [ExprZ -> Constr
IsPos (ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v
negateV ExprZ
t)]]

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