{-# 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prefix -> Prefix
removeEmptyQuantifiers

removeEmptyQuantifiers :: Prefix -> Prefix
removeEmptyQuantifiers :: Prefix -> Prefix
removeEmptyQuantifiers = 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 = forall a b. (a -> b) -> [a] -> [b]
map forall {a}. [(a, LitSet)] -> (a, LitSet)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
  where
    f :: [(a, LitSet)] -> (a, LitSet)
f [(a, LitSet)]
qs = (forall a b. (a, b) -> a
fst (forall a. [a] -> a
head [(a, LitSet)]
qs), 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) forall a. a -> [a] -> [a]
: Prefix
prefix
  where
    rest :: LitSet
rest = [Int] -> LitSet
IntSet.fromList [Int
1..Int
nv] LitSet -> LitSet -> LitSet
`IntSet.difference` 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 forall a b. (a -> b) -> a -> b
$ 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 = forall a. MonotoneBoolean a => a
true
      | (-Int
l) Int -> LitSet -> Bool
`IntSet.member` LitSet
ls = 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 forall a b. (a -> b) -> a -> b
$ 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 = forall a. Num a => a -> a
abs Int
l
      (if Int
l forall a. Ord a => a -> a -> Bool
> Int
0 then forall a. a -> a
id else forall a. Complement a => a -> a
notB) forall a b. (a -> b) -> a -> b
$ 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) =
  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 forall a. IntMap a
IntMap.empty forall a. IntMap a
IntMap.empty Prefix
prefix1 Prefix
prefix2) (Int
nv1 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 <- forall s (m :: * -> *). MonadState s m => m s
get
      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 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 <- forall s (m :: * -> *). MonadState s m => m s
get
      forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv forall a. Num a => a -> a -> a
+ LitSet -> Int
IntSet.size LitSet
ys)
      let s :: IntMap Int
s  = forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvforall 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 (forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Formula
subst1' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix (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) forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst1
          subst2' :: VarMap Formula
subst2' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix (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) 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 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
qforall 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 <- forall s (m :: * -> *). MonadState s m => m s
get
      forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv forall a. Num a => a -> a -> a
+ LitSet -> Int
IntSet.size LitSet
ys)
      let s :: IntMap Int
s  = forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvforall 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 (forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Formula
subst1' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix IntMap Int
s 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 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 <- forall s (m :: * -> *). MonadState s m => m s
get
      forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv forall a. Num a => a -> a -> a
+ LitSet -> Int
IntSet.size LitSet
ys)
      let s :: IntMap Int
s  = forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvforall 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 (forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst2' :: VarMap Formula
subst2' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix IntMap Int
s 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 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) =
  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 forall a. IntMap a
IntMap.empty forall a. IntMap a
IntMap.empty Prefix
prefix1 Prefix
prefix2) (Int
nv1 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 <- forall s (m :: * -> *). MonadState s m => m s
get
      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 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 <- forall s (m :: * -> *). MonadState s m => m s
get
      forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv forall a. Num a => a -> a -> a
+ LitSet -> Int
IntSet.size LitSet
ys)
      let s :: IntMap Int
s  = forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvforall 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 (forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Formula
subst1' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix (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) forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Formula
subst1
          subst2' :: VarMap Formula
subst2' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix (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) 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 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
qforall 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 <- forall s (m :: * -> *). MonadState s m => m s
get
      forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv forall a. Num a => a -> a -> a
+ LitSet -> Int
IntSet.size LitSet
ys)
      let s :: IntMap Int
s  = forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvforall 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 (forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst1' :: VarMap Formula
subst1' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix IntMap Int
s 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 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 <- forall s (m :: * -> *). MonadState s m => m s
get
      forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv forall a. Num a => a -> a -> a
+ LitSet -> Int
IntSet.size LitSet
ys)
      let s :: IntMap Int
