Import of code from J Slaney web-page.

url: http://users.cecs.anu.edu.au/~jks/software/magic.2.2.1.tar.gz
This commit is contained in:
arran 2017-10-20 22:21:43 +08:00
commit e2efc4b8cd
57 changed files with 12700 additions and 0 deletions

47
README Normal file
View File

@ -0,0 +1,47 @@
MaGIC (Matrix Generator for Implication Connectives) is a tool that
produces small algebraic models of non-classical propositional logics,
especially of the substructural sort. The logics are considered as
Hilbert (axiom) systems. Interaction with MaGIC is through a plain
text "terminal" window and is based on a menu. Help is available from
the menu.
Synopsis:
magic [-b <filename>] [-t] [-x]
Options:
-b <filename> runs the program in batch mode with the specified file
as input. The file should be one previously saved with the "Save"
option from a previous run of MaGIC. This allows output to be piped
through another program such as one of the utilities provided with
MaGIC.
-t produces "terse" output, mainly meaning that it suppresses system
calls such as those that clear the window each time the menu is
printed.
-x causes the dialogue to be in a form suitable for "xmagic", the (now
defunct) X Windows interface to MaGIC. It is the result of a
message from Gustav Meglicki to John Slaney to the effect that the
machine-readable I/O was "insufficiently user-hostile". Since
xmagic is no longer supported, this option is a mere relic.
Installation:
The main directory containing this README should have two
subdirectories, one containing the program sources and the other
containing various data files used by MaGIC. To make, go to the src
directory and edit the Makefile. Only the top few lines require any
change - mainly it is a matter of filling in the directories where
the data files and the binaries are to be kept. Then "make" should
make the programs and "make install" should simply move them and the
data into the specified directories.As usual, "make clean" removes
the .o files and possibly other junk.
Problems in installing or using MaGIC should be reported to the author
John.Slaney@anu.edu.au
It is also recommended that if you install MaGIC you let us know, so
that we can inform you of any bug fixes or updates.

19
dat/BTW.show Normal file
View File

@ -0,0 +1,19 @@
B Axioms 1 - 8 as for FD.
9. ((A -> B) & (A -> C)) -> (A -> (B & C))
10. ((A -> C) & (B -> C)) -> ((A v B) -> C)
Rules 1 - 2, 8 - 12 as for FD.
Rules 6 and 7 replaced by the above axioms.
Rules 3 - 5 replaced by:
4'. A -> B ==> (C -> A) -> (C -> B)
5'. A -> B ==> (B -> C) -> (A -> C)
DW is B with rule 8 replaced by the axiom form:
Axiom 11. (A -> ~B) -> (B -> ~A)
TW is DW with rules 4' and 5' replaced by the axiom forms:
Axiom 12. (A -> B) -> ((C -> A) -> (C -> B))
13. (A -> B) -> ((B -> C) -> (A -> C))

15
dat/CUT.show Normal file
View File

@ -0,0 +1,15 @@
A user-defined connective may optionally be marked with a "cut".
This serves to control backtracking much as in Prolog. MaGIC will
not generate two models whose most significant difference is in
a connective with a cut.
Thus for example, where `A' is a primitive 0-adic connective and
a rule
A v ~A /
has been added, MaGIC will normally generate failures of the law
of the excluded middle. However, if `A' has been marked with a cut
then MaGIC will generate models in which that law fails: if it
fails for more than one element of a model, only the smallest such
element will be reported.

21
dat/FDL.show Normal file
View File

@ -0,0 +1,21 @@
FD Axioms: 1. A -> A
2. (A & B) -> A
3. (A & B) -> B
4. A -> (A v B)
5. B -> (A v B)
6. ~~A -> A
7. F -> A
8. A -> T
Rules: 1. A -> B, A ==> B
2. A, B ==> A & B
3. A -> B, B -> C ==> A -> C
4. A -> B, B -> A ==> (C -> A) -> (C -> B)
5. A -> B, B -> A ==> (B -> C) -> (A -> C)
6. A -> B, A -> C ==> A -> (B & C)
7. A -> C, B -> C ==> (A v B) -> C
8. A -> ~B ==> B -> ~A
9. A ==> t -> A
10. t -> A ==> A
11. A -> (B -> C) ==> (A o B) -> C
12. (A o B) -> C ==> A -> (B -> C)

21
dat/LOG.show Normal file
View File

@ -0,0 +1,21 @@
Axioms for the stronger logics are as follows:
EW is TW plus ((A -> A) -> B) -> B
C is TW plus A -> ((A -> B) -> B)
T is TW plus (A -> (A -> B)) -> (A -> B)
and (A -> ~A) -> ~A
E is T plus ((A -> A) -> B) -> B
R is C plus (A -> (A -> B)) -> (A -> B)
CK is C plus A -> (B -> A)
S4 is E plus A -> (B -> B)
Axiomatisations of fragments of these logics result by
selecting the axioms and rules which explicitly mention
the appropriate connectives.

41
dat/MEN.show Normal file
View File

@ -0,0 +1,41 @@
Menu options:
a: Add a pre- or user-defined axiom or rule to the logic.
b: Specify a formula to fail in the matrices found.
c: Define a connective. E.g. + defined ~a -> b.
d: Delete either an axiom, a user-defined connective or the bad guy.
e: Exit from MAGIC.
f: Choose the fragment (pre-defined connectives).
g: Search for matrices.
h: Display this page.
i: Change the output formats.
j: Set a condition on which to jump out of the search.
k: Re-initialise everything.
l: Change your mind about your favourite logic.
m: Display information about MaGIC (version number etc).
n: Change number of processes (parallel version only).
o: Re-order dyadic connectives for scope or significance purposes.
p: Select which tables to print when matrices are found.
q: Quit MaGIC (equivalent to e).
r: Read a job specification from a named file.
s: Write the current job specification to a named file.

22
dat/OUT.show Normal file
View File

@ -0,0 +1,22 @@
Output formats are as follows:
"Pretty": Matrices are printed in human-readable form.
This is the default for tty output. Each
matrix is followed by an assignment of values
falsifying the "bad guy" if there is one.
"Ugly": Matrices are printed in a standard machine-
readable form with -1 as break character.
No headings, comments, etc. are included.
"Summary": Only the numbers of matrices are printed.
This is useful for checking the size of a
job before getting a printout of matrices.
It runs slightly faster than "pretty" or
"ugly".
"None": No matrices are printed, although the final
statistics are still sent to the tty. This
is the default for file output.

22
dat/WFF.show Normal file
View File

@ -0,0 +1,22 @@
The following conventions govern typing of formulas.
(a) Variables are any (upper or lower case) letters other
than those (such as 'o' and 'v') used as connectives.
't', 'f', 'T' and 'F' are sentential constants.
(b) Parentheses are as normal, with the features that
connectives of smaller scope bind more tightly than
those of larger scope, and that except as scope and
parentheses dictate, association is to the left.
Unary connectives have minimal scope. The binary ones
in order of increasing scope are o & v -> followed
by user-defined ones. The scope order may be changed.
A period may replace a left parenthesis whose right
mate is as far to the right as is reasonable.
(c) Spaces are ignored. RETURN terminates the formula.

BIN
dat/ba.16 Normal file

Binary file not shown.

BIN
dat/dl.10 Normal file

Binary file not shown.

BIN
dat/dln.14 Normal file

Binary file not shown.

1
dat/l.8 Normal file
View File

@ -0,0 +1 @@
/¿“ïý{Žütúv<C3BA>Æ¡ï×qèß}úŸÇ!¤A¿ÒÕd4è׺ ý\—£A¿Óõd4è÷ºž<EFBFBD>†ƒ~çëÉx8èg¿úݯ§ãá ßÿz<ô?ÝOý_÷³ÑpÐÿw? úßï§ÃAÿÿý|<ä"]è/®LŒ ô—IWF†úÓ¤K#ƒý-Òµ‰<E280B0>þ6éÚÌÈÐà@Ëtmrdp ¿Åº6164Пj]èoµ®M<C2AE> ôÇZ§†úÛ­kcCƒýñÖŹ±¡Á<C2A1>þzéêÈÐ@®uyjhp ?ߺ<7648Пs]žèï®OŒ ô÷I×gF†ú{¬ëcCƒý½Öõ©±¡Á<C2A1>þ~ëúÜØÐà@Ïu}rlhp ¿Ç»>1>4Ðßë]Ÿèïÿ®<C3BF> ôÇìúkö«“£ƒýuûÕÑáÁ<C3A1>þ¼ýòèà@<>~}btp ¿g¿>9:8Ðß·_Ÿèïñ¯OŒô÷ü×'LJúsÿËÃý½ÿõéñáÁ<C3A1>þþÿúøðà@ÿ<>tb ÿOº?324Ðÿ/ÝŸèÿµîO ôÿ[÷çƆú®û“Cý¿×ý鱡Á<C2A1>þÿéþüÈ@ÿÿu~lhp ÿÿ»??>4Ðÿ³ßŸèÿÛïÏŽôÿï÷çGúÿûÓÃýÿÿýùñáÁ<C3A1>üúF è_ŒHWŒ2 2"]2bЀþMˆtÍ„ú7#Ò53F 4 “"]3iÄ <C384>ú7aÒ5Æ Ð?)“.2h@ÿ¦Lºfʘô<>ʤ¦ 4p@ÿæLºfÌ<66>AúGgÒEsÆ 4p@ÿ0MºpÈ€þÕ‰tÕˆ!ôÏʤ˦ 4p@ÿìLºlΘ蟥I—M2p@ÿ,Nºlâ˜èß…H×M1 7"]7cÄ<63><C384>úw1ÒuG п “®0fÈ ý»2éº)c† 8 w&]7gÌ<67>AôïÒ¤ë&<26>2hà€þ]œtÝÄ1C Ð?.1 7#]7sÄ<73><C384>úg1Óe Ð?›™.9rÈÀý»péº ã† èß•K×M7dÐÀý»wéºqCè¾KÎ7dà€þQªuÑ <C391>úW©ÖU“F 8 ˜j]8iÐÀý«UëªQà Ð?[µ.5hà€þáªuá¬Qà Ð?Œµ.4 j]7aÔ ý»TëºI£ п[µ®5jØ <C398>úw±ÖuG 8 n]7aÜ°AúwéÖu“Æ 4p@ÿ¬ÝºlØ <C398>úwíÖuÓÆ 4p@ÿ°ÝºpÚ°AôïÞ­ëÆ 4p@ÿðݺpÞ¸èÆ[Ž6hà€þåŠuå¬Ã п|±®œ7bØ <C398>ú—-ו# 蟶I—Ž2h@ÿôMºtÞ˜èß¾I׎2h@ÿô]ºtÞ¸è§ZO4p@ÿxÕºxÖ¨aƒèÇZO5hà€þñ«uñ¼Qƒè·[O6hà€þñ»uñ¼qà Ð?Ž·.ž8nØ <C398>ú×#ÖÕ3F пN±®ž4bЀþu´Ã è_§ZWO5hà€þõªuõ¬Qà пnµ®ž6jØ <C398>ú×±ÖÕG 4p@ÿúÕºzÞ¨aƒè_§\WO9hà€þuËuõ´Ã пž¹®ž9rØ <C398>ú÷!ÒõF èß<C3A8>H×Ï1d@ÿ>Lº~˜!ƒôïˤ만2h@ÿþLº~Θ!ƒôïÓ¤ë'<27>2hà€þ}¸tý„qCèß—K×O7dÐÀýûwéúyㆠп<C390>—®Ÿ8nÈÀýóvëòià Ð?·.Ÿ7nØ <C398>ú÷¡ÖõF 8 Ÿj]?iÔ <C394>ú÷«Öõ³F 4p@ÿ>Öº~â¨Aôïíë'Œ6hà€þ}ºuý¤qà пo·®Ÿ6nØ <C398>ú÷ïÖõóÆ 4p@ÿ>Þº~â¸è߇\×O9h@ÿ>åº~ÒÈaƒèß·\×O9lÐÀýãzéâ!úש×Õ“F8 Ýz]=mô°Aô¯c¯«'Ž4 ½{]=zØ <C398>ú÷¡×õF4p@ÿ>õº~Òèaƒèß·^×O=lÐÀýûØëú‰£‡ 8 ¿{]?{ô°Aôïçë'Œ2 _>]?eü<65>Aú÷ÿÓõ㇠è߇_×O?lÐÀýûôëúI㇠8 ß~]?mü°Aôïã¯ë'Ž6hà€þýÿuýøaƒè߇×O?|Ѐþ}úwý¤ñà Ð?ïÿ.>h@ÿ¾ÿ»~úøáƒôïÿ¿ëÇ4 ³_8p@ÿ2f¿râÈ<C3A2>ú—3û•#‡Ð?<3F>Ù/9xà€þmÌ~íÄ‘ôogökgŽ:xà€þmÎ~í䑃èßÆí×N;tà€þiÝ~éÐÁôoëök§Ž:xà€þqÝ~ñÔ¡ƒèßÞí׎:xà€þñÝ~ñܱCп¾Ù¯9tà€þyÝ~ùÔ¡ƒèŸßí—Ï;tðÀýó¼ýòÉCè߇ì×O9p@ÿ>f¿~âÈ<C3A2>ú÷3ûõ3G8 ¶_?aìÐÁôïãöë'Ž:xà€þ}Ý~ýÔ±Cп¿Û¯Ÿ;vèà<C3A8>ú÷yûõ“Ç<p@ÿ>|¿~Âø¡ôïã÷ë'Ž:p@ÿ¾~¿~êø¡ƒèßÿï×<C3AF>:p@ÿ8÷¿xðÀýëÜÿêÉ£пÞý¯=|ðÀýóÝÿòуè߇þ×O=xà€þ}ìýÄуèßçþ×O=xà€þýîýìÑÃпÿ¯Ÿ0~øà<C3B8>ú÷ñÿõÇ<p@ÿ>ÿ¿~òøáƒèŸ÷ÿ—<p@ÿ¾ÿ¿~úøáƒèßÿÿ×<C3BF>>xà€þˆtÿ„ýÿéþ#† èÿŸH÷Ï1h@ÿ¿LºÊ<7F>AúÿgÒýsÆ 4 ÿŸ&Ý?iÈÀýÿ6éþic† 8 ÿÿ"Ý?oÄÀýÿ7éþyc† 8 ÿß2Ý?mä<6D><C3A4>úÿïÒýóÆ 8 ÿŸjÝ?iÐÀýÿUëþY£† 8 ÿkÝ?qÔ <C394>úÿ¯ÖýóF 8 ÿßnÝ?mØ <C398>úÿïÖýóÆ 4p@ÿ?Þºâ¸èÿ×K÷O2h@ÿ?׺ò¨Aôÿó­û'<27>6hà€þÿŽuÿìà èÿïZ÷Ï5lÐÀýÿœëþÉ# èÿïÏ9lÐÀýÿéþù#ôÿÿ¤ûç<C3BB>2h@ÿÿ_ºþ¸!ôÿû­û§<C3BB>6hà€þÿ¯uÿüQƒèÿÿ[÷Ï7lÐÀýÿŸëþù# èÿï^÷Ï=lÐÀýÿßëþù£‡ 8 ÿÿ?Ý?ü<7F>ýÿÿëþù㇠8 ÿßÿÝ?}ø ýÿÿïþùã‡Ðÿ<C390>ÙïŸ8p@ÿf¿æÈ¡ôÿoöûçŽ<p@ÿ¿n¿êÐÁôÿïöûçŽ:xà€þÞ~ÿä¡ôÿûöû§<C3BB>:xà€þÿÏ~ÿü‘ôÿÿöûç<C3BB>:xà€þÿÿ~ÿüñCèÿçþ÷O<p@ÿ÷¿öèáƒèÿÿþ÷Ï=xà€þÿÿôáƒèÿÿÿ÷Ï?|ðÀ

BIN
dat/ln.10 Normal file

Binary file not shown.

BIN
dat/po.6 Normal file

Binary file not shown.

BIN
dat/pon.7 Normal file

Binary file not shown.

BIN
dat/pont.8 Normal file

Binary file not shown.

BIN
dat/pot.8 Normal file

Binary file not shown.

BIN
dat/tn.16 Normal file

Binary file not shown.

BIN
dat/to.16 Normal file

Binary file not shown.

142
src/MaGIC.c Normal file
View File

@ -0,0 +1,142 @@
/* MaGIC1.c V2.1
*
* This is the serial version of MaGIC intended eventually to be
* compatible with xmagic version 2.1. It requires such
* structures as JOB to be defined in MAGIC.h.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#define TOPFILE
#include "MaGIC.h"
static boolean interrupted;
int main(argc,argv)
int argc;
char *argv[];
{
int i, option;
boolean batch;
char batchfile[80];
extern char *optarg;
void timesup(), intrupt();
int getopt();
noclear = false;
batch = false;
filing = false;
xdialog = false;
while ((option = getopt (argc, argv, "b:tx#:")) != -1)
switch( option ) {
case 'x':
xdialog = true;
case 't':
noclear = true;
break;
case 'b':
batch = true;
i = 0;
while ((batchfile[i] = optarg[i])) i++;
}
theJob = (JOB*) malloc(sizeof(JOB));
signal( SIGALRM, timesup );
interrupted = false;
signal( SIGINT, intrupt );
strings_initial();
tests_initial();
logics_initial();
job_defaults( batch );
perm_initial();
while ((i = dialog(batch,batchfile)))
if ( i > 0 ) {
if ( !batch ) {
printf("\n Searching.....\n");
fflush(stdout);
}
job_start();
subf_set();
interrupted = false;
alarm(theJob->maxtime);
if ( newsiz() )
do if ( pre_set() ) {
setperm();
transref(&(tr_par));
}
while ( newdes() );
job_stop(batch);
alarm(0);
if ( batch ) exit(0);
}
if ( !noclear ) {
#ifdef __CYGWIN__
puts( "\033[2J" );
#else
system("clear");
#endif
}
return 0;
}
/*
* Action on signal from alarm.
*/
void timesup()
{
tr_par.done = true;
}
/*
* Action on signal from ^C or whatever SIGINT may be.
*/
void intrupt()
{
tr_par.done = true;
if ( interrupted++ ) exit(3);
}

61
src/MaGIC.h Normal file
View File

@ -0,0 +1,61 @@
/*
* MaGIC.h May 1993
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include <ctype.h>
#include <signal.h>
#include <unistd.h>
#ifdef SYSTEMV
#include <sys/systm.h>
#endif
#include "vntr.h"
#include "Mdef.h"
#include "axioms.h"
#include "Mtypes.h"
#include "Mglob.h"
#include "Mproto.h"
/*
* We need more timing apparatus if times.h is available.
*/
#ifdef HASTIMES
#include <sys/times.h>
#include <limits.h>
struct tms time_buffer;
#endif

98
src/Makefile Normal file
View File

@ -0,0 +1,98 @@
# Edit the first few lines of this file to suit your setup.
# You *must* set MAGLIB to the appropriate data directory.
# Where the data files live (must be readable to the MaGIC user)
MAGLIB = /FullPathnameOfMyDataDirectory !!! EDIT !!!
# Where the binaries live
BIN = /FullPathnameOfMyBin !!! EDIT !!!
# Set the optimization level to O3 (includes inlining of functions) for
# performance, or g for debugging.
OPTIMIZATION = -O3
# OPTIMIZATION = -g -Wall
#
# Uncomment WARNINGS to see warning messages during compilation.
# WARNINGS = -w
# If you have times.h (NB _not_ time.h) on your system leave the next
# item alone. If you don't, comment it out.
HASTIMES = -DHASTIMES
##########################################################################
# If you have no gcc or if you wish to compile MaGIC with another #
# compiler, change the next line to suit yourself. #
##########################################################################
CC = gcc
##########################################################################
# You should not have to change the stuff below #
##########################################################################
CFLAGS = $(OPTIMIZATION) $(HASTIMES) $(WARNINGS) -DDATA_DIR=\"$(MAGLIB)/\"
MOBJECTS = MaGIC.o axioms.o dialog.o getjob.o wffs.o mp_parse.o isom.o logic_set.o logic_test.o logic_pretest.o setup.o logic_io.o axiom_tests.o
RMOBJECTS = RM.o RM_input.o RM_output.o
UTES = u2p u2pic onegen one_plus_t_gen u2tex sub_irr
MORPHS = image embedded homomorphic nt_homomorphic
POSTPROCS = $(UTES) $(MORPHS)
UTOBJECTS = u2p.o u2pic.o onegen.o one_plus_t_gen.o u2tex.o sub_irr.o
MORPHOBJECTS = image.o embedded.o homomorphic.o nt_homomorphic.o hmi.o
all: magic utilities
magic: $(MOBJECTS) vntr.o
$(CC) -o magic $(MOBJECTS) vntr.o $(LOCLIB)
utilities: $(POSTPROCS)
u2p: u2p.o $(RMOBJECTS)
$(CC) -o u2p u2p.o $(RMOBJECTS)
u2pic: u2pic.o $(RMOBJECTS)
$(CC) -o u2pic u2pic.o $(RMOBJECTS)
onegen: onegen.o $(RMOBJECTS)
$(CC) -o onegen onegen.o $(RMOBJECTS)
one_plus_t_gen: one_plus_t_gen.o $(RMOBJECTS)
$(CC) -o one_plus_t_gen one_plus_t_gen.o $(RMOBJECTS)
u2tex: u2tex.o $(RMOBJECTS)
$(CC) -o u2tex u2tex.o $(RMOBJECTS)
sub_irr: sub_irr.o $(RMOBJECTS)
$(CC) -o sub_irr sub_irr.o $(RMOBJECTS)
image: image.o hmi.o $(RMOBJECTS)
$(CC) -o image image.o hmi.o $(RMOBJECTS)
embedded: embedded.o hmi.o $(RMOBJECTS)
$(CC) -o embedded embedded.o hmi.o $(RMOBJECTS)
homomorphic: homomorphic.o hmi.o $(RMOBJECTS)
$(CC) -o homomorphic homomorphic.o hmi.o $(RMOBJECTS)
nt_homomorphic: nt_homomorphic.o hmi.o $(RMOBJECTS)
$(CC) -o nt_homomorphic nt_homomorphic.o hmi.o $(RMOBJECTS)
install: all
mkdir -p $(BIN)
mv magic $(POSTPROCS) $(BIN)
mkdir -p $(MAGLIB)
cp ../dat/*.* $(MAGLIB)
clean:
rm -f *.o core $(POSTPROCS) magic
$(MOBJECTS): MaGIC.h vntr.h Mproto.h Mdef.h Mglob.h Mtypes.h axioms.h
vntr.o: vntr.h
$(RMOBJECTS) $(UTOBJECTS) $(MORPHOBJECTS): RM.h
$(MORPHOBJECTS): hmi.h

139
src/Mdef.h Normal file
View File

@ -0,0 +1,139 @@
/*
* Mdef.h
*
* This is part of the header for MaGIC. It contains the definitions
* of symbolic constants.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#define VERSION "2.1"
#define RELEASE_DATE "May 1993"
/*
* We need to distinguish between the main file where global
* variables are mostly defined and the other files where they are
* just declared.
*/
#ifdef TOPFILE
#define GLOBAL
#else
#define GLOBAL extern
#endif
/*
* The input data files are all in a directory:
*/
#ifndef DATA_DIR
#define DATA_DIR "/usr/local/lib/MaGIC/"
#endif
/*
* The clock returns times in 1/TICK sec.:
*/
#define TICK 100
/*
* Next the bounds for various arrays. These are the maxima for
* meaningful symbols (SYMBOLMAX), user-defined connectives (CMAX),
* (sub)formulae (FMAX), testable rules (TMAX) and isomorphs
* per process (ISOMAX). VMAX is the maximum number of variables
* for formulae. RTMAX is the maximum number of premises (or
* conclusions) in a rule.
*/
#define SYMBOLMAX 256
#define CMAX 32
#define FMAX 1024
#define TMAX 64
#define ISOMAX 8192
#define SH_VL 128
#define VMAX 22
#define RTMAX 8
#define ISLMAX (ISOMAX * SH_VL)
#define SLEN 80
/*
* And a dummy formula offset for primitives.
*/
#define PRIMITIVE -1
/*
* And the maximum sizes for the various fragments
*/
#ifdef SMALLDISK
#define S_pot 7
#else
#define S_pot 8
#endif
#define S_pO 6
#define S_pont 8
#define S_poN 7
#define S_ln 10
#define S_lat 8
#define S_ba 16
#define S_dln 14
#define S_dlat 10
#define S_Ton 16
#define S_to 16
/*
* The null premise and null conclusion are negative integers
*/
#define TRIVIAL -1
#define ABSURD -2
/*
* These constructs are useful abbreviations
*/
#define FORALL(x) for (x=0; x<=siz; x++)
#define FORaLL(x) for (x=siz; x>=0; x--)
#define READLN { fflush(stdout); while (getchar() != '\n') ; }
#define IFF(x,y) ((x && y) || (!x && !y))
#define REMOVE(x,y) y &= ~((unsigned)1 << x)
#define ADDTO(x,y) y |= ((unsigned)1 << x)
#define IN(x,y) ((y & (1 << x)) != 0)
#define SINGLETON(x) (!(x & (x-1)))
#define EP { if ( xdialog ) { printf("E\n"); fflush(stdout); }}
#define outfml(p,q,f) outformula(p,q,f,VARS);
#define symbol_listed(x,s) (symbol_position(x,s) >= 0)

131
src/Mglob.h Normal file
View File

@ -0,0 +1,131 @@
/*
* Mglob.h
*
* This file contains the declarations of global variables for
* MaGIC. Note that TR.h contains its own globals.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
GLOBAL JOB *theJob; /* Run specification */
GLOBAL TRIN tr_par; /* vntr job specification */
GLOBAL FILE
*outfil,
*fopen();
GLOBAL int
nulladic[CMAX], /* Defined sential constants */
monadic[CMAX][SZ], /* Defined connectives */
dyadic[CMAX][SZ][SZ], /* Ditto */
vu[VMAX],
rvu[VMAX], /* Variables used in wffs */
badvalue[VMAX], /* Refuting assignment */
kost[TMAX], /* Matrix lookups for axioms */
siz, /* Highest value */
infil, /* File descriptor for input */
input_bit, /* Offset of next bit in input */
start_time, /* Clock reading */
stop_time, /* Clock reading */
tot, /* Total matrices tested */
isoms, isoms2, /* Isomorphs omitted */
begin_timer,
end_timer, /* For timing of serial version */
Sizmax, /* Local version of sizmax */
Vmax, /* Local version of VMAX */
zero; /* Dummy integer */
GLOBAL boolean
xdialog, /* Running from xmagic */
noclear, /* No system calls */
filing, /* Output file open */
default_fragment[LOGMAX][PCMAX]; /* Connectives */
GLOBAL char
buffa, /* 8 bits of input data */
answer[SLEN], /* For input of axioms etc */
thisvector[V_LENGTH], /* Current matrix stretched out */
thatvector[V_LENGTH], /* Last good matrix ditto */
isolist[ISLMAX]; /* Blanks for isomorphisms */
GLOBAL WFF
*tx; /* Last active subformula */
GLOBAL ISM istak[ISOMAX]; /* Spare records for morphisms */
GLOBAL PRM *perm; /* List of permutations */
GLOBAL int
C[SZ][SZ], /* The implication matrix */
ord[SZ][SZ], /* The partial order table */
K[SZ][SZ], /* The conjunction matrix */
A[SZ][SZ], /* The disjunction matrix */
fus[SZ][SZ], /* The fusion matrix */
N[SZ], /* The negation matrix */
box[SZ], /* The necessity matrix */
diamond[SZ], /* The possibility matrix */
desig[SZ], /* Designated values */
maximal[SZ], /* Maximal guys under ord */
atom[2][CMAX], /* 'a' and 'b' for definitions */
impindex[SZ][SZ], /* Info cell for C[x][y] */
boxindex[SZ], /* Info cell for box[x] */
ucc0[CMAX], /* Info cell for nulladic[x] */
ucc1[CMAX][SZ], /* Info cell for monadic[x][y] */
ucc2[CMAX][SZ][SZ]; /* And dyadic[x][y][z] */
GLOBAL int
good, /* Matrices accepted */
negno, /* Negation #, this size */
ordno, /* Order #, this negation */
desno, /* Des #, this order */
matno, /* Matrix #, this des */
boxno, /* Box #, this matrix */
matplus[CMAX], /* Matno for user's connectives */
matsum, /* Matrices this des choice */
des, /* Least designated value */
undes, /* Greatest undesignated value */
firstchange, /* First cell changed this test */
firstarrow, /* First cell of -> matrix */
firstbox, /* First cell of ! matrix */
got_a_fail, /* Badguy fails in matrix */
F_N, /* f_n and contraposition */
afx; /* Affixing is in force */
GLOBAL unsigned
greater_than[SZ], /* {y: ord[x][y]} */
Greater_than[SZ], /* {y: ord[x][y],x!=y} */
less_than[SZ], /* {y: ord[y][x]} */
Less_than[SZ]; /* less_than[x] \ x */
GLOBAL L_DEFAULT
default_orders[LOGMAX]; /* Defaults for logics */

