{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE CPP #-}
{-# 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 (..)
    , evalLit
    , QFFormula
    , fromLAAtom
    , (.|.)
    , evalQFFormula
    , 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) = RelOp -> ExprZ -> ExprZ -> QFFormula
forall e r. IsOrdRel e r => RelOp -> e -> e -> r
ordRel RelOp
op ExprZ
a' ExprZ
b'
  where
    (ExprZ
e1,Integer
c1) = Expr Rational -> (ExprZ, Integer)
toRat Expr Rational
a
    (ExprZ
e2,Integer
c2) = Expr Rational -> (ExprZ, Integer)
toRat Expr Rational
b
    a' :: ExprZ
a' = Integer
Scalar ExprZ
c2 Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e1
    b' :: ExprZ
b' = Integer
Scalar ExprZ
c1 Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
e2

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

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

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

eqZ :: ExprZ -> ExprZ -> QFFormula
eqZ :: ExprZ -> ExprZ -> QFFormula
eqZ ExprZ
e1 ExprZ
e2 = Lit -> QFFormula
forall a. a -> BoolExpr a
Atom (ExprZ
e1 ExprZ -> ExprZ -> Lit
`leZ` ExprZ
e2) QFFormula -> QFFormula -> QFFormula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Lit -> QFFormula
forall a. a -> BoolExpr a
Atom (ExprZ
e1 ExprZ -> ExprZ -> Lit
`geZ` ExprZ
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
(Var -> Lit -> ShowS)
-> (Lit -> String) -> ([Lit] -> ShowS) -> Show Lit
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
(Lit -> Lit -> Bool) -> (Lit -> Lit -> Bool) -> Eq Lit
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
Eq Lit
-> (Lit -> Lit -> Ordering)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Lit)
-> (Lit -> Lit -> Lit)
-> Ord 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
$cp1Ord :: Eq Lit
Ord)

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

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

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

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

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

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

subst1 :: Var -> ExprZ -> QFFormula -> QFFormula
subst1 :: Var -> ExprZ -> QFFormula -> QFFormula
subst1 Var
x ExprZ
e = (Lit -> Lit) -> QFFormula -> QFFormula
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 ExprZ
e1) = Bool -> Integer -> ExprZ -> Lit
Divisible Bool
b Integer
c (ExprZ -> Lit) -> ExprZ -> Lit
forall a b. (a -> b) -> a -> b
$ Var -> ExprZ -> ExprZ -> ExprZ
forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
LA.applySubst1 Var
x ExprZ
e ExprZ
e1
    f (IsPos ExprZ
e1) = ExprZ -> Lit
IsPos (ExprZ -> Lit) -> ExprZ -> Lit
forall a b. (a -> b) -> a -> b
$ Var -> ExprZ -> ExprZ -> ExprZ
forall r. (Num r, Eq r) => Var -> Expr r -> Expr r -> Expr r
LA.applySubst1 Var
x ExprZ
e ExprZ
e1

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

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

