{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.QBF
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Reference:
--
-- * Mikoláš Janota, William Klieber, Joao Marques-Silva, Edmund Clarke.
--   Solving QBF with Counterexample Guided Refinement.
--   In Theory and Applications of Satisfiability Testing (SAT 2012), pp. 114-128.
--   <https://doi.org/10.1007/978-3-642-31612-8_10>
--   <https://www.cs.cmu.edu/~wklieber/papers/qbf-cegar-sat-2012.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.QBF
  ( Quantifier (..)
  , Prefix
  , normalizePrefix
  , quantifyFreeVariables
  , Matrix
  , solve
  , solveNaive
  , solveCEGAR
  , solveCEGARIncremental
  , solveQE
  , solveQE_CNF
  ) where

import Control.Monad
import Control.Monad.State.Strict
import Control.Monad.Trans.Except
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.Function (on)
import Data.List (groupBy, foldl')
import Data.Maybe

import ToySolver.Data.Boolean
import ToySolver.Data.BoolExpr (BoolExpr)
import qualified ToySolver.Data.BoolExpr as BoolExpr
import ToySolver.FileFormat.CNF (Quantifier (..))
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types (LitSet, VarSet, VarMap)
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Store.CNF

import qualified ToySolver.SAT.ExistentialQuantification as QE

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

type Prefix = [(Quantifier, VarSet)]

normalizePrefix :: Prefix -> Prefix
normalizePrefix :: Prefix -> Prefix
normalizePrefix = Prefix -> Prefix
groupQuantifiers (Prefix -> Prefix) -> (Prefix -> Prefix) -> Prefix -> Prefix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prefix -> Prefix
removeEmptyQuantifiers

removeEmptyQuantifiers :: Prefix -> Prefix
removeEmptyQuantifiers :: Prefix -> Prefix
removeEmptyQuantifiers = ((Quantifier, IntSet) -> Bool) -> Prefix -> Prefix
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Quantifier
_,IntSet
xs) -> Bool -> Bool
not (IntSet -> Bool
IntSet.null IntSet
xs))

groupQuantifiers :: Prefix -> Prefix
groupQuantifiers :: Prefix -> Prefix
groupQuantifiers = (Prefix -> (Quantifier, IntSet)) -> [Prefix] -> Prefix
forall a b. (a -> b) -> [a] -> [b]
map Prefix -> (Quantifier, IntSet)
forall a. [(a, IntSet)] -> (a, IntSet)
f ([Prefix] -> Prefix) -> (Prefix -> [Prefix]) -> Prefix -> Prefix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Quantifier, IntSet) -> (Quantifier, IntSet) -> Bool)
-> Prefix -> [Prefix]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Quantifier -> Quantifier -> Bool)
-> ((Quantifier, IntSet) -> Quantifier)
-> (Quantifier, IntSet)
-> (Quantifier, IntSet)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Quantifier, IntSet) -> Quantifier
forall a b. (a, b) -> a
fst)
  where
    f :: [(a, IntSet)] -> (a, IntSet)