301
src/Mproto.h Normal file
View File

@ -0,0 +1,301 @@
/*
* Mproto.h (included in MaGIC.h)
*
* This file contains the function prototypes for MaGIC. Note that
* the prototypes for vntr.c are in the file vntr.h (also included
* in MaGIC.h).
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
/*
* In file MaCIC.c
*/
int main();
void timesup();
void intrupt();
/*
* In file axioms.c
*/
void strings_initial();
void tests_initial();
void logics_initial();
void init_B();
void init_DW();
void init_TW();
void init_EW();
void init_RW();
void init_LIN();
void init_CK();
void init_T();
void init_E();
void init_R();
void init_S4();
/*
* In file axiom_tests.c
*/
boolean Exmid();
boolean Boolalg();
boolean SemiBool();
boolean paradox();
boolean f_arrow_t();
void E_assertion(unsigned info[]);
void contraction(unsigned info[]);
void Wstar(unsigned info[]);
void Reductio(unsigned info[]);
void assertion(unsigned info[]);
void ata(unsigned info[]);
void TaT(unsigned info[]);
void mingle(unsigned info[]);
void t_atomic(unsigned info[]);
void FF_T(unsigned info[]);
void PARADOX(unsigned info[]);
void RWX(unsigned info[]);
void necessity(unsigned info[]);
void necessitation(unsigned info[]);
void NKI_test(unsigned info[]);
void set_prefix(unsigned info[]);
void set_suffix(unsigned info[]);
void squeeze(unsigned info[], int a, int b, int c, int d);
void pretest_prefix();
void pretest_suffix();
void test_S4axiom();
void test_S5axiom();
void test_Daxiom();
void test_NK();
boolean test_mslat(trs T);
boolean test_jslat(trs T);
boolean Btest(TRS *T);
boolean B2test(TRS *T);
boolean Stest(TRS *T);
boolean Ctest(TRS *T);
boolean WBtest(TRS *T);
boolean NecImpDist(TRS *T);
boolean NecAdj(TRS *T);
boolean NecW(TRS *T);
/*
* In file dialog.c
*/
int dialog(boolean batch, char *batchfile);
char menu();
char readin(char *str);
void paws();
void job_defaults(boolean batch);
void set_frag( boolean set_sizmax );
void check_frag(int x);
void print_axiom(FILE *f, AXIOM x);
void display();
void disp(FILE *f);
void help(helpcode x);
void put_out(char *f_nm);
/*
* In file getjob.c
*/
void add_axioms();
void add_one_axiom( AXIOM select );
void bad_guy();
void connective();
void deletion();
void fragment();
void input_direct();
void jump_condition();
void logic_choice();
void set_logic( LOGIC lptr );
void print_version();
int n_of_procs();
void order_change();
void user_order(symb oldsymbols[], char *string, int neworder[]);
void print_options();
boolean read_job(char *batchfile);
void store_job();
void injob(FILE *f);
void outjob(FILE *f);
void trim();
void nospace(char *s);
void delete_saxiom();
void delete_uaxiom();
void delete_connective();
void nodelcon(char *s, symb spec, int formula);
/*
* In file isom.c
*/
void perm_initial();
void setperm();
int lower_than(int x);
int higher_than(int x);
void newperm(int *vec);
boolean isomorphic(ism ptr, trs T);
void snip(ism p);
void subst(ism p1, ism p2);
boolean isomorphic_anyhow(trs T);
void add_isoms(trs T);
boolean add_this(char mat[], ism i_tree);
ism tack_on(ism p, char mat[]);
/*
* In file logic_io.c
*/
int newsiz();
int newneg();
int neword();
int newdes();
void sep(int *x);
int next_bit();
int got_siz();
boolean got_neg();
boolean got_ord();
boolean got_des();
void mat_print();
void newmatplus(int x, int y);
void siz_print(FILE *f, output_style x);
void neg_print(FILE *f, output_style x);
void ord_print(FILE *f, output_style x);
void des_print(FILE *f, output_style x);
void C_print(FILE *f, output_style x);
void box_print(FILE *f, output_style x);
void u_print0(FILE *f, output_style x, int y);
void u_print1(FILE *f, output_style x, int y);
void u_print2(FILE *f, output_style x, int y);
void printup(FILE *f, output_style x);
void pretty_size(FILE *f);
void pretty_negno(FILE *f);
void pretty_ordno(FILE *f);
void pretty_desno(FILE *f);
void pretty_matno(FILE *f);
void pretty_boxno(FILE *f);
void pretty_umat(FILE *f, int x);
void fail_print(FILE *f);
void insert_badvalues( int offset );
void stats_print();
/*
* In file logic_pretest.c
*/
void new_two_ref(int a, int x, int b, int y);
boolean find_twos(unsigned info[], TRS *Tr);
void pretest_fus();
void affix_case(int a, int b, int c, int d);
void test_assertion();
void test_contraction();
void test_TW_upper_bounds();
/*
* In file logic_set.c
*/
boolean pre_set();
boolean utest(int x, unsigned info[]);
void set_vuloc(int r, int rr);
boolean badcase(int x, unsigned info[]);
int eval(int r, unsigned z[]);
int anothercase(int x);
boolean set_poss(unsigned info[], trs T);
void fusion(unsigned info[]);
boolean permutable(int a, int b, int c, unsigned info[]);
boolean logic_poss(unsigned info[]);
void logic_axioms(boolean x);
void efficient_logic_set();
/*
* In file logic_test.c
*/
boolean Good_matrix(unsigned info[], trs T);
void vect_into_C(unsigned info[]);
boolean fus_test(trs T);
boolean axtest(trs T);
void set_used(int x, trs T, boolean topper);
void setcon();
int getval(int y);
/*
* In file mp_parse.c
*/
int parse( symb fla[] );
int s_parse( symb fla[] );
int Match( symb start[] );
int Finish( int subf[], symb conn[], int tot );
int Loc( symb mn, int lft, int rgt );
boolean is_var(symb x);
int symbol_position( int x, symb s );
/*
* In file setup.c
*/
void subf_set();
int worstcase(int x, int ntop);
void set_u(int arr[], int x);
void CLoCK(int *timer);
void set_up_cc();
void job_start();
void job_stop(boolean batch);
void set_orders(char s[]);
void uglydisp(FILE *f);
void set_up_trin();
/*
* In file wffs.c
*/
symb newsymbol( char *string, symb symbol_list1[], symb symbol_list2[] );
void wff_initial();
boolean got_formula(int x, int y, int yy, char *s);
int infml(input_case x, int y, int yy);
boolean next_symbol( char longs[] );
symb this_symbol( char *string );
boolean seek_symbol( char longs[], symb fml[], int *k );
void fix_atoms(int y, int wf);
void outformula(int p, int q, FILE *f, varmode vm);
boolean is_in(symb s, int w);
void purge( symb badsym );

187
src/Mtypes.h Normal file
View File

@ -0,0 +1,187 @@
/*
* Mtypes.h
*
* This file is part of the header for MaGIC. It contains
* the type definitions. The special header axioms.h has to
* be included from here, as it uses the enumerated type
* boolean and defines such constants as AXMAX which are in
* turn used here in the definitions of the big structures.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
/*
* First the output codes. This is just an enumeration.
*/
typedef enum
{
NONE,
PRETTY,
UGLY,
SUMMARY
} output_style;
/*
* There is another enumeration of cases for formula input
*/
typedef enum
{
IN_CONC,
IN_PREM,
IN_BGUY,
IN_DEFN
} input_case;
/*
* And one for formula output
*/
typedef enum
{
VARS,
VALS
} varmode;
/*
* Then the various help codes
*/
typedef enum
{
MEN,
WFF1,
WFF2,
FDL,
BTW,
LOG,
OUT,
HELPMAX
} helpcode;
/*
* It remains to define the structure types used. Each
* "struct xxxtype" expression is abbreviated using typedef
* to preserve sanity later on. JOB is for communication of
* the major problem specification between the front end and
* MaGIC itself. The others are fairly self-explanatory.
*/
typedef struct isomorph
{ char *icv; /* Isomorphic version of info */
struct isomorph
*left,
*right,
*parent; /* Links to make a binary tree */
} ISM, *ism;
typedef struct symbol_list
{
char s[SLEN]; /* Connective as a string */
struct symbol_list
*next, *last; /* Links for list */
} SYMB, *symb;
typedef struct
{ symb sym; /* The main symbol */
int lsub,
rsub, /* Offsets of the subformulas */
*mtx, /* Start of the relevant matrix */
*lv,
*rv, /* To values of subformulas */
val; /* Currently assigned value */
} WFF;
typedef struct PerMutAtion
{
char h[SZ]; /* Image under homomorphism */
struct PerMutAtion
*pup; /* Pointer to the next guy up */
} PRM;
typedef enum {
lattices,
distributive_lattices,
total_orders
} L_DEFAULT;
typedef enum {
n_exists,
lat_exists,
fus_exists,
nec_exists,
PCMAX
} XF;
typedef struct
{
int adicity[CMAX], /* Of defined connectives */
croot[TMAX][RTMAX], /* Roots of rule conclusions */
proot[TMAX][RTMAX], /* Roots of rule premises */
defcon[CMAX], /* Roots of defined connectives */
failure, /* Root of badguy */
maxtime, /* Maximum clock reading */
maxmat, /* Maximum good matrices */
sizmax; /* Maximum matrix size */
output_style
tty_out,
fil_out; /* Output formats */
char data_dir[SLEN], /* Text name of input directory */
outfil_name[SLEN]; /* Text name of output file */
WFF form[FMAX]; /* (Subformulas of) axioms etc */
SYMB symtable[SYMBOLMAX]; /* Symbol table for connectives */
symb symtab, /* List of symbols used */
symbol[3][CMAX+8], /* Symbol table entries */
dcs[CMAX+1]; /* Defined connectives */
boolean axiom[AXMAX], /* Selected axioms (default none) */
concut[CMAX], /* Flags connectives with "cuts" */
f_n, f_lat,
f_t, f_T,
f_F, /* The fragment (default 1) */
f_fus, f_nec, /* The fragment (default 0) */
sizmax_ismax, /* (Boolean) Let sizmax float up */
distrib, /* Distributive lattice requested */
totord; /* Total orders requested */
LOGIC logic; /* The system (default FD) */
} JOB;

230
src/RM.c Normal file
View File

@ -0,0 +1,230 @@
/* RM.c (Read_Matrices) March 1991
*
* This is the basic post-processor for MaGIC.
*
* Selectmats reads in matrix representations of algebraic
* models for propositional logics and performs an operation
* on each one that satisfies a condition. It is called with
* three parameters, being a pointer to a MATRIX structure,
* the name of the user-defined selection function and the
* print mode (UGLY, PRETTY, TeX or NONE).
*
* The selector is allowed to return TRUE (1), FALSE (0) or
* END_OF_JOB (-1). Any other value is treated as 0.
*
* See RM.h for a description of the data structures.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "RM.h"
void selectmats(int (*selector)(), PRINTMODE printmode)
{
int i, done;
MATRIX *m;
m = mat_initial();
m->total_got = m->total_put = 0;
done = 0;
read_header(stdin,m);
if ( newsiz(stdin,m) )
do {
m->total_got++;
for (i=0; i<VALUEMAX; i++)
m->my_values[i] = -1;
*(m->my_string) = '\0';
switch ((*selector)(m)) {
case 1:
m->total_put++;
increment_ok(m);
printmat(m,printmode,SELECTED,stdout);
break;
case -1:
done = 1;
}
}
while (!done && newcase(stdin,m));
switch(printmode) {
case UGLY:
FORALLCON((m),i) printf(" -1");
printf(" -1 -1 -1 -1 -1\n");
break;
case PRETTY:
printf("\n\n Total read: %d\n Total written: %d\n\n",
m->total_got, m->total_put );
break;
case TeX:
printf("\n\n\\end{document}\n");
break;
case NONE:
break;
}
}
void relatemats(int (*selector)(), char *filename, char *relname)
{
int i, done;
MATRIX *m1;
FILE *f1;
MATRIX *m2;
FILE *f2;
f1 = fopen(filename,"r");
m1 = mat_initial();
m1->total_got = m1->total_put = 0;
done = 0;
read_header(f1,m1);
if (newsiz(f1,m1))
do {
m1->total_got++;
for (i=0; i<VALUEMAX; i++)
m1->my_values[i] = -1;
m1->my_string[0] = 0;
f2 = fopen(filename,"r");
m2 = mat_initial();
m2->total_got = m1->total_put = 0;
done = 0;
read_header(f2,m2);
if (newsiz(f2,m2))
do {
m2->total_got++;
for (i=0; i<VALUEMAX; i++)
m2->my_values[i] = -1;
*m2->my_string = 0;
switch ((*selector)(m1,m2)) {
case 1:
print_related(m1,m2,relname);
break;
case -1:
done = 1;
}
}
while (!done && newcase(f2,m2));
fclose(f2);
}
while (!done && newcase(f1,m1));
}
/*
* True is a dummy function which can be used to force every
* matrix to be printed out just as it is read in.
*/
int True(MATRIX *m)
{
return 1;
}
/*
* There are two versions of the matrix numbers. The ones
* prefixed with "ok" record the numbers on which compute has
* been performed. Those without record the numbers read in.
*
* Before compute happens, the "ok" numbers are incremented.
*/
void increment_ok(MATRIX *m)
{
int first, i;
for ( first = 0; first < m->cmax && m->okmatplus[first]; first++ ) ;
for ( i = first; i < m->cmax; i++ ) m->okmatplus[i] = 1;
if ( first ) m->okmatplus[first-1]++;
else {
if ( !m->okmatno ) {
if ( !m->okdesno ) {
if ( !m->okordno ) {
if ( m->fragment[NEG] )
m->oknegno++;
}
m->okordno++;
}
m->okdesno++;
}
m->okmatno++;
}
}
/*
* Mat_malloc allocates memory to a MATRIX pointer and does
* the necessary initialisation.
*/
MATRIX *mat_initial()
{
MATRIX *m;
m = (MATRIX *) malloc(sizeof(MATRIX));
/*
* WFF initialisation will go in here
*/
return m;
}
/*
* An abort function is provided. This causes a clean exit
* after printing an error message (with integer insert).
*
* Setting the integer argument to -1 disables this option.
*/
void Abort( char *s, int x)
{
fprintf( stderr, "\n\n Aborting on detection of an error\n " );
if ( x == -1 ) fprintf( stderr, s );
else fprintf( stderr, s, x );
fprintf( stderr, "\n" );
exit(1);
}

295
src/RM.h Normal file
View File

@ -0,0 +1,295 @@
/* Header for Read_Matrices
*
* Selectmats reads in matrix representations of algebraic
* models for propositional logics and prints out each one
* that satisfies a condition. It is called with three
* parameters, being a pointer to a MATRIX, the name of the
* user-defined selection function and the print mode
* (PRETTY, UGLY or TeX).
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
/*
* The setup is read into MATRIX fields as follows:
*
* siz the greatest-numbered value. So the
* values are the integers 0...siz.
*
* neg the negation table (if present).
*
* ord the partial order of implication.
*
* A, K disjunction and conjunction tables.
*
* designated designation and undesignation of values.
*
* tee the least designated value (if defined).
*
* eff the negation of tee (if defined).
*
* C the implication table.
*
* box the necessity table.
*
* fus the fusion table (if defined).
*
* fis the fission table (if defined).
*
* dcs the symbols for defined connectives.
*
* adicity of the defined connectives
*
* nulladic
* monadic
* dyadic matrices for the user's connectives.
*
* fused boolean flag: fusion is defined.
*
* tee_exists boolean flag: tee is defined.
*
* negno
* ordno
* desno
* matno Offset numbers of the current setup.
*
* oknegno
* okordno
* okdesno
* okmatno Offset numbers of the latest good setup.
*
* fragment connectives defined
*
*
* In addition, the constant SZ is defined as the greatest
* possible number of values. That is, siz < SZ always.
*
* The universal quantifier FORALL is defined for use in the
* host program if desired. FORALLCON is also provided to run
* through the user-defined primitives in their change order.
*
* The data type WFF is exactly as in MaGIC, for input and
* testing of formulas. The parser may be linked in.
*
* The array my_values and the string my_string are provided
* for communication of the results of tests etc to the
* printout routine. They are initialised to a series of
* -1s and to the null string respectively. These values
* should be used for the null communication.
*
* Several other MATRIX fields are used to control the
* environment, mostly to determine printing options.
*
* cmax number of user-added primitives
* total_got number of matrices read in
* total_put number which have passes the test
* singlematrix treat as though the only matrix
*
* Those are all integers. There are a couple of defined
* enumeration types, PRINTMODE and PRINTCOUNTER. These are
* the types of the parameters printmode and printcountermode
* passed to printmat. The former of these determines whether
* output is PRETTY, UGLY or TeX, while the latter determines
* whether the numbering of matrices is to be incremental
* within the output only or whether the numbers remain as on
* input.
*/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <ctype.h>
#define SZ 16
#define FMAX 256
#define CMAX 32
#define VALUEMAX 10
#define FORALL(m,x) for ( x = 0; x <= m->siz; x++ )
#define FOREACH(m,x) for ( x = m->siz; x >= 0; x-- )
#define FORALLCON(m,x) for ( x = 0; x < m->cmax; x++)
typedef enum { NONE, PRETTY, UGLY, TeX } PRINTMODE;
typedef enum { SELECTED, UNSELECTED } COUNTERMODE;
enum { NEG, TEE, TOP, BOT, FUS, LAT, BOX, FRAGMAX } ;
typedef struct well_formed_formula {
char *sym; /* The main symbol */
int lsub;
int rsub; /* Offsets of the subformulas */
int *mtx; /* Start of the relevant matrix */
int *lv;
int *rv; /* To values of subformulas */
int val; /* Currently assigned value */
} WFF;
/*
* Now for the big one: this is the matrix structure.
*/
typedef struct {
WFF form[FMAX];
WFF *tx;
int siz;
int neg[SZ];
int ord[SZ][SZ];
int designated[SZ];
int tee;
int eff;
int A[SZ][SZ];
int K[SZ][SZ];
int C[SZ][SZ];
int fus[SZ][SZ];
int fis[SZ][SZ];
int box[SZ];
int diamond[SZ];
int adicity[CMAX];
int nulladic[CMAX];
int monadic[CMAX][SZ];
int dyadic[CMAX][SZ][SZ];
int negno;
int oknegno;
int ordno;
int okordno;
int desno;
int okdesno;
int matno;
int okmatno;
int boxno;
int okboxno;
int matplus[CMAX];
int okmatplus[CMAX];
int fused;
int tee_exists;
int cmax;
int total_got;
int total_put;
int fragment[FRAGMAX];
int my_values[VALUEMAX];
char my_string[256];
char dcs[CMAX][16];
char symbols[3][15];
} MATRIX;
FILE *fopen();
/*
* Finally, here are the function prototypes for RM.c
*/
void selectmats(int (*selector)(), PRINTMODE printmode);
void relatemats(int (*selector)(), char *filename, char *relname);
int True(MATRIX *m);
void increment_ok(MATRIX *m);
MATRIX* mat_initial();
void Abort(char *s, int x);
/*
* These are the prototypes for RM_input.c
*/
void read_header(FILE *f, MATRIX *m);
int newsiz(FILE *f, MATRIX *m);
int newneg(FILE *f, MATRIX *m);
int neword(FILE *f, MATRIX *m);
int newdes(FILE *f, MATRIX *m);
int newC(FILE *f, MATRIX *m);
int newbox(FILE *f, MATRIX *m);
int newcon(FILE *f, MATRIX *m, int x);
int newcase(FILE *f, MATRIX *m);
int gotsiz(FILE *f, MATRIX *m);
int gotneg(FILE *f, MATRIX *m);
int gotord(FILE *f, MATRIX *m);
int gotdes(FILE *f, MATRIX *m);
int gotaro(FILE *f, MATRIX *m);
int gotbox(FILE *f, MATRIX *m);
int gotcon(FILE *f, MATRIX *m, int x);
/*
* These are the prototypes for RM_output.c
*/
void displaymat(MATRIX *m, char *legend);
void printmat(MATRIX *m, PRINTMODE printmode,
COUNTERMODE countermode, FILE *f);
void write_header(MATRIX *m);
void pu_print(MATRIX *m, int x, FILE *f);
void uu_print(MATRIX *m, int x);
void pbox_print( MATRIX *m, FILE *f );
void ubox_print(MATRIX *m);
void pC_print(MATRIX *m, FILE *f);
void uC_print(MATRIX *m);
void pdesprint(MATRIX *m, FILE *f);
void udesprint(MATRIX *m);
void pordprint(MATRIX *m, FILE *f);
void uordprint(MATRIX *m);
void pnegprint(MATRIX *m, FILE *f);
void unegprint(MATRIX *m);
void psizprint(MATRIX *m, FILE *f);
void usizprint(MATRIX *m);
void neg_number(MATRIX *m, FILE *f);
void ord_number(MATRIX *m, FILE *f);
void des_number(MATRIX *m, FILE *f);
void C_number(MATRIX *m, FILE *f);
void box_number(MATRIX *m, FILE *f);
void u_number(MATRIX *m, int x, FILE *f);
void nullprint(MATRIX *m, char *s, int x, FILE *f);
void unullprint(MATRIX *m, int x);
void monprint(MATRIX *m, char *s, char c, int arr[], FILE *f);
void umonprint(MATRIX *m, int arr[]);
void dyprint(MATRIX *m, char *s1, char c, int arr[][SZ],
char *s2, char d, int darr[][SZ], FILE *f);
void udyprint(MATRIX *m, int arr[][SZ]);
void tex_header();
void tex_mystuff(MATRIX *m);
void texchar(char c);
void tex_uprint(MATRIX *m, int x);
void tex_boxprint(MATRIX *m);
void tex_Cprint(MATRIX *m);
void tex_desprint(MATRIX *m);
void tex_ordprint(MATRIX *m);
void tex_negprint(MATRIX *m);
void tex_sizprint(MATRIX *m);
void tex_nullprint(MATRIX *m, char *s, int x);
void tex_monprint(MATRIX *m, char *s, char c, int arr[]);
void tex_dyprint(MATRIX *m, char *s1, char c, int arr[][SZ],
char *s2, char d, int darr[][SZ]);
void tex_dymatprint(MATRIX *m, int offset, char *s, char c, int arr[][SZ]);
void print_related(MATRIX *m1, MATRIX *m2, char *relname);

272
src/RM_input.c Normal file
View File

