#include "assignments.cuh"
#include <math.h>
#include <string.h>
#include <stdio.h>
#include <assert.h>

//The two different definitions seem to have no noticable performance differnce.
//abs(a) has a tiiiny performance drop vs the other, but it's not worth being so hw-implementation specific 
//for it.
//#define FAST_32_BIT_ABS(a)((((a)>>31)^a)-((a)>>31))
#define FAST_32_BIT_ABS(a) abs(a)

//Exploits the fact LIT_TRUE is 01 and LIT_FALSE is 10. 
//
//Right side: ((l & 1) ^ (lit < 0))
//The LSB of LIT_TRUE and LIT_FALSE are true and false respectively.
//lit<0 is 1 if lit is negated, 0 otherwise, l XOR'd with (lit<0) will yield
//0^1 when not negated and true, and 1^0 when negated and false.
//
//Left side: ((l>>1) ^ (l & 1))
//To capture the other cases (LIT_ERROR=11, LIT_UNSET=00) and return 0 in both, 
//we get the two bits of error and unset as separate bits, and XOR them together
//resulting in 1 only if LIT_TRUE or LIT_FALSE.
//
//Note: On compute capability 7.X to 8.6 (currently), we get 64 "results per clock cycle per multiprocessor" on
//AND OR and XOR: https://docs.nvidia.com/cuda/cuda-c-programming-guide/index.html#arithmetic-instructions__throughput-native-arithmetic-instructions
__device__ __host__ int is_lit_sated(const assignment_t* const a, const  int32_t lit) {
	int l = get_lit(a, lit);
	return ((l >> 1) ^ (l & 1)) & ((l & 1) ^ (lit < 0));
}

__device__ __host__ int is_lit_sated_complete(const assignment_t* const a, const int32_t lit, const uint64_t altBWAssignment) {
	int l = get_lit(a, lit);
	//TODO: lit<0 appears to be branching (according to visual profiler on the 1080's) so
	//instead, try (i>>31)&0x1 to get the top bit. If it's 1 it's negative, otherwise positive. Relies on how
	//the numbers are repsesented!
	return ((l == LIT_UNSET) & (((lit < 0) & (~((altBWAssignment >> ((-lit) - 1)) & 1))) | ((lit > 0) & (((altBWAssignment >> (lit - 1)) & 1))))) | ((l != LIT_UNSET) & ((l >> 1) ^ (l & 1)) & ((l & 1) ^ (lit < 0)));
}


__device__ __host__ int clear_assignment(assignment_t* a, uint32_t litCount) {
	if (!a)
		return 0;
	//Abuse the fact LIT_UNSET is 0 and zero out memory. If LIT_UNSET changes, then: 
	//uint32_t mask = LIT_UNSET | (LIT_UNSET<<2) | (LIT_UNSET<<4) | (LIT_UNSET<<6) | (LIT_UNSET<<8) | (LIT_UNSET<<10) | (LIT_UNSET<<10) |  ...
	memset(a, 0, sizeof(assignment_t)* ASSIGNMENT_COUNT(litCount));
	return 1;
}

__device__ __host__ litval_t get_lit(const assignment_t* a, int32_t lit) {
	lit = FAST_32_BIT_ABS(lit);
	const uint32_t word = ((lit - 1) / LITS_PER_WORD);
	const uint32_t indx = (lit - 1) % LITS_PER_WORD;
	return (litval_t)((a[word] >> (indx * 2)) & 3);
}

__device__ __host__ void set_lit(assignment_t* a, int32_t lit, litval_t value) {
	lit = FAST_32_BIT_ABS(lit);
	const uint32_t word = ((lit - 1) / LITS_PER_WORD);
	const uint32_t shifts = 2 * ((lit - 1) % LITS_PER_WORD);
	a[word] = (a[word] & ~(3 << shifts)) | (value << shifts);
}

	.file	"tmpxft_0034e82c_00000000-6_assignments.cudafe1.cpp"
	.text
#APP

#NO_APP
	.type	_ZL26__cudaUnregisterBinaryUtilv, @function
_ZL26__cudaUnregisterBinaryUtilv:
.LFB2034:
	.cfi_startproc
	endbr64
	movq	_ZL20__cudaFatCubinHandle(%rip), %rdi
	jmp	__cudaUnregisterFatBinary@PLT
	.cfi_endproc
.LFE2034:
	.size	_ZL26__cudaUnregisterBinaryUtilv, .-_ZL26__cudaUnregisterBinaryUtilv
	.globl	_Z16clear_assignmentPjj
	.type	_Z16clear_assignmentPjj, @function