f [(a, IntSet)]
qs = ((a, IntSet) -> a
forall a b. (a, b) -> a
fst ([(a, IntSet)] -> (a, IntSet)
forall a. [a] -> a
head [(a, IntSet)]
qs), [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [IntSet
xs | (a
_,IntSet
xs) <- [(a, IntSet)]
qs])

quantifyFreeVariables :: Int -> Prefix -> Prefix
quantifyFreeVariables :: Int -> Prefix -> Prefix
quantifyFreeVariables Int
nv Prefix
prefix
  | IntSet -> Bool
IntSet.null IntSet
rest = Prefix
prefix
  | Bool
otherwise = (Quantifier
E, IntSet
rest) (Quantifier, IntSet) -> Prefix -> Prefix
forall a. a -> [a] -> [a]
: Prefix
prefix
  where
    rest :: IntSet
rest = [Int] -> IntSet
IntSet.fromList [Int
1..Int
nv] IntSet -> IntSet -> IntSet
`IntSet.difference` [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [IntSet
vs | (Quantifier
_q, IntSet
vs) <- Prefix
prefix]

prefixStartWithA :: Prefix -> Bool
prefixStartWithA :: Prefix -> Bool
prefixStartWithA ((Quantifier
A,IntSet
_) : Prefix
_) = Bool
True
prefixStartWithA Prefix
_ = Bool
False

prefixStartWithE :: Prefix -> Bool
prefixStartWithE :: Prefix -> Bool
prefixStartWithE ((Quantifier
E,IntSet
_) : Prefix
_) = Bool
True
prefixStartWithE Prefix
_ = Bool
False

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

type Matrix = BoolExpr SAT.Lit

reduct :: Matrix -> LitSet -> Matrix
reduct :: Matrix -> IntSet -> Matrix
reduct Matrix
m IntSet
ls = Matrix -> Matrix
forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify (Matrix -> Matrix) -> Matrix -> Matrix
forall a b. (a -> b) -> a -> b
$ Matrix
m Matrix -> (Int -> Matrix) -> Matrix
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> Matrix
s
  where
    s :: Int -> Matrix
s Int
l
      |   Int
l  Int -> IntSet -> Bool
`IntSet.member` IntSet
ls = Matrix
forall a. MonotoneBoolean a => a
true
      | (-Int
l) Int -> IntSet -> Bool
`IntSet.member` IntSet
ls = Matrix
forall a. MonotoneBoolean a => a
false
      | Bool
otherwise = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
l

substVarMap :: Matrix -> VarMap Matrix -> Matrix
substVarMap :: Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
m VarMap Matrix
s = Matrix -> Matrix
forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify (Matrix -> Matrix) -> Matrix -> Matrix
forall a b. (a -> b) -> a -> b
$ Matrix
m Matrix -> (Int -> Matrix) -> Matrix
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
l -> do
  let v :: Int
v = Int -> Int
forall a. Num a => a -> a
abs Int
l
  (if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Matrix -> Matrix
forall a. a -> a
id else Matrix -> Matrix
forall a. Complement a => a -> a
notB) (Matrix -> Matrix) -> Matrix -> Matrix
forall a b. (a -> b) -> a -> b
$ Matrix -> Int -> VarMap Matrix -> Matrix
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault (Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
v) Int
v VarMap Matrix
s

-- XXX
prenexAnd :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd :: (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (Int
nv1, Prefix
prefix1, Matrix
matrix1) (Int
nv2, Prefix
prefix2, Matrix
matrix2) =
  State Int (Int, Prefix, Matrix) -> Int -> (Int, Prefix, Matrix)
forall s a. State s a -> s -> a
evalState (Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f [] IntSet
IntSet.empty VarMap Matrix
forall a. IntMap a
IntMap.empty VarMap Matrix
forall a. IntMap a
IntMap.empty Prefix
prefix1 Prefix
prefix2) (Int
nv1 Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
nv2)
  where
    f :: Prefix -> VarSet
      -> VarMap (BoolExpr SAT.Lit) -> VarMap (BoolExpr SAT.Lit)
      -> Prefix -> Prefix
      -> State Int (Int, Prefix, Matrix)
    f :: Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f Prefix
prefix IntSet
_bvs VarMap Matrix
subst1 VarMap Matrix
subst2 [] [] = do
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      (Int, Prefix, Matrix) -> State Int (Int, Prefix, Matrix)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nv, Prefix
prefix, Matrix -> Matrix
forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify (Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
matrix1 VarMap Matrix
subst1 Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.&&. Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
matrix2 VarMap Matrix
subst2))
    f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 ((Quantifier
A,IntSet
xs1) : Prefix
prefix1') ((Quantifier
A,IntSet
xs2) : Prefix
prefix2') = do
      let xs :: IntSet
xs = IntSet -> IntSet -> IntSet
IntSet.union IntSet
xs1 IntSet
xs2
          ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
      let s :: IntMap Int
s  = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Matrix
subst1' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
xs1) IntMap Int
s) VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst1
          subst2' :: VarMap Matrix
subst2' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
xs2) IntMap Int
s) VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst2
      Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
A, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1' VarMap Matrix
subst2' Prefix
prefix1' Prefix
prefix2'
    f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 ((Quantifier
q,IntSet
xs) : Prefix
prefix1') Prefix
prefix2 | Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
E Bool -> Bool -> Bool
|| Bool -> Bool
not (Prefix -> Bool
prefixStartWithE Prefix
prefix2) = do
      let ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
      let s :: IntMap Int
s  = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Matrix
subst1' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom IntMap Int
s VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst1
      Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1' VarMap Matrix
subst2 Prefix
prefix1' Prefix
prefix2
    f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 Prefix
prefix1 ((Quantifier
q,IntSet
xs) : Prefix
prefix2')  = do
      let ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
      let s :: IntMap Int
s  = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst2' :: VarMap Matrix
subst2' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom IntMap Int
s VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst2
      Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1 VarMap Matrix
subst2' Prefix
prefix1 Prefix
prefix2'

-- XXX
prenexOr :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr :: (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (Int
nv1, Prefix
prefix1, Matrix
matrix1) (Int
nv2, Prefix
prefix2, Matrix
matrix2) =
  State Int (Int, Prefix, Matrix) -> Int -> (Int, Prefix, Matrix)
forall s a. State s a -> s -> a
evalState (Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f [] IntSet
IntSet.empty VarMap Matrix
forall a. IntMap a
IntMap.empty VarMap Matrix
forall a. IntMap a
IntMap.empty Prefix
prefix1 Prefix
prefix2) (Int
nv1 Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
nv2)
  where
    f :: Prefix -> VarSet
      -> VarMap (BoolExpr SAT.Lit) -> VarMap (BoolExpr SAT.Lit)
      -> Prefix -> Prefix
      -> State Int (Int, Prefix, Matrix)
    f :: Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f Prefix
prefix IntSet
_bvs VarMap Matrix
subst1 VarMap Matrix
subst2 [] [] = do
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      (Int, Prefix, Matrix) -> State Int (Int, Prefix, Matrix)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nv, Prefix
prefix, Matrix -> Matrix
forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify (Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
matrix1 VarMap Matrix
subst1 Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.||. Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
matrix2 VarMap Matrix
subst2))
    f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 ((Quantifier
E,IntSet
xs1) : Prefix
prefix1') ((Quantifier
E,IntSet
xs2) : Prefix
prefix2') = do
      let xs :: IntSet
xs = IntSet -> IntSet -> IntSet
IntSet.union IntSet
xs1 IntSet
xs2
          ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
      let s :: IntMap Int
s  = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Matrix
subst1' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
xs1) IntMap Int
s) VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst1
          subst2' :: VarMap Matrix
