/* ----------------------------------------------------------
% (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
==================================================================== */
/*--------------------------------------------------------------------
* << trans.c >>
* constriant transformation module
* 1992-Nov-4 sort bodies literals. (new_constraint, unfold_derivation)
--------------------------------------------------------------------*/
#include "include.h"
#define DEBUG 0 /* if debug, 1 */
struct cset *DEF_list; /* sets of new predicate derivation clauses */
struct cset *CSTR_list; /* sets of non-modular clauses */
struct cset *INITDEF_list; /* sets of non-modular clauses */
int CSTR_number;
int old_CSTR_number;
struct clause *CONST_literals, *REST_literals; /* used in split, attach */
struct itrace *newfsave; /* old newf_list */
jmp_buf trans_fail; /* transformation failure */
/*
[startmodular]-----------------------------------
. abandon_transformation
. . <index_newflist> --> new.c
. . reducedfun+
. add_to_set+
. . index_newflist~
. . <add_cs_to_set> --> tr_sub.c
. clear_up_DEF
. . remove_from_CSTR
. end_unfoldfold+
. . <recalc_component>+ ---> mainsub.c
. foldunfold+
. . <P_status>+ ------> tr_sub.c
. . set_temporal_def
. . <step_asking>+ ------> tr_sub.c
. . check_INITDEF+
. . is_modular_head+
. . . vheadoccurrence.
. . unfold_cstr+
. . . [apply]
. . . [target_literal]
. . . from_to+
. . . insert_cs+
. . . reorder.
. . unfold_derivation+
. . . [apply]
. . . [target_literal]
. . . literalnumber~
. . . reorder~
. modular_form
. . <satisfiable> -------> tr_sub.c
. . <split>+ ---------> split.c
. . surface_copy_clause+
. . Pcmp+
. . new_constraint+
. . . <try_fold>+ ---> modular.c
. . . <variant_v>+ ---> tr_split.c
. . . new_pred_set+
. . . . newpred+
. . . . set_new_def+
. . . . vpair_length+
. . set_const_pst+
. init_unfoldfold+
*/
/* ------------ begin init & end unfoldfold --------------*/
void init_unfoldfold()
{
newfsave = newf_list; /* save newf_list */
DEF_list = NULL; /* derivation clauses */
CSTR_list = NULL; /* new clauses */
old_CSTR_number = CSTR_number = 0; /* initial clause number */
INITDEF_list = NULL; /* initial derivation clauses */
}
void end_unfoldfold()
{
void recalc_component(); /* mainsub.c */
recalc_component();
CSTR_list = NULL; /* new clauses */
old_CSTR_number = CSTR_number = 0; /* initial clause number */
INITDEF_list = NULL; /* initial derivation clauses */
}
/* when transformation fails, */
void abandon_transformation() /* abandon all new predicates */
{
register struct cset *cs;
register struct func *f;
newf_list = newfsave; /* restore newf_list (init_unfoldfold) */
for (cs = INITDEF_list; cs != NULL; cs = cs->cs_link)
if (cs->cs_status == FALSE_REGISTERED)
{
f = Pred(cs->cs_clause->c_form);
if (f->f_integ == NULL) continue;
index_func(f);
reducedfun(f);
f->def.f_set = NULL;
f->f_unitcount = f->f_setcount = 0;
f->f_integ->it_link = newf_list;
newf_list = f->f_integ;
}
newf_list = index_newflist(newf_list,newfsave);
}
void quit_transformation() /* quit transformation (in step trace) */
{
register struct cset *cs;
register struct func *f;
for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
{
f = Pred(cs->cs_clause->c_form);
f->f_setcount = f->f_unitcount = 0; /* reset in add_cs_to_set*/
if (cs->cs_status == REGISTERED ||
cs->cs_status == REMOVED)
index_func(f); /* register into global hash table */
else if (cs->cs_status == DERIVATION)
{
index_func(f); /* register into global hash table */
add_cs_to_set(cs,'a');
}
}
for (cs = CSTR_list; cs != NULL; cs = cs->cs_link)
if (cs->cs_status != REMOVED)
add_cs_to_set(cs,'a');
}
/* ------------ end init & end unfoldfold --------------*/
int check_INITDEF() /* INITDEF_list is satisfiable ??*/
{
register struct cset *cs;
for(cs = INITDEF_list; cs != NULL; cs = cs->cs_link)
if (cs->cs_status == FALSE_REGISTERED)
return(FALSE);
return(TRUE);
}
void remove_from_CSTR(f) /* used in clear_up_DEF */
struct func *f;
{
register struct cset *cs;
register struct clause *c;
for (cs = CSTR_list; cs != (struct cset *)NULL; cs = cs->cs_link)
if (cs->cs_status == MODULAR_DEFINED ||
cs->cs_status == UNTOUCHED)
for(c = cs->cs_clause; c != NULL_CL;
c = c->c_link)
if (Pred(c->c_form) == f) {
cs->cs_status = REMOVED;
Pred(cs->cs_clause->c_form)->f_setcount--;
break;
}
}
void clear_up_DEF() /* delete useless clauses */
{
register struct cset *cs;
register struct func *f;
int changed = 1;
while(changed == 1)
{
changed = 0;
for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
{
if (cs->cs_status == REMOVED){
f = Pred(cs->cs_clause->c_form);
if (f->f_unitcount > 0)
cs->cs_status = REGISTERED;
else if (f->f_setcount == 0)
{
changed = 1;
cs->cs_status = FALSE_REGISTERED;
f->f_integ->it_clause->c_form = FAIL;
remove_from_CSTR(f);
}
}
}
}
}
void add_to_set() /* register definition clauses */
{
register struct cset *cs;
register struct func *f;
newf_list = index_newflist(newf_list,newfsave);
for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
{
f = Pred(cs->cs_clause->c_form);
if (cs->cs_status == REGISTERED ||
cs->cs_status == REMOVED)
index_func(f); /* register into global hash table */
f->f_setcount = f->f_unitcount = 0; /* reset in add_cs_to_set*/
}
for (cs = CSTR_list; cs != NULL; cs = cs->cs_link)
if (cs->cs_status == MODULAR_DEFINED ||
cs->cs_status == UNIT_DEFINED ||
(Is_Msolvable && (cs->cs_status == TEMPORAL_DEFINED)))
add_cs_to_set(cs,'a');
}
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
startmodular(clist,vlist,anum)
constraint transformation entry
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct clause *startmodular(clist, vlist, anum) /* entry */
struct clause *clist;
struct term *vlist;
int anum;
{
int result;
register struct clause *c;
init_unfoldfold(); /* reset gloval vars */
if (clist != NULL)
clist = modular_form(clist,vlist,anum); /* set DEF_list */
if (clist == NULL || clist == MFAIL ||DEF_list == NULL)
{
end_unfoldfold();
return(clist); /* no need for transformation */
}
INITDEF_list = DEF_list; /* initial derivation clauses */
TTB
if (setjmp(trans_fail)) /* quit/abort transformation */
{ /* <-- step_asking() */
end_unfoldfold();
/* if clist has defs */
for (c = clist; c != NULL; c = c->c_link) {
if (Pred(c->c_form)->def.f_set == (struct set *)NULL)
return(MFAIL);
}
return(clist);
}
TTE
result = foldunfold();
if (result == TRUE) /* transformation success */
{
clear_up_DEF();
add_to_set();
end_unfoldfold();
return(clist);
}
else { /* transformation failure */
abandon_transformation();
end_unfoldfold();
return(MFAIL);
}
}
void Pcmp(cmp) /* print compartment */
struct compartment *cmp;
{
for (; cmp != NULL; cmp = cmp->cmp_link)
{
Pclause(cmp->cmp_clause,NULL);NL;
}
if (CONST_literals != NULL) {
printf("ground = ");
Pclause(CONST_literals,NULL);NL;
}
if (REST_literals != NULL)
{
printf("rest = ");
Pclause(REST_literals, NULL);NL;
}
}
/* define new predicates */
struct clause *modular_form(clist, vlist, anum)
struct clause *clist;
struct term *vlist;
int anum;
{
struct compartment *cmp,*cm;
struct clause *crest, *cc;
register struct clause *c;
void set_const_pst();
cmp = split(surface_copy_clause(clist,TEMPORAL), vlist, anum);
if (cmp == (struct compartment *)MFAIL) return(MFAIL);
/* global vars */
crest = REST_literals;
/* printf("split ");
Pclause(clist,NULL);
printf("into\n");
Pcmp(cmp);
NL;
*/
if (CONST_literals != NULL)
if (! satisfiable(CONST_literals,anum)) return(MFAIL);
for (cm = cmp; cm != NULL; cm = cm->cmp_link) {
cc = c = new_constraint(cm);
if (c == MFAIL) return(MFAIL);
if (c == NULL) continue;
while (c->c_link != NULL) c = c->c_link; /* c <- end of cc */
c->c_link = crest;
crest = cc;
}
return(crest);
}
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++
new_constraint(cmp)
change cmp into surface modular form by
making new predicates or folding
. . new_constraint+
. . . try_fold+
. . . . match+
. . . . . match_term+
. . . . termnumber
. . . variant_v+
. . . . Pvariant+
. . . new_pred_set+
. . . . newpred+
. . . . set_new_def+
. . . . vpair_length+
. . . variables+
++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct clause *new_constraint(cmp) /* make new pred or folding */
struct compartment *cmp;
{
struct term *t;
struct clause *c,*new_pred_set();
struct variant *ccopy,*variant_v();
c = sort_clause(cmp->cmp_clause); /* 92/11/4 BUG fix */
cmp->cmp_clause = c;
if (c == NULL) return(NULL);
if (is_modular_clause(c)) return(c);
/* here works in future */
/* if (!need_trans(cmp))
returnc(restore_head(c->c_form,cmp->cmp_vp,cmp->cmp_vp_size)); */
ccopy = variant_v(c,MEDIUM);
if (ccopy->v_anum > MODULARMAX) /* heuristics */
{
FILE *f = wfp;
wfp = stderr;
tprint0("Warning: Transformation failure by exceeding the");
tprint0("limit of the number of variables (cf) %%M command\n");
Pterm(c,NULL_ENV);NL;
wfp = f;
return(MFAIL);
}
t = try_fold(c, ccopy->v_anum);
if (t != NULL)
{
TTB
tprint0("#folding "); Pclause(c,NULL); tprint0(" ==> ");
Pterm(t,NULL);
TTE
STAT_FOLD++; /* statistics */
if (t == FAIL) return(MFAIL);
else return(Nclause(t,NULL,MEDIUM));
}
return(new_pred_set(ccopy));
}
struct clause *new_pred_set(cc) /* set new pred & return */
struct variant *cc;
{
struct func *newfunc;
struct term *t1,*t2;
struct clause *c1,*c2;
register struct vpair *a;
register int i;
int arity,vpair_length(); /* tr_split.c */
STAT_DEF++; /* statistics */
while (1) {
sprintf(nbuf, "%s%d", genname, GENSYM++);
if (exist_fname(nbuf) == NULL) break;
}
arity = vpair_length(cc->v_pair);
newfunc = Nfunc(TEMPFUN, nbuf, arity);
newpred(newfunc);
(t1 = Nterm(arity,MEDIUM))->type.t_func = newfunc; /* orig. head */
(t2 = Nterm(arity,MEDIUM))->type.t_func = newfunc; /* copy head */
c1 = Nclause(t1,NULL,MEDIUM); /* new constraint */
c2 = Nclause(t2,cc->v_clause,MEDIUM); /* new head == body */
for (i = arity - 1, a = cc->v_pair; 0 <= i; i--,a=a->v_link)
{
Arg(t1,i) = a->v1;
Arg(t2,i) = a->v2;
}
set_new_def(c2,cc->v_var,cc->v_anum); /* to DEF_list */
return(c1);
}
void set_new_def(c,vl,anum) /* add c to DEF_list */
struct clause *c; /* head == body. */
struct term *vl;
int anum;
{
register struct cset *s;
s = Ncset(TEMPORAL);
s->cs_status = DERIVATION;
s->cs_clause = c;
s->cs_link = DEF_list;
s->cs_anumber = anum;
s->cs_vlist = vl;
DEF_list = s; /* global var */
}
int is_modular_head(t) /* check head t is modular or not */
struct term *t;
{
struct func *f;
register int i;
register struct term *arg;
if (! is_functor(t)) {
wfp = stderr;
Pterm(t,NULL_ENV);
error("Only Functors can be used as Constraints");
}
f = Pred(t);
for (i = 0; i < f->f_arity; i++)
{
arg = Arg(t,i);
if (isvar(arg))
{
if (vheadoccurrence(arg) > 1) /* double occurrence */
return(FALSE);
}
else if (is_pst(arg)) continue; /* 91.10.1 ??? */
else return(FALSE);
}
return(TRUE);
}
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
foldunfold()
fold/unfold transformation loop
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int foldunfold() /* fold-unfold transformation main */
{
register struct cset *cs;
struct clause *body;
register struct func *f;
void unfold_derivation(),unfold_cstr(),set_temporal_def();
for (;;)
{
clear_up_DEF();
if (check_INITDEF() == FALSE) return(FALSE);
TTB
P_status(); /* print stack */
if Is_ctstep
if (step_asking() != 0) continue; /* user's input */
TTE
/* target def-clause */
for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
if (cs->cs_status == DERIVATION) break;
if (cs != NULL) /* unfold def-clause */
{
STAT_UNFOLD++;
unfold_derivation(cs);
continue;
}
/* get one clause from CSTR_list*/
for (cs = CSTR_list; cs != NULL; cs = cs->cs_link)
if (cs->cs_status == UNTOUCHED) break;
if (cs == NULL) return(TRUE); /* no target --> fail */
f = Pred(cs->cs_clause->c_form);
if (is_modular_head(cs->cs_clause->c_form))
{
STAT_UNFOLD++;
unfold_cstr(cs);
continue;
}
body = modular_form(cs->cs_clause->c_link,
cs->cs_vlist, cs->cs_anumber);
cs->cs_clause->c_link = body;
if (body == MFAIL) /* fail transformation */
{
cs->cs_status = REMOVED;
f->f_setcount--;
}
else if (body == NULL) /* unit definition */
{
cs->cs_status = UNIT_DEFINED;
f->f_unitcount++;
/* M-solvability */
if (Is_Msolvable) set_temporal_def(f);
TTB
tprint1("#reduce body <%d>",cs->cs_number);
TTE
}
else
{
cs->cs_status = MODULAR_DEFINED;
TTB
tprint1("#modularize <%d>",cs->cs_number);
TTE
}
}
}
void set_temporal_def(f)
struct func *f;
{
register struct cset *cs;
for (cs = CSTR_list; cs != (struct cset *)NULL; cs = cs->cs_link) {
switch (cs->cs_status) {
case UNTOUCHED:
if (f == Pred(cs->cs_clause->c_form))
cs->cs_status = TEMPORAL_DEFINED;
break;
case MODULAR_DEFINED:
if (f == Pred(cs->cs_clause->c_link->c_form)) {
cs->cs_status = TEMPORAL_DEFINED;
set_temporal_def(Pred(cs->cs_clause->c_form));
}
}
}
}
struct clause *reorder(cl,tc) /* used in unfold_derivation, _cstr */
struct clause *cl,*tc; /* cl:literals, tc:target literal */
{
register struct clause *c;
if (cl == NULL_CL) return(NULL_CL);
for (c = cl; c != NULL_CL; c = c->c_link)
if (c->c_link == tc) break;
if (c == NULL_CL) return(cl);
else {
c->c_link = tc->c_link;
tc->c_link = cl;
return(tc);
}
}
void unfold_derivation(cs) /* unfold derivation clause (in unfoldfold) */
struct cset *cs;
{
struct clause *tc,*ccopy;
struct func *f;
struct itrace *it;
int res;
ccopy = surface_copy_clause(cs->cs_clause,ETERNAL);
tc = target_literal(cs->cs_clause->c_link);
cs->cs_clause->c_link = reorder(cs->cs_clause->c_link,tc);
if (tc == NULL) /* no need for transformation */
{
cs->cs_status = REGISTERED;
return;
}
TTB /* print target literal */
tprint1("#unfold-[%d] ",cs->cs_number);
Pterm(tc->c_form,NULL);
TTE
res = apply(tc->c_form,cs->cs_clause->c_form,
tc->c_link,cs->cs_anumber);
f = Pred(cs->cs_clause->c_form);
f->f_integ = it = snew(itrace);
it->it_clause = ccopy; /* BUG 92/11/4 */
it->it_anumber = cs->cs_anumber;
it->it_cnumber = literalnumber(cs->cs_clause->c_link);
it->it_link = newf_list; newf_list = it;
if (res == FALSE)
{
it->it_clause->c_form = FAIL;
cs->cs_status = FALSE_REGISTERED;
remove_from_CSTR(f);
TTB tprint0(" ->FAIL"); TTE
}
else
{
if (f->f_unitcount > 0)
cs->cs_status = REGISTERED;
else cs->cs_status = REMOVED;
TTB tprint0(" =>TRUE"); TTE
}
}
void insert_cs(cs,newcs) /* used in unfold_cstr */
struct cset *cs, *newcs; /* append newcs after cs */
{
register struct cset *c;
if (newcs == NULL) return;
for (c = newcs; c->cs_link != NULL; c = c->cs_link);
/* c <= end of newcs */
c->cs_link = cs->cs_link;
cs->cs_link = newcs;
}
struct cset *from_to(s1,s2) /* used in unfold_cstr */
struct cset *s1,*s2; /* s1->..->c->s2 ===> s1->..->c->NULL*/
{
struct cset *c;
if (s1 == s2) return(NULL);
for (c = s1; c->cs_link != s2; c= c->cs_link);
c->cs_link = NULL;
return(s1);
}
void unfold_cstr(cs) /* unfold CSTR clause (in unfoldfold) */
struct cset *cs;
{
struct clause *tc;
struct func *f;
int res;
struct cset *cstr_save; /* old CSTR_list */
f = Pred(cs->cs_clause->c_form);
tc = target_literal(cs->cs_clause->c_link);
cs->cs_clause->c_link = reorder(cs->cs_clause->c_link,tc);
if (tc == NULL) /* no need for transformation */
{
cs->cs_status = MODULAR_DEFINED;
return;
}
TTB /* print target literal */
tprint1("#unfold=[%d] ",cs->cs_number);
Pterm(tc->c_form,NULL);
TTE
f->f_setcount--;
cs->cs_status = REMOVED;
cstr_save = CSTR_list;
res = apply(tc->c_form,cs->cs_clause->c_form,
tc->c_link,cs->cs_anumber);
if (res == FALSE)
{
TTB tprint0(" ->FAIL"); TTE
}
else
{
struct cset *newcs;
newcs = from_to(CSTR_list,cstr_save); /* new defs */
CSTR_list = cstr_save;
insert_cs(cs,newcs); /* put newcs after cs */
TTB tprint0(" =>TRUE"); TTE
}
}
/*
[apply]-------------------- head unification & goal replacement
. [system_function]
. <system_pred> ---> defsysp.c
. <reduce_clause> ---> tr_sub.c
. apply_add_clause
. . <up_eclause> ---> modular.c
. . <satisfiable~> ---> tr_sub.c
. . <add_clause>+ ---> tr_sub.c
. extend_apply+
. . [tunify]
. . eclause_conc.
*/
int apply(target,head,rest,anum) /* head:-target,rest. */
struct term *target,*head;
struct clause *rest;
int anum;
{
struct pair *e0;
struct func *f = Pred(target);
struct node *dummy;
struct eclause *ec;
struct pair *esave = ep;
struct ustack *usave = usp;
if (anum > 0) e0=Nenv(anum);
else e0=NULL_ENV;
if (issystem(f)) {
dummy = Newnode(NULL,NULL,NULL,NULL,NULL);
if (isfunc(f)) {
if (system_function(target,e0,dummy) == SYSFAIL) {
ep = esave;
return(FALSE);
}
/* has solution */
ec = reduce_clause(rest,e0);
if (ec == (struct eclause *)MFAIL)
{
ep = esave; return(FALSE);
}
apply_add_clause(head,e0,ec);
ep = esave;
return(TRUE);
}
else { /* isnonfunc */
if (system_pred(target,e0,dummy,dummy,DOWN) == SYSFAIL)
return(FALSE);
/* has possibly many solutions */
do {
ec = reduce_clause(rest,e0);
apply_add_clause(head,e0,ec);
undo(usave);
if (anum > 0) e0 = Nenv(anum);
else e0=NULL_ENV;
} while (system_pred(target,e0,dummy,dummy,BACKTRACK) == SYSTRUE);
ep = esave;
undo(usave);
return(TRUE);
}
}
/* user predicate */
return(extend_apply(target,head,rest,e0,f,f->def.f_set));
}
int extend_apply(target,head,rest,e0,f,s) /* in apply */
struct term *target,*head;
struct clause *rest;
struct pair *e0;
struct func *f;
register struct set *s;
{
struct eclause *ec;
struct ustack *usave = usp;
int *hsave,cn;
struct pair *e1;
if (s == (struct set *)NULL) {
if (Handle_Undefined == TRUE) {
sprintf(nbuf,">>> %s <<< is UNDEFINED!",f->f_name);
error(nbuf);
}
else return(FALSE);
}
for (cn = 0 ; s != NULL; s = s->s_link) {
hsave = hp;
if (s->s_ground_head) /* no var/PST in the head */
{
if (tunify(target,e0,
s->s_clause->c_form,NULL,2)==FALSE) /* safe unify */
{
hp = hsave;
continue;
}
if (s->s_anumber > 0) e1 = Nenv(s->s_anumber);
else e1 = NULL_ENV;
}
else
{
if (s->s_anumber > 0) e1 = Nenv(s->s_anumber);
else e1 = NULL_ENV;
if (tunify(target,e0,
s->s_clause->c_form,e1,2)==FALSE) /* safe unify */
{
hp = hsave;
continue;
}
}
ec = eclause_conc(reduce_clause(s->s_clause->c_link, e1),
eclause_conc(reduce_clause(s->s_constraint,e1),
reduce_clause(rest,e0)));
if (apply_add_clause(head,e0,ec)!=FALSE)
cn++; /* # of new clauses */
undo(usave); /* restore environments */
}
if (cn == 0) return(FALSE);
else return(TRUE);
}
int apply_add_clause(head,e0,ec) /* in apply, extend_apply */
struct term *head;
struct pair *e0;
struct eclause *ec;
{
struct clause *newbody;
struct term *newhead;
struct pair *e1;
int i;
if (ec == (struct eclause *)MFAIL) return(FALSE);
up_init();
newhead = termset(head, e0,MEDIUM);
newbody = up_eclause(ec,MEDIUM);
if (p_number != 0) {
renum_pvars((struct pstvar *)pv_list,v_number);
if (p_number > 0) e1=Nenv(p_number);
else e1=NULL_ENV;
i = p_number;
while (i > 0) {
i--;
e1[i].p_body = ((struct pstvar *)pv_list)->old_var;
e1[i].p_env = e0;
pv_list = ((struct pstvar *)pv_list)->v_link;
}
}
up_restore();
if (newbody != NULL && v_number == 0 && p_number == 0)
{ /* containts no variables */
if (satisfiable(newbody,0)) newbody = NULL;
else return(FALSE);
}
add_clause(Nclause(newhead,newbody,MEDIUM), v_list, v_number+p_number);
return(TRUE);
}
syntax highlighted by Code2HTML, v. 0.9.1