/* ----------------------------------------------------------
% (C)1992 Institute for New Generation Computer Technology
% (Read COPYRIGHT for detailed information.)
----------------------------------------------------------- */
/*=====================================================================
* cu-Prolog III (Constraint Unification Prolog)
* Copyright: Institute for New Generation Computer Technology,Japan
* 1989--91
==================================================================== */
/*--------------------------------------------------------------------
* << modular.c >>
* constraint transformation entry, tools
* 94.6.28 termset speedup
--------------------------------------------------------------------*/
#include "include.h"
#if SUN4 == 1
#include <sys/time.h>
#else
#if CPUTIME != 0
#include <sys/types.h>
#include <sys/times.h>
#endif
#endif
#define in_cheap(X) (( &cheap[0] <= ((int *)X)) && (((int *)X) < chp))
#define in_upper_heap(X,Y) ( in_sheap(X) || ( (Y==MEDIUM) && in_cheap(X)) )
long CONSTRAINT_OLD_TIME;
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
modular(c)
@ mode entry
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
void modular(c,vlist,anum) /* constraint trans. from top level (@) */
struct clause *c;
struct term *vlist;
int anum;
{
struct clause *sol;
sol = startmodular(c, vlist, anum); /* tranformation */
tprint0("solution = ");
if (sol == MFAIL){ /* fail transformation */
tprint0("fail.\n");
}
else if (sol == NULL){ /* nil constraint */
tprint0("nil (true).\n");
}
else /* c.t. success */
{
Pclause(sol, NULL_ENV); NL;
show_newdefs(); /* print DEF_list */
}
}
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
cu(t,e)
process unify() built-in predicate
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
/* constraint transformation embedded in Prolog : unify() pred. */
int cu(t,e) /* 0: cu fail 1: success */
struct term *t;
struct pair *e;
{
register struct pair *p, *q;
struct pair *ee;
struct term *tt;
struct clause *c, *clist;
#if CPUTIME != 0
struct tms TIMES;
#endif
if (t == NULL) return(TRUE);
if (! isvar(Arg2(t))) return(FALSE); /* second arg = var */
p = &e[vnumber(Arg2(t))];
if (p->p_body != NULL) return(FALSE); /* second arg-->var */
#if SUN4 == 1
CONSTRAINT_OLD_TIME = clock();
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_OLD_TIME = TIMES.tms_stime + TIMES.tms_utime;
#endif
#endif
p->p_env = Nenv(0); /* cf. 'q' in termset() */
up_init();
tt = Arg1(t);
ee = e;
down(q,tt,ee);
if (tt == NIL){
p->p_body = NIL;
p->p_env = NULL;
#if SUN4 == 1
CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
CONSTRAINT_OLD_TIME;
#endif
#endif
return(TRUE);
}
clist = c = Nclause(termset(head_of_list(tt),ee,TEMPORAL),
NULL_CL,TEMPORAL);
while (1) {
tt = tail_of_list(tt);
down(q,tt,ee);
if ((tt == NIL) || (! is_list(tt))) break;
c->c_link = Nclause(termset(head_of_list(tt),ee,TEMPORAL),
NULL_CL,TEMPORAL);
c = c->c_link;
}
if (tt != NIL) {
up_restore();
p->p_env = NULL;
error("Illegal form of constraint list.");
}
if (p_number != 0) {
renum_pvars((struct pstvar *)pv_list,v_number);
q=Nenv(p_number);
}
up_restore();
c = startmodular(clist,v_list,v_number+p_number); /* transformation */
if (c == MFAIL){ /* fail transformation */
p->p_env = NULL;
#if SUN4 == 1
CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
CONSTRAINT_OLD_TIME;
#endif
#endif
return(FALSE); /* fail */
}
else if (c == NULL)
{
p->p_body = NIL;
p->p_env = NULL;
#if SUN4 == 1
CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
CONSTRAINT_OLD_TIME;
#endif
#endif
return(TRUE);
}
else
{
p->p_body = tolist(c,STINGY);
TB
tprint0(" ====> ");
Pterm(p->p_body, p->p_env);
TE
#if SUN4 == 1
CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
CONSTRAINT_OLD_TIME;
#endif
#endif
return(TRUE); /* success */
}
}
/* change clause(t1,t2,t3) to list([t1,t2,t3]) <- cu() */
struct term *tolist(c,flag)
struct clause *c;
int flag;
{
register struct clause *cc, *croot;
if (c == NULL) return(NIL);
switch (flag) {
case STINGY:
for (cc = c; cc->c_link != NULL; cc=cc->c_link)
cc->c_type = LIST_TYPE;
cc->c_link = (struct clause *)NIL;
return((struct term *)c);
default:
croot=cc=Nlist(head_of_list(c),(struct clause *)NIL,flag);
while (c->c_link != NULL) {
c=c->c_link;
cc->c_link=Nlist(head_of_list(c),(struct clause *)NIL,flag);
cc = cc->c_link;
}
return((struct term *)croot);
}
}
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
transform(precond,newc,newenv)
constriant solver of CAHC , called by resolve() in refute.c
precond: old constraint (from goal)
newc, newenv: new constraint (from program)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
/* constraint transformation entry <- resolve() */
struct eclause *transform(precond, newc, newenv)
struct eclause *precond;
struct clause *newc;
struct pair *newenv;
{
struct eclause *eclause_append();
struct eclause *cond;
struct clause *c,*clist;
struct pair *env,*q;
#if CPUTIME != 0
struct tms TIMES;
#endif
if (precond == NULL && newc == NULL) return(NULL);
#if SUN4 == 1
CONSTRAINT_OLD_TIME = clock();
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_OLD_TIME = TIMES.tms_stime + TIMES.tms_utime;
#endif
#endif
cond = eclause_append(precond, reduce_clause(newc,newenv));
if (cond == (struct eclause *)MFAIL) /* reduce_clause failure */
{
TB tprint0("fail (reducetion)"); TE
return((struct eclause *)MFAIL);
}
env = Nenv(0);
up_init();
clist = up_eclause(cond,MEDIUM); /* set clause */
up_restore();
if (p_number != 0) {
renum_pvars((struct pstvar *)pv_list,v_number);
q=Nenv(p_number); /* 1991-03-10 */
}
if (clist == NULL) {
#if SUN4 == 1
CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
CONSTRAINT_OLD_TIME;
#endif
#endif
return(NULL); /* no constraint */
}
TB
tprint0(">>transform: ");
Peclause(cond);
tprint0(" ==> ");
TE
c = startmodular(clist,v_list,v_number+p_number);
if (c == MFAIL) { /* constraint transformation failure */
TB tprint0("fail"); TE
#if SUN4 == 1
CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
CONSTRAINT_OLD_TIME;
#endif
#endif
return((struct eclause *)MFAIL);
}
cond = reduce_clause(c,env);
if (cond == NULL_ECL) {
TB tprint0("null"); TE
}
else if (cond == (struct eclause *)MFAIL)
{
TB tprint0("fail (reduction)"); TE
}
else {
TB Peclause(cond); TE
}
#if SUN4 == 1
CONSTRAINT_HANDLING_TIME += clock()-CONSTRAINT_OLD_TIME;
#else
#if CPUTIME != 0
times(&TIMES);
CONSTRAINT_HANDLING_TIME += TIMES.tms_stime + TIMES.tms_utime -
CONSTRAINT_OLD_TIME;
#endif
#endif
return(cond);
}
struct eclause *eclause_append(head,tail) /* <- transform() */
register struct eclause *head, *tail;
{
if (head == (struct eclause *)MFAIL ||
tail == (struct eclause *)MFAIL)
return((struct eclause *)MFAIL);
while (head != NULL_ECL) {
tail = Neclause(head->c_form,head->c_env,tail,TEMPORAL);
head = head->c_link;
}
return(tail);
}
/* --------- term set ------------- */
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
struct term *termset(t,e,flag)
struct clause *up_eclause(ec,flag)
make variant of terms with an environment
Before termset, up_init() and after termset, up_restore().
Before termset, set p=Nenv(0), then p will be a unifier.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct up_log
{
struct term *u_old,*u_new;
struct pair *u_oldenv;
struct up_log *u_link;
};
struct ustack *ustack_save_up; /* save old usp */
int UHASHSIZE=17;
struct up_log *UP_Log[17], *UP_pstLog[17];
int log_size(n) /* for debug */
int n;
{
register int i;
register struct up_log *u;
for (u=UP_Log[n],i=0; u!=NULL; u=u->u_link,i++);
return(i);
}
int pstlog_size(n) /* for debug */
int n;
{
register int i;
register struct up_log *u;
for (u=UP_pstLog[n],i=0; u!=NULL; u=u->u_link,i++);
return(i);
}
void initialize_log()
{
register int i;
for (i=0; i<UHASHSIZE; i++) UP_Log[i]=UP_pstLog[i]=NULL;
}
int print_tepair_length() /* for debug */
{
int i;
for (i=0; i<UHASHSIZE; i++)
printf("%d/%d ",log_size(i),pstlog_size(i));
putchar('\n');
}
int tepairtype(t,e)
struct term *t;
struct pair *e;
{
return(((int)t + (int)e) % UHASHSIZE);
}
void up_init0()
{
ustack_save_up = usp;
v_number = 0; v_list = NULL_TERM;
p_number = 0; pv_list = NULL_TERM;
}
void up_restore0()
{
undo(ustack_save_up);
}
void up_init()
{
up_init0();
initialize_log();
}
void up_restore()
{
initialize_log();
up_restore0();
}
void push_log(oldt,oldenv,newt)
struct term *oldt,*newt;
struct pair *oldenv;
{
register struct up_log *u;
register int tt;
MEMORY_ALLOC(u,up_log,TEMPORAL);
u->u_old = oldt;
u->u_new = newt;
u->u_oldenv = oldenv;
tt = tepairtype(oldt,oldenv);
u->u_link = UP_Log[tt];
UP_Log[tt] = u;
}
struct term *search_log(t,e) /* search (t,e) in UP_log */
struct term *t;
struct pair *e;
{
register struct up_log *u;
for (u = UP_Log[tepairtype(t,e)]; u != NULL; u = u->u_link)
if (u->u_old == t && u->u_oldenv == e)
return(u->u_new);
return(NULL);
}
void push_pstlog(oldt,oldenv,newt)
struct term *oldt,*newt;
struct pair *oldenv;
{
register struct up_log *u;
register int tt;
MEMORY_ALLOC(u,up_log,TEMPORAL);
u->u_old = oldt;
u->u_new = newt;
u->u_oldenv = oldenv;
tt = tepairtype(oldt,oldenv);
u->u_link = UP_pstLog[tt];
UP_pstLog[tt] = u;
}
struct term *search_pstlog(t,e) /* search (t,e) in UP_log */
struct term *t;
struct pair *e;
{
register struct up_log *u;
for (u = UP_pstLog[tepairtype(t,e)]; u != NULL; u = u->u_link)
if (u->u_old == t && u->u_oldenv == e)
return(u->u_new);
return(NULL);
}
void check_constant_term(t)
struct term *t;
{
register int i;
if (t->t_arity < 0) t->t_arity = - t->t_arity;
for (i = 0; i < Pred(t)->f_arity; i++)
if (! isconst(Arg(t,i))) return;
t->t_arity = - t->t_arity;
}
/* term prepare for cu() : v_list and v_number are changed */
struct term *termset(t,e,flag)
register struct term *t;
register struct pair *e;
int flag;
{
register struct pair *p,*q;
register struct term *nt;
if (t == NULL) return(t);
down(p,t,e);
if (p != NULL) { /* if t is a free var */
if (p == Anonymous_env)
return(Anonymous_var);
if (p->p_env == NULL) {/* if t is a new var */
/* use p->p_env as work area */
upush(&(p->p_env));
Nvar(vname(t),flag);
p->p_env = (struct pair *)v_list;
q = Nenv(1);
q->p_body = t;
q->p_env = e;
return(v_list);
}
else{
((struct var *)p->p_env)->v_occurrence++;
return( (struct term *)p->p_env );
}
}
if (t->type.ident == PST_TYPE)
return(up_pst(((struct pst *)t),e,flag));
if (flag==ETERNAL && (nt = search_log(t,e)) != NULL) return(nt);
/* already set */
switch (t->type.ident) {
case ATOMIC_TYPE:
nt = up_atomic(t,flag); /* constant term */
break;
case CLAUSE_TYPE:
nt = (struct term *)Nclause(termset(head_of_list(t),e,flag),
(struct clause *)termset(tail_of_list(t),e,flag),flag);
break;
case LIST_TYPE:
case CONST_LIST_TYPE:
nt = (struct term *)Nlist(termset(head_of_list(t),e,flag),
(struct clause *)termset(tail_of_list(t),e,flag),flag);
break;
default:
if (isconst_functor(t))
{
nt = up_const_functor(t,flag);
break;
}
nt = Nterm(t->t_arity,flag);
nt->type.t_func = t->type.t_func;
{
register int i;
for (i = 0; i < t->t_arity; i++)
Arg(nt,i) = termset(Arg(t,i), e, flag);
}
check_constant_term(nt); /* check if nt is constant term */
}
/* print_tepair_length(); */
if (flag == ETERNAL) push_log(t,e,nt);
return(nt);
}
struct term *up_pst(pt,e,flag)
struct pst *pt;
struct pair *e;
int flag;
{
struct pst_item *target;
struct pst *nt;
struct pstvar *pv;
struct eclause *t0,*targetobj;
struct pair *e0;
struct term *oldt;
if ((target = find_pstitem((struct term *)pt,e)) != NULL_PSTIT)
{
t0 = target->p_lists;
e0 = NULL;
if (flag==ETERNAL && (oldt = search_pstlog(t0,e0)) != NULL)
return(oldt);
targetobj = termset_pstobj(target->p_lists,flag);
}
else
{
t0 = pt->p_lists;
e0 = e;
if ((oldt = search_pstlog(t0,e0)) != NULL) return(oldt);
targetobj = termset_pstobj_sub(pt->p_lists,e,flag);
}
MEMORY_ALLOC(nt,pst,flag);
nt->type = PST_TYPE;
MEMORY_ALLOC(pv,pstvar,flag);
pv->v_type = VAR_PST_TYPE;
pv->v_name = vname(Anonymous_var);
pv->v_number = p_number++;
pv->v_link = pv_list;
pv->old_var = pt->p_var;
nt->p_var = pv_list = (struct term *)pv;
nt->p_lists = targetobj;
if (flag == ETERNAL) push_pstlog(t0,e0,(struct term *)nt);
return((struct term *)nt);
}
struct eclause *termset_pstobj(pobj,flag)
struct eclause *pobj;
int flag;
{
if (pobj==NULL_ECL) return(pobj);
else
return(Npstobj(termset(pobj->c_form,pobj->c_env,flag),
NULL_ENV,
termset_pstobj(pobj->c_link,flag),
flag));
}
struct eclause *termset_pstobj_sub(pobj,e,flag)
struct eclause *pobj;
struct pair *e;
int flag;
{
struct eclause *pl, *ptop;
if (pobj == NULL_ECL)
return(pobj);
ptop = pl = Npstobj(termset(pobj->c_form,e,flag),
NULL_ENV,NULL_ECL,flag);
while (pobj->c_link != NULL_ECL) {
pl->c_link=
Npstobj(termset(pobj->c_link->c_form,e,flag),
NULL_ENV,NULL_ECL,flag);
pobj = pobj->c_link;
pl = pl->c_link;
}
return(ptop);
}
struct term *up_const(t,flag)
register struct term *t;
int flag;
{
struct term *up_atomic(), *up_const_functor();
if (in_upper_heap(t,flag)) return(t);
switch (t->type.ident) {
case ATOMIC_TYPE:
return(up_atomic(t,flag));
case CONST_LIST_TYPE:
return((struct term *)Nlist(up_const(head_of_list(t),flag),
(struct clause *)up_const(tail_of_list(t),flag),
flag));
default: /* functor */
return(up_const_functor(t,flag));
}
}
struct term *up_atomic(t,flag)
register struct term *t;
int flag;
{
register struct term *tt;
if (flag == TEMPORAL || in_upper_heap(t,flag)) return(t);
tt = Nterm(0,flag);
tt->type.ident = t->type.ident;
tt->t_arity = t->t_arity;
if (is_int(t)) num_value(tt) = num_value(t);
else if (! is_string(t)) num_value(tt) = num_value(t);
else str_value(tt) = nalloc(str_value(t),flag);
return(tt);
}
struct term *up_const_functor(t,flag)
register struct term *t;
int flag;
{
register struct term *tt;
register int i;
if (flag == TEMPORAL || in_upper_heap(t,flag)) return(t);
i = -t->t_arity;
if (i == 0) /* constant */
{
tt = Nterm(0,flag);
Pred(tt) = Pred(t);
return(tt);
}
tt = Nterm(i,flag);
Pred(tt) = Pred(t);
tt->t_arity = -i;
while (i > 0) {
i--;
Arg(tt,i) = up_const(Arg(t,i),flag);
}
return(tt);
}
struct clause *up_eclause(ec,flag)
struct eclause *ec;
int flag;
{
if (ec == NULL) return(NULL);
return(Nclause(termset(ec->c_form, ec->c_env,flag),
up_eclause(ec->c_link,flag),
flag));
}
struct clause *up_itrace_clause(cl,anum)
struct clause *cl;
int anum;
{
register struct variant *va;
struct variant *variant();
va = variant(cl,ETERNAL);
return(va->v_clause);
}
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
try_fold(c,n)
try fold transformation
c: clause
n: # of vars + # of psts in c
if there is H<=>C in new predicate derivation clauses and Cu=cu,
return Hu (u is a variable replacement).
else return NULL
try_fold() is called by new_constraint() in trans.c
. . . try_fold+
. . . . match+
. . . . . match_term+
. . . . termnumber
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct term *try_fold(c,n) /* fold transformation */
struct clause *c; /* target clause */
int n; /* # of different vars and psts in c */
{
register struct itrace *it;
struct ustack *usave;
struct term *t,*head;
struct pair *e;
struct pair *esave = ep;
int j, count,termnumber();
if (c == NULL) return(NULL);
if (newf_list == NULL) return(NULL);
count = literalnumber(c); /* number of terms in c */
usave = usp;
esave = ep;
e = Nenv(n);
for (it = newf_list; it != NULL; it = it->it_link ) {
if ((it->it_anumber == n) && (it->it_cnumber == count) )
if (match(c, it->it_clause->c_link, e) == FALSE)
{
undo(usave);
ep = esave;
continue;
}
else{
if (it->it_clause->c_form == FAIL) {
undo(usave); ep = esave;
return(FAIL);
}
head = it->it_clause->c_form;
t = Nterm(Pred(head)->f_arity, MEDIUM);
Pred(t) = Pred(head);
for (j = 0; j < Pred(head)->f_arity ; j++) {
Arg(t,j) = e[termnumber(Arg(head,j))].p_body;
/* patch for PST var 1991-03-02 */
if (Arg(t,j)==NULL) Arg(t,j)=Anonymous_var;
}
undo(usave); ep = esave; /* patch 1991-03-03 */
return(t); /* found something */
}
}
return(NULL);
}
int termnumber(t)
struct term *t; /* var or PST */
{
if (isvar(t)) return(vnumber(t));
else if (is_pst(t)) return(vnumber( ((struct pst *)t)->p_var));
else printf("illegal term type : termnumber");
}
int match(clo,clt,e) /* clause matcher */
struct clause *clo,*clt;
struct pair *e;
{
register struct clause *c1,*c2;
for (c1 = clo,c2 = clt; c1 != NULL ; c1 = c1->c_link,c2 = c2->c_link)
if (Pred(c1->c_form) != Pred(c2->c_form))
return(FALSE); /* fail */
for (c1 = clo, c2 = clt; c1 != NULL; c1 = c1->c_link, c2 = c2->c_link)
if (match_term(c1->c_form , c2->c_form , e) == FALSE)
return(FALSE);
return(TRUE); /* success */
}
int match_term(t1,t2,e) /* term unification (t1,e) = (t2,e) */
struct term *t1,*t2;
struct pair *e; /* return envs */
{
register struct pair *p;
if (isvar(t2)) {
if (!isvar(t1)) return(FALSE);
p = &e[vnumber(t2)];
if (p->p_body == NULL) {
p->p_body = t1;
return(TRUE);
}
else if(p->p_body == t1) return(TRUE);
else return(FALSE);
}
else if (isvar(t1)) return(FALSE);
if (Pred(t1) != Pred(t2)) return(FALSE);
switch (t1->type.ident) {
case ATOMIC_TYPE:
if ((t1==t2) ||(atomic_equal(t1,t2))) return(TRUE);
else return(FALSE);
case LIST_TYPE:
case CONST_LIST_TYPE:
if (match_term(head_of_list(t1),head_of_list(t2),e) &&
match_term(tail_of_list(t1),tail_of_list(t2),e))
return(TRUE);
else return(FALSE);
case CLAUSE_TYPE:
while ((t1!=NULL) && (t2!=NULL)) {
if (match_term(head_of_list(t1),head_of_list(t2),e) == FALSE)
return(FALSE);
t1=tail_of_list(t1);
t2=tail_of_list(t2);
}
if (t1==t2) return(TRUE);
else return(FALSE);
case PST_TYPE:
if (t2->type.ident != PST_TYPE) return(FALSE);
p = &e[termnumber(t2)];
if (p->p_body == NULL)
{
if (match_term((struct term *)((struct pst *)t1)->p_lists,
(struct term *)((struct pst *)t2)->p_lists,e)
== FALSE) return(FALSE);
p->p_body = t1;
return(TRUE);
}
else if (p->p_body == t1) return(TRUE);
else if (p->p_body != t1) return(FALSE);
case ECLAUSE_TYPE: /* pst_objects */
while ((t1!=NULL) && (t2!=NULL)) {
if (match_term(((struct eclause *)t1)->c_form,
((struct eclause *)t2)->c_form,e) == FALSE) return(FALSE);
t1=(struct term *)((struct eclause *)t1)->c_link;
t2=(struct term *)((struct eclause *)t2)->c_link;
}
if (t1==t2) return(TRUE);
else return(FALSE);
default: {
register int i,j = t1->t_arity;
if (j < 0) j = -j;
for(i = 0 ; i<j ; i++)
if (match_term(Arg(t1,i), Arg(t2,i), e) == FALSE) return(FALSE);
return(TRUE);
}
}
}
syntax highlighted by Code2HTML, v. 0.9.1