subst2' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
xs2) IntMap Int
s) VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst2
      Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
A, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1' VarMap Matrix
subst2' Prefix
prefix1' Prefix
prefix2'
    f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 ((Quantifier
q,IntSet
xs) : Prefix
prefix1') Prefix
prefix2 | Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
A Bool -> Bool -> Bool
|| Bool -> Bool
not (Prefix -> Bool
prefixStartWithA Prefix
prefix2)= do
      let ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
      let s :: IntMap Int
s  = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Matrix
subst1' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom IntMap Int
s VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst1
      Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1' VarMap Matrix
subst2 Prefix
prefix1' Prefix
prefix2
    f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 Prefix
prefix1 ((Quantifier
q,IntSet
xs) : Prefix
prefix2')  = do
      let ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
      let s :: IntMap Int
s  = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst2' :: VarMap Matrix
subst2' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom IntMap Int
s VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst2
      Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1 VarMap Matrix
subst2' Prefix
prefix1 Prefix
prefix2'

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

solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solve = Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveCEGARIncremental

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

-- | Naive Algorithm for a Winning Move
solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveNaive Int
nv Prefix
prefix Matrix
matrix =
  case Prefix
prefix' of
    [] -> if (Int -> Bool) -> Matrix -> Bool
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Int -> Bool
forall a. HasCallStack => a
undefined Matrix
matrix
          then (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
IntSet.empty)
          else (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe IntSet
forall a. Maybe a
Nothing)
    (Quantifier
E,IntSet
_) : Prefix
_ -> do
      Maybe IntSet
m <- Prefix -> Matrix -> IO (Maybe IntSet)
f Prefix
prefix' Matrix
matrix
      (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe IntSet
m, Maybe IntSet
m)
    (Quantifier
A,IntSet
_) : Prefix
_ -> do
      Maybe IntSet
m <- Prefix -> Matrix -> IO (Maybe IntSet)
f Prefix
prefix' Matrix
matrix
      (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe IntSet
m, Maybe IntSet
m)
  where
    prefix' :: Prefix
prefix' = Prefix -> Prefix
normalizePrefix Prefix
prefix

    {- Naive Algorithm for a Winning Move
    Function Solve (QX. Φ)
    begin
      if Φ has no quant then
        return (Q = ∃) ? SAT(φ) : SAT(¬φ)
      Λ ← {true, false}^X  // consider all assignments
      while true do
        if Λ = ∅ then      // all assignments used up
          return NULL
        τ ← pick(Λ)        // pick a candidate solution
        μ ← Solve(Φ[τ])    // find a countermove
        if μ = NULL then   // winning move
          return τ
        Λ ← Λ \ {τ}        // remove bad candidate
      end
    end
    -}
    f :: Prefix -> Matrix -> IO (Maybe LitSet)
    f :: Prefix -> Matrix -> IO (Maybe IntSet)
f [] Matrix
_matrix = [Char] -> IO (Maybe IntSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
    f [(Quantifier
q,IntSet
xs)] Matrix
matrix = do
      Solver
solver <- IO Solver
SAT.newSolver
      Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
      Encoder IO
enc <- Solver -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
      case Quantifier
q of
        Quantifier
E -> Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc Matrix
matrix
        Quantifier
A -> Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc (Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
matrix)
      Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
      if Bool
ret then do
        Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
        Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> IO (Maybe IntSet))
-> Maybe IntSet -> IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]
      else
        Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
    f ((Quantifier
_q,IntSet
xs) : Prefix
prefix') Matrix
matrix = do
      Either IntSet ()
ret <- ExceptT IntSet IO () -> IO (Either IntSet ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT IntSet IO () -> IO (Either IntSet ()))
-> ExceptT IntSet IO () -> IO (Either IntSet ())
forall a b. (a -> b) -> a -> b
$ do
        let moves :: [LitSet]
            moves :: [IntSet]
moves = ([Int] -> IntSet) -> [[Int]] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> IntSet
IntSet.fromList ([[Int]] -> [IntSet]) -> [[Int]] -> [IntSet]
forall a b. (a -> b) -> a -> b
$ [[Int]] -> [[Int]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[Int
x, -Int
x] | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]
        [IntSet]
-> (IntSet -> ExceptT IntSet IO ()) -> ExceptT IntSet IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [IntSet]
moves ((IntSet -> ExceptT IntSet IO ()) -> ExceptT IntSet IO ())
-> (IntSet -> ExceptT IntSet IO ()) -> ExceptT IntSet IO ()
forall a b. (a -> b) -> a -> b
$ \IntSet
tau -> do
          Maybe IntSet
ret <- IO (Maybe IntSet) -> ExceptT IntSet IO (Maybe IntSet)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe IntSet) -> ExceptT IntSet IO (Maybe IntSet))
-> IO (Maybe IntSet) -> ExceptT IntSet IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ Prefix -> Matrix -> IO (Maybe IntSet)
f Prefix
prefix' (Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
tau)
          case Maybe IntSet
