program main

!*****************************************************************************80
!
!! cnf_io_test() tests cnf_io().
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    15 April 2022
!
!  Author:
!
!    John Burkardt
!
  implicit none

  call timestamp ( )
  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'cnf_io_test():'
  write ( *, '(a)' ) '  Fortran90 version'
  write ( *, '(a)' ) '  Test cnf_io().'

  call test01 ( )
  call test02 ( )
  call test03 ( )
  call test04 ( )
  call test05 ( )
  call test06 ( )
  call test07 ( )
!
!  Terminate.
!
  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'cnf_io_test():'
  write ( *, '(a)' ) '  Normal end of execution.'
  write ( *, '(a)' ) ' '
  call timestamp ( )

  stop 0
end
subroutine test01 ( )

!*****************************************************************************80
!
!! test01() calls cnf_write() to write a small CNF example to a CNF file.
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    23 May 2008
!
!  Author:
!
!    John Burkardt
!
  implicit none

  integer, parameter :: c_num = 2
  integer, parameter :: l_num = 5

  character ( len = 80 ) cnf_file_name
  integer, dimension ( c_num ) :: l_c_num = (/ 2, 3 /)
  integer, dimension ( l_num ) :: l_val = (/ 1, -3, 2, 3, -1 /)
  integer, parameter :: v_num = 3

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'test01():'
  write ( *, '(a)' ) '  cnf_write() can write CNF data to a CNF file.'

  cnf_file_name = 'cnf_io_v3_c2.cnf'

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Here is the data:'

  call cnf_print ( v_num, c_num, l_num, l_c_num, l_val )

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Now we call cnf_write() to store this information'
  write ( *, '(a)' ) '  in the file "' // trim ( cnf_file_name ) // '".'

  call cnf_write ( v_num, c_num, l_num, l_c_num, l_val, cnf_file_name )

  return
end
subroutine test02 ( )

!*****************************************************************************80
!
!! test02() calls cnf_header_read() to read the header of a small CNF example file.
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    01 June 2008
!
!  Author:
!
!    John Burkardt
!
  implicit none

  integer c_num
  character ( len = 80 ) cnf_file_name
  integer l_num
  integer v_num

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'test02():'
  write ( *, '(a)' ) '  cnf_header_read() reads the header of a CNF file.'

  cnf_file_name = 'cnf_io_v3_c2.cnf'

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Read the header of "' // trim ( cnf_file_name ) // '".'

  call cnf_header_read ( cnf_file_name, v_num, c_num, l_num )

  write ( *, '(a)' ) ' '
  write ( *, '(a,i8)' ) '  The number of variables       V_NUM  = ', v_num
  write ( *, '(a,i8)' ) '  The number of clauses         C_NUM  = ', c_num
  write ( *, '(a,i8)' ) '  The number of signed literals L_NUM  = ', l_num

  return
end
subroutine test03 ( )

!*****************************************************************************80
!
!! test03() calls cnf_data_read() to read the data of a small CNF example file.
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    02 June 2008
!
!  Author:
!
!    John Burkardt
!
  implicit none

  integer c_num
  character ( len = 80 ) cnf_file_name
  integer, allocatable :: l_c_num(:)
  integer l_num
  integer, allocatable :: l_val(:)
  integer v_num

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'test03():'
  write ( *, '(a)' ) '  cnf_data_read() reads the data of a CNF file.'

  cnf_file_name = 'cnf_io_v3_c2.cnf'

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Read the header of "' // trim ( cnf_file_name ) // '".'

  call cnf_header_read ( cnf_file_name, v_num, c_num, l_num )

  write ( *, '(a)' ) ' '
  write ( *, '(a,i8)' ) '  The number of variables       V_NUM  = ', v_num
  write ( *, '(a,i8)' ) '  The number of clauses         C_NUM  = ', c_num
  write ( *, '(a,i8)' ) '  The number of signed literals L_NUM  = ', l_num

  allocate ( l_c_num(c_num) )
  allocate ( l_val(l_num) )

  call cnf_data_read ( cnf_file_name, v_num, c_num, l_num, l_c_num, l_val )

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Here is the data as read from the file:'

  call cnf_print ( v_num, c_num, l_num, l_c_num, l_val )

  deallocate ( l_c_num )
  deallocate ( l_val )

  return
end
subroutine test04 ( )

!*****************************************************************************80
!
!! test04() calls cnf_write() to write a CNF example to a CNF file.
!
!  Discussion:
!
!    This formula is used as an example in the Quinn reference.
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    30 May 2008
!
!  Author:
!
!    John Burkardt
!
  implicit none

  integer, parameter :: c_num = 18
  integer, parameter :: l_num = 36

  character ( len = 80 ) cnf_file_name
  integer, dimension ( c_num ) :: l_c_num = (/ &
    2, 2, 2, 2, 2, 2, 2, 2, 2, 2, &
    2, 2, 2, 2, 2, 2, 2, 2 /)
  integer, dimension ( l_num ) :: l_val = (/ &
    1,    2, &
   -2,   -4, &
    3,    4, &
   -4,   -5, &
    5,   -6, &
    6,   -7, &
    6,    7, &
    7,  -16, &
    8,   -9, &
   -8,  -14, &
    9,   10, &
    9,  -10, &
  -10,  -11, &
   10,   12, &
   11,   12, &
   13,   14, &
   14,  -15, &
   15,   16 /)
  integer, parameter :: v_num = 16

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'test04():'
  write ( *, '(a)' ) '  cnf_write() can write CNF data to a CNF file.'

  cnf_file_name = 'cnf_io_v16_c18.cnf'

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Here is the data to be written to the file:'

  call cnf_print ( v_num, c_num, l_num, l_c_num, l_val )

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Now we call cnf_write() to store this information'
  write ( *, '(a)' ) '  in the file "' // trim ( cnf_file_name ) // '".'

  call cnf_write ( v_num, c_num, l_num, l_c_num, l_val, cnf_file_name )

  return