@ -0,0 +1,272 @@
/* Input.c March 1991
*
* Functions to read matrices for MaGIC postprocessor.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "RM.h"
void read_header(FILE *f, MATRIX *m)
{
int i, j = 0;
for (i=0; i<FRAGMAX; i++)
fscanf(f,"%d",m->fragment+i);
fscanf(f,"%d",&(m->cmax));
FORALLCON(m,i) {
fscanf(f,"%d",m->adicity+i);
do
fscanf(f,"%c",m->dcs[i]);
while (isspace(m->dcs[i][0]));
do
fscanf(f,"%c",m->dcs[i]+(++j));
while (!isspace(m->dcs[i][j]));
m->dcs[i][j] = 0;
}
}
int newsiz(FILE *f, MATRIX *m)
{
return(gotsiz(f,m)? (m->fragment[NEG]? newneg(f,m): neword(f,m)): 0);
}
int newneg(FILE *f, MATRIX *m)
{
return(gotneg(f,m)? neword(f,m): newsiz(f,m));
}
int neword(FILE *f, MATRIX *m)
{
return(gotord(f,m)? newdes(f,m):
(m->fragment[NEG]? newneg(f,m): newsiz(f,m)));
}
int newdes(FILE *f, MATRIX *m)
{
return(gotdes(f,m)? newC(f,m): neword(f,m));
}
int newC(FILE *f, MATRIX *m)
{
return(gotaro(f,m)? (m->fragment[BOX]? newbox(f,m): newcon(f,m,0)):
newdes(f,m));
}
int newbox(FILE *f, MATRIX *m)
{
return(gotbox(f,m)? newcon(f,m,0): newC(f,m));
}
int newcon(FILE *f, MATRIX *m, int x)
{
if (x >= m->cmax) return 1;
return(gotcon(f,m,x)? newcon(f,m,x+1):
(x? newcon(f,m,x-1):
(m->fragment[BOX]? newbox(f,m): newC(f,m))) );
}
int newcase(FILE *f, MATRIX *m)
{
if (m->cmax)
return newcon(f,m,m->cmax-1);
if (m->fragment[BOX] )
return newbox(f,m);
return newC(f,m);
}
int gotsiz(FILE *f, MATRIX *m)
{
fscanf(f,"%d",&(m->siz));
m->negno = m->ordno = 0;
m->oknegno = m->okordno = 0;
return (m->siz < SZ && m->siz > 0);
}
int gotneg(FILE *f, MATRIX *m)
{
int i;
fscanf(f,"%d",m->neg);
if (*(m->neg) < 0)
return 0;
m->negno++; m->ordno = 0;
m->okordno = 0;
for (i=1; i<=m->siz; i++ )
fscanf(f,"%d", m->neg+i);
return 1;
}
int gotord(FILE *f, MATRIX *m)
{
int i,j;
fscanf(f,"%d",*(m->ord));
if (**(m->ord) < 0)
return 0;
m->ordno++; m->desno = 0;
m->okdesno = 0;
FORALL(m,i) FORALL(m,j) if (i||j)
fscanf(f,"%d",m->ord[i]+j);
FORALL(m,i) FORALL(m,j) {
FORALL(m,m->A[i][j])
if (m->ord[i][m->A[i][j]] && m->ord[j][m->A[i][j]])
break;
FOREACH(m,m->K[i][j])
if (m->ord[m->K[i][j]][i] && m->ord[m->K[i][j]][j])
break;
}
return 1;
}
int gotdes(FILE *f, MATRIX *m)
{
int i;
fscanf(f,"%d",m->designated);
if (*(m->designated) < 0)
return 0;
FORALL(m,i)
if (i)
fscanf(f,"%d",m->designated+i);
FORALL(m,m->tee)
if ( m->designated[m->tee] )
break;
m->tee_exists = 1;
FORALL(m,i)
if (m->designated[i] && !m->ord[m->tee][i])
m->tee_exists = 0;
m->desno++; m->matno = 0;
m->okmatno = 0;
m->eff = m->neg[m->tee];
return 1;
}
int gotaro(FILE *f, MATRIX *m)
{
int i, j, k;
fscanf(f,"%d",*(m->C));
if (**(m->C) < 0)
return 0;
m->matno++;
if (m->fragment[BOX]) {
m->boxno = 0;
m->okboxno = 0;
}
else {
*(m->matplus) = 0;
*(m->okmatplus) = 0;
}
FORALL(m,i) FORALL(m,j)
if (i||j)
fscanf(f,"%d",m->C[i]+j);
m->fused = 1;
FORALL(m,i) FORALL(m,j) {
FORALL(m,m->fus[i][j])
if (m->ord[i][m->C[j][m->fus[i][j]]])
break;
if (m->fus[i][j] > m->siz)
m->fused = 0;
}
if (m->fused) {
FORALL(m,i) FORALL(m,j) FORALL(m,k)
if (m->ord[m->fus[i][j]][k] && !m->ord[i][m->C[j][k]])
m->fused = 0;
if (m->ord[i][m->C[j][k]] && !m->ord[m->fus[i][j]][k])
m->fused = 0;
}
if (m->fragment[NEG])
FORALL(m,i) FORALL(m,j)
m->fis[i][j] = m->C[m->neg[i]][j];
return 1;
}
int gotbox(FILE *f, MATRIX *m)
{
int i;
fscanf(f,"%d",m->box);
if (*(m->box) < 0)
return 0;
m->boxno++;
*(m->matplus) = 0;
*(m->okmatplus) = 0;
for (i=1; i<=m->siz; i++)
fscanf(f,"%d",m->box+i);
return 1;
}
int gotcon(FILE *f, MATRIX *m, int x)
{
int i, j, k;
fscanf(f,"%d",&k);
if (k < 0)
return 0;
m->matplus[x]++;
m->matplus[x+1] = 0;
m->okmatplus[x+1] = 0;
switch(m->adicity[x]) {
case 0:
m->nulladic[x] = k;
break;
case 1:
m->monadic[x][0] = k;
FORALL(m,i) if (i)
fscanf(f,"%d",m->monadic[x]+i);
break;
case 2:
m->dyadic[x][0][0] = k;
FORALL(m,i) FORALL(m,j)
if ( i||j )
fscanf(f,"%d",m->dyadic[x][i]+j);
}
return 1;
}

710
src/RM_output.c Normal file
View File

@ -0,0 +1,710 @@
/* Output.c March 1991
*
* These are the functions for ugly, pretty and TeX output of
* matrices. They are called from RM.c which is used by all
* MaGIC post-processing programs.
*/
/****************************************************************
* *
* MaGIC 2.0 *
* *
* (C) 1991 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "RM.h"
static int pnegno;
static int pordno;
static int pdesno;
static int pmatno;
static int pboxno;
static int pmatplus[CMAX];
static int singlematrix;
void displaymat(MATRIX *m, char *legend)
{
FILE *f;
f = fopen("/dev/tty","w");
singlematrix = 1;
system( "clear > /dev/tty" );
printmat( m, PRETTY, UNSELECTED, f );
fprintf( f, "\n\n %s", legend );
singlematrix = 0;
fclose(f);
}
void printmat(MATRIX *m, PRINTMODE printmode, COUNTERMODE countermode, FILE *f)
{
int i;
if ( countermode == SELECTED ) {
pnegno = m->oknegno;
pordno = m->okordno;
pdesno = m->okdesno;
pmatno = m->okmatno;
pboxno = m->okboxno;
FORALLCON(m,i)
pmatplus[i] = m->okmatplus[i];
}
else if ( countermode == UNSELECTED ) {
pnegno = m->negno;
pordno = m->ordno;
pdesno = m->desno;
pmatno = m->matno;
pboxno = m->boxno;
FORALLCON(m,i)
pmatplus[i] = m->matplus[i];
}
else Abort("Unrecognised print_counter mode: %d", countermode);
switch (printmode) {
case PRETTY:
pu_print( m, m->cmax-1, f );
if ( m->my_values[0] != -1 || m->my_string[0] ) {
fprintf( f, "\n %s", m->my_string );
for ( i = 0; m->my_values[i] != -1; i++ )
fprintf( f, " %d", m->my_values[i] );
fprintf( f, "\n" );
}
return;
case UGLY:
if ( m->total_put == 1 ) write_header( m );
uu_print( m, m->cmax-1 );
return;
case TeX:
if ( m->total_put == 1 ) tex_header();
tex_uprint( m, m->cmax-1 );
if ( m->my_values[0] != -1 || m->my_string[0] )
tex_mystuff( m );
return;
case NONE:
return;
}
Abort( "Unrecognised print mode: %d", printmode );
}
void write_header(MATRIX *m)
{
int i;
for ( i = 0; i < FRAGMAX; i++ )
printf( " %d", m->fragment[i] );
printf( "\n %d", m->cmax );
FORALLCON(m,i)
printf( " %d %s", m->adicity[i], m->dcs[i] );
printf( "\n");
}
void pu_print(MATRIX *m, int x, FILE *f)
{
if ( x < 0 ) {
if ( m->fragment[BOX] ) pbox_print( m, f );
else pC_print( m, f );
}
else {
if ( pmatplus[x] == 1 || singlematrix )
pu_print( m, x-1, f );
fprintf( f, "\n\n %s table ", m->dcs[x] );
u_number( m, x, f );
switch( m->adicity[x] ) {
case 0:
nullprint( m, m->dcs[x], m->nulladic[x], f );
break;
case 1:
monprint( m, m->dcs[x], 0, m->monadic[x], f );
break;
case 2:
dyprint( m, m->dcs[x], 0, m->dyadic[x], "", 0, 0, f );
}
}
}
void uu_print(MATRIX *m, int x)
{
if ( x < 0 ) {
if ( m->fragment[BOX] ) ubox_print( m );
else uC_print( m );
}
else {
if ( pmatplus[x] == 1 || singlematrix ) {
if ( m->total_put > 1 ) printf( " -1\n" );
uu_print( m, x-1 );
}
switch( m->adicity[x] ) {
case 0: unullprint( m, m->nulladic[x] );
break;
case 1: umonprint( m, m->monadic[x] );
break;
case 2: udyprint( m, m->dyadic[x] );
}
}
}
void pbox_print( MATRIX *m, FILE *f )
{
if ( pboxno == 1 || singlematrix ) pC_print( m, f );
fprintf( f, "\n\n Necessity " );
box_number( m, f );
monprint( m, "!", 0, m->box, f );
}
void ubox_print(MATRIX *m)
{
if ( pboxno == 1 || singlematrix ) {
if ( m->total_put > 1 ) printf( " -1\n");
uC_print( m );
}
umonprint( m, m->box );
}
void pC_print(MATRIX *m, FILE *f)
{
if ( pmatno == 1 || singlematrix ) pdesprint( m, f );
fprintf( f, "\n\n Implication " );
C_number( m, f );
if ( m->fused )
dyprint( m, "->", 0, m->C, "o", 0, m->fus, f );
else
dyprint( m, "->", 0, m->C, "", 0, 0, f );
}
void uC_print(MATRIX *m)
{
if ( pmatno == 1 || singlematrix ) {
if ( m->total_put > 1 ) printf( " -1\n");
udesprint( m );
}
udyprint( m, m->C );
}
void pdesprint(MATRIX *m, FILE *f)
{
if ( pdesno == 1 || singlematrix ) pordprint( m, f );
fprintf( f, "\n\n\n Choice of truths " );
des_number( m, f );
monprint( m, "True", '-', m->designated, f );
}
void udesprint(MATRIX *m)
{
if ( pdesno == 1 || singlematrix ) {
if ( m->total_put > 1 ) printf( " -1\n");
uordprint( m );
}
umonprint( m, m->designated );
}
void pordprint(MATRIX *m, FILE *f)
{
if ( pordno == 1 || singlematrix ) {
if ( m->fragment[NEG] ) pnegprint( m, f );
else psizprint( m, f );
}
fprintf( f, "\n\n\n Order table " );
ord_number( m, f );
dyprint( m, "_\b<", '-', m->ord, "", 0, 0, f );
}
void uordprint(MATRIX *m)
{
if ( pordno == 1 || singlematrix ) {
if ( m->total_put > 1 ) printf( " -1\n");
if ( m->fragment[NEG] ) unegprint( m );
else usizprint( m );
}
udyprint( m, m->ord );
}
void pnegprint(MATRIX *m, FILE *f)
{
if ( pnegno == 1 || singlematrix ) psizprint( m, f );
fprintf( f, "\n\n\n Negation table " );
neg_number( m, f );
monprint( m, "~", 0, m->neg, f );
}
void unegprint(MATRIX *m)
{
if ( pnegno == 1 || singlematrix ) {
if ( m->total_put > 1 ) printf( " -1\n");
usizprint( m );
}
umonprint( m, m->neg );
}
void psizprint(MATRIX *m, FILE *f)
{
fprintf( f, "\n\n\n Size: %d\n", m->siz+1 );
}
void usizprint(MATRIX *m)
{
printf( " %d\n", m->siz );
}
void neg_number(MATRIX *m, FILE *f)
{
fprintf( f, "%d.%d", m->siz+1, pnegno );
}
void ord_number(MATRIX *m, FILE *f)
{
if ( !m->fragment[NEG] ) fprintf( f, "%d", m->siz+1 );
else neg_number( m, f );
fprintf( f, ".%d", pordno );
}
void des_number(MATRIX *m, FILE *f)
{
ord_number( m, f );
fprintf( f, ".%d", pdesno );
}
void C_number(MATRIX *m, FILE *f)
{
des_number( m, f );
fprintf( f, ".%d", pmatno );
}
void box_number(MATRIX *m, FILE *f)
{
C_number( m, f );
fprintf( f, ".%d", pboxno );
}
void u_number(MATRIX *m, int x, FILE *f)
{
if ( !x ) {
if ( m->fragment[BOX] ) box_number( m, f );
else C_number( m, f );
}
else u_number( m, x-1, f );
fprintf( f, ".%d", pmatplus[x] );
}
void nullprint(MATRIX *m, char *s, int x, FILE *f)
{
fprintf( f, " %s = %d\n", s, x );
}
void unullprint(MATRIX *m, int x)
{
printf( "%d\n", x );
}
void monprint(MATRIX *m, char *s, char c, int arr[], FILE *f)
{
int i, offset;
fprintf( f, "\n\n " );
for ( offset = 0; s[offset]; offset++ ) fprintf( f, " " );
if ( offset > 1 ) fprintf(f, " ");
fprintf( f, "a |" );
FORALL(m,i) fprintf( f, " %x", i );
fprintf( f, "\n " );
for ( i = 0; i < offset; i++ ) fprintf( f, "-" );
if ( offset > 1 ) fprintf( f, "--" );
fprintf( f, "--+" );
FORALL(m,i) fprintf( f, "--" );
fprintf( f, "\n " );
if ( offset > 1 ) fprintf( f, "%s(a) |", s );
else fprintf( f, "%sa |", s );
FORALL(m,i)
if ( c == '-' ) fprintf( f, " %c", arr[i]? '+': '-' );
else fprintf( f, " %x", arr[i] );
fprintf( f, "\n" );
}
void umonprint(MATRIX *m, int arr[])
{
int i;
FORALL(m,i)
printf( " %d", arr[i] );
printf( "\n" );
}
void dyprint(MATRIX *m, char *s1, char c, int arr[][SZ],
char *s2, char d, int darr[][SZ], FILE *f)
{
int i, j, offset = 0;
for ( i = 0; s1[i]; i++ )
if ( s1[i] == '\b' ) offset--; else offset++;
fprintf( f, "\n\n %s |", s1 );
FORALL(m,i) fprintf( f, " %x", i );
if ( *s2 ) {
fprintf( f, "%15s |", s2 );
FORALL(m,i) fprintf( f, " %x", i );
}
fprintf( f, "\n " );
for ( i = 1; i < offset; i++ ) fprintf( f, "-" );
fprintf( f, "---+" );
FORALL(m,i) fprintf( f, "--" );
if ( *s2 ) {
for ( i = 14; i; i-- )
fprintf( f, (i > strlen(s2)? " ": "-") );
fprintf( f, "--+" );
FORALL(m,i) fprintf( f, "--" );
}
FORALL(m,i) {
fprintf( f, "\n " );
for ( j = 1; j < offset; j++ ) fprintf( f, " " );
fprintf( f, "%x |", i );
FORALL(m,j)
if ( c == '-' )
fprintf( f, " %c", arr[i][j]? '+': '-' );
else fprintf( f, " %x", arr[i][j] );
if ( *s2 ) {
fprintf( f, "%15x |", i );
FORALL(m,j)
if ( d == '-' )
fprintf( f, " %c", darr[i][j]? '+': '-' );
else fprintf( f, " %x", darr[i][j] );
}
}
fprintf( f, "\n" );
}
void udyprint(MATRIX *m, int arr[][SZ])
{
int i, j;
FORALL(m,i) FORALL(m,j)
printf( " %d", arr[i][j] );
printf( "\n" );
}
void tex_header()
{
printf( "\\documentstyle{article}\n");
printf( "\\oddsidemargin=15mm\n");
printf( "\\evensidemargin=15mm\n");
printf( "\\textwidth=160mm\n");
printf( "\\topmargin=0mm\n");
printf( "\\textheight=250mm\n");
printf( "\\begin{document}\n\n");
printf( "\\pagestyle{empty}\n");
printf( "\\newcommand{\\C}{\\rightarrow}\n");
printf( "\\newcommand{\\N}{\\neg}\n");
printf( "\\newcommand{\\A}{\\mbox{$\\,${\\footnotesize");
printf( " $\\vee$}$\\,$}}\n");
printf( "\\newcommand{\\fs}{\\circ}\n");
printf( "\\newcommand{\\hugeskip}{\\vspace{10mm}}\n");
printf( "\\setlength{\\tabcolsep}{1.5mm}\n\n");
}
void tex_mystuff(MATRIX *m)
{
int i;
printf( "\n%s", m->my_string);
for ( i = 0; m->my_values[i] != -1; i++ )
printf( " \\ %d", m->my_values[i]);
}
void texchar(char c)
{
switch(c) {
case '&':
case '%':
case '$':
case '#':
case 'v':
case '^':
case '_':
case '{':
case '}': printf( "\\%c", c ); return;
case '~': printf( "$\\N$" ); return;
case '>': printf( "$\\C$" ); return;
case '<': printf( "$\\leq$" ); return;
case 'o': printf( "$\\fs$" ); return;
case '-': printf( "$-$" ); return;
case '!': printf( "$\\Box$" ); return;
case '?': printf( "$\\Diamond$" ); return;
}
putchar( c );
}
void texstring(char *s)
{
do texchar( *s );
while ( *s++ );
}
void tex_uprint(MATRIX *m, int x)
{
if ( x < 0 ) {
if ( m->fragment[BOX] ) tex_boxprint( m );
else tex_Cprint( m );
}
else {
if ( pmatplus[x] == 1 || singlematrix )
tex_uprint( m, x-1 );
printf(
"\n\n\\hugeskip\\noindent\\parbox[t]{160mm}{");
texstring( m->dcs[x] );
printf( " table " );
u_number( m, x, stdout );
switch( m->adicity[x] ) {
case 0:
tex_nullprint( m, m->dcs[x], m->nulladic[x] );
break;
case 1:
tex_monprint( m, m->dcs[x], ' ', m->monadic[x] );
break;
case 2:
tex_dyprint( m, m->dcs[x], 0, m->dyadic[x], "", 0, 0 );
}
printf( "}" );
}
}
void tex_boxprint(MATRIX *m)
{
if ( pboxno == 1 || singlematrix ) tex_Cprint( m );
printf(
"\n\n\\hugeskip\\noindent\\parbox[t]{160mm}{Necessity " );
box_number( m, stdout );
tex_monprint( m, "!", ' ', m->box );
printf( "}" );
}
void tex_Cprint(MATRIX *m)
{
if ( pmatno == 1 || singlematrix ) tex_desprint( m );
printf(
"\n\n\\hugeskip\\noindent\\parbox[t]{160mm}{Implication " );
C_number( m, stdout );
if ( m->fused )
tex_dyprint( m, ">", 0, m->C, "o", 0, m->fus );
else
tex_dyprint( m, ">", 0, m->C, "", 0, 0 );
printf( "}" );
}
void tex_desprint(MATRIX *m)
{
if ( pdesno == 1 || singlematrix ) tex_ordprint( m );
printf("\n\n\\hugeskip\\noindent\\parbox[t]{160mm}{Choice of truths " );
des_number( m, stdout );
tex_monprint( m, "True", '-', m->designated );
printf( "}" );
}
void tex_ordprint(MATRIX *m)
{
if ( pordno == 1 || singlematrix ) {
if ( m->fragment[NEG] ) tex_negprint( m );
else tex_sizprint( m );
}
printf("\n\n\\hugeskip\\noindent\\parbox[t]{160mm}{Order table " );
ord_number( m, stdout );
tex_dyprint( m, "<", '-', m->ord, "", 0, 0 );
printf( "}" );
}
void tex_negprint(MATRIX *m)
{
if ( pnegno == 1 || singlematrix ) tex_sizprint( m );
printf("\n\n\\hugeskip\\noindent\\parbox[t]{160mm}{Negation table " );
neg_number( m, stdout );
tex_monprint( m, "~", ' ', m->neg );
printf( "}" );
}
void tex_sizprint(MATRIX *m)
{
if ( m->total_put > 1 ) printf( "\n\n\\newpage");
printf( "\\noindent Size: %d", m->siz+1 );
}
void tex_nullprint(MATRIX *m, char *s, int x)
{
printf( " \\ ");
texstring( s );
printf( " = %d", x );
}
void tex_monprint(MATRIX *m, char *s, char c, int arr[])
{
int i;
printf("\\\\[3mm]\n\\hspace*{5mm}\\begin{tabular}{r|" );
FORALL(m,i) putchar( 'c' );
printf( "}\na &");
FORALL(m,i) {
printf( " %x ", i );
if ( i < m->siz ) putchar( '&' );
}
printf( "\\\\\\hline\n");
texstring( s );
printf("(a)");
printf( " & ");
FORALL(m,i) {
if ( c == '-' )
texchar( arr[i]? '+': '-' );
else printf( " %x ", arr[i] );
if ( i < m->siz ) putchar( '&' );
else printf( "\\\\\n");
}
printf( "\\end{tabular}");
}
void tex_dyprint(MATRIX *m, char *s1, char c, int arr[][SZ],
char *s2, char d, int darr[][SZ])
{
printf( "\\\\[3mm]\n" );
tex_dymatprint( m, 5, s1, c, arr );
if ( *s2 ) tex_dymatprint( m, 10, s2, d, darr);
}
void tex_dymatprint(MATRIX *m, int offset, char *s, char c, int arr[][SZ])
{
int i, j;
printf( "\\hspace*{%dmm}\\begin{tabular}{r|", offset );
FORALL(m,i) putchar( 'c' );
printf( "}\n");
texstring( s );
printf( " &");
FORALL(m,i) {
printf( " %x ", i );
if ( i < m->siz ) putchar( '&' );
}
printf( "\\\\\\hline\n");
FORALL(m,i) {
printf( "%x &", i );
FORALL(m,j) {
if ( c == '-' )
texchar( arr[i][j]? '+': '-' );
else printf( " %x ", arr[i][j] );
if ( j < m->siz ) putchar( '&' );
else printf( "\\\\\n");
}
}
printf( "\\end{tabular}");
}
void print_related(MATRIX *m1, MATRIX *m2, char *relname)
{
printf("%s m%d m%d\n", relname, m1->total_got, m2->total_got);
}

583
src/axiom_tests.c Normal file
View File

@ -0,0 +1,583 @@
#include "MaGIC.h"
/*
* This file contains the code for testing each axiom. There are
* four types of case. First are axioms which do not depend on the
* contents of the implication, or box matrices at all. These give
* rise to 0-refutations. That is, they are either true or false
* of the extensional setup. They can be tested before entry to the
* search routine. An example is the law of the excluded middle
* A v ~A which depends only on the lattice, the negation operation
* and the choice of designated values.
*
* The second group consists of axioms such as A & (A->B) -> B,
* which require one reference to the implication or box matrix.
* These are tested at the stage of setting up the search space
* and secured by taking out the impossible values (such as any x
* for cell [A->B] such that not A&x ord B).
*
* The third group consists of axioms which require a small number
* of matrix references. `Small' means 2 in MaGIC at present. An
* example is the S4 axiom !A -> !!A, any failure of which requires
* values x for !A and y for !x such that not x ord y.
*
* Finally, there are a few cases in which multiple matrix entries
* are involved. These are treated by `lazy constraint generation'
* at the testing stage after candidate matrices have been found.
*/
/*
* GROUP 0 (0-refutations)
*/
boolean f_arrow_t() /*** f -> t ***/
{
return ( ord[N[des]][des] );
}
boolean Exmid() /*** a v ~a ***/
{
int a;
FORALL(a)
if ( !desig[A[a][N[a]]]) return false;
return true;
}
boolean Boolalg() /*** a&~a -> b ***/
{
int a;
FORALL(a)
if ( A[a][N[a]] != siz ) return false;
return true;
}
boolean SemiBool() /*** a&~a -> bv~b ***/
{
int a, b;
FORALL(a) FORALL(b)
if ( !ord[K[a][N[a]]][A[b][N[b]]] ) return false;
return true;
}
boolean paradox() /*** des = T ***/
{
int a;
FORALL(a) if ( !ord[a][des] ) return false;
return true;
}
/**********************************************************************/
/*
* GROUP 1 (1-refutations)
*
* The parameter here is the vector of possible-value sets.
* The general form of the procedure is
* for each relevant possible-value set s do
* for each impossible value x of s do
* remove x from s
* end for
* end for
* The vector is indexed by impindex and boxindex. Impindex[x][y]
* picks out the offset of the vector entry corresponding to the
* implication [x->y] while boxindex[x] picks out that corresponding
* to [!x]. REMOVE is a macro for taking a value out of a set.
*
* Note that no value needs to be returned by these operations, as
* only the side effect of diminishing the possible-value sets is
* intended.
*/
void E_assertion(unsigned info[]) /*** t->a -> a ***/
{
int a, b;
FORALL(b) if ( desig[b] )
FORALL(a)
info[impindex[b][a]] &= less_than[a];
}
void contraction(unsigned info[]) /*** (a->.a->b) ->. a->b ***/
{
int a, b, c;
if ( theJob->f_lat ) Wstar(info);
if ( theJob->f_n ) Reductio(info);
FORALL(a) FORALL(b) if ( !ord[a][b] )
FORALL(c) if ( ord[a][c] )
REMOVE(c,info[impindex[a][b]]);
}
void Wstar(unsigned info[]) /*** a & (a->b) -> b ***/
{
int a, b, c;
FORALL(a) FORALL(b) FORALL(c)
if ( !ord[K[a][c]][b] )
REMOVE(c,info[impindex[a][b]]);
}
void Reductio(unsigned info[]) /*** a->~a -> ~a ***/
{
int a, b;
if ( theJob->f_lat ) Exmid();
FORALL(a) FORALL(b)
if ( !ord[b][N[a]] )
REMOVE(b,info[impindex[a][N[a]]]);
}
void assertion(unsigned info[]) /*** 0->a = T, t->a = a ***/
{
int a, b;
FORALL(a) FORALL(b) {
if ( b < siz ) REMOVE(b,info[impindex[0][a]]);
if ( b != a ) REMOVE(b,info[impindex[des][a]]);
}
}
void ata(unsigned info[]) /*** a ->. t->a ***/
{
int a;
FORALL(a)
info[impindex[des][a]] &= greater_than[a];
}
void TaT(unsigned info[]) /*** T ->. a->T ***/
{
int a, b;
FORALL(a) if ( !ord[a][siz] ) {
*info = 0;
return;
}
FORALL(b) if ( b < siz )
FORALL(a)
REMOVE(b,info[impindex[a][siz]]);
}
void mingle(unsigned info[]) /*** a ->. a->a ***/
{
int a;
FORALL(a)
info[impindex[a][a]] &= greater_than[a];
}
void t_atomic(unsigned info[]) /*** p v (p -> q) ***/
{
int a, b, c;
FORALL(a) FORALL(c) if ( !desig[A[a][c]] )
FORALL(b)
REMOVE(c,info[impindex[a][b]]);
}
void FF_T(unsigned info[]) /*** T ->. F -> F ***/
{
int a, b;
FORALL(a)
if ( !ord[0][a] || !ord[a][siz] ) *info = 0;
FORALL(b) if ( b < siz )
FORALL(a)
REMOVE(b,info[impindex[0][a]]);
if ( F_N || theJob->axiom[AxB] || theJob->axiom[AxB2] )
FORALL(a) FORALL(b)
if ( b < siz )
REMOVE(b,info[impindex[a][siz]]);
}
void PARADOX(unsigned info[]) /*** a ->. b->a ***/
{
int a, b;
if ( !paradox() ) *info = 0;
FORALL(a) FORALL(b)
info[impindex[a][b]] &= greater_than[b];
}
void RWX(unsigned info[]) /*** If LEM, a+1 & (a+1->0) = 0 ***/
{
int a, b;
FORALL(a)
if ( !desig[A[a][N[a]]] ) return;
FORALL(a) if ( a )
FORALL(b) if ( K[a][b] )
REMOVE(b,info[impindex[a][0]]);
}
void necessity(unsigned info[]) /* !a implies a */
{
int a, x;
FORALL(a)
FORALL(x) if ( !ord[x][a] )
REMOVE(x,info[boxindex[a]]);
}
void necessitation(unsigned info[]) /* des(a) ==> des(!a) */
{
int a, x;
FORALL(a) if ( desig[a] )
FORALL(x) if ( !desig[x] )
REMOVE(x,info[boxindex[a]]);
}
void NKI_test(unsigned info[]) /* des(a) ==> !b implies a */
{
int a, b, x;
FORALL(a) if ( desig[a] )
FORALL(x) if ( !ord[x][a] )
FORALL(b)
REMOVE(x,info[boxindex[b]]);
}
/*
* This affixing check takes considerable time, but pays.
*/
void set_prefix(unsigned info[])
{
int i, j, k;
FORALL(i) FORALL(j)
for ( k = j+1; k <=siz; k++ )
if ( ord[j][k] && !( F_N && j < N[k] ))
if ( !(Greater_than[j] & Less_than[k]) )
squeeze( info, i, j, i, k );
}
void set_suffix(unsigned info[])
{
int i, j, k;
FORALL(i) FORALL(j)
for ( k = 0; k < i; k++ )
if ( ord[k][i] && !( F_N && i < N[k] ))
if ( !(Greater_than[k] & Less_than[i]) )
squeeze( info, i, j, k, j );
}
/*
* Squeeze, a subroutine of the above, squeezes out of the
* search space any values which are incompatible with this
* particular case of affixing: ord[ a->b ][ c->d ].
*/
void squeeze(unsigned info[], int a, int b, int c, int d)
{
int i;
int k, m;
k = impindex[a][b]; m = impindex[c][d];
FORALL(i) {
if ( IN(i,info[k]) ) {
if ( !(greater_than[i] & info[m]) )
REMOVE(i,info[impindex[a][b]]);
}
if ( IN(i,info[m]) ) {
if ( !(less_than[i] & info[k]) )
REMOVE(i,info[impindex[c][d]]);
}
}
}
/**********************************************************************/
/*
* GROUP 2 (2-refutations)
*/
void pretest_prefix()
{
int i, j, k;
FORALL(i) FORALL(j) if ( !( F_N && i < N[j] ))
for ( k = siz; k > j; k-- ) if ( ord[j][k] )
if ( !(Greater_than[j] & Less_than[k]) )
affix_case( i, j, i, k );
}
void pretest_suffix()
{
int i, j, k;
FORALL(i) FORALL(j) if ( !( F_N && i < N[j] ))
for ( k = 0; k < i; k++ ) if ( ord[k][i] )
if ( !(Greater_than[k] & Less_than[i]) )
affix_case( i, j, k, j );
}
void test_S4axiom()
{
int a, x, y;
FORALL(x)
FORALL(y) if ( !ord[x][y] )
FORALL(a)
new_two_ref( boxindex[a], x, boxindex[x], y );
}
void test_S5axiom()
{
int a, x, y;
FORALL(a)
FORALL(x) if ( !ord[a][x] )
FORALL(y)
new_two_ref( boxindex[N[a]], y, boxindex[N[y]], x );
}
void test_Daxiom()
{
int a, x, y;
FORALL(x)
FORALL(y) if ( !ord[x][N[y]] )
FORALL(a)
new_two_ref( boxindex[a], x, boxindex[N[a]], y );
}
void test_NK()
{
int a, b, x, y;
FORALL(a)
FORALL(x) if ( !ord[a][x] )
FORALL(b)
FORALL(y)
new_two_ref( boxindex[b], y, impindex[y][a], x );
}
/**********************************************************************/
/*
* GROUP 3 (many-refutations)
*
* The general form of the axiom test is
* for each assignment of values to the variables
* if the axiom fails
* call Ref with each cell used
* return false
* endif
* endfor
* return true
*/
boolean test_mslat(trs T)
{
int a, b, c;
FORaLL(b)
for ( c = siz-1; c > b; c-- )
if ( !ord[b][c] )
FORaLL(a)
if ( K[C[a][b]][C[a][c]] != C[a][K[b][c]] ) {
Ref( impindex[a][b], T );
Ref( impindex[a][c], T );
Ref( impindex[a][K[b][c]], T );
return false;
}
return true;
}
boolean test_jslat(trs T)
{
int a, b, c;
FORaLL(a)
for ( b = siz-1; b > a; b-- )
if ( !ord[a][b] )
FORaLL(c)
if ( K[C[a][c]][C[b][c]] != C[A[a][b]][c] ) {
Ref( impindex[a][c], T );
Ref( impindex[b][c], T );
Ref( impindex[A[a][b]][c], T );
return false;
}
return true;
}
boolean Btest(trs T)
{
int a, b, c;
FORaLL(a) FORaLL(b) FORaLL(c)
if ( !ord[C[a][b]] [C[C[c][a]][C[c][b]]] ) {
Ref(impindex[a][b], T);
Ref(impindex[c][a], T);
Ref(impindex[c][b], T);
Ref(impindex[C[c][a]][C[c][b]], T);
return false;
}
return true;
}
/**********************************/
boolean B2test(trs T)
{
int a, b, c;
FORaLL(a) FORaLL(b) FORaLL(c)
if ( !ord[C[a][b]] [C[C[b][c]][C[a][c]]] ) {
Ref(impindex[a][b], T);
Ref(impindex[b][c], T);
Ref(impindex[a][c], T);
Ref(impindex[C[b][c]][C[a][c]], T);
return false;
}
return true;
}
/**********************************/
boolean Stest(trs T)
{
int a, b, c;
FORaLL(a) FORaLL(b) FORaLL(c)
if ( !ord[C[a][C[b][c]]] [C[C[a][b]][C[a][c]]] ) {
Ref(impindex[a][b], T);
Ref(impindex[b][c], T);
Ref(impindex[a][c], T);
Ref(impindex[a][C[b][c]], T);
Ref(impindex[C[a][b]][C[a][c]], T);
return false;
}
return true;
}
/*********************************/
boolean Ctest(trs T)
{
int a, b, c;
FORaLL(a) FORaLL(c) if ( a < c )
FORaLL(b)
if ( C[c][C[a][b]] != C[a][C[c][b]] ) {
Ref(impindex[a][b], T);
Ref(impindex[c][b], T);
Ref(impindex[a][C[c][b]], T);
Ref(impindex[c][C[a][b]], T);
return false;
}
return true;
}
/*********************************/
boolean WBtest(trs T)
{
int a, b, c;
FORaLL(a) FORaLL(b) FORaLL(c)
if ( !ord[K[C[a][b]][C[b][c]]] [C[a][c]] ) {
Ref(impindex[a][b], T);
Ref(impindex[b][c], T);
Ref(impindex[a][c], T);
return false;
}
return true;
}
/*********************************/
boolean NecImpDist(trs T)
{
int a, b;
FORaLL(a) FORaLL(b)
if ( !ord[box[C[a][b]]] [C[box[a]][box[b]]] ) {
Ref(impindex[a][b], T);
Ref(impindex[box[a]][box[b]], T);
Ref(boxindex[a], T);
Ref(boxindex[b], T);
Ref(boxindex[C[a][b]], T);
return false;
}
return true;
}
/*********************************/
boolean NecAdj(trs T)
{
int a, b;
FORaLL(a) FORaLL(b)
if ( !ord[K[box[a]][box[b]]] [box[K[a][b]]] ) {
Ref(boxindex[a], T);
Ref(boxindex[b], T);
Ref(boxindex[K[a][b]], T);
return false;
}
return true;
}
/*********************************/
boolean NecW(trs T)
{
int a, b;
FORaLL(a) FORaLL(b)
if ( !ord[C[box[a]][C[box[a]][b]]] [C[box[a]][b]] ) {
Ref(boxindex[a], T);
Ref(impindex[box[a]][b], T);
Ref(impindex[box[a]][C[box[a]][b]], T);
return false;
}
return true;
}
/*********************************/

