/* ----------------------------------------------------------
% (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 <stdio.h>
#include <math.h>
/* 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
syntax highlighted by Code2HTML, v. 0.9.1