msakai / toysolver / 604

Committed 06 Feb 2025 03:40AM UTC coverage: 71.288% (-0.07%) from 71.354%

Build # 604

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #145 from msakai/update-stack-lts-202502

Update stack resolvers (2025-02)

Run Details

10696 of 15004 relevant lines covered (71.29%)

0.71 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

58.7

/src/ToySolver/QBF.hs

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

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

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

import qualified ToySolver.SAT.ExistentialQuantification as QE

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

type Prefix = [(Quantifier, VarSet)]

normalizePrefix :: Prefix -> Prefix
normalizePrefix = groupQuantifiers . removeEmptyQuantifiers

removeEmptyQuantifiers :: Prefix -> Prefix
removeEmptyQuantifiers = filter (\(_,xs) -> not (IntSet.null xs))

groupQuantifiers :: Prefix -> Prefix
groupQuantifiers = map f . groupBy ((==) `on` fst)
  where
    f qs = (fst (head qs), IntSet.unions [xs | (_,xs) <- qs])

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

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

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

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

type Matrix = Tseitin.Formula

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

reduct :: Matrix -> LitSet -> Matrix
reduct m ls = Tseitin.simplify $ Tseitin.fold s m
  where
    s l
      |   l  `IntSet.member` ls = true
      | (-l) `IntSet.member` ls = false
      | otherwise = litToMatrix l

substVarMap :: Matrix -> VarMap Matrix -> Matrix
substVarMap m s = Tseitin.simplify $ Tseitin.fold f m
  where
    f l = do
      let v = abs l
      (if l > 0 then id else notB) $ IntMap.findWithDefault (litToMatrix v) v s

-- XXX
prenexAnd :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =
  evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)
  where
    f :: Prefix -> VarSet
      -> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
      -> Prefix -> Prefix
      -> State Int (Int, Prefix, Matrix)
    f prefix _bvs subst1 subst2 [] [] = do
      nv <- get
      return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .&&. substVarMap matrix2 subst2))
    f prefix bvs subst1 subst2 ((A,xs1) : prefix1') ((A,xs2) : prefix2') = do
      let xs = IntSet.union xs1 xs2
          ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1
          subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2
      f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'
    f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 | q==E || not (prefixStartWithE prefix2) = do
      let ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst1' = fmap litToMatrix s `IntMap.union` subst1
      f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2
    f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2')  = do
      let ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst2' = fmap litToMatrix s `IntMap.union` subst2
      f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'

-- XXX
prenexOr :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexOr (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =
  evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)
  where
    f :: Prefix -> VarSet
      -> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
      -> Prefix -> Prefix
      -> State Int (Int, Prefix, Matrix)
    f prefix _bvs subst1 subst2 [] [] = do
      nv <- get
      return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .||. substVarMap matrix2 subst2))
    f prefix bvs subst1 subst2 ((E,xs1) : prefix1') ((E,xs2) : prefix2') = do
      let xs = IntSet.union xs1 xs2
          ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1
          subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2
      f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'
    f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 | q==A || not (prefixStartWithA prefix2)= do
      let ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst1' = fmap litToMatrix s `IntMap.union` subst1
      f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2
    f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2')  = do
      let ys = IntSet.intersection bvs xs
      nv <- get
      put (nv + IntSet.size ys)
      let s  = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
          xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
          subst2' = fmap litToMatrix s `IntMap.union` subst2
      f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'

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

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

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

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

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

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

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

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

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

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

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

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

data CNFOrDNF
  = CNF [LitSet]
  | DNF [LitSet]
  deriving (Show)

negateCNFOrDNF :: CNFOrDNF -> CNFOrDNF
negateCNFOrDNF (CNF xss) = DNF (map (IntSet.map negate) xss)
negateCNFOrDNF (DNF xss) = CNF (map (IntSet.map negate) xss)

toCNF :: Int -> CNFOrDNF -> CNF.CNF
toCNF nv (CNF clauses) = CNF.CNF nv (length clauses) (map (SAT.packClause . IntSet.toList) clauses)
toCNF nv (DNF [])    = CNF.CNF nv 1 [SAT.packClause []]
toCNF nv (DNF cubes) = CNF.CNF (nv + length cubes) (length cs) (map SAT.packClause cs)
  where
    zs = zip [nv+1..] cubes
    cs = map fst zs : [[-sel, lit] | (sel, cube) <- zs, lit <- IntSet.toList cube]

solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveQE nv prefix matrix = do
  store <- newCNFStore
  SAT.newVars_ store nv
  encoder <- Tseitin.newEncoder store
  Tseitin.addFormula encoder matrix
  cnf <- getCNFFormula store
  let prefix' =
        if CNF.cnfNumVars cnf > nv then
          prefix ++ [(E, IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf])]
        else
          prefix
  (b, m) <- solveQE_CNF (CNF.cnfNumVars cnf) prefix' (map SAT.unpackClause (CNF.cnfClauses cnf))
  return (b, fmap (IntSet.filter (\lit -> abs lit <= nv)) m)

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

    f :: Prefix -> [SAT.Clause] -> IO CNFOrDNF
    f [] matrix = return $ CNF [IntSet.fromList clause | clause <- matrix]
    f ((E,xs) : prefix') matrix = do
      cnf <- liftM (toCNF nv) $ f prefix' matrix
      dnf <- QE.shortestImplicantsE (xs `IntSet.union` IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf]) cnf
      return $ DNF dnf
    f ((A,xs) : prefix') matrix = do
      cnf <- liftM (toCNF nv . negateCNFOrDNF) $ f prefix' matrix
      dnf <- QE.shortestImplicantsE (xs `IntSet.union` IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf]) cnf
      return $ negateCNFOrDNF $ DNF dnf

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

-- ∀y ∃x. x ∧ (y ∨ ¬x)
_test :: IO (Bool, Maybe LitSet)
_test = solveNaive 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .||. notB x))
  where
    x  = litToMatrix 1
    y  = litToMatrix 2

_test' :: IO (Bool, Maybe LitSet)
_test' = solveCEGAR 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .||. notB x))
  where
    x  = litToMatrix 1
    y  = litToMatrix 2

_test1 :: (Int, Prefix, Matrix)
_test1 = prenexAnd (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], notB (litToMatrix 1))