368
src/axioms.c Normal file
View File

@ -0,0 +1,368 @@
/*
* axioms.c
*
* This file contains the code specific to the pre-defined
* axioms and logics. To add or remove an axiom, or to add,
* remove or alter the definition of a logic, various changes
* must be made in this file and in axioms.h, as described in
* the documentation.
*/
#include "MaGIC.h"
/*
* Strings_initial simply sets the strings containing the names
* of known logics and the surface forms of known axioms
*/
void strings_initial()
{
strcpy(logic_name[Null_logic], "");
strcpy(logic_name[FD], "FD");
strcpy(logic_name[B], "B");
strcpy(logic_name[DW], "DW");
strcpy(logic_name[TW], "TW");
strcpy(logic_name[EW], "EW");
strcpy(logic_name[RW], "C");
strcpy(logic_name[LIN], "LIN");
strcpy(logic_name[T], "T");
strcpy(logic_name[E], "E");
strcpy(logic_name[R], "R");
strcpy(logic_name[CK], "CK");
strcpy(logic_name[S4], "S4");
strcpy(ax_string[RulPref], "p -> q / (r -> p) -> (r -> q)");
strcpy(ax_string[RulSuff], "p -> q / (q -> r) -> (p -> r)");
strcpy(ax_string[AxKcomp], "((p -> q) & (p -> r)) -> (p -> (q & r))");
strcpy(ax_string[AxAcomp], "((p -> r) & (q -> r)) -> ((p v q) -> r)");
strcpy(ax_string[AxX], "p v ~p");
strcpy(ax_string[AxBA], "(p & ~p) -> q");
strcpy(ax_string[AxSBA], "(p & ~p) -> (q v ~q)");
strcpy(ax_string[AxW2], "(p & (p -> q)) -> q");
strcpy(ax_string[AxK], "p -> (q -> p)");
strcpy(ax_string[AxK2], "p / q -> p");
strcpy(ax_string[AxM], "p -> (p -> p)");
strcpy(ax_string[AxRED], "(p -> ~p) -> ~p");
strcpy(ax_string[RulC3], "p / (p -> q) -> q");
strcpy(ax_string[AxCt], "p -> (t -> p)");
strcpy(ax_string[Axat], "p v (p -> q)");
strcpy(ax_string[AxTF], "T -> (F -> F)");
strcpy(ax_string[AxC2], "p -> ((p -> q) -> q)");
strcpy(ax_string[AxFN], "(p -> ~q) -> (q -> ~p)");
strcpy(ax_string[AxW], "(p -> (p -> q)) -> (p -> q)");
strcpy(ax_string[AxB], "(q -> r) -> ((p -> q) -> (p -> r))");
strcpy(ax_string[AxB2], "(p -> q) -> ((q -> r) -> (p -> r))");
strcpy(ax_string[AxS], "(p -> (q -> r)) -> ((p -> q) -> (p -> r))");
strcpy(ax_string[AxC], "(p -> (q -> r)) -> (q -> (p -> r))");
strcpy(ax_string[AxWB], "((p -> q) & (q -> r)) -> (p -> r)");
strcpy(ax_string[RulNec], "p / !p");
strcpy(ax_string[AxNec], "!p -> p");
strcpy(ax_string[Ax4], "!p -> !!p");
strcpy(ax_string[AxNID], "!(p -> q) -> (!p -> !q)");
strcpy(ax_string[AxNand], "(!p & !q) -> !(p & q)");
strcpy(ax_string[AxNW], "(!p -> (!p -> q)) -> (!p -> q)");
strcpy(ax_string[AxNK], "p -> (!q -> p)");
strcpy(ax_string[AxNKI], "p / !q -> p");
strcpy(ax_string[Ax5], "p -> !?p");
strcpy(ax_string[AxD], "!p -> ?p");
}
/*
* Tests_initial sets the list of axiom test functions.
* The zero_tests are executed when the extensional
* setup has been read, before any call to transref.
* The one_tests are executed when impossible values are
* being removed from the search space inside transref.
* The two_tests are called by transref to pre-process
* two-refutations in order to avoid having to generate
* before testing them. The many_tests are the default
* test routines called when the candidate matrix has
* been generated. All tests are null by default
*/
void tests_initial()
{
AXIOM a;
for ( a = AxNull; a < AXMAX; a++ ) {
TL[a].zero_test = TL[a].many_test = 0;
TL[a].one_test = TL[a].two_test = TL[a].three_test = 0;
}
TL[AxX].zero_test = Exmid;
TL[AxBA].zero_test = Boolalg;
TL[AxSBA].zero_test = SemiBool;
TL[AxK2].zero_test = paradox;
TL[RulPref].one_test = set_prefix;
TL[RulSuff].one_test = set_suffix;
TL[AxW2].one_test = Wstar;
TL[AxK].one_test = PARADOX;
TL[AxM].one_test = mingle;
TL[AxRED].one_test = Reductio;
TL[RulC3].one_test = E_assertion;
TL[AxCt].one_test = ata;
TL[Axat].one_test = t_atomic;
TL[AxTF].one_test = FF_T;
TL[RulNec].one_test = necessitation;
TL[AxNec].one_test = necessity;
TL[AxNKI].one_test = NKI_test;
TL[RulPref].two_test = pretest_prefix;
TL[RulSuff].two_test = pretest_suffix;
TL[Ax4].two_test = test_S4axiom;
TL[Ax5].two_test = test_S5axiom;
TL[AxD].two_test = test_Daxiom;
TL[AxC2].two_test = test_assertion;
TL[AxW].two_test = test_contraction;
TL[AxNK].two_test = test_NK;
TL[AxKcomp].many_test = test_mslat;
TL[AxAcomp].many_test = test_jslat;
TL[AxNID].many_test = NecImpDist;
TL[AxNand].many_test = NecAdj;
TL[AxB].many_test = Btest;
TL[AxB2].many_test = B2test;
TL[AxS].many_test = Stest;
TL[AxC].many_test = Ctest;
TL[AxWB].many_test = WBtest;
TL[AxNW].many_test = NecW;
}
/*
* Logics_initial sets the arrays showing which axioms are valid in
* which logics. Note that each logic has its own subroutine, except
* for the base logics FD and B, which have no proper axioms.
*/
void logics_initial()
{
LOGIC l;
AXIOM a;
for ( l = Null_logic; l < LOGMAX; l++ ) {
for ( a = AxNull; a < AXMAX; a++ )
valid[l][a] = false;
default_orders[l] = distributive_lattices;
default_fragment[l][n_exists] = true;
default_fragment[l][lat_exists] = true;
default_fragment[l][fus_exists] = false;
default_fragment[l][nec_exists] = false;
}
init_B();
init_DW();
init_TW();
init_EW();
init_RW();
init_LIN();
init_CK();
init_T();
init_E();
init_R();
init_S4();
}
void init_B()
{
valid[B][RulPref] = true;
valid[B][RulSuff] = true;
valid[B][AxKcomp] = true;
valid[B][AxAcomp] = true;
}
void init_DW()
{
valid[DW][AxFN] = true;
valid[DW][RulPref] = true;
valid[DW][RulSuff] = true;
valid[DW][AxKcomp] = true;
valid[DW][AxAcomp] = true;
}
void init_TW()
{
valid[TW][AxFN] = true;
valid[TW][AxB] = true;
valid[TW][AxB2] = true;
valid[TW][RulPref] = true;
valid[TW][RulSuff] = true;
valid[TW][AxKcomp] = true;
valid[TW][AxAcomp] = true;
}
void init_EW()
{
valid[EW][AxFN] = true;
valid[EW][AxB] = true;
valid[EW][AxB2] = true;
valid[EW][RulC3] = true;
valid[EW][RulPref] = true;
valid[EW][RulSuff] = true;
valid[EW][AxKcomp] = true;
valid[EW][AxAcomp] = true;
}
void init_RW()
{
valid[RW][AxFN] = true;
valid[RW][AxB] = true;
valid[RW][AxB2] = true;
valid[RW][RulC3] = true;
valid[RW][AxCt] = true;
valid[RW][AxTF] = true;
valid[RW][AxC2] = true;
valid[RW][AxC] = true;
valid[RW][RulPref] = true;
valid[RW][RulSuff] = true;
valid[RW][AxKcomp] = true;
valid[RW][AxAcomp] = true;
}
void init_LIN()
{
valid[LIN][AxFN] = true;
valid[LIN][AxB] = true;
valid[LIN][AxB2] = true;
valid[LIN][RulC3] = true;
valid[LIN][AxCt] = true;
valid[LIN][AxTF] = true;
valid[LIN][AxC2] = true;
valid[LIN][AxC] = true;
valid[LIN][RulPref] = true;
valid[LIN][RulSuff] = true;
valid[LIN][AxKcomp] = true;
valid[LIN][AxAcomp] = true;
valid[LIN][RulNec] = true;
valid[LIN][AxNec] = true;
valid[LIN][Ax4] = true;
valid[LIN][AxD] = true;
valid[LIN][AxNID] = true;
valid[LIN][AxNW] = true;
valid[LIN][AxNK] = true;
valid[LIN][AxNKI] = true;
default_orders[LIN] = lattices;
default_fragment[LIN][nec_exists] = true;
}
void init_T()
{
valid[T][AxFN] = true;
valid[T][AxB] = true;
valid[T][AxB2] = true;
valid[T][AxS] = true;
valid[T][AxX] = true;
valid[T][AxW] = true;
valid[T][AxW2] = true;
valid[T][AxWB] = true;
valid[T][AxRED] = true;
valid[T][RulPref] = true;
valid[T][RulSuff] = true;
valid[T][AxKcomp] = true;
valid[T][AxAcomp] = true;
valid[T][AxNW] = true;
}
void init_E()
{
valid[E][AxFN] = true;
valid[E][AxB] = true;
valid[E][AxB2] = true;
valid[T][AxS] = true;
valid[E][RulC3] = true;
valid[E][AxX] = true;
valid[E][AxW] = true;
valid[E][AxW2] = true;
valid[E][AxWB] = true;
valid[E][AxRED] = true;
valid[E][RulPref] = true;
valid[E][RulSuff] = true;
valid[E][AxKcomp] = true;
valid[E][AxAcomp] = true;
valid[E][AxNW] = true;
}
void init_R()
{
valid[R][AxFN] = true;
valid[R][AxB] = true;
valid[R][AxB2] = true;
valid[T][AxS] = true;
valid[R][RulC3] = true;
valid[R][AxCt] = true;
valid[R][AxTF] = true;
valid[R][AxC2] = true;
valid[R][AxC] = true;
valid[R][AxX] = true;
valid[R][AxW] = true;
valid[R][AxW2] = true;
valid[R][AxWB] = true;
valid[R][AxRED] = true;
valid[R][RulPref] = true;
valid[R][RulSuff] = true;
valid[R][AxKcomp] = true;
valid[R][AxAcomp] = true;
valid[R][AxNW] = true;
}
void init_CK()
{
valid[CK][AxFN] = true;
valid[CK][AxB] = true;
valid[CK][AxB2] = true;
valid[CK][RulC3] = true;
valid[CK][AxCt] = true;
valid[CK][AxTF] = true;
valid[CK][AxC2] = true;
valid[CK][AxC] = true;
valid[CK][AxK] = true;
valid[CK][AxK2] = true;
valid[CK][AxM] = true;
valid[CK][RulPref] = true;
valid[CK][RulSuff] = true;
valid[CK][AxKcomp] = true;
valid[CK][AxAcomp] = true;
valid[CK][AxNKI] = true;
valid[CK][AxNK] = true;
}
void init_S4()
{
valid[S4][AxFN] = true;
valid[S4][AxB] = true;
valid[S4][AxB2] = true;
valid[T][AxS] = true;
valid[S4][RulC3] = true;
valid[S4][AxX] = true;
valid[S4][AxW] = true;
valid[S4][AxW2] = true;
valid[S4][AxWB] = true;
valid[S4][AxRED] = true;
valid[S4][AxBA] = true;
valid[S4][AxSBA] = true;
valid[S4][AxK2] = true;
valid[S4][AxM] = true;
valid[S4][RulPref] = true;
valid[S4][RulSuff] = true;
valid[S4][AxKcomp] = true;
valid[S4][AxAcomp] = true;
valid[CK][AxNKI] = true;
}

125
src/axioms.h Normal file
View File

@ -0,0 +1,125 @@
/*
* axioms.h May 1993
*
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
/*
* First define the logics and axioms
*/
typedef enum {
Null_logic,
FD,
B,
DW,
TW,
EW,
RW,
LIN,
T,
E,
R,
CK,
S4,
LOGMAX
} LOGIC;
typedef enum {
AxNull,
RulPref,
RulSuff,
AxKcomp,
AxAcomp,
AxX,
AxBA,
AxSBA,
AxW2,
AxK,
AxK2,
AxM,
AxRED,
RulC3,
AxCt,
Axat,
AxTF,
AxB,
AxB2,
AxS,
AxC2,
AxW,
AxC,
AxWB,
AxFN,
RulNec,
AxNec,
AxD,
Ax4,
Ax5,
AxNID,
AxNand,
AxNW,
AxNK,
AxNKI,
AXMAX
} AXIOM;
/*
* There now follow the maximum sizes for the various
* logics and fragments.
*/
typedef struct {
boolean (*zero_test)();
void (*one_test)();
void (*two_test)();
void (*three_test)();
boolean (*many_test)();
} testlist;
GLOBAL char
logic_name[LOGMAX][8], /* Text names of known logics */
ax_string[AXMAX][64]; /* Text forms of known axioms */
GLOBAL boolean
taxiom[AXMAX], /* Tested axioms */
valid[LOGMAX][AXMAX]; /* Axioms valid in each logic */
GLOBAL testlist
TL[AXMAX]; /* Test functions for axioms */

568
src/dialog.c Normal file
View File

