-- Copyright (C) 2016 Peter Selinger.
--
-- This file is free software and may be distributed under the terms
-- of the MIT license. Please see the file LICENSE for details.

-- | A more convenient interface to the functionality of 
-- "SAT.MiniSat.Functional". This layer:
--
-- * permits any ordered type to be used as the type of boolean
-- variables;
--
-- * represents solutions as a 'Map' from variables to booleans.

module SAT.MiniSat.Variable where

import SAT.MiniSat.Functional
import SAT.MiniSat.Literals

import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Maybe

-- ----------------------------------------------------------------------
-- * Auxiliary functions

-- | Extract the underlying variable of a literal.
var_of_lit :: Lit a -> a
var_of_lit :: forall a. Lit a -> a
var_of_lit (Pos a
v) = a
v
var_of_lit (Neg a
v) = a
v

-- | Map a variable function over literals.
lit_map :: (a -> b) -> Lit a -> Lit b
lit_map :: forall a b. (a -> b) -> Lit a -> Lit b
lit_map a -> b
f (Pos a
x) = b -> Lit b
forall a. a -> Lit a
Pos (a -> b
f a
x)
lit_map a -> b
f (Neg a
x) = b -> Lit b
forall a. a -> Lit a
Neg (a -> b
f a
x)

-- | Turn a list into a set and then back into a list. This sorts the
-- list and removes duplicates.
setify :: (Ord a) => [a] -> [a]
setify :: forall a. Ord a => [a] -> [a]
setify [a]
a = Set a -> [a]
forall a. Set a -> [a]
Set.toList ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a]
a)

-- ----------------------------------------------------------------------
-- * Primitive API function

-- | Compute the list of all solutions of a SAT instance.
--
-- A conjunctive normal form is represented as a list of clauses, each
-- of which is a list of literals.
--
-- A solution is represented as a (total or partial) truth assignment,
-- i.e., a map from variables to booleans.
cnf_solve_all :: (Ord v) => [[Lit v]] -> [Map v Bool]
cnf_solve_all :: forall v. Ord v => [[Lit v]] -> [Map v Bool]
cnf_solve_all [[Lit v]]
cnf = [Map v Bool]
results where
  vars :: [v]
vars = [v] -> [v]
forall a. Ord a => [a] -> [a]
setify [ v
v | [Lit v]
c <- [[Lit v]]
cnf, Lit v
l <- [Lit v]
c, let v :: v
v = Lit v -> v
forall a. Lit a -> a
var_of_lit Lit v
l ]
  bij :: [(v, Int)]
bij = [v] -> [Int] -> [(v, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
vars [Int
0..]
  int_of_var :: v -> Int
int_of_var = Map v Int -> v -> Int
forall k a. Ord k => Map k a -> k -> a
(Map.!) ([(v, Int)] -> Map v Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(v, Int)]
bij)
  var_of_int :: Int -> v
var_of_int = Map Int v -> Int -> v
forall k a. Ord k => Map k a -> k -> a
(Map.!) ([(Int, v)] -> Map Int v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Int
n,v
v) | (v
v,Int
n) <- [(v, Int)]
bij ])
  m_cnf :: [[Lit Int]]
m_cnf = ([Lit v] -> [Lit Int]) -> [[Lit v]] -> [[Lit Int]]
forall a b. (a -> b) -> [a] -> [b]
map [Lit v] -> [Lit Int]
convert_clause [[Lit v]]
cnf
  convert_clause :: [Lit v] -> [Lit Int]
convert_clause [Lit v]
c = [Lit Int] -> [Lit Int]
forall a. Ord a => [a] -> [a]
setify [ (v -> Int) -> Lit v -> Lit Int
forall a b. (a -> b) -> Lit a -> Lit b
lit_map v -> Int
int_of_var Lit v
l | Lit v
l <- [Lit v]
c ]
  m_results :: [[Maybe Bool]]
m_results = [[Lit Int]] -> [[Maybe Bool]]
m_solve [[Lit Int]]
m_cnf
  results :: [Map v Bool]
results = ([Maybe Bool] -> Map v Bool) -> [[Maybe Bool]] -> [Map v Bool]
forall a b. (a -> b) -> [a] -> [b]
map [Maybe Bool] -> Map v Bool
forall {a}. [Maybe a] -> Map v a
convert_result [[Maybe Bool]]
m_results
  convert_result :: [Maybe a] -> Map v a
convert_result [Maybe a]
l = Map v a
r
    where
      r :: Map v a
r = [(v, a)] -> Map v a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Int -> v
var_of_int Int
n, a
b) | (Int
n, Just a
b) <- [Int] -> [Maybe a] -> [(Int, Maybe a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Maybe a]
l ]

-- ----------------------------------------------------------------------
-- * Derived API functions

-- | Check whether the SAT instance is satisfiable, and return a
-- satisfying assignment if there is one.
cnf_solve :: (Ord v) => [[Lit v]] -> Maybe (Map v Bool)
cnf_solve :: forall v. Ord v => [[Lit v]] -> Maybe (Map v Bool)
cnf_solve [[Lit v]]
cnf = [Map v Bool] -> Maybe (Map v Bool)
forall a. [a] -> Maybe a
listToMaybe ([[Lit v]] -> [Map v Bool]
forall v. Ord v => [[Lit v]] -> [Map v Bool]
cnf_solve_all [[Lit v]]
cnf)

-- | Check whether the SAT instance is satisfiable.
cnf_satisfiable :: (Ord v) => [[Lit v]] -> Bool
cnf_satisfiable :: forall v. Ord v => [[Lit v]] -> Bool
cnf_satisfiable [[Lit v]]
cnf = Maybe (Map v Bool) -> Bool
forall a. Maybe a -> Bool
isJust ([[Lit v]] -> Maybe (Map v Bool)
forall v. Ord v => [[Lit v]] -> Maybe (Map v Bool)
cnf_solve [[Lit v]]
cnf)