--     SATSolver  Clausal Normal Form Satisfiability Solver
--     Copyright (C) 2007  Andrii Loki Zvorygin andrii.z@gmail.com
-- 
--     This program is free software: you can redistribute it and/or modify
--     it under the terms of the GNU General Public License as published by
--     the Free Software Foundation, either version 3 of the License, or
--     (at your option) any later version.
-- 
--     This program is distributed in the hope that it will be useful,
--     but WITHOUT ANY WARRANTY; without even the implied warranty of
--     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--     GNU General Public License for more details.
-- 
--     You should have received a copy of the GNU General Public License
--     along with this program.  If not, see <http://www.gnu.org/licenses/>.
module Main
   where

-- need to read .cnf file
-- find amount of variables
-- get random binary string of length equal to variables
-- then go by get lines substituting appropriate variables, if result is 1 then continue, if result is 0 then output 0 as result, once reached end with all 1's output 1

import Numeric
import System.Environment
import System.Random

main = do
   args <- getArgs
   let file = args !! 0
   fileStr <- readFile file
   let lineTokens = lines fileStr
       title = cLine lineTokens
       pLined = pLine lineTokens
       variables = (words $ pLined) !! 2 -- read $ (words $ lineTokens !! 1) !! 2
       numVariables = read variables
       clauses   = (words $ pLined) !! 3 -- (words $ lineTokens !! 1) !! 3
       numClauses = read clauses
       strTokens = words $ unlines $ cnfLine lineTokens -- convert file String to [String] by words
       intTokens = map read strTokens -- convert token [String] to [Int]
      -- positIntTokens = map posit intTokens
--       uniqueIntTokens = unique positIntTokens -- amount of variables, calculated by finding unique
       -- maxInt = getMax intTokens -- amount of variables, calculated by finding max 
--   putStrLn $ "unique variables: " ++ (show $ length uniqueIntTokens)
   if variables == "--help"
      then putStrLn "$ SATSolve <filename.cnf>"
      else do
         putStrLn $ "Loki's Shunso CNF Categorizer"
         putStrLn $ "header of CNF file:       " 
         putStr   $ title
         putStrLn $ pLined
         putStrLn $ "number of variables:      " ++ variables ++ " hex: " ++ showHex numVariables "" -- amount of variables
         putStrLn $ "number of clauses:        " ++ clauses ++ " hex: " ++ showHex (read clauses) ""
	 putStrLn $ "max variable combinations:" ++ (show ((2^(fromIntegral (read variables)))::Integer)) ++ " hex: " ++ showHex ((2^(fromIntegral (read variables)))::Integer) ""
         -- gen random binary string of length maxInt
         loopSolve intTokens numVariables numClauses


cnfLine :: [String] -- ^ takes lines of CNF file 
        -> [String] -- ^ returns only CNF containing lines 
cnfLine [] = "":[]
cnfLine (x:xs) = 
   case head x of
      'c' -> cnfLine xs
      'p' -> cnfLine xs
      _   -> (x:xs)


cLine :: [String] -- ^ takes lines of CNF file 
       -> String  -- ^ returns header 
cLine [] = ""
cLine (x:xs) =
   if head x == 'c'
      then x ++ "\n" ++ cLine xs
      else ""


pLine :: [String] -- ^ takes lines of CNF file 
       -> String  -- ^ returns p line that has number of variables and number of clauses 
pLine [] = ""
pLine (x:xs) = 
   if head x == 'p'
      then x
      else pLine xs
 

loopSolve :: [Int]  -- ^ CNF expression
           -> Int   -- ^ number of variables 
           -> Int   -- ^ number of clauses
           -> IO () -- ^ outputs solution to screen
loopSolve a b c = loopSolve2 a b c (1 :: Integer) 0 
loopSolve2 :: [Int]  -- ^ CNF expression
            -> Int   -- ^ number of variables 
            -> Int   -- ^ number of clauses
	    -> Integer   -- ^ counter for number of atempts
            -> Int   -- ^ counter for maximum clauses solved -- MAX-SAT
	    -> IO () -- ^ outputs solution to screen