@ -0,0 +1,568 @@
/*
* dialog.c V2.1 (May 1993)
*
* The main interactive part of MaGIC.c. This module contains
* some of the procedures to be executed in response to menu
* selections, most of the others being in getjob.c.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "MaGIC.h"
/*
* The dialog function gets the job specifications from the
* user, setting up theJob accordingly. It returns 1 if
* option 'g' is selected from the menu, 0 if 'e' or 'q' is
* selected and n > 1 to change (in the parallel case) to n
* processes.
*/
int dialog(boolean batch, char *batchfile)
{
if ( batch ) return read_job( batchfile );
for(;;) switch( menu() ) {
case 'a': add_axioms(); break;
case 'b': bad_guy(); break;
case 'c': connective(); break;
case 'd': deletion(); break;
case 'e':
case 'q': return 0;
case 'f': fragment(); break;
case 'g': return 1;
case 'h': help(0); paws(); break;
case 'i': input_direct(); break;
case 'j': jump_condition(); break;
case 'k': job_defaults(batch); break;
case 'l': logic_choice(); break;
case 'm': print_version(); break;
case 'n':
case '#': return n_of_procs();
case 'o': order_change(); break;
case 'p': print_options(); break;
case 'r': read_job( 0 ); break;
case 's': store_job();
}
}
/*
* Menu first ensures that the fragment is consistent with the
* selected logic, axioms and badguy. Then it displays the
* currently selected job and the menu. Finally it takes the
* next user choice of menu selection and returns the character
* code for the next action.
*/
char menu()
{
char readin();
set_frag( true );
if ( xdialog ) {
printf("J\n");
outjob( stdout );
}
else display();
return readin("abcdefghijklmnopqrst#");
}
/*
* Readin returns the first character from stdin which matches
* one in its parameter, converting to lower case as required.
* It then discards all characters up to and including the next
* line feed. It is used mainly to get menu selections.
*/
char readin(char *str)
{
char ch;
int i;
fflush(stdout);
for(;;) {
fgets(answer,SLEN,stdin);
ch = 0;
for ( i = 0; answer[i]; i++ ) {
if ( isupper(ch = answer[i]) ) ch = tolower(ch);
if ( strchr(str,ch) ) return ch;
}
}
}
/*
* "Pause".
*/
void paws()
{
if ( xdialog ) fflush(stdout);
else {
printf("\n\n Now type RETURN to continue.........");
READLN;
}
}
/*
* Job_defaults is the initialisation procedure. It gets the
* initial choice of system and sets theJob to its defaults.
*/
void job_defaults( boolean batch )
{
int i, j;
zero = 0;
for ( i = 0; i < SYMBOLMAX; i++ ) {
strcpy( theJob->symtable[i].s, "" );
theJob->symtable[i].last = theJob->symtable[i].next = 0;
}
for ( i = 0; i < 3; i++ )
for ( j = 0; j < CMAX+8; j++ )
theJob->symbol[i][j] = 0;
theJob->symtab = 0;
newsymbol( "(", 0, 0 );
newsymbol( ")", 0, 0 );
newsymbol( ".", 0, 0 );
newsymbol( "a", 0, 0 );
newsymbol( "b", 0, 0 );
newsymbol( "t", theJob->symbol[0], 0 );
newsymbol( "f", theJob->symbol[0], 0 );
newsymbol( "T", theJob->symbol[0], 0 );
newsymbol( "F", theJob->symbol[0], 0 );
newsymbol( "~", theJob->symbol[1], 0 );
newsymbol( "!", theJob->symbol[1], 0 );
newsymbol( "?", theJob->symbol[1], 0 );
newsymbol( "o", theJob->symbol[2], 0 );
newsymbol( "&", theJob->symbol[2], 0 );
newsymbol( "v", theJob->symbol[2], 0 );
newsymbol( "->", theJob->symbol[2], 0 );
strcpy( theJob->data_dir, DATA_DIR );
for ( i = 0; i <= CMAX; i++ ) {
theJob->dcs[i] = 0;
if ( i < CMAX ) {
theJob->defcon[i] = 0;
theJob->concut[i] = false;
}
}
for ( i = 0; i < TMAX; i++ )
for ( j = 0; j < RTMAX; j++ )
theJob->croot[i][j] = theJob->proot[i][j] = 0;
theJob->failure = 0;
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 = 0;
theJob->maxtime = 0;
Sizmax = theJob->sizmax = SZ;
theJob->sizmax_ismax = true;
wff_initial();
if ( !batch ) {
if ( !noclear ) {
#ifdef __CYGWIN__
puts("\033[2J");
#else
system("clear");
#endif
}
theJob->logic = FD;
if ( !xdialog ) {
printf("\n This is MaGIC %s, finding matrices for", VERSION);
printf(" your favourite logic.\n");
printf(" Matrices come in all sizes up to %dx%d.\n",
SZ,SZ);
logic_choice();
}
}
}
/*
* Set_frag makes the selected fragment include all the used
* connectives and sets Sizmax accordingly.
*/
void set_frag( boolean set_sizmax )
{
int i, j;
for ( i = 0; i < AXMAX; i++ ) if ( theJob->axiom[i] ) {
if ( strchr(ax_string[i],'~') || strchr(ax_string[i],'f')
|| strchr(ax_string[i],'?') )
theJob->f_n = 1;
if ( strchr(ax_string[i],'t') || strchr(ax_string[i],'f') )
theJob->f_t = 1;
if ( strchr(ax_string[i],'&') || strchr(ax_string[i],'v') )
theJob->f_lat = 1;
if ( strchr(ax_string[i],'!') || strchr(ax_string[i],'?') )
theJob->f_nec = 1;
if ( i == AxK || i == AxK2 || i == AxTF )
theJob->f_T = theJob->f_t = 1;
}
if ( theJob->f_n && valid[theJob->logic][AxC] )
theJob->f_fus = 1;
for ( i = 0; theJob->croot[i][0]; i++ ) {
for ( j = 0; theJob->croot[i][j]; j++ )
if ( theJob->croot[i][j] != ABSURD )
check_frag(theJob->croot[i][j]);
for ( j = 0; theJob->proot[i][j]; j++ )
if ( theJob->proot[i][j] != TRIVIAL )
check_frag(theJob->proot[i][j]);
}
if ( theJob->failure )
check_frag(theJob->failure);
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->defcon[i] != PRIMITIVE )
check_frag(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;
F_N =
((theJob->f_n && valid[theJob->logic][AxFN])
|| theJob->axiom[AxFN]);
afx =
((valid[theJob->logic][RulPref] && valid[theJob->logic][RulSuff])
|| (theJob->axiom[RulPref] && theJob->axiom[RulSuff]));
if ( set_sizmax ) {
if ( !(theJob->f_lat || theJob->f_n) )
Sizmax = theJob->f_t? S_pot: S_pO;
else if ( !theJob->f_lat )
Sizmax = theJob->f_t? S_pont: S_poN;
else if ( !theJob->distrib )
Sizmax = theJob->f_n? S_ln: S_lat;
else if ( !theJob->totord )
Sizmax = ((theJob->f_n && theJob->logic==S4)
|| theJob->axiom[AxBA])? S_ba:
(theJob->f_n? S_dln: S_dlat);
else Sizmax = theJob->f_n? S_Ton: S_to;
if ( theJob->sizmax > Sizmax || theJob->sizmax_ismax )
theJob->sizmax = Sizmax;
}
}
/*
* This function adds to the fragment any connectives which
* occur in the given formula. It attends to the main
* connective only, calling itself recursively to deal with
* the subformulae.
*/
void check_frag(int x)
{
if (!x) return;
if (!theJob->form[x].sym->s[1]) {
switch(theJob->form[x].sym->s[0]) {
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 '?': theJob->f_n = 1;
case '!': theJob->f_nec = 1; break;
case '&':
case 'v': theJob->f_lat = 1;
}
}
check_frag(theJob->form[x].lsub);
check_frag(theJob->form[x].rsub);
}
/*
* Print_axiom just writes out axiom #x on stream f.
*/
void print_axiom(FILE *f, AXIOM x)
{
fprintf(f, "%s", ax_string[x]);
}
/*
* Display shows the current choices and the menu.
*/
void display()
{
if ( !noclear ) {
#ifdef __CYGWIN__
puts("\033[2J");
#else
system("clear");
#endif
}
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\n");
printf(" M)aGIC N)o. Procs O)rder P)rint Opts\n");
printf(" Q)uit R)ead S)tore ");
}
/*
* Disp is the function to print an account of the current
* contents of theJob. It is to have verbose and terse modes.
*/
void disp(FILE *f)
{
AXIOM ax;
int i, j;
boolean b;
#ifdef PARALLEL
fprintf(f, "\n Parallel MaGIC running %d out of %d processes\n",
gm->nprocs, PARALLEL);
#endif
if ( theJob->totord && default_orders[theJob->logic] != total_orders )
fprintf(f, "\n Logic:%8cT%s", ' ', logic_name[theJob->logic]);
else if ( theJob->distrib &&
default_orders[theJob->logic] != distributive_lattices )
fprintf(f, "\n Logic:%8cD%s", ' ', logic_name[theJob->logic]);
else if ( !theJob->distrib &&
default_orders[theJob->logic] != lattices )
fprintf(f, "\n Logic:%8cL%s", ' ', logic_name[theJob->logic]);
else fprintf(f, "\n Logic:%8c%s", ' ', logic_name[theJob->logic]);
b = false;
for ( ax = AxNull+1; ax < AXMAX; ax++ ) if ( theJob->axiom[ax] ) {
if ( !b ) {
b = true;
fprintf(f, "\n\n Plus: ");
}
else fprintf(f, "\n ");
print_axiom(f,ax);
}
for ( i = 0; theJob->croot[i][0]; i++ ) {
if ( i ) fprintf(f, "\n ");
else fprintf(f, "\n\n Extra: ");
for ( j = 0; theJob->proot[i][j]; j++ ) {
if ( j ) fprintf(f, ", ");
if ( theJob->proot[i][j] != TRIVIAL )
outfml(theJob->proot[i][j],
theJob->proot[i][j],f);
}
if ( theJob->proot[i][0] != TRIVIAL ) fprintf(f, " / ");
for ( j = 0; theJob->croot[i][j]; j++ ) {
if ( j ) fprintf(f, ", ");
if ( theJob->croot[i][j] != ABSURD )
outfml(theJob->croot[i][j],
theJob->croot[i][j],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_nec ) {
fprintf(f, ", !");
if ( theJob->f_n ) fprintf(f, ", ?");
}
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 if ( !theJob->defcon[1] ) fprintf(f, "\n\n Definition: ");
else fprintf(f, "\n\n Definitions:");
if ( !theJob->adicity[i] )
fprintf(f, " %s ", theJob->dcs[i]->s);
else if ( theJob->adicity[i] == 1 ) {
if ( theJob->dcs[i]->s[1] )
fprintf(f, " %s a ", theJob->dcs[i]->s);
else fprintf(f, " %sa ", theJob->dcs[i]->s);
}
else fprintf(f, " a %s b ", theJob->dcs[i]->s);
if ( theJob->defcon[i] == PRIMITIVE ) {
fprintf(f, "Primitive");
if ( theJob->concut[i] ) fprintf(f, " (cut)");
}
else outfml(theJob->defcon[i], theJob->defcon[i],f);
}
if ( theJob->failure ) {
fprintf(f, "\n\n Fail: ");
outfml(theJob->failure, 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 seconds\n or ", theJob->maxtime);
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);
}
/*
* The Help facility is extremely primitive. It simply transfers
* the contents of a short file to stdout. The parameter codes
* the place in the program from which the Help call was made.
*/
void help(helpcode x)
{
switch( x ) {
case MEN:
put_out("MEN");
break;
case WFF1:
case WFF2:
put_out("WFF");
break;
case FDL:
put_out("FDL");
break;
case BTW:
put_out("BTW");
break;
case LOG:
put_out("LOG");
break;
case OUT:
put_out("OUT");
break;
case HELPMAX:
break;
}
}
/*
* This is essentially a macro for Help (above).
* It prepends the data directory name, appends ".show"
* and does the file transfer.
*
* If we are in terse mode, nothing happens because the
* front end xmagic has its own Help routine.
*/
void put_out(char *f_nm)
{
FILE *f1;
char s[100];
if ( !noclear ) {
#ifdef __CYGWIN__
puts( "\033[2J" );
strcpy(s,DATA_DIR);
strcat(s,f_nm);
strcat(s,".show");
if ( (f1 = fopen(s,"r")) == NULL ) {
printf("Cannot open %s.",s);
}
else {
while (fgets(s,80,f1) != NULL) {
printf("%s",s);
}
fclose(f1);
}
#else
sprintf(s,"clear; more %s%s.show", DATA_DIR, f_nm);
system( s );
#endif
}
}

11
src/embedded.c Normal file
View File

@ -0,0 +1,11 @@
#include "RM.h"
#include "hmi.h"
int main(int argc, char *argv[])
{
if (argc != 2)
Abort("synopsis: embedding <file of algebras>",-1);
relatemats(embedding, argv[1], "subalgebra");
return 0;
}

1298
src/getjob.c Normal file

File diff suppressed because it is too large Load Diff

329
src/hmi.c Normal file
View File

@ -0,0 +1,329 @@
#include "RM.h"
#include "hmi.h"
/*
* Is there a homomorphic image of m1 in m2?
*/
int homo(MATRIX *m1, MATRIX *m2)
{
int h[SZ];
int x,y;
/*
* First check that the fragments agree
*/
for (x=NEG; x<FRAGMAX; x++)
if (m1->fragment[x] != m2->fragment[x])
return 0;
FORALLCON(m1,x);
FORALLCON(m2,y);
if (x != y )
return 0;
/*
* Now initialise to "undefined" and ask for a solution
*/
for (x=0; x<SZ; x++)
h[x] = -1;
return homomorphism(m1,m2,h);
}
/*
* Recursively generate a homomorphism if there is one
*/
int homomorphism(MATRIX *m1, MATRIX *m2, int h[])
{
int x,y;
int localh[SZ];
copy_h(m1,h,localh);
FORALL(m1,x)
if (h[x] < 0) {
FORALL(m2,y) {
copy_h(m1,h,localh);
localh[x] = y;
if (propagated(m1,m2,localh) &&
homomorphism(m1,m2,localh)) {
copy_h(m1,localh,h);
return 1;
}
}
return 0;
}
copy_h(m1,localh,h);
return 1;
}
/*
* Is there a non-trivial homomorphic image of m1 in m2?
*/
int nt_homo(MATRIX *m1, MATRIX *m2)
{
int h[SZ];
int x,y;
/*
* First check that the fragments agree
*/
for (x=NEG; x<FRAGMAX; x++)
if (m1->fragment[x] != m2->fragment[x])
return 0;
FORALLCON(m1,x);
FORALLCON(m2,y);
if (x != y )
return 0;
/*
* Now initialise to "undefined" and ask for a solution
*/
for (x=0; x<SZ; x++)
h[x] = -1;
return nt_homomorphism(m1,m2,h);
}
/*
* Recursively generate a non-trivial homomorphism if there is one
*/
int nt_homomorphism(MATRIX *m1, MATRIX *m2, int h[])
{
int x,y;
int localh[SZ];
copy_h(m1,h,localh);
FORALL(m1,x)
if (h[x] < 0) {
FORALL(m2,y) {
copy_h(m1,h,localh);
localh[x] = y;
if (propagated(m1,m2,localh) &&
nt_homomorphism(m1,m2,localh)) {
copy_h(m1,localh,h);
return 1;
}
}
return 0;
}
FORALL(m1,x)
FORALL(m1,y)
if (x < y && localh[x] != localh[y]) {
copy_h(m1,localh,h);
return 1;
}
return 0;
}
/*
* Is m1 [isomorphic to] a subalgebra of m2?
*/
int embedding(MATRIX *m1, MATRIX *m2)
{
int h[SZ];
int x,y;
/*
* First check that the fragments agree and the sizes are OK
*/
for (x=NEG; x<FRAGMAX; x++)
if (m1->fragment[x] != m2->fragment[x])
return 0;
FORALLCON(m1,x);
FORALLCON(m2,y);
if (x != y )
return 0;
if (m1->siz > m2->siz)
return 0;
/*
* Now initialise to "undefined" and ask for a solution
*/
for (x=0; x<SZ; x++)
h[x] = -1;
return injected_into(m1,m2,h);
}
/*
* Recursively generate an injective homomorphism if there is one
*/
int injected_into(MATRIX *m1, MATRIX *m2, int h[])
{
int x,y;
int localh[SZ];
copy_h(m1,h,localh);
FORALL(m1,x)
if (h[x] < 0) {
FORALL(m2,y) {
copy_h(m1,h,localh);
localh[x] = y;
if (propagated(m1,m2,localh) &&
injected_into(m1,m2,localh)) {
copy_h(m1,localh,h);
return 1;
}
}
return 0;
}
FORALL(m1,x) FORALL(m1,y)
if (x < y && localh[x] == localh[y])
return 0;
copy_h(m1,localh,h);
return 1;
}
/*
* Is there a (surjective) homomorphism from m1 onto m2?
*/
int epimorphic_image(MATRIX *m1, MATRIX *m2)
{
int h[SZ];
int x,y;
/*
* First check that the fragments agree and the sizes are OK
*/
for (x=NEG; x<FRAGMAX; x++)
if (m1->fragment[x] != m2->fragment[x])
return 0;
FORALLCON(m1,x);
FORALLCON(m2,y);
if (x != y )
return 0;
if (m1->siz < m2->siz)
return 0;
/*
* Now initialise to "undefined" and ask for a solution
*/
for (x=0; x<SZ; x++)
h[x] = -1;
return mapped_onto(m1,m2,h);
}
/*
* Recursively generate a surjective homomorphism if there is one
*/
int mapped_onto(MATRIX *m1, MATRIX *m2, int h[])
{
int x,y;
int invh[SZ];
int localh[SZ];
copy_h(m1,h,localh);
FORALL(m1,x)
if (h[x] < 0) {
FORALL(m2,y) {
copy_h(m1,h,localh);
localh[x] = y;
if (propagated(m1,m2,localh) &&
mapped_onto(m1,m2,localh)) {
copy_h(m1,localh,h);
return 1;
}
}
return 0;
}
FORALL(m2,y)
invh[y] = -1;
FORALL(m1,x)
invh[localh[x]] = x;
FORALL(m2,y)
if (invh[y] < 0)
return 0;
copy_h(m1,localh,h);
return 1;
}
void copy_h(MATRIX *m, int source[], int dest[])
{
int x;
FORALL(m,x)
dest[x] = source[x];
}
int propagated(MATRIX *m1, MATRIX *m2, int h[])
{
int localh[SZ];
int x;
for (x=0; x<SZ; x++)
localh[x] = h[x];
if (m1->fragment[NEG] &&
!monprop(m1,m1->neg,m2->neg,localh))
return 0;
if (m1->fragment[BOX] &&
!monprop(m1,m1->box,m2->box,localh))
return 0;
FORALLCON(m1,x)
if (m1->adicity[x] == 1 &&
!monprop(m1,m1->monadic[x],m2->monadic[x],localh))
return 0;
if (!dyprop(m1,m1->C,m2->C,localh))
return 0;
if (m1->fragment[FUS] &&
!dyprop(m1,m1->fus,m2->fus,localh))
return 0;
if (m1->fragment[LAT]) {
if (!dyprop(m1,m1->K,m2->K,localh))
return 0;
if (!dyprop(m1,m1->A,m2->A,localh))
return 0;
}
FORALLCON(m1,x)
if (m1->adicity[x] == 2 &&
!dyprop(m1,m1->dyadic[x],m2->dyadic[x],localh))
return 0;
FORALL(m1,x)
h[x] = localh[x];
return 1;
}
int monprop(MATRIX *m1, int a[], int b[], int lh[])
{
int x;
FORALL(m1,x)
if (lh[x] >= 0 && lh[a[x]] != b[lh[x]]) {
if (lh[a[x]] < 0)
lh[a[x]] = b[lh[x]];
else
return 0;
}
return 1;
}
int dyprop(MATRIX *m1, int a[][SZ], int b[][SZ], int lh[])
{
int x,y;
FORALL(m1,x)
if (lh[x] >= 0)
FORALL(m1,y)
if (lh[y] >= 0 && lh[a[x][y]] != b[lh[x]][lh[y]]) {
if (lh[a[x][x]] < 0)
lh[a[x][y]] = b[lh[x]][lh[y]];
else return 0;
}
return 1;
}

17
src/hmi.h Normal file
View File

@ -0,0 +1,17 @@
/*
* Function prototypes for homomorphism testers
*/
int homo(MATRIX *m1, MATRIX *m2);
int homomorphism(MATRIX *m1, MATRIX *m2, int h[]);
int nt_homo(MATRIX *m1, MATRIX *m2);
int nt_homomorphism(MATRIX *m1, MATRIX *m2, int h[]);
int embedding(MATRIX *m1, MATRIX *m2);
int injected_into(MATRIX *m1, MATRIX *m2, int h[]);
int epimorphic_image(MATRIX *m1, MATRIX *m2);
int mapped_onto(MATRIX *m1, MATRIX *m2, int h[]);
void copy_h(MATRIX *m, int source[], int dest[]);
int propagated(MATRIX *m1, MATRIX *m2, int h[]);
int monprop(MATRIX *m1, int a[], int b[], int lh[]);
int dyprop(MATRIX *m1, int a[][SZ], int b[][SZ], int lh[]);

11
src/homomorphic.c Normal file
View File

@ -0,0 +1,11 @@
#include "RM.h"
#include "hmi.h"
int main(int argc, char *argv[])
{
if (argc != 2)
Abort("synopsis: homomorphic <file of algebras>",-1);
relatemats(homo, argv[1], "Homomorphism");
return 0;
}

9
src/image.c Normal file
View File

@ -0,0 +1,9 @@
#include "RM.h"
#include "hmi.h"
main(int argc, char *argv[])
{
if (argc != 2)
Abort("synopsis: embedding <file of algebras>",-1);
relatemats(epimorphic_image, argv[1], "MapsOnto");
}

528
src/isom.c Normal file
View File

@ -0,0 +1,528 @@
/*
* isom.c V2.1 (May 1993)
*
* This contains all the procedures pertaining to the
* elimination of isomorphic copies from the output of
* matrix-generating programs such as MaGIC.c.
*
* It is assumed that the external variables siz, neg[],
* ord[][], des, C[][] and box[] are available and that
* this module is called, presumably by the accept()
* function, every time a new matrix is found. If there
* are any isomorphic copies, the integer isoms is
* incremented.
*
* There are two parts to all this. First come some
* procedures to find the acceptable permutations on the
* current siz, neg[], ord[][] and des. Then there are
* the routines to be executed on discovery of a new
* matrix.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "MaGIC.h"
#define firstopen (tr_par.vlength - tr_par.vlength)
static boolean
manyisoms; /* Not all isoms have been stacked */
static ism
nextisom; /* First free isom in the list */
static int
lastisovect; /* Last unfree segment of isolist */
static int
isoused; /* Number of isoms used this case */
static char
shvector[V_LENGTH]; /* The variable part of thisvector */
/*
* This initialisation function just sets up perm.
*/
void perm_initial()
{
perm = (PRM*) malloc(sizeof(PRM));
perm->h[0] = -1;
perm->pup = 0;
isoused = ISOMAX;
}
/*
* Setperm finds the automorphisms which do not disturb
* ord, N or des. The bulk of it is a crude test-and-change.
*/
void setperm()
{
int i, j;
int p_poss[SZ][SZ],
p_used[SZ],
sh[SZ],
single[SZ];
PRM *prmptr;
for (i=0; i<isoused; i++) {
istak[i].icv = (i? 0: isolist);
istak[i].left = istak[i].right = 0;
if ( !i || i == ISOMAX-1 ) istak[i].parent = 0;
else istak[i].parent = istak+i+1;
}
isoused = 1;
nextisom = istak+1;
for ( i = 0; i < V_LENGTH; i++ ) thisvector[i] = -1;
manyisoms = false;
lastisovect = 0;
istak[0].icv[0] = SZ;
for ( prmptr = perm; prmptr->h[0] >= 0; prmptr = prmptr->pup )
prmptr->h[0] = -1;
FORALL(i) FORALL(j) {
p_poss[i][j] = (lower_than(i)==lower_than(j)) &&
(higher_than(i)==higher_than(j));
if ( theJob->f_n &&
(( N[i]==i && N[j]!=j ) || ( N[j]==j && N[i]!=i )))
p_poss[i][j] = 0;
}
FORALL(i) {
if ( theJob->f_t ) {
if ( i != des )
p_poss[des][i] = p_poss[i][des] = 0;
if ( theJob->f_n && i != N[des] )
p_poss[N[des]][i] = p_poss[i][N[des]] = 0;
}
else if ( desig[i] )
FORALL(j) if ( !desig[j] )
p_poss[i][j] = p_poss[j][i] = 0;
p_used[i] = 1; sh[i] = i;
single[i] = 1;
FORALL(j)
if ( i != j && p_poss[i][j] )
single[i] = 0;
}
goto CHANGE; /* !!! */
PTEST: FORALL(i) FORALL(j)
if ( ord[i][j] != ord[sh[i]][sh[j]] )
goto CHANGE;
newperm(sh);
CHANGE: FORALL(i)
if ( !(( theJob->f_n && i < N[i] ) || single[i] )) {
p_used[sh[i]] = 0;
if ( theJob->f_n )
p_used[sh[N[i]]] = 0;
for ( j = sh[i]-1; j >= 0; j-- )
if ( p_poss[i][j] && !p_used[j] ) {
sh[i] = j;
if ( theJob->f_n )
sh[N[i]] = N[j];
p_used[j] = 1;
if ( theJob->f_n )
p_used[N[j]] = 1;
for (i--; i >= 0 && !(theJob->f_n && i < N[i]); i--)
if ( !single[i] ) {
for (j = siz; j; j-- )
if ( p_poss[i][j] && !p_used[j] ) {
sh[i] = j;
if ( theJob->f_n )
sh[N[i]] = N[j];
p_used[j] = 1;
if ( theJob->f_n)
p_used[N[j]] = 1;
break;
}
}
goto PTEST;
}
}
}
/*
* How many elements are below x?
*/
int lower_than(int x)
{
int i;
int j = 0;
for ( i=0; i < x; i++ ) j += ord[i][x];
return j;
}
/*
* Similarly, how many are above?
*/
int higher_than(int x)
{
int i;
int j = 0;
for ( i = siz; i > x; i-- ) j += ord[x][i];
return j;
}
/*
* Add a permutation to the perm list.
*/
void newperm(int *vec)
{
int i;
PRM *p;
for ( p = perm; p->pup && p->h[0] >= 0; p = p->pup) ;
if ( !p->pup ) {
p->pup = (PRM*) malloc(sizeof(PRM));
p->pup->pup = 0;
p->pup->h[0] = -1;
}
FORALL(i) p->h[i] = *(vec+i);
}
/*
* That completes the first half, concerned with generating
* the list of allowable permutations. Now, assuming that
* list given, deal with isomorphisms between good matrices.
*
* Isomorphic usually returns 1 if the matrix was already in the
* isomorphism tree below ptr, snipping it out as it does so
* (since it is not going to be generated twice). If not,
* all the isomorphic copies which lie within the search space
* are generated and added to the tree.
*
* If the flag "manyisoms" is set, indicating that some isomorphic
* copies of earlier things have not been recorded because of lack
* of space, then the copies of the current matrix, instead of
* being added directly to the tree, are compared with the current
* matrix to see whether one of them preceeds it. If the current
* matrix is the first in its isomorphism class, its copies are
* inserted in the tree. If not, the temporary store is emptied
* and 1 returned.
*
* The flag "manyisoms" is raised if the number of stored copies
* gets to equal ISOMAX, and lowered at the start of each search.
*/
boolean isomorphic(ism ptr, trs T)
{
int i, j;
boolean do_add = false;
if ( !tr_par.vlength ) return false;
j = 0;
for ( i = 0; i < tr_par.vlength; i++ )
if ( T->coinorder[i] >= firstopen )
shvector[j++] = thisvector[i];
for ( i = 0; i < tr_par.vlength; i++ ) {
if ( shvector[i] < ptr->icv[i] ) {
if ( ptr->left )
return isomorphic(ptr->left,T);
do_add = true;
break;
}
if ( shvector[i] > ptr->icv[i] ) {
if ( ptr->right )
return isomorphic(ptr->right,T);
do_add = true;
break;
}
}
if ( do_add ) {
if ( isomorphic_anyhow(T) ) {
isoms2++;
return true;
}
add_isoms( T );
return false;
}
snip(ptr);
isoms++;
return true;
}
/*
* Snip removes a node from the isom tree.
* The action is slightly different if the node is the root.
*/
void snip(ism p)
{
ism q;
int i;
if ( p == istak ) {
if ( !p->left && !p->right ) {
*(p->icv) = SZ;
}
else {
if ( p->right )
for ( q = p->right; q->left; q = q->left ) ;
else for ( q = p->left; q->right; q = q->right ) ;
for ( i = 0; i < tr_par.vlength; i++ )
p->icv[i] = q->icv[i];
snip(q);
}
}
else {
if ( !p->left )
subst(p,p->right);
else if ( !p->right )
subst(p,p->left);
else {
for ( q = p->right; q->left; q = q->left ) ;
for ( i = 0; i < tr_par.vlength; i++ )
p->icv[i] = q->icv[i];
subst(q,q->right);
}
}
}
/*
* A subroutine of the above, this moves p2 into the place
* of p1, marking p1 as defunct so that it can be re-used.
*/
void subst(ism p1, ism p2)
{
if ( p2 )
p2->parent = p1->parent;
if ( p1->parent->left == p1 )
p1->parent->left = p2;
else p1->parent->right = p2;
*(p1->icv) = SZ;
p1->parent = nextisom;
nextisom = p1;
}
/*
* Isomorphic_anyhow if manyisoms and this is not the first
* in its isomorphism class. This function and add_isoms are
* very similar and should probably be amalgamated at some stage.
*/
boolean isomorphic_anyhow(trs T)
{
int i, j, k;
char ac[V_LENGTH];
PRM *aptr;
if ( !manyisoms ) return false;
for ( aptr = perm; aptr->h[0] >= 0; aptr = aptr->pup ) {
FORALL(i) FORALL(j)
ac[impindex[(int)aptr->h[i]][(int)aptr->h[j]]] = aptr->h[C[i][j]];
FORALL(i)
ac[boxindex[(int)aptr->h[i]]] = aptr->h[box[i]];
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->defcon[i] == PRIMITIVE )
switch ( theJob->adicity[i] ) {
case 0:
ac[ucc0[i]] = aptr->h[nulladic[i]];
break;
case 1:
FORALL(j)
ac[ucc1[i][(int)aptr->h[j]]] =
aptr->h[monadic[i][j]];
break;
case 2:
FORALL(j) FORALL(k)
ac[ucc2[i][(int)aptr->h[j]][(int)aptr->h[k]]] =
aptr->h[dyadic[i][j][k]];
}
for ( i = firstopen; i < tr_par.vlength; i++ )
if ( thisvector[T->inorder[i]] != ac[T->inorder[i]] ) {
if ( thisvector[T->inorder[i]] > ac[T->inorder[i]] )
return true;
break;
}
}
return false;
}
/*
* Add_isoms, called from isomorphic, generates all the non-
* trivial automorphic copies of the matrix got by applying
* allowable permutations and puts them into the "isom" tree.
*/
void add_isoms(trs T)
{
int i, j, k, same;
char ac[V_LENGTH], shac[V_LENGTH];
PRM *aptr;
for ( aptr = perm;
aptr->h[0] >= 0 && nextisom &&
lastisovect < ISLMAX - tr_par.vlength;
aptr = aptr->pup ) {
FORALL(i) FORALL(j)
ac[impindex[(int)aptr->h[i]][(int)aptr->h[j]]] = aptr->h[C[i][j]];
if ( theJob->f_nec )
FORALL(i)
ac[boxindex[(int)aptr->h[i]]] = aptr->h[box[i]];
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->defcon[i] == PRIMITIVE )
switch ( theJob->adicity[i] ) {
case 0: ac[ucc0[i]] = aptr->h[nulladic[i]];
break;
case 1:
FORALL(j)
ac[ucc1[i][(int)aptr->h[j]]] =
aptr->h[monadic[i][j]];
break;
case 2:
FORALL(j) FORALL(k)
ac[ucc2[i][(int)aptr->h[j]][(int)aptr->h[k]]] =
aptr->h[dyadic[i][j][k]];
}
same = true;
j = 0;
for ( i = 0; i < tr_par.vlength; i++ )
if ( T->coinorder[i] >= firstopen ) {
shac[j] = ac[i];
if ( shac[j] != shvector[j] ) same = false;
j++;
}
if ( !same ) {
if ( *((*(istak)).icv) != SZ ) {
add_this(shac,istak);
if ( !nextisom || lastisovect >= ISLMAX - tr_par.vlength )
manyisoms = true;
}
else
for ( i = 0; i < tr_par.vlength; i++ )
(*(istak)).icv[i] = shac[i];
}
}
}
/*
* If the matrix mat is not in the i_tree, put it in and return true.
* If it is there already, return false.
*/
boolean add_this(char mat[], ism i_tree)
{
int i;
for ( i = 0; i < tr_par.vlength; i++ )
if ( mat[i] < i_tree->icv[i] ) {
if ( i_tree->left )
return add_this(mat,i_tree->left);
i_tree->left = tack_on(i_tree,mat);
return true;
}
else if ( mat[i] > i_tree->icv[i] ) {
if ( i_tree->right )
return add_this(mat,i_tree->right);
i_tree->right = tack_on(i_tree,mat);
return true;
}
return false;
}
/*
* Extend the isom tree with a new entry. Its parent is
* p and its matrix is mat.
* If there is no free ism in the stack, crash gracefully.
*/
ism tack_on(ism p, char mat[])
{
ism pi;
int i;
pi = nextisom;
if ( !pi ) skipout("Isomorphism stack overflow",SKIP);
if ( pi >= istak+isoused ) isoused++;
nextisom = pi->parent;
pi->left = pi->right = 0;
pi->parent = p;
lastisovect += tr_par.vlength;
pi->icv = isolist+lastisovect;
for ( i = 0; i < tr_par.vlength; i++ )
pi->icv[i] = mat[i];
return pi;
}

835
src/logic_io.c Normal file
View File

