{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Arith.Cooper.Base
-- Copyright   :  (c) Masahiro Sakai 2011-2014
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Naive implementation of Cooper's algorithm
--
-- Reference:
--
-- * <http://hagi.is.s.u-tokyo.ac.jp/pub/staff/hagiya/kougiroku/ronri/5.txt>
--
-- * <http://www.cs.cmu.edu/~emc/spring06/home1_files/Presburger%20Arithmetic.ppt>
--
-- See also:
--
-- * <http://hackage.haskell.org/package/presburger>
--
-----------------------------------------------------------------------------
module ToySolver.Arith.Cooper.Base
    (
    -- * Language of presburger arithmetics
      ExprZ
    , Lit (..)
    , QFFormula
    , fromLAAtom
    , (.|.)
    , Model
    , Eval (..)

    -- * Projection
    , project
    , projectN
    , projectCases
    , projectCasesN

    -- * Constraint solving
    , solve
    , solveQFFormula
    , solveQFLIRAConj
    ) where

import Control.Monad
import qualified Data.Foldable as Foldable
import Data.List
import Data.Maybe
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import Data.Ratio
import qualified Data.Semigroup as Semigroup
import Data.Set (Set)
import qualified Data.Set as Set
import Data.VectorSpace hiding (project)

import ToySolver.Data.OrdRel
import ToySolver.Data.Boolean
import ToySolver.Data.BoolExpr (BoolExpr (..))
import qualified ToySolver.Data.BoolExpr as BoolExpr
import qualified ToySolver.Data.LA as LA
import ToySolver.Data.IntVar
import qualified ToySolver.Arith.FourierMotzkin as FM

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

-- | Linear arithmetic expression over integers.
type ExprZ = LA.Expr Integer

fromLAAtom :: LA.Atom Rational -> QFFormula
fromLAAtom :: Atom Rational -> QFFormula
fromLAAtom (OrdRel Expr Rational
a RelOp
op Expr Rational
b) = forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
op Expr Integer
a' Expr Integer
b'
  where
    (Expr Integer
e1,Integer
c1) = Expr Rational -> (Expr Integer, Integer)
toRat Expr Rational
a
    (Expr Integer
e2,Integer
c2) = Expr Rational -> (Expr Integer, Integer)
toRat Expr Rational
b
    a' :: Expr Integer
a' = Integer
c2 forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
e1
    b' :: Expr Integer
b' = Integer
c1 forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
e2

-- | (t,c) represents t/c, and c must be >0.
type Rat = (ExprZ, Integer)

toRat :: LA.Expr Rational -> Rat
toRat :: Expr Rational -> (Expr Integer, Integer)
toRat Expr Rational
e = seq :: forall a b. a -> b -> b
seq Integer
m forall a b. (a -> b) -> a -> b
$ (forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff forall {a}. Integral a => Ratio a -> a
f Expr Rational
e, Integer
m)
  where
    f :: Ratio a -> a
f Ratio a
x = forall a. Ratio a -> a
numerator (forall a. Num a => Integer -> a
fromInteger Integer
m forall a. Num a => a -> a -> a
* Ratio a
x)
    m :: Integer
m = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Integral a => a -> a -> a
lcm Integer
1 [forall a. Ratio a -> a
denominator Rational
c | (Rational
c,Var
_) <- forall r. Expr r -> [(r, Var)]
LA.terms Expr Rational
e]

leZ, ltZ, geZ, gtZ :: ExprZ -> ExprZ -> Lit
leZ :: Expr Integer -> Expr Integer -> Lit
leZ Expr Integer
e1 Expr Integer
e2 = Expr Integer
e1 Expr Integer -> Expr Integer -> Lit
`ltZ` (Expr Integer
e2 forall v. AdditiveGroup v => v -> v -> v
^+^ forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
1)
ltZ :: Expr Integer -> Expr Integer -> Lit
ltZ Expr Integer
e1 Expr Integer
e2 = Expr Integer -> Lit
IsPos forall a b. (a -> b) -> a -> b
$ (Expr Integer
e2 forall v. AdditiveGroup v => v -> v -> v
^-^ Expr Integer
e1)
geZ :: Expr Integer -> Expr Integer -> Lit
geZ = forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr Integer -> Expr Integer -> Lit
leZ
gtZ :: Expr Integer -> Expr Integer -> Lit
gtZ = forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr Integer -> Expr Integer -> Lit
ltZ

eqZ :: ExprZ -> ExprZ -> QFFormula
eqZ :: Expr Integer -> Expr Integer -> QFFormula
eqZ Expr Integer
e1 Expr Integer
e2 = forall a. a -> BoolExpr a
Atom (Expr Integer
e1 Expr Integer -> Expr Integer -> Lit
`leZ` Expr Integer
e2) forall a. MonotoneBoolean a => a -> a -> a
.&&. forall a. a -> BoolExpr a
Atom (Expr Integer
e1 Expr Integer -> Expr Integer -> Lit
`geZ` Expr Integer
e2)

-- | Literals of Presburger arithmetic.
data Lit
    = IsPos ExprZ
    -- ^ @IsPos e@ means @e > 0@
    | Divisible Bool Integer ExprZ
    -- ^
    -- * @Divisible True d e@ means @e@ can be divided by @d@ (i.e. @d | e@)
    -- * @Divisible False d e@ means @e@ can not be divided by @d@ (i.e. @¬(d | e)@)
    deriving (Var -> Lit -> ShowS
[Lit] -> ShowS
Lit -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Lit] -> ShowS
$cshowList :: [Lit] -> ShowS
show :: Lit -> String
$cshow :: Lit -> String
showsPrec :: Var -> Lit -> ShowS
$cshowsPrec :: Var -> Lit -> ShowS
Show, Lit -> Lit -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lit -> Lit -> Bool
$c/= :: Lit -> Lit -> Bool
== :: Lit -> Lit -> Bool
$c== :: Lit -> Lit -> Bool
Eq, Eq Lit
Lit -> Lit -> Bool
Lit -> Lit -> Ordering
Lit -> Lit -> Lit
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Lit -> Lit -> Lit
$cmin :: Lit -> Lit -> Lit
max :: Lit -> Lit -> Lit
$cmax :: Lit -> Lit -> Lit
>= :: Lit -> Lit -> Bool
$c>= :: Lit -> Lit -> Bool
> :: Lit -> Lit -> Bool
$c> :: Lit -> Lit -> Bool
<= :: Lit -> Lit -> Bool
$c<= :: Lit -> Lit -> Bool
< :: Lit -> Lit -> Bool
$c< :: Lit -> Lit -> Bool
compare :: Lit -> Lit -> Ordering
$ccompare :: Lit -> Lit -> Ordering
Ord)

