{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.Cooper.FOL
-- Copyright   :  (c) Masahiro Sakai 2011-2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
module ToySolver.Arith.Cooper.FOL
    ( eliminateQuantifiers
    , solveFormula
    ) where

import Control.Monad

import ToySolver.Data.OrdRel
import ToySolver.Data.Boolean
import qualified ToySolver.Data.FOL.Arith as FOL
import qualified ToySolver.Data.LA.FOL as LAFOL
import ToySolver.Data.IntVar
import ToySolver.Arith.Cooper.Base

-- | Eliminate quantifiers and returns equivalent quantifier-free formula.
--
-- @'eliminateQuantifiers' φ@ returns @(ψ, lift)@ such that:
--
-- * ψ is a quantifier-free formula and @LIA ⊢ ∀y1, …, yn. φ ↔ ψ@ where @{y1, …, yn} = FV(φ) ⊇ FV(ψ)@, and
--
-- * if @M ⊧_LIA ψ@ then @lift M ⊧_LIA φ@.
--
-- φ may or may not be a closed formula.
--
eliminateQuantifiers :: FOL.Formula (FOL.Atom Rational) -> Maybe QFFormula
eliminateQuantifiers :: Formula (Atom Rational) -> Maybe QFFormula
eliminateQuantifiers = Formula (Atom Rational) -> Maybe QFFormula
f
  where
    f :: Formula (Atom Rational) -> Maybe QFFormula
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 -> QFFormula
fromLAAtom (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 QFFormula
f Formula (Atom Rational)
a) (Formula (Atom Rational) -> Maybe QFFormula
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 QFFormula
f Formula (Atom Rational)
a) (Formula (Atom Rational) -> Maybe QFFormula
f Formula (Atom Rational)
b)
    f (FOL.Not Formula (Atom Rational)
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Complement a => a -> a
notB (Formula (Atom Rational) -> Maybe QFFormula
f Formula (Atom Rational)
a)
    f (FOL.Imply 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. Boolean a => a -> a -> a
(.=>.) (Formula (Atom Rational) -> Maybe QFFormula
f Formula (Atom Rational)
a) (Formula (Atom Rational) -> Maybe QFFormula
f Formula (Atom Rational)
b)
    f (FOL.Equiv 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. Boolean a => a -> a -> a
(.<=>.) (Formula (Atom Rational) -> Maybe QFFormula
f Formula (Atom Rational)
a) (Formula (Atom Rational) -> Maybe QFFormula
f Formula (Atom Rational)
b)
    f (FOL.Forall Var
x Formula (Atom Rational)
body) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Complement a => a -> a
notB forall a b. (a -> b) -> a -> b
$ Formula (Atom Rational) -> Maybe QFFormula
f forall a b. (a -> b) -> a -> b
$ forall a. Var -> Formula a -> Formula a
FOL.Exists Var
x forall a b. (a -> b) -> a -> b
$ forall a. Formula a -> Formula a
FOL.Not Formula (Atom Rational)
body
    f (FOL.Exists Var
x Formula (Atom Rational)
body) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
project Var
x) (Formula (Atom Rational) -> Maybe QFFormula
f Formula (Atom Rational)
body)

-- | @'solveFormula' {x1,…,xm} φ@
--
-- * returns @'Sat' M@ such that @M ⊧_LIA φ@ when such @M@ exists,
--
-- * returns @'Unsat'@ when such @M@ does not exists, and
--
-- * returns @'Unknown'@ when @φ@ is beyond LIA.
--
solveFormula :: VarSet -> FOL.Formula (FOL.Atom Rational) -> FOL.SatResult Integer
solveFormula :: VarSet -> Formula (Atom Rational) -> SatResult Integer
solveFormula VarSet
vs Formula (Atom Rational)
formula =
  case Formula (Atom Rational) -> Maybe QFFormula
eliminateQuantifiers Formula (Atom Rational)
formula of
    Maybe QFFormula
Nothing -> forall r. SatResult r
FOL.Unknown
    Just QFFormula
formula' ->
       case VarSet -> QFFormula -> Maybe (Model Integer)
solveQFFormula VarSet
vs QFFormula
formula' of
         Maybe (Model Integer)
Nothing -> forall r. SatResult r
FOL.Unsat
         Just Model Integer
m -> forall r. Model r -> SatResult r
FOL.Sat Model Integer
m