module state_machine
  use bitvec_ops, only: nand_eval, flat_circuit_eval
  implicit none
  private
  public :: bmc_check, induction_check, BMCResult

  integer, parameter :: MAX_STATE_BITS = 32
  integer, parameter :: MAX_STEPS = 100
  integer, parameter :: MAX_VARS = 1024

  type :: BMCResult
    logical :: property_holds
    integer :: counterexample_step
    logical :: counterexample_state(MAX_STATE_BITS)
  end type BMCResult

contains

  function bmc_check(transition_gates, num_trans_gates, &
                     property_gates, num_prop_gates, &
                     init_state, state_width, bound) result(res)
    integer, intent(in) :: num_trans_gates, num_prop_gates, state_width, bound
    integer, intent(in) :: transition_gates(MAX_VARS, 2)
    integer, intent(in) :: property_gates(MAX_VARS, 2)
    logical, intent(in) :: init_state(MAX_STATE_BITS)
    type(BMCResult) :: res

    logical :: current_state(MAX_STATE_BITS)
    logical :: next_state(MAX_STATE_BITS)
    logical :: wire_values(MAX_VARS)
    logical :: prop_wires(MAX_VARS)
    integer :: step

    res%property_holds = .true.
    res%counterexample_step = -1
    current_state = .false.
    current_state(1:state_width) = init_state(1:state_width)

    do step = 0, bound - 1
      call flat_circuit_eval(property_gates, num_prop_gates, &
                             current_state, state_width, prop_wires)

      if (.not. prop_wires(state_width + num_prop_gates)) then
        res%property_holds = .false.
        res%counterexample_step = step
        res%counterexample_state(1:state_width) = current_state(1:state_width)
        return
      end if

      call flat_circuit_eval(transition_gates, num_trans_gates, &
                             current_state, state_width, wire_values)
      next_state(1:state_width) = wire_values(state_width+1:state_width+state_width)
      current_state = next_state
    end do
  end function bmc_check

  function induction_check(transition_gates, num_trans_gates, &
                           property_gates, num_prop_gates, &
                           state_width, k) result(holds)
    integer, intent(in) :: num_trans_gates, num_prop_gates, state_width, k
    integer, intent(in) :: transition_gates(MAX_VARS, 2)
    integer, intent(in) :: property_gates(MAX_VARS, 2)
    logical :: holds

    type(BMCResult) :: base_result
    logical :: init_state(MAX_STATE_BITS)

    init_state = .false.
    base_result = bmc_check(transition_gates, num_trans_gates, &
                            property_gates, num_prop_gates, &
                            init_state, state_width, k)

    holds = base_result%property_holds
  end function induction_check

end module state_machine