instance Variables Lit where
  vars :: Lit -> VarSet
vars (IsPos Expr Integer
t) = forall a. Variables a => a -> VarSet
vars Expr Integer
t
  vars (Divisible Bool
_ Integer
_ Expr Integer
t) = forall a. Variables a => a -> VarSet
vars Expr Integer
t

instance Complement Lit where
  notB :: Lit -> Lit
notB (IsPos Expr Integer
e) = Expr Integer
e Expr Integer -> Expr Integer -> Lit
`leZ` forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
0
  notB (Divisible Bool
b Integer
c Expr Integer
e) = Bool -> Integer -> Expr Integer -> Lit
Divisible (Bool -> Bool
not Bool
b) Integer
c Expr Integer
e

-- | Quantifier-free formula of Presburger arithmetic.
type QFFormula = BoolExpr Lit

instance IsEqRel (LA.Expr Integer) QFFormula where
  Expr Integer
a .==. :: Expr Integer -> Expr Integer -> QFFormula
.==. Expr Integer
b = Expr Integer -> Expr Integer -> QFFormula
eqZ Expr Integer
a Expr Integer
b
  Expr Integer
a ./=. :: Expr Integer -> Expr Integer -> QFFormula
./=. Expr Integer
b = forall a. Complement a => a -> a
notB forall a b. (a -> b) -> a -> b
$ Expr Integer -> Expr Integer -> QFFormula
eqZ Expr Integer
a Expr Integer
b

instance IsOrdRel (LA.Expr Integer) QFFormula where
  ordRel :: RelOp -> Expr Integer -> Expr Integer -> QFFormula
ordRel RelOp
op Expr Integer
lhs Expr Integer
rhs =
    case RelOp
op of
      RelOp
Le  -> forall a. a -> BoolExpr a
Atom forall a b. (a -> b) -> a -> b
$ Expr Integer -> Expr Integer -> Lit
leZ Expr Integer
lhs Expr Integer
rhs
      RelOp
Ge  -> forall a. a -> BoolExpr a
Atom forall a b. (a -> b) -> a -> b
$ Expr Integer -> Expr Integer -> Lit
geZ Expr Integer
lhs Expr Integer
rhs
      RelOp
Lt  -> forall a. a -> BoolExpr a
Atom forall a b. (a -> b) -> a -> b
$ Expr Integer -> Expr Integer -> Lit
ltZ Expr Integer
lhs Expr Integer
rhs
      RelOp
Gt  -> forall a. a -> BoolExpr a
Atom forall a b. (a -> b) -> a -> b
$ Expr Integer -> Expr Integer -> Lit
gtZ Expr Integer
lhs Expr Integer
rhs
      RelOp
Eql -> Expr Integer
lhs forall e r. IsEqRel e r => e -> e -> r
.==. Expr Integer
rhs
      RelOp
NEq -> Expr Integer
lhs forall e r. IsEqRel e r => e -> e -> r
./=. Expr Integer
rhs

-- | @d | e@ means @e@ can be divided by @d@.
(.|.) :: Integer -> ExprZ -> QFFormula
Integer
n .|. :: Integer -> Expr Integer -> QFFormula
.|. Expr Integer
e = forall a. a -> BoolExpr a
Atom forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Expr Integer -> Lit
Divisible Bool
True Integer
n Expr Integer
e

subst1 :: Var -> ExprZ -> QFFormula -> QFFormula
subst1 :: Var -> Expr Integer -> QFFormula -> QFFormula
subst1 Var
x Expr Integer
e = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Lit -> Lit
f
  where
    f :: Lit -> Lit