s  = forall a. [(Int, a)] -> IntMap a
IntMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (LitSet -> [Int]
IntSet.toList LitSet
ys) [(Int
nvforall 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 (forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
          subst2' :: VarMap Formula
subst2' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Formula
litToMatrix IntMap Int
s 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 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 forall b. Boolean b => (Int -> b) -> Formula -> b
Tseitin.fold forall a. HasCallStack => a
undefined Formula
matrix
          then forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, forall a. a -> Maybe a
Just LitSet
IntSet.empty)
          else forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, forall a. Maybe a
Nothing)
    (Quantifier
E,LitSet
_) : Prefix
_ -> do
      Maybe LitSet
m <- Prefix -> Formula -> IO (Maybe LitSet)
f Prefix
prefix' Formula
matrix
      forall (m :: * -> *) a. Monad m => a -> m a
return (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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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 = forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
    f [(Quantifier
q,LitSet
xs)] Formula
matrix = do
      Solver
solver <- IO Solver
SAT.newSolver
      forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
      Encoder IO
enc <- forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
      case Quantifier
q of
        Quantifier
E -> forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc Formula
matrix
        Quantifier
A -> forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc (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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
IntSet.fromList [if 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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    f ((Quantifier
_q,LitSet
xs) : Prefix
prefix') Formula
matrix = do
      Either LitSet ()
ret <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
        let moves :: [LitSet]
            moves :: [LitSet]
moves = forall a b. (a -> b) -> [a] -> [b]
map [Int] -> LitSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[Int
x, -Int
x] | Int
x <- LitSet -> [Int]
IntSet.toList LitSet
xs]
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [LitSet]
moves forall a b. (a -> b) -> a -> b
$ \LitSet
tau -> do
          Maybe LitSet
ret <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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  -> forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE LitSet
tau
            Just LitSet
_nu -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      case Either LitSet ()
ret of
        Left LitSet
tau -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just LitSet
tau)
        Right () -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall b. Boolean b => (Int -> b) -> Formula -> b
Tseitin.fold forall a. HasCallStack => a
undefined Formula
matrix
          then forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, forall a. a -> Maybe a
Just LitSet
IntSet.empty)
          else forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, 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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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 = 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
      forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
      Encoder IO
enc <- forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
      case Quantifier
q of
        Quantifier
E -> forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc Formula
matrix
        Quantifier
A -> forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc (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
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
IntSet.fromList [if 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
        forall (m :: * -> *) a. Monad m => a -> m a
return 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
qforall a. Eq a => a -> a -> Bool
==Quantifier
E
                  then 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,[],forall a. MonotoneBoolean a => a
true) [(Int, Prefix, Formula)]
ys
                  else 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,[],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) forall a. a -> [a] -> [a]
: Prefix
prefix2)) Formula
matrix2
            case Maybe LitSet
ret of
              Maybe LitSet
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
              Just LitSet
tau' -> do
                let tau :: LitSet
tau = (Int -> Bool) -> LitSet -> LitSet
IntSet.filter (\Int
l -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just LitSet
tau)
                  Just LitSet
nu -> [LitSet] -> IO (Maybe LitSet)
loop (LitSet
nu 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 forall b. Boolean b => (Int -> b) -> Formula -> b
Tseitin.fold forall a. HasCallStack => a
undefined Formula
matrix
          then forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, forall a. a -> Maybe a
Just LitSet
IntSet.empty)
          else forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, 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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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
      forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
      Encoder IO
enc <- forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
      LitSet
_xs <-
        case forall a. [a] -> a
last Prefix
prefix of
          (Quantifier
E, LitSet
xs) -> do
            forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc Formula
matrix
            forall (m :: * -> *) a. Monad m => a -> m a
return LitSet
xs
          (Quantifier
A, LitSet
xs) -> do
            forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc (forall a. Complement a => a -> a
notB Formula
matrix)
            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 = 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
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
IntSet.fromList [if 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
              forall (m :: * -> *) a. Monad m => a -> m a
return 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
qforall a. Eq a => a -> a -> Bool
==Quantifier
E
                        then 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,[],forall a. MonotoneBoolean a => a
true) [(Int, Prefix, Formula)]
ys
                        else 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,[],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) forall a. a -> [a] -> [a]
: Prefix
prefix2)) Formula
matrix2
                  case Maybe LitSet
ret of
                    Maybe LitSet
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                    Just LitSet
tau' -> do
                      let tau :: LitSet
tau = (Int -> Bool) -> LitSet -> LitSet
IntSet.filter (\Int
l -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just LitSet
tau)
                        Just LitSet
