From 1cece1c1fbec5d67699bcd34ab8f38869973f2e2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 27 Mar 2013 10:38:50 -0700 Subject: [PATCH] Datalog improvements: - add cancel status - display statistics on cancel (by me & Nikolaj) Signed-off-by: Nuno Lopes --- src/muz_qe/dl_cmds.cpp | 11 ++++-- src/muz_qe/dl_context.cpp | 25 ++++++++++++-- src/muz_qe/dl_context.h | 8 ++++- src/muz_qe/dl_instruction.cpp | 59 ++++++++++++++++++-------------- src/muz_qe/dl_instruction.h | 38 +++++++++++--------- src/muz_qe/dl_mk_array_blast.cpp | 2 +- src/muz_qe/dl_mk_bit_blast.cpp | 2 +- src/muz_qe/rel_context.cpp | 59 +++++++++++++++++++++----------- src/muz_qe/rel_context.h | 14 ++++---- src/shell/datalog_frontend.cpp | 1 - 10 files changed, 142 insertions(+), 77 deletions(-) diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index d49a8a671..aef14e051 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -234,7 +234,6 @@ public: catch (z3_exception& ex) { ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl; } - dlctx.cleanup(); } switch (status) { case l_false: @@ -250,6 +249,7 @@ public: ctx.regular_stream() << "unknown\n"; switch(dlctx.get_status()) { case datalog::INPUT_ERROR: + ctx.regular_stream() << "input error\n"; break; case datalog::MEMOUT: @@ -261,14 +261,21 @@ public: break; case datalog::OK: + UNREACHABLE(); + break; + + case datalog::CANCELED: + ctx.regular_stream() << "canceled\n"; + dlctx.display_profile(ctx.regular_stream()); break; default: - // exception was raised. + UNREACHABLE(); break; } break; } + dlctx.cleanup(); print_statistics(ctx); m_target = 0; } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 89f2fcf4a..592cfaccd 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -229,11 +229,13 @@ namespace datalog { m_pinned(m), m_vars(m), m_rule_set(*this), + m_transformed_rule_set(*this), m_rule_fmls(m), m_background(m), m_mc(0), m_closed(false), m_saturation_was_run(false), + m_last_status(OK), m_last_answer(m), m_engine(LAST_ENGINE), m_cancel(false) { @@ -873,6 +875,11 @@ namespace datalog { m_rule_set.add_rules(rs); } + void context::record_transformed_rules() { + m_transformed_rule_set.reset(); + m_transformed_rule_set.add_rules(m_rule_set); + } + void context::apply_default_transformation() { ensure_closed(); m_transf.reset(); @@ -942,18 +949,18 @@ namespace datalog { void context::cancel() { m_cancel = true; + m_last_status = CANCELED; m_transf.cancel(); if (m_pdr.get()) m_pdr->cancel(); if (m_bmc.get()) m_bmc->cancel(); - if (m_rel.get()) m_rel->cancel(); if (m_tab.get()) m_tab->cancel(); } void context::cleanup() { m_cancel = false; + m_last_status = OK; if (m_pdr.get()) m_pdr->cleanup(); if (m_bmc.get()) m_bmc->cleanup(); - if (m_rel.get()) m_rel->cleanup(); if (m_tab.get()) m_tab->cleanup(); } @@ -1178,6 +1185,20 @@ namespace datalog { } } + void context::display_profile(std::ostream& out) const { + out << "\n---------------\n"; + out << "Original rules\n"; + display_rules(out); + + out << "\n---------------\n"; + out << "Transformed rules\n"; + m_transformed_rule_set.display(out); + + if (m_rel) { + m_rel->display_profile(out); + } + } + void context::reset_statistics() { if (m_pdr) { m_pdr->reset_statistics(); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index d278d3abc..ddf200b70 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -52,7 +52,8 @@ namespace datalog { OK, TIMEOUT, MEMOUT, - INPUT_ERROR + INPUT_ERROR, + CANCELED }; class context { @@ -92,6 +93,7 @@ namespace datalog { sym2decl m_preds_by_name; pred2syms m_argument_var_names; rule_set m_rule_set; + rule_set m_transformed_rule_set; expr_ref_vector m_rule_fmls; svector m_rule_names; expr_ref_vector m_background; @@ -323,6 +325,7 @@ namespace datalog { void transform_rules(); void transform_rules(rule_transformer& transf); void replace_rules(rule_set & rs); + void record_transformed_rules(); void apply_default_transformation(); @@ -349,6 +352,8 @@ namespace datalog { void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out); + void display_profile(std::ostream& out) const; + // ----------------------------------- // // basic usage methods @@ -356,6 +361,7 @@ namespace datalog { // ----------------------------------- void cancel(); + bool canceled() const { return m_cancel; } void cleanup(); void reset_cancel() { cleanup(); } diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index 503ffec3b..401a42e98 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -58,14 +58,18 @@ namespace datalog { reset_timelimit(); } + rel_context& execution_context::get_rel_context() { + return m_context.get_rel_context(); + } + struct compare_size_proc { typedef std::pair pr; bool operator()(pr const& a, pr const& b) const { return a.second > b.second; } - }; - void execution_context::report_big_relations(unsigned threshold, std::ostream & out) { + + void execution_context::report_big_relations(unsigned threshold, std::ostream & out) const { unsigned n = register_count(); svector > sizes; size_t total_bytes = 0; @@ -110,6 +114,7 @@ namespace datalog { bool execution_context::should_terminate() { return + m_context.canceled() || memory::above_high_watermark() || (m_stopwatch && m_timelimit_ms != 0 && @@ -135,7 +140,7 @@ namespace datalog { process_costs(); } - void instruction::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const { + void instruction::display_indented(rel_context const & ctx, std::ostream & out, std::string indentation) const { out << indentation; display_head_impl(ctx, out); if (ctx.output_profile()) { @@ -182,7 +187,7 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str()); } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { const char * rel_name = m_pred->get_name().bare_str(); if (m_store) { out << "store " << m_reg << " into " << rel_name; @@ -213,7 +218,7 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { ctx.set_register_annotation(m_reg, "alloc"); } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "dealloc " << m_reg; } }; @@ -248,7 +253,7 @@ namespace datalog { ctx.set_register_annotation(m_src, str); } } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt; } }; @@ -304,11 +309,11 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { m_body->make_annotations(ctx); } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const { out << "while"; print_container(m_controls, out); } - virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const { + virtual void display_body_impl(rel_context const & ctx, std::ostream & out, std::string indentation) const { m_body->display_indented(ctx, out, indentation+" "); } }; @@ -385,7 +390,7 @@ namespace datalog { ctx.get_register_annotation(m_rel1, a1); ctx.set_register_annotation(m_res, "join " + a1 + " " + a2); } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const { out << "join " << m_rel1; print_container(m_cols1, out); out << " and " << m_rel2; @@ -434,7 +439,7 @@ namespace datalog { a << "filter_equal " << m_col << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); ctx.set_register_annotation(m_reg, a.str()); } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "filter_equal " << m_reg << " col: " << m_col << " val: " << ctx.get_rmanager().to_nice_string(m_value); } @@ -476,7 +481,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "filter_identical " << m_reg << " "; print_container(m_cols, out); } @@ -519,7 +524,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "filter_interpreted " << m_reg << " using " << mk_pp(m_cond, m_cond.get_manager()); } @@ -619,12 +624,16 @@ namespace datalog { return true; } virtual void make_annotations(execution_context & ctx) { - std::string str; - if (ctx.get_register_annotation(m_tgt, str) && m_delta!=execution_context::void_register) { - ctx.set_register_annotation(m_delta, "delta of "+str); + std::string str = "union"; + if (!ctx.get_register_annotation(m_tgt, str)) { + ctx.set_register_annotation(m_tgt, "union"); } + if (m_delta != execution_context::void_register) { + str = "delta of " + str; + } + ctx.set_register_annotation(m_delta, str); } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt; if (m_delta!=execution_context::void_register) { out << " with delta " << m_delta; @@ -678,7 +687,7 @@ namespace datalog { return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt; out << (m_projection ? " deleting columns " : " with cycle "); print_container(m_cols, out); @@ -739,7 +748,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "join_project " << m_rel1; print_container(m_cols1, out); out << " and " << m_rel2; @@ -800,7 +809,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col << " val: " << ctx.get_rmanager().to_nice_string(m_value); } @@ -854,7 +863,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "filter_by_negation on " << m_tgt; print_container(m_cols1, out); out << " with " << m_neg_rel; @@ -892,7 +901,7 @@ namespace datalog { ctx.set_reg(m_tgt, rel); return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "mk_unary_singleton into " << m_tgt << " sort:" << ctx.get_rmanager().to_nice_string(m_sig[0]) << " val:" << ctx.get_rmanager().to_nice_string(m_sig[0], m_fact[0]); @@ -922,7 +931,7 @@ namespace datalog { ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred)); return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "mk_total into " << m_tgt << " sort:" << ctx.get_rmanager().to_nice_string(m_sig); } @@ -947,7 +956,7 @@ namespace datalog { ctx.get_rel_context().get_rmanager().mark_saturated(m_pred); return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "mark_saturated " << m_pred->get_name().bare_str(); } virtual void make_annotations(execution_context & ctx) { @@ -970,7 +979,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { out << "instr_assert_signature of " << m_tgt << " signature:"; print_container(m_sig, out); } @@ -1042,7 +1051,7 @@ namespace datalog { } } - void instruction_block::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const { + void instruction_block::display_indented(rel_context const& ctx, std::ostream & out, std::string indentation) const { instr_seq_type::const_iterator it = m_data.begin(); instr_seq_type::const_iterator end = m_data.end(); for(; it!=end; ++it) { diff --git a/src/muz_qe/dl_instruction.h b/src/muz_qe/dl_instruction.h index 89f95c860..ae6310ba6 100644 --- a/src/muz_qe/dl_instruction.h +++ b/src/muz_qe/dl_instruction.h @@ -31,6 +31,7 @@ namespace datalog { class execution_context; class instruction_block; + class rel_context; inline void check_overflow(unsigned i) { if (i == UINT_MAX) { @@ -78,7 +79,7 @@ namespace datalog { void reset(); - rel_context & get_rel_context() { return m_context.get_rel_context(); }; + rel_context & get_rel_context(); void set_timelimit(unsigned time_in_ms); void reset_timelimit(); @@ -91,10 +92,9 @@ namespace datalog { If register contains zero, it should be treated as if it contains an empty relation. */ - reg_type reg(reg_idx i) { - if (i>=m_registers.size()) { - check_overflow(i); - m_registers.resize(i+1,0); + reg_type reg(reg_idx i) const { + if (i >= m_registers.size()) { + return 0; } return m_registers[i]; } @@ -102,27 +102,29 @@ namespace datalog { \brief Return value of the register and assign zero into it place. */ reg_type release_reg(reg_idx i) { - SASSERT(i=m_registers.size()) { + if (i >= m_registers.size()) { check_overflow(i); m_registers.resize(i+1,0); } - if(m_registers[i]) { + if (m_registers[i]) { m_registers[i]->deallocate(); } - m_registers[i]=val; + m_registers[i] = val; } + void make_empty(reg_idx i) { - if(reg(i)) { + if (reg(i)) { set_reg(i, 0); } } @@ -130,14 +132,16 @@ namespace datalog { unsigned register_count() const { return m_registers.size(); } + bool get_register_annotation(reg_idx reg, std::string & res) const { return m_reg_annotation.find(reg, res); } + void set_register_annotation(reg_idx reg, std::string str) { m_reg_annotation.insert(reg, str); } - void report_big_relations(unsigned threshold, std::ostream & out); + void report_big_relations(unsigned threshold, std::ostream & out) const; }; @@ -208,7 +212,7 @@ namespace datalog { The newline character at the end should not be printed. */ - virtual void display_head_impl(rel_context & ctx, std::ostream & out) const { + virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const { out << ""; } /** @@ -216,7 +220,7 @@ namespace datalog { Each line must be prepended by \c indentation and ended by a newline character. */ - virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {} + virtual void display_body_impl(rel_context const & ctx, std::ostream & out, std::string indentation) const {} public: typedef execution_context::reg_type reg_type; typedef execution_context::reg_idx reg_idx; @@ -227,10 +231,10 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) = 0; - void display(rel_context & ctx, std::ostream & out) const { + void display(rel_context const& ctx, std::ostream & out) const { display_indented(ctx, out, ""); } - void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const; + void display_indented(rel_context const & ctx, std::ostream & out, std::string indentation) const; static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt); /** @@ -329,10 +333,10 @@ namespace datalog { void make_annotations(execution_context & ctx); - void display(rel_context & ctx, std::ostream & out) const { + void display(rel_context const & ctx, std::ostream & out) const { display_indented(ctx, out, ""); } - void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const; + void display_indented(rel_context const & ctx, std::ostream & out, std::string indentation) const; }; diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index 537b0b5ac..048269c5a 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -213,7 +213,7 @@ namespace datalog { rule_set* rules = alloc(rule_set, m_ctx); rule_set::iterator it = source.begin(), end = source.end(); bool change = false; - for (; it != end; ++it) { + for (; !m_ctx.canceled() && it != end; ++it) { change = blast(**it, *rules) || change; } if (!change) { diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index e6612022f..338eed0b4 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -265,7 +265,7 @@ namespace datalog { expr_ref fml(m); reset(); rule_set * result = alloc(rule_set, m_context); - for (unsigned i = 0; i < sz; ++i) { + for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) { rule * r = source.get_rule(i); r->to_formula(fml); if (blast(r, fml)) { diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 8e22a704c..c79acf67f 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -39,8 +39,8 @@ namespace datalog { m(ctx.get_manager()), m_rmanager(ctx), m_answer(m), - m_cancel(false), - m_last_result_relation(0) { + m_last_result_relation(0), + m_ectx(ctx) { // register plugins for builtin tables @@ -94,9 +94,9 @@ namespace datalog { decl_set original_predicates; m_context.collect_predicates(original_predicates); - instruction_block rules_code; + m_code.reset(); instruction_block termination_code; - execution_context ex_ctx(m_context); + m_ectx.reset(); lbool result; @@ -104,9 +104,13 @@ namespace datalog { while (true) { m_context.transform_rules(); - compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code); + if (m_context.canceled()) { + result = l_undef; + break; + } + compiler::compile(m_context, m_context.get_rules(), m_code, termination_code); - TRACE("dl", rules_code.display(*this, tout); ); + TRACE("dl", m_code.display(*this, tout); ); bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time); @@ -114,29 +118,32 @@ namespace datalog { unsigned timeout = time_limit ? (restart_time!=0) ? std::min(remaining_time_limit, restart_time) : remaining_time_limit : restart_time; - ex_ctx.set_timelimit(timeout); + m_ectx.set_timelimit(timeout); } - bool early_termination = !rules_code.perform(ex_ctx); - ex_ctx.reset_timelimit(); - VERIFY( termination_code.perform(ex_ctx) ); + bool early_termination = !m_code.perform(m_ectx); + m_ectx.reset_timelimit(); + VERIFY( termination_code.perform(m_ectx) || m_context.canceled()); - rules_code.process_all_costs(); + m_code.process_all_costs(); - IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream());); - + IF_VERBOSE(10, m_ectx.report_big_relations(1000, verbose_stream());); + + if (m_context.canceled()) { + result = l_undef; + break; + } if (!early_termination) { m_context.set_status(OK); result = l_true; break; } - if (memory::above_high_watermark()) { m_context.set_status(MEMOUT); result = l_undef; break; } - if (timeout_after_this_round || m_cancel) { + if (timeout_after_this_round) { m_context.set_status(TIMEOUT); result = l_undef; break; @@ -154,9 +161,7 @@ namespace datalog { restart_time = static_cast(new_restart_time); } - rules_code.reset(); - termination_code.reset(); - ex_ctx.reset(); + termination_code.reset(); m_context.reopen(); restrict_predicates(original_predicates); m_context.replace_rules(original_rules); @@ -164,10 +169,12 @@ namespace datalog { } m_context.reopen(); restrict_predicates(original_predicates); + m_context.record_transformed_rules(); m_context.replace_rules(original_rules); m_context.close(); - TRACE("dl", ex_ctx.report_big_relations(100, tout);); - m_cancel = false; + TRACE("dl", m_ectx.report_big_relations(100, tout);); + m_code.process_all_costs(); + m_code.make_annotations(m_ectx); return result; } @@ -504,5 +511,17 @@ namespace datalog { get_rmanager().display(out); } + void rel_context::display_profile(std::ostream& out) const { + out << "\n--------------\n"; + out << "Instructions\n"; + m_code.display(*this, out); + + out << "\n--------------\n"; + out << "Big relations\n"; + m_ectx.report_big_relations(1000, out); + + get_rmanager().display_relation_sizes(out); + } + }; diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index b05532d14..2e2b5cd9d 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -22,6 +22,7 @@ Revision History: #define _REL_CONTEXT_H_ #include "ast.h" #include "dl_relation_manager.h" +#include "dl_instruction.h" #include "lbool.h" namespace datalog { @@ -35,10 +36,11 @@ namespace datalog { ast_manager& m; relation_manager m_rmanager; expr_ref m_answer; - volatile bool m_cancel; relation_base * m_last_result_relation; decl_set m_output_preds; fact_vector m_table_facts; + execution_context m_ectx; + instruction_block m_code; void reset_negated_tables(); @@ -53,8 +55,8 @@ namespace datalog { relation_manager & get_rmanager(); const relation_manager & get_rmanager() const; - ast_manager& get_manager() { return m; } - context& get_context() { return m_context; } + ast_manager& get_manager() const { return m; } + context& get_context() const { return m_context; } relation_base & get_relation(func_decl * pred); relation_base * try_get_relation(func_decl * pred) const; expr_ref get_last_answer() { return m_answer; } @@ -70,10 +72,6 @@ namespace datalog { void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred); - void cancel() { m_cancel = true; } - - void cleanup() { m_cancel = false; } - /** \brief Restrict the set of used predicates to \c res. @@ -107,6 +105,8 @@ namespace datalog { void display_output_facts(std::ostream & out) const; void display_facts(std::ostream & out) const; + void display_profile(std::ostream& out) const; + lbool saturate(); }; diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 07052609e..fe2699504 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -209,7 +209,6 @@ unsigned read_datalog(char const * file) { rules_code.make_annotations(ex_ctx); ex_ctx.set_timelimit(timeout); - SASSERT(!ex_ctx.should_terminate()); early_termination = !rules_code.perform(ex_ctx); if(early_termination) {