{-# 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
  , litToMatrix
  , 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.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, LitSet) -> Bool) -> Prefix -> Prefix
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Quantifier
_,LitSet
xs) -> Bool -> Bool
not (LitSet -> Bool
IntSet.null LitSet
xs))

groupQuantifiers :: Prefix -> Prefix
groupQuantifiers :: Prefix -> Prefix
groupQuantifiers = (Prefix -> (Quantifier, LitSet)) -> [Prefix] -> Prefix
forall a b. (a -> b) -> [a] -> [b]
map Prefix -> (Quantifier, LitSet)
forall {a}. [(a, LitSet)] -> (a, LitSet)
f ([Prefix] -> Prefix) -> (Prefix -> [Prefix]) -> Prefix -> Prefix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Quantifier, LitSet) -> (Quantifier, LitSet) -> 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, LitSet) -> Quantifier)
-> (Quantifier, LitSet)
-> (Quantifier, LitSet)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Quantifier, LitSet) -> Quantifier
forall a b. (a, b) -> a
fst)
  where
    f :: [(a, LitSet)] -> (a, LitSet)
f [(a, LitSet)]
qs = ((a, LitSet) -> a
forall a b. (a, b) -> a
fst ([(a, LitSet)] -> (a, LitSet)
forall a. HasCallStack => [a] -> a
head [(a, LitSet)]
qs), [LitSet] -> LitSet
forall (f :: * -> *). Foldable f => f LitSet -> LitSet
IntSet.unions [LitSet
xs | (a
_,LitSet
xs) <- [(a, LitSet)]
qs])

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

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

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

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

type Matrix = Tseitin.Formula

litToMatrix :: SAT.Lit -> Matrix
litToMatrix :: Int -> Formula
litToMatrix = Int -> Formula
Tseitin.Atom

reduct :: Matrix -> LitSet -> Matrix
reduct :: Formula -> LitSet -> Formula
reduct Formula
m LitSet
ls = Formula -> Formula
Tseitin.simplify (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ (Int -> Formula) -> Formula -> Formula
forall b. Boolean b => (Int -> b) -> Formula -> b
Tseitin.fold Int -> Formula
s Formula
m
  where
    s :: Int -> Formula
s Int
l
      |   Int
l  Int -> LitSet -> Bool
`IntSet.member` LitSet
ls = Formula
forall a. MonotoneBoolean a => a
true
      | (-Int
l) Int -> LitSet -> Bool
`IntSet.member` LitSet
ls = Formula
forall a. MonotoneBoolean a => a
false
      | Bool
otherwise = Int -> Formula
litToMatrix Int
l

substVarMap :: Matrix -> VarMap Matrix -> Matrix
substVarMap :: Formula -> VarMap Formula -> Formula
substVarMap Formula
m VarMap Formula
s = Formula -> Formula
Tseitin.simplify (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ (Int -> Formula) -> Formula -> Formula
forall b. Boolean b => (Int -> b) -> Formula -> b
Tseitin.fold Int -> Formula
f Formula
m
  where
    f :: Int -> Formula
f 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 Formula -> Formula
forall a. a -> a
id else Formula -> Formula
forall a. Complement a => a -> a
notB) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Int -> VarMap Formula -> Formula
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault (Int -> Formula
litToMatrix Int
v) Int
v VarMap Formula
s

-- XXX
prenexAnd :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd :: (Int, Prefix, Formula)
-> (Int, Prefix, Formula) -> (Int, Prefix, Formula)
prenexAnd (Int
nv1, Prefix
prefix1, Formula
matrix1) (Int
nv2, Prefix
prefix2, Formula
matrix2) =
  State Int (Int, Prefix, Formula) -> Int -> (Int, Prefix, Formula)
forall s a. State s a -> s -> a
evalState (Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f [] LitSet
IntSet.empty VarMap Formula
forall a. IntMap a
IntMap.empty VarMap Formula
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 Tseitin.Formula -> VarMap Tseitin.Formula
      -> Prefix -> Prefix
      -> State Int (Int, Prefix, Matrix)
    f :: Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f Prefix
prefix LitSet
_bvs VarMap Formula
subst1 VarMap Formula
subst2 [] [] = do
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      (Int, Prefix, Formula) -> State Int (Int, Prefix, Formula)
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nv, Prefix
prefix, Formula -> Formula
Tseitin.simplify (Formula -> VarMap Formula -> Formula
substVarMap Formula
matrix1 VarMap Formula
subst1 Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> VarMap Formula -> Formula
substVarMap Formula
matrix2 VarMap Formula
subst2))
    f Prefix
prefix LitSet
bvs VarMap Formula
subst1 VarMap Formula
subst2 ((Quantifier
A,LitSet
xs1) : Prefix
prefix1') ((Quantifier
A,LitSet
xs2) : Prefix
prefix2') = do
      let xs :: LitSet
xs = LitSet -> LitSet -> LitSet
IntSet.union LitSet
xs1 LitSet
xs2
          ys :: LitSet
ys = LitSet -> LitSet -> LitSet
IntSet.intersection LitSet
bvs LitSet
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
+ LitSet -> Int
IntSet.size LitSet
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 (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: LitSet
xs' = (LitSet
xs LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
bvs) LitSet -> LitSet -> LitSet
`IntSet.union` [Int] -> LitSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Formula
subst1' = (Int -> Formula) -> IntMap Int -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> LitSet -> Bool
`IntSet.member` LitSet
xs1) IntMap Int
s) VarMap Formula -> VarMap Formula -> VarMap Formula
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst1
          subst2' :: VarMap Formula
