-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Utilities for symbolic predicate logic expressions
--   
--   <a>picologic</a> provides symbolic logic expressions that can be
--   integrated with the <a>picosat</a> solver.
@package picologic
@version 0.1.2

module Picologic.AST
data Expr

-- | Variable
Var :: Ident -> Expr

-- | Logical negation
Neg :: Expr -> Expr

-- | Logical conjunction
Conj :: Expr -> Expr -> Expr

-- | Logical disjunction
Disj :: Expr -> Expr -> Expr

-- | Logical biconditional
Iff :: Expr -> Expr -> Expr

-- | Material implication
Implies :: Expr -> Expr -> Expr
newtype Ident
Ident :: String -> Ident
newtype Solutions
Solutions :: [[Expr]] -> Solutions
type Ctx = Map Ident Bool

-- | Variables in expression
variables :: Expr -> [Ident]

-- | Evaluate expression.
eval :: Ctx -> Expr -> Bool

-- | Conjunctive normal form. (May result in exponential growth)
cnf :: Expr -> Expr

-- | Negation normal form. (May result in exponential growth)
nnf :: Expr -> Expr

-- | Remove tautologies.
simp :: Expr -> Expr
instance Data.Data.Data Picologic.AST.Expr
instance GHC.Classes.Ord Picologic.AST.Expr
instance GHC.Classes.Eq Picologic.AST.Expr
instance Data.Data.Data Picologic.AST.Ident
instance GHC.Show.Show Picologic.AST.Ident
instance GHC.Classes.Ord Picologic.AST.Ident
instance GHC.Classes.Eq Picologic.AST.Ident

module Picologic.Parser
parseFile :: FilePath -> IO (Either ParseError Expr)
parseExpr :: String -> Either ParseError Expr
readExpr :: String -> Expr

module Picologic.Pretty

-- | Pretty print with unicode symbols.
ppExprU :: Expr -> Doc

-- | Pretty print with ascii symbols.
ppExprA :: Expr -> Doc

-- | Pretty print into S-Expressions
ppExprLisp :: Expr -> Doc
ppSolutions :: Solutions -> String
instance GHC.Show.Show Picologic.AST.Expr

module Picologic.Solver

-- | Yield the solutions for an expression using the PicoSAT solver.
solveProp :: Expr -> IO Solutions

-- | Yield the solutions for an expression using the PicoSAT solver. The
--   Expression must be in CNF form already.
solveCNF :: Expr -> IO Solutions

-- | Yield one single solution for an expression using the PicoSAT solver.
--   The Expression must be in CNF form already.
solveOneCNF :: Expr -> IO [Expr]

-- | Yield the integer clauses given to the SAT solver.
clausesExpr :: Expr -> [[Int]]

module Picologic.Tseitin
tseitinCNF :: Expr -> Expr
dropTseitinVarsInSolutions :: Solutions -> Solutions
dropTseitinVars :: [Expr] -> [Expr]


-- | Example usage:
--   
--   <pre>
--   import Picologic
--   p, q, r :: Expr
--   p = readExpr "~(A | B)"
--   q = readExpr "(A | ~B | C) &amp; (B | D | E) &amp; (D | F)"
--   r = readExpr "(φ &lt;-&gt; ψ)"
--   </pre>
--   
--   The expression can be pretty printed using logical symbols:
--   
--   <pre>
--   &gt;&gt;&gt; ppExprU p
--   ¬(A ∨ B)
--   
--   &gt;&gt;&gt; ppExprU q
--   ((((A ∨ ¬B) ∨ C) ∧ ((B ∨ D) ∨ E)) ∧ (D ∨ F))
--   
--   &gt;&gt;&gt; ppExprU (cnf r)
--   ((φ ∧ (φ ∨ ¬ψ)) ∧ ((ψ ∨ ¬φ) ∧ ψ))
--   </pre>
--   
--   To run the expression against the SAT solver run:
--   
--   <pre>
--   &gt;&gt;&gt; solveProp p &gt;&gt;= putStrLn . ppSolutions
--   ~A ~B
--   ~A B
--   A ~B
--   </pre>
module Picologic