{-# DEPRECATED evalQFFormula "Use Eval class instead" #-}
-- | @'evalQFFormula' M φ@ returns whether @M ⊧_LIA φ@ or not.
evalQFFormula :: Model Integer -> QFFormula -> Bool
evalQFFormula :: Model Integer -> QFFormula -> Bool
evalQFFormula = Model Integer -> QFFormula -> Bool
forall m e v. Eval m e v => m -> e -> v
eval

{-# DEPRECATED evalLit "Use Eval class instead" #-}
evalLit :: Model Integer -> Lit -> Bool
evalLit :: Model Integer -> Lit -> Bool
evalLit = Model Integer -> Lit -> Bool
forall m e v. Eval m e v => m -> e -> v
eval

instance Eval (Model Integer) Lit Bool where
  eval :: Model Integer -> Lit -> Bool
eval Model Integer
m (IsPos ExprZ
e) = Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
m ExprZ
e Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0
  eval Model Integer
m (Divisible Bool
True Integer
n ExprZ
e)  = Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
m ExprZ
e Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
  eval Model Integer
m (Divisible Bool
False Integer
n ExprZ
e) = Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
m ExprZ
e Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n Integer -> Integer -> Bool
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
(Var -> Witness -> ShowS)
-> (Witness -> String) -> ([Witness] -> ShowS) -> Show Witness
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 ExprZ
e) = Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
model ExprZ
e Integer -> Integer -> Integer
`checkedDiv` Integer
c
  eval Model Integer
model (WCase2 Integer
c Integer
j Integer
delta Set ExprZ
us)
    | Set Integer -> Bool
forall a. Set a -> Bool
Set.null Set Integer
us' = Integer
j Integer -> Integer -> Integer
`checkedDiv` Integer
c
    | Bool
otherwise = (Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (((Integer
u Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
delta Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
delta) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
delta)) Integer -> Integer -> Integer
`checkedDiv` Integer
c
    where
      us' :: Set Integer
us' = (ExprZ -> Integer) -> Set ExprZ -> Set Integer
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Model Integer -> ExprZ -> Integer
forall m e v. Eval m e v => m -> e -> v
LA.eval Model Integer
model) Set ExprZ
us
      u :: Integer
u = Set Integer -> Integer
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' = [QFFormula] -> QFFormula
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 = [Model Integer] -> Model Integer
forall a. [a] -> a
head ([Model Integer] -> Model Integer)
-> [Model Integer] -> Model Integer
forall a b. (a -> b) -> a -> b
$ do
      (QFFormula
phi, Model Integer -> Model Integer
mt') <- [(QFFormula, Model Integer -> Model Integer)]
xs
      Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Model Integer -> QFFormula -> Bool
forall m e v. Eval m e v => m -> e -> v
eval Model Integer
m QFFormula
phi
      Model Integer -> [Model Integer]
forall (m :: * -> *) a. Monad m => a -> m a
return (Model Integer -> [Model Integer])
-> Model Integer -> [Model Integer]
forall a b. (a -> b) -> a -> b
$ Model Integer -> Model Integer
mt' Model Integer
m
    orB' :: [BoolExpr a] -> BoolExpr a
orB' = [BoolExpr a] -> BoolExpr a
forall a. MonotoneBoolean a => [a] -> a
orB ([BoolExpr a] -> BoolExpr a)
-> ([BoolExpr a] -> [BoolExpr a]) -> [BoolExpr a] -> BoolExpr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BoolExpr a -> [BoolExpr a]) -> [BoolExpr a] -> [BoolExpr a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap BoolExpr a -> [BoolExpr a]
forall a. BoolExpr a -> [BoolExpr a]
f
      where
        f :: BoolExpr a -> [BoolExpr a]
f (Or [BoolExpr a]
xs) = (BoolExpr a -> [BoolExpr a]) -> [BoolExpr a] -> [BoolExpr a]
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, Model Integer -> Model Integer
forall a. a -> a
id)
    f (Var
v:[Var]
vs) QFFormula
formula = (QFFormula
formula3, Model Integer -> Model Integer
mt1 (Model Integer -> Model Integer)
-> (Model Integer -> Model Integer)
-> Model Integer
-> Model Integer
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
  (QFFormula, Model Integer -> Model Integer)
-> [(QFFormula, Model Integer -> Model Integer)]
forall (m :: * -> *) a. Monad m => a -> m a
return (QFFormula
phi, \Model Integer
m -> Var -> Integer -> Model Integer -> Model Integer
forall a. Var -> a -> IntMap a -> IntMap a
IM.insert Var
x (Model Integer -> Witness -> Integer
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 [(QFFormula, Witness)]
-> [(QFFormula, Witness)] -> [(QFFormula, Witness)]
forall a. [a] -> [a] -> [a]
++ [(QFFormula, Witness)]
case2, let phi' :: QFFormula
phi' = QFFormula -> QFFormula
simplify QFFormula
phi, QFFormula
phi' QFFormula -> QFFormula -> Bool
forall a. Eq a => a -> a -> Bool
/= QFFormula
forall a. MonotoneBoolean a => a
false]
  where
    -- eliminate Not, Imply and Equiv.
    formula0 :: QFFormula
    formula0 :: QFFormula
formula0 = QFFormula -> QFFormula
forall a. Complement a => BoolExpr a -> BoolExpr a
pos QFFormula
formula
      where
        pos :: BoolExpr a -> BoolExpr a
pos (Atom a
a) = a -> BoolExpr a
forall a. a -> BoolExpr a
Atom a
a
        pos (And [BoolExpr a]
xs) = [BoolExpr a] -> BoolExpr a
forall a. [BoolExpr a] -> BoolExpr a
And ((BoolExpr a -> BoolExpr a) -> [BoolExpr a] -> [BoolExpr a]
forall a b. (a -> b) -> [a] -> [b]
map BoolExpr a -> BoolExpr a
pos [BoolExpr a]
xs)
        pos (Or [BoolExpr a]
xs) = [BoolExpr a] -> BoolExpr a
forall a. [BoolExpr a] -> BoolExpr a
Or ((BoolExpr a -> BoolExpr a) -> [BoolExpr a] -> [BoolExpr a]
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 BoolExpr a -> BoolExpr a -> BoolExpr a
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 BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
y) BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. MonotoneBoolean a => a -> a -> a
.&&. (BoolExpr a
y BoolExpr a -> BoolExpr a -> BoolExpr a
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 BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
t) BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. MonotoneBoolean a => a -> a -> a
.&&. (BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a
Not BoolExpr a
c BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
e))

        neg :: BoolExpr a -> BoolExpr a
neg (Atom a
a) = a -> BoolExpr a
forall a. a -> BoolExpr a
Atom (a -> a
forall a. Complement a => a -> a
notB a
a)
        neg (And [BoolExpr a]
xs) = [BoolExpr a] -> BoolExpr a
forall a. [BoolExpr a] -> BoolExpr a
Or ((BoolExpr a -> BoolExpr a) -> [BoolExpr a] -> [BoolExpr a]
forall a b. (a -> b) -> [a] -> [b]
map BoolExpr a -> BoolExpr a
neg [BoolExpr a]
xs)
        neg (Or [BoolExpr a]
xs) = [BoolExpr a] -> BoolExpr a
forall a. [BoolExpr a] -> BoolExpr a
And ((BoolExpr a -> BoolExpr a) -> [BoolExpr a] -> [BoolExpr a]
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 BoolExpr a -> BoolExpr a -> BoolExpr a
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 BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
y) BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. MonotoneBoolean a => a -> a -> a
.&&. (BoolExpr a
y BoolExpr a -> BoolExpr a -> BoolExpr a
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 BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
t) BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. MonotoneBoolean a => a -> a -> a
.&&. (BoolExpr a -> BoolExpr a
forall a. BoolExpr a -> BoolExpr a
Not BoolExpr a
c BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. Boolean a => a -> a -> a
.=>. BoolExpr a
e))

    -- xの係数の最小公倍数
    c :: Integer
    c :: Integer
c = LCM Integer -> Integer
forall a. LCM a -> a
getLCM (LCM Integer -> Integer) -> LCM Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Lit -> LCM Integer) -> QFFormula -> LCM Integer
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 ExprZ
e) = Integer -> LCM Integer
forall a. a -> LCM a
LCM (Integer -> LCM Integer) -> Integer -> LCM Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe Integer
1 (Var -> ExprZ -> Maybe Integer
forall r. Num r => Var -> Expr r -> Maybe r
LA.lookupCoeff Var
x ExprZ
e)
         f (Divisible Bool
_ Integer
_ ExprZ
e) = Integer -> LCM Integer
forall a. a -> LCM a
LCM (Integer -> LCM Integer) -> Integer -> LCM Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe Integer
1 (Var -> ExprZ -> Maybe Integer
forall r. Num r => Var -> Expr r -> Maybe r
LA.lookupCoeff Var
x ExprZ
e)

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

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

    -- d|x+t という形の論理式の d の最小公倍数
    delta :: Integer
    delta :: Integer
