Development mirror of Jussi Rintanen’s planner Madagascar https://research.ics.aalto.fi/software/sat/madagascar/
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 

91 lines
2.3 KiB

/* 2012 (C) Jussi Rintanen, jrintanen.jr@gmail.com */
float memoryused();
void initclausedb(); /* This must be called once before adding any clauses. */
int *allocpermclause(int,int);
int *allocclause(int,int);
int clauselen(int *);
int SATinstance(int *);
void showclauses(satinstance);
void updateactivity(int *,int);
void setLBD(int *,int);
void free_clauses(int);
int GCaggressiveness;
double collectgarbage();
double allocatedbyCDB;
int clausecount;
void check_malloc_success(void *,int);
int ptr2intpad(int *); /* Calculate number of sizeof(int) to align. */
void falsifiedsomeclause(satinstance);
/* The pointers to the next clauses in which the watched literals occur
are respectively either 4 or 8 bytes (1 or 2 sizeof(int)s), depending
on whether we are in a 32 or 64 bit processor. This affects the indices
of the different fields in the clause data structure. */
#if defined(__LP64__)
#define PREFIXWORDS 8
#else
#define PREFIXWORDS 6
#endif
#if defined(__LP64__)
#define PREFIX_WATCHA -8
#define PREFIX_WATCHB -6
#else
#define PREFIX_WATCHA -6
#define PREFIX_WATCHB -5
#endif
#define PREFIX_ACTIVITY -4
#define PREFIX_LBD -3
#define PREFIX_INSTANCE -2
#define PREFIX_CLAUSELEN -1
/* Clauses in the clause data base:
location content
-6 watched literal watched clauses link 1
-5 watched literal watched clauses link 2
-4 activity
-3 LBD
-2 SAT instance number
-1 # of literals in clause
0 1st literal
1 2nd literal
. .
. .
n-1 last literal
n -1
WARNING: These fields should always be accessed with the PREFIX_xxx macros.
*/
/* Macros for accessing the pointers at c[PREFIX_WATCHA] and c[PREFIX_WATCHB].
The issue is that c[] is an integer (4 byte) array, and in 64-bit
architectures pointers are twice as long. */
#define ASSIGN_WATCHA *((PTRINT *)(c+PREFIX_WATCHA))
#define ACCESS_WATCHA *((PTRINT *)(c+PREFIX_WATCHA))
#define ADDRESS_WATCHA ((PTRINT *)(c+PREFIX_WATCHA))
#define ASSIGN_WATCHB *((PTRINT *)(c+PREFIX_WATCHB))
#define ACCESS_WATCHB *((PTRINT *)(c+PREFIX_WATCHB))
#define ADDRESS_WATCHB ((PTRINT *)(c+PREFIX_WATCHB))
#define lsASSIGN_WATCHA *((PTRINT *)(ls+PREFIX_WATCHA))
#define lsACCESS_WATCHA *((PTRINT *)(ls+PREFIX_WATCHA))
#define lsASSIGN_WATCHB *((PTRINT *)(ls+PREFIX_WATCHB))
#define lsACCESS_WATCHB *((PTRINT *)(ls+PREFIX_WATCHB))