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.
 
 
 
 
 

265 lines
6.6 KiB

/* 2012 (C) Jussi Rintanen, jrintanen.jr@gmail.com */
#if defined(__LP64__)
#define PTRINT long
#else
#define PTRINT int
#endif
typedef struct _thread {
int cround; /* Counter which is incremented for new conflict clauses */
int maxwasseen;
int *wasseen; /* Counter when literal was last encountered */
#define MAXCCLENGTH 10000000
int cc[MAXCCLENGTH]; /* Conflict clause which is being constructed */
#ifndef FUIP
int stck[MAXCCLENGTH]; /* The stack used during computing the conflict clause */
#endif
} thread;
thread *threads;
#define SVAR(v) (v)
#define ACTVAR(a) ((a)+(sati->nOfSVars))
#define TVAR(v,t) ((v)+(t)*(sati->nOfVarsPerTime))
#define TLIT(l,t) ((l)+2*(t)*(sati->nOfVarsPerTime))
#define TACT(a,t) ((ACTVAR(a))+(t)*(sati->nOfVarsPerTime))
typedef struct _nintlist { int hd; struct _nintlist *tl; } nintlist;
/*********************** VARIABLES *******************/
#define STATUSTYPE char
/************* LITERALS & WATCH LISTS *****************/
/* The watch list has the watch list EMBEDDED in the clause data structure
(Biere et al. ???)
*/
#define LITWATCHES(l) (sati->lits[(l)].watches)
typedef struct _literal {
int *watches;
#ifdef WEIGHTS
short score; /* Scores for choosing decision variables */
#endif
} literal;
/********************** HEAP *********************/
/* Heap for keeping track of the highest score variables.
Each element in the heap has two components:
k: key, i.e. the index of the variable
v: value, i.e. the current VSIDS score/weight
*/
typedef struct {
int k;
short v;
} pair;
typedef struct _heap {
int els;
int maxels;
pair *array;
} *heap;
/******************* SAT INSTANCE *******************/
#define REASONDLEVEL
#ifdef REASONDLEVEL
typedef struct {
PTRINT reason;
int dlevel;
} RD;
#endif
typedef struct _satinstance {
short id; /* Unique integer id for the instance */
int thread; /* The thread this is run in. */
short value; /* The truth-value of the instance, -1 = unknown */
int nOfVars; /* Number of propositional variables */
int nOfVarsPerTime; /* Number of vars per time point */
short nOfTPoints; /* Number of time points */
nintlist **l2its; /* Array for 2-literal clauses (for all time points), non-changing */
int **al2its; /* Array for 2-literal clauses (for all time points), non-changing */
literal *lits; /* Data structure for literals */
int *declevels;
#ifdef COSTS
int declevelscost;
#endif
#if defined REPRTWO || defined REPRFOUR
#define VALTYPE int
#else
#define VALTYPE char
#endif
VALTYPE *variableval;
int dlevel; /* Current decision level of the SAT instance. */
int decisions; /* How many decision made */
int conflicts; /* How many conflicts */
int decaysteps; /* Counter for variable weight decays */
int conflicttype2lit;
int *conflictclause; /* Clause that was falsified */
int conflictl1; /* Following four set when empty clause derived. */
int conflictl2;
#ifndef MULTICORE
int cc[MAXCCLENGTH]; /* Conflict clause which is being constructed */
#ifndef FUIP
int stck[MAXCCLENGTH]; /* The stack used during computing the conflict clause */
#endif
#endif
#ifdef VSIDS
STATUSTYPE *variablestatus;
/* These are the status bits.
bit 0 is phase there?
bit 1 phase
bit 2 dirty? (whether inferred with the goal clauses)
*/
#define VARSTATUS(v) (sati->variablestatus[(v)])
#endif
#ifndef REASONDLEVEL
PTRINT *variablereason;
int *variabledlevel;
#define LITREASON(l) (sati->variablereason[VAR(l)])
#define LITDLEVEL(l) (sati->variabledlevel[VAR(l)])
#else
RD *variablerd;
#define LITREASON(l) (sati->variablerd[VAR(l)].reason)
#define LITDLEVEL(l) (sati->variablerd[VAR(l)].dlevel)
#endif
#ifdef VSIDS
int *hindex; /* Index of each variable in the heap. */
heap scoreheap; /* Literals ordered according to their score */
#endif
int *initialunittable; /* Table for the unit clauses in the input */
int maxinitialunits; /* The size of the table */
int initialunits; /* Number of unit clauses in the table */
int *unitstack; /* Stack of assignments made */
int endunitstack,startunitstack; /* Unprocessed part of the stack */
int nOfSVars; /* Planning: number of state variables (per time) */
int nOfActions; /* Planning number of actions (per time) */
int complete; /* true if all input clauses have been added */
int notcalledbefore; /* true if solve0 not called yet. */
/* Fields for the heuristics */
int pheuristic; /* Which planning-based heuristic to use. */
int heuristic; /* Which branching heuristic to use. */
/* Unit clauses that have been learned */
#define MAXUCC 10000
int NofUCClauses;
int UCC[MAXUCC];
/* Variables for the planning heuristic */
int heuristic_mode; /* This is 0 for actions, 1 for inertia, 2 for noops. */
int heuristic_time; /* The next two are for inertia and noops. */
int heuristic_index;
#ifdef COSTS
int costbound; /* Cost bound */
int currentcost; /* Cost of current (partial) assignment */
int *costs; /* Costs all (untimed) state variables */
#endif
#ifdef GOALWEIGHTS
int *supportsg; /* Which subgoal action supports. */
int *supportsa; /* Which action (previous decision) action supports. */
#endif
#ifdef LBD
int LBDcounter;
int *LBDflag;
#endif
} *satinstance;
typedef enum { InitC, FinalC, TransC } clausetype;
float estimateinstancesize(int,int,int);
satinstance newinstance(int,int,int,int,int);
void freeinstance(satinstance);
void addnewclause(satinstance,int,clausetype); /* Number of literals in the clause (> 2) */
void addliteral(satinstance,int,int); /* Put literal to the given loc in the clause */
void finishclause(satinstance); /* Finish adding the clause */
int add1clause(satinstance,int,clausetype); /* Add a 1-literal clause */
void add2clause(satinstance,int,int,clausetype); /* Add a 2-literal clause */
void instancecomplete();
void planningparameters(satinstance,int,int);
void setheuristic(satinstance,int);
void setpheuristic(satinstance,int);
int solve(satinstance);
int solve0(satinstance,int,int);
int noT2clauses;
void addtimedvarcost(satinstance,int,int);
int varvalue(satinstance,int);
int vartruep(satinstance,int);
int tvarvalue(satinstance,int,int);
int tvarvar(satinstance,int);
int tvartime(satinstance,int);
int VALUE(int);
int NEG(int);
int VAR(int);
int PLIT(int);
int NLIT(int);
int LIT(int);
#define UNASS -1
int propagate(satinstance);
void init_clausesets(int);
double allocatedbyCL;
float memoryused();
int flagShortCutHorizon;
void shortcuts(satinstance sati);
typedef struct _shortcutclause {
int l1,l2,tdiff;
} shortcutclause;
shortcutclause *shortcutclauses;
int nofshortcutclauses;
int maxshortcutclauses;
void nextround(satinstance sati);