/* dialog.c 11-11-89
**** The main interactive part of MaGIC.c. This module ****
**** contains the procedures to be executed in response ****
**** to menu selections. ****/
/************************************************************/
#include "mp_parse.c"
#define READLN { fflush(stdout); while (getchar() != '\n') ; }
char answer[80]; /* For input of axioms etc */
nt Sizmax;
/************************************************************
************************************************************/
Return 1 if 'g' selected, 0 if 'e'
Return n > 1 to change to n processes ***/
{
char menu();
while (1) switch( menu() )
{
case 'a': add_axiom(); break;
case 'b': bad_guy(); break;
case 'c': connective(); break;
case 'd': deletion(); break;
case 'e': return(0);
case 'f': fragment(); break;
case 'g': return(1);
case 'h': help(0); paws(); break;
case 'i': IO_setting(); break;
case 'j': jump_condition(); break;
case 'k': job_defaults(); break;
case 'l': logic_choice(); break;
case '#': return(n_of_procs());
}
}
/***********************************************************/
char menu() /*** Return a user choice of next action ***/
{ char c, readin();
set_frag();
display();
return( readin("abcdefghijkl#") );
}
/************************************************************/
char readin(str) char *str; /*** Return the first char
from stdin which
matches one in str. ***/
{ char ch; int i;
fflush(stdout);
while ( 1 )
{
gets(answer);
for ( i = 0; ch = answer[i]; i++ )
{
if ( isupper(ch) ) ch = tolower(ch);
if ( strchr(str,ch) ) return(ch);
}
}
}
/*********************************************************/
{
printf("\n\n Now type RETURN to continue.........");
READLN
}
/*********************************************************/
of the first " "|" ,."-delimited
substring of LOGICS matching
str, or -1 if no match. ***/
{ int i,j;
for ( i = 0; str[i]; i++ )
if ( LOGICS[i] != str[i] ) goto P1;
if ( LOGICS[i]==',' ) return(0);
if ( LOGICS[i-1]==' ' )
{
for ( j = 0; str[j]; j++ )
if ( LOGICS[i+j] != str[j] ) goto P2;
if ( LOGICS[i+j]==',' || LOGICS[i+j]=='.'
|| LOGICS[i+j]==' ' ) return(i);
return(-1);
}
/*********************************************************/
char *copy(s,x) char *s; int x;
/*** Return copy of s from offset x
to (not including) first non-
alphanumeric character. ***/
{ char rtn[80];
int i = 0;
for ( s += x; (*s>='A'&&*s<='Z')||(*s>='0'&&*s<='9'); s++ )
rtn[i++] = *s;
rtn[i] = '\0';
return(rtn);
}
/*********************************************************/
trim() /*** Convert logic_name to upper case and remove
non-alphanumeric characters ***/
{ int i,j = 0;
for ( i = 0; *(theJob->logic_name+i); i++ )
{
if ( islower(*(theJob->logic_name+i)) )
*(theJob->logic_name+i) = toupper(*(theJob->logic_name+i));
if (isupper(*(theJob->logic_name+i))
|| isdigit(*(theJob->logic_name+i)))
theJob->logic_name[j++] = *(theJob->logic_name+i);
}
while ( j < i ) theJob->logic_name[j++] = '\0';
}
/*********************************************************/
settings. ***/
{ char c;
int i,j;
theJob->symbols[0] = "tfTF ";
theJob->symbols[1] = "~ ";
theJob->symbols[2] = "o&v> ";
for ( i = 1; i < AXMAX; i++ ) theJob->axiom[i] = 0;
theJob->tty_out = PRETTY; theJob->fil_out = NONE;
theJob->outfil_name[0] = '\0';
theJob->maxmat = theJob->maxtime = 0;
Sizmax = theJob->sizmax = SZ; theJob->sizmax_ismax = 1;
theJob->f_t = theJob->f_n = theJob->f_lat = theJob->f_fus = 1;
wff_initial();
if ( !noclear ) system("clear");
printf("\n This is MaGIC "); printf(VERSION);
printf(", finding matrices for ");
printf("your favourite logic.\n");
printf(" Matrices come in all sizes up to %dx%d.\n",SZ,SZ);
logic_choice();
}
/**********************************************************/
{ int i,j;
for ( i = 0; i < FMAX; i++ )
{
theJob->form[i].lsub = theJob->form[i].rsub = 0;
if ( i < 8 )
theJob->form[i].sym = ( i < 5? 'p'+i: ( i == 5? 'f':
( i == 6? 'T': 'F' )));
else
theJob->form[i].sym = ( i < 8+CMAX ? ' ' :
( i > 7+(3*CMAX) ? '\0' :
( i < 8+(2*CMAX)? 'a': 'b' )));
}
for ( i = 0; i < CMAX; i++ )
{
theJob->atom[0][i] = 8+CMAX+i;
theJob->atom[1][i] = 8+(2*CMAX)+i;
theJob->defcon[i] = 0;
}
theJob->dcs[0] = '\0';
for ( i = 0; i < TMAX; i++ ) theJob->root[i] = 0;
theJob->failure = 0;
}
/**********************************************************/
and set Sizmax accordingly ***/
{ int i;
for ( i = 0; i < 19; i++ ) if ( theJob->axiom[i] )
{
if ( i == AxX || i == AxBA || i == AxSBA || i == AxRED )
theJob->f_n = 1;
if ( i == AxK || i == AxK2 || i == AxCt )
theJob->f_t = 1;
if ( i == AxX || i == AxBA || i == AxSBA || i == AxW2
|| i == AxWB || i == Axat ) theJob->f_lat = 1;
if ( i == AxK || i == AxK2 || i == AxTF ) theJob->f_T = 1;
}
if ( theJob->f_n && (theJob->logic == RW ||
theJob->logic == R || theJob->logic == CK) )
theJob->f_fus = 1;
for ( i = 0; theJob->root[i]; i++ )
check_frag(theJob->form+theJob->root[i]);
if ( theJob->failure ) check_frag(theJob->form+theJob->failure);
for ( i = 0; theJob->dcs[i]; i++ )
check_frag(theJob->form+theJob->defcon[i]);
if ( theJob->totord ) theJob->f_lat = 1;
if ( theJob->f_lat ) theJob->f_t = theJob->f_T = theJob->f_F = 1;
if (( theJob->f_F || theJob->f_T ) && theJob->f_n )
theJob->f_F = theJob->f_T = 1;
if ( !(theJob->f_lat || theJob->f_n) ) Sizmax = theJob->f_t? 7: 6;
else if ( !theJob->f_lat ) Sizmax = theJob->f_t? 8: 7;
else if ( *(theJob->logic_name) == 'L' )
Sizmax = theJob->f_n? 10: 8;
else if ( !theJob->totord ) Sizmax =
(theJob->f_n && theJob->logic==S4 || theJob->axiom[AxBA])? 16:
(theJob->f_n? 14: 9);
else Sizmax = theJob->f_n? 16: 12;
if ( theJob->sizmax > Sizmax || theJob->sizmax_ismax )
theJob->sizmax = Sizmax;
}
/**********************************************************/
check_frag(s) WFF *s; /*** Attend to connectives
used in (sub)formula ***/
{
if ( !s ) return(0);
switch(s->sym)
{
case '~': theJob->f_n = 1; break;
case 'f': theJob->f_n = 1;
case 't': theJob->f_t = 1; break;
case 'T': theJob->f_T = 1; break;
case 'F': theJob->f_F = 1; break;
case 'o': theJob->f_fus = 1; break;
case '&':
case 'v': theJob->f_lat = 1;
}
check_frag(s->lsub);
check_frag(s->rsub);
}
/**********************************************************/
add_axiom()
{ int i;
put_out( "AX.show" );
printf(" %-5d< User-defined axiom >", AXMAX-1);
printf("\n\n Select one of the above by typing its number: ");
fflush(stdout); scanf("%d", &i); READLN
if (i==AXMAX-1) user_axiom();
else if ( i > 0 && i < AXMAX-1 ) theJob->axiom[i] = 1;
}
/**********************************************************/
user_axiom() /*** Take user definition of a formula
to go in next root[]. ***/
{ int i;
for ( i = 0; theJob->root[i] && i<TMAX; i++ ) ;
if (i == TMAX )
{
printf(
"\n\n Maximum number of user-defined axioms is %d",TMAX);
paws();
return(0);
}
got_formula(0,i,"axiom");
}
/**********************************************************/
bad_guy() /*** Take user definition of a formula
to go in failure. ***/
{
got_formula(1,0,"formula");
}
/*********************************************************/
connective() /*** Take definition of an operator in
response to menu option "c". ***/
{ int i,j;
char c;
for ( i = 0; theJob->defcon[i] && i<CMAX; i++ ) ;
if (i==CMAX)
{
printf("\n\n Maximum number of definitions is %d", CMAX);
paws();
return(0);
}
printf("\n\n Type the new connective: ");
fflush(stdout); scanf("%c", &c); READLN
if ( strchr("&v~->o)(.fpqrstabFT",c) || strchr(theJob->dcs,c) )
{
printf("\n No fair: \"%c\" already means something.",c);
paws(); return(0);
}
else if ( noclear ) printf("\n Accepted !!\n");
printf("\n What is the adicity of %c ", c);
fflush(stdout); scanf("%d", theJob->adicity+i); READLN
if ( theJob->adicity[i]<0 || theJob->adicity[i]>2 )
{
printf("\n No fair: adicity must be 0, 1 or 2.");
paws(); return(0);
}
if ( !theJob->adicity[i] ) printf("\n Define %c ", c);
else if ( theJob->adicity[i] == 1 ) printf("\n Define %ca ", c);
else printf("\n Define a %c b ", c);
fflush(stdout);
theJob->defcon[i] = 0;
if ( got_formula(2,i,"definition") )
{
for ( j = 0; theJob->symbols[theJob->adicity[i]][j] != ' '; j++ ) ;
theJob->symbols[theJob->adicity[i]][j] = c;
if ( !theJob->adicity[i] ) theJob->form[8+i].sym = c;
theJob->dcs[i] = c; theJob->dcs[i+1] = '\0';
}
}
/**********************************************************/
{
int rc;
while (1) switch( infml(x,y) )
{
case -1: return(0);
case 0: return(1);
case 1: printf("\n H)elp, R)epeat %s or N)either? ", s);
switch(readin("hnr"))
{
case 'n': return(0);
case 'h': help(x+1); break;
case 'r': printf("\n Definition: "); fflush(stdout);
}
}
}
/***********************************************************/
{ int i,j;
printf("\n Delete (a) pre-defined axiom?");
printf("\n (b) bad guy?");
printf("\n (c) user-defined axiom? ");
switch( readin("abc") )
{
case 'a': j = 0;
for ( i = 1; i < AXMAX; i++ )
if ( theJob->axiom[i] )
{
if ( j ) j = AXMAX;
else j = i;
}
if ( j )
{
if ( j < AXMAX ) theJob->axiom[j] = 0;
else
{
for ( i = 1; i < AXMAX; i++ )
if ( theJob->axiom[i] )
{
printf("\n %2d ", i);
print_axiom(stdout,i);
}
printf("\n\n Delete which one? "); fflush(stdout);
scanf("%d", &i); READLN
if ( i > 0 && i < AXMAX ) theJob->axiom[i] = 0;
}
}
break;
case 'b': theJob->failure = 0; break;
case 'c': if ( *(theJob->root) )
{
if ( theJob->root[1] )
{
for ( i = 0; theJob->root[i]; i++ )
{
printf("\n %d ", i+1);
outfml(theJob->form+theJob->root[i],
theJob->form+theJob->root[i],stdout);
}
printf("\n\n Delete which one? ");
fflush(stdout); scanf("%d", &j); READLN
}
else i = j = 1;
for ( ; j > 0 && j <= i; j++ )
theJob->root[j-1] = theJob->root[j];
}
}
}
/**************************************/
fragment()
{
if ( noclear)
{
printf("\n\n Select which connectives you want\n\n");
printf(" ~ (y/n) "); theJob->f_n = ( readin("yn") == 'y' );
printf(" & and v (y/n) "); theJob->f_lat = ( readin("yn") == 'y' );
printf(" t (y/n) "); theJob->f_t = ( readin("yn") == 'y' );
printf(" T (y/n) "); theJob->f_T = ( readin("yn") == 'y' );
printf(" F (y/n) "); theJob->f_F = ( readin("yn") == 'y' );
printf(" o (y/n) "); theJob->f_fus = ( readin("yn") == 'y' );
}
else
{
printf("\n\n Do you want negation defined? (y/n) ");
theJob->f_n = ( readin("yn") == 'y' );
printf("\n Do you want & and v defined? (y/n) ");
theJob->f_lat = ( readin("yn") == 'y' );
if ( theJob->f_lat ) theJob->f_t = 1; else
{
printf("\n Do you want constant t defined? (y/n) ");
theJob->f_t = ( readin("yn") == 'y' );
}
if ( theJob->f_lat ) theJob->f_T = theJob->f_F = 1; else
{
printf("\n Do you want constant T defined? (y/n) ");
theJob->f_T = ( readin("yn") == 'y' );
if ( theJob->f_T && theJob->f_n ) theJob->f_F = 1; else
{
printf("\n Do you want constant F defined? (y/n) ");
theJob->f_F = ( readin("yn") == 'y' );
}
}
if ( theJob->f_n && (theJob->logic == RW ||
theJob->logic == R || theJob->logic == CK) )
theJob->f_fus = 1;
else
{
printf("\n Do you want fusion o defined? (y/n) ");
theJob->f_fus = ( readin("yn") == 'y' );
}
}
}
/***********************************************************/
logic_choice()
{ char glc;
theJob->logic = -1; theJob->totord = 0;
printf("\n\n What is your favourite logic? "); fflush(stdout);
gets(theJob->logic_name);
trim();
theJob->logic = strpos(theJob->logic_name, LOGICS);
if ( theJob->logic >= 0 ) return(1);
if ( *(theJob->logic_name)=='L' || *(theJob->logic_name)=='T' )
theJob->logic = strpos(theJob->logic_name+1, LOGICS);
if ( theJob->logic >= 0 )
{
theJob->totord = (*(theJob->logic_name)=='T'); return(1);
}
printf(
"\n\n There is no such logic as \"%s\".\n",theJob->logic_name);
printf("\n Logics are %s\n\n",LOGICS);
printf(
" Prefix \"L\" for no distribution, \"T\" for total order.");
printf("\n\n\n H)elp or R)eselect? ");
if ( readin("hr") == 'h' )
{
help(3); paws();
help(4); paws();
help(5);
}
logic_choice();
}
/**********************************************************/
{ char oc;
printf("\n\n");
do {
printf(
"\n Tty: P)retty U)gly S)ummary N)one H)elp ");
oc = readin("pusnh");
theJob->tty_out = oc=='u'? UGLY: (oc=='p'? PRETTY:
(oc=='s'? SUMMARY: NONE));
if (oc=='h') help(6);
}
while ( oc == 'h' );
do {
printf(
"\n File: P)retty U)gly S)ummary N)one H)elp ");
oc = readin("pusnh");
theJob->fil_out = oc=='u'? UGLY: (oc=='p'? PRETTY:
(oc=='s'? SUMMARY: NONE));
if ( oc == 'h' ) help(6);
}
while ( oc == 'h' );
if (!theJob->fil_out) return(0);
if ( *(theJob->outfil_name) )
{
printf(" New output file? (y/n) ");
if ( readin("yn") == 'n' ) return(0);
}
if ( filing ) { fclose(outfil); filing = 0; }
do {
printf(" \n Name output file: "); fflush(stdout);
gets(theJob->outfil_name);
}
while ( !*(theJob->outfil_name) );
}
/**********************************************************/
{ char oc;
printf("\n Shall I stop when:");
printf(" (a) I'm exhausted?\n");
printf("%20c(b) time's up?\n", ' ');
printf("%20c(c) I've found enough matrices?\n", ' ');
printf("%20c(d) the matrices get too big?\n", ' ');
printf("%20c(e) a combination of the above? ", ' ');
oc = readin("abcde");
theJob->sizmax = Sizmax;
theJob->maxtime = theJob->maxmat = 0;
theJob->sizmax_ismax = 1;
switch( oc )
{
case 'c': printf("\n How many is enough? ");
fflush(stdout); scanf("%d", &(theJob->maxmat));
if ( theJob->maxmat < 0 ) theJob->maxmat = 0; break;
case 'd': printf("\n How big is big enough? ");
fflush(stdout); scanf("%d", &(theJob->sizmax));
if ( theJob->sizmax > 1 ) theJob->sizmax_ismax = 0; break;
case 'e': printf("\n How many matrices are enough? ");
fflush(stdout); scanf("%d", &(theJob->maxmat));
if ( theJob->maxmat < 0 ) theJob->maxmat = 0;
printf("\n How big can they get? ");
fflush(stdout); scanf("%d", &(theJob->sizmax));
if ( theJob->sizmax > 1 ) theJob->sizmax_ismax = 0;
case 'b': printf("\n How many seconds have I got? ");
fflush(stdout); scanf("%d", &(theJob->maxtime));
if ( theJob->maxtime < 5 ) theJob->maxtime = 0; break;
}
}
/***********************************************************/
n_of_procs() /*** In the parallel version, return the new
choice of number of processes. In the
serial version, return -1 (nonsense) ***/
{
char *npcp;
int i;
#ifdef PARALLEL
npcp = strchr(answer,'#');
while ( *npcp && ( *npcp < '0' || *npcp > '9' )) npcp++;
if ( !*npcp ) return(gm->nprocs);
i = 0;
do {
i = i*10 + *npcp - '0';
npcp++;
}
while ( *npcp >= '0' && *npcp <= '9' );
if ( i < 2 || i > PARALLEL )
{
printf("\n Number of processes must be in range 2 - %d\n\n",
PARALLEL);
paws();
return(gm->nprocs);
}
#else
i = -1;
#endif
return(i);
}
/***********************************************************/
{
if ( noclear ) fprintf(f, "%2d ", x);
switch( x )
{
case AxX: fprintf(f, "p v ~p"); break;
case AxBA: fprintf(f, "(p & ~p) -> q"); break;
case AxSBA: fprintf(f, "(p & ~p) -> (q v ~q)"); break;
case AxW2: fprintf(f, "(p & (p -> q)) -> q"); break;
case AxK: fprintf(f, "p -> (q -> p)"); break;
case AxK2: fprintf(f, "p -> (q -> q)"); break;
case AxM: fprintf(f, "p -> (p -> p)"); break;
case AxRED: fprintf(f, "(p -> ~p) -> ~p"); break;
case AxC3: fprintf(f, "(t -> p) -> p"); break;
case AxCt: fprintf(f, "p -> (t -> p)"); break;
case Axat: fprintf(f, "p v (p -> q)"); break;
case AxTF: fprintf(f, "T -> (F -> F)"); break;
case AxB: fprintf(f,
"(q -> r) -> ((p -> q) -> (p -> r))");
break;
case AxB2: fprintf(f,
"(p -> q) -> ((q -> r) -> (p -> r))");
break;
case AxC2: fprintf(f, "p -> ((p -> q) -> q)"); break;
case AxW: fprintf(f,
"(p -> (p -> q)) -> (p -> q)"); break;
case AxC: fprintf(f,
"(p -> (q -> r)) -> (q -> (p -> r))");
break;
case AxWB: fprintf(f,
"((p -> q) & (q -> r)) -> (p -> r)");
}
}
/**********************************************************/
{
if ( !noclear ) system( "clear" );
disp(stdout);
printf(" A)xiom B)adguy C)onnective D)elete\n");
printf(" E)xit F)ragment G)enerate H)elp\n");
printf(" I)O J)ump K)ill L)ogic ");
}
/**********************************************************/
{ int i,j = 0;
#ifdef PARALLEL
fprintf(f, "\n Parallel MaGIC running %d out of %d processes\n",
gm->nprocs, PARALLEL);
#endif
fprintf(f, "\n Logic:%8c%s", ' ', theJob->logic_name);
for ( i = 1; i < AXMAX; i++ ) if ( theJob->axiom[i] )
{
if ( !j )
{
j = 1; fprintf(f, "\n\n Plus: ");
}
else fprintf(f, "\n ");
print_axiom(f,i);
}
for ( i = 0; theJob->root[i]; i++ )
{
if ( i ) fprintf(f, "\n ");
else fprintf(f, "\n\n Extra: ", i+1);
outfml(theJob->form+theJob->root[i],
theJob->form+theJob->root[i],f);
}
fprintf(f, "\n\n Fragment: ->");
if ( theJob->f_lat ) fprintf(f, ", &, v");
if ( theJob->f_n ) fprintf(f, ", ~");
if ( theJob->f_fus ) fprintf(f, ", o");
if ( theJob->f_t )
{
fprintf(f, ", t");
if ( theJob->f_n ) fprintf(f, ", f");
}
if ( theJob->f_T ) fprintf(f, ", T");
if ( theJob->f_F ) fprintf(f, ", F");
for ( i = 0; theJob->defcon[i]; i++ )
{
if ( i ) fprintf(f, "\n ");
else fprintf(f, "\n\n Definitions:");
if ( !theJob->adicity[i] )
fprintf(f, " %c ", theJob->dcs[i]);
else if ( theJob->adicity[i]==1 )
fprintf(f, " %ca ", theJob->dcs[i]);
else fprintf(f, " a %c b ", theJob->dcs[i]);
outfml(theJob->form+theJob->defcon[i],
theJob->form+theJob->defcon[i],f);
}
if ( theJob->failure )
{
fprintf(f, "\n\n Fail: ");
outfml(theJob->form+theJob->failure,
theJob->form+theJob->failure, f);
}
fprintf(f, "\n\n TTY output: %s\n File output: %s",
(theJob->tty_out==NONE? "none":
(theJob->tty_out==UGLY? "ugly":
(theJob->tty_out==PRETTY? "pretty": "summary"))),
(theJob->fil_out==NONE? "none":
(theJob->fil_out==UGLY? "ugly":
(theJob->fil_out==PRETTY? "pretty": "summary"))));
if ( theJob->fil_out )
fprintf(f,"\n Output file: \"%s\"", theJob->outfil_name);
fprintf(f, "\n\n Search concludes ");
if (theJob->maxtime) fprintf(f, "after %d second%s\n or ",
theJob->maxtime, (theJob->maxtime==1? "": "s"));
if (theJob->maxmat) fprintf(f, "when %d matri%s found\n or ",
theJob->maxmat, (theJob->maxmat==1? "x": "ces"));
fprintf(f, "when size %d finished.\n\n\n", theJob->sizmax);
}
/**********************************************************/
{
switch( x )
{
case 0: put_out("MEN.show"); break;
case 1:
case 2: put_out("WFF.show"); break;
case 3: put_out("FDL.show"); break;
case 4: put_out("BTW.show"); break;
case 5: put_out("LOG.show"); break;
case 6: put_out("OUT.show");
}
}
/***********************************************************/
{
char s[50], *t;
int i,j=0;
if ( noclear ) return(0);
system( "clear" );
t = "more ";
for ( i = 0; t[i]; i++ ) s[j++] = t[i];
t = DATA_DIR;
for ( i = 0; t[i]; i++ ) s[j++] = t[i];
while ( s[j++] = *f_nm++ ) ;
system( s );
}
/***********************************************************/
nfml(x,y) int x,y; /*** Input a formula from stdin.
x is the destination: 0=axiom,
1=badguy 2=definition. y is
the offset for x==0 or x==2.
Return 0 iff successful ***/
{ int i, j;
WFF *wf;
char fml[80];
if ( x != 2 ) printf("\n\n Enter formula (or RETURN): ");
fflush(stdout);
gets(answer);
j = 0;
for ( i = 0; answer[i]; i++ )
if ( strchr(")(.~&vo>ftFT", answer[i])
|| strchr(theJob->dcs, answer[i])
|| ( strchr("pqrst", answer[i]) && x < 2 )
|| ( answer[i] == 'a' && x == 2 && theJob->adicity[y] )
|| ( answer[i] == 'b' && x == 2 && theJob->adicity[y] == 2 ))
fml[j++] = answer[i];
else if ( !strchr(" -", answer[i]) )
{
printf(
"\n Illegal input: unrecognised symbol %c\n\n ", answer[i]);
for ( j = 0; j < i; j++ ) printf(" "); printf("!\n ");
printf(answer); printf("\n\n");
return( 1 );
}
for ( i = j; fml[i]; i++ ) fml[i] = '\0';
if ( !j ) return(-1);
if ( x == 2 )
{
if ( j == 1 )
{
printf("\n ERROR: definition is too short!\n\n");
return(1);
}
if ( theJob->adicity[y] && !strchr(fml,'a') )
{
printf("\n ERROR: variable \"a\" does not occurin the definition\n\n");
return(1);
}
if ( theJob->adicity[y] == 2 && !strchr(fml,'b') )
{
printf("\n ERROR: variable \"b\" does not occur in the definition\n\n");
return(1);
}
}
wf = parse(fml,theJob->form,theJob->symbols);
if ( !wf ) return(1);
if ( !x ) theJob->root[y] = wf-theJob->form;
else if ( x == 1 ) theJob->failure = wf-theJob->form;
else {
fix_atoms(y,wf);
theJob->defcon[y] = wf-theJob->form;
}
return(0);
}
/**********************************************************/
fix_atoms(y,dy) int y; WFF *dy; /*** Change occurrences of
'a' and 'b' in the definition
of defined connective #y to
its own atom[0] and atom[1] ***/
{
if ( !dy ) return(0);
if ( dy->lsub )
{
if ( dy->lsub->sym == 'a' )
dy->lsub = theJob->form+theJob->atom[0][y];
else if ( dy->lsub->sym == 'b' )
dy->lsub = theJob->form+theJob->atom[1][y];
else fix_atoms(y,dy->lsub);
}
if ( dy->rsub )
{
if ( dy->rsub->sym == 'a' )
dy->rsub = theJob->form+theJob->atom[0][y];
else if ( dy->rsub->sym == 'b' )
dy->rsub = theJob->form+theJob->atom[1][y];
else fix_atoms(y,dy->rsub);
}
}
/*******************************************************/
outfml(p,q,f) WFF *p, *q; FILE *f;
/*** Print subformula rooted at p to f
Note q is the root of a formula ***/
{ int i,j,k;
char c;
c = p->sym; k = -1;
for ( j = 0; theJob->dcs[j]; j++ )
if ( c == theJob->dcs[j] )
{
k = theJob->adicity[j]; break;
}
if ( c == '&' || c=='v' || c=='>' || c=='o' || k==2 )
{
if ( p != q ) fprintf( f, "(" );
outfml(p->lsub,q,f); fprintf( f, " " );
if ( c == '>' ) fprintf( f, "-" );
fprintf( f, "%c ", c );
outfml(p->rsub,q,f);
if ( p != q ) fprintf( f, ")" );
}
else
{
fprintf( f, "%c", c );
if ( c == '~' || k == 1 )
outfml(p->rsub,q,f);
}
}
.