delta = LCM Integer -> Integer
forall a. LCM a -> a
getLCM (LCM Integer -> Integer) -> LCM Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Lit -> LCM Integer) -> QFFormula -> LCM Integer
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 ExprZ
_) = Integer -> LCM Integer
forall a. a -> LCM a
LCM Integer
d
        f (IsPos ExprZ
_) = Integer -> LCM Integer
forall a. a -> LCM a
LCM Integer
1

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

    -- formula1を真にする最小のxが存在する場合
    case1 :: [(QFFormula, Witness)]
    case1 :: [(QFFormula, Witness)]
case1 = [ (Var -> ExprZ -> QFFormula -> QFFormula
subst1 Var
x ExprZ
e QFFormula
formula1, Integer -> ExprZ -> Witness
WCase1 Integer
c ExprZ
e)
            | Integer
j <- [Integer
1..Integer
delta], ExprZ
t <- Set ExprZ -> [ExprZ]
forall a. Set a -> [a]
Set.toList Set ExprZ
ts, let e :: ExprZ
e = ExprZ
t ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^+^ Integer -> ExprZ
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 (QFFormula -> QFFormula) -> QFFormula -> QFFormula
forall a b. (a -> b) -> a -> b
$ (Lit -> QFFormula) -> QFFormula -> QFFormula
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 ExprZ
e) =
          case Var -> ExprZ -> Maybe Integer
