Skip to content

GitLab

why3
why3
Commit ccc5698c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

remove the old TPTP parser

parent 52364c72
Hide whitespace changes
Inline Side-by-side
Showing with 8 additions and 1155 deletions
Makefile.in
View file @ ccc5698c
......@@ -261,15 +261,15 @@ PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer
PLUGINS = genequlin tptpfof tptp
TFF1MODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
TFF1CMO = $(addsuffix .cmo, $(TFF1MODULES))
TFF1CMX = $(addsuffix .cmx, $(TFF1MODULES))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \
$(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
$(TFF1MODULES)
$(TPTPMODULES)
PLUGML = $(addsuffix .ml, $(PLUGMODULES))
PLUGMLI = $(addsuffix .mli, $(PLUGMODULES))
......@@ -308,11 +308,11 @@ lib/plugins/%.cmo: plugins/transform/%.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/tptp.cmxs: $(TFF1CMX)
lib/plugins/tptp.cmxs: $(TPTPCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/tptp.cmo: $(TFF1CMO)
lib/plugins/tptp.cmo: $(TPTPCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $^
......@@ -1007,65 +1007,6 @@ src/coq_config.ml:
endif
########
# Tptp2why
########
ifeq (@enable_whytptp@,yes)
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2whymain
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
TPTPML = $(addsuffix .ml, $(TPTPMODULES))
TPTPMLI = $(addsuffix .mli, $(TPTPMODULES))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
# build targets
plugins.byte byte: lib/plugins/whytptp.cmo
plugins.opt opt : lib/plugins/whytptp.cmxs
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: EXTOBJS += $(MENHIRLIB)
lib/plugins/whytptp.cmxs lib/plugins/whytptp.cmo: INCLUDES += $(MENHIRINC)
lib/plugins/whytptp.cmxs: $(TPTPCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -shared -o $@ $^
lib/plugins/whytptp.cmo: $(TPTPCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $^
install_no_local::
cp -f lib/plugins/whytptp.cm* $(LIBDIR)/why3/plugins/
# depend and clean targets
include .depend.tptp2why
.depend.tptp2why: $(TPTPGENERATED)
$(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@
depend: .depend.tptp2why
clean::
rm -f $(TPTPGENERATED)
rm -f src/tptp2why/*.cm* src/tptp2why/*.o
rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
rm -f src/tptp2why/*.output src/tptp2why/*.automaton
rm -f lib/plugins/whytptp.cm* lib/plugins/whytptp.o
rm -f .depend.tptp2why
endif
#######
# tools
#######
......@@ -1397,7 +1338,7 @@ $(DISTRIB_TAR): doc/manual.pdf
ln -s ../theories $(DISTRIB_DIR)/share/theories
cp --parents $(DISTRIB_FILES) $(DISTRIB_DIR)
rm -f $(DISTRIB_DIR)/src/config.ml
cd $(DISTRIB_DIR); rm -f $(LIBGENERATED) $(TPTPGENERATED) \
cd $(DISTRIB_DIR); rm -f $(LIBGENERATED) \
$(COQGENERATED) $(WHY3DOCGENERATED) $(PLUGGENERATED)
cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
......@@ -1469,8 +1410,7 @@ headers:
src/transform/close_epsilon.ml* \
src/transform/lift_epsilon.ml*
headache -c misc/headache_config.txt -h misc/header_sc.txt \
src/transform/hypothesis_selection.ml* \
src/tptp2why/*.ml*
src/transform/hypothesis_selection.ml*
sed -i -f misc/fixnames.sed -- \
Makefile.in configure.in src/*.ml* src/*/*.ml* \
src/tools/cpulimit.c
......
configure.in
View file @ ccc5698c
......@@ -87,18 +87,6 @@ AC_ARG_ENABLE(coq-libs,
[ --enable-coq-libs enable Coq realizations],,
enable_coq_libs=yes)
# TPTP parser
AC_ARG_ENABLE(whytptp,
[ --enable-whytptp enable TPTP parser (requires Menhir)],,
enable_whytptp=yes)
# Menhir library
AC_ARG_ENABLE(menhirlib,
[ --enable-menhirlib enable Menhir library],,
enable_menhirlib=no)
# hypothesis selection
AC_ARG_ENABLE(hypothesis-selection,
......@@ -263,29 +251,6 @@ if test "$USEOCAMLFIND" = yes; then
fi
fi
AC_CHECK_PROG(MENHIR,menhir,menhir,no)
if test "$MENHIR" = no ; then
enable_whytptp=no
enable_menhirlib=no
AC_MSG_WARN(cannot find menhir.)
fi
# checking for libmenhir
if test "$enable_menhirlib" = yes ; then
if test "$USEOCAMLFIND" = yes; then
MENHIRLIB=$(ocamlfind query menhirLib)
fi
if test -n "$MENHIRLIB"; then
echo "ocamlfind found menhir library in $MENHIRLIB"
else
MENHIRLIB="+menhirLib"
AC_CHECK_FILE($OCAMLLIB/menhirLib,,enable_menhirlib=no)
if test "$enable_menhirlib" = no; then
AC_MSG_WARN(Lib menhir not found.)
fi
fi
fi
# checking for rubber
AC_CHECK_PROG(RUBBER,rubber,rubber,no)
if test "$enable_doc" = yes ; then
......@@ -502,7 +467,6 @@ AC_SUBST(OCAMLOPT)
AC_SUBST(OCAMLDEP)
AC_SUBST(OCAMLLEX)
AC_SUBST(OCAMLYACC)
AC_SUBST(MENHIR)
AC_SUBST(OCAMLDOC)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
......@@ -517,7 +481,6 @@ AC_SUBST(enable_profiling)
AC_SUBST(CAMLP5O)
AC_SUBST(enable_ide)
AC_SUBST(MENHIRLIB)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(SQLITE3LIB)
AC_SUBST(enable_bench)
......@@ -532,9 +495,6 @@ AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVERSION)
AC_SUBST(enable_whytptp)
AC_SUBST(enable_menhirlib)
AC_SUBST(enable_hypothesis_selection)
AC_SUBST(enable_doc)
......@@ -580,8 +540,6 @@ if test "$enable_coq_support" = "yes" ; then
echo " FP arithmetic : $enable_coq_fp_libs $reason_coq_fp_libs"
fi
fi
echo "TPTP parser : $enable_whytptp"
echo "Menhir library : $enable_menhirlib"
echo "hypothesis selection : $enable_hypothesis_selection"
echo "profiling : $enable_profiling"
echo "localdir : $enable_local"
src/tptp2why/tests/ansi.py deleted 100644 → 0
View file @ 52364c72
from sys import stderr
class Ansi:
"""ANSI control sequences control"""
CSI = "\x1B["
# colors
Black = "0"
Red = "1"
Green = "2"
Yellow = "3"
Blue = "4"
Magenta = "5"
Cyan = "6"
White = "7"
Reset = "9"
# effects
bold = "1"
reset = "0"
underline = "4"
blinkSlow = "5"
blinkFast = "6"
negative = "7"
normal = "22"
notUnderlined = "24"
# fore|back ground
foreground = "3"
background = "4"
def colorize( s, color = "reset", pos = "foreground", *args ):
"applies changes to the string given"
prefix = Ansi.CSI + getattr( Ansi, pos, Ansi.foreground) + getattr( Ansi, color, Ansi.reset )
suffix = Ansi.CSI + "m"
for item in args:
prefix += ";" + getattr( Ansi, item, Ansi.normal )
prefix += "m"
return prefix + s + suffix
def inBlue( s, bold = False, pos = "foreground" ):
args = []
if bold:
args.append( "bold" )
return colorize( s, "Blue", pos, *args )
def inGreen( s, bold = False, pos = "foreground" ):
args = []
if bold:
args.append( "bold" )
return colorize( s, "Green", pos, *args )
def inRed( s, bold = False, pos = "foreground" ):
args = []
if bold:
args.append( "bold" )
return colorize( s, "Red", pos, *args )
def inBlack( s, bold = False, pos = "foreground" ):
args = []
if bold:
args.append( "bold" )
return colorize( s, "Black", pos, *args )
def inNormal( s, bold = False, pos = "foreground" ):
"uses normal color"
args = []
if bold:
args.append( "bold" )
return colorize( s, "Reset", pos, *args )
class Log:
logStream = stderr
@classmethod
def log( self, s, bold=False ):
"""
>>> Log.setLogStream( sys.stdout )
>>> Log.log( 'coin' )
coin
>>> Log.setLogStream( file('/dev/null', 'w') )
>>> Log.log( 'pan' )
"""
print >> self.logStream, ansi.inNormal( s, bold= bold )
@classmethod
def logImportant( self, s, bold=False ):
"prints in reversed blue"
print >> self.logStream, ansi.inBlue( s, bold=bold, pos="background" )
@classmethod
def logSoft( self, s ):
"prints in blue"
print >> self.logStream, inBlue( s )
@classmethod
def logFail( self, s ):
"for fails, print in red"
print >> self.logStream, ansi.inRed( s, bold=True )
@classmethod
def logCritical( self, s ):
"for critical warning, very visible !"
print >> self.logStream, inRed( s, pos="background", blink=1 )
@classmethod
def setLogStream( self, logStream ):
self.logStream = logStream
src/tptp2why/tests/dispatcher deleted 100755 → 0
View file @ 52364c72
#!/usr/bin/env python
# launches some provers on a bunch of tptp problems, after conversion
# with tptp2why
import sys
import getopt
import time
import subprocess
from os import path
import re
import ansi
#------------------------------------------------------------------------------
# parsing options
usage = """usage : dispatcher [--help] [-P prover [-P prover...]] \
[-p prover [-p prover...]] [-I dir] [-o file][--] file1 [file2...]
Tries to solve the given tptp files (*.p) with given provers, through why or \
directly. Every prover is called on every problem.
options :
-P prover : adds a why prover
-p prover : adds a prover to be called directly on tptp problem
-I dir : use this dir to search for included files"""
class Options:
"contains all options parsed on the command line"
optstring = "P:p:I:o:h"
long_optstring = ["help"]
provers = []
tptpProvers = []
def parse(self):
self.path = path.dirname(sys.argv[0])
self.options, self.args = \
getopt.getopt(sys.argv[1:], self.optstring, self.long_optstring)
# add each prover to self.provers
for opt,prover in self.options:
if opt == "-P":
self.provers.append(prover)
elif opt == "-p":
self.tptpProvers.append(prover)
self.options = dict(self.options)
# those options are now useless
self.options.pop("-P", None)
self.options.pop("-p", None)
def __init__(self):
self.parse()
print "search for files in", self.path
options = Options()
if "--help" in options.options or "-h" in options.options:
print usage
sys.exit(0)
#------------------------------------------------------------------------------
# finding provers
def sendTo(problem, prover, useWhy = True):
"calls the prover on the problem, and return its return value and output's \
lines"
if useWhy:
prover = "why - -P "+prover
else:
if "-I" in options.options:
prover = prover + " -I "+options.options["-I"]
s = subprocess.Popen(prover, shell=True, \
stdin=subprocess.PIPE, stdout=subprocess.PIPE)
print "\n"+ansi.inBlue("*", pos="background"), "send data to prover "+ prover
output = s.communicate(problem)[0].splitlines()
return (s.returncode, output)
#-----------------------------------------------------------------------------
# interpreting provers output
def isValid(retcode, output):
"returns True in case of success"
for pattern in ["Valid","valid", "[Pp]roof found", "[cC]ompletion [fF]ound"]:
if any( [ re.search(pattern, line) for line in output ] ):
return True
return False
def isFailure(retcode, output):
"returns True in case of failure"
if retcode != 0:
return True
for pattern in ["[fF]ailure","[fF]alse", "[nN]o [Pp]roof found"]:
if any( [ re.search(pattern, line) for line in output ] ):
return True
return False
def handleOutput(retcode, output):
"""if we can find it is a failure or a success, print it.
Else, print the output."""
print "retcode :",(ansi.inGreen(`retcode`)
if retcode==0 else ansi.inRed(`retcode`))
if isFailure(retcode, output):
print ansi.inRed("Failure")
return
elif isValid(retcode, output):
print ansi.inGreen("Valid")
return
else:
for line in output:
print line
def main():
for f in options.args:
print "\n\n"+ ansi.inBlue("file "+f, pos="background") + "\n"
try:
fd = open(f, 'r')
problem = fd.read()
fd.close()
# tptp provers
for prover in options.tptpProvers:
try:
retcode, output = sendTo(problem, prover, useWhy = False)
handleOutput(retcode, output)
except:
pass
# why-driven provers
# first, transform the problem
if "-I" in options.options:
command = "tptp2why - -I "+options.options["-I"]
else:
command = "tptp2why -"
preprocess = subprocess.Popen(command, shell=True, \
stdout=subprocess.PIPE, stdin=subprocess.PIPE)
problem = preprocess.communicate(problem)[0]
# then give it to provers
for prover in options.provers:
try:
retcode, output = sendTo(problem, prover)
handleOutput(retcode, output)
except e: print "exception :",e
except Exception, e:
print "exception :", e, e.args
if __name__=="__main__":
main()
src/tptp2why/tests/eprover.sh deleted 100755 → 0
View file @ 52364c72
#!/bin/sh
exec eprover -s -xAuto -tAuto --memory-limit=Auto --tstp-in --cpu-limit=2 $@
src/tptp2why/tests/spass.sh deleted 100755 → 0
View file @ 52364c72
#!/bin/sh
FILE=$( tempfile spass )
cat - > ${FILE} && SPASS -TPTP -PGiven=0 -PProblem=0 -TimeLimit=2 ${FILE}
rm -f ${FILE}
src/tptp2why/tptp2whymain.ml deleted 100644 → 0
View file @ 52364c72
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Simon Cruanes *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** this is a parser for tptp problems (.p files) *)
open TptpTree
open Why3
open Lexing
open TptpTranslate
(** module to process a single file *)
module Process : sig
val read_channel : Env.read_channel
end = struct
let fromInclude = function | Include x -> x | _ -> assert false
let isInclude = function | Include _ -> true | _ -> false
(** for a given file, returns the list of declarations
for this file and all the files it includes, recursively *)
let rec getAllDecls ?first:(first=false) include_dir filename =
try
let filename = if first then filename else include_dir^"/"^filename in
let input = if filename = "-" then stdin else open_in filename in
let decls = myparse input in
close_in input;
process_recursively ~include_dir:include_dir decls
with (Sys_error _) as e ->
print_endline ("error : unable to open "^filename);
raise e
(** read completely a channel *)
and getDeclsFromChan input =
let decls = myparse input in
process_recursively decls
(** search a list of declarations for include statements *)
and process_recursively ?(include_dir=".") decls =
let (to_include, real_decl) = List.partition isInclude decls in
let to_include = List.map fromInclude to_include in (* remove Include *)
let all_decls = List.concat
(List.map (getAllDecls include_dir) to_include) in
all_decls @ real_decl
(** parses a single file *)
and myparse chan =
let lb = Lexing.from_channel chan in
TptpParser.tptp TptpLexer.token lb
let read_channel _env path file c =
let decls = getDeclsFromChan c in
if Debug.test_flag Typing.debug_parse_only ||
Debug.test_flag Typing.debug_type_only
then Util.Mstr.empty
else
let my_theory = theory_of_decls path file decls in
Util.Mstr.add "Tptp" my_theory Util.Mstr.empty
end
(** register as a .p/.ax file parser *)
let () = Env.register_format "tptp" ["p"] Process.read_channel
(*
Local Variables:
compile-command: "unset LANG; make -C ../.."
End:
*)
src/tptp2why/tptpLexer.mll deleted 100644 → 0
View file @ 52364c72
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Simon Cruanes *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
{
open Format
open Lexing
open TptpParser
let keywords = Hashtbl.create 97
let () =
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[
"fof", FOF;
"cnf", CNF;
"include", INCLUDE
]
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let stringBuf = Buffer.create 256
exception LexicalError of string * Lexing.position
let report fmter (s, pos) =
fprintf fmter "file %s, line %d, char %d"
s (pos.pos_lnum) (pos.pos_cnum-pos.pos_bol)
(** report errors *)
let () = Why3.Exn_printer.register (fun fmt exn -> match exn with
| TptpParser.Error ->
Format.fprintf fmt "syntax error.@."
| LexicalError (s, pos) ->
Format.fprintf fmt "lexical error: %a@." report (s, pos)
| e -> raise e)
}