end
subroutine test05 ( )

!*****************************************************************************80
!
!! test05() calls cnf_header_read() to read the header of a CNF example file.
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    01 June 2008
!
!  Author:
!
!    John Burkardt
!
  implicit none

  integer c_num
  character ( len = 80 ) cnf_file_name
  integer l_num
  integer v_num

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'test05():'
  write ( *, '(a)' ) '  cnf_header_read() reads the header of a CNF file.'

  cnf_file_name = 'cnf_io_v16_c18.cnf'

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Read the header of "' // trim ( cnf_file_name ) // '".'

  call cnf_header_read ( cnf_file_name, v_num, c_num, l_num )

  write ( *, '(a)' ) ' '
  write ( *, '(a,i8)' ) '  The number of variables       V_NUM  = ', v_num
  write ( *, '(a,i8)' ) '  The number of clauses         C_NUM  = ', c_num
  write ( *, '(a,i8)' ) '  The number of signed literals L_NUM  = ', l_num

  return
end
subroutine test06 ( )

!*****************************************************************************80
!
!! test06() calls cnf_data_read() to read the data of a small CNF example file.
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    02 June 2008
!
!  Author:
!
!    John Burkardt
!
  implicit none

  integer c_num
  character ( len = 80 ) cnf_file_name
  integer, allocatable :: l_c_num(:)
  integer l_num
  integer, allocatable :: l_val(:)
  integer v_num

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'test06():'
  write ( *, '(a)' ) '  cnf_data_read() reads the data of a CNF file.'

  cnf_file_name = 'cnf_io_v16_c18.cnf'

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Read the header of "' // trim ( cnf_file_name ) // '".'

  call cnf_header_read ( cnf_file_name, v_num, c_num, l_num )

  write ( *, '(a)' ) ' '
  write ( *, '(a,i8)' ) '  The number of variables       V_NUM  = ', v_num
  write ( *, '(a,i8)' ) '  The number of clauses         C_NUM  = ', c_num
  write ( *, '(a,i8)' ) '  The number of signed literals L_NUM  = ', l_num

  allocate ( l_c_num(c_num) )
  allocate ( l_val(l_num) )

  call cnf_data_read ( cnf_file_name, v_num, c_num, l_num, l_c_num, l_val )

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Here is the data as read from the file:'

  call cnf_print ( v_num, c_num, l_num, l_c_num, l_val )

  deallocate ( l_c_num )
  deallocate ( l_val )

  return
end
subroutine test07 ( )

!*****************************************************************************80
!
!! test07() calls cnf_evaluate() to evaluate a formula.
!
!  Discussion:
!
!    This formula is used as an example in the Quinn reference.
!    Here, we seek the logical inputs that make the formula true.
!
!  Licensing:
!
!    This code is distributed under the MIT license.
!
!  Modified:
!
!    30 May 2008
!
!  Author:
!
!    John Burkardt
!
  implicit none

  integer, parameter :: c_num = 18
  integer, parameter :: l_num = 36
  integer, parameter :: v_num = 16

  logical cnf_evaluate
  logical f_val
  integer i
  integer ihi
  integer, dimension ( c_num ) :: l_c_num = (/ &
    2, 2, 2, 2, 2, 2, 2, 2, 2, 2, &
    2, 2, 2, 2, 2, 2, 2, 2 /)
  integer, dimension ( l_num ) :: l_val = (/ &
    1,    2, &
   -2,   -4, &
    3,    4, &
   -4,   -5, &
    5,   -6, &
    6,   -7, &
    6,    7, &
    7,  -16, &
    8,   -9, &
   -8,  -14, &
    9,   10, &
    9,  -10, &
  -10,  -11, &
   10,   12, &
   11,   12, &
   13,   14, &
   14,  -15, &
   15,   16 /)
  integer solution_num
  logical v_val(v_num)

  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) 'test07():'
  write ( *, '(a)' ) '  Seek inputs to a circuit that produce a 1 (TRUE) output.'
  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '  Here is the CNF data defining the formula:'

  call cnf_print ( v_num, c_num, l_num, l_c_num, l_val )
!
!  Initialize the logical vector.
!
  v_val(1:v_num) = .false.
!
!  Compute the number of binary vectors to check.
!
  ihi = 2**v_num

  write ( *, '(a)' ) ' '
  write ( *, '(a,i8)' ) '  Number of input vectors to check is  ', ihi
  write ( *, '(a)' ) ' '
  write ( *, '(a)' ) '   #       Index    ---------Input Values----------'
  write ( *, '(a)' ) ' '
!
!  Check every possible input vector.
!
  solution_num = 0

  do i = 1, ihi

    f_val = cnf_evaluate ( v_num, c_num, l_num, l_c_num, l_val, v_val )

    if ( f_val ) then
      solution_num = solution_num + 1
      write ( *, '(2x,i2,2x,i10,3x,16l1)' )  solution_num, i - 1, v_val(1:v_num)
    end if

    call lvec_next ( v_num, v_val )

  end do
!
!  Report.
!
  write ( *, '(a)' ) ' '
  write ( *, '(a,i8)' ) '  Number of solutions found was ', solution_num

  return
end