subst2' = (Int -> Formula) -> IntMap Int -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> LitSet -> Bool
`IntSet.member` LitSet
xs2) IntMap Int
s) VarMap Formula -> VarMap Formula -> VarMap Formula
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst2
      Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
A, LitSet
xs')]) (LitSet
bvs LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
xs') VarMap Formula
subst1' VarMap Formula
subst2' Prefix
prefix1' Prefix
prefix2'
    f Prefix
prefix LitSet
bvs VarMap Formula
subst1 VarMap Formula
subst2 ((Quantifier
q,LitSet
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 :: LitSet
ys = LitSet -> LitSet -> LitSet
IntSet.intersection LitSet
bvs LitSet
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
+ LitSet -> Int
IntSet.size LitSet
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 (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: LitSet
xs' = (LitSet
xs LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
bvs) LitSet -> LitSet -> LitSet
`IntSet.union` [Int] -> LitSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Formula
subst1' = (Int -> Formula) -> IntMap Int -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix IntMap Int
s VarMap Formula -> VarMap Formula -> VarMap Formula
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst1
      Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, LitSet
xs')]) (LitSet
bvs LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
xs') VarMap Formula
subst1' VarMap Formula
subst2 Prefix
prefix1' Prefix
prefix2
    f Prefix
prefix LitSet
bvs VarMap Formula
subst1 VarMap Formula
subst2 Prefix
prefix1 ((Quantifier
q,LitSet
xs) : Prefix
prefix2')  = do
      let ys :: LitSet
ys = LitSet -> LitSet -> LitSet
IntSet.intersection LitSet
bvs LitSet
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
+ LitSet -> Int
IntSet.size LitSet
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 (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: LitSet
xs' = (LitSet
xs LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
bvs) LitSet -> LitSet -> LitSet
`IntSet.union` [Int] -> LitSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst2' :: VarMap Formula
subst2' = (Int -> Formula) -> IntMap Int -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix IntMap Int
s VarMap Formula -> VarMap Formula -> VarMap Formula
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst2
      Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, LitSet
xs')]) (LitSet
bvs LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
xs') VarMap Formula
subst1 VarMap Formula
subst2' Prefix
prefix1 Prefix
prefix2'

-- XXX
prenexOr :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr :: (Int, Prefix, Formula)
-> (Int, Prefix, Formula) -> (Int, Prefix, Formula)
prenexOr (Int
nv1, Prefix
prefix1, Formula
matrix1) (Int
nv2, Prefix
prefix2, Formula
matrix2) =
  State Int (Int, Prefix, Formula) -> Int -> (Int, Prefix, Formula)
forall s a. State s a -> s -> a
evalState (Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f [] LitSet
IntSet.empty VarMap Formula
forall a. IntMap a
IntMap.empty VarMap Formula
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 Tseitin.Formula -> VarMap Tseitin.Formula
      -> Prefix -> Prefix
      -> State Int (Int, Prefix, Matrix)
    f :: Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f Prefix
prefix LitSet
_bvs VarMap Formula
subst1 VarMap Formula
subst2 [] [] = do
      Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
      (Int, Prefix, Formula) -> State Int (Int, Prefix, Formula)
forall a. a -> StateT Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nv, Prefix
prefix, Formula -> Formula
Tseitin.simplify (Formula -> VarMap Formula -> Formula
substVarMap Formula
matrix1 VarMap Formula
subst1 Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> VarMap Formula -> Formula
substVarMap Formula
matrix2 VarMap Formula
subst2))
    f Prefix
prefix LitSet
bvs VarMap Formula
subst1 VarMap Formula
subst2 ((Quantifier
E,LitSet
xs1) : Prefix
prefix1') ((Quantifier
E,LitSet
xs2) : Prefix
prefix2') = do
      let xs :: LitSet
xs = LitSet -> LitSet -> LitSet
IntSet.union LitSet
xs1 LitSet
xs2
          ys :: LitSet
ys = LitSet -> LitSet -> LitSet
IntSet.intersection LitSet
bvs LitSet
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
+ LitSet -> Int
IntSet.size LitSet
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 (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: LitSet
xs' = (LitSet
xs LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
bvs) LitSet -> LitSet -> LitSet
`IntSet.union` [Int] -> LitSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Formula
subst1' = (Int -> Formula) -> IntMap Int -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> LitSet -> Bool
`IntSet.member` LitSet
xs1) IntMap Int
s) VarMap Formula -> VarMap Formula -> VarMap Formula
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst1
          subst2' :: VarMap Formula
subst2' = (Int -> Formula) -> IntMap Int -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> LitSet -> Bool
`IntSet.member` LitSet
xs2) IntMap Int
s) VarMap Formula -> VarMap Formula -> VarMap Formula
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst2
      Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
