ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros
literal.h File Reference
#include <limits.h>
#include "global.h"
Include dependency graph for literal.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define LD_MAX_VAR   30u
 
#define LD_MAX_LIT   (1 + LD_MAX_VAR)
 
#define EXTERNAL_MAX_VAR   ((1 << LD_MAX_VAR) - 1)
 
#define INTERNAL_MAX_VAR   ((1u << LD_MAX_VAR) - 2)
 
#define INTERNAL_MAX_LIT   (2 * INTERNAL_MAX_VAR + 1)
 
#define ILLEGAL_LIT   ((1u << LD_MAX_LIT) - 1)
 
#define INVALID_IDX   UINT_MAX
 
#define INVALID_LIT   UINT_MAX
 
#define VALID_INTERNAL_INDEX(IDX)
 
#define VALID_INTERNAL_LITERAL(LIT)
 
#define VALID_EXTERNAL_LITERAL(LIT)
 
#define IDX(LIT)
 
#define LIT(IDX)
 
#define NOT(LIT)
 
#define NEGATED(LIT)
 
#define STRIP(LIT)
 

Macro Definition Documentation

◆ EXTERNAL_MAX_VAR

#define EXTERNAL_MAX_VAR   ((1 << LD_MAX_VAR) - 1)

Definition at line 12 of file literal.h.

◆ IDX

#define IDX ( LIT)
Value:
(KISSAT_assert (VALID_INTERNAL_LITERAL (LIT)), (((unsigned) (LIT)) >> 1))
KISSAT_assert
#define KISSAT_assert(ignore)
Definition global.h:13
LIT
#define LIT(IDX)
Definition literal.h:31
VALID_INTERNAL_LITERAL
#define VALID_INTERNAL_LITERAL(LIT)
Definition literal.h:23

Definition at line 28 of file literal.h.

28#define IDX(LIT) \
29 (KISSAT_assert (VALID_INTERNAL_LITERAL (LIT)), (((unsigned) (LIT)) >> 1))

◆ ILLEGAL_LIT

#define ILLEGAL_LIT   ((1u << LD_MAX_LIT) - 1)

Definition at line 16 of file literal.h.

◆ INTERNAL_MAX_LIT

#define INTERNAL_MAX_LIT   (2 * INTERNAL_MAX_VAR + 1)

Definition at line 14 of file literal.h.

◆ INTERNAL_MAX_VAR

#define INTERNAL_MAX_VAR   ((1u << LD_MAX_VAR) - 2)

Definition at line 13 of file literal.h.

◆ INVALID_IDX

#define INVALID_IDX   UINT_MAX

Definition at line 18 of file literal.h.

◆ INVALID_LIT

#define INVALID_LIT   UINT_MAX

Definition at line 19 of file literal.h.

◆ LD_MAX_LIT

#define LD_MAX_LIT   (1 + LD_MAX_VAR)

Definition at line 10 of file literal.h.

◆ LD_MAX_VAR

#define LD_MAX_VAR   30u

Definition at line 9 of file literal.h.

◆ LIT

#define LIT ( IDX)
Value:
(KISSAT_assert (VALID_INTERNAL_INDEX (IDX)), ((IDX) << 1))
VALID_INTERNAL_INDEX
#define VALID_INTERNAL_INDEX(IDX)
Definition literal.h:21
IDX
#define IDX(LIT)
Definition literal.h:28

Definition at line 31 of file literal.h.

◆ NEGATED

#define NEGATED ( LIT)
Value:
(KISSAT_assert (VALID_INTERNAL_LITERAL (LIT)), ((LIT) & 1u))

Definition at line 35 of file literal.h.

◆ NOT

#define NOT ( LIT)
Value:
(KISSAT_assert (VALID_INTERNAL_LITERAL (LIT)), ((LIT) ^ 1u))

Definition at line 33 of file literal.h.

◆ STRIP

#define STRIP ( LIT)
Value:
(KISSAT_assert (VALID_INTERNAL_LITERAL (LIT)), ((LIT) & ~1u))

Definition at line 37 of file literal.h.

◆ VALID_EXTERNAL_LITERAL

#define VALID_EXTERNAL_LITERAL ( LIT)
Value:
((LIT) && ((LIT) != INT_MIN) && ABS (LIT) <= EXTERNAL_MAX_VAR)
EXTERNAL_MAX_VAR
#define EXTERNAL_MAX_VAR
Definition literal.h:12
ABS
#define ABS(a)
Definition util_old.h:250

Definition at line 25 of file literal.h.

25#define VALID_EXTERNAL_LITERAL(LIT) \
26 ((LIT) && ((LIT) != INT_MIN) && ABS (LIT) <= EXTERNAL_MAX_VAR)

◆ VALID_INTERNAL_INDEX

#define VALID_INTERNAL_INDEX ( IDX)
Value:
((IDX) < VARS)
VARS
#define VARS
Definition internal.h:250

Definition at line 21 of file literal.h.

◆ VALID_INTERNAL_LITERAL

#define VALID_INTERNAL_LITERAL ( LIT)
Value:
((LIT) < LITS)
LITS
#define LITS
Definition internal.h:251

Definition at line 23 of file literal.h.