@ -0,0 +1,835 @@
/*
* logic_io.c V2.1 (May 1993)
*
* This file contains the routines for reading in setups
* and for making the appropriate initialisations. It
* also contains the procedures for printing any matrices
* found.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1992 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "MaGIC.h"
/*
* First the semi-trivial function cluster to control the loop
*/
int newsiz()
{
N[0] = 0;
return( got_siz()? (theJob->f_n? newneg(): neword()): 0 );
}
int newneg()
{
return( got_neg()? neword(): newsiz() );
}
int neword()
{
return( got_ord()? newdes(): (theJob->f_n? newneg(): newsiz()) );
}
int newdes()
{
return( got_des()? 1: neword() );
}
/*
* Sep is a subroutine to print the separator "-1" if the
* chosen format is UGLY. The parameter is the counter for
* the appropriate level.
*/
void sep(int *x)
{
if ( *x ) {
if ( theJob->tty_out==UGLY ) printf(" -1\n");
if ( theJob->fil_out==UGLY ) fprintf(outfil, " -1\n");
*x = 0;
}
}
/*
* Next_bit returns 1 or 0 depending on the next bit in the
* input file. This is to allow very compressed data to be used.
*/
int next_bit()
{
if ( input_bit == 8 ) {
if ( read(infil,&buffa,1) < 1 ) return 0;
input_bit = 0;
}
if ( buffa & ((char)1 << input_bit++) ) return 1;
return 0;
}
/*
* Return the new size, or 0 if there isn't one.
* The values of T and F are incidentally set at this stage.
*/
int got_siz()
{
if ( theJob->f_n )
sep( &negno );
else sep( &ordno );
if ( next_bit() ) siz++; else siz = 0;
if ( tr_par.done || siz>=theJob->sizmax ) siz = 0;
if ( theJob->f_T ) theJob->form[VMAX+2].val = siz;
if ( theJob->f_F ) theJob->form[VMAX+3].val = 0;
return siz;
}
/*
* Set the next negation table.
* Return 1 if successful, 0 if not.
*/
boolean got_neg()
{
int i;
sep(&ordno);
if ( tr_par.done || !next_bit() ) return false;
if ( N[0] ) {
FORaLL(i)
if ( N[i] > i ) break;
N[N[i]] = N[i];
N[i] = i;
}
else FORALL(i) N[i] = siz-i;
return true;
}
/*
* Read the next order table.
* Return 1 if successful, 0 if not.
* At this stage, decide which elements are maximal, define
* lattice meet and join if they exist, and set up cc, the
* index to the communication vector of transref.
*/
boolean got_ord()
{
int i, j, k;
sep( &desno );
if ( tr_par.done || !next_bit() ) return false;
FORALL(i) FORALL(j)
if ( i < j ) ord[i][j] = next_bit();
else ord[i][j] = (i == j);
FORALL(i) {
maximal[i] = 1;
for ( j = i+1; j <=siz; j++ ) maximal[i] *= !ord[i][j];
}
if ( theJob->f_lat ) {
FORALL(i) {
for ( j = i; j <= siz; j++ ) {
for (k = j; !(ord[i][k] && ord[j][k]); k++) ;
A[i][j] = A[j][i] = k;
for (k = i; !(ord[k][i] && ord[k][j]); k--) ;
K[i][j] = K[j][i] = k;
}
}
}
set_up_cc();
return true;
}
/*
* Read the next choice of designated values, or of least
* designated value if t is defined.
* Return 1 on success, 0 on failure.
*
* The set of designated (true) values can be calculated
* here, and the values of t and f filled in.
*/
boolean got_des()
{
int i;
if ( matsum ) {
if ( theJob->tty_out == SUMMARY ) {
printf(" %d matri%s",
matsum, (matsum>1? "ces": "x"));
fflush(stdout);
}
if ( theJob->fil_out == SUMMARY )
fprintf(outfil, " %d matri%s",
matsum, (matsum>1? "ces": "x"));
matsum = 0;
}
sep( &matno );
if ( tr_par.done || !next_bit() ) return false;
FORALL(i) desig[i] = next_bit();
for ( des = 0; !desig[des]; des++ ) ;
for ( undes = siz; desig[undes]; undes-- ) ;
if ( theJob->f_t ) {
theJob->form[VMAX].val = des;
if ( theJob->f_n ) theJob->form[VMAX+1].val = N[des];
}
return true;
}
/*
======================================================================
*/
/*
* That's the end of the input routines. Now for the output ones.
*
* Mat_print is called from the tester with each good matrix.
*/
void mat_print()
{
int i, j;
boolean b;
firstchange = -1;
for ( i = 0; i < tr_par.vlength; i++ ) {
if ( thisvector[i] != thatvector[i] ) firstchange = i;
thatvector[i] = thisvector[i];
}
if ( !matno ) firstchange = tr_par.vlength;
if ( firstchange < 0 ) skipout("Same matrix found twice",SKIP);
j = -1;
for ( i = 0; theJob->dcs[i]; i++ );
for (--i; i >= 0; i--)
if ( theJob->defcon[i] == PRIMITIVE ) {
switch( theJob->adicity[i] ) {
case 0:
newmatplus( j, ucc0[i] );
break;
case 1:
newmatplus( j, ucc1[i][0] );
break;
case 2:
newmatplus( j, ucc2[i][0][0] );
}
j = i;
}
if ( theJob->f_nec ) {
newmatplus( j, firstbox );
if ( firstchange >= firstarrow ) sep(&boxno);
}
else newmatplus( j, firstarrow );
b = true;
for ( i = 0; theJob->dcs[i]; i++ );
for ( --i; i>=0; i-- )
if ( theJob->defcon[i] == PRIMITIVE )
if ( matplus[i]++ ) {
b = false;
break;
}
if ( b && theJob->f_nec )
if ( boxno++ ) b = false;
if ( b )
if ( !matno++ )
if ( !desno++ )
if ( !ordno++ )
if ( theJob->f_n )
negno++;
good++;
matsum++;
if ( theJob->tty_out ) printup(stdout,theJob->tty_out);
if ( theJob->fil_out ) printup(outfil,theJob->fil_out);
}
/*
* Essentially a macro for the above:
*/
void newmatplus(int x, int y)
{
if ( firstchange >= y && x >= 0 ) sep(matplus+x);
}
/*
* Printing the new size is part of printing the new negation
* table or, if negation is not defined, the new order table.
* The parameter x is the output mode, and f the destination.
*/
void siz_print(FILE *f, output_style x)
{
switch(x) {
case UGLY:
fprintf(f, " %d\n", siz);
break;
case PRETTY:
fprintf(f, "\n\n\n\n Size: %d\n", siz+1);
break;
case SUMMARY:
fprintf(f, "\n\n\n Size: %d", siz+1);
case NONE:
break;
}
}
/*
* Printing the new negation table is part of printing the new
* order table.
* The parameter x is the output mode, and f the destination.
*/
void neg_print(FILE *f, output_style x)
{
int i;
if ( negno == 1 ) siz_print(f,x);
switch(x) {
case UGLY:
FORALL(i) fprintf(f, " %d", N[i]);
fprintf(f, "\n");
break;
case PRETTY:
fprintf(f, "\n\n Negation table ");
pretty_negno(f);
fprintf(f, "\n\n a |");
FORALL(i) fprintf(f, " %x", i);
fprintf(f, "\n ---+");
FORALL(i) fprintf(f, "--");
fprintf(f, "\n ~a |");
FORALL(i) fprintf(f, " %x", N[i]);
fprintf(f, "\n");
break;
case SUMMARY:
fprintf(f, "\n\n Negation ");
pretty_negno(f);
case NONE:
break;
}
}
/*
* Printing the new order table is part of printing the new
* choice of designated values.
* The parameter x is the output mode, and f the destination.
*/
void ord_print(FILE *f, output_style x)
{
int i, j;
if ( ordno == 1 ) {
if ( theJob->f_n ) neg_print(f,x);
else siz_print(f,x);
}
switch(x) {
case NONE:
break;
case UGLY:
FORALL(i) FORALL(j)
fprintf(f, " %d", ord[i][j]);
fprintf(f, "\n");
break;
case PRETTY:
fprintf(f, "\n\n Order ");
pretty_ordno(f);
fprintf(f, "\n\n < |");
FORALL(i) fprintf(f, " %x", i);
fprintf(f, "\n --+");
FORALL(i) fprintf(f, "--");
FORALL(i)
{ fprintf(f, "\n%10x |", i);
FORALL(j)
fprintf(f, " %c", (ord[i][j]? '+': '-'));
}
fprintf(f, "\n");
break;
case SUMMARY:
fprintf(f, "\n\n Order ");
pretty_ordno(f);
}
}
/*
* Printing the new choice of designated values is part of
* printing the new implication matrix.
* The parameter x is the output mode, and f the destination.
*
* If t is defined only it is printed. Otherwise the true
* values are listed. In ugly format, the boolean vector
* true (1 if value is designated, 0 if not) is printed.
* Note that this convention for ugly output is different
* from that of MaGIC version 1.1 and causes incompatibility
* with post-processing software.
*/
void des_print(FILE *f, output_style x)
{
int i;
if ( desno == 1 ) ord_print(f,x);
switch(x) {
case NONE:
break;
case UGLY:
FORALL(i) fprintf(f, " %d", desig[i]);
fprintf(f, "\n" );
break;
case PRETTY:
if ( theJob->f_t ) {
fprintf(f, "\n\n Choice ");
pretty_desno(f);
fprintf(f, " of t: %x\n", des);
}
else {
fprintf(f, "\n\n Choice ");
pretty_desno(f);
fprintf(f, " of truths: ");
FORALL(des) if ( desig[des] )
fprintf(f, " %x", des);
fprintf(f, "\n");
}
break;
case SUMMARY:
if ( theJob->f_t )
fprintf(f, "\n\n t = %x", des);
else {
fprintf(f, "\n\n truth =");
FORALL(des) if ( desig[des] )
fprintf(f, " %x", des);
}
}
}
/*
* Printing the new implication matrix is part of printing
* the new algebra.
* The parameter x is the output mode, and f the destination.
*/
void C_print(FILE *f, output_style x)
{
int i, j;
if ( matno == 1 ) des_print(f,x);
switch(x) {
case SUMMARY:
case NONE:
return;
case UGLY:
FORALL(i) FORALL(j) fprintf(f, " %d", C[i][j]);
break;
case PRETTY:
fprintf(f, "\n\n Implication matrix ");
pretty_matno(f);
fprintf(f, "\n\n -> |");
FORALL(i) fprintf(f, " %x", i);
fprintf(f, "\n ---+");
FORALL(i) fprintf(f, "--");
FORALL(i) {
fprintf(f, "\n%10x |", i);
FORALL(j) fprintf(f, " %x", C[i][j]);
}
fprintf(f, "\n");
}
}
/*
* Printing a new ! table may be part of printup.
* The parameter x is the output mode, and f the destination.
*/
void box_print(FILE *f, output_style x)
{
int i;
switch(x) {
case UGLY:
FORALL(i) fprintf(f, " %d", box[i]);
fprintf(f, "\n");
break;
case PRETTY:
fprintf(f, "\n ! matrix ");
pretty_boxno( f );
fprintf(f, "\n\n a |");
FORALL(i) fprintf(f, " %x", i);
fprintf(f, "\n ---+");
FORALL(i) fprintf(f, "--");
fprintf(f, "\n !a |");
FORALL(i) fprintf(f, " %x", box[i]);
if ( theJob->f_n ) {
fprintf(f, "\n ?a |");
FORALL(i) fprintf(f, " %x", diamond[i]);
}
fprintf(f, "\n");
break;
case SUMMARY:
case NONE:
return;
}
}
/*
* Printing a nulladic user connective may be part of printup.
* The parameter x is the output mode, and f the destination.
*/
void u_print0(FILE *f, output_style x, int y)
{
switch(x) {
case UGLY:
fprintf(f, " %d\n", nulladic[y]);
break;
case PRETTY:
fprintf(f, "\n Choice ");
pretty_umat( f, y );
fprintf(f, " of %s: %x\n",
theJob->dcs[y]->s, nulladic[y]);
break;
case SUMMARY:
case NONE:
return;
}
}
/*
* Printing a monadic user connective may be part of printup.
* The parameter x is the output mode, and f the destination.
*/
void u_print1(FILE *f, output_style x, int y)
{
int i;
switch(x) {
case UGLY:
FORALL(i) fprintf(f, " %d", monadic[y][i]);
fprintf(f, "\n");
break;
case PRETTY:
fprintf(f, "\n %s matrix ", theJob->dcs[y]->s);
pretty_umat( f, y );
fprintf(f, "\n\n ");
for ( i = 0; i < strlen(theJob->dcs[y]->s); i++ )
printf(" ");
fprintf(f, "a |");
FORALL(i) fprintf(f, " %x", i);
fprintf(f, "\n ----");
for ( i = 0; i < strlen(theJob->dcs[y]->s); i++ )
printf("-");
fprintf(f, "+");
FORALL(i) fprintf(f, "--");
fprintf(f, "\n %s(a) |", theJob->dcs[y]->s);
FORALL(i) fprintf(f, " %x", monadic[y][i]);
fprintf(f, "\n");
break;
case SUMMARY:
case NONE:
return;
}
}
/*
* Printing a dyadic user connective may be part of printup.
* The parameter x is the output mode, and f the destination.
*/
void u_print2(FILE *f, output_style x, int y)
{
int i, j, k;
switch(x) {
case NONE:
case SUMMARY:
return;
case UGLY:
FORALL(i) FORALL(j)
fprintf(f, " %d", dyadic[y][i][j]);
break;
case PRETTY:
fprintf(f, "\n %s matrix ", theJob->dcs[y]->s);
pretty_umat( f, y );
fprintf(f, "\n\n %s |",
theJob->dcs[y]->s);
FORALL(i) fprintf(f, " %x", i);
fprintf(f, "\n --");
for ( i = 0; i < strlen(theJob->dcs[y]->s); i++ )
printf("-");
fprintf(f, "+");
FORALL(i) fprintf(f, "--");
FORALL(i) {
fprintf(f, "\n");
for ( k = 0; k < strlen(theJob->dcs[y]->s); k++ )
printf(" ");
fprintf(f, "%19x |", i);
FORALL(j)
fprintf(f, " %x", dyadic[y][i][j]);
}
fprintf(f, "\n");
}
}
/*
* This is the printup routine called with every good matrix.
* The parameter x is the output mode, and f the destination.
*/
void printup(FILE *f, output_style x)
{
int i;
if ( firstchange >= firstarrow ) C_print(f,x);
if ( theJob->f_nec && firstchange >= firstbox ) box_print(f,x);
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->defcon[i] == PRIMITIVE )
switch( theJob->adicity[i] ) {
case 0:
if ( firstchange >= ucc0[i] )
u_print0(f,x,i);
break;
case 1:
if (firstchange >= ucc1[i][0] )
u_print1(f,x,i);
break;
case 2:
if (firstchange >= ucc2[i][0][0] )
u_print2(f,x,i);
}
if ( x == PRETTY ) {
if ( theJob->failure ) fail_print(f);
fprintf(f, "\n");
fflush(f);
}
}
/*
* This is the series of functions for pretty-printing the
* matrix numbers.
*/
void pretty_size(FILE *f)
{
fprintf( f, "%d", siz+1 );
}
void pretty_negno(FILE *f)
{
pretty_size(f);
fprintf( f, ".%d", negno );
}
void pretty_ordno(FILE *f)
{
if ( theJob->f_n )
pretty_negno(f);
else pretty_size(f);
fprintf( f, ".%d", ordno );
}
void pretty_desno(FILE *f)
{
pretty_ordno(f);
fprintf( f, ".%d", desno );
}
void pretty_matno(FILE *f)
{
pretty_desno(f);
fprintf( f, ".%d", matno );
}
void pretty_boxno(FILE *f)
{
pretty_matno(f);
if ( theJob->f_nec ) fprintf( f, ".%d", boxno );
}
/*
* DOES NOT LOOK RIGHT AT ALL
*
void pretty_umat(FILE *f, int x)
{
int i;
for ( i = x-1; i >= 0; i-- )
if ( theJob->defcon[i] == PRIMITIVE ) {
pretty_umat( f, i );
break;
}
if ( i < 0 ) pretty_matno(f);
fprintf( f, ".%d", matplus[x] );
}
*
*/
void pretty_umat(FILE *f, int x)
{
if ( x < 0 ) pretty_boxno(f);
else {
pretty_umat(f,x-1);
if ( theJob->defcon[x] == PRIMITIVE )
fprintf( f, ".%d", matplus[x] );
}
}
/*
* The assignment of values failing the bad guy is appended to
* each structure recorded in pretty format.
*/
void fail_print(FILE *f)
{
insert_badvalues( theJob->failure );
fprintf(f,"\n Failure: ");
outformula( theJob->failure, theJob->failure, f, VALS );
fprintf(f,"\n");
}
void insert_badvalues( int offset )
{
if ( !offset ) return;
insert_badvalues( theJob->form[offset].lsub );
insert_badvalues( theJob->form[offset].rsub );
if ( offset <= Vmax ) theJob->form[offset].val = badvalue[offset];
}
/*
* At the end of a job some runtime statistics are sent to
* stdout. Note that this is not done in batch mode.
*/
void stats_print()
{
int tim;
CLoCK(&tim);
printf("\n\n\n\n\n Matrices generated by MaGIC: ");
fflush(stdout);
system("date");
printf("\n\n Good ones found: %d\n", good);
printf(" Bad ones tested: %d\n", tot-(good+isoms+isoms2));
printf(" Isomorphs omitted: %d", isoms);
if ( isoms2 ) printf(" + %d", isoms2);
#ifdef HASTIMES
end_timer = time_buffer.tms_utime;
printf("\n Time (cpu): %1.2f seconds",
(end_timer - begin_timer)/(1.0*CLK_TCK));
#endif
printf("\n Time (wall clock): %1.2f seconds\n\n\n",
(tim - start_time)/(TICK*1.0));
}

184
src/logic_pretest.c Normal file
View File

@ -0,0 +1,184 @@
/*
* logic_pretest.c V2.1 (May 1993)
*
* Most 2-refutations can be found before the search for matrices
* starts. The function find_twos does this. As in the cases of
* the test and setup routines, this process is very case-ridden.
*
* When a 2-refutation is found, it is reported to transref by
* means of the call new_two_ref. Transref takes care of all the
* processing, including making sure it is not a repeat of one
* already reported or subsumed by a 1-refutation.
*
* As for set_poss, the parameter info is the vector of sets of
* possible values. It must not be changed by anything in this
* file, as is is needed (and sometimes updated) by transref.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "MaGIC.h"
static unsigned possval[SZ][SZ];
static trs Tpt;
void new_two_ref( int a, int x, int b, int y )
{
int cells[3], vals[3];
boolean valency[3];
cells[0] = a; vals[0] = x; valency[0] = false;
cells[1] = b; vals[1] = y; valency[1] = false;
cells[2] = -1; vals[2] = 0; valency[2] = false;
new_small_ref(cells, vals, valency, Tpt);
}
boolean find_twos(unsigned info[], trs Tr)
{
int i, j;
FORALL(i) FORALL(j) possval[i][j] = info[impindex[i][j]];
Tpt = Tr;
if ( theJob->f_fus ) pretest_fus();
for ( i = 1; i < AXMAX; i++ ) if ( taxiom[i] && TL[i].two_test )
(*(TL[i].two_test))();
return true;
}
boolean find_twos_and_threes(unsigned info[], trs Tr)
{
int i, j;
FORALL(i) FORALL(j) possval[i][j] = info[impindex[i][j]];
Tpt = Tr;
if ( theJob->f_fus ) pretest_fus();
for ( i = 1; i < AXMAX; i++ ) if ( taxiom[i] && TL[i].two_test )
(*(TL[i].two_test))();
for ( i = 1; i < AXMAX; i++ ) if ( taxiom[i] && TL[i].three_test )
(*(TL[i].three_test))();
return true;
}
void new_three_ref( int a, int x, int b, int y, int c, int z )
{
int cells[4], vals[4];
boolean valency[4];
cells[0] = a; vals[0] = x; valency[0] = false;
cells[1] = b; vals[1] = y; valency[1] = false;
cells[2] = c; vals[2] = z; valency[2] = false;
cells[3] = -1; vals[3] = 0; valency[3] = false;
new_small_ref(cells, vals, valency, Tpt);
}
/*
* Where m is maximal, a->m is maximal for all a. Also, if m1 and
* m2 are maximal and different then a->m1 and a->m2 are different.
*/
void pretest_fus()
{
int m1, m2, a, x;
FORALL(m1) if ( maximal[m1] )
for ( m2 = m1+1; m2 <= siz; m2++ ) if ( maximal[m2] )
FORALL(x) if ( maximal[x] )
FORALL(a)
new_two_ref( impindex[a][m1], x, impindex[a][m2], x );
}
/*
* For affixing, we need to look at possval, which is why this is here.
* Report the incompatible pairs of values for a->b, c->d.
*/
void affix_case(int a, int b, int c, int d)
{
int i, j;
FORALL(i) if ( IN(i,possval[a][b]) )
FORALL(j) if ( IN(j,possval[c][d]) )
if ( !ord[i][j] )
new_two_ref( impindex[a][b], i, impindex[c][d], j );
}
void test_assertion()
{
int i, j;
int a, b;
FORALL(a) FORALL(j) if ( !ord[a][j] )
FORALL(i) if ( a != i || j == i )
FORALL(b) if ( IN(i,possval[a][b]) && IN(j,possval[i][b]) )
new_two_ref( impindex[a][b], i, impindex[i][b], j );
}
void test_contraction()
{
int i, j;
int a, b;
FORALL(i) FORALL(j) if ( !ord[j][i] )
FORALL(b) if ( i != b )
FORALL(a) if ( IN(i,possval[a][b]) )
if ( IN(j,possval[a][i]) )
new_two_ref( impindex[a][b], i, impindex[a][i], j );
}

530
src/logic_set.c Normal file
View File

@ -0,0 +1,530 @@
/*
* logic_set.c V2.1 (May 1993)
*
* The procedures going with set_poss() called from the
* search. Also pre_set() called from job_initial().
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "MaGIC.h"
static int vuloc[VMAX]; /* Local version of vu */
static int phi; /* The changeable subformula */
static int phicc; /* Vector cell of phi */
static int phival; /* The value of formula phi */
/*
* Pre_set checks that such axioms as Excluded Middle are
* satisfied, returning 0 (false) if not. These principles
* are the ones that can be checked without generating any
* implication matrix, or even setting up a search space,
* so the search is avoided if they fail.
*/
boolean pre_set()
{
int i,j;
FORALL(i) {
greater_than[i] = less_than[i] = 0;
FORALL(j) {
if ( ord[i][j] ) ADDTO(j,greater_than[i]);
if ( ord[j][i] ) ADDTO(j,less_than[i]);
}
Greater_than[i] = (greater_than[i] & ~(1 << i));
Less_than[i] = (less_than[i] & ~(1 << i));
}
for ( i = 1; i < AXMAX; i++ )
if ( theJob->axiom[i] && TL[i].zero_test )
if (!(*(TL[i].zero_test))()) return false;
if ( theJob->f_T )
FORALL(i)
if ( !ord[i][siz] ) return false;
if ( theJob->f_F )
FORALL(i)
if ( !ord[0][i] ) return false;
for ( i = 0; theJob->croot[i][0]; i++ )
if ( ! kost[i] )
if ( ! utest(i,0) ) return false;
return true;
}
/*
* Utest returns true if the user-defined axiom or rule #x
* is valid (preserves designation for all assignments to the
* variables it involves). It is assumed that changeable
* connectives are not involved.
*/
boolean utest(int x, unsigned info[])
{
int i, j;
if ( kost[x] > 1 ) return true;
for ( i = 1; i <= Vmax; i++ ) {
theJob->form[i].val = 0;
vuloc[i] = 0;
}
phi = 0;
phival = 0;
FORALL(i) FORALL(j) C[i][j] = (ord[i][j]? des: undes);
for ( i = 0; theJob->croot[x][i]; i++ )
set_vuloc( theJob->croot[x][i], theJob->croot[x][i] );
for ( i = 0; theJob->proot[x][i]; i++ )
set_vuloc( theJob->proot[x][i], theJob->proot[x][i] );
do if ( badcase( x, info )) {
if ( kost[x] ) REMOVE(phival,info[phicc]);
else return false;
}
while ( anothercase(x) );
return true;
}
/*
* The following few functions implement the testing of zero
* and one refutations in a rather crude but acceptable way.
* First we record the variables used locally.
*/
void set_vuloc(int r, int rr)
{
int i;
if ( r < 0 ) return;
if ( r < VMAX ) vuloc[r] = 1;
else {
set_vuloc(theJob->form[r].lsub,rr);
set_vuloc(theJob->form[r].rsub,rr);
if ( r != rr && !strcmp(theJob->form[r].sym->s,"->") )
phi = r;
else if ( r != rr && !strcmp(theJob->form[r].sym->s,"o") )
phi = r;
else if ( !strcmp(theJob->form[r].sym->s,"!") )
phi = r;
else for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->form[r].sym == theJob->dcs[i] ) {
if ( theJob->defcon[i] == PRIMITIVE )
phi = r;
else set_vuloc(theJob->defcon[i],rr);
}
}
}
/*
* This tests the rule for one assignment of values to its
* constituent atoms. Note the returned value is 1 for a
* failure of the rule and 0 for success.
*/
boolean badcase(int x, unsigned info[])
{
int i;
for ( i = 0; theJob->proot[x][i] > 0; i++ )
if ( !desig[eval( theJob->proot[x][i], info )] ) return false;
for ( i = 0; theJob->croot[x][i] > 0; i++ )
if ( desig[eval( theJob->croot[x][i], info )] ) return false;
return true;
}
/*
* Eval returns the current value of the subformula rooted
* at r. This is not a fast way of testing, but it will do.
* Note that C is set up so that true cases get designated
* values and false cases undesignated ones.
*/
int eval(int r, unsigned z[])
{
int dr, Ls, Rs;
symb c;
if ( r < 1 ) skipout("Attempt to test rubbish",SKIP);
c = theJob->form[r].sym;
if ( is_var(c) ) return theJob->form[r].val;
Ls = theJob->form[r].lsub;
Rs = theJob->form[r].rsub;
if ( !strcmp(c->s,"->") ) {
if ( r == phi ) {
phicc = impindex[eval(Ls,z)][eval(Rs,z)];
while ( phival < siz && !IN(phival,z[phicc]) )
phival++;
return phival;
}
return C[eval(Ls,z)][eval(Rs,z)];
}
if ( !c->s[1] ) switch( c->s[0] ) {
case 'T':
return siz;
case 'F':
return 0;
case 't':
return des;
case 'f':
return N[des];
case '&':
return K[eval(Ls,z)][eval(Rs,z)];
case 'v':
return A[eval(Ls,z)][eval(Rs,z)];
case 'o':
if ( r == phi ) {
phicc = impindex[eval(Ls,z)][N[eval(Rs,z)]];
while ( phival < siz && !IN(phival,z[phicc]) )
phival++;
return N[phival];
}
return N[C[eval(Ls,z)][N[eval(Rs,z)]]];
case '~':
return N[eval(Rs,z)];
case '!':
if ( r == phi ) {
phicc = boxindex[eval(Rs,z)];
while ( phival < siz &&
!IN(phival,z[phicc]) )
phival++;
return phival;
}
return box[eval(Rs,z)];
}
for ( dr = 0; theJob->dcs[dr] != theJob->form[r].sym; dr++ ) ;
if ( r == phi ) {
switch( theJob->adicity[dr] ) {
case 0:
phicc = ucc0[dr];
break;
case 1:
phicc = ucc1[dr][eval(Rs,z)];
break;
case 2:
phicc = ucc2[dr][eval(Ls,z)][eval(Rs,z)];
}
while ( phival < siz && !IN(phival,z[phicc]) )
phival++;
return phival;
}
else {
if ( theJob->adicity[dr] == 1 )
theJob->form[atom[0][dr]].val = eval(Rs,z);
else if ( theJob->adicity[dr] == 2 ) {
theJob->form[atom[0][dr]].val = eval(Ls,z);
theJob->form[atom[1][dr]].val = eval(Rs,z);
}
return eval( theJob->defcon[dr], z );
}
}
int anothercase(int x)
{
int i;
if ( kost[x] ) {
if ( phival == siz ) phival = 0;
else return ++phival;
}
for ( i = 1; i <= Vmax; i++ ) if ( vuloc[i] ) {
if ( theJob->form[i].val == siz ) theJob->form[i].val = 0;
else return ++(theJob->form[i].val);
}
return 0;
}
/*
* Set_poss is called from transref when a search space is
* being initialised. The vector info will contain (as bit
* vectors) supersets of the possible values for each cell.
* Set_poss may take values out but should on no account
* put values in. Since transref is allowed to split up
* the seasrch space and search bits of it separately, this
* function should not be based on any assumption about what
* values will be present as possibilities.
*
* The first values to be pruned away are those which are
* larger than siz, the maximum value. The arrow matrix C
* should also have only designated (true) values in cells
* a -> b where ord[a][b], and only undesignated values in
* cells a -> b where not ord[a][b].
*
* Logic_poss trims off more values according to the
* postulates of the chosen logic and any pre-defined axioms
* which have been selected.
*
* In affixing logics (all except FD), affixing and the
* existence of fusion force more values out.
*/
boolean set_poss(unsigned info[], trs T)
{
int i, j, k, pr;
unsigned mask;
pr = 0;
for ( i = 0; theJob->dcs[i]; i++ ) ;
while ( i ) {
if ( theJob->defcon[--i] == PRIMITIVE ) {
switch ( theJob->adicity[i] ) {
case 0: co_priority( ucc0[i], pr, T );
break;
case 1:
FORALL(j)
co_priority( ucc1[i][j], pr, T );
break;
case 2:
FORALL(j) FORALL(k)
co_priority( ucc2[i][j][k], pr, T );
}
pr++;
}
}
if ( theJob->f_nec )
FORALL(i) co_priority( boxindex[i], pr, T );
FORALL(i) FORALL(j) co_priority( impindex[i][j], pr+1, T );
mask = 0;
FORALL(i) ADDTO(i,mask);
for ( i = 0; i < tr_par.vlength; i++ ) info[i] &= mask;
FORALL(i) FORALL(j) FORALL(k)
if IFF( (ord[i][j]),(!desig[k]) )
REMOVE(k,info[impindex[i][j]]);
if ( !logic_poss(info) ) return 0;
if ( theJob->f_fus ) fusion(info);
for ( i = 0; theJob->croot[i][0]; i++ )
if ( kost[i] == 1 ) utest( i, info );
return 1;
}
/*
* Fusion requires that if m is any maximal element then any
* a->m is also maximal.
*/
void fusion(unsigned info[])
{
int m, x, a;
FORALL(m) if ( maximal[m] )
FORALL(x) if ( !maximal[x] )
FORALL(a)
REMOVE(x,info[impindex[a][m]]);
}
/*
* If permutation is selected, wherever ord[a][ b->c ] we must
* have ord[b][ a->c ]. Hence if ord[a][x] for ALL or NONE of
* the values for b->c, then we can remove from the values for
* a->c any y such that !ord[b][y] or ord[b][y] respectively.
*/
boolean permutable(int a, int b, int c, unsigned info[])
{
int k, m;
k = impindex[a][c]; m = impindex[b][c];
if ( (greater_than[a] & info[m]) == info[m] )
info[k] &= greater_than[b];
if ( !(greater_than[a] & info[m]) )
info[k] &= ~greater_than[b];
if ( (greater_than[b] & info[k]) == info[k] )
info[m] &= greater_than[a];
if ( !(greater_than[b] & info[k]) )
info[m] &= ~greater_than[a];
return( info[k] != 0 && info[m] != 0 );
}
/*
* This function calls the above cases as required, according
* to the axioms selected. Some additional slightly messy
* features of C-type logics are additionally implemented.
*/
boolean logic_poss(unsigned info[])
{
int i, j, k;
if ( theJob->logic==R )
TaT(info);
if ( (theJob->logic==RW || theJob->logic==LIN)
&& theJob->f_n && theJob->f_lat )
RWX(info);
for ( i = 1; i < AXMAX; i++)
if ( theJob->axiom[i] && TL[i].one_test )
(*(TL[i].one_test))(info);
if ( afx && ( theJob->axiom[AxC] || theJob->axiom[AxC2] ))
FORALL(i) FORALL(j) if ( i < j )
FORALL(k)
if ( !permutable( i, j, k, info ) )
return false;
return (*info != 0);
}
/*
* The axioms valid in the chosen logic are set or unset
* here according to whether the parameter x is 1 or 0.
*/
#define TUNSET(axm) taxiom[axm] = 0
void logic_axioms(boolean x)
{
AXIOM ax;
if ( theJob->f_n && theJob->logic != FD )
theJob->axiom[AxFN] = x;
for ( ax = AxNull; ax < AXMAX; ax++ )
if ( valid[theJob->logic][ax] )
theJob->axiom[ax] = x;
for ( ax = AxNull; ax < AXMAX; ax++ ) {
if ( strchr(ax_string[ax],'~') && !theJob->f_n )
theJob->axiom[ax] = 0;
if ( strchr(ax_string[ax],'&') && !theJob->f_lat )
theJob->axiom[ax] = 0;
if ( strchr(ax_string[ax],'v') && !theJob->f_lat )
theJob->axiom[ax] = 0;
if ( strchr(ax_string[ax],'o') && !theJob->f_fus )
theJob->axiom[ax] = 0;
if ( strchr(ax_string[ax],'!') && !theJob->f_nec )
theJob->axiom[ax] = 0;
if ( strchr(ax_string[ax],'t') && !theJob->f_t )
theJob->axiom[ax] = 0;
if ( strchr(ax_string[ax],'f') && !(theJob->f_t && theJob->f_n) )
theJob->axiom[ax] = 0;
if ( strchr(ax_string[ax],'T') && !theJob->f_T )
theJob->axiom[ax] = 0;
if ( strchr(ax_string[ax],'F') && !theJob->f_F )
theJob->axiom[ax] = 0;
}
if (x) efficient_logic_set();
}
/*
* The above sets all the axioms valid in a particular logic
* - for example, so that they are not printed. For the search
* however, it is much more efficient only to test a few of them
* as selected by this function.
*/
void efficient_logic_set()
{
AXIOM ax;
for ( ax = AxNull; ax < AXMAX; ax++ )
taxiom[ax] = theJob->axiom[ax];
switch(theJob->logic) {
case Null_logic:
case FD:
case B:
case DW:
case TW:
case EW:
case T:
case LOGMAX:
break;
case R:
case RW:
case LIN:
case CK:
taxiom[AxB2] = false;
case S4:
case E:
taxiom[AxWB] = false;
taxiom[AxB] = false;
break;
}
if ( theJob->axiom[AxC] )
taxiom[AxC2] = true;
}

362
src/logic_test.c Normal file
View File

