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.
 
 
 
 
 

491 lines
11 KiB

/* 2012 (C) Jussi Rintanen, jrintanen.jr@gmail.com */
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "main.h"
#include "interface.h"
#include "clausedb.h"
#include "clausesets.h"
#include "printplan.h"
#include "asyntax.h"
#include "ordintsets.h"
#include "operators.h"
#include "translate2sat.h"
#define noDEBUG
#define noASSERTS
#define noALIGNMENT /* There is a problem: the padding is not handled by GC! */
typedef struct _clausedblist {
int *block;
int permanent;
int blockptr;
struct _clausedblist *nextblock;
} clausedblist;
#if defined(__LP64__)
#define BLOCKSIZE 1024*1024*8
#else
#define BLOCKSIZE 1024*1024*2
#endif
clausedblist *cdb;
int CDBclauses;
/* Given an int *, calculate the number of sizeof(int) to the
next 64 byte alignment boundary. This is to align data structures
with cache line boundaries.
*/
int ptr2intpad(int *ptr) {
int alignment = (((int)ptr)&63) >> 2;
if(alignment) return 16-alignment;
else return 0;
}
void check_malloc_success(void *ptr,int i) {
if(ptr == NULL) {
fprintf(stderr,"ERROR: Could not allocate more memory %i.\n",i);
exit(1);
}
}
/* Clauses in the clause data base:
location content
-3 activity
-2 SAT instance number
-1 # of literals in clause
0 1st literal
1 2nd literal
. .
. .
n-1 last literal
n -1
WARNING: These should always be accessed with the indices PREFIX_xxxx
defined in clausedb.h.
*/
void initclausedb() {
cdb = (clausedblist *)malloc(sizeof(struct _clausedblist));
check_malloc_success(cdb,1);
cdb->block = (int *)malloc(BLOCKSIZE*sizeof(int));
check_malloc_success(cdb->block,2);
allocatedbyCDB = BLOCKSIZE*sizeof(int);
cdb->blockptr = 0;
cdb->permanent = 1;
cdb->nextblock = NULL;
#ifdef DEBUG
printf("FIRST CBD BLOCK %i\n",(int)cdb);
#endif
CDBclauses = 0;
clausecount = 0;
GCaggressiveness = 0; /* Remove only very old clauses. */
}
/* Update clause activity counter. The pointer is to the first literal. */
void updateactivity(int *c,int act) {
c[PREFIX_ACTIVITY] = act;
}
/* Set the LBD field of a clause. */
void setLBD(int *c,int lbd) {
c[PREFIX_LBD] = lbd;
}
/* Allocate a clause. If permflag is 1, space allocated for
the clause won't be freed or reused. */
int *allocc(int inst,int len,int permflag) {
clausedblist *cls,*temp;
int *ptr;
#ifdef ALIGNMENT
int alignment;
#endif
#ifdef MULTICORE
#pragma omp critical
#endif
{
CDBclauses += 1;
clausecount += 1;
cls = cdb;
while(cls != NULL
&& (cls->permanent != permflag
|| cls->blockptr+len+PREFIXWORDS+5 > BLOCKSIZE))
{
cls = cls->nextblock;
}
if(cls == NULL) { /* Allocate a new block. */
#ifdef DEBUG
printf("NEW CDB BLOCK (total of %i clauses now).\n",CDBclauses);
#endif
temp = cdb;
cdb = (clausedblist *)malloc(sizeof(struct _clausedblist));
check_malloc_success(cdb,3);
cdb->block = (int *)malloc(BLOCKSIZE*sizeof(int));
check_malloc_success(cdb->block,4);
allocatedbyCDB += BLOCKSIZE*sizeof(int);
cdb->permanent = permflag;
cdb->nextblock = temp;
cdb->blockptr = 0;
cls = cdb;
printf("\t\t\t\tAllocated %i MB %s(total %i MB)\n",
BLOCKSIZE/1024/1024*sizeof(int),
(permflag ? "permanent " : ""),
(int)(memoryused()));
}
#ifdef DEBUG
printf("Allocating clause %i of length %i\n",cdb->blockptr,len);
#endif
/* Allocate it from an existing block. */
#ifdef DEBUG
printf("Allocating clause %i of length %i\n",cls->blockptr,len);
#endif
/* Clauses should be aligned with cache line boundaries (16x4Bs?).
Add something to cls->blockptr to make it align.
*/
#ifdef ALIGNMENT
cls->blockptr += ptr2intpad(&(cls->block[cls->blockptr]));
#endif
ptr = &(cls->block[cls->blockptr+PREFIXWORDS]);
}
cls->block[cls->blockptr+PREFIXWORDS+PREFIX_ACTIVITY] = 0;
cls->block[cls->blockptr+PREFIXWORDS+PREFIX_LBD] = 0;
cls->block[cls->blockptr+PREFIXWORDS+PREFIX_INSTANCE] = inst;
cls->block[cls->blockptr+PREFIXWORDS+PREFIX_CLAUSELEN] = len;
cls->block[cls->blockptr+len+PREFIXWORDS] = -1;
cls->blockptr += len+1+PREFIXWORDS;
return ptr;
}
/* Extract information from a clause pointed to by ptr (the first literal.) */
int clauselen(int *ptr) {
return ptr[PREFIX_CLAUSELEN];
}
int SATinstance(int *ptr) {
return ptr[PREFIX_INSTANCE];
}
/* Allocate space for a non-permanent clause. */
int *allocpermclause(int inst,int len) { return allocc(inst,len,1); }
int *allocclause(int inst,int len) { return allocc(inst,len,0); }
/* The following has not been tested after the -2 and -3 fields were added. */
void showclauses(satinstance sati) {
clausedblist *cls;
int i,j,b;
printf("All clauses in clause db:\n");
cls = cdb;
b=0;
while(cls != NULL) {
i = 0;
while(i < cls->blockptr) {
printf("Clause at %i.%i:",b,i);
for(j=i+PREFIXWORDS;j<i+PREFIXWORDS+(cls->block[i+PREFIXWORDS+PREFIX_CLAUSELEN]);j++) {
printf(" [%i]:",cls->block[j]); printTlit(sati,cls->block[j]);
}
printf("\n");
i = i+(cls->block[i+PREFIXWORDS+PREFIX_CLAUSELEN])+PREFIXWORDS+1;
}
cls = cls->nextblock;
b += 1;
}
}
#ifdef LBD
int nofclausesinblock(clausedblist *block) {
int n = 0;
int i = 0;
while(i < block->blockptr) {
n++;
i = i+(block->block[i+PREFIXWORDS+PREFIX_CLAUSELEN])+PREFIXWORDS+1;
}
return n;
}
int nofnoninputclauses() {
clausedblist *block = cdb;
int n = 0;
while(block) {
if(block->permanent == 0) n += nofclausesinblock(block);
block = block->nextblock;
}
return n;
}
int intCmp0(int *a,int *b) {
if(*a > *b) return 1;
else return 0;
}
int medianLBD() {
int n = nofnoninputclauses();
{
int i,j;
int tmp[n];
clausedblist *block = cdb;
j = 0;
while(block != NULL) {
if(block->permanent == 0) {
i = 0;
while(i < block->blockptr) {
tmp[j++] = block->block[i+PREFIXWORDS+PREFIX_LBD];
i = i+(block->block[i+PREFIXWORDS+PREFIX_CLAUSELEN])+PREFIXWORDS+1;
}
}
block = block->nextblock;
}
qsort(tmp,j,sizeof(int),intCmp0);
return tmp[j >> 1];
}
}
#endif
/***********************************************************************/
/*** Garbage collection: reclaim space used by useless clauses. ***/
/***********************************************************************/
int uselessp(satinstance sati,int *c,int lbdbound) {
int len,age,lbd;
len = c[PREFIXWORDS+PREFIX_CLAUSELEN];
lbd = c[PREFIXWORDS+PREFIX_LBD];
age = sati->conflicts - c[PREFIXWORDS+PREFIX_ACTIVITY];
if(len <= 5) return 0;
if(age > 200000) return 1;
if(lbd < lbdbound) return 0;
if(lbd == lbdbound && age < 500) return 0;
return 1;
}
PTRINT *nextwlelement(satinstance sati,int lit,int *ls) {
if(ls[0] == lit) return &(ls[PREFIX_WATCHA]);
else {
#ifdef ASSERTS
assert(ls[1] == lit);
#endif
return &(ls[PREFIX_WATCHB]);
}
}
void findinlist(satinstance sati,int lit,int *c) {
int *ls;
if(sati->value == 0) return; /* Instance is not used any more. */
ls = sati->lits[lit].watches;
do {
if(ls == c) {
printf("Clause %ld found in the list of %i.\n",(PTRINT)c,lit);
return;
}
ls = *(nextwlelement(sati,lit,ls));
} while(ls != NULL);
printf("Clause not found!!!\n");
}
/* Remove a clause from the list of clauses in which a literal is watched. */
void removefromwlist(satinstance sati,int lit,int *c) {
int *ls;
int **prev;
if(sati->value == 0) return; /* Instance is not used any more. */
ls = sati->lits[lit].watches;
prev = &(sati->lits[lit].watches);
do {
if(ls == c) {
*prev = *(nextwlelement(sati,lit,ls));
return;
}
prev = nextwlelement(sati,lit,ls);
ls = *prev;
#ifdef ASSERTS
assert(ls != NULL);
#endif
} while(1==1);
}
/* Replace a clause by another one in the list of clauses. */
void replaceinwlist(satinstance sati,int lit,int *c1,int *c2) {
int *ls;
if(sati->value == 0) return; /* Instance is not used any more. */
ls = sati->lits[lit].watches;
if(ls==c1) {
sati->lits[lit].watches = c2;
return;
}
do {
if(ls[0] == lit) {
if(c1 == lsACCESS_WATCHA) {
lsASSIGN_WATCHA = c2;
return;
}
ls = lsACCESS_WATCHA;
} else {
#ifdef ASSERTS
assert(ls[1] == lit);
#endif
if(c1 == lsACCESS_WATCHB) {
lsASSIGN_WATCHB = c2;
return;
}
ls = lsACCESS_WATCHB;
}
#ifdef ASSERTS
assert(ls != NULL);
#endif
} while(1==1);
}
/* Delete useless clauses and free the space used by them. */
int garbagecollection() {
int i;
int freed,inst;
int ptr,fill,bytes;
clausedblist *blocks;
float freedMB;
#ifdef LBD
int lbdbound = medianLBD();
#endif
#ifdef LBD
/* printf("\t\t\t\t\t\tMedian LBD: %i\n",lbdbound); */
#endif
printf("\t\t\t\t\t\tGC:"); fflush(stdout);
freed = 0; /* Number of bytes freed. */
blocks = cdb;
while(blocks != NULL) {
ptr = 0;
fill = 0; /* Where to move clauses when compacting. */
#ifdef DEBUG
printf("Fill factor %i/%i (%.2f %, %.2f MB)",blocks->blockptr,BLOCKSIZE,((double)blocks->blockptr)*100.0/((double)BLOCKSIZE),((double)blocks->blockptr)*4.0/1024.0/1024.0);
#endif
while(ptr < blocks->blockptr) {
inst = blocks->block[ptr+PREFIXWORDS+PREFIX_INSTANCE];
bytes = blocks->block[ptr+PREFIXWORDS+PREFIX_CLAUSELEN]+PREFIXWORDS+1;
/* Test integrity */
// findinlist(seqs[inst].sati,
// blocks->block[ptr+PREFIXWORDS],
// &(blocks->block[ptr+PREFIXWORDS]));
// findinlist(seqs[inst].sati,
// blocks->block[ptr+PREFIXWORDS+1],
// &(blocks->block[ptr+PREFIXWORDS]));
if((seqs[inst].sati->value == 0)
|| (!blocks->permanent && (uselessp(seqs[inst].sati,blocks->block+ptr,lbdbound)))) { /* Useless clause? */
removefromwlist(seqs[inst].sati,
blocks->block[ptr+PREFIXWORDS],
blocks->block+ptr+PREFIXWORDS);
removefromwlist(seqs[inst].sati,
blocks->block[ptr+PREFIXWORDS+1],
blocks->block+ptr+PREFIXWORDS);
freed += bytes;
} else { /* Otherwise shift it. */
if(fill < ptr) {
replaceinwlist(seqs[inst].sati,
blocks->block[ptr+PREFIXWORDS],
blocks->block+ptr+PREFIXWORDS,
blocks->block+fill+PREFIXWORDS);
replaceinwlist(seqs[inst].sati,
blocks->block[ptr+PREFIXWORDS+1],
blocks->block+ptr+PREFIXWORDS,
blocks->block+fill+PREFIXWORDS);
for(i=0;i<bytes;i++) blocks->block[fill+i] = blocks->block[ptr+i];
}
fill += bytes;
}
ptr += bytes; /* Next clause */
}
#ifdef DEBUG
printf(" -> (%.2f %, %.2f MB).\n",
((double)fill)*100/((double)BLOCKSIZE),
((double)fill)*4.0/1024.0/1024.0);
#endif
blocks->blockptr = fill;
blocks = blocks->nextblock;
}
freedMB = ((float)freed) / (1024.0*256.0);
printf(" %.2f MB\n",freedMB); fflush(stdout);
return (int)freedMB;
}