module bitvec_ops
  implicit none
  private
  public :: nand_eval, bulk_clause_check, ripple_carry_add, flat_circuit_eval

  integer, parameter :: MAX_BITS = 64
  integer, parameter :: MAX_CLAUSES = 4096
  integer, parameter :: MAX_VARS = 1024

contains

  pure function nand_eval(a, b) result(c)
    logical, intent(in) :: a, b
    logical :: c
    c = .not. (a .and. b)
  end function nand_eval

  subroutine bulk_clause_check(clauses, num_clauses, clause_lens, assignment, num_vars, satisfied)
    integer, intent(in) :: num_clauses, num_vars
    integer, intent(in) :: clauses(MAX_CLAUSES, MAX_VARS)
    integer, intent(in) :: clause_lens(MAX_CLAUSES)
    logical, intent(in) :: assignment(MAX_VARS)
    logical, intent(out) :: satisfied(MAX_CLAUSES)

    integer :: i, j, lit, var
    logical :: clause_sat

    do i = 1, num_clauses
      clause_sat = .false.
      do j = 1, clause_lens(i)
        lit = clauses(i, j)
        var = abs(lit)
        if (var > 0 .and. var <= num_vars) then
          if (lit > 0) then
            if (assignment(var)) then
              clause_sat = .true.
              exit
            end if
          else
            if (.not. assignment(var)) then
              clause_sat = .true.
              exit
            end if
          end if
        end if
      end do
      satisfied(i) = clause_sat
    end do
  end subroutine bulk_clause_check

  subroutine ripple_carry_add(a, b, width, result, carry_out)
    logical, intent(in) :: a(MAX_BITS), b(MAX_BITS)
    integer, intent(in) :: width
    logical, intent(out) :: result(MAX_BITS)
    logical, intent(out) :: carry_out

    integer :: i
    logical :: carry, sum_bit, a_xor_b

    carry = .false.
    do i = 1, width
      a_xor_b = a(i) .neqv. b(i)
      sum_bit = a_xor_b .neqv. carry
      carry = (a(i) .and. b(i)) .or. (a_xor_b .and. carry)
      result(i) = sum_bit
    end do
    carry_out = carry
  end subroutine ripple_carry_add

  subroutine flat_circuit_eval(gates, num_gates, inputs, num_inputs, wire_values)
    integer, intent(in) :: num_gates, num_inputs
    integer, intent(in) :: gates(MAX_VARS, 2)
    logical, intent(in) :: inputs(MAX_VARS)
    logical, intent(out) :: wire_values(MAX_VARS)

    integer :: i, in1, in2

    wire_values(1:num_inputs) = inputs(1:num_inputs)

    do i = 1, num_gates
      in1 = gates(i, 1)
      in2 = gates(i, 2)
      wire_values(num_inputs + i) = nand_eval(wire_values(in1), wire_values(in2))
    end do
  end subroutine flat_circuit_eval

end module bitvec_ops