A, LitSet
xs')]) (LitSet
bvs LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
xs') VarMap Formula
subst1' VarMap Formula
subst2' Prefix
prefix1' Prefix
prefix2'
    f Prefix
prefix LitSet
bvs VarMap Formula
subst1 VarMap Formula
subst2 ((Quantifier
q,LitSet
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 :: LitSet
ys = LitSet -> LitSet -> LitSet
IntSet.intersection LitSet
bvs LitSet
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
+ LitSet -> Int
IntSet.size LitSet
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 (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: LitSet
xs' = (LitSet
xs LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
bvs) LitSet -> LitSet -> LitSet
`IntSet.union` [Int] -> LitSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Formula
subst1' = (Int -> Formula) -> IntMap Int -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix IntMap Int
s VarMap Formula -> VarMap Formula -> VarMap Formula
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst1
      Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, LitSet
xs')]) (LitSet
bvs LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
xs') VarMap Formula
subst1' VarMap Formula
subst2 Prefix
prefix1' Prefix
prefix2
    f Prefix
prefix LitSet
bvs VarMap Formula
subst1 VarMap Formula
subst2 Prefix
prefix1 ((Quantifier
q,LitSet
xs) : Prefix
prefix2')  = do
      let ys :: LitSet
ys = LitSet -> LitSet -> LitSet
IntSet.intersection LitSet
bvs LitSet
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
+ LitSet -> Int
IntSet.size LitSet
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 (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
          xs' :: LitSet
xs' = (LitSet
xs LitSet -> LitSet -> LitSet
`IntSet.difference` LitSet
bvs) LitSet -> LitSet -> LitSet
`IntSet.union` [Int] -> LitSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst2' :: VarMap Formula
subst2' = (Int -> Formula) -> IntMap Int -> VarMap Formula
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix IntMap Int
s VarMap Formula -> VarMap Formula -> VarMap Formula
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst2
      Prefix
-> LitSet
-> VarMap Formula
-> VarMap Formula
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Formula)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, LitSet
xs')]) (LitSet
bvs LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
xs') VarMap Formula
subst1 VarMap Formula
subst2' Prefix
prefix1 Prefix
prefix2'

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

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

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

-- | Naive Algorithm for a Winning Move
solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveNaive :: Int -> Prefix -> Formula -> IO (Bool, Maybe LitSet)
solveNaive Int
nv Prefix
prefix Formula
matrix =
  case Prefix
prefix' of
    [] -> if (Int -> Bool) -> Formula -> Bool
forall b. Boolean b => (Int -> b) -> Formula -> b
Tseitin.fold Int -> Bool
forall a. HasCallStack => a
undefined Formula
matrix
          then (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just LitSet
IntSet.empty)
          else (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe LitSet
forall a. Maybe a
Nothing)
    (Quantifier
E,LitSet
_) : Prefix
_ -> do
      Maybe LitSet
m <- Prefix -> Formula -> IO (Maybe LitSet)
f Prefix
prefix' Formula
matrix
      (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe LitSet
m, Maybe LitSet
m)
    (Quantifier
A,LitSet
_) : Prefix
_ -> do
      Maybe LitSet
m <- Prefix -> Formula -> IO (Maybe LitSet)
f Prefix
prefix' Formula
matrix
      (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe LitSet
m, Maybe LitSet
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 -> Formula -> IO (Maybe LitSet)
f [] Formula
_matrix = [Char] -> IO (Maybe LitSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
    f [(Quantifier
q,LitSet
xs)] Formula
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 -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc Formula
matrix
        Quantifier
A -> Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc (Formula -> Formula
forall a. Complement a => a -> a
notB Formula
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 LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> IO (Maybe LitSet))
-> Maybe LitSet -> IO (Maybe LitSet)
forall a b. (a -> b) -> a -> b
$ LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just (LitSet -> Maybe LitSet) -> LitSet -> Maybe LitSet
forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
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 <- LitSet -> [Int]
IntSet.toList LitSet
xs]
      else
        Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LitSet
forall a. Maybe a
Nothing
    f ((Quantifier
_q,LitSet
xs) : Prefix
prefix') Formula
matrix = do
      Either LitSet ()
ret <- ExceptT LitSet IO () -> IO (Either LitSet ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT LitSet IO () -> IO (Either LitSet ()))
-> ExceptT LitSet IO () -> IO (Either LitSet ())
forall a b. (a -> b) -> a -> b
$ do
        let moves :: [LitSet]
            moves :: [LitSet]
moves = ([Int] -> LitSet) -> [[Int]] -> [LitSet]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> LitSet
IntSet.fromList ([[Int]] -> [LitSet]) -> [[Int]] -> [LitSet]
forall a b. (a -> b) -> a -> b
$ [[Int]] -> [[Int]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [[Int
x, -Int
x] | Int
x <- LitSet -> [Int]
IntSet.toList LitSet
xs]
        [LitSet]
-> (LitSet -> ExceptT LitSet IO ()) -> ExceptT LitSet IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [LitSet]
moves ((LitSet -> ExceptT LitSet IO ()) -> ExceptT LitSet IO ())
-> (LitSet -> ExceptT LitSet IO ()) -> ExceptT LitSet IO ()
forall a b. (a -> b) -> a -> b
$ \LitSet
tau -> do
          Maybe LitSet
ret <- IO (Maybe LitSet) -> ExceptT LitSet IO (Maybe LitSet)
forall (m :: * -> *) a. Monad m => m a -> ExceptT LitSet m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe LitSet) -> ExceptT LitSet IO (Maybe LitSet))
-> IO (Maybe LitSet) -> ExceptT LitSet IO (Maybe LitSet)
forall a b. (a -> b) -> a -> b
$ Prefix -> Formula -> IO (Maybe LitSet)
f Prefix
prefix' (Formula -> LitSet -> Formula
reduct Formula
matrix LitSet
tau)
          case Maybe LitSet
ret of
            Maybe LitSet
Nothing  -> LitSet -> ExceptT LitSet IO ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE LitSet
tau
            Just LitSet
_nu -> () -> ExceptT LitSet IO ()
forall a. a -> ExceptT LitSet IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      case Either LitSet ()
ret of
        Left LitSet
tau -> Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just LitSet
tau)
        Right () -> Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LitSet
forall a. Maybe a
Nothing

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

-- | Abstraction-Based Algorithm for a Winning Move
solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGAR :: Int -> Prefix -> Formula -> IO (Bool, Maybe LitSet)
solveCEGAR Int
nv Prefix
prefix Formula
matrix =
  case Prefix
prefix' of
    [] -> if (Int -> Bool) -> Formula -> Bool
forall b. Boolean b => (Int -> b) -> Formula -> b
Tseitin.fold Int -> Bool
forall a. HasCallStack => a
undefined Formula
matrix
          then (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just LitSet
IntSet.empty)
          else (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe LitSet
forall a. Maybe a
Nothing)
    (Quantifier
E,LitSet
_) : Prefix
_ -> do
      Maybe LitSet
m <- Int -> Prefix -> Formula -> IO (Maybe LitSet)
f Int
nv Prefix
prefix' Formula
matrix
      (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe LitSet
m, Maybe LitSet
m)
    (Quantifier
A,LitSet
_) : Prefix
_ -> do
      Maybe LitSet
m <- Int -> Prefix -> Formula -> IO (Maybe LitSet)
f Int
nv Prefix
prefix' Formula
matrix
      (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe LitSet
m, Maybe LitSet
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 -> Formula -> IO (Maybe LitSet)
f Int
_nv [] Formula
_matrix = [Char] -> IO (Maybe LitSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
    f Int
nv [(Quantifier
q,LitSet
xs)] Formula
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 -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc Formula
matrix
        Quantifier
A -> Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc (Formula -> Formula
forall a. Complement a => a -> a
notB Formula
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 LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> IO (Maybe LitSet))
-> Maybe LitSet -> IO (Maybe LitSet)
forall a b. (a -> b) -> a -> b
$ LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just (LitSet -> Maybe LitSet) -> LitSet -> Maybe LitSet
forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
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 <- LitSet -> [Int]
IntSet.toList LitSet
xs]
      else
        Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LitSet
forall a. Maybe a
Nothing
    f Int
nv ((Quantifier
q,LitSet
xs) : prefix' :: Prefix
prefix'@((Quantifier
_q2,LitSet
_) : Prefix
prefix'')) Formula
matrix = do
      let loop :: [LitSet] -> IO (Maybe LitSet)
