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

# include "satisfy_brute.h"

/******************************************************************************/

void i4_to_bvec ( int i4, int n, int bvec[] )

/******************************************************************************/
/*
  Purpose:

    i4_to_bvec() converts an integer into a binary vector.

  Licensing:

    This code is distributed under the MIT license.

  Modified:

    20 March 2009

  Author:

    John Burkardt

  Input:

    int I4, the integer.

    int N, the dimension of the vector.

  Output:

    int BVEC[N], the vector of binary remainders.
*/
{
  int i;

  for ( i = n - 1; 0 <= i; i-- )
  {
    bvec[i] = i4 % 2;
    i4 = i4 / 2;
  }

  return;
}
/******************************************************************************/

void satisfy_brute ( int n, int formula ( int bvec[] ) )

/******************************************************************************/
/*
  Purpose:

    satisfy_brute() solves the satisfy problem using brute force.

  Licensing:

    This code is distributed under the MIT license.

  Modified:

    27 October 2022

  Author:

    John Burkardt

  Reference:

    Michael Quinn,
    Parallel Programming in C with MPI and OpenMP,
    McGraw-Hill, 2004,
    ISBN13: 978-0071232654,
    LC: QA76.73.C15.Q55.

  Input:

    int n: the number of variables in the formula.

    int formula ( int bvec[] ): a function which evaluates the formula.
*/
{
  int *bvec;
  int i;
  int ihi;
  int j;
  int solution_num;
  int value;

  bvec = ( int * ) malloc ( n * sizeof ( int ) );

  printf ( "\n" );
  printf ( "satisfy_brute():\n" );
  printf ( "  We have a logical function of N logical arguments.\n" );
  printf ( "  We do an exhaustive search of all 2^N possibilities,\n" );
  printf ( "  seeking those inputs that make the function TRUE.\n" );
/*
  Compute the number of binary vectors to check.
*/
  ihi = 1;
  for ( i = 1; i <= n; i++ )
  {
    ihi = ihi * 2;
  }
  printf ( "\n" );
  printf ( "  The number of logical variables is N = %d\n", n );
  printf ( "  The number of input vectors to check is %d\n", ihi );
  printf ( "\n" );
  printf ( "   #       Index    ---------Input Values------------------------\n" );
  printf ( "\n" );
/*
  Check every possible input vector.
*/
  solution_num = 0;

  for ( i = 0; i < ihi; i++ )
  {
    i4_to_bvec ( i, n, bvec );

    value = formula ( bvec );

    if ( value == 1 )
    {
      solution_num = solution_num + 1;

      printf ( "  %2d  %10d:  ", solution_num, i );
      for ( j = 0; j < n; j++ )
      {
        printf ( " %d", bvec[j] );
      }
      printf ( "\n" );
    }
  }
/*
  Report.
*/
  printf ( "\n" );
  printf ( "  Number of solutions found was %d\n", solution_num );

  free ( bvec );

  return;
}