mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
speed up parsing of large Datalog files, remove pinned
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
efe2a70f6f
commit
8d23b2b813
|
|
@ -46,7 +46,7 @@ namespace datalog {
|
|||
unsigned m_lvl;
|
||||
class stopwatch* m_sw;
|
||||
public:
|
||||
verbose_action(char const* msg, unsigned lvl = 1);
|
||||
verbose_action(char const* msg, unsigned lvl = 11);
|
||||
~verbose_action();
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -41,15 +41,12 @@ class line_reader {
|
|||
static const char s_delimiter = '\n';
|
||||
static const unsigned s_expansion_step = 1024;
|
||||
|
||||
#if 0
|
||||
std::istream & m_stm;
|
||||
#else
|
||||
FILE * m_file;
|
||||
#endif
|
||||
svector<char> m_data;
|
||||
bool m_eof;
|
||||
bool m_eof_behind_buffer;
|
||||
unsigned m_next_index;
|
||||
bool m_ok;
|
||||
|
||||
//actually by one larger than the actual size of m_data,
|
||||
//to fit in the terminating delimiter
|
||||
|
|
@ -88,27 +85,17 @@ class line_reader {
|
|||
|
||||
public:
|
||||
|
||||
#if 0
|
||||
line_reader(std::istream & stm)
|
||||
: m_stm(stm),
|
||||
m_eof(false),
|
||||
m_eof_behind_buffer(false),
|
||||
m_next_index(0),
|
||||
m_data_size(0) {
|
||||
m_data.resize(2*s_expansion_step);
|
||||
resize_data(0);
|
||||
}
|
||||
#else
|
||||
line_reader(const char * fname)
|
||||
:m_eof(false),
|
||||
m_eof_behind_buffer(false),
|
||||
m_next_index(0),
|
||||
m_data_size(0) {
|
||||
:m_eof(false),
|
||||
m_eof_behind_buffer(false),
|
||||
m_next_index(0),
|
||||
m_data_size(0),
|
||||
m_ok(true) {
|
||||
m_data.resize(2*s_expansion_step);
|
||||
resize_data(0);
|
||||
#if _WINDOWS
|
||||
errno_t err = fopen_s(&m_file, fname, "rb");
|
||||
SASSERT(err==0);
|
||||
m_ok = err == 0;
|
||||
#else
|
||||
m_file = fopen(fname, "rb");
|
||||
#endif
|
||||
|
|
@ -116,7 +103,8 @@ public:
|
|||
~line_reader() {
|
||||
fclose(m_file);
|
||||
}
|
||||
#endif
|
||||
|
||||
bool operator()() { return m_ok; }
|
||||
|
||||
/**
|
||||
\brief Retrieve next line from the stream.
|
||||
|
|
@ -170,6 +158,38 @@ public:
|
|||
bool eof() const { return m_eof; }
|
||||
};
|
||||
|
||||
class char_reader {
|
||||
line_reader m_line_reader;
|
||||
char const* m_line;
|
||||
public:
|
||||
char_reader(char const* file):
|
||||
m_line_reader(file),
|
||||
m_line(0)
|
||||
{}
|
||||
|
||||
bool operator()() { return m_line_reader(); }
|
||||
|
||||
char get() {
|
||||
if (!m_line) {
|
||||
if (m_line_reader.eof()) {
|
||||
return EOF;
|
||||
}
|
||||
m_line = m_line_reader.get_line();
|
||||
}
|
||||
if (!(m_line[0])) {
|
||||
m_line = 0;
|
||||
return '\n';
|
||||
}
|
||||
char result = m_line[0];
|
||||
++m_line;
|
||||
return result;
|
||||
}
|
||||
|
||||
bool eof() {
|
||||
return m_line_reader.eof();
|
||||
}
|
||||
};
|
||||
|
||||
class reserved_symbols {
|
||||
typedef map<char const *, dtoken, str_hash_proc, str_eq_proc> str2token;
|
||||
str2token m_str2token;
|
||||
|
|
@ -200,6 +220,7 @@ public:
|
|||
|
||||
class dlexer {
|
||||
std::istream* m_input;
|
||||
char_reader* m_reader;
|
||||
char m_prev_char;
|
||||
char m_curr_char;
|
||||
int m_line;
|
||||
|
|
@ -219,7 +240,12 @@ public:
|
|||
|
||||
void next() {
|
||||
m_prev_char = m_curr_char;
|
||||
m_curr_char = m_input->get();
|
||||
if (m_reader) {
|
||||
m_curr_char = m_reader->get();
|
||||
}
|
||||
else {
|
||||
m_curr_char = m_input->get();
|
||||
}
|
||||
m_pos++;
|
||||
}
|
||||
|
||||
|
|
@ -234,6 +260,7 @@ public:
|
|||
|
||||
dlexer():
|
||||
m_input(0),
|
||||
m_reader(0),
|
||||
m_prev_char(0),
|
||||
m_curr_char(0),
|
||||
m_line(1),
|
||||
|
|
@ -242,8 +269,9 @@ public:
|
|||
m_parsing_domains(false) {
|
||||
}
|
||||
|
||||
void set_stream(std::istream& s) {
|
||||
m_input = &s;
|
||||
void set_stream(std::istream* s, char_reader* r) {
|
||||
m_input = s;
|
||||
m_reader = r;
|
||||
next();
|
||||
}
|
||||
|
||||
|
|
@ -279,7 +307,10 @@ public:
|
|||
m_tok_pos = m_pos;
|
||||
next();
|
||||
while (m_curr_char != '"') {
|
||||
if (m_input->eof()) {
|
||||
if (m_input && m_input->eof()) {
|
||||
return TK_ERROR;
|
||||
}
|
||||
if (m_reader && m_reader->eof()) {
|
||||
return TK_ERROR;
|
||||
}
|
||||
if (m_curr_char == '\n') {
|
||||
|
|
@ -458,17 +489,17 @@ public:
|
|||
|
||||
virtual bool parse_file(char const * filename) {
|
||||
reset();
|
||||
if (filename != 0) {
|
||||
if (filename != 0) {
|
||||
set_path(filename);
|
||||
std::ifstream stream(filename);
|
||||
if (!stream) {
|
||||
char_reader reader(filename);
|
||||
if (!reader()) {
|
||||
get_err() << "ERROR: could not open file '" << filename << "'.\n";
|
||||
return false;
|
||||
}
|
||||
return parse_stream(stream);
|
||||
return parse_stream(0, &reader);
|
||||
}
|
||||
else {
|
||||
return parse_stream(std::cin);
|
||||
return parse_stream(&std::cin, 0);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -476,7 +507,7 @@ public:
|
|||
reset();
|
||||
std::string s(string);
|
||||
std::istringstream is(s);
|
||||
return parse_stream(is);
|
||||
return parse_stream(&is, 0);
|
||||
}
|
||||
|
||||
protected:
|
||||
|
|
@ -504,13 +535,13 @@ protected:
|
|||
return std::cerr;
|
||||
}
|
||||
|
||||
bool parse_stream(std::istream& is) {
|
||||
bool parse_stream(std::istream* is, char_reader* r) {
|
||||
bool result = false;
|
||||
try {
|
||||
m_error=false;
|
||||
dlexer lexer;
|
||||
m_lexer = &lexer;
|
||||
m_lexer->set_stream(is);
|
||||
m_lexer->set_stream(is, r);
|
||||
dtoken tok = m_lexer->next_token();
|
||||
tok = parse_domains(tok);
|
||||
tok = parse_decls(tok);
|
||||
|
|
@ -964,10 +995,11 @@ protected:
|
|||
}
|
||||
|
||||
dtoken parse_include(char const* filename, bool parsing_domain) {
|
||||
IF_VERBOSE(2, verbose_stream() << "include: " << filename << "\n";);
|
||||
std::string path(m_path);
|
||||
path += filename;
|
||||
std::ifstream stream(path.c_str());
|
||||
if (!stream) {
|
||||
char_reader stream(path.c_str());
|
||||
if (!stream()) {
|
||||
get_err() << "ERROR: could not open file '" << path << "'.\n";
|
||||
return TK_ERROR;
|
||||
}
|
||||
|
|
@ -975,7 +1007,7 @@ protected:
|
|||
dlexer lexer;
|
||||
{
|
||||
flet<dlexer*> lexer_let(m_lexer, &lexer);
|
||||
m_lexer->set_stream(stream);
|
||||
m_lexer->set_stream(0, &stream);
|
||||
tok = m_lexer->next_token();
|
||||
if(parsing_domain) {
|
||||
tok = parse_domains(tok);
|
||||
|
|
@ -991,15 +1023,16 @@ protected:
|
|||
dtoken parse_mapfile(dtoken tok, sort * s, char const* filename) {
|
||||
std::string path(m_path);
|
||||
path += filename;
|
||||
std::ifstream stream(path.c_str());
|
||||
if (!stream) {
|
||||
line_reader reader(path.c_str());
|
||||
|
||||
if (!reader()) {
|
||||
get_err() << "Warning: could not open file '" << path << "'.\n";
|
||||
return m_lexer->next_token();
|
||||
}
|
||||
|
||||
std::string line;
|
||||
while(read_line(stream, line)) {
|
||||
symbol sym=symbol(line.c_str());
|
||||
while(!reader.eof()) {
|
||||
symbol sym=symbol(reader.get_line());
|
||||
m_context.get_constant_number(s, sym);
|
||||
}
|
||||
return m_lexer->next_token();
|
||||
|
|
@ -1272,7 +1305,7 @@ private:
|
|||
|
||||
dlexer lexer;
|
||||
m_lexer = &lexer;
|
||||
m_lexer->set_stream(stm);
|
||||
m_lexer->set_stream(&stm, 0);
|
||||
dtoken tok = m_lexer->next_token();
|
||||
tok = parse_decls(tok);
|
||||
m_lexer = 0;
|
||||
|
|
|
|||
|
|
@ -509,7 +509,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
bool sparse_table::add_fact(const char * data) {
|
||||
verbose_action _va("add_fact", 3);
|
||||
verbose_action _va("add_fact", 10);
|
||||
m_data.write_into_reserve(data);
|
||||
return add_reserve_content();
|
||||
}
|
||||
|
|
@ -829,7 +829,6 @@ namespace datalog {
|
|||
|
||||
virtual table_base * operator()(const table_base & tb1, const table_base & tb2) {
|
||||
|
||||
verbose_action _va("join_project");
|
||||
const sparse_table & t1 = get(tb1);
|
||||
const sparse_table & t2 = get(tb2);
|
||||
|
||||
|
|
|
|||
|
|
@ -514,27 +514,13 @@ namespace datalog {
|
|||
SASSERT(m_last_result_relation);
|
||||
return m_last_result_relation->contains_fact(f);
|
||||
}
|
||||
|
||||
void rel_context::reset_tables() {
|
||||
get_rmanager().reset_saturated_marks();
|
||||
rule_set::decl2rules::iterator it = m_context.get_rules().begin_grouped_rules();
|
||||
rule_set::decl2rules::iterator end = m_context.get_rules().end_grouped_rules();
|
||||
for (; it != end; ++it) {
|
||||
func_decl* p = it->m_key;
|
||||
relation_base & rel = get_relation(p);
|
||||
rel.reset();
|
||||
}
|
||||
for (unsigned i = 0; i < m_table_facts.size(); ++i) {
|
||||
func_decl* pred = m_table_facts[i].first;
|
||||
relation_fact const& fact = m_table_facts[i].second;
|
||||
get_relation(pred).add_fact(fact);
|
||||
}
|
||||
}
|
||||
|
||||
void rel_context::add_fact(func_decl* pred, relation_fact const& fact) {
|
||||
get_rmanager().reset_saturated_marks();
|
||||
get_relation(pred).add_fact(fact);
|
||||
m_table_facts.push_back(std::make_pair(pred, fact));
|
||||
if (m_context.get_params().dump_aig().size()) {
|
||||
m_table_facts.push_back(std::make_pair(pred, fact));
|
||||
}
|
||||
}
|
||||
|
||||
void rel_context::add_fact(func_decl* pred, table_fact const& fact) {
|
||||
|
|
|
|||
|
|
@ -48,8 +48,6 @@ namespace datalog {
|
|||
|
||||
relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
|
||||
|
||||
void reset_tables();
|
||||
|
||||
lbool saturate(scoped_query& sq);
|
||||
|
||||
void set_cancel(bool f);
|
||||
|
|
|
|||
Loading…
Reference in a new issue