<commit_before>/**************************************************************************
  BDD demonstration of the N-Queen chess problem.
  -----------------------------------------------
  The BDD variables correspond to a NxN chess board like:

     0    N      2N     ..  N*N-N
     1    N+1    2N+1   ..  N*N-N+1
     2    N+2    2N+2   ..  N*N-N+2
     ..   ..     ..     ..  ..
     N-1  2N-1   3N-1   ..  N*N-1

   So for example a 4x4 is:

     0 4  8 12
     1 5  9 13
     2 6 10 14
     3 7 11 15

   One solution is then that 2,4,11,13 should be true, meaning a queen
   should be placed there:

     . X . .
     . . . X
     X . . .
     . . X .

**************************************************************************/
#include <stdlib.h>
#include <stdio.h>

#include "bddlib.h"

int N;                   /* Size of the chess board */
bdd_t **X;               /* BDD variable array */
bdd_t queen;             /* N-queen problem express as a BDD */
bdd_mgr_t *mgr;

static void
ref (bdd_t b)
{
    bdd_inc_ref (mgr, b);
    /* bdd_mgr_perform_gc (mgr); */
}

static void
deref (bdd_t b)
{
    bdd_dec_ref (mgr, b);
}

/* Build the requirements for all other fields than (i,j) assuming
   that (i,j) has a queen */
static void build(int i, int j)
{
    bdd_t a, b, c, d;
    bdd_t ab, abc, abcd, queen_abcd;
    int k,l;

    a = bdd_true;
    ref (a);
    b = bdd_true;
    ref (b);
    c = bdd_true;
    ref (c);
    d = bdd_true;
    ref (d);
   
    /* No one in the same column */
    for (l=0 ; l<N ; l++)
        if (l != j) {
            bdd_t tmp1, tmp2, tmp3;
            tmp1 = bdd_not (mgr, X[i][l]);
            ref (tmp1);
            tmp2 = bdd_implies (mgr, X[i][j], tmp1);
            ref (tmp2);
            tmp3 = bdd_and (mgr, a, tmp2);
            ref (tmp3);
            deref (a);
            a = tmp3;
            ref (a);
            deref (tmp3);
            deref (tmp2);
            deref (tmp1);
        }

    /* No one in the same row */
    for (k=0 ; k<N ; k++)
        if (k != i) {
            bdd_t tmp1, tmp2, tmp3;
            tmp1 = bdd_not (mgr, X[k][j]);
            ref (tmp1);
            tmp2 = bdd_implies (mgr, X[i][j], tmp1);
            ref (tmp2);
            tmp3 = bdd_and (mgr, b, tmp2);
            ref (tmp3);
            deref (b);
            b = tmp3;
            ref (b);
            deref (tmp3);
            deref (tmp2);
            deref (tmp1);
        }

    /* No one in the same up-right diagonal */
    for (k=0 ; k<N ; k++)
    {
        int ll = k-i+j;
        if (ll>=0 && ll<N)
            if (k != i) {
                bdd_t tmp1, tmp2, tmp3;
                tmp1 = bdd_not (mgr, X[k][ll]);
                ref (tmp1);
                tmp2 = bdd_implies (mgr, X[i][j], tmp1);
                ref (tmp2);
                tmp3 = bdd_and (mgr, c, tmp2);
                ref (tmp3);
                deref (c);
                c = tmp3;
                ref (c);
                deref (tmp3);
                deref (tmp2);
                deref (tmp1);
            }
    }

    /* No one in the same down-right diagonal */
    for (k=0 ; k<N ; k++)
    {
        int ll = i+j-k;
        if (ll>=0 && ll<N)
            if (k != i) {
                bdd_t tmp1, tmp2, tmp3;
                tmp1 = bdd_not (mgr, X[k][ll]);
                ref (tmp1);
                tmp2 = bdd_implies (mgr, X[i][j], tmp1);
                ref (tmp2);
                tmp3 = bdd_and (mgr, d, tmp2);
                ref (tmp3);
                deref (d);
                d = tmp3;
                ref (d);
                deref (tmp3);
                deref (tmp2);
                deref (tmp1);
            }
    }

    ab = bdd_and (mgr, a, b);
    ref (ab);
    abc = bdd_and (mgr, ab, c);
    ref (abc);
    abcd = bdd_and (mgr, abc, d);
    ref (abcd);
    queen_abcd = bdd_and (mgr, queen, abcd);
    ref (queen_abcd);
    deref (queen);
    queen = queen_abcd;
    ref (queen);

    deref (ab);
    deref (abc);
    deref (abcd);
    deref (queen_abcd);
    deref (d);
    deref (c);
    deref (b);
    deref (a);
}