_test2 :: (Int, Prefix, Matrix)
_test2 = prenexOr (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], litToMatrix 1)

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE BangPatterns #-}
4	-----------------------------------------------------------------------------
5	-- \|
6	-- Module : ToySolver.QBF
7	-- Copyright : (c) Masahiro Sakai 2016
8	-- License : BSD-style
9	--
10	-- Maintainer : masahiro.sakai@gmail.com
11	-- Stability : provisional
12	-- Portability : non-portable
13	--
14	-- Reference:
15	--
16	-- * Mikoláš Janota, William Klieber, Joao Marques-Silva, Edmund Clarke.
17	-- Solving QBF with Counterexample Guided Refinement.
18	-- In Theory and Applications of Satisfiability Testing (SAT 2012), pp. 114-128.
19	-- <https://doi.org/10.1007/978-3-642-31612-8_10>
20	-- <https://www.cs.cmu.edu/~wklieber/papers/qbf-cegar-sat-2012.pdf>
21	--
22	-----------------------------------------------------------------------------
23	module ToySolver.QBF
24	( Quantifier (..)
25	, Prefix
26	, normalizePrefix
27	, quantifyFreeVariables
28	, Matrix
29	, litToMatrix
30	, solve
31	, solveNaive
32	, solveCEGAR
33	, solveCEGARIncremental
34	, solveQE
35	, solveQE_CNF
36	) where
37
38	import Control.Monad
39	import Control.Monad.State.Strict
40	import Control.Monad.Trans.Except
41	import qualified Data.IntMap as IntMap
42	import qualified Data.IntSet as IntSet
43	import Data.Function (on)
44	import Data.List (groupBy, foldl')
45	import Data.Maybe
46
47	import ToySolver.Data.Boolean
48	import ToySolver.FileFormat.CNF (Quantifier (..))
49	import qualified ToySolver.FileFormat.CNF as CNF
50	import qualified ToySolver.SAT as SAT
51	import ToySolver.SAT.Types (LitSet, VarSet, VarMap)
52	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
53	import ToySolver.SAT.Store.CNF
54
55	import qualified ToySolver.SAT.ExistentialQuantification as QE
56
57	-- ----------------------------------------------------------------------------
58
59	type Prefix = [(Quantifier, VarSet)]
60
61	normalizePrefix :: Prefix -> Prefix
62	normalizePrefix = groupQuantifiers . removeEmptyQuantifiers	1✔
63
64	removeEmptyQuantifiers :: Prefix -> Prefix
65	removeEmptyQuantifiers = filter (\(_,xs) -> not (IntSet.null xs))	1✔
66
67	groupQuantifiers :: Prefix -> Prefix
68	groupQuantifiers = map f . groupBy ((==) `on` fst)	1✔
69	where
70	f qs = (fst (head qs), IntSet.unions [xs \| (_,xs) <- qs])	1✔
71
72	quantifyFreeVariables :: Int -> Prefix -> Prefix
73	quantifyFreeVariables nv prefix	×
74	\| IntSet.null rest = prefix	×
75	\| otherwise = (E, rest) : prefix	×
76	where
77	rest = IntSet.fromList [1..nv] `IntSet.difference` IntSet.unions [vs \| (_q, vs) <- prefix]	×
78
79	prefixStartWithA :: Prefix -> Bool
80	prefixStartWithA ((A,_) : _) = True	×
81	prefixStartWithA _ = False	×
82
83	prefixStartWithE :: Prefix -> Bool
84	prefixStartWithE ((E,_) : _) = True	×
85	prefixStartWithE _ = False	×
86
87	-- ----------------------------------------------------------------------------
88
89	type Matrix = Tseitin.Formula
90
91	litToMatrix :: SAT.Lit -> Matrix
92	litToMatrix = Tseitin.Atom	1✔
93
94	reduct :: Matrix -> LitSet -> Matrix
95	reduct m ls = Tseitin.simplify $ Tseitin.fold s m	1✔
96	where
97	s l	1✔
98	\| l `IntSet.member` ls = true	1✔
99	\| (-l) `IntSet.member` ls = false	1✔
100	\| otherwise = litToMatrix l	×
101
102	substVarMap :: Matrix -> VarMap Matrix -> Matrix
103	substVarMap m s = Tseitin.simplify $ Tseitin.fold f m	1✔
104	where
105	f l = do	1✔
106	let v = abs l	1✔
107	(if l > 0 then id else notB) $ IntMap.findWithDefault (litToMatrix v) v s	×
108
109	-- XXX
110	prenexAnd :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
111	prenexAnd (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =	1✔
112	evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)	1✔
113	where
114	f :: Prefix -> VarSet
115	-> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
116	-> Prefix -> Prefix
117	-> State Int (Int, Prefix, Matrix)
118	f prefix _bvs subst1 subst2 [] [] = do	1✔
119	nv <- get	1✔
120	return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .&&. substVarMap matrix2 subst2))	1✔
121	f prefix bvs subst1 subst2 ((A,xs1) : prefix1') ((A,xs2) : prefix2') = do	×
122	let xs = IntSet.union xs1 xs2	×
123	ys = IntSet.intersection bvs xs	×
124	nv <- get	×
125	put (nv + IntSet.size ys)	×
126	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
127	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	×
128	subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1	×
129	subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2	×
130	f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'	×
131	f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 \| q==E \|\| not (prefixStartWithE prefix2) = do	×
132	let ys = IntSet.intersection bvs xs	×
133	nv <- get	×
134	put (nv + IntSet.size ys)	×
135	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
136	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	×
137	subst1' = fmap litToMatrix s `IntMap.union` subst1	×
138	f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2	×
139	f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2') = do	1✔
140	let ys = IntSet.intersection bvs xs	×
141	nv <- get	1✔
142	put (nv + IntSet.size ys)	1✔
143	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
144	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	1✔
145	subst2' = fmap litToMatrix s `IntMap.union` subst2	×
146	f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'	×
147
148	-- XXX
149	prenexOr :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
150	prenexOr (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =	1✔
151	evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)	1✔
152	where
153	f :: Prefix -> VarSet
154	-> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
155	-> Prefix -> Prefix
156	-> State Int (Int, Prefix, Matrix)
157	f prefix _bvs subst1 subst2 [] [] = do	1✔
158	nv <- get	1✔
159	return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .\|\|. substVarMap matrix2 subst2))	1✔
160	f prefix bvs subst1 subst2 ((E,xs1) : prefix1') ((E,xs2) : prefix2') = do	×
161	let xs = IntSet.union xs1 xs2	×
162	ys = IntSet.intersection bvs xs	×
163	nv <- get	×
164	put (nv + IntSet.size ys)	×
165	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
166	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	×
167	subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1	×
168	subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2	×
169	f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'	×
170	f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 \| q==A \|\| not (prefixStartWithA prefix2)= do	×
171	let ys = IntSet.intersection bvs xs	×
172	nv <- get	×
173	put (nv + IntSet.size ys)	×
174	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
175	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	×
176	subst1' = fmap litToMatrix s `IntMap.union` subst1	×
177	f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2	×
178	f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2') = do	1✔
179	let ys = IntSet.intersection bvs xs	×
180	nv <- get	1✔
181	put (nv + IntSet.size ys)	1✔
182	let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]	×
183	xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)	1✔
184	subst2' = fmap litToMatrix s `IntMap.union` subst2	×
185	f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'	×
186
187	-- ----------------------------------------------------------------------------
188
189	solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
190	solve = solveCEGARIncremental	×
191
192	-- ----------------------------------------------------------------------------
193
194	-- \| Naive Algorithm for a Winning Move
195	solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
196	solveNaive nv prefix matrix =	×
197	case prefix' of	×
198	[] -> if Tseitin.fold undefined matrix	×
199	then return (True, Just IntSet.empty)	×
200	else return (False, Nothing)	×
201	(E,_) : _ -> do	×
202	m <- f prefix' matrix	×
203	return (isJust m, m)	×
204	(A,_) : _ -> do	×
205	m <- f prefix' matrix	×
206	return (isNothing m, m)	×
207	where
208	prefix' = normalizePrefix prefix	×
209
210	{- Naive Algorithm for a Winning Move
211	Function Solve (QX. Φ)
212	begin
213	if Φ has no quant then
214	return (Q = ∃) ? SAT(φ) : SAT(¬φ)
215	Λ ← {true, false}^X // consider all assignments
216	while true do
217	if Λ = ∅ then // all assignments used up
218	return NULL
219	τ ← pick(Λ) // pick a candidate solution
220	μ ← Solve(Φ[τ]) // find a countermove
221	if μ = NULL then // winning move
222	return τ
223	Λ ← Λ \ {τ} // remove bad candidate
224	end
225	end
226	-}
227	f :: Prefix -> Matrix -> IO (Maybe LitSet)
228	f [] _matrix = error "should not happen"	×
229	f [(q,xs)] matrix = do	×
230	solver <- SAT.newSolver	×
231	SAT.newVars_ solver nv	×
232	enc <- Tseitin.newEncoder solver	×
233	case q of	×
234	E -> Tseitin.addFormula enc matrix	×
235	A -> Tseitin.addFormula enc (notB matrix)	×
236	ret <- SAT.solve solver	×
237	if ret then do	×
238	m <- SAT.getModel solver	×
239	return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs]	×
240	else
241	return Nothing	×
242	f ((_q,xs) : prefix') matrix = do	×
243	ret <- runExceptT $ do	×
244	let moves :: [LitSet]
245	moves = map IntSet.fromList $ sequence [[x, -x] \| x <- IntSet.toList xs]	×
246	forM_ moves $ \tau -> do	×
247	ret <- lift $ f prefix' (reduct matrix tau)	×
248	case ret of	×
249	Nothing -> throwE tau	×
250	Just _nu -> return ()	×
251	case ret of	×
252	Left tau -> return (Just tau)	×
253	Right () -> return Nothing	×
254
255	-- ----------------------------------------------------------------------------
256
257	-- \| Abstraction-Based Algorithm for a Winning Move
258	solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
259	solveCEGAR nv prefix matrix =	1✔
260	case prefix' of	1✔
261	[] -> if Tseitin.fold undefined matrix	×
262	then return (True, Just IntSet.empty)	×
263	else return (False, Nothing)	1✔
264	(E,_) : _ -> do	1✔
265	m <- f nv prefix' matrix	1✔
266	return (isJust m, m)	1✔
267	(A,_) : _ -> do	1✔
268	m <- f nv prefix' matrix	1✔
269	return (isNothing m, m)	1✔
270	where
271	prefix' = normalizePrefix prefix	1✔
272
273	{-
274	Function Solve (QX. Φ)
275	begin
276	if Φ has no quant then
277	return (Q = ∃) ? SAT(φ) : SAT(¬φ)
278	ω ← ∅
279	while true do
280	α ← (Q = ∃) ? ∧_{μ∈ω} Φ[μ] : ∨_{μ∈ω} Φ[μ] // abstraction
281	τ' ← Solve(Prenex(QX.α)) // find a candidate
282	if τ' = NULL then return NULL // no winning move
283	τ ← {l \| l ∈ τ′ ∧ var(l) ∈ X} // filter a move for X
284	μ ← Solve(Φ[τ])
285	if μ = NULL then return τ
286	ω ← ω∪{μ}
287	end
288	end
289	-}
290	f :: Int -> Prefix -> Matrix -> IO (Maybe LitSet)
291	f _nv [] _matrix = error "should not happen"	×
292	f nv [(q,xs)] matrix = do	1✔
293	solver <- SAT.newSolver	1✔
294	SAT.newVars_ solver nv	1✔
295	enc <- Tseitin.newEncoder solver	1✔
296	case q of	1✔
297	E -> Tseitin.addFormula enc matrix	1✔
298	A -> Tseitin.addFormula enc (notB matrix)	1✔
299	ret <- SAT.solve solver	1✔
300	if ret then do	1✔
301	m <- SAT.getModel solver	1✔
302	return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs]	1✔
303	else
304	return Nothing	1✔
305	f nv ((q,xs) : prefix'@((_q2,_) : prefix'')) matrix = do	1✔
306	let loop counterMoves = do	1✔
307	let ys = [(nv, prefix'', reduct matrix nu) \| nu <- counterMoves]	1✔
308	(nv2, prefix2, matrix2) =
309	if q==E	1✔
310	then foldl' prenexAnd (nv,[],true) ys	1✔
311	else foldl' prenexOr (nv,[],false) ys	1✔
312	ret <- f nv2 (normalizePrefix ((q,xs) : prefix2)) matrix2	1✔
313	case ret of	1✔
314	Nothing -> return Nothing	1✔
315	Just tau' -> do	1✔
316	let tau = IntSet.filter (\l -> abs l `IntSet.member` xs) tau'	1✔
317	ret2 <- f nv prefix' (reduct matrix tau)	1✔
318	case ret2 of	1✔
319	Nothing -> return (Just tau)	1✔
320	Just nu -> loop (nu : counterMoves)	1✔
321	loop []	1✔
322
323	-- ----------------------------------------------------------------------------
324
325	-- \| Abstraction-Based Algorithm for a Winning Move
326	solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
327	solveCEGARIncremental nv prefix matrix =	1✔
328	case prefix' of	1✔
329	[] -> if Tseitin.fold undefined matrix	×
330	then return (True, Just IntSet.empty)	×
331	else return (False, Nothing)	1✔
332	(E,_) : _ -> do	1✔
333	m <- f nv IntSet.empty prefix' matrix	×
334	return (isJust m, m)	1✔
335	(A,_) : _ -> do	1✔
336	m <- f nv IntSet.empty prefix' matrix	×
337	return (isNothing m, m)	1✔
338	where
339	prefix' = normalizePrefix prefix	1✔
340
341	{-
342	Function Solve (QX. Φ)
343	begin
344	if Φ has no quant then
345	return (Q = ∃) ? SAT(φ) : SAT(¬φ)
346	ω ← ∅
347	while true do
348	α ← (Q = ∃) ? ∧_{μ∈ω} Φ[μ] : ∨_{μ∈ω} Φ[μ] // abstraction
349	τ' ← Solve(Prenex(QX.α)) // find a candidate
350	if τ' = NULL then return NULL // no winning move
351	τ ← {l \| l ∈ τ′ ∧ var(l) ∈ X} // filter a move for X
352	μ ← Solve(Φ[τ])
353	if μ = NULL then return τ
354	ω ← ω∪{μ}
355	end
356	end
357	-}
358	f :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
359	f nv _assumptions prefix matrix = do	1✔
360	solver <- SAT.newSolver	1✔
361	SAT.newVars_ solver nv	1✔
362	enc <- Tseitin.newEncoder solver	1✔
363	_xs <-
364	case last prefix of	1✔
365	(E, xs) -> do	1✔
366	Tseitin.addFormula enc matrix	1✔
367	return xs	×
368	(A, xs) -> do	1✔
369	Tseitin.addFormula enc (notB matrix)	1✔
370	return xs	×
371	let g :: Int -> LitSet -> Prefix -> Matrix -> IO (Maybe LitSet)
372	g _nv _assumptions [] _matrix = error "should not happen"	×
373	g _nv assumptions [(_q,xs)] _matrix = do	1✔
374	ret <- SAT.solveWith solver (IntSet.toList assumptions)	1✔
375	if ret then do	1✔
376	m <- SAT.getModel solver	1✔
377	return $ Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs]	1✔
378	else
379	return Nothing	1✔
380	g nv assumptions ((q,xs) : prefix'@((_q2,_) : prefix'')) matrix = do	1✔
381	let loop counterMoves = do	1✔
382	let ys = [(nv, prefix'', reduct matrix nu) \| nu <- counterMoves]	1✔
383	(nv2, prefix2, matrix2) =
384	if q==E	1✔
385	then foldl' prenexAnd (nv,[],true) ys	1✔
386	else foldl' prenexOr (nv,[],false) ys	1✔
387	ret <- f nv2 assumptions (normalizePrefix ((q,xs) : prefix2)) matrix2	×
388	case ret of	1✔
389	Nothing -> return Nothing	1✔
390	Just tau' -> do	1✔
391	let tau = IntSet.filter (\l -> abs l `IntSet.member` xs) tau'	1✔
392	ret2 <- g nv (assumptions `IntSet.union` tau) prefix' (reduct matrix tau)	1✔
393	case ret2 of	1✔
394	Nothing -> return (Just tau)	1✔
395	Just nu -> loop (nu : counterMoves)	1✔
396	loop []	1✔
397	g nv IntSet.empty prefix matrix	1✔
398
399	-- ----------------------------------------------------------------------------
400
401	data CNFOrDNF
402	= CNF [LitSet]
403	\| DNF [LitSet]
404	deriving (Show)	×
405
406	negateCNFOrDNF :: CNFOrDNF -> CNFOrDNF
407	negateCNFOrDNF (CNF xss) = DNF (map (IntSet.map negate) xss)	1✔
408	negateCNFOrDNF (DNF xss) = CNF (map (IntSet.map negate) xss)	1✔
409
410	toCNF :: Int -> CNFOrDNF -> CNF.CNF
411	toCNF nv (CNF clauses) = CNF.CNF nv (length clauses) (map (SAT.packClause . IntSet.toList) clauses)	1✔
412	toCNF nv (DNF []) = CNF.CNF nv 1 [SAT.packClause []]	1✔
413	toCNF nv (DNF cubes) = CNF.CNF (nv + length cubes) (length cs) (map SAT.packClause cs)	1✔
414	where
415	zs = zip [nv+1..] cubes	1✔
416	cs = map fst zs : [[-sel, lit] \| (sel, cube) <- zs, lit <- IntSet.toList cube]	1✔
417
418	solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
419	solveQE nv prefix matrix = do	1✔
420	store <- newCNFStore	1✔
421	SAT.newVars_ store nv	1✔
422	encoder <- Tseitin.newEncoder store	1✔
423	Tseitin.addFormula encoder matrix	1✔
424	cnf <- getCNFFormula store	1✔
425	let prefix' =	1✔
426	if CNF.cnfNumVars cnf > nv then	×
427	prefix ++ [(E, IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf])]	×
428	else
429	prefix	1✔
430	(b, m) <- solveQE_CNF (CNF.cnfNumVars cnf) prefix' (map SAT.unpackClause (CNF.cnfClauses cnf))	1✔
431	return (b, fmap (IntSet.filter (\lit -> abs lit <= nv)) m)	1✔
432
433	solveQE_CNF :: Int -> Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
434	solveQE_CNF nv prefix matrix = g (normalizePrefix prefix) matrix	1✔
435	where
436	g :: Prefix -> [SAT.Clause] -> IO (Bool, Maybe LitSet)
437	g ((E,xs) : prefix') matrix = do	1✔
438	cnf <- liftM (toCNF nv) $ f prefix' matrix	1✔
439	solver <- SAT.newSolver	1✔
440	SAT.newVars_ solver (CNF.cnfNumVars cnf)	1✔
441	forM_ (CNF.cnfClauses cnf) $ \clause -> do	1✔
442	SAT.addClause solver (SAT.unpackClause clause)	1✔
443	ret <- SAT.solve solver	1✔
444	if ret then do	1✔
445	m <- SAT.getModel solver	1✔
446	return (True, Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs])	1✔
447	else do	1✔
448	return (False, Nothing)	1✔
449	g ((A,xs) : prefix') matrix = do	1✔
450	cnf <- liftM (toCNF nv . negateCNFOrDNF) $ f prefix' matrix	1✔
451	solver <- SAT.newSolver	1✔
452	SAT.newVars_ solver (CNF.cnfNumVars cnf)	1✔
453	forM_ (CNF.cnfClauses cnf) $ \clause -> do	1✔
454	SAT.addClause solver (SAT.unpackClause clause)	1✔
455	ret <- SAT.solve solver	1✔
456	if ret then do	1✔
457	m <- SAT.getModel solver	1✔
458	return (False, Just $ IntSet.fromList [if SAT.evalLit m x then x else -x \| x <- IntSet.toList xs])	1✔
459	else do	1✔
460	return (True, Nothing)	1✔
461	g prefix matrix = do	1✔
462	ret <- f prefix matrix	1✔
463	case ret of	1✔
464	CNF xs -> return (not (any IntSet.null xs), Nothing)	1✔
465	DNF xs -> return (any IntSet.null xs, Nothing)	×
466
467	f :: Prefix -> [SAT.Clause] -> IO CNFOrDNF
468	f [] matrix = return $ CNF [IntSet.fromList clause \| clause <- matrix]	1✔
469	f ((E,xs) : prefix') matrix = do	1✔
470	cnf <- liftM (toCNF nv) $ f prefix' matrix	1✔
471	dnf <- QE.shortestImplicantsE (xs `IntSet.union` IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf]) cnf	1✔
472	return $ DNF dnf	1✔
473	f ((A,xs) : prefix') matrix = do	1✔
474	cnf <- liftM (toCNF nv . negateCNFOrDNF) $ f prefix' matrix	1✔
475	dnf <- QE.shortestImplicantsE (xs `IntSet.union` IntSet.fromList [nv+1 .. CNF.cnfNumVars cnf]) cnf	1✔
476	return $ negateCNFOrDNF $ DNF dnf	1✔
477
478	-- ----------------------------------------------------------------------------
479
480	-- ∀y ∃x. x ∧ (y ∨ ¬x)
481	_test :: IO (Bool, Maybe LitSet)
482	_test = solveNaive 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .\|\|. notB x))	×
483	where
484	x = litToMatrix 1	×
485	y = litToMatrix 2	×
486
487	_test' :: IO (Bool, Maybe LitSet)
488	_test' = solveCEGAR 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .\|\|. notB x))	×
489	where
490	x = litToMatrix 1	×
491	y = litToMatrix 2	×
492
493	_test1 :: (Int, Prefix, Matrix)
494	_test1 = prenexAnd (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], notB (litToMatrix 1))	×
495
496	_test2 :: (Int, Prefix, Matrix)
497	_test2 = prenexOr (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], litToMatrix 1)	×

msakai / toysolver / 604

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous