/* ---------------------------------------------------------- % (C)1992 Institute for New Generation Computer Technology % (Read COPYRIGHT for detailed information.) ----------------------------------------------------------- */ /*===================================================================== * cu-Prolog III (Constraint Unification Prolog) * header files: include.h, funclist.h, varset.h, globalv.h, sysp.h, * syspdef.h * Prolog: main.c, mainsub.c, new.c, read.c, print.c, refute.c, unify.c * System predicates: defsysp.c, syspred1.c, syspred2.c, jpsgsub.c * Constraint: modular.c, trans.c, tr_sub.c, tr_split.c ==================================================================== */ /*-------------------------------------------------------------------- * << include.h >> * (define structures, macros, etc) * * 91.12 cu-Prolog III release * 92.7 refine for ICOT Free Software release * 93.7.30 --------------------------------------------------------------------*/ #include #include /* CPUTIME : print CPU time for UNIX 4.2 BSD * if your system has times() function #define CPUTIME 60 * if your system is SUN4 #define SUN4 1 * else #define CPUTIME 0 */ #ifdef __FreeBSD__ #define CPUTIME 60 #else #define SUN4 1 #endif #define KANJI 1 /* 1: allow EUC Kanji for str functions */ /* Tee print macro */ #define tputc(X) {if (wfp) putc(X,wfp);if (lfp) putc(X,lfp);} #define tprint0(X) {if (wfp) fprintf(wfp,X);if (lfp) fprintf(lfp,X);} #define tprint1(X,V) {if (wfp) fprintf(wfp,X,V);if (lfp) fprintf(lfp,X,V);} #define tprint2(X,V1,V2) {if (wfp) fprintf(wfp,X,V1,V2);\ if (lfp) fprintf(lfp,X,V1,V2);} #define tprint3(X,V1,V2,V3) {if (wfp) fprintf(wfp,X,V1,V2,V3);\ if (lfp) fprintf(lfp,X,V1,V2,V3);} #define tprint4(X,V1,V2,V3,V4) {if (wfp) fprintf(wfp,X,V1,V2,V3,V4);\ if (lfp) fprintf(lfp,X,V1,V2,V3,V4);} #define NL tputc('\n') #define readword(S) fscanf(fp,"%s",S);if (lfp) fprintf(lfp,"%s",S); #define skipline while (cbuf != '\n') next() #define KEYIN (fp == stdin) #define advance (next(), adv()) /* string equal */ #define streq(p,q) (*(p) == *(q) && strcmp(p,q) == 0) /* type of token */ #define NAME 0 #define NUMBER 1 #define STRING 2 #define FILE_TYPE 3 #define VARNAME 4 #define BRACKET 5 /* ()[]| */ #define COMMA 6 /* , */ #define FULLSTOP 7 /* . */ #define CONST_MARK 8 /* ; */ /* VT-100 Escape Sequence */ #define C_HIGHLIGHT "\033[01m" #define C_UNDER "\033[04m" #define C_BLINK "\033[05m" #define C_REVERSE "\033[07m" #define C_NORMAL "\033[0m" #define C_SAVE "\033[s" #define C_LOAD "\033[u" #define C_CLS "\033[2J" /* storage type */ #define TEMPORAL 0 #define MEDIUM 1 #define ETERNAL 2 #define STINGY 3 /* flag for checking constant term used in Rterm and termset */ #define CONSTANT_TERM 1 #define NOT_CONSTANT_TERM 0 /* discrimination of term */ #define VAR_VOID_TYPE 1 #define VAR_PST_TYPE 2 #define VAR_GLOBAL_TYPE 3 #define ATOMIC_TYPE 4 #define PST_TYPE 5 #define PST_ITEM_TYPE 6 #define CLAUSE_TYPE 7 #define ECLAUSE_TYPE 8 #define LIST_TYPE 9 #define CONST_LIST_TYPE 10 struct term { /* atomic formula (literal) */ union { int ident; /* descriminated accordint to this */ struct func *t_func; /* functor(predicate) name */ } type; int t_arity; /* arity. when < 0 complex const */ union { struct term *t_arg[1]; /* args */ float n_value; char *s_value; FILE *f_value; } tag; }; #define NULL_TERM (struct term *)NULL #define FLOAT_NUM 0 #define INT_NUM 1 /* #define STRING 2 */ #define FILE_POINTER 3 /* num,string,file */ #define is_atomic(Term) (Term->type.ident == ATOMIC_TYPE) #define is_num(Term) (is_atomic(Term) && (Term->t_arity <= INT_NUM)) #define is_string(Term) (is_atomic(Term) && (Term->t_arity == STRING)) #define EUCOS 0x80 /* EUC offset */ #define is_int(Term) (is_atomic(Term) && (Term->t_arity == INT_NUM)) #define is_file(Term) (is_atomic(Term) && (Term->t_arity == FILE_POINTER)) #define is_pst(Term) ((Term)->type.ident == PST_TYPE) #define is_pstitem(Term) ((Term)->type.ident == PST_ITEM_TYPE) #define is_list(Term) (((Term)->type.ident == LIST_TYPE) ||\ ((Term)->type.ident == CONST_LIST_TYPE)) #define is_clause(Term) ((Term)->type.ident == CLAUSE_TYPE) #define is_eclause(Term) ((Term)->type.ident == ECLAUSE_TYPE) #define num_value(Term) ((Term)->tag.n_value) #define str_value(Term) ((Term)->tag.s_value) #define filep_value(Term) ((Term)->tag.f_value) #define head_of_list(Term) (((struct clause *)Term)->c_form) #define tail_of_list(Term) ((struct term *)((struct clause *)Term)->c_link) #ifdef __FreeBSD__ #define is_readable(FP) (FP->_flags & __SRD) #define is_writable(FP) (FP->_flags & __SWR) #else #define is_readable(FP) (FP->_flag & _IOREAD) #define is_writable(FP) (FP->_flag & _IOWRT) #endif #define is_functor(Term) ((Term)->type.ident > CONST_LIST_TYPE) #define isconst_functor(Term) ((Term)->t_arity <= 0) #define isconst(Term) (is_atomic(Term) || \ (is_functor(Term) && (isconst_functor(Term)))) #define notconst(Term) (isvar(Term) || is_pst(Term) ||\ ((! is_atomic(Term)) && (Term->t_arity > 0))) #define isatom(Term) (is_atomic(Term) || (Term->t_arity == 0)) #define Arg(T,N) (T)->tag.t_arg[N] /* N+1 th argument of term T */ #define Arg1(T) Arg(T,0) #define Arg2(T) Arg(T,1) #define Arg3(T) Arg(T,2) #define Arg4(T) Arg(T,3) #define Arg5(T) Arg(T,4) #define Pred(T) (T)->type.t_func /* predicate symbol */ #define Predname(T) (T)->type.t_func->f_name /* predicate symbol name */ #ifndef FLT_EPSILON /* ==2^-23 */ /* #define FLT_EPSILON 1.19209290E-07 */ #define FLT_EPSILON 2E-07 #endif #define atomic_equal(u,t) \ (is_atomic(t) && (t->t_arity == u->t_arity) &&\ ( (is_int(t) && ((int)num_value(t) == (int)num_value(u))) || \ (is_num(t) && \ ((float)fabs(num_value(t)-num_value(u)) \ <= FLT_EPSILON*fabs(num_value(t)))) ||\ (is_string(t) && (strcmp(str_value(t),str_value(u)) == 0)) ||\ (is_file(t) && (filep_value(t) == filep_value(u))))) struct var { int v_type; /* v_type = VAR_TYPE */ int v_number; char *v_name; struct var *v_link; struct clause *v_constraint; /* constraint of CAHC */ struct component *v_component; /* used in the component check */ short int v_head_occur; /* var occurrence in head */ short int v_occurrence; /* var occurrence */ }; #define isvar(t) ( ((struct var *)t)->v_type <= VAR_GLOBAL_TYPE \ && ((struct var *)t)->v_type >= VAR_VOID_TYPE ) #define novar(Term) (is_atomic(Term) ||\ (Term->type.ident == CONST_LIST_TYPE) ||\ ((! isvar(Term)) && (Term->t_arity <= 0))) #define is_voidvar(t) (((struct var *)t)->v_type == VAR_VOID_TYPE) #define is_notvoidvar(t) (((struct var *)t)->v_type == VAR_GLOBAL_TYPE ||\ ((struct var *)t)->v_type == VAR_PST_TYPE) #define vname(t) (((struct var *)t)->v_name) #define vnumber(t) (((struct var *)t)->v_number) #define voccurrence(t) (((struct var *)t)->v_occurrence) #define vheadoccurrence(t) (((struct var *)t)->v_head_occur) #define vincrement(t) ((struct var *)t)->v_occurrence++ #define vdecrement(t) ((struct var *)t)->v_occurrence-- #define vconstraint(t) (((struct var *)t)->v_constraint) #define vcomponent(t) (((struct var *)t)->v_component) #define vlink(t) ((struct term *)(((struct var *)t)->v_link)) typedef int (*SYSFUNC)(); /* for system predicate */ struct component /* component of arguments */ { struct func *c_label; struct component *c_next; }; #define Component(F,N) (F)->f_component[N] /* N+1 th argument of func F */ #define NOPSTLABEL (struct func *)NULL /* label of non-PST term */ struct func { /* predicate (functor) */ unsigned short int f_arity, f_number, f_mark; unsigned short int f_setcount; /* number of definitions */ char *f_name; union { struct set *f_set; /* definition clauses */ SYSFUNC f_sysfunc; /* system function */ } def; struct func *f_link; struct itrace *f_integ; /* integrate() history */ int f_unitcount; /* number of unit defs */ struct component *f_component[1]; /* component of arguments */ }; /* predicate(functor) type definition */ #define USERFUN 0 /* user function, default value */ #define SYSFUN 1 /* system pred */ #define SPYFUN 2 /* spy fun. or not */ #define REDUCEDFUN 4 /* reduced fun. or not */ #define FINITEFUN 8 /* finete fun. or not */ #define TEMPFUN 16 /* temporary func */ #define NEWPRED 32 /* new predicate */ #define NONFUNC 64 /* non-functional (many solutions) */ #define TYPE1SYS 9 /* system (functional) pred */ #define TYPE1SYS_REDUCED 13 /* reduced # of arguments system pred */ #define TYPE2SYS 65 /* system (non-functional) pred */ #define TYPE2SYS_REDUCED 69 /* reduced # of arguments system non-functional */ #define NON_UNFOLDABLE 128 /* non unfoldable pred at the unfold/fold */ #define STAY_IF 256 /* stay if TRUE/FALSE for NON_UNFOLDABLE pred */ #define STAY_IF_TRUE_PRED 384 #define STAY_IF_FALSE_PRED 128 #define VACUITY_NOCHECK 512 /* vacuity non check flag */ #define COMPONENT_CHECKED 1024 /* component checked */ /* #define systemfun(F) (F->f_mark) != SYSFUN #define userfun(F) (F->f_mark) &= (^SYSFUN) */ #define issystem(F) ( ((F->f_mark) & SYSFUN) != 0 ) #define isuser(F) ( ((F->f_mark) & SYSFUN) == 0 ) #define isnonfunc(F) ( ((F->f_mark) & NONFUNC) != 0 ) #define isfunc(F) ( ((F->f_mark) & NONFUNC) == 0 ) #define is_funcsys(F) (issystem(F) && isfunc(F)) #define is_nofuncsys(F) (issystem(F) && isnonfunc(F)) #define spyfun(F) (F->f_mark) |= SPYFUN #define nospyfun(F) (F->f_mark) &= (~SPYFUN) #define spychange(F) (F->f_mark) ^= SPYFUN #define isspy(F) ( ((F->f_mark) & SPYFUN) != 0 ) #define isnospy(F) ( ((F->f_mark) & SPYFUN) == 0 ) #define reducedfun(F) (F->f_mark) |= REDUCEDFUN #define isreduced(F) ( ((F->f_mark) & REDUCEDFUN) != 0) #define isnoreduced(F) ( ((F->f_mark) & REDUCEDFUN) == 0) #define finitefun(F) (F->f_mark) |= FINITEFUN #define recursivefun(F) (F->f_mark) &= (~FINITEFUN) #define isfinite(F) ( ((F->f_mark) & FINITEFUN) != 0) #define isrecursive(F) ( ((F->f_mark) & FINITEFUN) == 0) #define newpred(F) (F->f_mark) |= NEWPRED #define isnewpred(F) ( ((F->f_mark) & NEWPRED) != 0) #define isnotnewpred(F) ( ((F->f_mark) & FINITEFUN) == 0) #define isallunit(F) (F->f_setcount == F->f_unitcount) #define component_checked(F) (F->f_mark) |= COMPONENT_CHECKED #define component_not_checked(F) (F->f_mark) &= (~COMPONENT_CHECKED) #define is_component_checked(F) ( ((F->f_mark) & COMPONENT_CHECKED) != 0 ) #define is_component_not_checked(F) ( ((F->f_mark) & COMPONENT_CHECKED) == 0 ) /* type of operator */ #define PREFIX 0100 #define POSTFIX 0200 #define INFIX 0300 struct operator { struct func *o_func; int o_prec; /* precedence of operator 0-1200 */ int o_type; /* type of operator: xf,yf,fx,fy,xfy,yfx,xfx */ /* bit pattern of o_type is: PREFIX=0100, POSTFIX=0200, INFIX=0300, leftdown = 0010, rifgtdown = 0001 xf -- 0210, yf -- 0200, fx -- 0101, fy -- 0100, xfy -- 0310, yfx -- 0301, xfx -- 0311 */ struct operator *o_link; /* link to another operator */ }; struct clause { /* sequence of atomic formula */ int c_type; /* CLAUSE_TYPE or LIST_TYPE */ struct term *c_form; /* atomic formula */ struct clause *c_link; }; #define NULL_CL (struct clause *)NULL struct set { /* definition horn clause */ unsigned short int s_anumber; unsigned short int s_bodynumber; /* number of body literals */ int s_ground_head; /* the head is ground or not : TRUE/FALSE */ struct clause *s_clause; /* Horn clause */ struct set *s_link; /* next def */ struct term *s_vlist; /* variables */ struct clause *s_constraint; /* constraint clause */ }; struct cset{ /* clause stack */ struct clause *cs_clause; struct term *cs_vlist; unsigned short int cs_anumber; /* v_number + p_number */ unsigned short int cs_status; /* 0: not unfolded 1: unfolded */ unsigned short int cs_cnum; /* the number of literals in the body */ unsigned short int cs_number; /* set number */ struct cset *cs_mother; /* mother derivation clause */ struct cset *cs_link; }; #define is_unitclause(Set) (Set->s_bodynumber == 0) /* dummy definition (for non-functional system predicate) */ #define DUMMY_DEF (struct set *)1 struct pair { /* environment for SS */ struct term *p_body; /* term */ struct pair *p_env; /* environment */ }; #define NULL_ENV (struct pair *)NULL struct ustack { /* user stack */ int *u_addr; /* address */ int u_val; /* content */ }; struct node { /* node for Prolog refutation */ struct clause *n_clause; /* goal */ struct pair *n_env; /* variable environment */ struct set *n_set; /* OR-program clauses */ struct node *n_link, *n_last; struct eclause *n_constraint; /* constraint of CAHC */ unsigned short int n_count, n_spy, n_tmp, n_scount; int *n_hp; struct pair *n_ep; struct ustack *n_usp; }; #define NULL_NODE (struct node *)NULL struct eclause { /* environment + clause(copy) */ int c_type; struct term *c_form; /* atomic formula */ struct eclause *c_link; /* equiv eclause link */ struct pair *c_env; /* formular environment */ }; #define NULL_ECL (struct eclause *)NULL struct itrace{ /* integrate trace */ unsigned short int it_anumber, it_cnumber; /* #of var,literals (key) */ struct clause *it_clause; /* Horn clause (history) */ struct itrace *it_link; }; struct pst { /* Partial Specified Term */ int type; /* PST_TYPE */ struct term *p_var; /* var comes here */ struct eclause *p_lists; /* property lists */ }; struct pstvar { int v_type; /* v_type = VAR_PST_TYPE */ int v_number; char *v_name; struct term *v_link; struct term *old_var; }; struct pst_item { struct pair *p_var; /* PST var */ struct eclause *p_lists; /* property lists */ struct pst_item *p_link; /* link to other items */ }; #define NULL_PSTIT (struct pst_item *)NULL /* deref: if (t,e) is var ,then p != NULL, else p == NULL */ /* t,p,e must be variables !!!! */ #define down(p, t, e)\ while(1){ \ if (is_notvoidvar(t)) {\ p = &e[vnumber(t)];\ if (p->p_body == NULL_TERM) break;\ t = p->p_body;\ e = p->p_env;\ }\ else if (is_voidvar(t)) {p = Anonymous_env; break; }\ else { p = NULL_ENV; break; } } /* various modes of cu-Prolog */ #define Notrace_mode tflag = 0 #define Normaltrace_mode tflag = 1 #define Steptrace_mode tflag = 2 #define Leap_mode tflag = 3 #define Is_Notrace (tflag == 0) #define Is_Normaltrace (tflag == 1) #define Is_Steptrace (tflag == 2) #define Is_Leap (tflag == 3) #define Is_Trace (tflag != 0) #define Msolvable_mode sflag = 0 #define Modular_mode sflag = 1 #define Is_Msolvable (sflag == 0) #define Is_Modular (sflag == 1) #define Is_ctnotrace (CTmode == 0) #define Is_ctnormal (CTmode == 1) #define Is_ctstep (CTmode == 2) #define CTnotrace CTmode = 0 #define CTnormal CTmode = 1 #define CTstep CTmode = 2 /* c.t. trace(normal, step) begin&end */ #define TTB if (CTmode != 0){ #define TTE TE /* c.t. step trace begin&end */ #define TSTB if Is_ctstep { #define TSTE TE /* c.t. normal trace begin&end */ #define TNTB if Is_ctnormal { #define TNTE TE /* trace begin & end */ #define TB if (Is_Trace) { #define STB(F) if (Is_Trace && isspy(F) ) { #define TE NL; } #define STE TE /* modularize fail */ /* #define MFAIL (struct clause *)1 */ /* return value of the execution of system predicate */ #define SYSNO 1 /* is not system pred. */ #define SYSTRUE 2 /* system pred. success */ #define SYSFAIL 3 /* system pred. fail */ #define SUSPEND 4 #define TRUE 1 #define FALSE 0 /* refutation search staus flag used in syspred.c, refute.c */ #define DOWN 1 #define UP 2 #define BACKTRACK 3 /* predicate symbol hash table size */ #define HASH_SIZE 478 #define NAMELEN_MAX 1024 /* size of name buffer */ #define REFMAX 10000 /* refutation max (Refcount) default */ #define Modmax_def 50 /* modularize max (MODULAR_MAX) default */ /* struct allocation macro s:struct name */ #define snew(s) (struct s *)salloc(sizeof (struct s) / sizeof (int)) #define cnew(s) (struct s *)challoc(sizeof (struct s) / sizeof (int)) #define new(s) (struct s *)alloc(sizeof (struct s) / sizeof (int)) #define MEMORY_ALLOC(X,Y,F) \ switch (F) { \ case TEMPORAL: \ X=new(Y); break;\ case MEDIUM: \ X=cnew(Y); break; \ default:\ X=snew(Y); } #define in_sheap(X) (( &sheap[0] <= ((int *)X)) && (((int *)X) < shp)) #define Npstobj(Head,Env,Tail,Flag) Neclause(Head,Env,Tail,Flag) /* the maximum number of variables */ #define VMAX 30 /* for constraint transformation (trans.c tr_sub.c tr_split.c) */ /* values of cs->cs_status */ #define REMOVED 1 /* for CSTR_list */ #define UNTOUCHED 0 #define MODULAR_DEFINED 2 #define UNIT_DEFINED 3 /* for DEF_list */ #define DERIVATION 4 #define REGISTERED 5 #define FALSE_REGISTERED 6 #define REDUCED_DEF 7 /* for M-solvability */ #define TEMPORAL_DEFINED 8 struct compartment{ struct clause *cmp_clause; struct compartment *cmp_link; }; struct vpair{ /* link between v1 and v2 */ struct term *v1; /* original var or pst */ struct term *v2; /* variant var or pst */ struct vpair *v_link; }; struct variant { struct clause *v_clause; /* variant clause */ struct term *v_var; /* variable list in v_clause */ struct vpair *v_pair; /* variable correspondence */ int v_anum; /* # of v+ # of pst */ }; /* maximum number of open files */ #define MAX_OPEN_FILES 20 #define FILE_NAME_LEN 128 /* heap units */ #define SHEAP_UNIT (sizeof(int)) #define HEAP_UNIT (sizeof(int)) #define CHEAP_UNIT (sizeof(int)) #define ESP_UNIT (sizeof(struct pair)) #define USTACK_UNIT (sizeof(struct ustack)) #define NAME_UNIT (sizeof(char)) /**************** global functions *************/ #include "funclist.h" /**************** global vars ******************/ #if MAIN == 1 #include "varset.h" struct func *hash_list[HASH_SIZE]; /* predicate hash table */ #else #include "globalv.h" extern struct func *hash_list[]; #endif /*************** system predicate *************/ #if SYSPRED == 1 #include "syspdef.h" #else #include "sysp.h" #endif