f (Divisible Bool
b Integer
c Expr Integer
e1) = Bool -> Integer -> Expr Integer -> Lit
Divisible Bool
b Integer
c forall a b. (a -> b) -> a -> b
$ forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
LA.applySubst1 Var
x Expr Integer
e Expr Integer
e1
    f (IsPos Expr Integer
e1) = Expr Integer -> Lit
IsPos forall a b. (a -> b) -> a -> b
$ forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
LA.applySubst1 Var
x Expr Integer
e Expr Integer
e1

simplify :: QFFormula -> QFFormula
simplify :: QFFormula -> QFFormula
simplify = forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Lit -> QFFormula
simplifyLit

simplifyLit :: Lit -> QFFormula
simplifyLit :: Lit -> QFFormula
simplifyLit (IsPos Expr Integer
e) =
  case forall r. Num r => Expr r -> Maybe r
LA.asConst Expr Integer
e of
    Just Integer
c -> if Integer
c forall a. Ord a => a -> a -> Bool
> Integer
0 then forall a. MonotoneBoolean a => a
true else forall a. MonotoneBoolean a => a
false
    Maybe Integer
Nothing ->
      -- e > 0  <=>  e - 1 >= 0
      -- <=>  LA.mapCoeff (`div` d) (e - 1) >= 0
      -- <=>  LA.mapCoeff (`div` d) (e - 1) + 1 > 0
      forall a. a -> BoolExpr a
Atom forall a b. (a -> b) -> a -> b
$ Expr Integer -> Lit
IsPos forall a b. (a -> b) -> a -> b
$ forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff (forall a. Integral a => a -> a -> a
`div` Integer
d) Expr Integer
e1 forall v. AdditiveGroup v => v -> v -> v
^+^ forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
1
  where
    e1 :: Expr Integer
e1 = Expr Integer
e forall v. AdditiveGroup v => v -> v -> v
^-^ forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
1
    d :: Integer
d  = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Integer]
cs then Integer
1 else forall a. Num a => a -> a
abs forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> [a] -> a
foldl1' forall a. Integral a => a -> a -> a
gcd [Integer]
cs
    cs :: [Integer]
cs = [Integer
c | (Integer
c,Var
x) <- forall r. Expr r -> [(r, Var)]
LA.terms Expr Integer
e1, Var
x forall a. Eq a => a -> a -> Bool
/= Var
LA.unitVar]
simplifyLit lit :: Lit
lit@(Divisible Bool
b Integer
c Expr Integer
e)
  | forall r. Num r => Var -> Expr r -> r
LA.coeff Var
LA.unitVar Expr Integer
e2 forall a. Integral a => a -> a -> a
`mod` Integer
d forall a. Eq a => a -> a -> Bool
/= Integer
0 = if Bool
b then forall a. MonotoneBoolean a => a
false else forall a. MonotoneBoolean a => a
true
  | Integer
c' forall a. Eq a => a -> a -> Bool
== Integer
1   = if Bool
b then forall a. MonotoneBoolean a => a
true else forall a. MonotoneBoolean a => a
false
  | Integer
d  forall a. Eq a => a -> a -> Bool
== Integer
1   = forall a. a -> BoolExpr a
Atom Lit
lit
  | Bool
otherwise = forall a. a -> BoolExpr a
Atom forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Expr Integer -> Lit
Divisible Bool
b Integer
c' Expr Integer
e'
  where
    e2 :: Expr Integer
e2 = forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff (forall a. Integral a => a -> a -> a
`mod` Integer
c) Expr Integer
e
    d :: Integer
d  = forall a. Num a => a -> a
abs forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Integral a => a -> a -> a
gcd Integer
c [Integer
c2 | (Integer
c2,Var
x) <- forall r. Expr r -> [(r, Var)]
LA.terms Expr Integer
e2, Var
x forall a. Eq a => a -> a -> Bool
/= Var
LA.unitVar]
    c' :: Integer
c' = Integer
c Integer -> Integer -> Integer
`checkedDiv` Integer
d
    e' :: Expr Integer
e' = forall b a. (Num b, Eq b) => (a -> b) -> Expr a -> Expr b
LA.mapCoeff (Integer -> Integer -> Integer
`checkedDiv` Integer
d) Expr Integer
e2

instance Eval (Model Integer) Lit Bool where
  eval :: Model Integer -> Lit -> Bool
eval Model Integer
m (IsPos Expr Integer
e) = forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
m Expr Integer
e forall a. Ord a => a -> a -> Bool
> Integer
0
  eval Model Integer
m (Divisible Bool
True Integer
n Expr Integer
e)  = forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
m Expr Integer
e forall a. Integral a => a -> a -> a
`mod` Integer
n forall a. Eq a => a -> a -> Bool
== Integer
0
  eval Model Integer
m (Divisible Bool
False Integer
n Expr Integer
e) = forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
m Expr Integer
e forall a. Integral a => a -> a -> a
`mod` Integer
n forall a. Eq a => a -> a -> Bool
/= Integer
0

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

data Witness = WCase1 Integer ExprZ | WCase2 Integer Integer Integer (Set ExprZ)
  deriving (Var -> Witness -> ShowS
[Witness] -> ShowS
Witness -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Witness] -> ShowS
$cshowList :: [Witness] -> ShowS
show :: Witness -> String
$cshow :: Witness -> String
showsPrec :: Var -> Witness -> ShowS
$cshowsPrec :: Var -> Witness -> ShowS
Show)

