<commit_before>module Main (main) where

import BoolExpr
import BDD.Raw
import BDD.Util
import NQueens

import Control.Monad (liftM, forM_, when)
import System.Environment (getProgName, getArgs)
import System.Exit (exitFailure)
import Text.Printf (hPrintf, printf)
import System.IO (stderr)
import Data.IORef (newIORef, readIORef, writeIORef)

main :: IO ()
main = getParams >>= testQueensEquiv

getParams :: IO Int
getParams = do
    args <- getArgs
    case args of
        [n] -> case reads n of
                   [(n', "")] -> return n'
                   _ -> usage
        _ -> usage    

usage :: IO a
usage = do
    hPrintf stderr "usage: %s N\n" =<< getProgName
    exitFailure

-- testQueensEquiv :: Int -> IO ()
-- testQueensEquiv n = do
--     let (expr, _decoder) = queens n
--     let nVars = numVars expr :: Int
--     withBddMgr nVars $ \mgr -> do
--         bdd <- buildBdd mgr expr
--         numSols <- liftM realToFrac (bdd_sat_count mgr bdd) :: IO Double
--         putStr . show =<< bdd_mgr_get_num_nodes mgr
--         putStrLn " nodes in use"
--         case numDistinctSolutions n of
--             Just s | fromIntegral s /= numSols -> do
--                 printf "FAILED: wrong number of solutions---expected %d, got %d\n"
--                        s (round numSols :: Int)
--                 exitFailure
--             _ -> return ()

testQueensEquiv :: Int -> IO ()
testQueensEquiv n = do
    let nVars = n * n
    withBddMgr nVars $ \mgr -> do
        bdd <- buildQueens n mgr
        numSols <- liftM realToFrac (bdd_sat_count mgr bdd) :: IO Double
        putStr . show =<< bdd_mgr_get_num_nodes mgr
        putStrLn " nodes in use"
        case numDistinctSolutions n of
            Just s | fromIntegral s /= numSols -> do
                printf "FAILED: wrong number of solutions---expected %d, got %d\n"
                       s (round numSols :: Int)
                exitFailure
            _ -> return ()


-- This is nearly a verbatim translation from the C++ N-queens
-- encoding in the BuDDy 2.4 examples.  Way more efficient than my
-- earlier encoding, for some reason.
--
-- The number of nodes does not match the BuDDy queens example
-- exactly, but if garbage collection is (effectively) disabled in
-- BuDDy, the counts are within 100 for N up to 12.
--
-- For the N-Queens problem, garbage collection makes a big
-- difference!
buildQueens :: Int -> BddMgr -> IO Bdd
buildQueens nVars mgr = do
    let n = fromIntegral nVars
        loc i j = bdd_mgr_get_ith_var mgr (i * n + j)

    queen <- newIORef bdd_true

    -- place a queen in each row
    forM_ [0..n-1] $ \i -> do
        e <- newIORef bdd_false
        forM_ [0..n-1] $ \j -> do
            eVal <- readIORef e
            writeIORef e =<< bdd_or mgr eVal =<< loc i j
        queenVal <- readIORef queen
        writeIORef queen =<< bdd_and mgr queenVal =<< readIORef e

    -- build requirements for each variable
    forM_ [0..n-1] $ \i -> do
        forM_ [0..n-1] $ \j -> do
            a <- newIORef bdd_true
            b <- newIORef bdd_true
            c <- newIORef bdd_true
            d <- newIORef bdd_true

            forM_ [0..n-1] $ \k -> do<commit_msg>Added progress output.<commit_after>module Main (main) where

import BoolExpr
import BDD.Raw
import BDD.Util
import NQueens

import Control.Monad (liftM, forM_, when)
import System.Environment (getProgName, getArgs)
import System.Exit (exitFailure)
import Text.Printf (hPrintf, printf)
import System.IO (stderr)
import Data.IORef (newIORef, readIORef, writeIORef)

main :: IO ()
main = getParams >>= testQueensEquiv

getParams :: IO Int
getParams = do
    args <- getArgs
    case args of
        [n] -> case reads n of
                   [(n', "")] -> return n'
                   _ -> usage
        _ -> usage    

usage :: IO a
usage = do
    hPrintf stderr "usage: %s N\n" =<< getProgName
    exitFailure

-- testQueensEquiv :: Int -> IO ()
-- testQueensEquiv n = do
--     let (expr, _decoder) = queens n
--     let nVars = numVars expr :: Int
--     withBddMgr nVars $ \mgr -> do
--         bdd <- buildBdd mgr expr
--         numSols <- liftM realToFrac (bdd_sat_count mgr bdd) :: IO Double
--         putStr . show =<< bdd_mgr_get_num_nodes mgr
--         putStrLn " nodes in use"
--         case numDistinctSolutions n of
--             Just s | fromIntegral s /= numSols -> do
--                 printf "FAILED: wrong number of solutions---expected %d, got %d\n"
--                        s (round numSols :: Int)
--                 exitFailure
--             _ -> return ()

testQueensEquiv :: Int -> IO ()
testQueensEquiv n = do
    let nVars = n * n
    withBddMgr nVars $ \mgr -> do
        bdd <- buildQueens n mgr
        numSols <- liftM realToFrac (bdd_sat_count mgr bdd) :: IO Double
        putStr . show =<< bdd_mgr_get_num_nodes mgr
        putStrLn " nodes in use"
        case numDistinctSolutions n of
            Just s | fromIntegral s /= numSols -> do
                printf "FAILED: wrong number of solutions---expected %d, got %d\n"
                       s (round numSols :: Int)
                exitFailure
            _ -> return ()


-- This is nearly a verbatim translation from the C++ N-queens
-- encoding in the BuDDy 2.4 examples.  Way more efficient than my
-- earlier encoding, for some reason.
--
-- The number of nodes does not match the BuDDy queens example
-- exactly, but if garbage collection is (effectively) disabled in
-- BuDDy, the counts are within 100 for N up to 12.
--
-- For the N-Queens problem, garbage collection makes a big
-- difference!
buildQueens :: Int -> BddMgr -> IO Bdd
buildQueens nVars mgr = do
    let n = fromIntegral nVars
        loc i j = bdd_mgr_get_ith_var mgr (i * n + j)

    queen <- newIORef bdd_true

    -- place a queen in each row
    forM_ [0..n-1] $ \i -> do
        e <- newIORef bdd_false
        forM_ [0..n-1] $ \j -> do
            eVal <- readIORef e
            writeIORef e =<< bdd_or mgr eVal =<< loc i j
        queenVal <- readIORef queen
        writeIORef queen =<< bdd_and mgr queenVal =<< readIORef e

    -- build requirements for each variable
    forM_ [0..n-1] $ \i -> do
        forM_ [0..n-1] $ \j -> do
            hPrintf stderr "Adding position %s,%s\n" (show i) (show j)

            a <- newIORef bdd_true
            b <- newIORef bdd_true
            c <- newIORef bdd_true
            d <- newIORef bdd_true

            forM_ [0..n-1] $ \k -> do
{'fraction_non_alphanumeric': 0.10538568989601117, 'fraction_numerical': 0.005277044854881266, 'mean_word_length': 1.8729380294248774, 'pattern_counts': {'":': 0, '<': 57, '<?xml version=': 0, '>': 45, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2853467', 'n_tokens_mistral': 2162, 'n_tokens_neox': 2103, 'n_words': 720}