ret of
            Maybe IntSet
Nothing  -> IntSet -> ExceptT IntSet IO ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE IntSet
tau
            Just IntSet
_nu -> () -> ExceptT IntSet IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      case Either IntSet ()
ret of
        Left IntSet
tau -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
tau)
        Right () -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing

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

-- | Abstraction-Based Algorithm for a Winning Move
solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveCEGAR Int
nv Prefix
prefix Matrix
matrix =
  case Prefix
prefix' of
    [] -> if (Int -> Bool) -> Matrix -> Bool
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Int -> Bool
forall a. HasCallStack => a
undefined Matrix
matrix
          then (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
IntSet.empty)
          else (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe IntSet
forall a. Maybe a
Nothing)
    (Quantifier
E,IntSet
_) : Prefix
_ -> do
      Maybe IntSet
m <- Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv Prefix
prefix' Matrix
matrix
      (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe IntSet
m, Maybe IntSet
m)
    (Quantifier
A,IntSet
_) : Prefix
_ -> do
      Maybe IntSet
m <- Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv Prefix
prefix' Matrix
matrix
      (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe IntSet
m, Maybe IntSet
m)
  where
    prefix' :: Prefix
prefix' = Prefix -> Prefix
normalizePrefix Prefix
prefix

    {-
    Function Solve (QX. Φ)
    begin
      if Φ has no quant then
        return (Q = ∃) ? SAT(φ) : SAT(¬φ)
      ω ← ∅
      while true do
        α ← (Q = ∃) ? ∧_{μ∈ω} Φ[μ] : ∨_{μ∈ω} Φ[μ] // abstraction
        τ' ← Solve(Prenex(QX.α)) // find a candidate
        if τ' = NULL then return NULL // no winning move
        τ ← {l | l ∈ τ′ ∧ var(l) ∈ X} // filter a move for X
        μ ← Solve(Φ[τ])
        if μ = NULL then return τ
        ω ← ω∪{μ}
      end
    end
    -}
    f :: Int -> Prefix -> Matrix -> IO (Maybe LitSet)
    f :: Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
_nv [] Matrix
_matrix = [Char] -> IO (Maybe IntSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
    f Int
nv [(Quantifier
q,IntSet
xs)] Matrix
matrix = do
      Solver
solver <- IO Solver
SAT.newSolver
      Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
      Encoder IO
enc <- Solver -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
      case Quantifier
q of
        Quantifier
E -> Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc Matrix
matrix
        Quantifier
A -> Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc (Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
matrix)
      Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
      if Bool
ret then do
        Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
        Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> IO (Maybe IntSet))
-> Maybe IntSet -> IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]
      else
        Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
    f Int
nv ((Quantifier
q,IntSet
xs) : prefix' :: Prefix
prefix'@((Quantifier
_q2,IntSet
_) : Prefix
prefix'')) Matrix
matrix = do
      let loop :: [IntSet] -> IO (Maybe IntSet)
loop [IntSet]
counterMoves = do
            let ys :: [(Int, Prefix, Matrix)]
ys = [(Int
nv, Prefix
prefix'', Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
nu) | IntSet
nu <- [IntSet]
counterMoves]
                (Int
nv2, Prefix
prefix2, Matrix
matrix2) =
                  if Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
E
                  then ((Int, Prefix, Matrix)
 -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix))