@ -0,0 +1,362 @@
/*
* logic_test.c V2.1 (May 1993)
*
* This is the "test" module for MaGIC. Good_matrix is
* called from transref, and the rest of this file contains
* only what depends on it (with the exception of functions
* for removing isomorphs and for printing matrices, which
* are in other files).
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "MaGIC.h"
/*
* The logic of Good_matrix, schematically, is as follows.
*
* Translate the communication vector info into
* testable data structures.
* If these fail to satisfy some postulate
* Report the refutation just found to the
* search controller.
* return FALSE.
* endif
* If the badguy (if any) fails
* If the structure is not isomorphic
* to any already generated
* Print the matrix.
* endif
* endif
* return TRUE.
*
* The pre-defined axioms, including those defining the logic,
* are tested first. Then any user-defined ones are tested.
*
* Before that, however, check to see that the break conditions
* are not met.
*/
boolean Good_matrix(unsigned info[], trs T)
{
int ti;
if ( theJob->maxmat && good == theJob->maxmat) tr_par.done = true;
if ( tr_par.done ) return true;
tot++;
vect_into_C(info);
for ( ti = AxNull; ti < AXMAX; ti++ )
if ( taxiom[ti] && TL[ti].many_test )
if ( !(*(TL[ti].many_test))(T) ) return false;
if ( !fus_test(T) ) return false;
if ( !axtest(T) ) return false;
if ( theJob->failure && !got_a_fail ) {
no_ref( T ); return false;
}
if ( isomorphic(istak,T) ) return true;
mat_print();
return true;
}
/*
* Translate the communication vector into testable data structures.
*/
void vect_into_C(unsigned info[])
{
register int
i, j;
int k;
FORALL(i) FORALL(j) C[i][j] = info[impindex[i][j]];
if ( theJob->f_nec )
FORALL(i) box[i] = info[boxindex[i]];
for ( k = 0; theJob->dcs[k]; k++ )
if ( theJob->defcon[k] == PRIMITIVE )
switch( theJob->adicity[k] ) {
case 0: nulladic[k] = theJob->form[VMAX+4+k].val
= info[ucc0[k]];
break;
case 1: FORALL(i) monadic[k][i] = info[ucc1[k][i]];
break;
case 2: FORALL(i) FORALL(j)
dyadic[k][i][j] = info[ucc2[k][i][j]];
}
for (i = 0; i < tr_par.vlength; i++) thisvector[i] = info[i];
if ( theJob->f_n && theJob->f_nec )
FORALL(i) diamond[i] = N[box[N[i]]];
}
/*
* Where fusion is stipulated to exist but is not definable,
* it is necessary to test for it. This tends to give large
* refutations, so it is done as late as possible.
*
* Defining fus[a][b] as the least x such that ord[a][C[b][x]],
* check that this exists and is also least in the relation ord.
*/
boolean fus_test(trs T)
{ int i,j,k,m;
if ( !theJob->f_fus ) return true;
if ( theJob->axiom[AxC] && theJob->f_n ) {
FORALL(i) FORALL(j) fus[i][j] = N[C[i][N[j]]];
return true;
}
FORaLL(i) FORaLL(j) {
FORALL(fus[i][j])
if ( ord[i][C[j][fus[i][j]]] ) break;
if ( fus[i][j] > siz ) {
FORALL(k) Ref( impindex[j][k], T );
return false;
}
for ( k = fus[i][j]+1; k <= siz; k++ )
if ( ord[i][C[j][k]] && !ord[fus[i][j]][k] ) {
for ( m = 0; m <= fus[i][j]; m++ )
Ref( impindex[j][m], T );
Ref( impindex[j][k], T );
return false;
}
}
return true;
}
/*
* Eventually it is necessary to test any user-defined axioms
* and rules there may be. This is much slower than testing
* pre-defined ones.
*
* The test given here is the stupidest imaginable, simply
* making all assignments of values to variables and working
* out the consequent values of all subformulas in each case.
* It works fairly well, however, except when there are many
* variables in use. Then its stupidity trips it up badly, so
* there is a case for using a more sophisticated algorithm
* where the task is large.
*/
boolean axtest(trs T)
{
WFF *w;
int i, j;
got_a_fail = 0;
if ( !**(theJob->croot) && !theJob->failure ) return true;
if ( *(theJob->defcon) ) setcon();
for ( i = 0; i < CMAX; i++ ) {
theJob->form[atom[0][i]].val = 0;
theJob->form[atom[1][i]].val = 0;
}
theJob->form[0].val = 0;
for ( i = 1; i <= Vmax; i++ ) theJob->form[i].val = siz;
WORK: for ( w = theJob->form+VMAX+4+(CMAX*3); w != tx; w++ )
w->val = *(w->mtx + *(w->lv)*SZ + *(w->rv));
for ( i = 0; theJob->croot[i][0]; i++ ) if ( kost[i] > 1 ) {
if ( theJob->proot[i][0] != TRIVIAL ) {
for ( j = 0; theJob->proot[i][j]; j++ )
if ( !desig[theJob->form[theJob->proot[i][j]].val] )
goto AX_OK;
}
if ( theJob->croot[i][0] != ABSURD ) {
for ( j = 0; theJob->croot[i][j]; j++ )
if ( desig[theJob->form[theJob->croot[i][j]].val] )
goto AX_OK;
}
for ( j = 0; theJob->proot[i][j]; j++ )
set_used( theJob->proot[i][j], T, true );
for ( j = 0; theJob->croot[i][j]; j++ )
set_used( theJob->croot[i][j], T, true );
return false;
AX_OK: ;
}
if ( theJob->failure && !desig[theJob->form[theJob->failure].val] ) {
got_a_fail = 1;
for ( i = 1; i <= Vmax; i++ )
badvalue[i] = rvu[i]? theJob->form[i].val: SZ;
}
for ( i = 1; i <= Vmax; i++ )
if ( vu[i] ) {
if ( theJob->form[i].val ) {
theJob->form[i].val--;
goto WORK;
}
theJob->form[i].val = siz;
}
return true;
}
/*
* Find the appeals to changeable values in subformula #x.
* Topper is a flag saying whether this is the outermost
* level (so that implications at that level can be read
* as appeals to ord).
*/
void set_used(int x, trs T, boolean topper)
{
int i;
WFF *wf;
if ( x <= 0 ) return;
wf = theJob->form+x;
set_used( wf->lsub, T, false );
set_used( wf->rsub, T, false );
if ( !strcmp(wf->sym->s,"->") && !topper )
Ref( impindex[*(wf->lv)][*(wf->rv)], T );
else if ( !strcmp(wf->sym->s,"!") )
Ref( boxindex[*(wf->rv)], T );
else if ( !strcmp(wf->sym->s,"?") )
Ref( boxindex[N[*(wf->rv)]], T );
else if ( !strcmp(wf->sym->s,"o") ) {
if ( theJob->f_n && valid[theJob->logic][AxC] )
Ref( impindex[*(wf->lv)][N[*(wf->rv)]], T );
else for ( i = 0; i <= wf->val; i++ )
Ref( impindex[*(wf->rv)][i], T );
}
else for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->dcs[i] == wf->sym ) {
if ( theJob->defcon[i] == PRIMITIVE )
switch( theJob->adicity[i] ) {
case 0: Ref( ucc0[i], T );
break;
case 1: Ref( ucc1[i][*(wf->rv)], T );
break;
case 2: Ref( ucc2[i][*(wf->lv)][*(wf->rv)], T );
break;
}
else {
if ( theJob->adicity[i] == 2 ) {
theJob->form[atom[0][i]].val
= *(wf->lv);
theJob->form[atom[1][i]].val
= *(wf->rv);
}
else if ( theJob->adicity[i] == 1 )
theJob->form[atom[0][i]].val = *(wf->rv);
set_used(theJob->defcon[i], T, false);
}
break;
}
if ( wf->rsub )
wf->val = *(wf->mtx + ((*(wf->lv))*SZ + *(wf->rv)));
}
/*
* The routine to derive matrices for defined connectives
* calls the recursive getval as required.
*/
void setcon()
{
int i, j, k, m;
for ( i = 0; theJob->defcon[i]; i++ )
if ( theJob->defcon[i] != PRIMITIVE )
switch(theJob->adicity[i]) {
case 0:
nulladic[i] = theJob->form[VMAX+4+i].val =
getval(theJob->defcon[i]);
break;
case 1:
FORALL(j) {
for ( m = 0; m < CMAX; m++ )
theJob->form[atom[0][m]].val = j;
monadic[i][j] = getval(theJob->defcon[i]);
}
break;
case 2:
FORALL(j) {
for (m = 0; m < CMAX; m++ )
theJob->form[atom[0][m]].val = j;
FORALL(k) {
for ( m = 0; m < CMAX; m++ )
theJob->form[atom[1][m]].val = k;
dyadic[i][j][k] = getval(theJob->defcon[i]);
}
}
}
}
/*
* Recursively generate the value of a subformula.
*/
int getval(int y)
{
WFF *x;
x = theJob->form + y;
if ( x->rsub < 1 )
return x->val;
if ( x->lsub < 1 )
return *(x->mtx + getval(x->rsub));
return *(x->mtx + SZ*getval(x->lsub) + getval(x->rsub));
}

266
src/mp_parse.c Normal file
View File

@ -0,0 +1,266 @@
/*
* mp_parse.c V2.1 (May 1993)
*
* The parser for MaGIC and like programs. This accepts
* formulas in I Block normal form (that is, with our usual
* conventions about scope, association to the left, dots
* in place of parentheses etc. See works of R.K. Meyer or
* the author for details. Actual scope ordering is passed
* by means of the string cn which records the available
* connectives with the dyadic ones in scope order.
*
* Programs such as minlog also use this parser, so although
* for example WFF is defined in MaGIC.h it is defined again
* here to make life easier at some points. The WFF structure
* must have at least the three fields specified here, though
* of course it may have others if it is externally defined.
*
* Note that formula #0 is regarded as the dummy, to be
* returned in case of failure.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "MaGIC.h"
#define P_OK (c && c->s[0] != ')')
#define ERROR(sy,ws) { strcpy(P_ERR[0],(sy)->s); strcpy(P_ERR[1],ws); return 0; }
#define ERROR1(ws) { strcpy(P_ERR[0],""); strcpy(P_ERR[1],ws); return 0; }
static char P_ERR[2][32];
/*
* Now for the parser. It returns the offset of the successfully
* parsed formula, or 0 if the parse attempt was unsuccessful.
*
* s_parse (parse a subformula) is called to get the result.
* Finally, if an error was recorded, it is output.
*
* The parameters are the text to be parsed, the destination
* array of subformulas and the list of available connectives.
*/
int parse( symb fla[] )
{
int rc;
rc = s_parse( fla );
if ( !rc ) {
if ( xdialog ) printf("E");
printf("\n ERROR: \"%s\" %s",P_ERR[0],P_ERR[1]);
}
return rc;
}
/*
* S_parse parses successive subformulas which, separated by
* dyadic connectives, make up the string. It then calls
* Finish to sort out the binary parsing according to the
* scope conventions.
*
* This is a one-pass parser.
*/
int s_parse( symb fla[] )
{
int sbf[20]; /* Dyadic-separated subformulas */
int pptr=0; /* Offset of current symbol */
int oldptr; /* Previous value of pptr */
int ns = 0; /* "Next subformula" */
int i,j;
symb dcn[19]; /* Separating dyadics */
symb c;
c = *fla;
while ( P_OK ) {
oldptr = pptr;
while ( symbol_listed(1,(c=fla[pptr++])) ) ;
i = pptr-1;
if ( is_var(c) || symbol_listed(0,c) )
sbf[ns] = Loc(c, 0, 0);
else if ( c->s[0] == '(' || c->s[0] == '.' ) {
if ( !(sbf[ns] = s_parse( fla+pptr)) ) return 0;
j = Match(fla+pptr-1);
if ( !j ) return 0;
pptr += j-1;
}
else ERROR(fla[pptr-1]," can't begin a subformula");
if ( symbol_listed(1,fla[oldptr]) )
while ( i > oldptr )
sbf[ns] = Loc(fla[--i], 0, sbf[ns]);
c = fla[pptr];
if ( P_OK ) {
if ( symbol_listed(2,c) )
dcn[ns++] = c;
else ERROR(fla[pptr]," found where dyadic connective expected");
c = fla[++pptr];
if ( !P_OK)
ERROR(fla[pptr]," found where subformula expected to start");
}
}
return Finish(sbf, dcn, ns);
}
/*
* Return the offset of the right parenthesis matching the
* left one at start. Remember a dot is a left parenthesis
* whose imaginary right mate is as far to the right as is
* reasonable.
*/
int Match( symb start[] )
{
int i;
for ( i = 1; start[i] && start[i]->s[0] != ')'; i++ )
if ( start[i]->s[0] == '(' )
i += Match(start+i)-1;
if ( start[0]->s[0] == '.' )
return i;
if ( !start[i] )
ERROR1("Unmatched left parenthesis");
return i+1;
}
/*
* Given a formula A1 * .... * An where each Ai is a formula
* and each * is some dyadic connective, turn it into a binary
* wff tree as advertised in the definition of a formula.
*
* Array subf holds the offsets of the main subformulas. The
* corresponding connectives are in conn, while totl is the
* number of subformulas.
*/
int Finish( int subf[], symb conn[], int totl )
{
int i, m = 0;
int sk;
if ( !totl ) return *subf;
sk = 0;
for (i = 0; i < totl; i++)
if ( symbol_position(2,conn[i]) >= sk) {
m = i;
sk = symbol_position(2,conn[i]);
}
i = m+1;
return Loc(conn[m],
Finish(subf, conn, m),
Finish(subf+i, conn+i, totl-i)
);
}
/*
* Locate the given formula in the stack of those already
* parsed and return its offset. If it is not already there
* then add it and return its offset.
*
* Note that in order to force variables to the bottom of the
* stack of subformulas, there may be a section reserved for
* them with symbols initialised to '?'. If not, never mind.
*/
int Loc( symb mn, int lft, int rgt )
{
int i;
for (i = 0; theJob->form[i].sym; i++)
if ( theJob->form[i].sym == mn && theJob->form[i].lsub == lft
&& theJob->form[i].rsub == rgt )
return i;
else if ( is_var(mn) && theJob->form[i].sym->s[0] == '.' )
break;
theJob->form[i].sym = mn;
theJob->form[i].lsub = lft;
theJob->form[i].rsub = rgt;
return i;
}
/*
* A variable is any lower-case letter that is not a connective.
*/
boolean is_var(symb x)
{
int i;
for ( i = 0; i < 3; i++ )
if ( symbol_listed(i,x) ) return 0;
return (isalpha(x->s[0]) && !(x->s[1]));
}
/*
* Return the offset of symbol s in array theJob->symbol[x].
*/
int symbol_position( int x, symb s )
{
int i;
for ( i = 0; theJob->symbol[x][i]; i++ )
if ( theJob->symbol[x][i] == s ) return i;
return -1;
}

11
src/nt_homomorphic.c Normal file
View File

@ -0,0 +1,11 @@
#include "RM.h"
#include "hmi.h"
int main(int argc, char *argv[])
{
if (argc != 2)
Abort("synopsis: nt_homomorphic <file of algebras>",-1);
relatemats(nt_homo, argv[1], "NontrivialHomomorphism");
return 0;
}

94
src/one_plus_t_gen.c Normal file
View File

@ -0,0 +1,94 @@
#include "RM.h"
static int tot_got; /* Total of elements generated */
static int got[SZ]; /* Elements generated so far */
int main( argc, argv )
int argc;
char *argv[];
{
int option;
PRINTMODE p = UGLY;
int g2();
int getopt();
while ((option = getopt (argc, argv, "upt")) != -1)
switch( option ) {
case 'p': p = PRETTY; break;
case 't': p = TeX;
}
selectmats( g2, p );
return 0;
}
int g2(m)
MATRIX *m;
{
int i;
int generator;
int position = 0;
void try();
FORALL(m,generator) {
FORALL(m,i) got[i] = 0;
if (m->tee_exists) {
got[m->tee] = 1;
tot_got = 1;
}
else tot_got = 0;
FORALLCON(m,i)
if ( m->adicity[i] == 0 ) try( m, m->nulladic[i] );
try( m, generator );
if ( tot_got > m->siz ) {
m->my_values[position] = generator;
if ( position++ )
strcpy( m->my_string, "Possible generators: ");
else strcpy( m->my_string, "Generator: ");
}
}
return( position > 0 );
}
void try(m,x)
MATRIX *m;
int x;
{
int i, j;
if ( got[x] ) return;
got[x] = 1;
tot_got++;
if ( m->fragment[NEG] ) try( m, m->neg[x] );
if ( m->fragment[BOX] ) try( m, m->box[x] );
FORALLCON(m,i)
if ( m->adicity[i] == 1 ) try( m, m->monadic[i][x] );
FORALL(m,i) if ( got[i] ) {
try( m, m->C[i][x] );
try( m, m->C[x][i] );
if ( m->fragment[LAT] ) {
try( m, m->K[i][x] );
try( m, m->A[i][x] );
}
if ( m->fragment[FUS] ) {
try( m, m->fus[i][x] );
try( m, m->fus[x][i] );
}
FORALLCON(m,j) {
if ( m->adicity[j] == 2 )
try( m, m->dyadic[j][i][x] );
try( m, m->dyadic[j][x][i] );
}
}
}

152
src/onegen.c Normal file
View File

@ -0,0 +1,152 @@
/* One.c
*
* This uses RM (Read Matrices) to read ugly output from
* MaGIC and calls a function "g1" to choose those matrices
* generated by a single element using only the connectives
* present in the fragment, with the exception of the normal
* sentential constants. The one-generated matrices are
* printed out. The print format may be changed from the
* default (UGLY) to PRETTY or TeX by means of the command
* line switches "-p" or "-t".
*
* For details of the matrix structures and other goodies
* defined in the header, see RM.h. The following should be
* fairly self-explanatory, however. Note that my_values and
* my_string are optional extras used by printmat. These are
* re-initialised to <-1,-1,-1,....> and "" by mat_malloc.
* Use strcpy to put a message in m->my_string.
*
* Function g1 finds all the elements whose singletons generate
* the algebra, records them in my_values and returns 1 to print
* the matrix or 0 to suppress printing.
*
* Try is the recursive procedure for adding new elements
* to the array got[]. It is beside the point if element
* x has already been generated.
*
* Command line option -u (ugly) is allowed but has no effect
* since UGLY is the default print mode.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "RM.h"
static int tot_got; /* Total of elements generated */
static int got[SZ]; /* Elements generated so far */
int main( argc, argv )
int argc;
char *argv[];
{
int option;
PRINTMODE p = UGLY;
int g1();
int getopt();
while ((option = getopt (argc, argv, "upt")) != -1)
switch( option ) {
case 'p': p = PRETTY; break;
case 't': p = TeX;
}
selectmats( g1, p );
return 0;
}
int g1(m)
MATRIX *m;
{
int i;
int generator;
int position = 0;
void try();
FORALL(m,generator) {
FORALL(m,i) got[i] = 0;
tot_got = 0;
FORALLCON(m,i)
if ( m->adicity[i] == 0 ) try( m, m->nulladic[i] );
try( m, generator );
if ( tot_got > m->siz ) {
m->my_values[position] = generator;
if ( position++ )
strcpy( m->my_string, "Possible generators: ");
else strcpy( m->my_string, "Generator: ");
}
}
return( position > 0 );
}
void try(m,x)
MATRIX *m;
int x;
{
int i, j;
if ( got[x] ) return;
got[x] = 1;
tot_got++;
if ( m->fragment[NEG] ) try( m, m->neg[x] );
if ( m->fragment[BOX] ) try( m, m->box[x] );
FORALLCON(m,i)
if ( m->adicity[i] == 1 ) try( m, m->monadic[i][x] );
FORALL(m,i) if ( got[i] ) {
try( m, m->C[i][x] );
try( m, m->C[x][i] );
if ( m->fragment[LAT] ) {
try( m, m->K[i][x] );
try( m, m->A[i][x] );
}
if ( m->fragment[FUS] ) {
try( m, m->fus[i][x] );
try( m, m->fus[x][i] );
}
FORALLCON(m,j) {
if ( m->adicity[j] == 2 )
try( m, m->dyadic[j][i][x] );
try( m, m->dyadic[j][x][i] );
}
}
}

464
src/setup.c Normal file
View File

@ -0,0 +1,464 @@
/*
* setup.c V2.1 (May 1993)
*
* These functions have nothing in common except that they
* are called near the outer levels of MaGIC and don't really
* fit into any other category.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include <sys/types.h> // needed for gettimeofday data types
#include <sys/time.h> // because we use gettimeofday for timing
#include <sys/stat.h> // nobody knows why this is included
#include <fcntl.h> // because we use "open" to read data file
#include "MaGIC.h"
/*
* Subf_set completes the contents of theJob->form.
* It also sets up vu[] and kost[].
*/
void subf_set()
{
int i, j;
for ( i = 0; theJob->form[i].sym; i++ ) {
theJob->form[i].val = 0;
theJob->form[i].mtx = 0;
theJob->form[i].lv =
&(theJob->form[theJob->form[i].lsub].val);
theJob->form[i].rv =
&(theJob->form[theJob->form[i].rsub].val);
for ( j = 0; theJob->dcs[j]; j++ )
if ( theJob->dcs[j] == theJob->form[i].sym ) {
switch( theJob->adicity[j] ) {
case 0:
theJob->form[i].mtx = nulladic+j;
break;
case 1:
theJob->form[i].mtx = monadic[j];
break;
case 2:
theJob->form[i].mtx = *(dyadic[j]);
}
break;
}
if ( !theJob->form[i].mtx &&
!strcmp(theJob->form[i].sym->s,"->") )
theJob->form[i].mtx = *C;
else if ( !theJob->form[i].sym->s[1] && !theJob->form[i].mtx )
switch( theJob->form[i].sym->s[0] ) {
case '~':
theJob->form[i].mtx = N;
break;
case '!':
theJob->form[i].mtx = box;
break;
case '?':
theJob->form[i].mtx = diamond;
break;
case 'v':
theJob->form[i].mtx = *A;
break;
case '&':
theJob->form[i].mtx = *K;
break;
case 'o':
theJob->form[i].mtx = *fus;
}
}
tx = theJob->form+i;
for ( i = 0; i < VMAX; i++ ) vu[i] = rvu[i] = 0;
Vmax = 0;
if ( theJob->failure ) {
set_u(vu,theJob->failure);
set_u(rvu,theJob->failure);
}
for ( i = 0; theJob->croot[i][0]; i++ ) {
kost[i] = 0;
for ( j = 0; theJob->croot[i][j]; j++ ) {
set_u(vu,theJob->croot[i][j]);
kost[i] += worstcase(theJob->croot[i][j],0);
}
for ( j = 0; theJob->proot[i][j]; j++ ) {
set_u(vu,theJob->proot[i][j]);
kost[i] += worstcase(theJob->proot[i][j],0);
}
}
}
/*
* Worstcase calculates the maximum number of lookups of
* changeable matrices in the assignment of a value to the
* formula rooted at x. This is 0 if that formula is a variable,
* a pre-defined constant or null. Otherwise it is the worstcases
* of its left and right subformulas plus the cost of its main
* connective. This cost is 0 for ~, & and v, 1 for -> and any
* user-given primitives, the worstcase of the definition for any
* user-defined connective and a number depending on the logic and
* the matrix size in the case of o.
*/
int worstcase(int x, int ntop)
{
int i, wcsum;
WFF *wf;
if ( x < 1 ) return 0;
wf = theJob->form+x;
if ( is_var(wf->sym) ) return 0;
wcsum = worstcase(wf->lsub,1) + worstcase(wf->rsub,1);
if ( !strcmp(wf->sym->s,"->") ) return (wcsum + ntop);
if ( !wf->sym->s[1] ) switch( wf->sym->s[0] ) {
case '&':
case 'v':
case '~':
case 't':
case 'f':
case 'T':
case 'F': return wcsum;
case '!': return (wcsum + 1);
case '?': return (wcsum + 1);
case 'o':
if ( F_N && theJob->axiom[AxC] )
return (wcsum + 1);
return (wcsum + siz + 1);
}
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->dcs[i] == wf->sym ) {
if ( theJob->defcon[i] == PRIMITIVE )
return (wcsum + 1);
return (wcsum + worstcase(theJob->defcon[i],1));
}
/*
This case should never happen!
*/
skipout("Unrecognised symbol in a formula",SKIP);
return 0;
}
/*
* Record the variables used in the formula rooted at x by
* setting the array arr.
*/
void set_u(int arr[], int x)
{
if ( x < 1 ) return;
if ( x < VMAX ) {
*(arr+x) = 1;
if ( x > Vmax ) Vmax = x;
}
else {
set_u(arr,theJob->form[x].lsub);
set_u(arr,theJob->form[x].rsub);
}
}
/*
* Here is a clock function which ought to work even in
* the worst of times.
*/
void CLoCK(int *timer)
{
struct timeval tp;
struct timezone tzp;
#ifdef HASTIMES
times(&time_buffer);
#endif
gettimeofday(&tp,&tzp);
*timer = tp.tv_sec & 0xffff;
*timer *= TICK;
*timer += (tp.tv_usec / (1000000/TICK));
}
/*
* This is called from got_ord in logic_io.c to set up the
* index from the structures representing the models to the
* vector to be used by transref. At the same time, it labels
* `forbidden' any cells at which backtracking is not allowed.
*/
void set_up_cc()
{
int i, j, k;
boolean fb;
tr_par.vlength = 0;
for ( i = 0; theJob->dcs[i]; i++ ) ;
while ( i ) {
if ( theJob->defcon[--i] == PRIMITIVE ) {
fb = theJob->concut[i];
switch ( theJob->adicity[i] ) {
case 0:
ucc0[i] = tr_par.vlength++;
tr_par.forbidden[ucc0[i]] = fb;
break;
case 1:
FORALL(j) {
ucc1[i][j] = tr_par.vlength++;
tr_par.forbidden[ucc1[i][j]] = fb;
}
break;
case 2:
FORALL(j) FORALL(k) {
ucc2[i][j][k] = tr_par.vlength++;
tr_par.forbidden[ucc2[i][j][k]] = fb;
}
}
}
}
if ( theJob->f_nec ) {
firstbox = tr_par.vlength;
FORALL(i) {
boxindex[i] = tr_par.vlength++;
tr_par.forbidden[boxindex[i]] = false;
}
}
firstarrow = tr_par.vlength;
FORALL(i) FORALL(j)
if ( !( F_N && i < N[j] )) {
impindex[i][j] = tr_par.vlength++;
tr_par.forbidden[impindex[i][j]] = false;
if ( F_N ) impindex[N[j]][N[i]] = impindex[i][j];
}
if ( tr_par.vlength > V_LENGTH ) {
printf(" %d > %d\n", tr_par.vlength, V_LENGTH);
skipout( "V_LENGTH is too small for this job", SKIP );
}
}
/*
* This is called immediately before transref.
*/
void job_start()
{
char infil_name[100];
set_orders(infil_name);
if ( (infil = open(infil_name,0)) < 0 )
skipout("Failed to open the data file",SKIP);
input_bit = 8;
if ( *(theJob->outfil_name) && !filing ) {
outfil = fopen(theJob->outfil_name,"w");
filing = 1;
}
if ( theJob->fil_out == PRETTY || theJob->fil_out == SUMMARY )
disp(outfil);
else if ( theJob->fil_out == UGLY )
uglydisp(outfil);
if ( theJob->tty_out == UGLY )
uglydisp(stdout);
logic_axioms(1);
CLoCK(&start_time);
#ifdef HASTIMES
begin_timer = time_buffer.tms_utime;
#endif
good = tot = isoms = isoms2 = 0;
siz = 0;
set_up_trin();
}
/*
* This, on the other hand, is not.
*/
void job_stop(boolean batch)
{
int i;
CLoCK( &stop_time );
#ifdef HASTIMES
end_timer = time_buffer.tms_utime;
#endif
if ( theJob->tty_out == UGLY ) {
printf(" -1\n");
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->defcon[i] == PRIMITIVE ) printf(" -1\n");
}
if (theJob->fil_out == UGLY ) {
fprintf(outfil, " -1\n");
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->defcon[i] == PRIMITIVE )
fprintf(outfil, " -1\n");
}
if ( !batch ) {
stats_print();
paws();
}
if ( filing ) {
fclose(outfil);
filing = 0;
}
if ( infil ) {
close(infil);
infil = 0;
}
tr_par.done = true;
logic_axioms(false);
}
/*
* Set_orders works out the input file name and extends the
* string passed to it with that name.
*/
void set_orders(char s[])
{
strcpy( s, theJob->data_dir );
if ( theJob->totord )
strcat(s,(theJob->f_n? "tn": "to"));
else if ( theJob->f_lat ) {
if ( !theJob->distrib )
strcat(s,(theJob->f_n? "ln": "l"));
else if ( theJob->axiom[AxBA] ||
( theJob->logic==S4 && theJob->f_n ))
strcat(s,"ba");
else strcat(s,(theJob->f_n? "dln": "dl"));
}
else {
if ( theJob->f_n && theJob->f_t )
strcat(s,"pont");
else if ( theJob->f_n )
strcat(s,"pon");
else if ( theJob->f_t )
strcat(s,"pot");
else strcat(s,"po");
}
sprintf( s+strlen(s), ".%d", Sizmax );
}
/*
* This routine just prints the header for ugly output.
*/
void uglydisp(FILE *f)
{
int i, j;
fprintf( f, " %d", theJob->f_n );
fprintf( f, " %d", theJob->f_t );
fprintf( f, " %d", theJob->f_T );
fprintf( f, " %d", theJob->f_F );
fprintf( f, " %d", theJob->f_fus );
fprintf( f, " %d", theJob->f_lat );
fprintf( f, " %d", theJob->f_nec );
j = 0;
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->defcon[i] == PRIMITIVE ) j++;
fprintf( f, " %d", j );
for ( i = 0; theJob->dcs[i]; i++ )
if ( theJob->defcon[i] == PRIMITIVE )
fprintf( f, " %d %s", theJob->adicity[i], theJob->dcs[i]->s );
fprintf( f, "\n" );
}
/*
* The job parameters are communicated to transref via a structure
* tr_par which must be set up before each call. Note that
* tr_par.forbidden which records functions on which there is a
* "cut" is set elsewhere.
*/
void set_up_trin()
{
tr_par.Test = Good_matrix;
tr_par.Onerefs = set_poss;
tr_par.Smallrefs = find_twos;
tr_par.batches = 10;
tr_par.extra_batches = EXTRA_DEFAULT;
tr_par.maxref = 6;
tr_par.maxbak = 0;
tr_par.verb = 0;
tr_par.Nosecs = false;
tr_par.topsoff = true;
tr_par.report_breaks = false;
tr_par.done = false;
}
/*
* These stubs are just to maintain compatibility with the vntr used
* by FINDER. They are not called.
*/
void report_branches(trin T) {}
void ref_size_report() {}

202
src/sub_irr.c Normal file
View File

