Tammet: Uus lehekülg: '

 #!/usr/bin/python3 # -*- coding: utf-8 -*- # # Runs prover on problems, collects results # # Call on the command line    import sys, csv import datetime import subprocess...'

2019-09-29T19:18:43Z

Uus lehekülg: '<pre> #!/usr/bin/python3 # -*- coding: utf-8 -*- # # Runs prover on problems, collects results # # Call on the command line import sys, csv import datetime import subprocess...'

Uus lehekülg

<pre>
#!/usr/bin/python3
# -*- coding: utf-8 -*-
#
# Runs prover on problems, collects results
#
# Call on the command line

import sys, csv
import datetime
import subprocess

# ====== configuration globals ======

# problems.csv should contain problem names,
# one per line, without a folder and without the .p suffix, like this (remove #):
# NUM847+1
# CSR028+3
# NUM304+1
# ...

problems_filename="problems.csv"

# the Problems folder of TPTP:

problem_path="/opt/TPTP/Problems/"

# summary results of running on problems:

# NB! if you stop the runner and restart, it will continue
# from the last problem NOT in the outfile.
# I.e. to run again from scratch, remove outfile

outfile="example_result.txt"

# folder for storing problem running logs:

log_folder="/tmp/"

# time in seconds per problem:

timeout=20

# ====== globals set in code =========

problem_list=[]

# ====== top level =========

def main():
global problems_list
problem_list=read_problems()
solved=read_solved()
#print(problem_list)
i=0
of=open(outfile,"a")
while i<len(problem_list):
problem=problem_list[i]
if not solved:
pass
elif solved and problem!=solved:
i+=1
continue
else:
solved=False
i=i+1
problem=problem_list[i]
#print(problem)
res=runone(problem)
if res[0]:
of.write(problem+",Proved,"+res[1]+","+res[2]+","+res[3]+"\n")
else:
of.write(problem+",Failed,"+res[1]+","+res[2]+","+str(timeout)+"\n")
of.flush()
i+=1
of.close()

def runone(problem):
global timeout
proved=False
timeline=""
pref=problem[:3]
runnr=0
timeline1=""
timeline2=""
path=problem_path+pref+"/"+problem+".p"
cmd="timeout "+str(timeout)+" ../gkc_41 "+path
print(path)
outfile=log_folder+problem
of=open(outfile,"w")
of.write(cmd+"\n")
of.write(str(datetime.datetime.now())+"\n")
p = subprocess.Popen(cmd, shell=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
for line in p.stdout.readlines():
#print("!!"+str(line))
line=line.decode("utf-8")
of.write(line)
if line.startswith("**** run "):
try:
tmp=line.split()
runnr=tmp[2]
except:
continue
elif line.startswith("this run seconds:"):
try:
tmp=line.split()
timeline1=tmp[3]
except:
timeline1=" "
elif line.startswith("total seconds:"):
try:
tmp=line.split()
timeline2=tmp[2]
except:
timeline2=" "
elif line.startswith("result: proof found"):
proved=True
#print("Proved,"+str(runnr))
elif "maxresident)k" in line:
line=line.replace("user ",",")
line=line.replace("system ",",")
line=line.replace("elapsed ",",")
line=line.replace("%CPU ",","+str(datetime.datetime.now())+",")
timeline=line
if proved:
print("Proved,"+str(runnr)+","+timeline1+","+timeline2)
else:
print("Failed,"+str(runnr)+","+timeline1+","+str(timeout))
retval = p.wait()
of.close()
return (proved,str(runnr),timeline1,timeline2)

def read_problems():
pfname=problems_filename
problems=[]
# --- read problems file ---
try:
csvfile=open(pfname)
freader = csv.reader(csvfile)
for row in freader:
niceprob=row[0].strip()
if niceprob and len(niceprob)>6 and \
niceprob[0].isupper() and niceprob[1].isupper() and niceprob[2].isupper():
problems.append(niceprob)
csvfile.close()
except Exception as e:
print("Could not open or read the input file "+problems)
return []
return problems

def read_solved():
pfname=outfile
solved=[]
last=""
try:
csvfile=open(pfname)
freader = csv.reader(csvfile)
except:
print("no solved file found")
return None
# --- read problems file ---
try:
csvfile=open(pfname)
freader = csv.reader(csvfile)
for row in freader:
if not row: continue
niceprob=row[0].strip()
if niceprob and len(niceprob)>6 and \
niceprob[0].isupper() and niceprob[1].isupper() and niceprob[2].isupper():
solved.append(niceprob)
last=niceprob
csvfile.close()
except Exception as e:
print("Could not open or read the solved file "+pfname)
return None
return last

# ---- run top level ----

main()
</pre>

An example script for provers - Redigeerimiste ajalugu

Tammet: Uus lehekülg: '
#!/usr/bin/python3 # -- coding: utf-8 -- # # Runs prover on problems, collects results # # Call on the command line import sys, csv import datetime import subprocess...'