loop [LitSet]
counterMoves = do
            let ys :: [(Int, Prefix, Formula)]
ys = [(Int
nv, Prefix
prefix'', Formula -> LitSet -> Formula
reduct Formula
matrix LitSet
nu) | LitSet
nu <- [LitSet]
counterMoves]
                (Int
nv2, Prefix
prefix2, Formula
matrix2) =
                  if Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
E
                  then ((Int, Prefix, Formula)
 -> (Int, Prefix, Formula) -> (Int, Prefix, Formula))
-> (Int, Prefix, Formula)
-> [(Int, Prefix, Formula)]
-> (Int, Prefix, Formula)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Formula)
-> (Int, Prefix, Formula) -> (Int, Prefix, Formula)
prenexAnd (Int
nv,[],Formula
forall a. MonotoneBoolean a => a
true) [(Int, Prefix, Formula)]
ys
                  else ((Int, Prefix, Formula)
 -> (Int, Prefix, Formula) -> (Int, Prefix, Formula))
-> (Int, Prefix, Formula)
-> [(Int, Prefix, Formula)]
-> (Int, Prefix, Formula)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Formula)
-> (Int, Prefix, Formula) -> (Int, Prefix, Formula)
prenexOr (Int
nv,[],Formula
forall a. MonotoneBoolean a => a
false) [(Int, Prefix, Formula)]
ys
            Maybe LitSet