@ -0,0 +1,202 @@
/* One.c
*
* This uses RM (Read Matrices) to read ugly output from MaGIC and calls
* a function "si" to choose those matrices which are subdirectly
* irreducible under the connectives present in the fragment. The
* matrices are printed out. The print format may be changed from the
* default (UGLY) to PRETTY or TeX by means of the command line switches
* "-p" or "-t".
*
* For details of the matrix structures and other goodies defined in the
* header, see RM.h. The following should be fairly self-explanatory,
* however. Note that my_values and my_string are optional extras used
* by printmat. These are re-initialised to <-1,-1,-1,....> and "" by
* mat_malloc. Use strcpy to put a message in m->my_string.
*
* Command line option -u (ugly) is allowed but has no effect since UGLY
* is the default print mode.
*/
#include "RM.h"
int si(MATRIX *m);
int non_degenerate(MATRIX* m, int g1, int g2, int congruence[]);
void adjust(MATRIX *m, int congruence[], int from, int to);
int extended(MATRIX *m, int congruence[], int a, int b);
int monex(MATRIX *m, int arr[], int a, int b, int congruence[]);
int dyex(MATRIX *m, int arr[][SZ], int a, int b, int congruence[]);
int orthogonal(MATRIX *m, int theCongruences[][SZ]);
int main( argc, argv )
int argc;
char *argv[];
{
int option;
PRINTMODE p = UGLY;
int g1();
int getopt();
while ((option = getopt (argc, argv, "upt")) != -1)
switch( option ) {
case 'p': p = PRETTY; break;
case 't': p = TeX;
}
selectmats(si,p);
return 0;
}
int si(MATRIX *m)
{
int theCongruences[2][SZ];
int gen1a, gen1b, gen2a, gen2b;
FORALL(m,gen1a) FORALL(m,gen1b) if (gen1b < gen1a) {
if (non_degenerate(m,gen1a,gen1b,theCongruences[0])) {
FORALL(m,gen2a) FORALL(m,gen2b) if (gen2b < gen2a) {
if (non_degenerate(m,gen2a,gen2b,theCongruences[1]) &&
orthogonal(m,theCongruences))
return 0;
}
}
}
return(1);
}
int non_degenerate(MATRIX* m, int g1, int g2, int congruence[])
{
int x, y, temp;
for (x=0; x<SZ; x++)
congruence[x] = -1;
FORALL(m,x)
congruence[x] = x;
congruence[g2] = g1;
/*
* EXTEND THE CONGRUENCE TO A FIXED POINT
*/
do {
temp = 0;
FORALL(m,x) FORALL(m,y)
if (x < y && congruence[x] == congruence[y]) {
if (extended(m,congruence,x,y))
temp = 1;
}
}
while (temp);
/*
* Now renumber the congruence classes contiguously starting from 0,
* in the order of their smallest-numbered members
*/
temp = -1;
FORALL(m,x)
if (congruence[x] >= 0) {
temp--;
adjust(m,congruence,congruence[x],temp);
}
for (x=-2,y=0; x>=temp; x--,y++)
adjust(m,congruence,x,y);
if (y == 0)
return 0;
return 1;
}
void adjust(MATRIX *m, int congruence[], int from, int to)
{
int x;
FORALL(m,x)
if (congruence[x] == from)
congruence[x] = to;
}
int extended(MATRIX *m, int congruence[], int a, int b)
{
int x;
int ex = 0;
if (m->fragment[NEG] &&
monex(m,m->neg,a,b,congruence))
ex = 1;
if (m->fragment[BOX] &&
monex(m,m->box,a,b,congruence))
ex = 1;
FORALLCON(m,x)
if (m->adicity[x] == 1 &&
monex(m,m->monadic[x],a,b,congruence))
ex = 1;
if (dyex(m,m->C,a,b,congruence))
ex = 1;
if (m->fragment[LAT] &&
dyex(m,m->K,a,b,congruence))
ex = 1;
if (m->fragment[LAT] &&
dyex(m,m->A,a,b,congruence))
ex = 1;
if ( m->fragment[FUS] &&
dyex(m,m->fus,a,b,congruence))
ex = 1;
FORALLCON(m,x)
if ( m->adicity[x] == 2 &&
dyex(m,m->dyadic[x],a,b,congruence))
ex = 1;
return ex;
}
int monex(MATRIX *m, int arr[], int a, int b, int congruence[])
{
if (congruence[arr[a]] == congruence[arr[b]])
return 0;
adjust(m,congruence,congruence[arr[b]],congruence[arr[a]]);
return 1;
}
int dyex(MATRIX *m, int arr[][SZ], int a, int b, int congruence[])
{
int x;
int ext = 0;
FORALL(m,x) {
if (congruence[arr[x][a]] != congruence[arr[x][b]]) {
adjust(m,congruence,congruence[arr[x][b]],congruence[arr[x][a]]);
ext = 1;
}
if (congruence[arr[a][x]] != congruence[arr[b][x]]) {
adjust(m,congruence,congruence[arr[b][x]],congruence[arr[a][x]]);
ext = 1;
}
}
return ext;
}
int orthogonal(MATRIX *m, int theCongruences[][SZ])
{
int x,y;
FORALL(m,x)
FORALL(m,y)
if (x<y &&
theCongruences[0][x] == theCongruences[0][y] &&
theCongruences[1][x] == theCongruences[1][y])
return 0;
return 1;
}

50
src/u2p.c Normal file
View File

@ -0,0 +1,50 @@
/* Pretty.c
*
* This is the simplest post-processing program for MaGIC.
* It reads MaGIC's "ugly" output from stdin and pretty-prints
* the matrices to stdout. MaGIC may be used in batch mode to
* pipe the matrices through a program such as this, or they
* may be read from a file.
*/
#include "RM.h"
int main()
{
selectmats( True, PRETTY );
return 0;
}
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/

76
src/u2pic.c Normal file
View File

@ -0,0 +1,76 @@
/* Upic.c
*
* This uses RM (Read Matrices) to read ugly output from
* MaGIC and calls a function "choose" to allow the user
* to decide of each matrix whether it should be kept or
* ignored. The chosen matrices are printed in the ugly
* format.
*
* For details of the matrix structures and other goodies
* defined in the header, see RM.h. The following should be
* fairly self-explanatory, however.
*/
#include "RM.h"
static FILE *tty;
int main()
{
int choose();
tty = fopen( "/dev/tty", "r" );
selectmats( choose, UGLY );
return 0;
}
int choose(m)
MATRIX *m;
{
displaymat( m, "Keep this matrix? (y/n/q)....." );
for (;;)
switch( getc(tty) ) {
case 'y': return 1;
case 'n': return 0;
case 'q': return -1;
}
}
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/

54
src/u2tex.c Normal file
View File

@ -0,0 +1,54 @@
/* Texmats.c
*
* This is a post-processing program for MaGIC.
* It reads ugly MaGIC output from stdin and prints the
* matrices to stdout in TeX format.
*
* See RM.h for more information.
*/
#include "RM.h"
int main()
{
selectmats( True, TeX );
return 0;
}
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/

1956
src/vntr.c Normal file

File diff suppressed because it is too large Load Diff

343
src/vntr.h Normal file
View File

@ -0,0 +1,343 @@
/****************************************************************
* *
* FINDER 3.0 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include <stdio.h>
#include <stdlib.h>
#ifndef __APPLE__
#include <malloc.h>
#endif
#include <string.h>
/*
* Constant definitions
*/
#define REF_MAX 512
#define REF_DEFAULT 16
#define EXTRA_DEFAULT 5
#define MAX_REF_SIZE 8
#ifndef SZ
#define SZ 32
#endif
#define V_LENGTH 1024
/*
* #define SURJ_MAX 64
*/
#define SURJ_MAX 256
#define STAK_MAX (REF_MAX*MAX_REF_SIZE)
#define RRA 50
#define RRB 30
#define NO_REPORT ((unsigned)1)
#define INT_REPORT ((unsigned)2)
#define FLOAT_REPORT ((unsigned)4)
#define DO_REPORT ((unsigned)8)
#define logical unsigned int
#define FOR(x,y) for( y = x; y; y = y->p )
#define FORR(x,y) FOR( x->cellvals, y )
/*
* Type definitions
*/
/*
*typedef enum {
* false,
* true
*} boolean;
*/
#define boolean char
#define false ((boolean)0)
#define true ((boolean)1)
typedef enum {
NOCUT,
FOUND,
RECORDED
} cutcode;
typedef enum {
PERFECT,
NULL_SPACE,
BIG_SPACE,
REF_LIST,
BUST,
IBUST,
NULL_REF,
SURJES,
SKIP
} exit_code;
typedef enum {
SETPOSSES,
DOSMALLS,
SEARCHES,
SOLUTIONS,
BAD_TESTS,
SURJ_BACKTRACKS,
NULL_BACKTRACKS,
F_SUBSUMED,
B_SUBSUMED,
B1_SUBSUMED,
PREREFS,
REFSIZE,
TOPLESS,
LOC_MEMORY,
MEMORY,
BRANCHES,
PRE_TIME,
SEARCH_TIME,
MAX_REPORT
} report_code;
typedef struct IL {
boolean positive; /* Represents positive literal */
short int v, w; /* A couple of integers */
struct IL *p; /* in a list */
} INTLIST, *intlist;
typedef struct reftype {
int cardinality; /* Just what is says */
boolean notop; /* Useless extension omitted */
intlist cellvals; /* The cell-valuess involved */
struct reftype *nxtr; /* Just for stack management */
} REF, *ref;
typedef struct rf_list { /* A list of refutations */
ref rf;
struct rf_list *nextref;
} REFLIST, *reflist;
typedef struct {
int blocks; /* How many times blocked */
ref back; /* For calculating secondaries */
reflist cvrefs; /* The refs involving this c-v */
reflist posrefs; /* Positives involving this c-v */
int vpos; /* Offset of its cell */
} CELLVALUE, *cellvalue;
typedef struct {
short poss; /* How many possible values */
short vpos; /* Vector position of this cell */
reflist inject; /* Index to injective function */
CELLVALUE cvals[SZ]; /* The cell-value structures */
boolean used; /* Involved in new refutation */
boolean has_value; /* This cell has a value */
} CELL, *cell;
typedef struct {
logical valset;
int last_seen[SZ];
intlist cellset;
} SURJ;
typedef struct {
logical report_type;
char s_report[80];
int i_report;
float f_report;
void (*do_report)();
} REPORT;
typedef struct cng {
int forkpoint;
int cutval;
logical comvec[V_LENGTH];
int inorder[V_LENGTH];
logical possvals[V_LENGTH];
boolean active;
struct cng *lastone;
} CUTT, *cutt;
typedef struct { REF news[1024]; } RBATCH, *rbatch;
typedef struct { INTLIST news[1024]; } ILBATCH, *ilbatch;
typedef struct { REFLIST news[1024]; } RLBATCH, *rlbatch;
typedef struct {
boolean (*Test)(), /* The principal test function */
(*Onerefs)(), /* Removal of impossible values */
(*Smallrefs)(); /* Special treatment for smalls */
int vlength, /* Local vector length */
batches, /* Local stack size / 1000 */
extra_batches, /* Batches after pretest */
maxref, /* Maximum refutation size */
maxbak, /* Maximum number of backtracks */
verb, /* Statistics verbosity setting */
ref_record[RRA][RRB],
branches[SZ];
boolean Nosecs, /* Suppress secondary refs */
topsoff, /* Remove redundant ref tops */
report_breaks, /* Print reason for end search */
forbidden[V_LENGTH], /* No backtracking */
done; /* End-of-search status raised */
REPORT reps[MAX_REPORT+1]; /* Search statistics */
} TRIN, *trin;
typedef struct {
trin job;
CELL vector[V_LENGTH];
logical comvec[V_LENGTH];
int inorder[V_LENGTH];
int coinorder[V_LENGTH];
int priority[V_LENGTH];
int this_cell;
int susguy;
int firstchange;
int forkpoint;
int maxval;
int stakmax;
int unfixt;
int local_memory;
int max_batches;
boolean novect;
boolean ts;
boolean cut_recorded;
boolean noref;
rbatch stak[REF_MAX];
ilbatch il_stak[STAK_MAX];
rlbatch rl_stak[STAK_MAX + REF_MAX];
intlist il_free;
reflist rl_free;
reflist duds;
ref newref;
ref stak_ptr;
SURJ surjection[SURJ_MAX];
cutt cutptr;
cutcode cut_flag;
} TRS, *trs;
#ifndef CLK_TCK
extern long sysconf();
#define CLK_TCK sysconf(3)
#endif
/*
* Global variables
*/
#ifdef TRFILE
#define TR_GLOB
#else
#define TR_GLOB extern
#endif
TR_GLOB trs debugger;
TR_GLOB int begin_time, end_time;
/*
* Function prototypes
*/
void transref ( trin job );
void init_trin ( trin tr );
void clean_up ( trs T );
void report_initial ( trs T );
trs tr_initial ( trin job );
void search ( trs T );
int pick_cell ( trs T );
int set_fork ( trs T, int rc );
void delete_cut ( trs T );
reflist get_rl ( trs T );
void put_rl ( trs T, reflist dead );
intlist get_il ( trs T, boolean b, int x, int y, intlist ip );
void put_il ( trs T, intlist dead );
int batches_used ( trs T );
ref get_ref ( trs T );
void put_ref ( trs T, ref dead, boolean flag );
void rec_put_il ( trs T, intlist ip, ref r, boolean flag );
void more_refs ( trs T );
void more_rls ( trs T );
void more_ils ( trs T );
boolean invalue ( trs T, cell c, int v );
void transfer_ref (trs T, cell c, ref rf);
void blockval ( trs T, cell c, int v, ref rrf, report_code RC );
boolean surjok ( trs T );
void outvalue ( trs T, cell c );
void untransfer_ref (trs T, cell c, ref rf);
void unblockval ( trs T, cell c, int v, ref rrf );
void mark_delete ( trs T, ref r );
void delete_duds ( trs T );
void delete_a_dud ( trs T, reflist r );
void setref ( trs T );
void reduceref ( trs T );
void addref ( int x, trs T );
void print_ref ( ref r );
void print_sus ( trs T, cell c );
void totsus ( trs T );
void make_coherent ( trs T );
void no_ref ( trs T );
void new_small_ref ( int cells[], int vals[], boolean valency[], trs T );
void remove_value ( trs T, cell c, int x );
intlist get_all_ils ( int cells[], int vals[], boolean valency[], int x, trs T );
boolean subsumed ( ref the_ref, trs T );
boolean subsumes ( ref little_ref, ref big_ref );
void back_sub ( trs T, ref the_ref );
void Ref ( int x, trs T );
void record_cut ( trs T );
void record_part_cut ( int x, trs T );
void complete_cut ( int ex, trs T );
boolean prepared ( trs T );
void setinx ( trs T );
boolean pre_test ( trs T );
boolean absfixt ( int x );
void surjective ( logical vec[], logical vset, trs T );
void injective ( logical vec[], int x, trs T );
void co_priority ( int x, int y, trs T );
void ref_size_report ();
void Report ( trin tr );
void report_branches ( trin tr );
void dump_refs ( int rows, int columns );
void job_done ( trin t, char *s );
int timestamp ();
void skipout ( char s[], int exitcode );
void test_backs (trs T);

499
src/wffs.c Normal file
View File

@ -0,0 +1,499 @@
/*
* wffs.c V2.1 (May 1993)
*
* This contains the routines from MaGIC (other than the
* parser) which deal with formulas.
*/
/****************************************************************
* *
* MaGIC 2.1 *
* *
* (C) 1993 Australian National University *
* *
* All rights reserved *
* *
* The information in this software is subject to change without *
* notice and should not be construed as a commitment by the *
* Australian National University. The Australian National Uni- *
* versity makes no representations about the suitability of *
* this software for any purpose. It is supplied "as is" without *
* express or implied warranty. If the software is modified in *
* a manner creating derivative copyright rights, appropriate *
* legends may be placed on the derivative work in addition to *
* that set forth above. *
* *
* Permission to use, copy, modify and distribute this software *
* and its documentation for any purpose and without fee is *
* hereby granted, provided that both the above copyright notice *
* and this permission notice appear in all copies and sup- *
* porting documentation, and that the name of the Australian *
* National University not be used in advertising or publicity *
* pertaining to distribution of the software without specific, *
* written prior permission. *
* *
****************************************************************/
#include "MaGIC.h"
#define oldsymbol(s) newsymbol(s,0,0)
#define found_symbol(s) (this_symbol(s)? true: false)
/*
* This grabs, initialises and returns the symbol with the
* given string, inserting it in the first unoccupied symbol
* structure if need be. It is added to the end of the given
* symbol lists if these are non-null.
*
* If the symbol already exists, no change is made to the
* symbol lists, even if they are non-null.
*/
symb newsymbol( char *string, symb symbol_list1[], symb symbol_list2[] )
{
int i;
symb sy = 0;
for ( i = 0; i < SYMBOLMAX; i++ )
if ( !strcmp(theJob->symtable[i].s,string) )
return (theJob->symtable + i);
for ( i = 0; i < SYMBOLMAX; i++ )
if ( !theJob->symtable[i].s[0] ) {
sy = theJob->symtable + i;
strcpy(sy->s, string);
sy->next = theJob->symtab;
sy->last = 0;
if ( theJob->symtab ) theJob->symtab->last = sy;
theJob->symtab = sy;
break;
}
if ( symbol_list1 ) {
for ( i = 0; symbol_list1[i]; i++ ) ;
symbol_list1[i] = sy;
symbol_list1[i+1] = 0;
}
if ( symbol_list2 ) {
for ( i = 0; symbol_list2[i]; i++ ) ;
symbol_list2[i] = sy;
symbol_list2[i+1] = 0;
}
return sy;
}
/*
* Wff_initial initialises theJob->form etc.
* It is called from dialog.c as part of setting
* up a new job.
*/
void wff_initial()
{
int i;
symb dummy_symbol;
dummy_symbol = oldsymbol("no_connective");
for ( i = 0; i < FMAX; i++ ) {
theJob->form[i].lsub = theJob->form[i].rsub = 0;
if ( i == 0 ) theJob->form[i].sym = dummy_symbol;
else if ( i == 1 ) theJob->form[i].sym = oldsymbol("a");
else if ( i == 2 ) theJob->form[i].sym = oldsymbol("b");
else if ( i < VMAX ) theJob->form[i].sym = oldsymbol(".");
else if ( i < VMAX+4+CMAX ) theJob->form[i].sym = oldsymbol(" ");
else theJob->form[i].sym = 0;
}
theJob->form[VMAX].sym = oldsymbol("t");
theJob->form[VMAX+1].sym = oldsymbol("f");
theJob->form[VMAX+2].sym = oldsymbol("T");
theJob->form[VMAX+3].sym = oldsymbol("F");
for ( i = 0; i < CMAX; i++ ) {
atom[0][i] = VMAX+4+CMAX+i;
theJob->form[atom[0][i]].sym = oldsymbol("a");
atom[1][i] = VMAX+4+(2*CMAX)+i;
theJob->form[atom[1][i]].sym = oldsymbol("b");
}
}
/*
* Got_formula calls infml to read in a formula if possible.
* If the user asks for help this is given, otherwise the
* boolean return value is 1 for success, 0 for failure.
*
* The parameters x, y and yy are passed on to infml. The
* string s states what type of formula ("axiom", etc) is
* sought.
*/
boolean got_formula(int x, int y, int yy, char *s)
{
for(;;)
switch( infml(x,y,yy) ) {
case -1:
return(0);
case 0:
return(1);
case 1:
if ( xdialog ) return(0);
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);
}
}
}
/*
* Infml calls for and processes a formula from stdin. The two
* parameters are: x, the destination (IN_CONC = axiom or
* conclusion, IN_PREM = premise, IN_BGUY = badguy, IN_DEFN =
* definition); y, the offset for cases other than x = IN_BGUY; yy,
* the second offset for cases x = IN_CONC and x = IN_PREM.
*
* Return value is 0 if successful in reading a formula and getting
* it parsed, 1 if an error is encountered, -1 if the null formula
* is input.
*
* The first action after input is to render the formula hygenic,
* checking for bad characters at the same time. A list of the
* symbols is compiled from the input string. By default, each
* string of characters surrounded by white space (or parentheses)
* is tried against the symbol table. If it is not found, initial
* segments are tried.
*/
int infml(input_case x, int y, int yy)
{
int i, k, wf;
symb fml[SLEN*2];
char longs[SLEN];
if ( x != IN_DEFN && !xdialog ) printf("\n Enter formula (or RETURN): ");
fflush(stdout);
fgets(answer,SLEN,stdin);
k = 0;
while ( next_symbol(longs) )
if ( !seek_symbol(longs,fml,&k) ) {
EP;
printf("\n Illegal input: unrecognised symbol %s\n\n ", longs);
return 1;
}
if ( !k ) return -1;
fml[k] = 0;
if ( x == IN_DEFN ) {
if ( k == 1 ) {
EP; printf("\n ERROR: definition is too short!\n\n");
return 1;
}
if ( theJob->adicity[y] ) {
for ( i = 0; i < k; i++ )
if ( !strchr(fml[i]->s,'a') ) break;
if ( i == k ) {
EP; printf("\n ERROR: variable \"a\" does not ");
printf("occur in the definition\n\n");
return 1;
}
}
if ( theJob->adicity[y] == 2 ) {
for ( i = 0; i < k; i++ )
if ( !strchr(fml[i]->s,'b') ) break;
if ( i == k ) {
EP; printf("\n ERROR: variable \"b\" does not ");
printf("occur in the definition\n\n");
return 1;
}
}
}
wf = parse(fml);
if ( !wf ) return 1;
if ( x == IN_CONC )
theJob->croot[y][yy] = wf;
else if ( x == IN_PREM )
theJob->proot[y][yy] = wf;
else if ( x == IN_BGUY )
theJob->failure = wf;
else {
fix_atoms(y,wf);
theJob->defcon[y] = wf;
}
return 0;
}
/*
* Get the first space-delimited sequence of nonspace characters
* from answer[], truncate answer[] to the following portion and
* return true. If there is no such sequence, return false.
*/
boolean next_symbol( char longs[] )
{
int i, j;
for ( i = 0; answer[i] && isspace(answer[i]); i++ );
if ( !answer[i] ) return false;
j = i;
do {
longs[i-j] = answer[i];
i++;
}
while ( answer[i-1] && !isspace(answer[i-1]) ); i--;
if ( answer[i] ) longs[i-j] = 0;
for ( j = 0; answer[j]; j++ ) answer[j] = answer[j+i];
return true;
}
/*
* String occurs in the current symbol table.
*/
symb this_symbol( char *string )
{
symb sy;
for ( sy = theJob->symtab; sy; sy = sy->next )
if ( !strcmp(sy->s,string) ) return sy;
return 0;
}
/*
* The "long string" longs may contain exactly a meaningful symbol,
* in which case this is placed in fml[*k] and *k incremented.
* Otherwise, the longest meaningful initial substring is placed
* in fml[*k], *k incremented and the remainder of longs treated
* recursively. The value returned is true on success, false if no
* meaningful initial string is found.
*/
boolean seek_symbol( char longs[], symb fml[], int *k )
{
char shorts[64], *cp;
int i, j;
if ( !*longs ) return true;
if ( found_symbol(longs) ) {
fml[(*k)++] = this_symbol(longs);
return true;
}
if ( (cp = strchr(longs,'(')) && (j = cp - longs) ) {
for ( i = 0; i < j; i++ ) shorts[i] = longs[i];
shorts[i] = 0;
if ( !seek_symbol(shorts, fml, k) ) return false;
for ( i = 0; longs[i]; i++ ) longs[i] = longs[i+j];
}
else if ( (cp = strchr(longs,')')) && (j = cp-longs) ) {
for ( i = 0; i < j; i++ ) shorts[i] = longs[i];
shorts[i] = 0;
if ( !seek_symbol(shorts, fml, k) ) return false;
for ( i = 0; longs[i]; i++ ) longs[i] = longs[i+j];
}
if ( strchr(")(",*longs) ) {
*shorts = *longs;
shorts[1] = 0;
fml[(*k)++] = oldsymbol(shorts);
return seek_symbol(longs+1, fml, k);
}
strcpy( shorts, longs );
for ( i = strlen(longs)-1; i; i-- ) {
shorts[i] = 0;
if ( found_symbol(shorts) ) {
fml[(*k)++] = this_symbol(shorts);
return seek_symbol(longs+i, fml, k);
}
}
if ( isalpha(*longs) ) {
*shorts = *longs;
shorts[1] = 0;
fml[(*k)++] = oldsymbol(shorts);
return seek_symbol(longs+1, fml, k);
}
return false;
}
/*
* Part of infml is to "fix the atoms". This means change the
* occurrences of 'a' and 'b' in the definition of defined
* connective #y to atom[0][y] and atom[1][y] respectively.
* The other parameter, dy, points to the subformula within
* which to search for 'a' and 'b'. Fix_atoms is recursive.
*/
void fix_atoms(int y, int wf)
{
WFF *dy;
if ( !wf ) return;
dy = theJob->form + wf;
if ( dy->lsub ) {
if ( !strcmp(theJob->form[dy->lsub].sym->s,"a") )
dy->lsub = atom[0][y];
else if ( !strcmp(theJob->form[dy->lsub].sym->s,"b") )
dy->lsub = atom[1][y];
else fix_atoms(y,dy->lsub);
}
if ( dy->rsub ) {
if ( !strcmp(theJob->form[dy->rsub].sym->s,"a") )
dy->rsub = atom[0][y];
else if ( !strcmp(theJob->form[dy->rsub].sym->s,"b") )
dy->rsub = atom[1][y];
else fix_atoms(y,dy->rsub);
}
}
/*
* Outfml is a very simple deparser which writes the formula
* rooted at p, a subformula of that rooted at q, to stream f.
*
* Local variable c is set to p->sym just for brevity.
*/
void outformula(int p, int q, FILE *f, varmode vm)
{
symb c;
if ( p <= 0 ) skipout("Attempt to print nonsense formula",SKIP);
c = theJob->form[p].sym;
if ( symbol_listed(2,c) ) {
if ( p != q ) fprintf( f, "(" );
outformula(theJob->form[p].lsub,q,f,vm);
fprintf( f, " %s ", c->s );
outformula(theJob->form[p].rsub,q,f,vm);
if ( p != q ) fprintf( f, ")" );
}
else if ( symbol_listed(1,c) ) {
fprintf( f, "%s", c->s );
if ( strlen(c->s) > 1 ) fprintf( f, " " );
outformula(theJob->form[p].rsub,q,f,vm);
}
else {
if ( p <= Vmax && vm == VALS )
fprintf( f, "%d", theJob->form[p].val );
else fprintf( f, "%s", c->s );
}
}
/*
* Is_in returns 1 (true) if c occurs in the formula *w
* and 0 (false) if it does not.
*/
boolean is_in(symb s, int w)
{
if ( w <= 0 ) return false;
if ( theJob->form[w].sym == s ) return true;
if ( is_in( s, theJob->form[w].lsub )) return true;
return is_in(s, theJob->form[w].rsub);
}
/*
* It is sometimes necessary to purge the formula list of any
* appeal to a given symbol. This is done especially when a
* connective has just been deleted.
*
* The first move is to propagate the bad symbol up the tree:
* anything with a bad subformula is also bad.
*/
void purge( symb badsym )
{
int i, j, k, m;
for ( k = 1; theJob->form[k].sym; k++ ) {
if ( theJob->form[theJob->form[k].lsub].sym == badsym )
theJob->form[k].sym = badsym;
if ( theJob->form[theJob->form[k].rsub].sym == badsym )
theJob->form[k].sym = badsym;
}
j = 1;
for ( i = 1; theJob->form[i].sym; i++ )
if ( theJob->form[i].sym == badsym ) {
if ( j < i ) j = i;
while ( theJob->form[++j].sym == badsym ) ;
if ( ! theJob->form[j].sym ) {
do {
theJob->form[i].sym = 0;
theJob->form[i].lsub = 0;
theJob->form[i].rsub = 0;
}
while ( ++i <= j );
return;
}
theJob->form[i].sym = theJob->form[j].sym;
theJob->form[i].lsub = theJob->form[j].lsub;
theJob->form[i].rsub = theJob->form[j].rsub;
theJob->form[j].sym = badsym;
for ( k = j+1; theJob->form[k].sym; k++ ) {
if ( theJob->form[k].lsub == j )
theJob->form[k].lsub = i;
if ( theJob->form[k].rsub == j )
theJob->form[k].rsub = i;
}
if ( theJob->failure == j ) theJob->failure = i;
for ( k = 0; theJob->croot[k][0]; k++ )
for ( m = 0; m < RTMAX; m++ ) {
if ( theJob->proot[k][m] == j )
theJob->proot[k][m] = i;
if ( theJob->croot[k][m] == j )
theJob->croot[k][m] = i;
}
for ( k = 0; theJob->dcs[k]; k++ )
if ( theJob->defcon[k] == j ) theJob->defcon[k] = i;
}
}