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

# include "satisfy_brute.h"

int main ( );
void satisfy_brute_test01 ( );
int formula_01 ( int bvec[] );
void timestamp ( );

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

int main ( )

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

    satisfy_brute_test() tests satisfy_brute().

  Licensing:

    This code is distributed under the MIT license.

  Modified:

    27 October 2022

  Author:

    John Burkardt
*/
{
  timestamp ( );
  printf ( "\n" );
  printf ( "satisfy_brute_test():\n" );
  printf ( "  C version\n" );
  printf ( "  Test satisfy_brute().\n" );

  satisfy_brute_test01 ( );
/*
  Terminate.
*/
  printf ( "\n" );
  printf ( "satisfy_brute_test():\n" );
  printf ( "  Normal end of execution.\n" );
  printf ( "\n" );
  timestamp ( );

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

void satisfy_brute_test01 ( )

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

    satisfy_brute_test01() tests satisfy_brute().

  Licensing:

    This code is distributed under the MIT license.

  Modified:

    27 October 2022

  Author:

    John Burkardt
*/
{
  int n;

  printf ( "\n" );
  printf ( "satisfy_brute_test01():\n" );
  printf ( "  satisfy_brute() seeks values of logical variables that make\n" );
  printf ( "  a given formula true;\n" );

  n = 23;

  satisfy_brute ( n, formula_01 );

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

int formula_01 ( int bvec[] )

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

    formula_01() evaluates a logical formula for a given assignment of variables.

  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 bvec[n], the binary inputs.

  Output:

    int formula_01, the value of the formula.
*/
{
  int value;

  value = 
       (  bvec[0]  ||  bvec[1]  )
    && ( !bvec[1]  || !bvec[3]  )
    && (  bvec[2]  ||  bvec[3]  )
    && ( !bvec[3]  || !bvec[4]  )
    && (  bvec[4]  || !bvec[5]  )
    && (  bvec[5]  || !bvec[6]  )
    && (  bvec[5]  ||  bvec[6]  )
    && (  bvec[6]  || !bvec[15] )
    && (  bvec[7]  || !bvec[8]  )
    && ( !bvec[7]  || !bvec[13] )
    && (  bvec[8]  ||  bvec[9]  )
    && (  bvec[8]  || !bvec[9]  )
    && ( !bvec[9]  || !bvec[10] )
    && (  bvec[9]  ||  bvec[11] )
    && (  bvec[10] ||  bvec[11] )
    && (  bvec[12] ||  bvec[13] )
    && (  bvec[13] || !bvec[14] )
    && (  bvec[14] ||  bvec[15] )
    && (  bvec[14] ||  bvec[16] )
    && (  bvec[17] ||  bvec[1]  )
    && (  bvec[18] || !bvec[0]  )
    && (  bvec[19] ||  bvec[1]  )
    && (  bvec[19] || !bvec[18] )
    && ( !bvec[19] || !bvec[9]  )
    && (  bvec[0]  ||  bvec[17] )
    && ( !bvec[1]  ||  bvec[20] )
    && ( !bvec[21] ||  bvec[20] )
    && ( !bvec[22] ||  bvec[20] )
    && ( !bvec[21] || !bvec[20] )
    && (  bvec[22] || !bvec[20] );

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

void timestamp ( )

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

    timestamp() prints the current YMDHMS date as a time stamp.

  Example:

    31 May 2001 09:45:54 AM

  Licensing:

    This code is distributed under the MIT license.

  Modified:

    24 September 2003

  Author:

    John Burkardt
*/
{
# define TIME_SIZE 40

  static char time_buffer[TIME_SIZE];
  const struct tm *tm;
  time_t now;

  now = time ( NULL );
  tm = localtime ( &now );

  strftime ( time_buffer, TIME_SIZE, "%d %B %Y %I:%M:%S %p", tm );

  printf ( "%s\n", time_buffer );

  return;
# undef TIME_SIZE
}