1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
# Copyright (C) 2017 Mate Soos
#
# This program is free software; you can redistribute it and/or
# modify it under the terms of the GNU General Public License
# as published by the Free Software Foundation; version 2
# of the License.
#
# This program 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. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program; if not, write to the Free Software
# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
# 02110-1301, USA.
from __future__ import print_function
import sqlite3
import optparse
class Query:
def __init__(self, dbfname):
self.conn = sqlite3.connect(dbfname)
self.c = self.conn.cursor()
self.runID = self.find_runID()
# zero out goodClauses
self.c.execute('delete from goodClauses;')
self.cur_good_ids_num = 0
self.num_goods_total = 0
self.cur_good_ids = []
def __enter__(self):
return self
def __exit__(self, exc_type, exc_value, traceback):
self.conn.commit()
self.conn.close()
def parse_and_add_lemmas(self, lemmafname):
with open(lemmafname, "r") as f:
for line in f:
line = line.strip().split(" ")
self.parse_one_line(line)
# final dump
self.dump_ids()
print("Parsed %d number of good lemmas" % self.num_goods_total)
def parse_one_line(self, line):
self.cur_good_ids_num += 1
self.num_goods_total += 1
# get ID
myid = int(line[0])
assert myid >= 0, "ID is always at least 0"
assert myid != 0, "ID with 0 should not even be printed"
num_used = int(line[1])
last_used = int(line[2])
# append to cur_good_ids
self.cur_good_ids.append((self.runID, myid, num_used, last_used))
# don't run out of memory, dump early
if self.cur_good_ids_num > 10000:
self.dump_ids()
def dump_ids(self):
self.c.executemany("""
INSERT INTO goodClauses (`runID`, `clauseID`, `num_used`, `last_confl_used`)
VALUES (?, ?, ?, ?);""", self.cur_good_ids)
self.cur_good_ids = []
self.cur_good_ids_num = 0
def find_runID(self):
q = """
SELECT runID
FROM startUp
order by startTime desc
"""
runID = None
for row in self.c.execute(q):
if runID is not None:
print("ERROR: More than one RUN in the SQL, can't add lemmas!")
exit(-1)
runID = int(row[0])
print("runID: %d" % runID)
return runID
if __name__ == "__main__":
usage = """usage: %prog [options] sqlite_db lemmas
It adds lemma indices from "lemmas" to the SQLite database, indicating whether
it was good or not."""
parser = optparse.OptionParser(usage=usage)
parser.add_option("--verbose", "-v", action="store_true", default=False,
dest="verbose", help="Print more output")
(options, args) = parser.parse_args()
if len(args) != 2:
print("Error. Please follow usage")
print(usage)
exit(-1)
dbfname = args[0]
lemmafname = args[1]
print("Using sqlite3db file %s" % dbfname)
print("Using lemma file %s" % lemmafname)
with Query(dbfname) as q:
q.parse_and_add_lemmas(lemmafname)
print("Finished adding good lemma indicators to db %s" % dbfname)
exit(0)
|