instance Eval (Model Integer) Witness Integer where
  eval :: Model Integer -> Witness -> Integer
eval Model Integer
model (WCase1 Integer
c Expr Integer
e) = forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
model Expr Integer
e Integer -> Integer -> Integer
`checkedDiv` Integer
c
  eval Model Integer
model (WCase2 Integer
c Integer
j Integer
delta Set (Expr Integer)
us)
    | forall a. Set a -> Bool
Set.null Set Integer
us' = Integer
j Integer -> Integer -> Integer
`checkedDiv` Integer
c
    | Bool
otherwise = (Integer
j forall a. Num a => a -> a -> a
+ (((Integer
u forall a. Num a => a -> a -> a
- Integer
delta forall a. Num a => a -> a -> a
- Integer
1) forall a. Integral a => a -> a -> a
`div` Integer
delta) forall a. Num a => a -> a -> a
* Integer
delta)) Integer -> Integer -> Integer
`checkedDiv` Integer
c
    where
      us' :: Set Integer
us' = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
model) Set (Expr Integer)
us
      u :: Integer
u = forall a. Set a -> a
Set.findMin Set Integer
us'

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

{-| @'project' x φ@ returns @(ψ, lift)@ such that:

* @⊢_LIA ∀y1, …, yn. (∃x. φ) ↔ ψ@ where @{y1, …, yn} = FV(φ) \\ {x}@, and

* if @M ⊧_LIA ψ@ then @lift M ⊧_LIA φ@.
-}
project :: Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
project :: Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
project Var
x QFFormula
formula = (QFFormula
formula', Model Integer -> Model Integer
mt)
  where
    xs :: [(QFFormula, Model Integer -> Model Integer)]
xs = Var -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
projectCases Var
x QFFormula
formula
    formula' :: QFFormula
formula' = forall {a}. [BoolExpr a] -> BoolExpr a
orB' [QFFormula
phi | (QFFormula
phi,Model Integer -> Model Integer
_) <- [(QFFormula, Model Integer -> Model Integer)]
xs]
    mt :: Model Integer -> Model Integer
mt Model Integer
m = forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ do
      (QFFormula
phi, Model Integer -> Model Integer
mt') <- [(QFFormula, Model Integer -> Model Integer)]
xs
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall m e v. Eval m e v => m -> e -> v
eval Model Integer
m QFFormula
phi
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Model Integer -> Model Integer
mt' Model Integer
m
    orB' :: [BoolExpr a] -> BoolExpr a
orB' = forall a. MonotoneBoolean a => [a] -> a
orB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. BoolExpr a -> [BoolExpr a]
f
      where
        f :: BoolExpr a -> [BoolExpr a]
f (Or [BoolExpr a]
xs) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap BoolExpr a -> [BoolExpr a]
f [BoolExpr a]
xs
        f BoolExpr a
x = [BoolExpr a
x]

{-| @'projectN' {x1,…,xm} φ@ returns @(ψ, lift)@ such that:

* @⊢_LIA ∀y1, …, yn. (∃x1, …, xm. φ) ↔ ψ@ where @{y1, …, yn} = FV(φ) \\ {x1,…,xm}@, and

* if @M ⊧_LIA ψ@ then @lift M ⊧_LIA φ@.
-}
projectN :: VarSet -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
projectN :: VarSet -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
projectN VarSet
vs2 = [Var] -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
f (VarSet -> [Var]
IS.toList VarSet
vs2)
  where
    f :: [Var] -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
    f :: [Var] -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
f [] QFFormula
formula     = (QFFormula
formula, forall a. a -> a
id)
    f (Var
v:[Var]
vs) QFFormula
formula = (QFFormula
formula3, Model Integer -> Model Integer
mt1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model Integer -> Model Integer
mt2)
      where
        (QFFormula
formula2, Model Integer -> Model Integer
mt1) = Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
project Var
v QFFormula
formula
        (QFFormula
formula3, Model Integer -> Model Integer
mt2) = [Var] -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
f [Var]
vs QFFormula
formula2

{-| @'projectCases' x φ@ returns @[(ψ_1, lift_1), …, (ψ_m, lift_m)]@ such that:

* @⊢_LIA ∀y1, …, yn. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_m)@ where @{y1, …, yn} = FV(φ) \\ {x}@, and

* if @M ⊧_LIA ψ_i@ then @lift_i M ⊧_LIA φ@.
-}
projectCases :: Var -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
projectCases :: Var -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
projectCases Var
x QFFormula
formula = do
  (QFFormula
phi, Witness
wit) <- Var -> QFFormula -> [(QFFormula, Witness)]
projectCases' Var
x QFFormula
formula
  forall (m :: * -> *) a. Monad m => a -> m a
return (QFFormula
phi, \Model Integer
m -> forall a. Var -> a -> IntMap a -> IntMap a
IM.insert Var
x (forall m e v. Eval m e v => m -> e -> v
eval Model Integer
m Witness
wit) Model Integer
m)

projectCases' :: Var -> QFFormula -> [(QFFormula, Witness)]
projectCases' :: Var -> QFFormula -> [(QFFormula, Witness)]
projectCases' Var
x QFFormula
formula = [(QFFormula
phi', Witness
w) | (QFFormula
phi,Witness
w) <- [(QFFormula, Witness)]
case1 forall a. [a] -> [a] -> [a]
++ [(QFFormula, Witness)]
case2, let phi' :: QFFormula
phi' = QFFormula -> QFFormula
simplify QFFormula
phi, QFFormula
phi' forall a. Eq a => a -> a -> Bool
/= forall a. MonotoneBoolean a => a
false]
  where
    -- eliminate Not, Imply and Equiv.
    formula0 :: QFFormula
    formula0 :: QFFormula
formula0 = forall {a}. Complement a => BoolExpr a -> BoolExpr a
pos QFFormula
formula
      where
        pos :: BoolExpr a -> BoolExpr a
pos (Atom a
a) = forall a. a -> BoolExpr a
Atom a
a
        pos (And [BoolExpr a]
xs) = forall {a}. [BoolExpr a] -> BoolExpr a
And (forall a b. (a -> b) -> [a] -> [b]
map BoolExpr a -> BoolExpr a
pos [BoolExpr a]
xs)
        pos (Or [BoolExpr a]
xs) = forall {a}. [BoolExpr a] -> BoolExpr a
Or (forall a b. (a -> b) -> [a] -> [b]
map BoolExpr a -> BoolExpr a
pos [BoolExpr a]
xs)
        pos (Not BoolExpr a
x) = BoolExpr a -> BoolExpr a
neg BoolExpr a
x
        pos (Imply BoolExpr a
x BoolExpr a
y) = BoolExpr a -> BoolExpr a
neg BoolExpr a
x forall a. MonotoneBoolean a => a -> a -> a
.||. BoolExpr a -> BoolExpr a
pos BoolExpr a
y
        pos (Equiv BoolExpr a
x BoolExpr a
y) = BoolExpr a -> BoolExpr a
pos ((BoolExpr a
x forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
y) forall a. MonotoneBoolean a => a -> a -> a
.&&. (BoolExpr a
y forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
x))
        pos (ITE BoolExpr a
c BoolExpr a
t BoolExpr a
e) = BoolExpr a -> BoolExpr a
pos ((BoolExpr a
c forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
t) forall a. MonotoneBoolean a => a -> a -> a
.&&. (forall a. BoolExpr a -> BoolExpr a
Not BoolExpr a
c forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
e))

        neg :: BoolExpr a -> BoolExpr a
neg (Atom a
a) = forall a. a -> BoolExpr a
Atom (forall a. Complement a => a -> a
notB a
a)
        neg (And [BoolExpr a]
xs) = forall {a}. [BoolExpr a] -> BoolExpr a
Or (forall a b. (a -> b) -> [a] -> [b]
map BoolExpr a -> BoolExpr a
neg [BoolExpr a]
xs)
        neg (Or [BoolExpr a]
xs) = forall {a}. [BoolExpr a] -> BoolExpr a
And (forall a b. (a -> b) -> [a] -> [b]
map BoolExpr a -> BoolExpr a
neg [BoolExpr a]
xs)
        neg (Not BoolExpr a
x) = BoolExpr a -> BoolExpr a
pos BoolExpr a
x
        neg (Imply BoolExpr a
x BoolExpr a
y) = BoolExpr a -> BoolExpr a
pos BoolExpr a
x forall a. MonotoneBoolean a => a -> a -> a
.&&. BoolExpr a -> BoolExpr a
neg BoolExpr a
y
        neg (Equiv BoolExpr a
x BoolExpr a
y) = BoolExpr a -> BoolExpr a
neg ((BoolExpr a
x forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
y) forall a. MonotoneBoolean a => a -> a -> a
.&&. (BoolExpr a
y forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
x))
        neg (ITE BoolExpr a
c BoolExpr a
t BoolExpr a
e) = BoolExpr a -> BoolExpr a
neg ((BoolExpr a
c forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
t) forall a. MonotoneBoolean a => a -> a -> a
.&&. (forall a. BoolExpr a -> BoolExpr a
Not BoolExpr a
c forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
e))

    -- xの係数の最小公倍数
    c :: Integer
    c :: Integer
c = forall a. LCM a -> a
getLCM forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap Lit -> LCM Integer
f QFFormula
formula0
      where
         f :: Lit -> LCM Integer
f (IsPos Expr Integer
e) = forall a. a -> LCM a
LCM forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe Integer
1 (forall r. Num r => Var -> Expr r -> Maybe r
LA.lookupCoeff Var
x Expr Integer
e)
         f (Divisible Bool
_ Integer
_ Expr Integer
e) = forall a. a -> LCM a
LCM forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe Integer
1 (forall r. Num r => Var -> Expr r -> Maybe r
LA.lookupCoeff Var
x Expr Integer
e)

    -- 式をスケールしてxの係数の絶対値をcへと変換し、その後cxをxで置き換え、
    -- xがcで割り切れるという制約を追加した論理式
    formula1 :: QFFormula
    formula1 :: QFFormula