nu -> [LitSet] -> IO (Maybe LitSet)
loop (LitSet
nu 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]
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 [LitSet]
xss) = [LitSet] -> CNFOrDNF
DNF (forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> LitSet -> LitSet
IntSet.map forall a. Num a => a -> a
negate) [LitSet]
xss)
negateCNFOrDNF (DNF [LitSet]
xss) = [LitSet] -> CNFOrDNF
CNF (forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> LitSet -> LitSet
IntSet.map 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 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [LitSet]
clauses) (forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> PackedClause
SAT.packClause 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 forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [LitSet]
cubes) (forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Int]]
cs) (forall a b. (a -> b) -> [a] -> [b]
map [Int] -> PackedClause
SAT.packClause [[Int]]
cs)
  where
    zs :: [(Int, LitSet)]
zs = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
nvforall a. Num a => a -> a -> a
+Int
1..] [LitSet]
cubes
    cs :: [[Int]]
cs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Int, LitSet)]
zs 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 <- forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
  forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ CNFStore IO
store Int
nv
  Encoder IO
encoder <- forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder CNFStore IO
store
  forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
encoder Formula
matrix
  CNF
cnf <- forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore IO
store
  let prefix' :: Prefix
prefix' =
        if CNF -> Int
CNF.cnfNumVars CNF
cnf forall a. Ord a => a -> a -> Bool
> Int
nv then
          Prefix
prefix forall a. [a] -> [a] -> [a]
++ [(Quantifier
E, [Int] -> LitSet
IntSet.fromList [Int
nvforall 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' (forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> [Int]
SAT.unpackClause (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf))
  forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
b, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> Bool) -> LitSet -> LitSet
IntSet.filter (\Int
lit -> forall a. Num a => a -> a
abs Int
lit 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 <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv) forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
      Solver
solver <- IO Solver
SAT.newSolver
      forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver (CNF -> Int
CNF.cnfNumVars CNF
cnf)
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
        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
        forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
IntSet.fromList [if 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
        forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, forall a. Maybe a
Nothing)
    g ((Quantifier
A,LitSet
xs) : Prefix
prefix') [[Int]]
matrix = do
      CNF
cnf <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv forall b c a. (b -> c) -> (a -> b) -> a -> c
. CNFOrDNF -> CNFOrDNF
negateCNFOrDNF) forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
      Solver
solver <- IO Solver
SAT.newSolver
      forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver (CNF -> Int
CNF.cnfNumVars CNF
cnf)
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
        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
        forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Int] -> LitSet
IntSet.fromList [if 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
        forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any LitSet -> Bool
IntSet.null [LitSet]
xs), forall a. Maybe a
Nothing)
        DNF [LitSet]
xs -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any LitSet -> Bool
IntSet.null [LitSet]
xs, forall a. Maybe a
Nothing)

    f :: Prefix -> [SAT.Clause] -> IO CNFOrDNF
    f :: Prefix -> [[Int]] -> IO CNFOrDNF
f [] [[Int]]
matrix = forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv) 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
nvforall a. Num a => a -> a -> a
+Int
1 .. CNF -> Int
CNF.cnfNumVars CNF
cnf]) CNF
cnf
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [LitSet] -> CNFOrDNF
DNF [LitSet]
dnf
    f ((Quantifier
A,LitSet
xs) : Prefix
prefix') [[Int]]
matrix = do
      CNF
cnf <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv forall b c a. (b -> c) -> (a -> b) -> a -> c
. CNFOrDNF -> CNFOrDNF
negateCNFOrDNF) 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
nvforall a. Num a => a -> a -> a
+Int
1 .. CNF -> Int
CNF.cnfNumVars CNF
cnf]) CNF
cnf
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CNFOrDNF -> CNFOrDNF
negateCNFOrDNF 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 forall a. MonotoneBoolean a => a -> a -> a
.&&. (Formula
y forall a. MonotoneBoolean a => a -> a -> a
.||. 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 forall a. MonotoneBoolean a => a -> a -> a
.&&. (Formula
y forall a. MonotoneBoolean a => a -> a -> a
.||. 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)], 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)