ret <- Int -> Prefix -> Formula -> IO (Maybe LitSet)
f Int
nv2 (Prefix -> Prefix
normalizePrefix ((Quantifier
q,LitSet
xs) (Quantifier, LitSet) -> Prefix -> Prefix
forall a. a -> [a] -> [a]
: Prefix
prefix2)) Formula
matrix2
            case Maybe LitSet
ret of
              Maybe LitSet
Nothing -> Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LitSet
forall a. Maybe a
Nothing
              Just LitSet
tau' -> do
                let tau :: LitSet
tau = (Int -> Bool) -> LitSet -> LitSet
IntSet.filter (\Int
l -> Int -> Int
forall a. Num a => a -> a
abs Int
l Int -> LitSet -> Bool
`IntSet.member` LitSet
xs) LitSet
tau'
                Maybe LitSet
ret2 <- Int -> Prefix -> Formula -> IO (Maybe LitSet)
f Int
nv Prefix
prefix' (Formula -> LitSet -> Formula
reduct Formula
matrix LitSet
tau)
                case Maybe LitSet
ret2 of
                  Maybe LitSet
Nothing -> Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just LitSet
tau)
                  Just LitSet
nu -> [LitSet] -> IO (Maybe LitSet)
loop (LitSet
nu LitSet -> [LitSet] -> [LitSet]
forall a. a -> [a] -> [a]
: [LitSet]
counterMoves)
      [LitSet] -> IO (Maybe LitSet)