formula1 = QFFormula -> QFFormula
simplify forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Lit -> Lit
f QFFormula
formula0 forall a. MonotoneBoolean a => a -> a -> a
.&&. (Integer
c Integer -> Expr Integer -> QFFormula
.|. forall r. Num r => Var -> Expr r
LA.var Var
x)
      where
        f :: Lit -> Lit
f lit :: Lit
lit@(IsPos Expr Integer
e) =
          case forall r. Num r => Var -> Expr r -> Maybe r
LA.lookupCoeff Var
x Expr Integer
e of
            Maybe Integer
Nothing -> Lit
lit
            Just Integer
a ->
              let s :: Integer
s = forall a. Num a => a -> a
abs (Integer
c Integer -> Integer -> Integer
`checkedDiv` Integer
a)
              in Expr Integer -> Lit
IsPos forall a b. (a -> b) -> a -> b
$ Integer -> Expr Integer -> Expr Integer
g Integer
s Expr Integer
e
        f lit :: Lit
lit@(Divisible Bool
b Integer
d Expr Integer
e) =
          case forall r. Num r => Var -> Expr r -> Maybe r
LA.lookupCoeff Var
x Expr Integer
e of
            Maybe Integer
Nothing -> Lit
lit
            Just Integer
a ->
              let s :: Integer
s = forall a. Num a => a -> a
abs (Integer
c Integer -> Integer -> Integer
`checkedDiv` Integer
a)
              in Bool -> Integer -> Expr Integer -> Lit
Divisible Bool
b (Integer
sforall a. Num a => a -> a -> a
*Integer
d) forall a b. (a -> b) -> a -> b
$ Integer -> Expr Integer -> Expr Integer
g Integer
s Expr Integer
e

        g :: Integer -> ExprZ -> ExprZ
        g :: Integer -> Expr Integer -> Expr Integer
