/* ----------------------------------------------------------
% (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
==================================================================== */
/*--------------------------------------------------------------------
* << tr_split.c >>
* divide constraint into equivalence classes
* 93.8.2 speedup copy_term
* 93.8.2 speedup copy_term
--------------------------------------------------------------------*/
#include "include.h"
#define DEBUG 0
extern struct cset *DEF_list;
extern struct cset *CSTR_list;
extern struct cset *INITDEF_list;
extern int CSTR_number;
extern struct clause *CONST_literals, *REST_literals;
extern struct itrace *newfsave;
extern jmp_buf trans_fail;
/* sub functions for transform.c (divide clause into equivalence classes)*/
/* this modulue uses global vars: CONST_literals, REST_literals
*
. . split+
. . . vconstraint.
. . . attach+
. . . . is_modular_literal~
. . . . attach_arg+
. . . . . novar
. . . . . replace_terms+
. . . . has_no_var+
. . . . . novar~
. . . divide_consts
. . . . has_no_pst+
. . . delete_constraint+
. . . remove_modular_literals+
. . . . is_modular_literal~
*/
/* ------------- begin 'split' ------------------ */
struct clause *CONST_PST_literals; /* used in split, divide_consts */
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++
split(clist,vlist,anum)
split a clause clist into equivalence class
vlist = variable list of clist
anum = # of variables + # of PSTs in clist
global vars:
CONST_literals : no vars and no psts
REST_literal : modular literals
+++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct compartment *split(clist, vlist, anum)
struct clause *clist;
struct term *vlist;
int anum;
{
register struct term *v;
register struct compartment *cmp,*cmplast;
struct clause *cnext,*remove_modular_literals();
void divide_consts();
CONST_literals = NULL; /* global vars */
REST_literals = NULL;
CONST_PST_literals = NULL;
clist = remove_modular_literals(clist);
if (clist == NULL) return(NULL);
else if (vlist == NULL) /* no variable */
divide_consts(clist); /* CONST or CONST_PST? */
else
{
/* clear_vconstraint(vlist) */
for (v = vlist; v != NULL; v = vlink(v))
vconstraint(v) = NULL;
if (attach(clist, vlist,anum) == FALSE)
return((struct compartment *)MFAIL);
delete_constraint(vlist);
}
for (cmplast = NULL; CONST_PST_literals != NULL;
CONST_PST_literals = cnext)
{
cnext = CONST_PST_literals->c_link;
CONST_PST_literals->c_link = NULL;
MEMORY_ALLOC(cmp,compartment,TEMPORAL);
cmp->cmp_clause = CONST_PST_literals;
cmp->cmp_link = cmplast;
cmplast = cmp;
}
for (v = vlist; v != NULL; v = vlink(v))
if (vconstraint(v) != NULL){
MEMORY_ALLOC(cmp,compartment,TEMPORAL);
cmp->cmp_clause = vconstraint(v);
cmp->cmp_link = cmplast;
cmplast = cmp;
}
return(cmplast);
}
/* remove modular literals in cl into REST_literals */
struct clause *remove_modular_literals(cl)
struct clause *cl;
{
register struct clause *cnext;
if (cl == NULL) return(NULL);
if (is_modular_literal(cl->c_form))
{
cnext = cl->c_link;
cl->c_link = REST_literals;
REST_literals = cl;
return(remove_modular_literals(cnext));
}
else
{
cnext = cl->c_link;
cl->c_link = remove_modular_literals(cnext);
return(cl);
}
}
void delete_constraint(vl) /* vconstraint(v)=NULL for all vl */
struct term *vl;
{
register struct term *v1, *v2;
register struct clause *c;
for (v1 = vl; v1 != NULL; v1 = vlink(v1))
{
if (vconstraint(v1) == NULL) continue;
c = vconstraint(v1);
for (v2 = vlink(v1); v2 != NULL; v2 = vlink(v2))
if (vconstraint(v2) == c) vconstraint(v2) = NULL;
}
}
int has_no_pst(t) /* check pst in arguments */
struct term *t;
{
register int i;
for (i = 0; i < Pred(t)->f_arity; i++)
if (is_pst(Arg(t,i))) return(FALSE);
return(TRUE);
}
void divide_consts(cl) /* cl: constraint clauses */
struct clause *cl;
{
register struct clause *c,*cnext;
for (c = cl; c != NULL; c = cnext)
{
cnext = c->c_link;
c->c_link = NULL;
if (has_no_pst(c->c_form))
{
c->c_link = CONST_literals;
CONST_literals = c;
}
else
{
c->c_link = CONST_PST_literals;
CONST_PST_literals = c;
}
}
}
int Attached; /* used in attach, attach_arg */
int attach(c, vl,anum) /* split main */
register struct clause *c;
struct term *vl;
int anum;
{
struct clause *cnext;
register struct term *t;
register int i, j;
while (c != NULL) {
cnext = c->c_link;
c->c_link = NULL;
t = c->c_form; j = Pred(t)->f_mark;
if (has_no_var(t))
{
c->c_link = CONST_literals;
CONST_literals = c;
}
else if ((j & NON_UNFOLDABLE) != 0) {
i = satisfiable(c,anum);
j &= STAY_IF;
if (((i == TRUE) && (j != 0)) ||
((i == FALSE) && (j == 0))) {
j = Pred(t)->f_arity;
for (i = 0; i < j; i++)
attach_arg(Arg(t,i),c,vl);
}
else if ((i == TRUE) && (j == 0))
/* do nothing */ ;
else /* in case of FAIL */
return(FALSE);
}
else if (is_modular_literal(t)) {
c->c_link = REST_literals;
REST_literals = c;
}
else {
/* attach_term(c,vl); */
Attached = 0;
j = Pred(t)->f_arity;
for (i = 0; i < j; i++)
attach_arg(Arg(t,i),c,vl);
if (Attached == 0) divide_consts(c);
}
c = cnext;
}
return(TRUE);
}
void attach_arg(arg,c,vl) /* sub of attach */
struct term *arg,*vl;
struct clause *c;
{
register int i;
if (novar(arg)) return;
/* printf("attach_arg arg=");Pterm(arg,NULL);
printf(" c=");Pclause(c,NULL);
NL;
*/
if (isvar(arg)) {
if (arg->type.ident == VAR_GLOBAL_TYPE) { /* 1991-03-02 */
if (vconstraint(arg) == NULL) vconstraint(arg) = c;
else replace_terms(vconstraint(arg),c,vl);
Attached = 1; /* global var */
return;
}
else return;
}
if (is_list(arg) || is_clause(arg)) {
attach_arg(head_of_list(arg),c,vl);
attach_arg(tail_of_list(arg),c,vl);
return;
}
if (is_pst(arg)) {
struct eclause *plists;
plists = ((struct pst *)arg)->p_lists;
while (plists != NULL_ECL) {
attach_arg(Arg2(plists->c_form),c,vl);
plists = plists->c_link;
}
return;
}
for (i = 0; i < Pred(arg)->f_arity; i++)
attach_arg(Arg(arg,i),c,vl);
}
void replace_terms(c1,c2,vl)
struct clause *c1;
register struct clause *c2;
struct term *vl;
{
register struct term *v;
if (c1 == c2) return;
for (v = vl; v != NULL; v = vlink(v))
if (vconstraint(v) == c1) vconstraint(v) = c2;
while (c2->c_link != NULL)
c2 = c2->c_link;
c2->c_link = c1;
}
/* ------------- end of 'split' ------------------ */
/* --------------- begin 'variant' ---------------- */
struct vpair *VPAIR; /* vpair of var,pst */
int Consider_Vacuous, /* consider vacuous or not */
PST_level; /* depth of pst */
#define TPHASHSIZE 59
struct vpair *Tpair[TPHASHSIZE]; /* hashed vpair for terms */
int termpairtype(t)
struct term *t;
{
return(((int)t) % TPHASHSIZE);
}
void print_Tpair_length() /* for debug */
{
int i;
for (i=0; i<TPHASHSIZE; i++) printf("%d ",vpair_length(Tpair[i]));
printf(":%d \n",vpair_length(VPAIR));
}
void clear_Tpair()
{
register int i;
/* print_Tpair_length(); (for debug) */
for (i=0; i<TPHASHSIZE; i++) Tpair[i]=(struct vpair *)NULL;
}
void Pvariant(va)
struct variant *va;
{
struct vpair *vp;
Pclause(va->v_clause,NULL);
if (va->v_pair == NULL) return;
putchar('\n');
for (vp=va->v_pair; vp != NULL; vp=vp->v_link)
{
printf("<");
Pterm(vp->v1,NULL);putchar(',');
Pterm(vp->v2,NULL);putchar('>');
}
}
void Pvpair(va)
struct vpair *va;
{
register struct vpair *vp;
for (vp=va; vp != NULL; vp=vp->v_link)
{
printf("<");
Pterm(vp->v1,NULL);putchar(':');
Pterm(vp->v2,NULL);printf("> ");
}
}
int vpair_length(vp)
struct vpair *vp;
{
register int i;
for(i = 0; vp != NULL; i++, vp=vp->v_link);
return(i);
}
/*
[variant]-----------------------------------
. copy_clause
. . copy_term
. . . Npstobj~
. . . in_sheap~
. . . copy_arg+
. . . . has_common_label
. . . . store_vpair
. . . exist_termpair.
. . . exist_vpair.
. . . copy_pst+
. . . . Npst
. . . . store_vpair~
. . . . copy_eclause+
. . . store_termpair
. . . var_trans+
. . . . store_vpair~
*/
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
variant(cl,flag) : normal copy
variant_v(cl,flag) : consider vacuous arguments
make a variant of a clause cl
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct variant *variant_main(cl,flag)
struct clause *cl;
int flag;
{
struct variant *ccopy;
VPAIR = (struct vpair *)NULL; /* global vars */
clear_Tpair();
v_list = pv_list = NULL;
v_number = p_number = 0;
PST_level = 0;
MEMORY_ALLOC(ccopy,variant,TEMPORAL);
ccopy->v_clause = copy_clause(cl,flag);
ccopy->v_var = v_list;
ccopy->v_anum = v_number + p_number;
ccopy->v_pair = VPAIR;
if (p_number != 0)
renum_pvars((struct pstvar *)pv_list,v_number);
/* print_Tpair_length(); */
return(ccopy);
}
struct variant *variant(cl,flag)
struct clause *cl;
int flag;
{
Consider_Vacuous = 0;
return(variant_main(cl,flag));
}
struct variant *variant_v(cl,flag) /* variant considering vacuous args */
struct clause *cl;
int flag;
{
Consider_Vacuous = 1;
return(variant_main(cl,flag));
}
void store_vpair(told,tnew) /* store told->tnew (var,pst)in VPAIR */
struct term *told,*tnew;
{
register struct vpair *vp,*p,*op;
MEMORY_ALLOC(vp,vpair,TEMPORAL);
vp->v1 = told; vp->v2 = tnew;
if (VPAIR==NULL || VPAIR->v1 > told)
{
vp->v_link = VPAIR;
VPAIR = vp;
return;
}
for (p=VPAIR; p != NULL; op=p,p=p->v_link)
if (told < p->v1) break;
vp->v_link = p; /* ...op->vp->p->... */
op->v_link = vp;
}
struct term *exist_vpair(t) /* check if t is in VPAIR */
struct term *t;
{
register struct vpair *vp;
for (vp = VPAIR; vp != NULL; vp = vp->v_link)
if (t <= vp->v1)
{
if (vp->v1 == t) return(vp->v2);
else return(NULL);
}
return(NULL);
}
void store_termpair(told,tnew) /* store told->tnew (term) to TermPAIR */
struct term *told,*tnew;
{
register struct vpair *vp;
register int tt;
MEMORY_ALLOC(vp,vpair,TEMPORAL);
vp->v1 = told; vp->v2 = tnew;
tt = termpairtype(told);
vp->v_link = Tpair[tt];
Tpair[tt] = vp;
}
struct term *exist_termpair(t) /* check if t is in TermPAIR */
struct term *t;
{
register struct vpair *vp;
for (vp = Tpair[termpairtype(t)]; vp != NULL; vp = vp->v_link)
if (vp->v1 == t) return(vp->v2);
return(NULL);
}
struct clause *copy_clause(cl,flag) /* sub. of variant */
struct clause *cl;
int flag;
{
struct term *copy_term();
if (cl == NULL) return(NULL);
return(Nclause(copy_term(cl->c_form,flag),
copy_clause(cl->c_link,flag),
flag)
);
}
struct term *copy_term(t,flag) /* variant of t */
struct term *t;
int flag;
{
struct term *nt, *copy_pst(), *copy_arg();
register int i;
if (t == NULL_TERM || is_atomic(t)) return(t);
else if (isvar(t)) {
if ((nt = exist_vpair(t)) != NULL) return(nt); /* check history */
return(var_trans(t,flag)); /* t is var */
}
else if (is_pst(t)) {
if ((nt = exist_vpair(t)) != NULL) return(nt); /* check history */
PST_level++;
nt = copy_pst((struct pst *)t,flag); /* t is PST */
PST_level--;
return(nt);
}
else if ((nt = exist_termpair(t)) != NULL) return(nt); /* check history */
switch(t->type.ident) { /* atom, complex term, eclause */
case CONST_LIST_TYPE:
if (in_sheap(t) || flag != ETERNAL) return(t);
case LIST_TYPE:
nt = (struct term *)Nlist(copy_term(head_of_list(t),flag),
(struct clause *)copy_term(tail_of_list(t),flag), flag);
break;
case CLAUSE_TYPE:
nt = (struct term *)Nclause(copy_term(head_of_list(t),flag),
(struct clause *)copy_term(tail_of_list(t),flag),flag);
break;
case ECLAUSE_TYPE: /* pst object */
nt = (struct term *)Npstobj(copy_term(((struct eclause *)t)->c_form,flag),
NULL_ENV,
(struct eclause *)
copy_term((struct term *)((struct eclause *)t)->c_link,
flag),
flag);
break;
/* case VAR_VOID_TYPE:
return(Anonymous_var);
case VAR_PST_TYPE:
error("System error occurrs at 'copy_term'"); */
default:
if (isconst_functor(t))
nt = up_const_functor(t,flag);
else
{
nt = Nterm(t->t_arity,flag);
Pred(nt) = Pred(t);
if (Consider_Vacuous == 1)
for (i = 0; i < t->t_arity; i++)
Arg(nt,i) = copy_arg(t,i,flag);
else
for (i = 0; i < t->t_arity; i++)
Arg(nt,i) = copy_term(Arg(t,i),flag);
}
}
store_termpair(t,nt);
return(nt);
}
struct term *copy_pst(pt,flag) /* copy pst */
struct pst *pt;
int flag;
{
register struct pst *p;
register struct term *nt;
struct eclause *copy_eclause();
nt = exist_termpair((struct term *)pt);
if (nt != NULL)
{
if (PST_level == 1) store_vpair((struct term *)pt,nt);
return(nt);
}
p = Npst(flag);
((struct pstvar *)(p->p_var))->old_var = pt->p_var;
p->p_lists=(struct eclause *)copy_term((struct term *)pt->p_lists,flag);
if (PST_level == 1) /* top level PST */
store_vpair((struct term *)pt,(struct term *)p);
else
store_termpair((struct term *)pt,(struct term *)p);
return((struct term *)p);
}
struct term *var_trans(v, flag) /* var that corresponds to v */
struct term *v;
int flag;
{
register struct term *nv;
if is_voidvar(v) return(Anonymous_var);
sprintf(nbuf,"V%d",v_number);
nv = Nvar(nbuf,flag);
voccurrence(nv) = voccurrence(v);
vheadoccurrence(nv) = vheadoccurrence(v);
store_vpair(v,nv);
return(nv);
}
struct term *copy_arg(t,i,flag) /* copy ith argument of t with vacuity check */
struct term *t;
int i,flag;
{
register struct term *arg,*nt;
arg = Arg(t,i);
if (is_pst(arg) && (PST_level == 1) &&
!has_common_label(
((struct pst *)arg)->p_lists,Component(Pred(t),i)))
{
struct term *nv;
if ((nt = exist_vpair(arg)) != NULL)
return(nt); /* check history */
if ((nt = exist_termpair(arg)) != NULL)
return(nt); /* check history */
sprintf(nbuf,"P%d",v_number);
nv = Nvar(nbuf,flag);
store_vpair(arg,nv);
return(nv);
}
else return(copy_term(arg,flag));
}
/* ---------- end of 'variant' ----------------- */
syntax highlighted by Code2HTML, v. 0.9.1