Copyright	(c) Masahiro Sakai 2016
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	BangPatterns

ToySolver.QBF

Description

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

Synopsis

data Quantifier
- = E
- | A
type Prefix = [(Quantifier, VarSet)]
normalizePrefix :: Prefix -> Prefix
quantifyFreeVariables :: Int -> Prefix -> Prefix
type Matrix = Formula
litToMatrix :: Lit -> Matrix
solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveQE_CNF :: Int -> Prefix -> [Clause] -> IO (Bool, Maybe LitSet)

Documentation

data Quantifier Source #

Quantifier

Constructors

E	existential quantifier (∃)
A	universal quantifier (∀)

Instances

Instances details

Bounded Quantifier Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods minBound :: Quantifier # maxBound :: Quantifier #
Enum Quantifier Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods succ :: Quantifier -> Quantifier # pred :: Quantifier -> Quantifier # toEnum :: Int -> Quantifier # fromEnum :: Quantifier -> Int # enumFrom :: Quantifier -> [Quantifier] # enumFromThen :: Quantifier -> Quantifier -> [Quantifier] # enumFromTo :: Quantifier -> Quantifier -> [Quantifier] # enumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier] #
Read Quantifier Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods readsPrec :: Int -> ReadS Quantifier # readList :: ReadS [Quantifier] # readPrec :: ReadPrec Quantifier # readListPrec :: ReadPrec [Quantifier] #
Show Quantifier Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods showsPrec :: Int -> Quantifier -> ShowS # show :: Quantifier -> String # showList :: [Quantifier] -> ShowS #
Eq Quantifier Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods (==) :: Quantifier -> Quantifier -> Bool # (/=) :: Quantifier -> Quantifier -> Bool #
Ord Quantifier Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods compare :: Quantifier -> Quantifier -> Ordering # (<) :: Quantifier -> Quantifier -> Bool # (<=) :: Quantifier -> Quantifier -> Bool # (>) :: Quantifier -> Quantifier -> Bool # (>=) :: Quantifier -> Quantifier -> Bool # max :: Quantifier -> Quantifier -> Quantifier # min :: Quantifier -> Quantifier -> Quantifier #

type Prefix = [(Quantifier, VarSet)] Source #

normalizePrefix :: Prefix -> Prefix Source #

quantifyFreeVariables :: Int -> Prefix -> Prefix Source #

type Matrix = Formula Source #

litToMatrix :: Lit -> Matrix Source #

solve :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet) Source #

solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet) Source #

Naive Algorithm for a Winning Move

solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet) Source #

Abstraction-Based Algorithm for a Winning Move

solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet) Source #

Abstraction-Based Algorithm for a Winning Move

solveQE :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet) Source #

solveQE_CNF :: Int -> Prefix -> [Clause] -> IO (Bool, Maybe LitSet) Source #