-> (Int, Prefix, Matrix)
-> [(Int, Prefix, Matrix)]
-> (Int, Prefix, Matrix)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (Int
nv,[],Matrix
forall a. MonotoneBoolean a => a
true) [(Int, Prefix, Matrix)]
ys
                  else ((Int, Prefix, Matrix)
 -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix))
-> (Int, Prefix, Matrix)
-> [(Int, Prefix, Matrix)]
-> (Int, Prefix, Matrix)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (Int
nv,[],Matrix
forall a. MonotoneBoolean a => a
false) [(Int, Prefix, Matrix)]
ys
            Maybe IntSet
ret <- Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv2 (Prefix -> Prefix
normalizePrefix ((Quantifier
q,IntSet
xs) (Quantifier, IntSet) -> Prefix -> Prefix
forall a. a -> [a] -> [a]
: Prefix
prefix2)) Matrix
matrix2
            case Maybe IntSet
ret of
              Maybe IntSet
Nothing -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
              Just IntSet
tau' -> do
                let tau :: IntSet
tau = (Int -> Bool) -> IntSet -> IntSet
IntSet.filter (\Int
l -> Int -> Int
forall a. Num a => a -> a
abs Int
l Int -> IntSet -> Bool
`IntSet.member` IntSet
xs) IntSet
tau'
                Maybe IntSet
ret2 <- Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv Prefix
prefix' (Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
tau)
                case Maybe IntSet
ret2 of
                  Maybe IntSet
Nothing -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
tau)
                  Just IntSet
nu -> [IntSet] -> IO (Maybe IntSet)
loop (IntSet
nu IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: [IntSet]
counterMoves)
      [IntSet] -> IO (Maybe IntSet)
loop []

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

-- | Abstraction-Based Algorithm for a Winning Move
solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveCEGARIncremental Int
nv Prefix
prefix Matrix
matrix =
  case Prefix
prefix' of
    [] -> if (Int -> Bool) -> Matrix -> Bool
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Int -> Bool
forall a. HasCallStack => a
undefined Matrix
matrix
          then (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
IntSet.empty)
          else (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe IntSet
forall a. Maybe a
Nothing)
    (Quantifier
E,IntSet
_) : Prefix
_ -> do
      Maybe IntSet
m <- Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv IntSet
IntSet.empty Prefix
prefix' Matrix
matrix
      (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe IntSet
m, Maybe IntSet
m)
    (Quantifier
A,IntSet
_) : Prefix
_ -> do
      Maybe IntSet
m <- Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv IntSet
IntSet.empty Prefix
prefix' Matrix
matrix
      (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe IntSet
m, Maybe IntSet
m)
  where
    prefix' :: Prefix
prefix' = Prefix -> Prefix
normalizePrefix Prefix
prefix

    {-
    Function Solve (QX. Φ)
    begin
      if Φ has no quant then
        return (Q = ∃) ? SAT(φ) : SAT(¬φ)
      ω ← ∅
      while true do
        α ← (Q = ∃) ? ∧_{μ∈ω} Φ[μ] : ∨_{μ∈ω} Φ[μ] // abstraction
        τ' ← Solve(Prenex(QX.α)) // find a candidate
        if τ' = NULL then return NULL // no winning move
        τ ← {l | l ∈ τ′ ∧ var(l) ∈ X} // filter a move for X
        μ ← Solve(Φ[τ])
        if μ = NULL then return τ
        ω ← ω∪{μ}
      end
    end
    -}
    f :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
    f :: Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv IntSet
_assumptions Prefix
prefix Matrix
matrix = do
      Solver
solver <- IO Solver
SAT.newSolver
      Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
      Encoder IO
enc <- Solver -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
      IntSet
_xs <-
        case Prefix -> (Quantifier, IntSet)
forall a. [a] -> a
last Prefix
prefix of
          (Quantifier
E, IntSet
xs) -> do
            Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc Matrix
matrix
            IntSet -> IO IntSet
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
xs
          (Quantifier
A, IntSet
xs) -> do
            Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc (Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
matrix)
            IntSet -> IO IntSet
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
xs
      let g :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
          g :: Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
g Int
_nv IntSet
_assumptions [] Matrix
_matrix = [Char] -> IO (Maybe IntSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
          g Int
_nv IntSet
assumptions [(Quantifier
_q,IntSet
xs)] Matrix
_matrix = do
            Bool
ret <- Solver -> [Int] -> IO Bool
SAT.solveWith Solver
solver (IntSet -> [Int]
IntSet.toList IntSet
assumptions)
            if Bool
ret then do
              Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
              Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> IO (Maybe IntSet))
-> Maybe IntSet -> IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]
            else
              Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
          g Int
nv IntSet
assumptions ((Quantifier
q,IntSet
xs) : prefix' :: Prefix
prefix'@((Quantifier
_q2,IntSet
_) : Prefix
prefix'')) Matrix
matrix = do
            let loop :: [IntSet] -> IO (Maybe IntSet)
