Commit 09dd0f2b authored by Simon Cruanes's avatar Simon Cruanes
Browse files

small changes

new transformation (currently equivalent to identity) for tptp driver
parent bf7ad68c
...@@ -25,7 +25,7 @@ transformation "eliminate_algebraic" ...@@ -25,7 +25,7 @@ transformation "eliminate_algebraic"
transformation "eliminate_if" transformation "eliminate_if"
transformation "eliminate_let" transformation "eliminate_let"
transformation "encoding_decorate" transformation "polymorphic_to_untyped"
(* TODO : transformation to eliminate types *) (* TODO : transformation to eliminate types *)
......
...@@ -71,13 +71,6 @@ def sendTo(problem, prover, useWhy = True): ...@@ -71,13 +71,6 @@ def sendTo(problem, prover, useWhy = True):
"calls the prover on the problem, and return its return value and output's \ "calls the prover on the problem, and return its return value and output's \
lines" lines"
if useWhy: if useWhy:
if "-I" in options.options:
command = "tptp2why - -I "+options.options["-I"]
else:
command = "tptp2why -"
left = subprocess.Popen(command, shell=True, \
stdout=subprocess.PIPE, stdin=subprocess.PIPE)
problem = left.communicate(problem)[0]
prover = "why - -P "+prover prover = "why - -P "+prover
else: else:
if "-I" in options.options: if "-I" in options.options:
...@@ -135,13 +128,23 @@ def main(): ...@@ -135,13 +128,23 @@ def main():
try: try:
retcode, output = sendTo(problem, prover, useWhy = False) retcode, output = sendTo(problem, prover, useWhy = False)
handleOutput(retcode, output) handleOutput(retcode, output)
except: pass except:
pass
# why-driven provers # 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: for prover in options.provers:
try: try:
retcode, output = sendTo(problem, prover) retcode, output = sendTo(problem, prover)
handleOutput(retcode, output) handleOutput(retcode, output)
except: pass except e: print "exception :",e
except Exception, e: except Exception, e:
print "exception :", e, e.args print "exception :", e, e.args
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment