--     SATGenerator  Clausal Normal Form Satisfiability Generator
--     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/>.

-- SatGenerator.hs variables clauses
-- outputs to stdout
module Main
   where

import System.Environment
import System.Random

-- | main function
main = do
   args <- getArgs 
   let variables = args !! 0  --  first argument is number of variables
       clauses = args !! 1 --  second argument is # of clauses
       clauseLength = args !! 2 --  third argument is # of variabels per clause
   if variables == "--help"
      then putStrLn "$ SATGenerate <# of variables> <# of clauses> <# of variables per clause> > <filename.cnf>"
      else do 
         putStrLn $ "c Generated by Loki's Random CNF Generator coded in Haskell" --  outputs generated .cnf to stdout
         putStrLn $ "p cnf " ++ variables ++ " " ++ clauses
         for (read clauses) $ genClause (read variables) (read clauseLength)

-- for loop,  takes number of rotations and IO t style function as arguments
for :: Int -> IO t -> IO ()
for 0 process = return ()
for times process = do { process;  for (times-1) process; }

-- generates clauses,  takes number of variables and clause length as arguments
genClause :: Int -> Int -> IO ()
genClause numVariables 0 = putStrLn "0"
genClause numVariables clauseLength = do
   variable <- randomRIO (numVariables*(-1),numVariables)
   if variable == 0
      then genClause numVariables clauseLength
      else do 
         putStr $ (show variable) ++ " "
	 genClause numVariables (clauseLength -1)