loopSolve2 intTokens numVariables numClauses atempts maxResult = do
            randGen <- newStdGen
            let (varValues, result) =  runSolver intTokens numVariables randGen
            if result == numClauses
               then do 
                  putStrLn $ "assignment of variables:  " ++ (show varValues)
                  putStrLn $ "number of clauses solved: " ++ (show $ result) ++ " hex: " ++ showHex result ""
	          putStrLn $ "number of atempts:        " ++ (show atempts) ++ " hex: " ++ showHex atempts ""
                  putStrLn $ "SATisfiable"              
               else if result > maxResult
                  then do 
                     putStrLn $ "assignment of variables:  " ++ (show varValues)
                     putStrLn $ "number of clauses solved: " ++ (show $ result) ++ " hex: " ++ showHex result ""
	             putStrLn $ "number of atempts:        " ++ (show atempts) ++ " hex: " ++ showHex atempts ""
                     loopSolve2 intTokens numVariables numClauses (atempts+1) result
                  else if atempts >= ((2^(fromIntegral (numVariables)))::Integer)
	             then do
	                putStrLn $ "max number of clauses solved: " ++ (show $ result) ++ " hex: " ++ showHex result ""
	                putStrLn $ "number of atempts:            " ++ (show atempts) ++ " hex: " ++ showHex atempts ""
		        putStrLn $ "2^" ++ (show numVariables) ++ " = " ++ (show $ 2^numVariables) ++ " max variable assignment combinations reached"
                        putStrLn $ "Not SATisfiable"              
	             else loopSolve2 intTokens numVariables numClauses (atempts+1) maxResult


for :: Int  -- ^ number of times to recurse
    -> IO t -- ^ process to run
    -> IO () -- ^ output
for 0 process = return ()
for times process = do { process ; for (times -1) process; }


runSolver :: [Int] -- ^ CNF expression 
           -> Int  -- ^ number of variables 
	   -> StdGen  -- ^ random number generator 
	   -> ([Int],Int) -- ^ returns tuple with [Int] variable values and binary Int to indicate if it was solved 
runSolver intTokens maxInt randGen = 
   let varValues = getValues maxInt randGen
   in
   (varValues, maxCNF intTokens varValues)


-- | evaluates to see if completely satisfied 
evaluateCNF :: [Int] -- ^ CNF expression 
            -> [Int] -- ^ variable values 
	    -> Int -- ^ returns binary Int result 
-- ^ if assigns 1 to variable result of clause is 1
-- ^ if assigns 0 to clause return 0
-- ^ if all clauses exhausted, return 1
evaluateCNF [] values = 1
evaluateCNF (x:xs) values = 
  if x == 0  --  end of clause
    then 0 --  since end of clause reached the result of formula is 0
    else if x > 0 -- check if negation occurs
       then if values !! (x-1) == 1 -- check that value is equal to 1
          then evaluateCNF (tillAfterZero xs) values
	  else evaluateCNF xs values
       else if values !! ((x*(-1))-1) == 0 -- check that negated value is equal to 1
          then evaluateCNF (tillAfterZero xs) values
	  else evaluateCNF xs values

-- | finds amount of clauses satisfied
maxCNF :: [Int] -- ^ CNF expression 
       -> [Int] -- ^ variable values 
       -> Int   -- ^ returns Int of number of clauses solved
maxCNF [] values = 0
maxCNF (x:xs) values = 
  if x == 0  --  end of clause
    then 0 + maxCNF xs values --  since end of clause reached the result of formula is 0
    else if x > 0 -- check if negation occurs
       then if values !! (x-1) == 1 -- check that value is equal to 1
          then 1 + maxCNF (tillAfterZero xs) values
	  else 0 + maxCNF xs values
       else if values !! ((x*(-1))-1) == 0 -- check that negated value is equal to 1
          then 1 + maxCNF (tillAfterZero xs) values
	  else 0 + maxCNF xs values

tillAfterZero :: [Int] -- ^ takes [Int] CNF expression 
              -> [Int] -- ^ drops until after intercepting the first 0 returning result
tillAfterZero [] = []
tillAfterZero (x:xs) = 
   if x == 0
      then xs
      else tillAfterZero xs


getValues :: Int 	-- ^ takes number of variables
          -> StdGen     -- ^ random number generator
	  -> [Int]      -- ^ returns binary [Int] of variable values
getValues 0 rand = []
getValues max rand = 
   let (value,rand2) = randomR (0,1) rand
   in value : getValues (max-1) rand2

-- | unused, outputs unique list of Int's
unique :: [Int] -> [Int]
unique [] = []
unique (x:xs) = 
   if elem x xs
      then unique xs
      else x : unique xs
-- | unused, outputs max Int from [Int]
getMax :: [Int] -> Int
getMax [] = 0
getMax (x:xs) = 
   if length (x:xs) > 1
      then if x >= head xs
              then getMax (x:(tail xs))
              else getMax xs
      else x
-- | unused, like absolute, only returns positive integer
posit :: Int -> Int
posit x = 
   if x < 0 
      then x*(-1)
      else x