{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
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
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'
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
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
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
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
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 []
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
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
_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)