loop []

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

-- | Abstraction-Based Algorithm for a Winning Move
solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGARIncremental :: Int -> Prefix -> Formula -> IO (Bool, Maybe LitSet)
solveCEGARIncremental Int
nv Prefix
prefix Formula
matrix =
  case Prefix
prefix' of
    [] -> if (Int -> Bool) -> Formula -> Bool
forall b. Boolean b => (Int -> b) -> Formula -> b
Tseitin.fold Int -> Bool
forall a. HasCallStack => a
undefined Formula
matrix
          then (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just LitSet
IntSet.empty)
          else (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe LitSet
forall a. Maybe a
Nothing)
    (Quantifier
E,LitSet
_) : Prefix
_ -> do
      Maybe LitSet
m <- Int -> LitSet -> Prefix -> Formula -> IO (Maybe LitSet)
f Int
nv LitSet
IntSet.empty Prefix
prefix' Formula
matrix
      (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe LitSet
m, Maybe LitSet
m)
    (Quantifier
A,LitSet
_) : Prefix
_ -> do
      Maybe LitSet
m <- Int -> LitSet -> Prefix -> Formula -> IO (Maybe LitSet)
f Int
nv LitSet
IntSet.empty Prefix
prefix' Formula
matrix
      (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe LitSet
m, Maybe LitSet
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 -> LitSet -> Prefix -> Formula -> IO (Maybe LitSet)
f Int
nv LitSet
_assumptions Prefix
prefix Formula
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
      LitSet
_xs <-
        case Prefix -> (Quantifier, LitSet)
forall a. HasCallStack => [a] -> a
last Prefix
prefix of
          (Quantifier
E, LitSet
xs) -> do
            Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc Formula
matrix
            LitSet -> IO LitSet
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return LitSet
xs
          (Quantifier
A, LitSet
xs) -> do
            Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc (Formula -> Formula
forall a. Complement a => a -> a
notB Formula
matrix)
            LitSet -> IO LitSet
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return LitSet
xs
      let g :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
          g :: Int -> LitSet -> Prefix -> Formula -> IO (Maybe LitSet)
g Int
_nv LitSet
_assumptions [] Formula
_matrix = [Char] -> IO (Maybe LitSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
          g Int
_nv LitSet
assumptions [(Quantifier
_q,LitSet
xs)] Formula
_matrix = do
            Bool
ret <- Solver -> [Int] -> IO Bool
SAT.solveWith Solver
solver (LitSet -> [Int]
IntSet.toList LitSet
assumptions)
            if Bool
ret then do
              Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
              Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LitSet -> IO (Maybe LitSet))
-> Maybe LitSet -> IO (Maybe LitSet)
forall a b. (a -> b) -> a -> b
$ LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just (LitSet -> Maybe LitSet) -> LitSet -> Maybe LitSet
forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
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 <- LitSet -> [Int]
IntSet.toList LitSet
xs]
            else
              Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LitSet
