mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-12-12 12:21:34 -08:00
parent 89fb55a864
commit 8cb30d0505
1 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/rel/dl_instruction.cpp
View file

@ -581,7 +581,6 @@ namespace datalog {
bool perform(execution_context & ctx) override { bool perform(execution_context & ctx) override {
log_verbose(ctx); log_verbose(ctx);
if (!ctx.reg(m_src)) { if (!ctx.reg(m_src)) {
std::cout << "not " << m_src << "\n";
ctx.make_empty(m_res); ctx.make_empty(m_res);
return true; return true;
} }
@ -591,7 +590,6 @@ namespace datalog {
relation_base & reg = *ctx.reg(m_src); relation_base & reg = *ctx.reg(m_src);
TRACE("dl_verbose", reg.display(tout <<"pre-filter-interpreted-and-project:\n");); TRACE("dl_verbose", reg.display(tout <<"pre-filter-interpreted-and-project:\n"););
if (!find_fn(reg, fn)) { if (!find_fn(reg, fn)) {
std::cout << m_cond << "\n";
fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr()); fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr());
if (!fn) { if (!fn) {
throw default_exception(default_exception::fmt(), throw default_exception(default_exception::fmt(),
@ -604,7 +602,6 @@ namespace datalog {
ctx.set_reg(m_res, (*fn)(reg)); ctx.set_reg(m_res, (*fn)(reg));
if (ctx.reg(m_res)->fast_empty()) { if (ctx.reg(m_res)->fast_empty()) {
std::cout << "fast empty\n";
ctx.make_empty(m_res); ctx.make_empty(m_res);
} }
// TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n");); // TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n"););