_Z16clear_assignmentPjj:
.LFB2029:
	.cfi_startproc
	endbr64
	testq	%rdi, %rdi
	je	.L7
	movl	%esi, %esi
	pushq	%rbx
	.cfi_def_cfa_offset 16
	.cfi_offset 3, -16
	movq	%rdi, %rbx
	cvtsi2sdq	%rsi, %xmm0
	mulsd	.LC0(%rip), %xmm0
	call	ceil@PLT
	xorl	%eax, %eax
	movq	%rbx, %rdi
	cvttsd2sil	%xmm0, %ecx
	movslq	%ecx, %rcx
	salq	$2, %rcx
	rep stosb
	movl	$1, %eax
	popq	%rbx
	.cfi_def_cfa_offset 8
	ret
.L7:
	.cfi_restore 3
	xorl	%eax, %eax
	ret
	.cfi_endproc
.LFE2029:
	.size	_Z16clear_assignmentPjj, .-_Z16clear_assignmentPjj
	.globl	_Z7get_litPKji
	.type	_Z7get_litPKji, @function
_Z7get_litPKji:
.LFB2030:
	.cfi_startproc
	endbr64
	movl	%esi, %eax
	movl	$16, %ecx
	negl	%eax
	cmovs	%esi, %eax
	decl	%eax
	cltd
	idivl	%ecx
	cltq
	leal	(%rdx,%rdx), %ecx
	movl	(%rdi,%rax,4), %eax
	shrl	%cl, %eax
	andl	$3, %eax
	ret
	.cfi_endproc
.LFE2030:
	.size	_Z7get_litPKji, .-_Z7get_litPKji
	.globl	_Z12is_lit_satedPKji
	.type	_Z12is_lit_satedPKji, @function
_Z12is_lit_satedPKji:
.LFB2027:
	.cfi_startproc
	endbr64
	call	_Z7get_litPKji
	shrl	$31, %esi
	movl	%eax, %edx
	sarl	%eax
	andl	$1, %edx
	xorl	%edx, %eax
	xorl	%edx, %esi
	andl	%esi, %eax
	ret
	.cfi_endproc
.LFE2027:
	.size	_Z12is_lit_satedPKji, .-_Z12is_lit_satedPKji
	.globl	_Z21is_lit_sated_completePKjim
	.type	_Z21is_lit_sated_completePKjim, @function
_Z21is_lit_sated_completePKjim:
.LFB2028:
	.cfi_startproc
	endbr64
	movq	%rdx, %r8
	call	_Z7get_litPKji
	movl	%esi, %ecx
	leal	-1(%rsi), %edx
	movl	%eax, %edi
	movl	%eax, %r9d
	notl	%ecx
	movq	%r8, %rax
	shrq	%cl, %rax
	movl	%esi, %ecx
	andl	$1, %r9d
	andl	$1, %eax
	shrl	$31, %ecx
	notl	%eax
	andl	%ecx, %eax
	btq	%rdx, %r8
	setc	%r8b
	xorl	%edx, %edx
	testl	%esi, %esi
	setg	%dl
	andl	%r8d, %edx
	orl	%edx, %eax
	xorl	%edx, %edx
	testl	%edi, %edi
	sete	%dl
	xorl	%esi, %esi
	andl	%edx, %eax
	movl	%edi, %edx
	sarl	%edx
	xorl	%r9d, %edx
	testl	%edi, %edi
	setne	%sil
	xorl	%r9d, %ecx
	andl	%esi, %edx
	andl	%ecx, %edx
	orl	%edx, %eax
	ret
	.cfi_endproc
.LFE2028:
	.size	_Z21is_lit_sated_completePKjim, .-_Z21is_lit_sated_completePKjim
	.globl	_Z7set_litPji8litval_t
	.type	_Z7set_litPji8litval_t, @function
_Z7set_litPji8litval_t:
.LFB2031:
	.cfi_startproc
	endbr64
	movl	%esi, %ecx
	movl	%edx, %esi
	movl	%ecx, %eax
	negl	%eax
	cmovs	%ecx, %eax
	movl	$16, %ecx
	decl	%eax
	cltd
	idivl	%ecx
	cltq
	leal	(%rdx,%rdx), %ecx
	leaq	(%rdi,%rax,4), %rdx
	movl	$3, %eax
	sall	%cl, %esi
	sall	%cl, %eax
	notl	%eax
	andl	(%rdx), %eax
	orl	%esi, %eax
	movl	%eax, (%rdx)
	ret
	.cfi_endproc
