File size: 2,604 Bytes
56de343 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 | 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
|