EXTRA_OBJECTS_TO_INSTALL =
EXTRA_OBJECTS_TO_CLEAN =
-TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/
+TPTPDIR= /home/$(USER)/work-area/TPTP-v4.0.1/
all: tptp2grafite mainTHF
clean: clean_tests clean_generated
> /dev/null || echo Failed: $$X; \
done
+thf:
+ for x in `cat thf_problems`; do\
+ echo $$x;\
+ ./mainTHF -tptppath $(TPTPDIR) $$x.p > THF/$$x.ma;\
+ done
+
include ../../Makefile.defs
include ../Makefile.common
%token IOR
%token NIEQ
%token IEQ
+ %token XOR
%token IMPLY
+ %token IMPLYLR
+ %token COIMPLY
%token PEQ
%token DOT
%token EOF
| LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
| term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
| term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
+ | term IMPLYLR term { T.Binder (`Forall,(T.Ident("_",None),Some $3),$1) }
+ | term COIMPLY term { T.Appl [T.Symbol("Iff",0);$1;$3] }
+ | term XOR term { T.Appl [T.Symbol("Xor",0);$1;$3] }
| term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
+ | term NIEQ term { T.Appl [T.Symbol("NotEq",0);$1;$3] }
| term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
| term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
| NOT term { T.Appl [T.Symbol("Not",0);$2] }