loop [IntSet]
counterMoves = do
                  let ys :: [(Int, Prefix, Matrix)]
ys = [(Int
nv, Prefix
prefix'', Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
nu) | IntSet
nu <- [IntSet]
counterMoves]
                      (Int
nv2, Prefix
prefix2, Matrix
matrix2) =
                        if Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
E
                        then ((Int, Prefix, Matrix)
 -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix))
-> (Int, Prefix, Matrix)
-> [(Int, Prefix, Matrix)]
-> (Int, Prefix, Matrix)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (Int
nv,[],Matrix
forall a. MonotoneBoolean a => a
true) [(Int, Prefix, Matrix)]
ys
                        else ((Int, Prefix, Matrix)
 -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix))
-> (Int, Prefix, Matrix)
-> [(Int, Prefix, Matrix)]
-> (Int, Prefix, Matrix)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (Int
nv,[],Matrix
forall a. MonotoneBoolean a => a
false) [(Int, Prefix, Matrix)]
ys
                  Maybe IntSet
ret <- Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv2 IntSet
assumptions (Prefix -> Prefix
normalizePrefix ((Quantifier
q,IntSet
xs) (Quantifier, IntSet) -> Prefix -> Prefix
forall a. a -> [a] -> [a]
: Prefix
prefix2)) Matrix
matrix2
                  case Maybe IntSet
ret of
                    Maybe IntSet
Nothing -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
                    Just IntSet
tau' -> do
                      let tau :: IntSet
tau = (Int -> Bool) -> IntSet -> IntSet
IntSet.filter (\Int
l -> Int -> Int
forall a. Num a => a -> a
abs Int
l Int -> IntSet -> Bool
`IntSet.member` IntSet
xs) IntSet
tau'
                      Maybe IntSet
ret2 <- Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
g Int
nv (IntSet
assumptions IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
tau) Prefix
prefix' (Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
tau)
                      case Maybe IntSet
ret2 of
                        Maybe IntSet
Nothing -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
tau)
                        Just IntSet
nu -> [IntSet] -> IO (Maybe IntSet)
loop (IntSet
nu IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: [IntSet]
counterMoves)
            [IntSet] -> IO (Maybe IntSet)
loop []
      Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
g Int
nv IntSet
IntSet.empty Prefix
prefix Matrix
matrix

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

data CNFOrDNF
  = CNF [LitSet]
  | DNF [LitSet]
  deriving (Int -> CNFOrDNF -> ShowS
[CNFOrDNF] -> ShowS
CNFOrDNF -> [Char]
(Int -> CNFOrDNF -> ShowS)
-> (CNFOrDNF -> [Char]) -> ([CNFOrDNF] -> ShowS) -> Show CNFOrDNF
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CNFOrDNF] -> ShowS
$cshowList :: [CNFOrDNF] -> ShowS
show :: CNFOrDNF -> [Char]
$cshow :: CNFOrDNF -> [Char]
showsPrec :: Int -> CNFOrDNF -> ShowS
$cshowsPrec :: Int -> CNFOrDNF -> ShowS
Show)

negateCNFOrDNF :: CNFOrDNF -> CNFOrDNF
negateCNFOrDNF :: CNFOrDNF -> CNFOrDNF
negateCNFOrDNF (CNF [IntSet]
xss) = [IntSet] -> CNFOrDNF
DNF ((IntSet -> IntSet) -> [IntSet] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> IntSet -> IntSet
IntSet.map Int -> Int
forall a. Num a => a -> a
negate) [IntSet]
xss)
negateCNFOrDNF (DNF [IntSet]
xss) = [IntSet] -> CNFOrDNF
CNF ((IntSet -> IntSet) -> [IntSet] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> IntSet -> IntSet
IntSet.map Int -> Int
forall a. Num a => a -> a
negate) [IntSet]
xss)

toCNF :: Int -> CNFOrDNF -> CNF.CNF
toCNF :: Int -> CNFOrDNF -> CNF
toCNF Int
nv (CNF [IntSet]
clauses) = Int -> Int -> [PackedClause] -> CNF
CNF.CNF Int
nv ([IntSet] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IntSet]
clauses) ((IntSet -> PackedClause) -> [IntSet] -> [PackedClause]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> PackedClause
SAT.packClause ([Int] -> PackedClause)
-> (IntSet -> [Int]) -> IntSet -> PackedClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList) [IntSet]
clauses)
toCNF Int
nv (DNF [])    = Int -> Int -> [PackedClause] -> CNF
CNF.CNF Int
nv Int
1 [[Int] -> PackedClause
SAT.packClause []]
toCNF Int
nv (DNF [IntSet]
cubes) = Int -> Int -> [PackedClause] -> CNF
CNF.CNF (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [IntSet] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IntSet]
cubes) ([[Int]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Int]]
cs) (([Int] -> PackedClause) -> [[Int]] -> [PackedClause]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> PackedClause
SAT.packClause [[Int]]
cs)
  where
    zs :: [(Int, IntSet)]
