{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE BangPatterns #-}
module ToySolver.QBF
( Quantifier (..)
, Prefix
, normalizePrefix
, quantifyFreeVariables
, Matrix
, solve
, solveNaive
, solveCEGAR
, solveCEGARIncremental
, solveQE
, solveQE_CNF
) where
import Control.Monad
import Control.Monad.State.Strict
import Control.Monad.Trans.Except
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import Data.Function (on)
import Data.List (groupBy, foldl')
import Data.Maybe
import ToySolver.Data.Boolean
import ToySolver.Data.BoolExpr (BoolExpr)
import qualified ToySolver.Data.BoolExpr as BoolExpr
import ToySolver.FileFormat.CNF (Quantifier (..))
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.Types (LitSet, VarSet, VarMap)
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Store.CNF
import qualified ToySolver.SAT.ExistentialQuantification as QE
type Prefix = [(Quantifier, VarSet)]
normalizePrefix :: Prefix -> Prefix
normalizePrefix :: Prefix -> Prefix
normalizePrefix = Prefix -> Prefix
groupQuantifiers (Prefix -> Prefix) -> (Prefix -> Prefix) -> Prefix -> Prefix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prefix -> Prefix
removeEmptyQuantifiers
removeEmptyQuantifiers :: Prefix -> Prefix
removeEmptyQuantifiers :: Prefix -> Prefix
removeEmptyQuantifiers = ((Quantifier, IntSet) -> Bool) -> Prefix -> Prefix
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Quantifier
_,IntSet
xs) -> Bool -> Bool
not (IntSet -> Bool
IntSet.null IntSet
xs))
groupQuantifiers :: Prefix -> Prefix
groupQuantifiers :: Prefix -> Prefix
groupQuantifiers = (Prefix -> (Quantifier, IntSet)) -> [Prefix] -> Prefix
forall a b. (a -> b) -> [a] -> [b]
map Prefix -> (Quantifier, IntSet)
forall a. [(a, IntSet)] -> (a, IntSet)
f ([Prefix] -> Prefix) -> (Prefix -> [Prefix]) -> Prefix -> Prefix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Quantifier, IntSet) -> (Quantifier, IntSet) -> Bool)
-> Prefix -> [Prefix]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Quantifier -> Quantifier -> Bool)
-> ((Quantifier, IntSet) -> Quantifier)
-> (Quantifier, IntSet)
-> (Quantifier, IntSet)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Quantifier, IntSet) -> Quantifier
forall a b. (a, b) -> a
fst)
where
f :: [(a, IntSet)] -> (a, IntSet)
f [(a, IntSet)]
qs = ((a, IntSet) -> a
forall a b. (a, b) -> a
fst ([(a, IntSet)] -> (a, IntSet)
forall a. [a] -> a
head [(a, IntSet)]
qs), [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [IntSet
xs | (a
_,IntSet
xs) <- [(a, IntSet)]
qs])
quantifyFreeVariables :: Int -> Prefix -> Prefix
quantifyFreeVariables :: Int -> Prefix -> Prefix
quantifyFreeVariables Int
nv Prefix
prefix
| IntSet -> Bool
IntSet.null IntSet
rest = Prefix
prefix
| Bool
otherwise = (Quantifier
E, IntSet
rest) (Quantifier, IntSet) -> Prefix -> Prefix
forall a. a -> [a] -> [a]
: Prefix
prefix
where
rest :: IntSet
rest = [Int] -> IntSet
IntSet.fromList [Int
1..Int
nv] IntSet -> IntSet -> IntSet
`IntSet.difference` [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [IntSet
vs | (Quantifier
_q, IntSet
vs) <- Prefix
prefix]
prefixStartWithA :: Prefix -> Bool
prefixStartWithA :: Prefix -> Bool
prefixStartWithA ((Quantifier
A,IntSet
_) : Prefix
_) = Bool
True
prefixStartWithA Prefix
_ = Bool
False
prefixStartWithE :: Prefix -> Bool
prefixStartWithE :: Prefix -> Bool
prefixStartWithE ((Quantifier
E,IntSet
_) : Prefix
_) = Bool
True
prefixStartWithE Prefix
_ = Bool
False
type Matrix = BoolExpr SAT.Lit
reduct :: Matrix -> LitSet -> Matrix
reduct :: Matrix -> IntSet -> Matrix
reduct Matrix
m IntSet
ls = Matrix -> Matrix
forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify (Matrix -> Matrix) -> Matrix -> Matrix
forall a b. (a -> b) -> a -> b
$ Matrix
m Matrix -> (Int -> Matrix) -> Matrix
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> Matrix
s
where
s :: Int -> Matrix
s Int
l
| Int
l Int -> IntSet -> Bool
`IntSet.member` IntSet
ls = Matrix
forall a. MonotoneBoolean a => a
true
| (-Int
l) Int -> IntSet -> Bool
`IntSet.member` IntSet
ls = Matrix
forall a. MonotoneBoolean a => a
false
| Bool
otherwise = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
l
substVarMap :: Matrix -> VarMap Matrix -> Matrix
substVarMap :: Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
m VarMap Matrix
s = Matrix -> Matrix
forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify (Matrix -> Matrix) -> Matrix -> Matrix
forall a b. (a -> b) -> a -> b
$ Matrix
m Matrix -> (Int -> Matrix) -> Matrix
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
l -> do
let v :: Int
v = Int -> Int
forall a. Num a => a -> a
abs Int
l
(if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Matrix -> Matrix
forall a. a -> a
id else Matrix -> Matrix
forall a. Complement a => a -> a
notB) (Matrix -> Matrix) -> Matrix -> Matrix
forall a b. (a -> b) -> a -> b
$ Matrix -> Int -> VarMap Matrix -> Matrix
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault (Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
v) Int
v VarMap Matrix
s
prenexAnd :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd :: (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (Int
nv1, Prefix
prefix1, Matrix
matrix1) (Int
nv2, Prefix
prefix2, Matrix
matrix2) =
State Int (Int, Prefix, Matrix) -> Int -> (Int, Prefix, Matrix)
forall s a. State s a -> s -> a
evalState (Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f [] IntSet
IntSet.empty VarMap Matrix
forall a. IntMap a
IntMap.empty VarMap Matrix
forall a. IntMap a
IntMap.empty Prefix
prefix1 Prefix
prefix2) (Int
nv1 Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
nv2)
where
f :: Prefix -> VarSet
-> VarMap (BoolExpr SAT.Lit) -> VarMap (BoolExpr SAT.Lit)
-> Prefix -> Prefix
-> State Int (Int, Prefix, Matrix)
f :: Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f Prefix
prefix IntSet
_bvs VarMap Matrix
subst1 VarMap Matrix
subst2 [] [] = do
Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
(Int, Prefix, Matrix) -> State Int (Int, Prefix, Matrix)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nv, Prefix
prefix, Matrix -> Matrix
forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify (Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
matrix1 VarMap Matrix
subst1 Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.&&. Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
matrix2 VarMap Matrix
subst2))
f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 ((Quantifier
A,IntSet
xs1) : Prefix
prefix1') ((Quantifier
A,IntSet
xs2) : Prefix
prefix2') = do
let xs :: IntSet
xs = IntSet -> IntSet -> IntSet
IntSet.union IntSet
xs1 IntSet
xs2
ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
let s :: IntMap Int
s = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
subst1' :: VarMap Matrix
subst1' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
xs1) IntMap Int
s) VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst1
subst2' :: VarMap Matrix
subst2' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
xs2) IntMap Int
s) VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst2
Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
A, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1' VarMap Matrix
subst2' Prefix
prefix1' Prefix
prefix2'
f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 ((Quantifier
q,IntSet
xs) : Prefix
prefix1') Prefix
prefix2 | Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
E Bool -> Bool -> Bool
|| Bool -> Bool
not (Prefix -> Bool
prefixStartWithE Prefix
prefix2) = do
let ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
let s :: IntMap Int
s = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
subst1' :: VarMap Matrix
subst1' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom IntMap Int
s VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst1
Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1' VarMap Matrix
subst2 Prefix
prefix1' Prefix
prefix2
f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 Prefix
prefix1 ((Quantifier
q,IntSet
xs) : Prefix
prefix2') = do
let ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
let s :: IntMap Int
s = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
subst2' :: VarMap Matrix
subst2' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom IntMap Int
s VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst2
Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1 VarMap Matrix
subst2' Prefix
prefix1 Prefix
prefix2'
prenexOr :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr :: (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (Int
nv1, Prefix
prefix1, Matrix
matrix1) (Int
nv2, Prefix
prefix2, Matrix
matrix2) =
State Int (Int, Prefix, Matrix) -> Int -> (Int, Prefix, Matrix)
forall s a. State s a -> s -> a
evalState (Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f [] IntSet
IntSet.empty VarMap Matrix
forall a. IntMap a
IntMap.empty VarMap Matrix
forall a. IntMap a
IntMap.empty Prefix
prefix1 Prefix
prefix2) (Int
nv1 Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
nv2)
where
f :: Prefix -> VarSet
-> VarMap (BoolExpr SAT.Lit) -> VarMap (BoolExpr SAT.Lit)
-> Prefix -> Prefix
-> State Int (Int, Prefix, Matrix)
f :: Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f Prefix
prefix IntSet
_bvs VarMap Matrix
subst1 VarMap Matrix
subst2 [] [] = do
Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
(Int, Prefix, Matrix) -> State Int (Int, Prefix, Matrix)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nv, Prefix
prefix, Matrix -> Matrix
forall a. BoolExpr a -> BoolExpr a
BoolExpr.simplify (Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
matrix1 VarMap Matrix
subst1 Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.||. Matrix -> VarMap Matrix -> Matrix
substVarMap Matrix
matrix2 VarMap Matrix
subst2))
f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 ((Quantifier
E,IntSet
xs1) : Prefix
prefix1') ((Quantifier
E,IntSet
xs2) : Prefix
prefix2') = do
let xs :: IntSet
xs = IntSet -> IntSet -> IntSet
IntSet.union IntSet
xs1 IntSet
xs2
ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
let s :: IntMap Int
s = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
subst1' :: VarMap Matrix
subst1' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
xs1) IntMap Int
s) VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst1
subst2' :: VarMap Matrix
subst2' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom ((Int -> Int -> Bool) -> IntMap Int -> IntMap Int
forall a. (Int -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey (\Int
x Int
_ -> Int
x Int -> IntSet -> Bool
`IntSet.member` IntSet
xs2) IntMap Int
s) VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst2
Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
A, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1' VarMap Matrix
subst2' Prefix
prefix1' Prefix
prefix2'
f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 ((Quantifier
q,IntSet
xs) : Prefix
prefix1') Prefix
prefix2 | Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
A Bool -> Bool -> Bool
|| Bool -> Bool
not (Prefix -> Bool
prefixStartWithA Prefix
prefix2)= do
let ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
let s :: IntMap Int
s = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
subst1' :: VarMap Matrix
subst1' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom IntMap Int
s VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst1
Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1' VarMap Matrix
subst2 Prefix
prefix1' Prefix
prefix2
f Prefix
prefix IntSet
bvs VarMap Matrix
subst1 VarMap Matrix
subst2 Prefix
prefix1 ((Quantifier
q,IntSet
xs) : Prefix
prefix2') = do
let ys :: IntSet
ys = IntSet -> IntSet -> IntSet
IntSet.intersection IntSet
bvs IntSet
xs
Int
nv <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ IntSet -> Int
IntSet.size IntSet
ys)
let s :: IntMap Int
s = [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [Int]
IntSet.toList IntSet
ys) [(Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ..]
xs' :: IntSet
xs' = (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.difference` IntSet
bvs) IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList (IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems IntMap Int
s)
subst2' :: VarMap Matrix
subst2' = (Int -> Matrix) -> IntMap Int -> VarMap Matrix
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom IntMap Int
s VarMap Matrix -> VarMap Matrix -> VarMap Matrix
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` VarMap Matrix
subst2
Prefix
-> IntSet
-> VarMap Matrix
-> VarMap Matrix
-> Prefix
-> Prefix
-> State Int (Int, Prefix, Matrix)
f (Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
q, IntSet
xs')]) (IntSet
bvs IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
xs') VarMap Matrix
subst1 VarMap Matrix
subst2' Prefix
prefix1 Prefix
prefix2'
solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solve = Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveCEGARIncremental
solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveNaive Int
nv Prefix
prefix Matrix
matrix =
case Prefix
prefix' of
[] -> if (Int -> Bool) -> Matrix -> Bool
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Int -> Bool
forall a. HasCallStack => a
undefined Matrix
matrix
then (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
IntSet.empty)
else (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe IntSet
forall a. Maybe a
Nothing)
(Quantifier
E,IntSet
_) : Prefix
_ -> do
Maybe IntSet
m <- Prefix -> Matrix -> IO (Maybe IntSet)
f Prefix
prefix' Matrix
matrix
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe IntSet
m, Maybe IntSet
m)
(Quantifier
A,IntSet
_) : Prefix
_ -> do
Maybe IntSet
m <- Prefix -> Matrix -> IO (Maybe IntSet)
f Prefix
prefix' Matrix
matrix
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe IntSet
m, Maybe IntSet
m)
where
prefix' :: Prefix
prefix' = Prefix -> Prefix
normalizePrefix Prefix
prefix
f :: Prefix -> Matrix -> IO (Maybe LitSet)
f :: Prefix -> Matrix -> IO (Maybe IntSet)
f [] Matrix
_matrix = [Char] -> IO (Maybe IntSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
f [(Quantifier
q,IntSet
xs)] Matrix
matrix = do
Solver
solver <- IO Solver
SAT.newSolver
Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
Encoder IO
enc <- Solver -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
case Quantifier
q of
Quantifier
E -> Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc Matrix
matrix
Quantifier
A -> Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc (Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
matrix)
Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
if Bool
ret then do
Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> IO (Maybe IntSet))
-> Maybe IntSet -> IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]
else
Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
f ((Quantifier
_q,IntSet
xs) : Prefix
prefix') Matrix
matrix = do
Either IntSet ()
ret <- ExceptT IntSet IO () -> IO (Either IntSet ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT IntSet IO () -> IO (Either IntSet ()))
-> ExceptT IntSet IO () -> IO (Either IntSet ())
forall a b. (a -> b) -> a -> b
$ do
let moves :: [LitSet]
moves :: [IntSet]
moves = ([Int] -> IntSet) -> [[Int]] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> IntSet
IntSet.fromList ([[Int]] -> [IntSet]) -> [[Int]] -> [IntSet]
forall a b. (a -> b) -> a -> b
$ [[Int]] -> [[Int]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[Int
x, -Int
x] | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]
[IntSet]
-> (IntSet -> ExceptT IntSet IO ()) -> ExceptT IntSet IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [IntSet]
moves ((IntSet -> ExceptT IntSet IO ()) -> ExceptT IntSet IO ())
-> (IntSet -> ExceptT IntSet IO ()) -> ExceptT IntSet IO ()
forall a b. (a -> b) -> a -> b
$ \IntSet
tau -> do
Maybe IntSet
ret <- IO (Maybe IntSet) -> ExceptT IntSet IO (Maybe IntSet)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe IntSet) -> ExceptT IntSet IO (Maybe IntSet))
-> IO (Maybe IntSet) -> ExceptT IntSet IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ Prefix -> Matrix -> IO (Maybe IntSet)
f Prefix
prefix' (Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
tau)
case Maybe IntSet
ret of
Maybe IntSet
Nothing -> IntSet -> ExceptT IntSet IO ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE IntSet
tau
Just IntSet
_nu -> () -> ExceptT IntSet IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
case Either IntSet ()
ret of
Left IntSet
tau -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
tau)
Right () -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveCEGAR Int
nv Prefix
prefix Matrix
matrix =
case Prefix
prefix' of
[] -> if (Int -> Bool) -> Matrix -> Bool
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Int -> Bool
forall a. HasCallStack => a
undefined Matrix
matrix
then (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
IntSet.empty)
else (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe IntSet
forall a. Maybe a
Nothing)
(Quantifier
E,IntSet
_) : Prefix
_ -> do
Maybe IntSet
m <- Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv Prefix
prefix' Matrix
matrix
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe IntSet
m, Maybe IntSet
m)
(Quantifier
A,IntSet
_) : Prefix
_ -> do
Maybe IntSet
m <- Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv Prefix
prefix' Matrix
matrix
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe IntSet
m, Maybe IntSet
m)
where
prefix' :: Prefix
prefix' = Prefix -> Prefix
normalizePrefix Prefix
prefix
f :: Int -> Prefix -> Matrix -> IO (Maybe LitSet)
f :: Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
_nv [] Matrix
_matrix = [Char] -> IO (Maybe IntSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
f Int
nv [(Quantifier
q,IntSet
xs)] Matrix
matrix = do
Solver
solver <- IO Solver
SAT.newSolver
Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
Encoder IO
enc <- Solver -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
case Quantifier
q of
Quantifier
E -> Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc Matrix
matrix
Quantifier
A -> Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc (Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
matrix)
Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
if Bool
ret then do
Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> IO (Maybe IntSet))
-> Maybe IntSet -> IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]
else
Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
f Int
nv ((Quantifier
q,IntSet
xs) : prefix' :: Prefix
prefix'@((Quantifier
_q2,IntSet
_) : Prefix
prefix'')) Matrix
matrix = do
let loop :: [IntSet] -> IO (Maybe IntSet)
loop [IntSet]
counterMoves = do
let ys :: [(Int, Prefix, Matrix)]
ys = [(Int
nv, Prefix
prefix'', Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
nu) | IntSet
nu <- [IntSet]
counterMoves]
(Int
nv2, Prefix
prefix2, Matrix
matrix2) =
if Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
E
then ((Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix))
-> (Int, Prefix, Matrix)
-> [(Int, Prefix, Matrix)]
-> (Int, Prefix, Matrix)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (Int
nv,[],Matrix
forall a. MonotoneBoolean a => a
true) [(Int, Prefix, Matrix)]
ys
else ((Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix))
-> (Int, Prefix, Matrix)
-> [(Int, Prefix, Matrix)]
-> (Int, Prefix, Matrix)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (Int
nv,[],Matrix
forall a. MonotoneBoolean a => a
false) [(Int, Prefix, Matrix)]
ys
Maybe IntSet
ret <- Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv2 (Prefix -> Prefix
normalizePrefix ((Quantifier
q,IntSet
xs) (Quantifier, IntSet) -> Prefix -> Prefix
forall a. a -> [a] -> [a]
: Prefix
prefix2)) Matrix
matrix2
case Maybe IntSet
ret of
Maybe IntSet
Nothing -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
Just IntSet
tau' -> do
let tau :: IntSet
tau = (Int -> Bool) -> IntSet -> IntSet
IntSet.filter (\Int
l -> Int -> Int
forall a. Num a => a -> a
abs Int
l Int -> IntSet -> Bool
`IntSet.member` IntSet
xs) IntSet
tau'
Maybe IntSet
ret2 <- Int -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv Prefix
prefix' (Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
tau)
case Maybe IntSet
ret2 of
Maybe IntSet
Nothing -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
tau)
Just IntSet
nu -> [IntSet] -> IO (Maybe IntSet)
loop (IntSet
nu IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: [IntSet]
counterMoves)
[IntSet] -> IO (Maybe IntSet)
loop []
solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveCEGARIncremental Int
nv Prefix
prefix Matrix
matrix =
case Prefix
prefix' of
[] -> if (Int -> Bool) -> Matrix -> Bool
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
BoolExpr.fold Int -> Bool
forall a. HasCallStack => a
undefined Matrix
matrix
then (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
IntSet.empty)
else (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe IntSet
forall a. Maybe a
Nothing)
(Quantifier
E,IntSet
_) : Prefix
_ -> do
Maybe IntSet
m <- Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv IntSet
IntSet.empty Prefix
prefix' Matrix
matrix
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isJust Maybe IntSet
m, Maybe IntSet
m)
(Quantifier
A,IntSet
_) : Prefix
_ -> do
Maybe IntSet
m <- Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv IntSet
IntSet.empty Prefix
prefix' Matrix
matrix
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> Bool
forall a. Maybe a -> Bool
isNothing Maybe IntSet
m, Maybe IntSet
m)
where
prefix' :: Prefix
prefix' = Prefix -> Prefix
normalizePrefix Prefix
prefix
f :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
f :: Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv IntSet
_assumptions Prefix
prefix Matrix
matrix = do
Solver
solver <- IO Solver
SAT.newSolver
Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver Int
nv
Encoder IO
enc <- Solver -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
solver
IntSet
_xs <-
case Prefix -> (Quantifier, IntSet)
forall a. [a] -> a
last Prefix
prefix of
(Quantifier
E, IntSet
xs) -> do
Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc Matrix
matrix
IntSet -> IO IntSet
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
xs
(Quantifier
A, IntSet
xs) -> do
Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
enc (Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
matrix)
IntSet -> IO IntSet
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
xs
let g :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
g :: Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
g Int
_nv IntSet
_assumptions [] Matrix
_matrix = [Char] -> IO (Maybe IntSet)
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
g Int
_nv IntSet
assumptions [(Quantifier
_q,IntSet
xs)] Matrix
_matrix = do
Bool
ret <- Solver -> [Int] -> IO Bool
SAT.solveWith Solver
solver (IntSet -> [Int]
IntSet.toList IntSet
assumptions)
if Bool
ret then do
Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe IntSet -> IO (Maybe IntSet))
-> Maybe IntSet -> IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]
else
Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
g Int
nv IntSet
assumptions ((Quantifier
q,IntSet
xs) : prefix' :: Prefix
prefix'@((Quantifier
_q2,IntSet
_) : Prefix
prefix'')) Matrix
matrix = do
let loop :: [IntSet] -> IO (Maybe IntSet)
loop [IntSet]
counterMoves = do
let ys :: [(Int, Prefix, Matrix)]
ys = [(Int
nv, Prefix
prefix'', Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
nu) | IntSet
nu <- [IntSet]
counterMoves]
(Int
nv2, Prefix
prefix2, Matrix
matrix2) =
if Quantifier
qQuantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
==Quantifier
E
then ((Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix))
-> (Int, Prefix, Matrix)
-> [(Int, Prefix, Matrix)]
-> (Int, Prefix, Matrix)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (Int
nv,[],Matrix
forall a. MonotoneBoolean a => a
true) [(Int, Prefix, Matrix)]
ys
else ((Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix))
-> (Int, Prefix, Matrix)
-> [(Int, Prefix, Matrix)]
-> (Int, Prefix, Matrix)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (Int
nv,[],Matrix
forall a. MonotoneBoolean a => a
false) [(Int, Prefix, Matrix)]
ys
Maybe IntSet
ret <- Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
f Int
nv2 IntSet
assumptions (Prefix -> Prefix
normalizePrefix ((Quantifier
q,IntSet
xs) (Quantifier, IntSet) -> Prefix -> Prefix
forall a. a -> [a] -> [a]
: Prefix
prefix2)) Matrix
matrix2
case Maybe IntSet
ret of
Maybe IntSet
Nothing -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing
Just IntSet
tau' -> do
let tau :: IntSet
tau = (Int -> Bool) -> IntSet -> IntSet
IntSet.filter (\Int
l -> Int -> Int
forall a. Num a => a -> a
abs Int
l Int -> IntSet -> Bool
`IntSet.member` IntSet
xs) IntSet
tau'
Maybe IntSet
ret2 <- Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
g Int
nv (IntSet
assumptions IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
tau) Prefix
prefix' (Matrix -> IntSet -> Matrix
reduct Matrix
matrix IntSet
tau)
case Maybe IntSet
ret2 of
Maybe IntSet
Nothing -> Maybe IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just IntSet
tau)
Just IntSet
nu -> [IntSet] -> IO (Maybe IntSet)
loop (IntSet
nu IntSet -> [IntSet] -> [IntSet]
forall a. a -> [a] -> [a]
: [IntSet]
counterMoves)
[IntSet] -> IO (Maybe IntSet)
loop []
Int -> IntSet -> Prefix -> Matrix -> IO (Maybe IntSet)
g Int
nv IntSet
IntSet.empty Prefix
prefix Matrix
matrix
data CNFOrDNF
= CNF [LitSet]
| DNF [LitSet]
deriving (Int -> CNFOrDNF -> ShowS
[CNFOrDNF] -> ShowS
CNFOrDNF -> [Char]
(Int -> CNFOrDNF -> ShowS)
-> (CNFOrDNF -> [Char]) -> ([CNFOrDNF] -> ShowS) -> Show CNFOrDNF
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CNFOrDNF] -> ShowS
$cshowList :: [CNFOrDNF] -> ShowS
show :: CNFOrDNF -> [Char]
$cshow :: CNFOrDNF -> [Char]
showsPrec :: Int -> CNFOrDNF -> ShowS
$cshowsPrec :: Int -> CNFOrDNF -> ShowS
Show)
negateCNFOrDNF :: CNFOrDNF -> CNFOrDNF
negateCNFOrDNF :: CNFOrDNF -> CNFOrDNF
negateCNFOrDNF (CNF [IntSet]
xss) = [IntSet] -> CNFOrDNF
DNF ((IntSet -> IntSet) -> [IntSet] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> IntSet -> IntSet
IntSet.map Int -> Int
forall a. Num a => a -> a
negate) [IntSet]
xss)
negateCNFOrDNF (DNF [IntSet]
xss) = [IntSet] -> CNFOrDNF
CNF ((IntSet -> IntSet) -> [IntSet] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> IntSet -> IntSet
IntSet.map Int -> Int
forall a. Num a => a -> a
negate) [IntSet]
xss)
toCNF :: Int -> CNFOrDNF -> CNF.CNF
toCNF :: Int -> CNFOrDNF -> CNF
toCNF Int
nv (CNF [IntSet]
clauses) = Int -> Int -> [PackedClause] -> CNF
CNF.CNF Int
nv ([IntSet] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IntSet]
clauses) ((IntSet -> PackedClause) -> [IntSet] -> [PackedClause]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> PackedClause
SAT.packClause ([Int] -> PackedClause)
-> (IntSet -> [Int]) -> IntSet -> PackedClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList) [IntSet]
clauses)
toCNF Int
nv (DNF []) = Int -> Int -> [PackedClause] -> CNF
CNF.CNF Int
nv Int
1 [[Int] -> PackedClause
SAT.packClause []]
toCNF Int
nv (DNF [IntSet]
cubes) = Int -> Int -> [PackedClause] -> CNF
CNF.CNF (Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [IntSet] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [IntSet]
cubes) ([[Int]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Int]]
cs) (([Int] -> PackedClause) -> [[Int]] -> [PackedClause]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> PackedClause
SAT.packClause [[Int]]
cs)
where
zs :: [(Int, IntSet)]
zs = [Int] -> [IntSet] -> [(Int, IntSet)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..] [IntSet]
cubes
cs :: [[Int]]
cs = ((Int, IntSet) -> Int) -> [(Int, IntSet)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, IntSet) -> Int
forall a b. (a, b) -> a
fst [(Int, IntSet)]
zs [Int] -> [[Int]] -> [[Int]]
forall a. a -> [a] -> [a]
: [[-Int
sel, Int
lit] | (Int
sel, IntSet
cube) <- [(Int, IntSet)]
zs, Int
lit <- IntSet -> [Int]
IntSet.toList IntSet
cube]
solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveQE Int
nv Prefix
prefix Matrix
matrix = do
CNFStore IO
store <- IO (CNFStore IO)
forall (m :: * -> *). PrimMonad m => m (CNFStore m)
newCNFStore
CNFStore IO -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ CNFStore IO
store Int
nv
Encoder IO
encoder <- CNFStore IO -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder CNFStore IO
store
Encoder IO -> Matrix -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Matrix -> m ()
Tseitin.addFormula Encoder IO
encoder Matrix
matrix
CNF
cnf <- CNFStore IO -> IO CNF
forall (m :: * -> *). PrimMonad m => CNFStore m -> m CNF
getCNFFormula CNFStore IO
store
let prefix' :: Prefix
prefix' =
if CNF -> Int
CNF.cnfNumVars CNF
cnf Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
nv then
Prefix
prefix Prefix -> Prefix -> Prefix
forall a. [a] -> [a] -> [a]
++ [(Quantifier
E, [Int] -> IntSet
IntSet.fromList [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 .. CNF -> Int
CNF.cnfNumVars CNF
cnf])]
else
Prefix
prefix
(Bool
b, Maybe IntSet
m) <- Int -> Prefix -> [[Int]] -> IO (Bool, Maybe IntSet)
solveQE_CNF (CNF -> Int
CNF.cnfNumVars CNF
cnf) Prefix
prefix' ((PackedClause -> [Int]) -> [PackedClause] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map PackedClause -> [Int]
SAT.unpackClause (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf))
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
b, (IntSet -> IntSet) -> Maybe IntSet -> Maybe IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> Bool) -> IntSet -> IntSet
IntSet.filter (\Int
lit -> Int -> Int
forall a. Num a => a -> a
abs Int
lit Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
nv)) Maybe IntSet
m)
solveQE_CNF :: Int -> Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
solveQE_CNF :: Int -> Prefix -> [[Int]] -> IO (Bool, Maybe IntSet)
solveQE_CNF Int
nv Prefix
prefix [[Int]]
matrix = Prefix -> [[Int]] -> IO (Bool, Maybe IntSet)
g (Prefix -> Prefix
normalizePrefix Prefix
prefix) [[Int]]
matrix
where
g :: Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
g :: Prefix -> [[Int]] -> IO (Bool, Maybe IntSet)
g ((Quantifier
E,IntSet
xs) : Prefix
prefix') [[Int]]
matrix = do
CNF
cnf <- (CNFOrDNF -> CNF) -> IO CNFOrDNF -> IO CNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv) (IO CNFOrDNF -> IO CNF) -> IO CNFOrDNF -> IO CNF
forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
Solver
solver <- IO Solver
SAT.newSolver
Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver (CNF -> Int
CNF.cnfNumVars CNF
cnf)
[PackedClause] -> (PackedClause -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) ((PackedClause -> IO ()) -> IO ())
-> (PackedClause -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver (PackedClause -> [Int]
SAT.unpackClause PackedClause
clause)
Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
if Bool
ret then do
Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs])
else do
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Maybe IntSet
forall a. Maybe a
Nothing)
g ((Quantifier
A,IntSet
xs) : Prefix
prefix') [[Int]]
matrix = do
CNF
cnf <- (CNFOrDNF -> CNF) -> IO CNFOrDNF -> IO CNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv (CNFOrDNF -> CNF) -> (CNFOrDNF -> CNFOrDNF) -> CNFOrDNF -> CNF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CNFOrDNF -> CNFOrDNF
negateCNFOrDNF) (IO CNFOrDNF -> IO CNF) -> IO CNFOrDNF -> IO CNF
forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
Solver
solver <- IO Solver
SAT.newSolver
Solver -> Int -> IO ()
forall (m :: * -> *) a. NewVar m a => a -> Int -> m ()
SAT.newVars_ Solver
solver (CNF -> Int
CNF.cnfNumVars CNF
cnf)
[PackedClause] -> (PackedClause -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf) ((PackedClause -> IO ()) -> IO ())
-> (PackedClause -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \PackedClause
clause -> do
Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause Solver
solver (PackedClause -> [Int]
SAT.unpackClause PackedClause
clause)
Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
if Bool
ret then do
Model
m <- Solver -> IO Model
SAT.getModel Solver
solver
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IntSet -> Maybe IntSet) -> IntSet -> Maybe IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList [if Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m Int
x then Int
x else -Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs])
else do
(Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Maybe IntSet
forall a. Maybe a
Nothing)
g Prefix
prefix [[Int]]
matrix = do
CNFOrDNF
ret <- Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix [[Int]]
matrix
case CNFOrDNF
ret of
CNF [IntSet]
xs -> (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not ((IntSet -> Bool) -> [IntSet] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any IntSet -> Bool
IntSet.null [IntSet]
xs), Maybe IntSet
forall a. Maybe a
Nothing)
DNF [IntSet]
xs -> (Bool, Maybe IntSet) -> IO (Bool, Maybe IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return ((IntSet -> Bool) -> [IntSet] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any IntSet -> Bool
IntSet.null [IntSet]
xs, Maybe IntSet
forall a. Maybe a
Nothing)
f :: Prefix -> [SAT.Clause] -> IO CNFOrDNF
f :: Prefix -> [[Int]] -> IO CNFOrDNF
f [] [[Int]]
matrix = CNFOrDNF -> IO CNFOrDNF
forall (m :: * -> *) a. Monad m => a -> m a
return (CNFOrDNF -> IO CNFOrDNF) -> CNFOrDNF -> IO CNFOrDNF
forall a b. (a -> b) -> a -> b
$ [IntSet] -> CNFOrDNF
CNF [[Int] -> IntSet
IntSet.fromList [Int]
clause | [Int]
clause <- [[Int]]
matrix]
f ((Quantifier
E,IntSet
xs) : Prefix
prefix') [[Int]]
matrix = do
CNF
cnf <- (CNFOrDNF -> CNF) -> IO CNFOrDNF -> IO CNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv) (IO CNFOrDNF -> IO CNF) -> IO CNFOrDNF -> IO CNF
forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
[IntSet]
dnf <- IntSet -> CNF -> IO [IntSet]
QE.shortestImplicantsE (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 .. CNF -> Int
CNF.cnfNumVars CNF
cnf]) CNF
cnf
CNFOrDNF -> IO CNFOrDNF
forall (m :: * -> *) a. Monad m => a -> m a
return (CNFOrDNF -> IO CNFOrDNF) -> CNFOrDNF -> IO CNFOrDNF
forall a b. (a -> b) -> a -> b
$ [IntSet] -> CNFOrDNF
DNF [IntSet]
dnf
f ((Quantifier
A,IntSet
xs) : Prefix
prefix') [[Int]]
matrix = do
CNF
cnf <- (CNFOrDNF -> CNF) -> IO CNFOrDNF -> IO CNF
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> CNFOrDNF -> CNF
toCNF Int
nv (CNFOrDNF -> CNF) -> (CNFOrDNF -> CNFOrDNF) -> CNFOrDNF -> CNF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CNFOrDNF -> CNFOrDNF
negateCNFOrDNF) (IO CNFOrDNF -> IO CNF) -> IO CNFOrDNF -> IO CNF
forall a b. (a -> b) -> a -> b
$ Prefix -> [[Int]] -> IO CNFOrDNF
f Prefix
prefix' [[Int]]
matrix
[IntSet]
dnf <- IntSet -> CNF -> IO [IntSet]
QE.shortestImplicantsE (IntSet
xs IntSet -> IntSet -> IntSet
`IntSet.union` [Int] -> IntSet
IntSet.fromList [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 .. CNF -> Int
CNF.cnfNumVars CNF
cnf]) CNF
cnf
CNFOrDNF -> IO CNFOrDNF
forall (m :: * -> *) a. Monad m => a -> m a
return (CNFOrDNF -> IO CNFOrDNF) -> CNFOrDNF -> IO CNFOrDNF
forall a b. (a -> b) -> a -> b
$ CNFOrDNF -> CNFOrDNF
negateCNFOrDNF (CNFOrDNF -> CNFOrDNF) -> CNFOrDNF -> CNFOrDNF
forall a b. (a -> b) -> a -> b
$ [IntSet] -> CNFOrDNF
DNF [IntSet]
dnf
_test :: IO (Bool, Maybe LitSet)
_test :: IO (Bool, Maybe IntSet)
_test = Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveNaive Int
2 [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
2), (Quantifier
E, Int -> IntSet
IntSet.singleton Int
1)] (Matrix
x Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Matrix
y Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.||. Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
x))
where
x :: Matrix
x = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1
y :: Matrix
y = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
2
_test' :: IO (Bool, Maybe LitSet)
_test' :: IO (Bool, Maybe IntSet)
_test' = Int -> Prefix -> Matrix -> IO (Bool, Maybe IntSet)
solveCEGAR Int
2 [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
2), (Quantifier
E, Int -> IntSet
IntSet.singleton Int
1)] (Matrix
x Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Matrix
y Matrix -> Matrix -> Matrix
forall a. MonotoneBoolean a => a -> a -> a
.||. Matrix -> Matrix
forall a. Complement a => a -> a
notB Matrix
x))
where
x :: Matrix
x = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1
y :: Matrix
y = Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
2
_test1 :: (Int, Prefix, Matrix)
_test1 :: (Int, Prefix, Matrix)
_test1 = (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (Int
1, [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
1)], Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1) (Int
1, [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
1)], Matrix -> Matrix
forall a. Complement a => a -> a
notB (Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1))
_test2 :: (Int, Prefix, Matrix)
_test2 :: (Int, Prefix, Matrix)
_test2 = (Int, Prefix, Matrix)
-> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (Int
1, [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
1)], Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1) (Int
1, [(Quantifier
A, Int -> IntSet
IntSet.singleton Int
1)], Int -> Matrix
forall a. a -> BoolExpr a
BoolExpr.Atom Int
1)