g Integer
s = forall b a. (Num b, Eq b) => (a -> Var -> b) -> Expr a -> Expr b
LA.mapCoeffWithVar (\Integer
c' Var
x' -> if Var
xforall a. Eq a => a -> a -> Bool
==Var
x' then forall a. Num a => a -> a
signum Integer
c' else Integer
sforall a. Num a => a -> a -> a
*Integer
c')

    -- d|x+t という形の論理式の d の最小公倍数
    delta :: Integer
    delta :: Integer
delta = forall a. LCM a -> a
getLCM forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap Lit -> LCM Integer
f QFFormula
formula1
      where
        f :: Lit -> LCM Integer
f (Divisible Bool
_ Integer
d Expr Integer
_) = forall a. a -> LCM a
LCM Integer
d
        f (IsPos Expr Integer
_) = forall a. a -> LCM a
LCM Integer
1

    -- ts = {t | t < x は formula1 に現れる原子論理式}
    ts :: Set ExprZ
    ts :: Set (Expr Integer)
ts = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap Lit -> Set (Expr Integer)
f QFFormula
formula1
      where
        f :: Lit -> Set (Expr Integer)
f (Divisible Bool
_ Integer
_ Expr Integer
_) = forall a. Set a
Set.empty
        f (IsPos Expr Integer
e) =
          case forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
LA.extractMaybe Var
x Expr Integer
e of
            Maybe (Integer, Expr Integer)
Nothing -> forall a. Set a
Set.empty
            Just (Integer
1, Expr Integer
e') -> forall a. a -> Set a
Set.singleton (forall v. AdditiveGroup v => v -> v
negateV Expr Integer
e') -- IsPos e <=> (x + e' > 0) <=> (-e' < x)
            Just (-1, Expr Integer
_) -> forall a. Set a
Set.empty -- IsPos e <=> (-x + e' > 0) <=> (x < e')
            Maybe (Integer, Expr Integer)
_ -> forall a. HasCallStack => String -> a
error String
"should not happen"

    -- formula1を真にする最小のxが存在する場合
    case1 :: [(QFFormula, Witness)]
    case1 :: [(QFFormula, Witness)]
case1 = [ (Var -> Expr Integer -> QFFormula -> QFFormula
subst1 Var
x Expr Integer
e QFFormula
formula1, Integer -> Expr Integer -> Witness
WCase1 Integer
c Expr Integer
e)
            | Integer
j <- [Integer
1..Integer
delta], Expr Integer
t <- forall a. Set a -> [a]
Set.toList Set (Expr Integer)
ts, let e :: Expr Integer
e = Expr Integer
t forall v. AdditiveGroup v => v -> v -> v
^+^ forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
j ]

    -- formula1のなかの x < t を真に t < x を偽に置き換えた論理式
    formula2 :: QFFormula
    formula2 :: QFFormula
formula2 = QFFormula -> QFFormula
simplify forall a b. (a -> b) -> a -> b
$ forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Lit -> QFFormula
f QFFormula
formula1
      where
        f :: Lit -> QFFormula
f lit :: Lit
lit@(IsPos Expr Integer
e) =
          case forall r. Num r => Var -> Expr r -> Maybe r
LA.lookupCoeff Var
x Expr Integer
e of
            Maybe Integer
Nothing -> forall a. a -> BoolExpr a
Atom Lit
lit
            Just Integer
1    -> forall a. MonotoneBoolean a => a
false -- IsPos e <=> ( x + e' > 0) <=> -e' < x
            Just (-1) -> forall a. MonotoneBoolean a => a
true  -- IsPos e <=> (-x + e' > 0) <=>  x  < e'
            Maybe Integer
_ -> forall a. HasCallStack => String -> a
error String
"should not happen"
        f lit :: Lit
lit@(Divisible Bool
_ Integer
_ Expr Integer
_) = forall a. a -> BoolExpr a
Atom Lit
lit

    -- us = {u | x < u は formula1 に現れる原子論理式}
    us :: Set ExprZ
    us :: Set (Expr Integer)
us = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap Lit -> Set (Expr Integer)
f QFFormula
formula1
      where
        f :: Lit -> Set (Expr Integer)
f (IsPos Expr Integer
e) =
          case forall r. Num r => Var -> Expr r -> Maybe (r, Expr r)
LA.extractMaybe Var
x Expr Integer
e of
            Maybe (Integer, Expr Integer)
Nothing -> forall a. Set a
Set.empty
            Just (Integer
1, Expr Integer
_)   -> forall a. Set a
Set.empty -- IsPos e <=> (x + e' > 0) <=> -e' < x
            Just (-1, Expr Integer
e') -> forall a. a -> Set a
Set.singleton Expr Integer
e' -- IsPos e <=> (-x + e' > 0) <=>  x  < e'
            Maybe (Integer, Expr Integer)
_ -> forall a. HasCallStack => String -> a
error String
"should not happen"
        f (Divisible Bool
_ Integer
_ Expr Integer
_) = forall a. Set a
Set.empty

    -- formula1を真にする最小のxが存在しない場合
    case2 :: [(QFFormula, Witness)]
    case2 :: [(QFFormula, Witness)]
case2 = [(Var -> Expr Integer -> QFFormula -> QFFormula
subst1 Var
x (forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
j) QFFormula
formula2, Integer -> Integer -> Integer -> Set (Expr Integer) -> Witness
WCase2 Integer
c Integer
j Integer
delta Set (Expr Integer)
us) | Integer
j <- [Integer
1..Integer
delta]]

{-| @'projectCasesN' {x1,…,xm} φ@ returns @[(ψ_1, lift_1), …, (ψ_n, lift_n)]@ such that:

* @⊢_LIA ∀y1, …, yp. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_n)@ where @{y1, …, yp} = FV(φ) \\ {x1,…,xm}@, and

* if @M ⊧_LIA ψ_i@ then @lift_i M ⊧_LIA φ@.
-}
projectCasesN :: VarSet -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
projectCasesN :: VarSet
-> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
projectCasesN VarSet
vs2 = [Var] -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
f (VarSet -> [Var]
IS.toList VarSet
vs2)
  where
    f :: [Var] -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
    f :: [Var] -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
f [] QFFormula
formula = forall (m :: * -> *) a. Monad m => a -> m a
return (QFFormula
formula, forall a. a -> a
id)
    f (Var
v:[Var]
vs) QFFormula
formula = do
      (QFFormula
formula2, Model Integer -> Model Integer
mt1) <- Var -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
projectCases Var
v QFFormula
formula
      (QFFormula
formula3, Model Integer -> Model Integer
mt2) <- [Var] -> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
f [Var]
vs QFFormula
formula2
      forall (m :: * -> *) a. Monad m => a -> m a
return (QFFormula
formula3, Model Integer -> Model Integer
mt1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model Integer -> Model Integer
mt2)

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

newtype LCM a = LCM{ forall a. LCM a -> a
getLCM :: a }

instance Integral a => Semigroup.Semigroup (LCM a) where
  LCM a
a <> :: LCM a -> LCM a -> LCM a
<> LCM a
b = forall a. a -> LCM a
LCM forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> a -> a
lcm a
a a
b
  stimes :: forall b. Integral b => b -> LCM a -> LCM a
stimes = forall b a. Integral b => b -> a -> a
Semigroup.stimesIdempotent

instance Integral a => Monoid (LCM a) where
  mempty :: LCM a
mempty = forall a. a -> LCM a
LCM a
1

checkedDiv :: Integer -> Integer -> Integer
checkedDiv :: Integer -> Integer -> Integer
checkedDiv Integer
a Integer
b =
  case Integer
a forall a. Integral a => a -> a -> (a, a)
`divMod` Integer
b of
    (Integer
q,Integer
0) -> Integer
q
    (Integer, Integer)
_ -> forall a. HasCallStack => String -> a
error String
"ToySolver.Cooper.checkedDiv: should not happen"

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

-- | @'solveQFFormula' {x1,…,xn} φ@ returns @Just M@ that @M ⊧_LIA φ@ when
-- such @M@ exists, returns @Nothing@ otherwise.
--
-- @FV(φ)@ must be a subset of @{x1,…,xn}@.
--
solveQFFormula :: VarSet -> QFFormula -> Maybe (Model Integer)
solveQFFormula :: VarSet -> QFFormula -> Maybe (Model Integer)
solveQFFormula VarSet
vs QFFormula
formula = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ do
  (QFFormula
formula2, Model Integer -> Model Integer
mt) <- VarSet
-> QFFormula -> [(QFFormula, Model Integer -> Model Integer)]
projectCasesN VarSet
vs QFFormula
formula
  let m :: Model Integer
      m :: Model Integer
m = forall a. IntMap a
IM.empty
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall m e v. Eval m e v => m -> e -> v
eval Model Integer
m QFFormula
formula2
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Model Integer -> Model Integer
mt Model Integer
m

-- | @'solve' {x1,…,xn} φ@ returns @Just M@ that @M ⊧_LIA φ@ when
-- such @M@ exists, returns @Nothing@ otherwise.
--
-- @FV(φ)@ must be a subset of @{x1,…,xn}@.
--
solve :: VarSet -> [LA.Atom Rational] -> Maybe (Model Integer)
solve :: VarSet -> [Atom Rational] -> Maybe (Model Integer)
solve VarSet
vs [Atom Rational]
cs = VarSet -> QFFormula -> Maybe (Model Integer)
solveQFFormula VarSet
vs forall a b. (a -> b) -> a -> b
$ forall a. MonotoneBoolean a => [a] -> a
andB forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Atom Rational -> QFFormula
fromLAAtom [Atom Rational]
cs

-- | @'solveQFLIRAConj' {x1,…,xn} φ I@ returns @Just M@ that @M ⊧_LIRA φ@ when
-- such @M@ exists, returns @Nothing@ otherwise.
--
-- * @FV(φ)@ must be a subset of @{x1,…,xn}@.
--
-- * @I@ is a set of integer variables and must be a subset of @{x1,…,xn}@.
--
solveQFLIRAConj :: VarSet -> [LA.Atom Rational] -> VarSet -> Maybe (Model Rational)
solveQFLIRAConj :: VarSet -> [Atom Rational] -> VarSet -> Maybe (Model Rational)
solveQFLIRAConj VarSet
vs [Atom Rational]
cs VarSet
ivs = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ do
  ([Atom Rational]
cs2, Model Rational -> Model Rational
mt) <- VarSet
-> [Atom Rational]
-> [([Atom Rational], Model Rational -> Model Rational)]
FM.projectN VarSet
rvs [Atom Rational]
cs
  Model Integer
m <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ VarSet -> [Atom Rational] -> Maybe (Model Integer)
solve VarSet
ivs [Atom Rational]
cs2
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Model Rational -> Model Rational
mt forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map forall a. Num a => Integer -> a
fromInteger Model Integer
m
  where
    rvs :: VarSet
rvs = VarSet
vs VarSet -> VarSet -> VarSet
`IS.difference` VarSet
ivs

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

_testHagiya :: QFFormula
_testHagiya :: QFFormula
_testHagiya = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
project Var
1 forall a b. (a -> b) -> a -> b
$ forall a. MonotoneBoolean a => [a] -> a
andB [QFFormula
c1, QFFormula
c2, QFFormula
c3]
  where
    [Expr Integer
x,Expr Integer
y,Expr Integer
z] = forall a b. (a -> b) -> [a] -> [b]
map forall r. Num r => Var -> Expr r
LA.var [Var
1..Var
3]
    c1 :: QFFormula
c1 = Expr Integer
x forall e r. IsOrdRel e r => e -> e -> r
.<. (Expr Integer
y forall v. AdditiveGroup v => v -> v -> v
^+^ Expr Integer
y)
    c2 :: QFFormula
c2 = Expr Integer
z forall e r. IsOrdRel e r => e -> e -> r
.<. Expr Integer
x
    c3 :: QFFormula
c3 = Integer
3 Integer -> Expr Integer -> QFFormula
.|. Expr Integer
x

{-
∃ x. x < y+y ∧ z<x ∧ 3|x
⇔
(2y>z+1 ∧ 3|z+1) ∨ (2y>z+2 ∧ 3|z+2) ∨ (2y>z+3 ∧ 3|z+3)
-}

_test3 :: QFFormula
_test3 :: QFFormula
_test3 = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
project Var
1 forall a b. (a -> b) -> a -> b
$ forall a. MonotoneBoolean a => [a] -> a
andB [QFFormula
p1,QFFormula
p2,QFFormula
p3,QFFormula
p4]
  where
    x :: Expr Integer
x = forall r. Num r => Var -> Expr r
LA.var Var
0
    y :: Expr Integer
y = forall r. Num r => Var -> Expr r
LA.var Var
1
    p1 :: QFFormula
p1 = forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
0 forall e r. IsOrdRel e r => e -> e -> r
.<. Expr Integer
y
    p2 :: QFFormula
p2 = Integer
2 forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Integer
x forall e r. IsOrdRel e r => e -> e -> r
.<. Expr Integer
y
    p3 :: QFFormula
p3 = Expr Integer
y forall e r. IsOrdRel e r => e -> e -> r
.<. Expr Integer
x forall v. AdditiveGroup v => v -> v -> v
^+^ forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
2
    p4 :: QFFormula
p4 = Integer
2 Integer -> Expr Integer -> QFFormula
.|. Expr Integer
y

{-
∃ y. 0 < y ∧ 2x<y ∧ y < x+2 ∧ 2|y
⇔
(2x < 2 ∧ 0 < x) ∨ (0 < 2x+2 ∧ x < 0)
-}

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