zs = [Int] -> [IntSet] -> [(Int, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..] [IntSet]
cubes
    cs :: [[Int]]
cs = ((Int, IntSet) -> Int) -> [(Int, IntSet)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, IntSet) -> Int
forall a b. (a, b) -> a
fst [(Int, IntSet)]
zs [Int] -> [[Int]] -> [[Int]]
forall a. a -> [a] -> [a]
: [[-Int
sel, Int
lit] | (Int
sel, IntSet
cube) <- [(Int, IntSet)]
zs, Int
lit <- IntSet -> [Int]
IntSet.toList IntSet
cube]

solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveQE Int
nv Prefix
prefix Matrix
matrix = do
  CNFStore IO
store <- IO (CNFStore IO)
forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  CNFStore IO -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ CNFStore IO
store Int
nv
  Encoder IO
encoder <- CNFStore IO -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder CNFStore IO
store
  Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
encoder Matrix
matrix
  CNF
cnf <- CNFStore IO -> IO CNF
forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore IO
store
  let prefix' :: Prefix
prefix' =
        if CNF -> Int
CNF.cnfNumVars CNF
cnf Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
nv then
          Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
E, [Int] -> IntSet
IntSet.fromList [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 .. CNF -> Int
CNF.cnfNumVars CNF
cnf])]
        else
          Prefix
prefix
  (Bool
b, Maybe IntSet
m) <- Int -> Prefix -> [[Int]] -> IO (Bool, Maybe IntSet)
solveQE_CNF (CNF -> Int
CNF.cnfNumVars CNF
cnf) Prefix
prefix' ((PackedClause -> [Int]) -> [PackedClause] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> [Int]
SAT.unpackClause (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf))
  (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
b, (IntSet -> IntSet) -> Maybe IntSet -> Maybe IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> Bool) -> IntSet -> IntSet
IntSet.filter (\Int
lit -> Int -> Int
forall a. Num a => a -> a
abs Int
lit Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
nv)) Maybe IntSet
m)

solveQE_CNF :: Int -> Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
solveQE_CNF :: Int -> Prefix -> [[Int]] -> IO (Bool, Maybe IntSet)
solveQE_CNF Int
nv Prefix
prefix [[Int]]
matrix = Prefix -> [[Int]] -> IO (Bool, Maybe IntSet)
g (Prefix -> Prefix
normalizePrefix Prefix
prefix) [[Int]]
matrix
  where
    g :: Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
    g :: Prefix -> [[Int]] -> IO (Bool, Maybe IntSet)
g ((Quantifier
E,IntSet
xs) : Prefix
prefix') [[Int]]
matrix = do
      CNF
cnf <- (CNFOrDNF -> CNF) -> IO CNFOrDNF -> IO CNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv) (IO CNFOrDNF -> IO CNF) -> IO CNFOrDNF -> IO CNF
forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
      Solver
solver <- IO Solver
SAT.newSolver
      Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver (CNF -> Int
CNF.cnfNumVars CNF
cnf)
      [PackedClause] -> (PackedClause -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) ((PackedClause -> IO ()) -> IO ())
-> (PackedClause -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
        Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver (PackedClause -> [Int]
SAT.unpackClause PackedClause
clause)
      Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
      if Bool
ret then do
        Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
        (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs])
      else do
        (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe IntSet
forall a. Maybe a
Nothing)
    g ((Quantifier
A,IntSet
xs) : Prefix
prefix') [[Int]]
matrix = do
      CNF
cnf <- (CNFOrDNF -> CNF) -> IO CNFOrDNF -> IO CNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv (CNFOrDNF -> CNF) -> (CNFOrDNF -> CNFOrDNF) -> CNFOrDNF -> CNF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CNFOrDNF -> CNFOrDNF
negateCNFOrDNF) (IO CNFOrDNF -> IO CNF) -> IO CNFOrDNF -> IO CNF
forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
      Solver
solver <- IO Solver
SAT.newSolver
      Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver (CNF -> Int
CNF.cnfNumVars CNF
cnf)
      [PackedClause] -> (PackedClause -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) ((PackedClause -> IO ()) -> IO ())
-> (PackedClause -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
        Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver (PackedClause -> [Int]
SAT.unpackClause PackedClause
clause)
      Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
      if Bool
ret then do
        Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
        (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs])
      else do
        (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Maybe IntSet
forall a. Maybe a
Nothing)
    g Prefix
prefix [[Int]]
matrix = do
      CNFOrDNF
