diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index 57f7575ca..e3ba4b1cd 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -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(); }; diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 32f3f64ba..1567dff4f 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -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 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 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 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; diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp index 3b2dc333a..2c806971f 100644 --- a/src/muz/rel/dl_sparse_table.cpp +++ b/src/muz/rel/dl_sparse_table.cpp @@ -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); diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 02b00be39..3b5e07c41 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -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) { diff --git a/src/muz/rel/rel_context.h b/src/muz/rel/rel_context.h index 68a6fbd90..84b100415 100644 --- a/src/muz/rel/rel_context.h +++ b/src/muz/rel/rel_context.h @@ -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);