{-# OPTIONS_GHC -Wall #-}
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
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 :: 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