forall r. Num r => Var -> Expr r -> Maybe r
LA.lookupCoeff Var
x ExprZ
e of
            Maybe Integer
Nothing -> Lit -> QFFormula
forall a. a -> BoolExpr a
Atom Lit
lit
            Just Integer
1    -> QFFormula
forall a. MonotoneBoolean a => a
false -- IsPos e <=> ( x + e' > 0) <=> -e' < x
            Just (-1) -> QFFormula
forall a. MonotoneBoolean a => a
true  -- IsPos e <=> (-x + e' > 0) <=>  x  < e'
            Maybe Integer
_ -> String -> QFFormula
forall a. HasCallStack => String -> a
error String
"should not happen"
        f lit :: Lit
lit@(Divisible Bool
_ Integer
_ ExprZ
_) = Lit -> QFFormula
forall a. a -> BoolExpr a
Atom Lit
lit

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

    -- formula1を真にする最小のxが存在しない場合
    case2 :: [(QFFormula, Witness)]
    case2 :: [(QFFormula, Witness)]
case2 = [(Var -> ExprZ -> QFFormula -> QFFormula
subst1 Var
x (Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
j) QFFormula
formula2, Integer -> Integer -> Integer -> Set ExprZ -> Witness
WCase2 Integer
c Integer
j Integer
delta Set ExprZ
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 = (QFFormula, Model Integer -> Model Integer)
-> [(QFFormula, Model Integer -> Model Integer)]
forall (m :: * -> *) a. Monad m => a -> m a
return (QFFormula
formula, Model Integer -> Model Integer
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
      (QFFormula, Model Integer -> Model Integer)
-> [(QFFormula, Model Integer -> Model Integer)]
forall (m :: * -> *) a. Monad m => a -> m a
return (QFFormula
formula3, Model Integer -> Model Integer
mt1 (Model Integer -> Model Integer)
-> (Model Integer -> Model Integer)
-> Model Integer
-> Model Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model Integer -> Model Integer
mt2)

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

newtype LCM a = LCM{ 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 = a -> LCM a
forall a. a -> LCM a
LCM (a -> LCM a) -> a -> LCM a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Integral a => a -> a -> a
lcm a
a a
b
  stimes :: b -> LCM a -> LCM a
stimes = b -> LCM a -> LCM a
forall b a. Integral b => b -> a -> a
Semigroup.stimesIdempotent

instance Integral a => Monoid (LCM a) where
  mempty :: LCM a
mempty = a -> LCM a
forall a. a -> LCM a
LCM a
1
#if !(MIN_VERSION_base(4,11,0))
  mappend = (Semigroup.<>)
#endif

checkedDiv :: Integer -> Integer -> Integer
checkedDiv :: Integer -> Integer -> Integer
checkedDiv Integer
a Integer
b =
  case Integer
a Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Integer
b of
    (Integer
q,Integer
0) -> Integer
q
    (Integer, Integer)
_ -> String -> 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 = [Model Integer] -> Maybe (Model Integer)
forall a. [a] -> Maybe a
listToMaybe ([Model Integer] -> Maybe (Model Integer))
-> [Model Integer] -> Maybe (Model Integer)
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 = Model Integer
forall a. IntMap a
IM.empty
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Model Integer -> QFFormula -> Bool
forall m e v. Eval m e v => m -> e -> v
eval Model Integer
m QFFormula
formula2
  Model Integer -> [Model Integer]
forall (m :: * -> *) a. Monad m => a -> m a
return (Model Integer -> [Model Integer])
-> Model Integer -> [Model Integer]
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 (QFFormula -> Maybe (Model Integer))
-> QFFormula -> Maybe (Model Integer)
forall a b. (a -> b) -> a -> b
$ [QFFormula] -> QFFormula
forall a. MonotoneBoolean a => [a] -> a
andB ([QFFormula] -> QFFormula) -> [QFFormula] -> QFFormula
forall a b. (a -> b) -> a -> b
$ (Atom Rational -> QFFormula) -> [Atom Rational] -> [QFFormula]
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 = [Model Rational] -> Maybe (Model Rational)
forall a. [a] -> Maybe a
listToMaybe ([Model Rational] -> Maybe (Model Rational))
-> [Model Rational] -> Maybe (Model Rational)
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 <- Maybe (Model Integer) -> [Model Integer]
forall a. Maybe a -> [a]
maybeToList (Maybe (Model Integer) -> [Model Integer])
-> Maybe (Model Integer) -> [Model Integer]
forall a b. (a -> b) -> a -> b
$ VarSet -> [Atom Rational] -> Maybe (Model Integer)
solve VarSet
ivs [Atom Rational]
cs2
  Model Rational -> [Model Rational]
forall (m :: * -> *) a. Monad m => a -> m a
return (Model Rational -> [Model Rational])
-> Model Rational -> [Model Rational]
forall a b. (a -> b) -> a -> b
$ Model Rational -> Model Rational
mt (Model Rational -> Model Rational)
-> Model Rational -> Model Rational
forall a b. (a -> b) -> a -> b
$ (Integer -> Rational) -> Model Integer -> Model Rational
forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map Integer -> Rational
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 = (QFFormula, Model Integer -> Model Integer) -> QFFormula
forall a b. (a, b) -> a
fst ((QFFormula, Model Integer -> Model Integer) -> QFFormula)
-> (QFFormula, Model Integer -> Model Integer) -> QFFormula
forall a b. (a -> b) -> a -> b
$ Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
project Var
1 (QFFormula -> (QFFormula, Model Integer -> Model Integer))
-> QFFormula -> (QFFormula, Model Integer -> Model Integer)
forall a b. (a -> b) -> a -> b
$ [QFFormula] -> QFFormula
forall a. MonotoneBoolean a => [a] -> a
andB [QFFormula
c1, QFFormula
c2, QFFormula
c3]
  where
    [ExprZ
x,ExprZ
y,ExprZ
z] = (Var -> ExprZ) -> [Var] -> [ExprZ]
forall a b. (a -> b) -> [a] -> [b]
map Var -> ExprZ
forall r. Num r => Var -> Expr r
LA.var [Var
1..Var
3]
    c1 :: QFFormula
c1 = ExprZ
x ExprZ -> ExprZ -> QFFormula
forall e r. IsOrdRel e r => e -> e -> r
.<. (ExprZ
y ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^+^ ExprZ
y)
    c2 :: QFFormula
c2 = ExprZ
z ExprZ -> ExprZ -> QFFormula
forall e r. IsOrdRel e r => e -> e -> r
.<. ExprZ
x
    c3 :: QFFormula
c3 = Integer
3 Integer -> ExprZ -> QFFormula
.|. ExprZ
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 = (QFFormula, Model Integer -> Model Integer) -> QFFormula
forall a b. (a, b) -> a
fst ((QFFormula, Model Integer -> Model Integer) -> QFFormula)
-> (QFFormula, Model Integer -> Model Integer) -> QFFormula
forall a b. (a -> b) -> a -> b
$ Var -> QFFormula -> (QFFormula, Model Integer -> Model Integer)
project Var
1 (QFFormula -> (QFFormula, Model Integer -> Model Integer))
-> QFFormula -> (QFFormula, Model Integer -> Model Integer)
forall a b. (a -> b) -> a -> b
$ [QFFormula] -> QFFormula
forall a. MonotoneBoolean a => [a] -> a
andB [QFFormula
p1,QFFormula
p2,QFFormula
p3,QFFormula
p4]
  where
    x :: ExprZ
x = Var -> ExprZ
forall r. Num r => Var -> Expr r
LA.var Var
0
    y :: ExprZ
y = Var -> ExprZ
forall r. Num r => Var -> Expr r
LA.var Var
1
    p1 :: QFFormula
p1 = Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
0 ExprZ -> ExprZ -> QFFormula
forall e r. IsOrdRel e r => e -> e -> r
.<. ExprZ
y
    p2 :: QFFormula
p2 = Scalar ExprZ
2 Scalar ExprZ -> ExprZ -> ExprZ
forall v. VectorSpace v => Scalar v -> v -> v
*^ ExprZ
x ExprZ -> ExprZ -> QFFormula
forall e r. IsOrdRel e r => e -> e -> r
.<. ExprZ
y
    p3 :: QFFormula
p3 = ExprZ
y ExprZ -> ExprZ -> QFFormula
forall e r. IsOrdRel e r => e -> e -> r
.<. ExprZ
x ExprZ -> ExprZ -> ExprZ
forall v. AdditiveGroup v => v -> v -> v
^+^ Integer -> ExprZ
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Integer
2
    p4 :: QFFormula
p4 = Integer
2 Integer -> ExprZ -> QFFormula
.|. ExprZ
y

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

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