.LFE2031:
	.size	_Z7set_litPji8litval_t, .-_Z7set_litPji8litval_t
	.section	.text.startup,"ax",@progbits
	.type	_ZL24__sti____cudaRegisterAllv, @function
_ZL24__sti____cudaRegisterAllv:
.LFB2057:
	.cfi_startproc
	endbr64
	pushq	%rax
	.cfi_def_cfa_offset 16
	leaq	_ZL15__fatDeviceText(%rip), %rdi
	call	__cudaRegisterFatBinary@PLT
	movq	%rax, %rdi
	movq	%rax, _ZL20__cudaFatCubinHandle(%rip)
	call	__cudaRegisterFatBinaryEnd@PLT
	leaq	_ZL26__cudaUnregisterBinaryUtilv(%rip), %rdi
	popq	%rdx
	.cfi_def_cfa_offset 8
	jmp	atexit@PLT
	.cfi_endproc
.LFE2057:
	.size	_ZL24__sti____cudaRegisterAllv, .-_ZL24__sti____cudaRegisterAllv
	.section	.init_array,"aw"
	.align 8
	.quad	_ZL24__sti____cudaRegisterAllv
	.section	.nvFatBinSegment,"aw"
	.align 8
	.type	_ZL15__fatDeviceText, @object
	.size	_ZL15__fatDeviceText, 24
_ZL15__fatDeviceText:
	.long	1180844977
	.long	1
	.quad	fatbinData
	.quad	0
	.local	_ZL20__cudaFatCubinHandle
	.comm	_ZL20__cudaFatCubinHandle,8,8
	.section	.rodata.cst8,"aM",@progbits,8
	.align 8
.LC0:
	.long	0
	.long	1068498944
	.ident	"GCC: (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0"
	.section	.note.GNU-stack,"",@progbits
	.section	.note.gnu.property,"a"
	.align 8
	.long	1f - 0f
	.long	4f - 1f
	.long	5
0:
	.string	"GNU"
1:
	.align 8
	.long	0xc0000002
	.long	3f - 2f
2:
	.long	0x3
3:
	.align 8
4:

#ifndef ASSIGNMENTS_CUH
#define ASSIGNMENTS_CUH

#include <hip/hip_runtime.h>
#include <inttypes.h>
#define ASSIGNMENT_COUNT(a) ((int) ceil((a)/(LITS_PER_WORD*1.0)))
#define LITS_PER_WORD (16)

typedef enum { LIT_UNSET = 0, LIT_TRUE = 1, LIT_FALSE = 2, LIT_ERROR = 3 } litval_t;
typedef uint32_t assignment_t;

__device__ __host__  litval_t get_lit(const assignment_t* a, int32_t lit);
__device__ __host__ void set_lit(assignment_t* a, int32_t lit, litval_t value);
__device__ __host__ int is_lit_sated(const assignment_t* const  a, const int32_t lit);
__device__ __host__ int is_lit_sated_complete(const assignment_t* const a, const int32_t lit, const uint64_t altBWAssignment);
__device__ __host__ int clear_assignment(assignment_t* a, uint32_t litCount);
#endif
	.text
	.file	"assignments.hip"
	.type	__hip_cuid_,@object             # @__hip_cuid_
	.bss
	.globl	__hip_cuid_
__hip_cuid_:
	.byte	0                               # 0x0
	.size	__hip_cuid_, 1

	.ident	"AMD clang version 18.0.0git (https://github.com/RadeonOpenCompute/llvm-project roc-6.3.2 25012 e5bf7e55c91490b07c49d8960fa7983d864936c4)"
	.section	".note.GNU-stack","",@progbits
	.addrsig
	.addrsig_sym __hip_cuid_

	.text
	.p2alignl 7, 3214868480
	.fill 96, 4, 3214868480
	.type	__hip_cuid_,@object             ; @__hip_cuid_
	.section	.bss,"aw",@nobits
	.globl	__hip_cuid_
__hip_cuid_:
	.byte	0                               ; 0x0
	.size	__hip_cuid_, 1

	.ident	"AMD clang version 18.0.0git (https://github.com/RadeonOpenCompute/llvm-project roc-6.3.2 25012 e5bf7e55c91490b07c49d8960fa7983d864936c4)"
	.section	".note.GNU-stack","",@progbits
	.addrsig
	.addrsig_sym __hip_cuid_
	.amdgcn_target "amdgcn-amd-amdhsa--gfx1100"
	.amdgpu_metadata
---
amdhsa.kernels:  []
amdhsa.target:   amdgcn-amd-amdhsa--gfx1100
amdhsa.version:
  - 1
  - 2
...

	.end_amdgpu_metadata
