829 lines
21 KiB
C
829 lines
21 KiB
C
|
|
/* 2012 (C) Jussi Rintanen */
|
|
|
|
#define noDECDEBUG
|
|
#define noHEURDEBUG
|
|
#define noDEBUGDISJ
|
|
|
|
typedef struct {
|
|
int l; /* Will satisfy subgoal l */
|
|
int var; /* with variable var (action, conditional effect) */
|
|
short t; /* at time point t */
|
|
int flaws; /* How many later actions this action disables/affects */
|
|
} planstep;
|
|
|
|
#define MAXPLANSTEPS 1000000
|
|
planstep plansteps[MAXPLANSTEPS];
|
|
int Nsteps;
|
|
|
|
#define STACKSIZE 50000
|
|
typedef struct _stackel {
|
|
int lit;
|
|
short t;
|
|
short val;
|
|
} stackel;
|
|
|
|
int stackptr;
|
|
stackel stack[STACKSIZE];
|
|
|
|
/* Order the subgoals according to a measure.
|
|
0. No measure is used (everything is 0).
|
|
1. How early does it have to be true.
|
|
TODO: 2. How early, + how constrained.
|
|
If two are equally early, choose the one that is more constrained
|
|
in the sense that can be TRUE in a smaller number of consecutive
|
|
time points. Choosing a highly constrained subgoal leads to failures
|
|
sooner.
|
|
*/
|
|
|
|
inline int anyactionapplicable(satinstance sati,int l,int t) {
|
|
compactCEstruct *ptr;
|
|
for(ptr=cCEs[l];ptr->var != -1;ptr++) { /* All ways of making l true. */
|
|
if(!tvarfalsep(sati,ptr->var,t)) { /* Is it applicable? */
|
|
return 1;
|
|
}
|
|
}
|
|
return 0;
|
|
}
|
|
|
|
inline int goallitvalue(satinstance sati,int l,int t0) {
|
|
int t,t2;
|
|
t = t0;
|
|
switch(HEURordmode) {
|
|
case 1:
|
|
/* How long the goal lit has been true before t. */
|
|
while(t >= 0 && tlittruep(sati,l,t)) t = t - 1;
|
|
return t+1;
|
|
case 2:
|
|
/* How long the goal lit has been true before t. */
|
|
while(t >= 0 && tlittruep(sati,l,t)) t = t - 1;
|
|
t2 = t;
|
|
/* How much earlier it was last false. */
|
|
while(t2 >= 0 && !tlitfalsep(sati,l,t2)) t2 = t2-1;
|
|
return (t+1)*200+(t-t2);
|
|
case 3:
|
|
/* How long the goal lit must have been true before t (check applicability
|
|
of actions making it true!) */
|
|
t = t-1;
|
|
while(t >= 0 && anyactionapplicable(sati,l,t) == 0) t = t - 1;
|
|
return t+1;
|
|
case 4:
|
|
/* How wide is the gap in which it must be made true? */
|
|
/* WARNING: This stops depth-first! */
|
|
t = t-1;
|
|
while(t >= 0 && anyactionapplicable(sati,l,t) == 0) t = t - 1;
|
|
t2 = t;
|
|
while(t2 >= 0 && !tlitfalsep(sati,l,t2)) t2 = t2 - 1;
|
|
return t-t2;
|
|
case 5:
|
|
/* Case 1 with Case 4 as a tie-breaker. */
|
|
/* How wide is the gap in which it must be made true? */
|
|
t = t-1;
|
|
while(t >= 0 && tlittruep(sati,l,t)) t = t - 1;
|
|
t2 = t;
|
|
while(t2 >= 0 && !tlitfalsep(sati,l,t2)) t2 = t2 - 1;
|
|
return t*1000+t-t2;
|
|
case 6:
|
|
/* Case 3 with Case 4 as a tie-breaker. */
|
|
/* How wide is the gap in which it must be made true? */
|
|
t = t-1;
|
|
while(t >= 0 && anyactionapplicable(sati,l,t) == 0) t = t - 1;
|
|
t2 = t;
|
|
while(t2 >= 0 && !tlitfalsep(sati,l,t2)) t2 = t2 - 1;
|
|
return t*1000+t-t2;
|
|
default:
|
|
return 0;
|
|
}
|
|
}
|
|
|
|
void push2goalstack(satinstance sati,int l,int t) {
|
|
int v,i;
|
|
|
|
i = stackptr++;
|
|
|
|
ASSERT(stackptr < STACKSIZE);
|
|
|
|
v = goallitvalue(sati,l,t);
|
|
|
|
/* Insert the literal in the stack. Lowest .val is on top (last). */
|
|
/* This means that we have a depth-first traversal: support for
|
|
one precondition (or top-level goal) is found first, before
|
|
proceeding with another precondition (or top-level goal). */
|
|
|
|
while(i > 0 && stack[i-1].val < v) {
|
|
stack[i].lit = stack[i-1].lit;
|
|
stack[i].t = stack[i-1].t;
|
|
stack[i].val = stack[i-1].val;
|
|
i = i-1;
|
|
}
|
|
|
|
stack[i].lit = l;
|
|
stack[i].t = t;
|
|
stack[i].val = v;
|
|
}
|
|
|
|
/* Push the constituent literals of a conjunctive goal formula in the stack. */
|
|
|
|
void push2goalstackCfma(satinstance sati,fma *f,int t) {
|
|
fmalist *fs;
|
|
switch(f->t) {
|
|
case patom: push2goalstack(sati,PLIT(f->a),t); break;
|
|
case natom: push2goalstack(sati,NLIT(f->a),t); break;
|
|
case conj:
|
|
fs = f->juncts;
|
|
while(fs != NULL) {
|
|
push2goalstackCfma(sati,fs->hd,t);
|
|
fs = fs->tl;
|
|
}
|
|
break;
|
|
case TRUE: break;
|
|
default:
|
|
assert(1==2);
|
|
}
|
|
}
|
|
|
|
/* Push a subset of the literals in a general NNF formula which are
|
|
sufficient for making the formula true, in the stack.
|
|
This is as in the ICAPS'11 submission.
|
|
For conjunctions all conjuncts have to be taken.
|
|
For disjunctions one of the disjuncts is taken. If at least one of
|
|
the disjuncts is true or unknown, then the chosen disjunct cannot
|
|
be a false one.
|
|
*/
|
|
|
|
/* The implementation is in with a stack of sets of literals.
|
|
The operations are
|
|
- adding a set into the set (empty or singleton)
|
|
- taking the union of two top stacks
|
|
- removing the top or the second set from the stack
|
|
- comparing the two top sets (cardinality?) for choosing a disjunct
|
|
|
|
tset_stack: element is the index of the first element of the set in tset_store
|
|
*/
|
|
|
|
typedef struct {
|
|
int l;
|
|
short t;
|
|
} storepair;
|
|
|
|
int stacktop;
|
|
int storetop;
|
|
int tset_stack[1000];
|
|
int tset_card[1000];
|
|
storepair tset_store[100000];
|
|
|
|
#define CARDTOP (storetop-tset_stack[stacktop]+1)
|
|
#define CARD2ND (tset_stack[stacktop]-tset_stack[stacktop-1])
|
|
|
|
void tset_emptyset() {
|
|
#ifdef DEBUGDISJ
|
|
printf("tset_emptyset\n");
|
|
#endif
|
|
stacktop += 1;
|
|
tset_card[stacktop] = 0;
|
|
tset_stack[stacktop] = storetop+1;
|
|
}
|
|
|
|
void tset_show() {
|
|
#ifdef DEBUGDISJ
|
|
int i,j;
|
|
printf("=========================================================\n");
|
|
for(i=0;i<=storetop+1;i++) {
|
|
for(j=0;j<=stacktop;j++) {
|
|
if(tset_stack[j] == i) printf("START %i (card %i)\n",j,tset_card[j]);
|
|
}
|
|
if(i<=storetop) {
|
|
printf("%i: ",i); printlit(tset_store[i].l); printf("@%i\n",tset_store[i].t);
|
|
}
|
|
}
|
|
printf(" =========================================================\n");
|
|
#endif
|
|
}
|
|
|
|
/* Add the empty set in the stack. */
|
|
|
|
void tset_makeempty() {
|
|
#ifdef DEBUGDISJ
|
|
printf("tset_makeempty\n");
|
|
#endif
|
|
stacktop=-1;
|
|
storetop=-1;
|
|
tset_emptyset(); /* Always have an empty set in the stack. */
|
|
}
|
|
|
|
/* Add a singleton set into the stack. */
|
|
|
|
void tset_singleton(int l,int t) {
|
|
#ifdef DEBUGDISJ
|
|
printf("tset_singleton "); printlit(l); printf("@%i\n",t);
|
|
#endif
|
|
storetop = storetop+1;
|
|
tset_store[storetop].l = l;
|
|
tset_store[storetop].t = t;
|
|
stacktop = stacktop+1;
|
|
tset_stack[stacktop] = storetop;
|
|
tset_card[stacktop] = 1;
|
|
}
|
|
|
|
/* Take the union of the two top sets. */
|
|
|
|
void tset_union() {
|
|
#ifdef DEBUGDISJ
|
|
printf("tset_union\n");
|
|
#endif
|
|
tset_card[stacktop-1] = tset_card[stacktop-1]+tset_card[stacktop];
|
|
stacktop = stacktop - 1;
|
|
}
|
|
|
|
/* Return TRUE if top element has a smaller cardinality than the second. */
|
|
|
|
int tset_top_better() {
|
|
if(tset_card[stacktop] < tset_card[stacktop-1]) return 1; else return 0;
|
|
}
|
|
|
|
/* Remove the top set from the stack. */
|
|
|
|
void tset_top_delete() {
|
|
#ifdef DEBUGDISJ
|
|
printf("tset_top_delete\n");
|
|
#endif
|
|
storetop = storetop-tset_card[stacktop];
|
|
stacktop = stacktop-1;
|
|
}
|
|
|
|
/* Remove the second set from the stack. */
|
|
|
|
void tset_second_delete() {
|
|
int i,n;
|
|
#ifdef DEBUGDISJ
|
|
printf("tset_second_delete\n");
|
|
#endif
|
|
n = tset_card[stacktop];
|
|
/* Move the top set where the second one was. */
|
|
for(i=0;i<n;i++) {
|
|
tset_store[tset_stack[stacktop-1]+i] = tset_store[tset_stack[stacktop]+i];
|
|
}
|
|
storetop = tset_stack[stacktop-1]+n-1;
|
|
stacktop = stacktop-1;
|
|
tset_card[stacktop]=n;
|
|
}
|
|
|
|
int traverseDfma(satinstance sati,fma *f,int t) {
|
|
fmalist *fs;
|
|
int have;
|
|
|
|
#ifdef DEBUGDISJ
|
|
tset_show();
|
|
#endif
|
|
|
|
switch(f->t) {
|
|
/* Here we have to restrict to literals that are not FALSE ? */
|
|
case patom:
|
|
if(tvarfalsep(sati,f->a,t)) return 0;
|
|
tset_singleton(PLIT(f->a),t);
|
|
return 1;
|
|
case natom:
|
|
if(tvartruep(sati,f->a,t)) return 0;
|
|
tset_singleton(NLIT(f->a),t);
|
|
return 1;
|
|
case conj: /* The literal sets for all conjuncts are combined. */
|
|
tset_emptyset();
|
|
fs = f->juncts;
|
|
while(fs != NULL) {
|
|
if(traverseDfma(sati,fs->hd,t) == 0) {
|
|
tset_top_delete();
|
|
return 0;
|
|
}
|
|
tset_union();
|
|
fs = fs->tl;
|
|
}
|
|
return 1;
|
|
case disj: /* The set for one of the disjuncts is chosen, others ignored. */
|
|
// tset_emptyset(); ???????????????????
|
|
have = 0;
|
|
fs = f->juncts;
|
|
while(fs != NULL) {
|
|
if(traverseDfma(sati,fs->hd,t)) {
|
|
if(have) {
|
|
#ifdef DEBUGDISJ
|
|
tset_show();
|
|
#endif
|
|
if(tset_top_better()) tset_second_delete(); else tset_top_delete();
|
|
}
|
|
have = 1;
|
|
}
|
|
fs = fs->tl;
|
|
}
|
|
return have;
|
|
case TRUE: tset_emptyset(); return 1;
|
|
case FALSE: return 0;
|
|
}
|
|
return 0;
|
|
}
|
|
|
|
void push2goalstackDfma(satinstance sati,fma *f,int t) {
|
|
int i,l,t2;
|
|
tset_makeempty();
|
|
if(traverseDfma(sati,f,t) == 0) return;
|
|
#ifdef DEBUGDISJ
|
|
tset_show();
|
|
#endif
|
|
// if(tset_stack[stacktop]+1>storetop) printf("Not pushing anything\n");
|
|
/* Push the literals from the traverseDfma stack into the heuristic stack. */
|
|
for(i=tset_stack[stacktop];i<=storetop;i++) {
|
|
l = tset_store[i].l;
|
|
t2 = tset_store[i].t;
|
|
#ifdef DEBUGDISJ
|
|
printf("Pushing %i:",l); printlit(l); printf("@%i\n",t2);
|
|
#endif
|
|
push2goalstack(sati,l,t2);
|
|
}
|
|
}
|
|
|
|
#ifdef HARDDEBUG
|
|
void showheustack(satinstance sati) {
|
|
int i;
|
|
printf("STACK CONTENTS:\n");
|
|
for(i=0;i<stackptr;i++) {
|
|
printlit(stack[i].lit);
|
|
printf("@%i (score %i)\n",stack[i].t,stack[i].val);
|
|
}
|
|
}
|
|
#endif
|
|
|
|
#define TMPARRAYSIZE 1000
|
|
|
|
void do_cpath(satinstance);
|
|
|
|
int weightedscore(satinstance sati,int i) {
|
|
return sati->lits[PLIT(TVAR(plansteps[i].var,plansteps[i].t))].score + 10000-100*plansteps[i].flaws;
|
|
}
|
|
|
|
/* Identify actions that are useful in reaching the goals. */
|
|
|
|
int do_cpath_heuristic(satinstance sati) {
|
|
int i,j,best,besttime;
|
|
#ifdef WEIGHTS
|
|
int tmparray[TMPARRAYSIZE];
|
|
#endif
|
|
|
|
nextround(sati);
|
|
|
|
Nsteps = 0;
|
|
stackptr = 0;
|
|
|
|
switch(sati->heuristic_mode) {
|
|
|
|
case 0: /* Choose an action. */
|
|
|
|
if(goalisdisjunctive) {
|
|
push2goalstackDfma(sati,goal,sati->nOfTPoints-1);
|
|
} else {
|
|
push2goalstackCfma(sati,goal,sati->nOfTPoints-1);
|
|
}
|
|
|
|
#ifdef HARDDEBUG
|
|
showheustack(sati);
|
|
#endif
|
|
|
|
/* Find paths */
|
|
do_cpath(sati);
|
|
|
|
/* Pick action. */
|
|
|
|
/* Only one action to choose from: return it directly. */
|
|
if(Nsteps == 1) return PLIT(TVAR(plansteps[0].var,plansteps[0].t));
|
|
|
|
if(Nsteps > 0) {
|
|
|
|
switch(HEURactionchoice) {
|
|
case 0: /* Choose action randomly. */
|
|
i = random() % Nsteps;
|
|
break;
|
|
case 1: /* Choose the earliest possible action. */
|
|
best = -1;
|
|
besttime = 100000;
|
|
for(i=0;i<Nsteps;i++) {
|
|
if(plansteps[i].t < besttime) {
|
|
best = i;
|
|
besttime = plansteps[i].t;
|
|
}
|
|
}
|
|
i = best;
|
|
break;
|
|
case 2: /* Choose action randomly, with bias to earlier. */
|
|
j = random() % Nsteps;
|
|
i = random() % (j+1);
|
|
break;
|
|
case 3: /* Choose action randomly, with bias to later. */
|
|
j = random() % Nsteps;
|
|
i = Nsteps-(random() % (j+1))-1;
|
|
break;
|
|
case 4: /* Choose action based on its weight, with ties broken
|
|
randomly. */
|
|
#ifdef WEIGHTS
|
|
best = -1;
|
|
for(i=0;i< Nsteps;i++) { /* Determine the best score. */
|
|
int score = weightedscore(sati,i);
|
|
if(score > best) best = score;
|
|
}
|
|
j = 0;
|
|
for(i=0;i<Nsteps;i++) { /* Collect the literals with the best score. */
|
|
if(weightedscore(sati,i) == best) {
|
|
tmparray[j++] = i;
|
|
ASSERT(j < 1000);
|
|
}
|
|
|
|
}
|
|
i = tmparray[random() % j];
|
|
break;
|
|
#else
|
|
fprintf(stderr,"Heuristic needs WEIGHTS compiled.\n");
|
|
exit(1);
|
|
#endif
|
|
}
|
|
|
|
return PLIT(TVAR(plansteps[i].var,plansteps[i].t));
|
|
// return TLIT(plansteps[i].l,plansteps[i].t);
|
|
|
|
}
|
|
|
|
sati->heuristic_mode = 1;
|
|
sati->heuristic_time = 1;
|
|
sati->heuristic_index = 0;
|
|
|
|
case 1: /* No actions needed. Do inertia. */
|
|
|
|
#ifdef HEURDEBUG
|
|
printf("Doing INERTIA\n");
|
|
#endif
|
|
|
|
while(sati->heuristic_time < sati->nOfTPoints) {
|
|
|
|
i = sati->heuristic_index;
|
|
j = sati->heuristic_time;
|
|
|
|
if(i+1 == sati->nOfSVars) {
|
|
sati->heuristic_index = 0;
|
|
sati->heuristic_time += 1;
|
|
} else {
|
|
sati->heuristic_index += 1;
|
|
}
|
|
|
|
if(tvarunsetp(sati,i,j)) {
|
|
if(tvartruep(sati,i,j-1)) return PLIT(TVAR(i,j));
|
|
else return NLIT(TVAR(i,j));
|
|
}
|
|
|
|
}
|
|
|
|
sati->heuristic_mode = 2;
|
|
sati->heuristic_time = 0;
|
|
sati->heuristic_index = 0;
|
|
|
|
case 2: /* All state variables have a value. Set actions to FALSE. */
|
|
|
|
while(sati->heuristic_time < sati->nOfTPoints-1) {
|
|
|
|
i = sati->heuristic_index;
|
|
j = sati->heuristic_time;
|
|
|
|
if(i+1 == sati->nOfActions) {
|
|
sati->heuristic_index = 0;
|
|
sati->heuristic_time += 1;
|
|
} else {
|
|
sati->heuristic_index += 1;
|
|
}
|
|
|
|
if(tvarunsetp(sati,ACTVAR(i),j)) return NLIT(TVAR(ACTVAR(i),j));
|
|
}
|
|
|
|
}
|
|
|
|
return -1;
|
|
|
|
}
|
|
|
|
int fmavalue(satinstance sati,fma *f,int t) {
|
|
fmalist *juncts;
|
|
switch(f->t) {
|
|
case patom: if(!tvarfalsep(sati,f->a,t)) return 1; else return 0;
|
|
case natom: if(!tvartruep(sati,f->a,t)) return 1; else return 0;
|
|
case disj:
|
|
juncts = f->juncts;
|
|
while(juncts != NULL) {
|
|
if(fmavalue(sati,juncts->hd,t) != 0) return 1;
|
|
juncts = juncts->tl;
|
|
}
|
|
return 0;
|
|
case conj:
|
|
juncts = f->juncts;
|
|
while(juncts != NULL) {
|
|
if(fmavalue(sati,juncts->hd,t) == 0) return 0;
|
|
juncts = juncts->tl;
|
|
}
|
|
return 1;
|
|
case TRUE: return 1;
|
|
case FALSE: return 0;
|
|
}
|
|
return 0;
|
|
}
|
|
|
|
/* Estimate the value for an action */
|
|
|
|
int actionvalue(satinstance sati,int var,int t,fma *precondition,int disjunctive) {
|
|
int i;
|
|
int val;
|
|
switch(HEURops) {
|
|
case 1: /* Evaluate 'constrainedness' of action */
|
|
/* How many steps later can this action be taken? */
|
|
val = 0;
|
|
while(t+1 < sati->nOfTPoints-1 && !tvarfalsep(sati,var,t+1)) {
|
|
t = t+1;
|
|
val = val + 1;
|
|
}
|
|
return val;
|
|
case 2: /* Evaluate 'constrainedness' of action */
|
|
/* How many steps later can this action be taken? */
|
|
val = 0;
|
|
while(t+1 < sati->nOfTPoints-1 && !tvarfalsep(sati,var,t+1)) {
|
|
t = t+1;
|
|
val = val + 1;
|
|
}
|
|
return 1000-val;
|
|
case 3: /* Evaluate 'constrainedness' of precondition */
|
|
/* How many steps later can the precondition be true? */
|
|
val = 0;
|
|
while(t+1 < sati->nOfTPoints && fmavalue(sati,precondition,t+1) != 0) {
|
|
t = t+1;
|
|
val = val + 1;
|
|
}
|
|
return val;
|
|
case 4: /* Evaluate 'constrainedness' of precondition */
|
|
/* How many steps later can the precondition be true? */
|
|
val = 0;
|
|
while(t+1 < sati->nOfTPoints && fmavalue(sati,precondition,t+1) != 0) {
|
|
t = t+1;
|
|
val = val + 1;
|
|
}
|
|
return 1000-val;
|
|
case 5:
|
|
/* How many steps earlier can the precondition be true? */
|
|
val = 0;
|
|
while(t-1 >= 0 && fmavalue(sati,precondition,t-1) != 0) {
|
|
t = t-1;
|
|
val = val + 1;
|
|
}
|
|
return val;
|
|
case 6:
|
|
/* How many steps earlier can the precondition be true? */
|
|
val = 0;
|
|
while(t-1 >= 0 && fmavalue(sati,precondition,t-1) != 0) {
|
|
t = t-1;
|
|
val = val + 1;
|
|
}
|
|
return 1000-val;
|
|
case 7:
|
|
/* How many later suggested actions the action disables/affects. */
|
|
val = 0;
|
|
for(i=0;i<Nsteps;i++) {
|
|
if((plansteps[i].t > t) && (actaffects(var,plansteps[i].var))) {
|
|
val = val + 1;
|
|
}
|
|
}
|
|
// printf("{%i}",val);
|
|
return 1000-val;
|
|
default: assert(2==7);
|
|
}
|
|
}
|
|
|
|
/* Go through actions at time point t-1 to find one that could
|
|
make literal l true at t. "Could" means: l occurs as a conditional
|
|
or unconditional effect, and we don't care about the condition.
|
|
|
|
This is based on the following parameters (given on command line):
|
|
HEURtime: which time to consider, 0 = earliest, 1 = latest, 2 = all
|
|
HEURops: which operator to consider 0 = first (arbitrary), 1 = all
|
|
HEURchoice: which action@time to choose, 0 = random, 1 = weight
|
|
*/
|
|
|
|
/* Choose an action at t1-1 that can make l@t TRUE. The action is returned
|
|
in var,t. */
|
|
|
|
void supports(satinstance sati,int t0,int t1,int l,int *var,int *t,fma **precondition,int *disjunctive) {
|
|
compactCEstruct *ptr;
|
|
int bestvalue,value;
|
|
int bestvar,bestt,bestdisjunctive;
|
|
fma *bestprecondition;
|
|
|
|
if(HEURops == 0) { /* Return the "first" (arbitrary) action. */
|
|
|
|
for(ptr=cCEs[l];ptr->var != -1;ptr++) { /* All ways of making l true. */
|
|
if(!tvarfalsep(sati,ptr->var,t1-1)) { /* Is it applicable? */
|
|
#ifdef HARDDEBUG
|
|
printf("Add ACTION %i:",ptr->var); printUvar(ptr->var); printf("@%i\n",t1-1);
|
|
#endif
|
|
*var = ptr->var;
|
|
*t = t1-1;
|
|
*precondition = ptr->condition;
|
|
*disjunctive = ptr->disjunctive;
|
|
return;
|
|
}
|
|
}
|
|
|
|
assert(1==2);
|
|
}
|
|
|
|
bestvar = -1;
|
|
|
|
for(ptr=cCEs[l];ptr->var != -1;ptr++) { /* All ways of making l true. */
|
|
if(!tvarfalsep(sati,ptr->var,t1-1)) { /* Is it applicable? */
|
|
#ifdef HARDDEBUG
|
|
printf("Consider ACTION %i:",ptr->var); printUvar(ptr->var); printf("@%i\n",t1-1);
|
|
#endif
|
|
if(bestvar == -1) {
|
|
bestvar = ptr->var;
|
|
bestt = t1-1;
|
|
bestprecondition = ptr->condition;
|
|
bestdisjunctive = ptr->disjunctive;
|
|
bestvalue = actionvalue(sati,ptr->var,t1-1,ptr->condition,ptr->disjunctive);
|
|
} else {
|
|
value = actionvalue(sati,ptr->var,t1-1,ptr->condition,ptr->disjunctive);
|
|
if(value > bestvalue) {
|
|
bestvar = ptr->var;
|
|
bestt = t1-1;
|
|
bestprecondition = ptr->condition;
|
|
bestdisjunctive = ptr->disjunctive;
|
|
bestvalue = value;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
assert(bestvar != -1);
|
|
|
|
#ifdef DECDEBUG
|
|
printf("Best action: ");
|
|
printUvar(bestvar);
|
|
printf("@%i for ",bestt);
|
|
printlit(l);
|
|
printf(" has value %i.\n",bestvalue);
|
|
#endif
|
|
|
|
*var = bestvar;
|
|
*t = bestt;
|
|
*precondition = bestprecondition;
|
|
*disjunctive = bestdisjunctive;
|
|
}
|
|
|
|
|
|
/* Is some action op actually making l true at t-1? (= op assigned TRUE?) */
|
|
|
|
int litmadetrue(satinstance sati,int l,int t,fma **precondition,int *disjunctive) {
|
|
int i;
|
|
|
|
if(!littruep(sati,litwithtime(sati,l,t))) return -1; /* l@t is not even true: no action! */
|
|
|
|
for(i=0;cCEs[l][i].var != -1;i++) { /* All ways of making l@t-1 true. */
|
|
if(tvartruep(sati,cCEs[l][i].var,t-1)) {
|
|
*precondition = cCEs[l][i].condition;
|
|
*disjunctive = cCEs[l][i].disjunctive;
|
|
return cCEs[l][i].var;
|
|
}
|
|
}
|
|
|
|
return -1; /* l@t-1 not made true. */
|
|
}
|
|
|
|
/***********************************************************************/
|
|
/*** Heuristic: ***/
|
|
/*** Find an unfulfilled (sub)goal and fulfill it at the earliest ***/
|
|
/*** possible time point. ***/
|
|
/*** ***/
|
|
/***********************************************************************/
|
|
|
|
#define noPRUNEfromGOAL
|
|
#define noPRUNEtoGOAL
|
|
|
|
void do_cpath(satinstance sati) {
|
|
int l,t,t1;
|
|
int j,var,isthere;
|
|
int suggestedactionsfound;
|
|
int depthlimitHIGH;
|
|
fma *precondition;
|
|
int disjunctive;
|
|
|
|
depthlimitHIGH = -1;
|
|
suggestedactionsfound = 0;
|
|
|
|
while(stackptr > 0) {
|
|
|
|
/* Pop literal-time pair from the stack. */
|
|
l = stack[stackptr-1].lit;
|
|
t = stack[--stackptr].t;
|
|
|
|
#ifdef PRUNEtoGOAL
|
|
if(HEURactiondepthlimit && suggestedactionsfound && t >= depthlimitHIGH)
|
|
return;
|
|
#endif
|
|
|
|
#ifdef HEURDEBUG
|
|
printf("Find action for goal "); printlit(l); printf("@%i.\n",t);
|
|
#endif
|
|
|
|
/* Starting from last time point, find last time t such that either
|
|
1) an action op@t-1 makes l@t TRUE, or
|
|
2) l@t-1 is FALSE and l@t is TRUE or UNASSIGNED.
|
|
*/
|
|
isthere = 0;
|
|
var = -1;
|
|
|
|
for(j=t;j>0;j--) {
|
|
var = litmadetrue(sati,l,j,&precondition,&disjunctive);
|
|
if(var != -1) {
|
|
isthere = 1;
|
|
t1 = j-1;
|
|
break;
|
|
}
|
|
|
|
if(litfalsep(sati,litwithtime(sati,l,j-1))) break;
|
|
}
|
|
|
|
if(j == 0) { /* Literal is true at time 0. */
|
|
#ifdef HEURDEBUG
|
|
printf("(true in the initial state.)\n");
|
|
#endif
|
|
continue;
|
|
}
|
|
|
|
/* Literal is last false at time point j-1. */
|
|
|
|
if(var == -1) { /* Choose an action that turns l true between j-1 and j. */
|
|
supports(sati,t,j,l,&var,&t1,&precondition,&disjunctive);
|
|
/* The following assertions cannot be false because
|
|
there must be an action that could make l true at t1 (i.e. is not FALSE).
|
|
If there were not, the frame action (-l & l) -> ... would
|
|
contradict Ass1 and Ass2.
|
|
*/
|
|
ASSERT(var != 0);
|
|
ASSERT(precondition->t != -1);
|
|
ASSERT(tlitfalsep(sati,l,j-1));
|
|
ASSERT(!tlitfalsep(sati,l,j));
|
|
}
|
|
|
|
if(seenp(sati,TVAR(var,t1))) continue; /* Operator already processed once. */
|
|
|
|
/* Don't go back to top-level goals. */
|
|
|
|
#ifndef PRUNEtoGOAL
|
|
if(HEURactiondepthlimit && suggestedactionsfound && t1 >= depthlimitHIGH)
|
|
return;
|
|
#endif
|
|
|
|
if(!isthere) { /* Add the variable to the list of candidate decisions. */
|
|
suggestedactionsfound += 1;
|
|
plansteps[Nsteps].var = var;
|
|
plansteps[Nsteps].t = t1;
|
|
plansteps[Nsteps].flaws = 0;
|
|
if(HEURops == 7) {
|
|
for(j=0;j<Nsteps;j++) {
|
|
if(actaffects(var,plansteps[j].var)) plansteps[Nsteps].flaws += 1;
|
|
}
|
|
}
|
|
plansteps[Nsteps++].l = l;
|
|
|
|
#ifdef HEURDEBUG
|
|
printf("Chose action ");
|
|
printUvar(var);
|
|
printf(" to make literal true @%i.\n",j);
|
|
#endif
|
|
|
|
#ifdef PRUNEfromGOAL
|
|
if(suggestedactionsfound == 1) depthlimitHIGH = t;
|
|
#else
|
|
if(suggestedactionsfound == 1) depthlimitHIGH = t1;
|
|
#endif
|
|
}
|
|
|
|
ASSERT(Nsteps < MAXPLANSTEPS);
|
|
|
|
if(suggestedactionsfound >= HEURactions) return;
|
|
|
|
#ifdef HARDDEBUG
|
|
printf(" Push preconditions of %i:",var); printUvar(var); printf("@%i into the stack (%i).\n",t1,isthere);
|
|
#endif
|
|
|
|
if(t1 > 0) { /* Push preconditions in the stack. */
|
|
if(disjunctive == 0) {
|
|
push2goalstackCfma(sati,precondition,t1);
|
|
} else {
|
|
push2goalstackDfma(sati,precondition,t1);
|
|
}
|
|
#ifdef HARDDEBUG
|
|
showheustack(sati);
|
|
#endif
|
|
|
|
}
|
|
}
|
|
}
|