int main(int ac, char **av)
{
    int n,i,j;

    if (ac != 2)
    {
        fprintf(stderr, "USAGE:  queen N\n");
        return 1;
    }

    N = atoi(av[1]);
    if (N <= 0)
    {
        fprintf(stderr, "USAGE:  queen N\n");
        return 1;
    }

    /* Initialize with 100000 nodes, 10000 cache entries and NxN variables */
    mgr = bdd_mgr_create_with_hint(N*N, 1024);

    fprintf (stderr, "initialized manager\n");

    queen = bdd_true;
    ref (queen);
   
    /* Build variable array */
    X = (bdd_t **) malloc (N * sizeof(bdd_t**));
    for (n=0 ; n<N ; n++)
        X[n] = (bdd_t *) malloc (N * sizeof(bdd_t*));

    fprintf (stderr, "allocated variable array\n");

    for (i=0 ; i<N ; i++)
        for (j=0 ; j<N ; j++) {
            X[i][j] = bdd_ith_var(mgr, i*N+j);
            ref (X[i][j]);
            fprintf (stderr, "added variable for %dx%d\n", i, j);
        }


    fprintf (stderr, "built variable array\n");

    /* Place a queen in each row */<commit_msg>increase initial manager size to 16M nodes<commit_after>/**************************************************************************
  BDD demonstration of the N-Queen chess problem.
  -----------------------------------------------
  The BDD variables correspond to a NxN chess board like:

     0    N      2N     ..  N*N-N
     1    N+1    2N+1   ..  N*N-N+1
     2    N+2    2N+2   ..  N*N-N+2
     ..   ..     ..     ..  ..
     N-1  2N-1   3N-1   ..  N*N-1

   So for example a 4x4 is:

     0 4  8 12
     1 5  9 13
     2 6 10 14
     3 7 11 15

   One solution is then that 2,4,11,13 should be true, meaning a queen
   should be placed there:

     . X . .
     . . . X
     X . . .
     . . X .

**************************************************************************/
#include <stdlib.h>
#include <stdio.h>

#include "bddlib.h"

int N;                   /* Size of the chess board */
bdd_t **X;               /* BDD variable array */
bdd_t queen;             /* N-queen problem express as a BDD */
bdd_mgr_t *mgr;

static void
ref (bdd_t b)
{
    bdd_inc_ref (mgr, b);
    /* bdd_mgr_perform_gc (mgr); */
}

static void
deref (bdd_t b)
{
    bdd_dec_ref (mgr, b);
}

/* Build the requirements for all other fields than (i,j) assuming
   that (i,j) has a queen */
static void build(int i, int j)
{
    bdd_t a, b, c, d;
    bdd_t ab, abc, abcd, queen_abcd;
    int k,l;

    a = bdd_true;
    ref (a);
    b = bdd_true;
    ref (b);
    c = bdd_true;
    ref (c);
    d = bdd_true;
    ref (d);
   
    /* No one in the same column */
    for (l=0 ; l<N ; l++)
        if (l != j) {
            bdd_t tmp1, tmp2, tmp3;
            tmp1 = bdd_not (mgr, X[i][l]);
            ref (tmp1);
            tmp2 = bdd_implies (mgr, X[i][j], tmp1);
            ref (tmp2);
            tmp3 = bdd_and (mgr, a, tmp2);
            ref (tmp3);
            deref (a);
            a = tmp3;
            ref (a);
            deref (tmp3);
            deref (tmp2);
            deref (tmp1);
        }

    /* No one in the same row */
    for (k=0 ; k<N ; k++)
        if (k != i) {
            bdd_t tmp1, tmp2, tmp3;
            tmp1 = bdd_not (mgr, X[k][j]);
            ref (tmp1);
            tmp2 = bdd_implies (mgr, X[i][j], tmp1);
            ref (tmp2);
            tmp3 = bdd_and (mgr, b, tmp2);
            ref (tmp3);
            deref (b);
            b = tmp3;
            ref (b);
            deref (tmp3);
            deref (tmp2);
            deref (tmp1);
        }

    /* No one in the same up-right diagonal */
    for (k=0 ; k<N ; k++)
    {
        int ll = k-i+j;
        if (ll>=0 && ll<N)
            if (k != i) {
                bdd_t tmp1, tmp2, tmp3;
                tmp1 = bdd_not (mgr, X[k][ll]);
                ref (tmp1);
                tmp2 = bdd_implies (mgr, X[i][j], tmp1);
                ref (tmp2);
                tmp3 = bdd_and (mgr, c, tmp2);
                ref (tmp3);
                deref (c);
                c = tmp3;
                ref (c);
                deref (tmp3);
                deref (tmp2);
                deref (tmp1);
            }
    }

    /* No one in the same down-right diagonal */
    for (k=0 ; k<N ; k++)
    {
        int ll = i+j-k;
        if (ll>=0 && ll<N)
            if (k != i) {
                bdd_t tmp1, tmp2, tmp3;
                tmp1 = bdd_not (mgr, X[k][ll]);
                ref (tmp1);
                tmp2 = bdd_implies (mgr, X[i][j], tmp1);
                ref (tmp2);
                tmp3 = bdd_and (mgr, d, tmp2);
                ref (tmp3);
                deref (d);
                d = tmp3;
                ref (d);
                deref (tmp3);
                deref (tmp2);
                deref (tmp1);
            }
    }

    ab = bdd_and (mgr, a, b);
    ref (ab);
    abc = bdd_and (mgr, ab, c);
    ref (abc);
    abcd = bdd_and (mgr, abc, d);
    ref (abcd);
    queen_abcd = bdd_and (mgr, queen, abcd);
    ref (queen_abcd);
    deref (queen);
    queen = queen_abcd;
    ref (queen);

    deref (ab);
    deref (abc);
    deref (abcd);
    deref (queen_abcd);
    deref (d);
    deref (c);
    deref (b);
    deref (a);
}


int main(int ac, char **av)
{
    int n,i,j;

    if (ac != 2)
    {
        fprintf(stderr, "USAGE:  queen N\n");
        return 1;
    }

    N = atoi(av[1]);
    if (N <= 0)
    {
        fprintf(stderr, "USAGE:  queen N\n");
        return 1;
    }

    /* Initialize with 100000 nodes, 10000 cache entries and NxN variables */
    mgr = bdd_mgr_create_with_hint(N*N, 1024 * 1024 * 16);

    fprintf (stderr, "initialized manager\n");

    queen = bdd_true;
    ref (queen);
   
    /* Build variable array */
    X = (bdd_t **) malloc (N * sizeof(bdd_t**));
    for (n=0 ; n<N ; n++)
        X[n] = (bdd_t *) malloc (N * sizeof(bdd_t*));

    fprintf (stderr, "allocated variable array\n");

    for (i=0 ; i<N ; i++)
        for (j=0 ; j<N ; j++) {
            X[i][j] = bdd_ith_var(mgr, i*N+j);
            ref (X[i][j]);
            fprintf (stderr, "added variable for %dx%d\n", i, j);
        }


    fprintf (stderr, "built variable array\n");

    /* Place a queen in each row */
{'fraction_non_alphanumeric': 0.1787359137677609, 'fraction_numerical': 0.027633512983831456, 'mean_word_length': 1.3169125993189557, 'pattern_counts': {'":': 0, '<': 27, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 40, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1014094', 'n_tokens_mistral': 3906, 'n_tokens_neox': 3762, 'n_words': 1074}