ret <- Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix [[Int]]
matrix
      case CNFOrDNF
ret of
        CNF [IntSet]
xs -> (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not ((IntSet -> Bool) -> [IntSet] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any IntSet -> Bool
IntSet.null [IntSet]
xs), Maybe IntSet
forall a. Maybe a
Nothing)
        DNF [IntSet]
xs -> (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return ((IntSet -> Bool) -> [IntSet] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any IntSet -> Bool
IntSet.null [IntSet]
xs, Maybe IntSet
forall a. Maybe a
Nothing)

    f :: Prefix -> [SAT.Clause] -> IO CNFOrDNF
    f :: Prefix -> [[Int]] -> IO CNFOrDNF
f [] [[Int]]
matrix = CNFOrDNF -> IO CNFOrDNF
forall (m :: * -> *) a. Monad m => a -> m a
return (CNFOrDNF -> IO CNFOrDNF) -> CNFOrDNF -> IO CNFOrDNF
forall a b. (a -> b) -> a -> b
$ [IntSet] -> CNFOrDNF
CNF [[Int] -> IntSet
IntSet.fromList [Int]
clause | [Int]
clause <- [[Int]]
matrix]
    f ((Quantifier
E,IntSet
xs) : Prefix
prefix') [[Int]]
matrix = do
      CNF
cnf <- (CNFOrDNF -> CNF) -> IO CNFOrDNF -> IO CNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv) (IO CNFOrDNF -> IO CNF) -> IO CNFOrDNF -> IO CNF
forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
      [IntSet]
dnf <- IntSet -> CNF -> IO [IntSet]
QE.shortestImplicantsE (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 .. CNF -> Int
CNF.cnfNumVars CNF
cnf]) CNF
cnf
      CNFOrDNF -> IO CNFOrDNF
forall (m :: * -> *) a. Monad m => a -> m a
return (CNFOrDNF -> IO CNFOrDNF) -> CNFOrDNF -> IO CNFOrDNF
forall a b. (a -> b) -> a -> b
$ [IntSet] -> CNFOrDNF
DNF [IntSet]
dnf
    f ((Quantifier
A,IntSet
xs) : Prefix
prefix') [[Int]]
matrix = do
      CNF
cnf <- (CNFOrDNF -> CNF) -> IO CNFOrDNF -> IO CNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv (CNFOrDNF -> CNF) -> (CNFOrDNF -> CNFOrDNF) -> CNFOrDNF -> CNF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CNFOrDNF -> CNFOrDNF
negateCNFOrDNF) (IO CNFOrDNF -> IO CNF) -> IO CNFOrDNF -> IO CNF
forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
      [IntSet]
dnf <- IntSet -> CNF -> IO [IntSet]
QE.shortestImplicantsE (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 .. CNF -> Int
CNF.cnfNumVars CNF
cnf]) CNF
cnf
      CNFOrDNF -> IO CNFOrDNF
forall (m :: * -> *) a. Monad m => a -> m a
return (CNFOrDNF -> IO CNFOrDNF) -> CNFOrDNF -> IO CNFOrDNF
forall a b. (a -> b) -> a -> b
$ CNFOrDNF -> CNFOrDNF
negateCNFOrDNF (CNFOrDNF -> CNFOrDNF) -> CNFOrDNF -> CNFOrDNF
forall a b. (a -> b) -> a -> b
$ [IntSet] -> CNFOrDNF
DNF [IntSet]
dnf

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

-- ∀y ∃x. x ∧ (y ∨ ¬x)
_test :: IO (Bool, Maybe LitSet)
_test :: IO (Bool, Maybe IntSet)
_test = Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveNaive Int
2 [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
2), (Quantifier
E, Int -> IntSet
IntSet.singleton Int
1)] (Matrix
x Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Matrix
y Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.||. Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
x))
  where
    x :: Matrix
x  = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1
    y :: Matrix
y  = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
2

_test' :: IO (Bool, Maybe LitSet)
_test' :: IO (Bool, Maybe IntSet)
_test' = Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveCEGAR Int
2 [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
2), (Quantifier
E, Int -> IntSet
IntSet.singleton Int
1)] (Matrix
x Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Matrix
y Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.||. Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
x))
  where
    x :: Matrix
x  = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1
    y :: Matrix
y  = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
2

_test1 :: (Int, Prefix, Matrix)
_test1 :: (Int, Prefix, Matrix)
_test1 = (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (Int
1, [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
1)], Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1) (Int
1, [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
1)], Matrix -> Matrix
forall a. Complement a => a -> a
notB (Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1))

_test2 :: (Int, Prefix, Matrix)
_test2 :: (Int, Prefix, Matrix)
_test2 = (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (Int
1, [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
1)], Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1) (Int
1, [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
1)], Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1)