forall a. Maybe a
Nothing
          g Int
nv LitSet
assumptions ((Quantifier
q,LitSet
xs) : prefix' :: Prefix
prefix'@((Quantifier
_q2,LitSet
_) : Prefix
prefix'')) Formula
matrix = do
            let loop :: [LitSet] -> IO (Maybe LitSet)
loop [LitSet]
counterMoves = do
                  let ys :: [(Int, Prefix, Formula)]
ys = [(Int
nv, Prefix
prefix'', Formula -> LitSet -> Formula
reduct Formula
matrix LitSet
nu) | LitSet
nu <- [LitSet]
counterMoves]
                      (Int
nv2, Prefix
prefix2, Formula
matrix2) =
                        if Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
E
                        then ((Int, Prefix, Formula)
 -> (Int, Prefix, Formula) -> (Int, Prefix, Formula))
-> (Int, Prefix, Formula)
-> [(Int, Prefix, Formula)]
-> (Int, Prefix, Formula)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Formula)
-> (Int, Prefix, Formula) -> (Int, Prefix, Formula)
prenexAnd (Int
nv,[],Formula
forall a. MonotoneBoolean a => a
true) [(Int, Prefix, Formula)]
ys
                        else ((Int, Prefix, Formula)
 -> (Int, Prefix, Formula) -> (Int, Prefix, Formula))
-> (Int, Prefix, Formula)
-> [(Int, Prefix, Formula)]
-> (Int, Prefix, Formula)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Formula)
-> (Int, Prefix, Formula) -> (Int, Prefix, Formula)
prenexOr (Int
nv,[],Formula
forall a. MonotoneBoolean a => a
false) [(Int, Prefix, Formula)]
ys
                  Maybe LitSet
ret <- Int -> LitSet -> Prefix -> Formula -> IO (Maybe LitSet)
f Int
nv2 LitSet
assumptions (Prefix -> Prefix
normalizePrefix ((Quantifier
q,LitSet
xs) (Quantifier, LitSet) -> Prefix -> Prefix
forall a. a -> [a] -> [a]
: Prefix
prefix2)) Formula
matrix2
                  case Maybe LitSet
ret of
                    Maybe LitSet
Nothing -> Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LitSet
forall a. Maybe a
Nothing
                    Just LitSet
tau' -> do
                      let tau :: LitSet
tau = (Int -> Bool) -> LitSet -> LitSet
IntSet.filter (\Int
l -> Int -> Int
forall a. Num a => a -> a
abs Int
l Int -> LitSet -> Bool
`IntSet.member` LitSet
xs) LitSet
tau'
                      Maybe LitSet
ret2 <- Int -> LitSet -> Prefix -> Formula -> IO (Maybe LitSet)
g Int
nv (LitSet
assumptions LitSet -> LitSet -> LitSet
`IntSet.union` LitSet
tau) Prefix
prefix' (Formula -> LitSet -> Formula
reduct Formula
matrix LitSet
tau)
                      case Maybe LitSet
ret2 of
                        Maybe LitSet
Nothing -> Maybe LitSet -> IO (Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just LitSet
tau)
                        Just LitSet
nu -> [LitSet] -> IO (Maybe LitSet)
loop (LitSet
nu LitSet -> [LitSet] -> [LitSet]
forall a. a -> [a] -> [a]
: [LitSet]
counterMoves)
            [LitSet] -> IO (Maybe LitSet)
loop []
      Int -> LitSet -> Prefix -> Formula -> IO (Maybe LitSet)
g Int
nv LitSet
IntSet.empty Prefix
prefix Formula
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
$cshowsPrec :: Int -> CNFOrDNF -> ShowS
showsPrec :: Int -> CNFOrDNF -> ShowS
$cshow :: CNFOrDNF -> [Char]
show :: CNFOrDNF -> [Char]
$cshowList :: [CNFOrDNF] -> ShowS
showList :: [CNFOrDNF] -> ShowS
Show)

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

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

solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveQE :: Int -> Prefix -> Formula -> IO (Bool, Maybe LitSet)
solveQE Int
nv Prefix
prefix Formula
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 -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
encoder Formula
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] -> LitSet
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 LitSet
m) <- Int -> Prefix -> [[Int]] -> IO (Bool, Maybe LitSet)
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 LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
b, (LitSet -> LitSet) -> Maybe LitSet -> Maybe LitSet
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> Bool) -> LitSet -> LitSet
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 LitSet
m)

solveQE_CNF :: Int -> Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
solveQE_CNF :: Int -> Prefix -> [[Int]] -> IO (Bool, Maybe LitSet)
solveQE_CNF Int
nv Prefix
prefix [[Int]]
matrix = Prefix -> [[Int]] -> IO (Bool, Maybe LitSet)
g (Prefix -> Prefix
normalizePrefix Prefix
prefix) [[Int]]
matrix
  where
    g :: Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
    g :: Prefix -> [[Int]] -> IO (Bool, Maybe LitSet)
g ((Quantifier
E,LitSet
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 LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just (LitSet -> Maybe LitSet) -> LitSet -> Maybe LitSet
forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
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 <- LitSet -> [Int]
IntSet.toList LitSet
xs])
      else do
        (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe LitSet
forall a. Maybe a
Nothing)
    g ((Quantifier
A,LitSet
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 LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, LitSet -> Maybe LitSet
forall a. a -> Maybe a
Just (LitSet -> Maybe LitSet) -> LitSet -> Maybe LitSet
forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
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 <- LitSet -> [Int]
IntSet.toList LitSet
xs])
      else do
        (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Maybe LitSet
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 [LitSet]
xs -> (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not ((LitSet -> Bool) -> [LitSet] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any LitSet -> Bool
IntSet.null [LitSet]
xs), Maybe LitSet
forall a. Maybe a
Nothing)
        DNF [LitSet]
xs -> (Bool, Maybe LitSet) -> IO (Bool, Maybe LitSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((LitSet -> Bool) -> [LitSet] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any LitSet -> Bool
IntSet.null [LitSet]
xs, Maybe LitSet
forall a. Maybe a
Nothing)

    f :: Prefix -> [SAT.Clause] -> IO CNFOrDNF
    f :: Prefix -> [[Int]] -> IO CNFOrDNF
f [] [[Int]]
matrix = CNFOrDNF -> IO CNFOrDNF
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CNFOrDNF -> IO CNFOrDNF) -> CNFOrDNF -> IO CNFOrDNF
forall a b. (a -> b) -> a -> b
$ [LitSet] -> CNFOrDNF
CNF [[Int] -> LitSet
IntSet.fromList [Int]
clause | [Int]
clause <- [[Int]]
matrix]
    f ((Quantifier
E,LitSet
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
      [LitSet]
dnf <- LitSet -> CNF -> IO [LitSet]
QE.shortestImplicantsE (LitSet
xs LitSet -> LitSet -> LitSet
`IntSet.union` [Int] -> LitSet
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CNFOrDNF -> IO CNFOrDNF) -> CNFOrDNF -> IO CNFOrDNF
forall a b. (a -> b) -> a -> b
$ [LitSet] -> CNFOrDNF
DNF [LitSet]
dnf
    f ((Quantifier
A,LitSet
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
      [LitSet]
dnf <- LitSet -> CNF -> IO [LitSet]
QE.shortestImplicantsE (LitSet
xs LitSet -> LitSet -> LitSet
`IntSet.union` [Int] -> LitSet
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 a. a -> IO a
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
$ [LitSet] -> CNFOrDNF
DNF [LitSet]
dnf

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

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

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

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

_test2 :: (Int, Prefix, Matrix)
_test2 :: (Int, Prefix, Formula)
_test2 = (Int, Prefix, Formula)
-> (Int, Prefix, Formula) -> (Int, Prefix, Formula)
prenexOr (Int
1, [(Quantifier
A, Int -> LitSet
IntSet.singleton Int
1)], Int -> Formula
litToMatrix Int
1) (Int
1, [(Quantifier
A, Int -> LitSet
IntSet.singleton Int
1)], Int -> Formula
litToMatrix Int
1)