-- 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 (Pos v) = v
var_of_lit (Neg v) = v

-- | Map a variable function over literals.
lit_map :: (a -> b) -> Lit a -> Lit b
lit_map f (Pos x) = Pos (f x)
lit_map f (Neg x) = Neg (f 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 a = Set.toList (Set.fromList 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 cnf = results where
  vars = setify [ v | c <- cnf, l <- c, let v = var_of_lit l ]
  bij = zip vars [0..]
  int_of_var = (Map.!) (Map.fromList bij)
  var_of_int = (Map.!) (Map.fromList [ (n,v) | (v,n) <- bij ])
  m_cnf = map convert_clause cnf
  convert_clause c = setify [ lit_map int_of_var l | l <- c ]
  m_results = m_solve m_cnf
  results = map convert_result m_results
  convert_result l = r
    where
      r = Map.fromList [ (var_of_int n, b) | (n, Just b) <- zip [0..] 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 cnf = listToMaybe (cnf_solve_all cnf)

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