diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 9b7093d1e..28fe3ed33 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -48,7 +48,7 @@ namespace api {
         if (!m.has_plugin(name)) {
             m.register_plugin(name, alloc(datalog::dl_decl_plugin));
         }        
-        datalog::relation_manager& r = m_context.get_rmanager();
+        datalog::relation_manager& r = m_context.get_rel_context().get_rmanager();
         r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
     }        
     
@@ -295,7 +295,7 @@ extern "C" {
         {
             scoped_timer timer(timeout, &eh);
             try {
-                r = to_fixedpoint_ref(d)->ctx().dl_query(num_relations, to_func_decls(relations));
+                r = to_fixedpoint_ref(d)->ctx().rel_query(num_relations, to_func_decls(relations));
             }
             catch (z3_exception& ex) {
                 mk_c(c)->handle_exception(ex);
diff --git a/src/muz_qe/datalog_parser.cpp b/src/muz_qe/datalog_parser.cpp
index afda12858..cfe283410 100644
--- a/src/muz_qe/datalog_parser.cpp
+++ b/src/muz_qe/datalog_parser.cpp
@@ -1326,9 +1326,6 @@ private:
             throw default_exception("tuple file %s for undeclared predicate %s", 
                 m_current_file.c_str(), predicate_name.bare_str());
         }
-        if(!m_context.can_add_table_fact(pred)) {
-            NOT_IMPLEMENTED_YET();
-        }
         unsigned pred_arity = pred->get_arity();
         sort * const * arg_sorts = pred->get_domain();
 
diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp
index dd35cc870..27161320e 100644
--- a/src/muz_qe/dl_bmc_engine.cpp
+++ b/src/muz_qe/dl_bmc_engine.cpp
@@ -57,7 +57,6 @@ namespace datalog {
 
         m_ctx.ensure_opened();
         m_rules.reset();
-        m_ctx.get_rmanager().reset_relations();
         datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
         datalog::rule_set        old_rules(m_ctx.get_rules());
         datalog::rule_ref_vector query_rules(rule_manager);
diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp
index 99c7b86f5..d403b5b5c 100644
--- a/src/muz_qe/dl_compiler.cpp
+++ b/src/muz_qe/dl_compiler.cpp
@@ -42,7 +42,7 @@ namespace datalog {
             return;
         }
         relation_signature sig;
-        m_context.get_rmanager().from_predicate(pred, sig);
+        m_context.get_rel_context().get_rmanager().from_predicate(pred, sig);
         reg_idx reg = get_fresh_register(sig);
         e->get_data().m_value=reg;
 
@@ -563,7 +563,7 @@ namespace datalog {
                 }
                 SASSERT(is_app(e));
                 relation_sort arg_sort;
-                m_context.get_rmanager().from_predicate(neg_pred, i, arg_sort);
+                m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort);
                 reg_idx new_reg;
                 make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, acc);
 
@@ -1096,7 +1096,7 @@ namespace datalog {
         func_decl_set::iterator fdit = preds.begin();
         func_decl_set::iterator fdend = preds.end();
         for(; fdit!=fdend; ++fdit) {
-            if(!m_context.get_rmanager().is_saturated(*fdit)) {
+            if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) {
                 return false;
             }
         }
@@ -1181,7 +1181,7 @@ namespace datalog {
 
         acc.set_observer(0);
 
-        TRACE("dl", execution_code.display(m_context, tout););
+        TRACE("dl", execution_code.display(m_context.get_rel_context(), tout););
     }
 
 
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 228dbc572..0f9f1d520 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -24,18 +24,12 @@ Revision History:
 #include"arith_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"dl_table.h"
-#include"dl_sparse_table.h"
 #include"dl_table_relation.h"
-#include"dl_bound_relation.h"
-#include"dl_interval_relation.h"
-#include"dl_finite_product_relation.h"
-#include"dl_product_relation.h"
 #include"dl_rule_transformer.h"
 #include"dl_mk_coi_filter.h"
 #include"dl_mk_explanations.h"
 #include"dl_mk_filter_rules.h"
 #include"dl_mk_interp_tail_simplifier.h"
-#include"dl_mk_magic_sets.h"
 #include"dl_mk_rule_inliner.h"
 #include"dl_mk_simple_joins.h"
 #include"dl_mk_similarity_compressor.h"
@@ -44,9 +38,6 @@ Revision History:
 #include"dl_compiler.h"
 #include"dl_instruction.h"
 #include"dl_context.h"
-#ifndef _EXTERNAL_RELEASE
-#include"dl_skip_table.h"
-#endif
 #include"for_each_expr.h"
 #include"ast_smt_pp.h"
 #include"ast_smt2_pp.h"
@@ -189,7 +180,6 @@ namespace datalog {
         virtual ~restore_rules() {}
         
         virtual void undo(context& ctx) {
-            ctx.reset_tables();
             ctx.replace_rules(*m_old_rules);
             reset();
         }
@@ -209,7 +199,6 @@ namespace datalog {
         m_trail.push_scope();
         m_trail.push(restore_rules(m_rule_set));
         m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_background));
-        m_trail.push(restore_vec_size_trail<context,fact_vector>(m_table_facts));
     }
 
     void context::pop() {
@@ -233,7 +222,6 @@ namespace datalog {
         m_decl_util(m),
         m_rewriter(m),
         m_var_subst(m),
-        m_rmanager(*this),
         m_rule_manager(*this),
         m_trail(*this),
         m_pinned(m),
@@ -243,25 +231,11 @@ namespace datalog {
         m_background(m),
         m_closed(false),
         m_saturation_was_run(false),
-        m_last_result_relation(0),
         m_last_answer(m),
         m_engine(LAST_ENGINE),
         m_cancel(false) {
         
         //register plugins for builtin tables
-        get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
-
-#ifndef _EXTERNAL_RELEASE
-        get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager()));
-#endif
-
-        //register plugins for builtin relations
-
-        get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
-        get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
     }
 
     context::~context() {
@@ -272,14 +246,12 @@ namespace datalog {
         m_trail.reset();
         m_rule_set.reset();
         m_argument_var_names.reset();
-        m_output_preds.reset();
         m_preds.reset();
         m_preds_by_name.reset();
         reset_dealloc_values(m_sorts);
-        if (m_last_result_relation) {
-            m_last_result_relation->deallocate();
-            m_last_result_relation = 0;
-        }
+        m_pdr = 0;
+        m_bmc = 0;
+        m_rel = 0;
     }
 
     bool context::is_fact(app * head) const {
@@ -455,59 +427,13 @@ namespace datalog {
         return e->get_data().m_value[arg_index];
     }
 
-    relation_plugin & context::get_ordinary_relation_plugin(symbol relation_name) {
-        relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
-        if (!plugin) {
-            std::stringstream sstm;
-            sstm << "relation plugin " << relation_name << " does not exist";
-            throw default_exception(sstm.str());
-        }
-        if (plugin->is_product_relation()) {
-            throw default_exception("cannot request product relation directly");
-        }
-        if (plugin->is_sieve_relation()) {
-            throw default_exception("cannot request sieve relation directly");
-        }
-        if (plugin->is_finite_product_relation()) {
-            throw default_exception("cannot request finite product relation directly");
-        }
-        return *plugin;
-    }
 
     void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
             symbol const * relation_names) {
-        relation_manager & rmgr = get_rmanager();
-
-        family_id target_kind = null_family_id;
-        switch (relation_name_cnt) {
-        case 0: 
-            return;
-        case 1:
-            target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
-            break;
-        default: {
-            svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
-            family_id rel_kind;           // the aggregate kind of non-table plugins
-            for (unsigned i = 0; i < relation_name_cnt; i++) {
-                relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
-                rel_kinds.push_back(p.get_kind());                
-            }
-            if (rel_kinds.size() == 1) {
-                rel_kind = rel_kinds[0];
-            }
-            else {
-                relation_signature rel_sig;
-                //rmgr.from_predicate(pred, rel_sig);
-                product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
-                rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
-            }
-            target_kind = rel_kind;
-            break;
-        }       
+        if (relation_name_cnt > 0) {
+            ensure_rel();
+            m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names);
         }
-
-        SASSERT(target_kind != null_family_id);
-        get_rmanager().set_predicate_kind(pred, target_kind);
     }
 
     func_decl * context::mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix, 
@@ -517,19 +443,25 @@ namespace datalog {
 
         register_predicate(new_pred);
 
-        if (orig_pred) {
-            family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred);            
-            if (target_kind != null_family_id) {
-                get_rmanager().set_predicate_kind(new_pred, target_kind);
-            }
+        if (m_rel.get()) {
+            m_rel->inherit_predicate_kind(new_pred, orig_pred);
         }
         return new_pred;
     }
 
     void context::set_output_predicate(func_decl * pred) { 
-        if (!m_output_preds.contains(pred)) {
-            m_output_preds.insert(pred);
-        }
+        ensure_rel();
+        m_rel->set_output_predicate(pred);
+    }
+
+    bool context::is_output_predicate(func_decl * pred) {
+        ensure_rel();
+        return m_rel->is_output_predicate(pred); 
+    }
+
+    const decl_set & context::get_output_predicates() { 
+        ensure_rel();
+        return m_rel->get_output_predicates();
     }
 
     void context::add_rule(expr* rl, symbol const& name) {
@@ -562,7 +494,6 @@ namespace datalog {
             throw default_exception(strm.str());
         }
         rule_ref r(rules[0].get(), rm);
-        get_rmanager().reset_saturated_marks();
         rule_ref_vector const& rls = m_rule_set.get_rules();
         rule* old_rule = 0;
         for (unsigned i = 0; i < rls.size(); ++i) {
@@ -795,7 +726,6 @@ namespace datalog {
     }
 
     void context::add_rule(rule_ref& r) {
-        get_rmanager().reset_saturated_marks();
         m_rule_set.add_rule(r);
     }
 
@@ -809,12 +739,10 @@ namespace datalog {
 
     void context::add_fact(func_decl * pred, const relation_fact & fact) {
         if (get_engine() == DATALOG_ENGINE) {
-            get_rmanager().reset_saturated_marks();
-            get_relation(pred).add_fact(fact);
-            m_table_facts.push_back(std::make_pair(pred, fact));
+            ensure_rel();
+            m_rel->add_fact(pred, fact);
         }
         else {
-            ast_manager& m = get_manager();
             expr_ref rule(m.mk_app(pred, fact.size(), (expr*const*)fact.c_ptr()), m);
             add_rule(rule, symbol::null);
         }
@@ -832,26 +760,18 @@ namespace datalog {
         add_fact(head->get_decl(), fact);
     }
 
-    bool context::can_add_table_fact(func_decl * pred) {
-        return get_relation(pred).from_table();
-    }
-
     void context::add_table_fact(func_decl * pred, const table_fact & fact) {
-        relation_base & rel0 = get_relation(pred);
-        if (get_engine() != DATALOG_ENGINE || 
-            !can_add_table_fact(pred) || 
-            !rel0.from_table()) {
+        if (get_engine() == DATALOG_ENGINE) {
+            ensure_rel();
+            m_rel->add_fact(pred, fact);
+        }
+        else {
             relation_fact rfact(m);
             for (unsigned i = 0; i < fact.size(); ++i) {
                 rfact.push_back(m_decl_util.mk_numeral(fact[i], pred->get_domain()[i]));
             }
             add_fact(pred, rfact);
         }
-        else {
-            get_rmanager().reset_saturated_marks();
-            table_relation & rel = static_cast<table_relation &>(rel0);
-            rel.add_table_fact(fact);
-        }
     }
     
     void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) {
@@ -968,117 +888,14 @@ namespace datalog {
         if (m_pdr.get()) m_pdr->updt_params();        
     }
 
-    void context::collect_predicates(decl_set & res) {
-        unsigned rule_cnt = m_rule_set.get_num_rules();
-        for (unsigned rindex=0; rindex<rule_cnt; rindex++) {
-            rule * r = m_rule_set.get_rule(rindex);
-            res.insert(r->get_head()->get_decl());
-            unsigned tail_len = r->get_uninterpreted_tail_size();
-            for (unsigned tindex=0; tindex<tail_len; tindex++) {
-                res.insert(r->get_tail(tindex)->get_decl());
-            }
-        }
-        decl_set::iterator oit = m_output_preds.begin();
-        decl_set::iterator oend = m_output_preds.end();
-        for (; oit!=oend; ++oit) {
-            res.insert(*oit);
-        }
-        get_rmanager().collect_predicates(res);
+    void context::collect_predicates(decl_set& res) {
+        ensure_rel();
+        m_rel->collect_predicates(res);
     }
-    
-    void context::restrict_predicates( const decl_set & res ) {
-        set_intersection(m_output_preds, res);
-        get_rmanager().restrict_predicates(res);
-    }
-    
-    lbool context::dl_saturate() {
-        if (!m_closed) {
-            close();
-        }
-        bool time_limit = soft_timeout()!=0;
-        unsigned remaining_time_limit = soft_timeout();
-        unsigned restart_time = initial_restart_timeout();
-        
-        rule_set original_rules(get_rules());
-        decl_set original_predicates;
-        collect_predicates(original_predicates);
-                
-        instruction_block rules_code;
-        instruction_block termination_code;
-        execution_context ex_ctx(*this);
 
-        lbool result;
-
-        TRACE("dl", display(tout););
-
-        while (true) {
-            model_converter_ref mc; // Ignored in Datalog mode
-            proof_converter_ref pc; // Ignored in Datalog mode
-            transform_rules(mc, pc);
-            compiler::compile(*this, get_rules(), rules_code, termination_code);
-
-            TRACE("dl", rules_code.display(*this, tout); );
-
-            bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
-
-            if (time_limit || restart_time!=0) {
-                unsigned timeout = time_limit ? (restart_time!=0) ? 
-                    std::min(remaining_time_limit, restart_time)
-                    : remaining_time_limit : restart_time;
-                ex_ctx.set_timelimit(timeout);
-            }
-
-            bool early_termination = !rules_code.perform(ex_ctx);
-            ex_ctx.reset_timelimit();
-            VERIFY( termination_code.perform(ex_ctx) );
-
-            rules_code.process_all_costs();
-
-            IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream()););
-        
-            if (!early_termination) {
-                m_last_status = OK;
-                result = l_true;
-                break;
-            }
-
-            if (memory::above_high_watermark()) {
-                m_last_status = MEMOUT;
-                result = l_undef;
-                break;
-            }
-            if (timeout_after_this_round || m_cancel) {
-                m_last_status = TIMEOUT;
-                result = l_undef;
-                break;
-            }
-            SASSERT(restart_time!=0);
-            if (time_limit) {
-                SASSERT(remaining_time_limit>restart_time);
-                remaining_time_limit-=restart_time;
-            }
-            uint64 new_restart_time = static_cast<uint64>(restart_time)*initial_restart_timeout();
-            if (new_restart_time>UINT_MAX) {
-                restart_time=UINT_MAX;
-            }
-            else {
-                restart_time=static_cast<unsigned>(new_restart_time);
-            }
-
-            rules_code.reset();
-            termination_code.reset();
-            ex_ctx.reset();
-            reopen();
-            restrict_predicates(original_predicates);
-            replace_rules(original_rules);
-            close();
-        }
-        reopen();
-        restrict_predicates(original_predicates);
-        replace_rules(original_rules);
-        close();
-        TRACE("dl", ex_ctx.report_big_relations(100, tout););
-        return result;
+    void context::restrict_predicates(decl_set const& res) {
+        ensure_rel();
+        m_rel->restrict_predicates(res);
     }
 
     expr_ref context::get_background_assertion() {
@@ -1101,6 +918,7 @@ namespace datalog {
         m_cancel = true;
         if (m_pdr.get()) m_pdr->cancel();
         if (m_bmc.get()) m_bmc->cancel();
+        if (m_rel.get()) m_rel->cancel();
     }
 
     void context::cleanup() {
@@ -1180,7 +998,7 @@ namespace datalog {
         
         switch(get_engine()) {
         case DATALOG_ENGINE:
-            return dl_query(query);
+            return rel_query(query);
         case PDR_ENGINE:
         case QPDR_ENGINE:
             return pdr_query(query);
@@ -1189,18 +1007,14 @@ namespace datalog {
             return bmc_query(query);
         default:
             UNREACHABLE();
-            return dl_query(query);
+            return rel_query(query);
         }
     }
 
     void context::new_query() {
         flush_add_rules();
-        if (m_last_result_relation) {
-            m_last_result_relation->deallocate();
-            m_last_result_relation = 0;
-        }
         m_last_status = OK;
-        m_last_answer = get_manager().mk_true();
+        m_last_answer = 0;
     }
 
     model_ref context::get_model() {
@@ -1233,7 +1047,6 @@ namespace datalog {
 
     lbool context::pdr_query(expr* query) {
         ensure_pdr();
-        m_last_answer = 0; 
         return m_pdr->query(query);
     }
 
@@ -1245,218 +1058,25 @@ namespace datalog {
 
     lbool context::bmc_query(expr* query) {
         ensure_bmc();
-        m_last_answer = 0;
         return m_bmc->query(query);
     }
 
-#define BEGIN_QUERY()                           \
-    rule_set original_rules(get_rules());       \
-    decl_set original_preds;                    \
-    collect_predicates(original_preds);         \
-    bool was_closed = m_closed;                 \
-    if (m_closed) {                             \
-        reopen();                               \
-    }                                           \
-
-#define END_QUERY()                             \
-    reopen();                                   \
-    replace_rules(original_rules);              \
-    restrict_predicates(original_preds);        \
-                                                \
-    if (was_closed) {                           \
-        close();                                \
-    }                                           \
-
-    lbool context::dl_query(unsigned num_rels, func_decl * const* rels) {
-        BEGIN_QUERY();
-        for (unsigned i = 0; i < num_rels; ++i) {
-            set_output_predicate(rels[i]);
+    void context::ensure_rel() {
+        if (!m_rel.get()) {
+            m_rel = alloc(rel_context, *this);
         }
-        close();
-        reset_negated_tables();
-        lbool res = dl_saturate();
+    }
 
-        switch(res) {
-        case l_true: {
-            expr_ref_vector ans(m);
-            expr_ref e(m);
-            bool some_non_empty = num_rels == 0;
-            for (unsigned i = 0; i < num_rels; ++i) {
-                relation_base& rel = get_relation(rels[i]);
-                if (!rel.empty()) {
-                    some_non_empty = true;
-                }
-                rel.to_formula(e);
-                ans.push_back(e);
-            }
-            SASSERT(!m_last_result_relation);
-            if (some_non_empty) {
-                m_last_answer = m.mk_and(ans.size(), ans.c_ptr());
-            }
-            else {
-                m_last_answer = m.mk_false();
-                res = l_false;
-            }
-            break;
-        }            
-        case l_false:
-            m_last_answer = m.mk_false();
-            break;
-        case l_undef:
-            break;
-        }
-        END_QUERY();
-        return res;
+    lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {
+        ensure_rel();
+        return m_rel->query(num_rels, rels);
     }
     
-    lbool context::dl_query(expr* query) {
-        BEGIN_QUERY();
-        rule_manager& rm = get_rule_manager();
-        rule_ref qrule(rm);
-        rule_ref_vector qrules(rm);
-        func_decl_ref query_pred(get_manager());
-        try {
-            rm.mk_query(query, query_pred, qrules, qrule);
-        }
-        catch(default_exception& exn) {
-            close();
-            m_last_status = INPUT_ERROR;
-            throw exn;
-        }
-        try {            
-            add_rules(qrules);
-        }
-        catch (default_exception& exn) {
-            close();
-            m_last_status = INPUT_ERROR;
-            throw exn;
-        }
-        
-        set_output_predicate(qrule->get_head()->get_decl());
-        close();
-        reset_negated_tables();
-        
-        if (generate_explanations()) {
-            model_converter_ref mc; // ignored in Datalog mode
-            proof_converter_ref pc; // ignored in Datalog mode
-            rule_transformer transformer(*this);
-            //expl_plugin is deallocated when transformer goes out of scope
-            mk_explanations * expl_plugin = 
-                alloc(mk_explanations, *this, explanations_on_relation_level());
-            transformer.register_plugin(expl_plugin);
-            transform_rules(transformer, mc, pc);
-
-            //we will retrieve the predicate with explanations instead of the original query predicate
-            query_pred = expl_plugin->get_e_decl(query_pred);
-            const rule_vector & query_rules = get_rules().get_predicate_rules(query_pred);
-            SASSERT(query_rules.size()==1);
-            qrule = query_rules.back();
-        }
-
-        if (magic_sets_for_queries()) {
-            model_converter_ref mc; // Ignored in Datalog mode
-            proof_converter_ref pc; // Ignored in Datalog mode
-            rule_transformer transformer(*this);
-            transformer.register_plugin(alloc(mk_magic_sets, *this, qrule.get()));
-            transform_rules(transformer, mc, pc);
-        }
-
-        lbool res = dl_saturate();
-        
-        if (res != l_undef) {
-            m_last_result_relation = get_relation(query_pred).clone();
-            if (m_last_result_relation->empty()) {
-                res = l_false;
-                m_last_answer = m.mk_false();
-            }
-            else {
-                m_last_result_relation->to_formula(m_last_answer);
-            }
-        }
-        
-        END_QUERY();
-        return res;
+    lbool context::rel_query(expr* query) {
+        ensure_rel();
+        return m_rel->query(query);
     }
 
-    void context::reset_tables() {
-        get_rmanager().reset_saturated_marks();
-        rule_set::decl2rules::iterator it  = m_rule_set.begin_grouped_rules();
-        rule_set::decl2rules::iterator end = m_rule_set.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 context::reset_negated_tables() {
-        rule_set::pred_set_vector const & pred_sets = m_rule_set.get_strats();
-        bool non_empty = false;
-        for (unsigned i = 1; i < pred_sets.size(); ++i) {
-            func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
-            for (; it != end; ++it) {
-                func_decl* pred = *it;
-                relation_base & rel = get_relation(pred);
-                if (!rel.empty()) {
-                    non_empty = true;
-                    break;
-                }
-            }
-        }
-        if (!non_empty) {
-            return;
-        }
-        // collect predicates that depend on negation.
-        func_decl_set depends_on_negation;
-        for (unsigned i = 1; i < pred_sets.size(); ++i) {
-            bool change = true;
-            while (change) {
-                change = false;
-                func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
-                for (; it != end; ++it) {
-                    func_decl* pred = *it;
-                    if (depends_on_negation.contains(pred)) {
-                        continue;
-                    }
-                    rule_vector const& rules = m_rule_set.get_predicate_rules(pred);
-                    bool inserted = false;
-                    for (unsigned j = 0; !inserted && j < rules.size(); ++j) {
-                        rule* r = rules[j];
-                        unsigned psz = r->get_positive_tail_size();
-                        unsigned tsz = r->get_uninterpreted_tail_size();
-                        if (psz < tsz) {
-                            depends_on_negation.insert(pred);
-                            change = true;
-                            inserted = true;
-                        }
-                        for (unsigned k = 0; !inserted && k < tsz; ++k) {
-                            func_decl* tail_decl = r->get_tail(k)->get_decl();
-                            if (depends_on_negation.contains(tail_decl)) {
-                                depends_on_negation.insert(pred);
-                                change   = true;
-                                inserted = true;
-                            }
-                        }
-                    }
-                }
-            }
-        }        
-        func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end();
-        for (; it != end; ++it) {
-            func_decl* pred = *it;
-            relation_base & rel = get_relation(pred);
-            
-            if (!rel.empty()) {
-                TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";);
-                rel.reset();
-            }
-        }
-    }
     
     expr* context::get_answer_as_formula() {
         if (m_last_answer) {
@@ -1473,6 +1093,10 @@ namespace datalog {
             ensure_bmc();
             m_last_answer = m_bmc->get_answer();
             return m_last_answer.get();
+        case DATALOG_ENGINE:
+            ensure_rel();
+            m_last_answer = m_rel->get_last_answer();
+            return m_last_answer.get();
         default:
             UNREACHABLE();
         }
@@ -1533,8 +1157,8 @@ namespace datalog {
     execution_result context::get_status() { return m_last_status; }
 
     bool context::result_contains_fact(relation_fact const& f) {
-        SASSERT(m_last_result_relation);
-        return m_last_result_relation->contains_fact(f);
+        ensure_rel();
+        return m_rel->result_contains_fact(f);
     }
     
     // TBD: algebraic data-types declarations will not be printed.
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index 5dcb3e1fa..89446ce3b 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -35,11 +35,11 @@ Revision History:
 #include"dl_rule_set.h"
 #include"pdr_dl_interface.h"
 #include"dl_bmc_engine.h"
+#include"rel_context.h"
 #include"lbool.h"
 #include"statistics.h"
 #include"params.h"
 #include"trail.h"
-#include"dl_external_relation.h"
 #include"model_converter.h"
 #include"proof_converter.h"
 #include"model2expr.h"
@@ -75,7 +75,6 @@ namespace datalog {
         typedef map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> sym2decl;
         typedef obj_map<const func_decl, svector<symbol> > pred2syms;
         typedef obj_map<const sort, sort_domain*> sort_domain_map;
-        typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
 
         ast_manager &      m;
         smt_params &       m_fparams;
@@ -84,7 +83,6 @@ namespace datalog {
         dl_decl_util       m_decl_util;
         th_rewriter        m_rewriter;
         var_subst          m_var_subst;
-        relation_manager   m_rmanager;
         rule_manager       m_rule_manager;
 
         trail_stack<context> m_trail;
@@ -94,7 +92,6 @@ namespace datalog {
         func_decl_set      m_preds;
         sym2decl           m_preds_by_name;
         pred2syms          m_argument_var_names;
-        decl_set           m_output_preds;
         rule_set           m_rule_set;
         expr_ref_vector    m_rule_fmls;
         svector<symbol>    m_rule_names;
@@ -102,23 +99,20 @@ namespace datalog {
 
         scoped_ptr<pdr::dl_interface>   m_pdr;
         scoped_ptr<bmc>                 m_bmc;
+        scoped_ptr<rel_context>         m_rel;
 
         bool               m_closed;
         bool               m_saturation_was_run;
         execution_result   m_last_status;
-        relation_base *    m_last_result_relation;
         expr_ref           m_last_answer;
         DL_ENGINE          m_engine;
         volatile bool      m_cancel;
-        fact_vector        m_table_facts;
 
         bool is_fact(app * head) const;
         bool has_sort_domain(relation_sort s) const;
         sort_domain & get_sort_domain(relation_sort s);
         const sort_domain & get_sort_domain(relation_sort s) const;
 
-        relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
-
         class engine_type_proc;
 
 
@@ -130,25 +124,12 @@ namespace datalog {
         void push();
         void pop();
         
-        relation_base & get_relation(func_decl * pred) { return get_rmanager().get_relation(pred); }
-        relation_base * try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); }
-
         bool saturation_was_run() const { return m_saturation_was_run; }
         void notify_saturation_was_run() { m_saturation_was_run = true; }
 
-        /**
-           \brief Store the relation \c rel under the predicate \c pred. The \c context object
-           takes over the ownership of the relation object.
-        */
-        void store_relation(func_decl * pred, relation_base * rel) {
-            get_rmanager().store_relation(pred, rel);
-        }
-
         void configure_engine();
 
         ast_manager & get_manager() const { return m; }
-        relation_manager & get_rmanager() { return m_rmanager; }
-        const relation_manager & get_rmanager() const { return m_rmanager; }
         rule_manager & get_rule_manager() { return m_rule_manager; }
         smt_params & get_fparams() const { return m_fparams; }
         fixedpoint_params const&  get_params() const { return m_params; }
@@ -247,8 +228,8 @@ namespace datalog {
             symbol const *  relation_names);
 
         void set_output_predicate(func_decl * pred);
-        bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
-        const decl_set & get_output_predicates() const { return m_output_preds; }
+        bool is_output_predicate(func_decl * pred);
+        const decl_set & get_output_predicates();
 
         rule_set const & get_rules() { flush_add_rules(); return m_rule_set; }
 
@@ -314,7 +295,6 @@ namespace datalog {
            and there is no transformation of relation values before they are put into the
            table.
          */
-        bool can_add_table_fact(func_decl * pred);
         void add_table_fact(func_decl * pred, const table_fact & fact);
         void add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]);
 
@@ -323,6 +303,7 @@ namespace datalog {
         */
         void close();
         void ensure_closed();
+        bool is_closed() { return m_closed; }
 
         /**
            \brief Undo the effect of the \c close operation.
@@ -351,13 +332,10 @@ namespace datalog {
         void display_rules(std::ostream & out) const {
             m_rule_set.display(out);
         }
-        void display_facts(std::ostream & out) const {
-            m_rmanager.display(out);
-        }
 
         void display(std::ostream & out) const {
             display_rules(out);
-            display_facts(out);
+            if (m_rel) m_rel->display_facts(out);
         }
 
         void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out);
@@ -407,23 +385,16 @@ namespace datalog {
         /**
            Query multiple output relations.
         */
-        lbool dl_query(unsigned num_rels, func_decl * const* rels);
+        lbool rel_query(unsigned num_rels, func_decl * const* rels);
 
-        /**
-           Reset tables that are under negation.
-         */
-        void reset_negated_tables();
-
-        /**
-           Just reset all tables.
-        */
-        void reset_tables(); 
 
         /**
            \brief retrieve last proof status.
         */
         execution_result get_status();
 
+        void set_status(execution_result r) { m_last_status = r; }
+
         /**
            \brief retrieve formula corresponding to query that returns l_true.
            The formula describes one or more instances of the existential variables
@@ -446,29 +417,36 @@ namespace datalog {
          */
         bool result_contains_fact(relation_fact const& f);
 
+#if 0
         /**
            \brief display facts generated for query.
         */
         void display_output_facts(std::ostream & out) const {
-            m_rmanager.display_output_tables(out);
+            get_rel_context().get_rmanager().display_output_tables(out);
         }
+#endif
 
-        /**
-           \brief expose datalog saturation for test.
-        */
-        lbool dl_saturate();
+        rel_context& get_rel_context() { ensure_rel(); return *m_rel; }
 
     private:
 
+        /**
+           Just reset all tables.
+        */
+        void reset_tables(); 
+
+
         void flush_add_rules();
 
         void ensure_pdr();
 
         void ensure_bmc();
 
+        void ensure_rel();
+
         void new_query();
 
-        lbool dl_query(expr* query);
+        lbool rel_query(expr* query);
 
         lbool pdr_query(expr* query);
 
diff --git a/src/muz_qe/dl_costs.cpp b/src/muz_qe/dl_costs.cpp
index 0b7641093..fe085d7f7 100644
--- a/src/muz_qe/dl_costs.cpp
+++ b/src/muz_qe/dl_costs.cpp
@@ -115,7 +115,7 @@ namespace datalog {
     }
 
 
-    void accounted_object::output_profile(context & ctx, std::ostream & out) const {
+    void accounted_object::output_profile(std::ostream & out) const {
         costs c;
         get_total_cost(c);
         c.output(out);
diff --git a/src/muz_qe/dl_costs.h b/src/muz_qe/dl_costs.h
index 0fc60451d..16cfc16b1 100644
--- a/src/muz_qe/dl_costs.h
+++ b/src/muz_qe/dl_costs.h
@@ -79,7 +79,7 @@ namespace datalog {
         void process_costs();
 
         bool passes_output_thresholds(context & ctx) const;
-        void output_profile(context & ctx, std::ostream & out) const;
+        void output_profile(std::ostream & out) const;
 
     private:
         //private and undefined copy constructor and operator= to avoid the default ones
diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp
index 9d6e9036f..503ffec3b 100644
--- a/src/muz_qe/dl_instruction.cpp
+++ b/src/muz_qe/dl_instruction.cpp
@@ -33,11 +33,11 @@ namespace datalog {
     //
     // -----------------------------------
     
-    execution_context::execution_context(context & datalog_context) 
-        : m_datalog_context(datalog_context),
+    execution_context::execution_context(context & context) 
+        : m_context(context),
         m_stopwatch(0),
         m_timelimit_ms(0),
-        m_eager_emptiness_checking(datalog_context.eager_emptiness_checking()) {}
+        m_eager_emptiness_checking(context.eager_emptiness_checking()) {}
 
     execution_context::~execution_context() {
         reset();
@@ -135,12 +135,12 @@ namespace datalog {
         process_costs();
     }
 
-    void instruction::display_indented(context & ctx, std::ostream & out, std::string indentation) const {
+    void instruction::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const {
         out << indentation;
         display_head_impl(ctx, out);
         if (ctx.output_profile()) {
             out << " {";
-            output_profile(ctx, out);
+            output_profile(out);
             out << '}';
         }
         out << "\n";
@@ -157,10 +157,10 @@ namespace datalog {
         virtual bool perform(execution_context & ctx) {
             if (m_store) {
                 if (ctx.reg(m_reg)) {
-                    ctx.get_datalog_context().store_relation(m_pred, ctx.release_reg(m_reg));
+                    ctx.get_rel_context().store_relation(m_pred, ctx.release_reg(m_reg));
                 }
                 else {
-                    context & dctx = ctx.get_datalog_context();
+                    rel_context & dctx = ctx.get_rel_context();
                     relation_base * empty_rel;
                     //the object referenced by sig is valid only until we call dctx.store_relation()
                     const relation_signature & sig = dctx.get_relation(m_pred).get_signature();
@@ -169,7 +169,7 @@ namespace datalog {
                 }
             }
             else {
-                relation_base& rel = ctx.get_datalog_context().get_relation(m_pred);
+                relation_base& rel = ctx.get_rel_context().get_relation(m_pred);
                 if ((!ctx.eager_emptiness_checking() || !rel.empty())) {
                     ctx.set_reg(m_reg, rel.clone());
                 }
@@ -182,7 +182,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(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & 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 +213,7 @@ namespace datalog {
         virtual void make_annotations(execution_context & ctx) {
             ctx.set_register_annotation(m_reg, "alloc");
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "dealloc " << m_reg;
         }
     };
@@ -248,7 +248,7 @@ namespace datalog {
                 ctx.set_register_annotation(m_src, str);
             }
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt;
         }
     };
@@ -304,11 +304,11 @@ namespace datalog {
         virtual void make_annotations(execution_context & ctx) {
             m_body->make_annotations(ctx);
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "while";
             print_container(m_controls, out);
         }
-        virtual void display_body_impl(context & ctx, std::ostream & out, std::string indentation) const {
+        virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {
             m_body->display_indented(ctx, out, indentation+"    ");
         }
     };
@@ -349,9 +349,9 @@ namespace datalog {
             }
 
             TRACE("dl",
-                r1.get_signature().output(ctx.get_datalog_context().get_manager(), tout);
+                r1.get_signature().output(ctx.get_rel_context().get_manager(), tout);
                 tout<<":"<<r1.get_size_estimate_rows()<<" x ";
-                r2.get_signature().output(ctx.get_datalog_context().get_manager(), tout);
+                r2.get_signature().output(ctx.get_rel_context().get_manager(), tout);
                 tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";);
 
             try {
@@ -371,7 +371,7 @@ namespace datalog {
             }
 
             TRACE("dl", 
-                ctx.reg(m_res)->get_signature().output(ctx.get_datalog_context().get_manager(), tout);
+                ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);
                 tout<<":"<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";);
 
             if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
@@ -385,7 +385,7 @@ namespace datalog {
             ctx.get_register_annotation(m_rel1, a1);
             ctx.set_register_annotation(m_res, "join " + a1 + " " + a2);
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "join " << m_rel1;
             print_container(m_cols1, out);
             out << " and " << m_rel2;
@@ -431,10 +431,10 @@ namespace datalog {
         }
         virtual void make_annotations(execution_context & ctx) {
             std::stringstream a;
-            a << "filter_equal " << m_col << " val: " << ctx.get_datalog_context().get_rmanager().to_nice_string(m_value);
+            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(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "filter_equal " << m_reg << " col: " << m_col << " val: "
                 << ctx.get_rmanager().to_nice_string(m_value);
         }
@@ -476,7 +476,7 @@ namespace datalog {
             }
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "filter_identical " << m_reg << " ";
             print_container(m_cols, out);
         }
@@ -519,7 +519,7 @@ namespace datalog {
             }
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "filter_interpreted " << m_reg << " using "
                 << mk_pp(m_cond, m_cond.get_manager());
         }
@@ -624,7 +624,7 @@ namespace datalog {
                 ctx.set_register_annotation(m_delta, "delta of "+str);
             }
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & 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 +678,7 @@ namespace datalog {
 
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & 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 +739,7 @@ namespace datalog {
             }
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "join_project " << m_rel1;
             print_container(m_cols1, out);
             out << " and " << m_rel2;
@@ -800,7 +800,7 @@ namespace datalog {
             }
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & 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);
         }
@@ -809,7 +809,7 @@ namespace datalog {
             std::string s1 = "src";
             ctx.get_register_annotation(m_src, s1);
             s << "select equal project col " << m_col << " val: " 
-              << ctx.get_datalog_context().get_rmanager().to_nice_string(m_value) << " " << s1;
+              << ctx.get_rel_context().get_rmanager().to_nice_string(m_value) << " " << s1;
             ctx.set_register_annotation(m_result, s.str());            
         }
     };
@@ -854,7 +854,7 @@ namespace datalog {
             }
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "filter_by_negation on " << m_tgt;
             print_container(m_cols1, out);
             out << " with " << m_neg_rel;
@@ -887,12 +887,12 @@ namespace datalog {
         }
         virtual bool perform(execution_context & ctx) {
             ctx.make_empty(m_tgt);
-            relation_base * rel = ctx.get_datalog_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
+            relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
             rel->add_fact(m_fact);
             ctx.set_reg(m_tgt, rel);
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & 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]);
@@ -919,10 +919,10 @@ namespace datalog {
         instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {}
         virtual bool perform(execution_context & ctx) {
             ctx.make_empty(m_tgt);
-            ctx.set_reg(m_tgt, ctx.get_datalog_context().get_rmanager().mk_full_relation(m_sig, m_pred));
+            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(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "mk_total into " << m_tgt << " sort:" 
                 << ctx.get_rmanager().to_nice_string(m_sig);
         }
@@ -944,10 +944,10 @@ namespace datalog {
         instr_mark_saturated(ast_manager & m, func_decl * pred) 
             : m_pred(pred, m) {}
         virtual bool perform(execution_context & ctx) {
-            ctx.get_datalog_context().get_rmanager().mark_saturated(m_pred);
+            ctx.get_rel_context().get_rmanager().mark_saturated(m_pred);
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "mark_saturated " << m_pred->get_name().bare_str();
         }
         virtual void make_annotations(execution_context & ctx) {            
@@ -970,7 +970,7 @@ namespace datalog {
             }
             return true;
         }
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "instr_assert_signature of " << m_tgt << " signature:";
             print_container(m_sig, out);
         }
@@ -1019,7 +1019,7 @@ namespace datalog {
 
             TRACE("dl",      
                 tout <<"% ";
-                instr->display_head_impl(ctx.get_datalog_context(), tout);
+                  instr->display_head_impl(ctx.get_rel_context(), tout);
                 tout <<"\n";);
             success = !ctx.should_terminate() && instr->perform(ctx);
         }
@@ -1042,12 +1042,12 @@ namespace datalog {
         }
     }
 
-    void instruction_block::display_indented(context & ctx, std::ostream & out, std::string indentation) const {
+    void instruction_block::display_indented(rel_context & 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) {
             instruction * i = (*it);
-            if (i->passes_output_thresholds(ctx) || i->being_recorded()) {
+            if (i->passes_output_thresholds(ctx.get_context()) || i->being_recorded()) {
                 i->display_indented(ctx, out, indentation);
             }
         }
diff --git a/src/muz_qe/dl_instruction.h b/src/muz_qe/dl_instruction.h
index c44c860a0..89f95c860 100644
--- a/src/muz_qe/dl_instruction.h
+++ b/src/muz_qe/dl_instruction.h
@@ -58,7 +58,7 @@ namespace datalog {
     private:
         typedef u_map<std::string> reg_annotations;
 
-        context &           m_datalog_context;
+        context &           m_context;
         reg_vector          m_registers;
 
         reg_annotations     m_reg_annotation;
@@ -73,12 +73,12 @@ namespace datalog {
          */
         bool                m_eager_emptiness_checking;
     public:
-        execution_context(context & datalog_context);
+        execution_context(context & context);
         ~execution_context();
 
         void reset();
 
-        context & get_datalog_context() { return m_datalog_context; };
+        rel_context & get_rel_context() { return m_context.get_rel_context(); };
 
         void set_timelimit(unsigned time_in_ms);
         void reset_timelimit();
@@ -208,7 +208,7 @@ namespace datalog {
 
            The newline character at the end should not be printed.
         */
-        virtual void display_head_impl(context & ctx, std::ostream & out) const {
+        virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
             out << "<instruction>";
         }
         /**
@@ -216,7 +216,7 @@ namespace datalog {
 
            Each line must be prepended by \c indentation and ended by a newline character.
         */
-        virtual void display_body_impl(context & ctx, std::ostream & out, std::string indentation) const {}
+        virtual void display_body_impl(rel_context & 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 +227,10 @@ namespace datalog {
 
         virtual void make_annotations(execution_context & ctx)  = 0;
 
-        void display(context & ctx, std::ostream & out) const {
+        void display(rel_context & ctx, std::ostream & out) const {
             display_indented(ctx, out, "");
         }
-        void display_indented(context & ctx, std::ostream & out, std::string indentation) const;
+        void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const;
 
         static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt);
         /**
@@ -329,10 +329,10 @@ namespace datalog {
 
         void make_annotations(execution_context & ctx);
 
-        void display(context & ctx, std::ostream & out) const {
+        void display(rel_context & ctx, std::ostream & out) const {
             display_indented(ctx, out, "");
         }
-        void display_indented(context & ctx, std::ostream & out, std::string indentation) const;
+        void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const;
     };
 
 
diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp
index 425d3fb60..b4683bdbe 100644
--- a/src/muz_qe/dl_mk_explanations.cpp
+++ b/src/muz_qe/dl_mk_explanations.cpp
@@ -607,7 +607,7 @@ namespace datalog {
         m_e_sort = m_decl_util.mk_rule_sort();
         m_pinned.push_back(m_e_sort);
 
-        relation_manager & rmgr = ctx.get_rmanager();
+        relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
         symbol er_symbol = explanation_relation_plugin::get_name(relation_level);
         m_er_plugin = static_cast<explanation_relation_plugin *>(rmgr.get_relation_plugin(er_symbol));
         if(!m_er_plugin) {
@@ -640,7 +640,7 @@ namespace datalog {
     void mk_explanations::assign_rel_level_kind(func_decl * e_decl, func_decl * orig) {
         SASSERT(m_relation_level);
 
-        relation_manager & rmgr = m_context.get_rmanager();
+        relation_manager & rmgr = m_context.get_rel_context().get_rmanager();
         unsigned sz = e_decl->get_arity();
         relation_signature sig;
         rmgr.from_predicate(e_decl, sig);
@@ -884,7 +884,7 @@ namespace datalog {
         m_context.collect_predicates(m_original_preds);
 
         rule_set * res = alloc(rule_set, m_context);
-        transform_facts(m_context.get_rmanager());
+        transform_facts(m_context.get_rel_context().get_rmanager());
         transform_rules(source, *res);
         return res;
     }
diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp
index 668cbf939..373a90969 100644
--- a/src/muz_qe/dl_mk_magic_sets.cpp
+++ b/src/muz_qe/dl_mk_magic_sets.cpp
@@ -365,7 +365,7 @@ namespace datalog {
                 rule * r = *it;
                 transform_rule(task.m_adornment, r);
             }
-            if(!m_context.get_relation(task.m_pred).empty()) {
+            if(!m_context.get_rel_context().get_relation(task.m_pred).empty()) {
                 //we need a rule to copy facts that are already in a relation into the adorned
                 //relation (since out intentional predicates can have facts, not only rules)
                 create_transfer_rule(task);
diff --git a/src/muz_qe/dl_mk_partial_equiv.cpp b/src/muz_qe/dl_mk_partial_equiv.cpp
index 68f333b1b..367a15743 100644
--- a/src/muz_qe/dl_mk_partial_equiv.cpp
+++ b/src/muz_qe/dl_mk_partial_equiv.cpp
@@ -97,7 +97,7 @@ namespace datalog {
             return 0;
         }
 
-        relation_manager & rm = m_context.get_rmanager();
+        relation_manager & rm = m_context.get_rel_context().get_rmanager();
         rule_set::decl2rules::iterator it  = source.begin_grouped_rules();
         rule_set::decl2rules::iterator end = source.end_grouped_rules();
 
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index 9c9bf7abb..fa532ee6c 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -205,7 +205,7 @@ namespace datalog {
 
     void mk_rule_inliner::count_pred_occurrences(rule_set const & orig)
     {
-        m_context.get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
+        m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
 
         rule_set::iterator rend = orig.end();
         for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp
index 8225aa315..42a5ba367 100644
--- a/src/muz_qe/dl_mk_similarity_compressor.cpp
+++ b/src/muz_qe/dl_mk_similarity_compressor.cpp
@@ -361,7 +361,7 @@ namespace datalog {
             collect_orphan_consts(*it, const_infos, val_fact);
             m_context.add_fact(aux_pred, val_fact);
         }
-        m_context.get_rmanager().mark_saturated(aux_pred);
+        m_context.get_rel_context().get_rmanager().mark_saturated(aux_pred);
 
         app * new_head = r->get_head();
         ptr_vector<app> new_tail;
diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp
index da1f80a53..363a4f0f7 100644
--- a/src/muz_qe/dl_mk_simple_joins.cpp
+++ b/src/muz_qe/dl_mk_simple_joins.cpp
@@ -569,10 +569,11 @@ namespace datalog {
         cost estimate_size(app * t) const {
             func_decl * pred = t->get_decl();
             unsigned n=pred->get_arity();
-            if( (m_context.saturation_was_run() && m_context.get_rmanager().try_get_relation(pred))
-                || m_context.get_rmanager().is_saturated(pred)) {
-                SASSERT(m_context.get_rmanager().try_get_relation(pred)); //if it is saturated, it should exist
-                unsigned rel_size_int = m_context.get_relation(pred).get_size_estimate_rows();
+            relation_manager& rm = m_context.get_rel_context().get_rmanager();
+            if( (m_context.saturation_was_run() && rm.try_get_relation(pred))
+                || rm.is_saturated(pred)) {
+                SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist
+                unsigned rel_size_int = m_context.get_rel_context().get_relation(pred).get_size_estimate_rows();
                 if(rel_size_int!=0) {
                     cost rel_size = static_cast<cost>(rel_size_int);
                     cost curr_size = rel_size;
diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp
index d20ad5055..19c28c036 100644
--- a/src/muz_qe/dl_mk_subsumption_checker.cpp
+++ b/src/muz_qe/dl_mk_subsumption_checker.cpp
@@ -250,7 +250,7 @@ namespace datalog {
     }
 
     void mk_subsumption_checker::scan_for_relations_total_due_to_facts() {
-        relation_manager& rm = m_context.get_rmanager();
+        relation_manager& rm = m_context.get_rel_context().get_rmanager();
 
         decl_set candidate_preds;
         m_context.collect_predicates(candidate_preds);
diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp
index 000a70b22..e3db82759 100644
--- a/src/muz_qe/dl_mk_unbound_compressor.cpp
+++ b/src/muz_qe/dl_mk_unbound_compressor.cpp
@@ -337,7 +337,7 @@ namespace datalog {
         // TODO mc, pc
         m_modified = false;
 
-        m_context.get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
+        m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
 
         unsigned init_rule_cnt = source.get_num_rules();
         SASSERT(m_rules.empty());
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index 9b0af2554..dedd37a78 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -1014,7 +1014,7 @@ namespace datalog {
         out << '.';
         if (ctx.output_profile()) {
             out << " {";
-            output_profile(ctx, out);
+            output_profile(out);
             out << '}';
         }
         out << '\n';
diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg
index aa78dad3d..61f993c0a 100644
--- a/src/muz_qe/fixedpoint_params.pyg
+++ b/src/muz_qe/fixedpoint_params.pyg
@@ -30,25 +30,25 @@ def_module_params('fixedpoint',
                           ('print_with_fixedpoint_extensions', BOOL, True, "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"),
                           ('print_low_level_smt2', BOOL, False, "use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"),
                           ('print_with_variable_declarations', BOOL, True, "use variable declarations when displaying rules (instead of attempting to use original names)"),
-                          ('bfs_model_search', BOOL, True, "PDR: (default true) use BFS strategy for expanding model search"),    
-                          ('use_farkas', BOOL, True, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"),
-                          ('generate_proof_trace', BOOL, False, "PDR: (default false) trace for 'sat' answer as proof object"),
-                          ('flexible_trace', BOOL, False, "PDR: (default false) allow PDR generate long counter-examples "
+                          ('bfs_model_search', BOOL, True, "PDR: use BFS strategy for expanding model search"),    
+                          ('use_farkas', BOOL, True, "PDR: use lemma generator based on Farkas (for linear real arithmetic)"),
+                          ('generate_proof_trace', BOOL, False, "PDR: trace for 'sat' answer as proof object"),
+                          ('flexible_trace', BOOL, False, "PDR: allow PDR generate long counter-examples "
                                                           "by extending candidate trace within search area"),
-                          ('unfold_rules', UINT, 0, "PDR: (default 0) unfold rules statically using iterative squarring"),
-                          ('use_model_generalizer', BOOL, False, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"),
-                          ('validate_result', BOOL, False, "PDR (default false) validate result (by proof checking or model checking)"),
-                          ('simplify_formulas_pre', BOOL, False, "PDR: (default false) simplify derived formulas before inductive propagation"),
-                          ('simplify_formulas_post', BOOL, False, "PDR: (default false) simplify derived formulas after inductive propagation"),
-                          ('slice', BOOL, True, "PDR: (default true) simplify clause set using slicing"),
-                          ('coalesce_rules', BOOL, False, "BMC: (default false) coalesce rules"),
-                          ('use_multicore_generalizer', BOOL, False, "PDR: (default false) extract multiple cores for blocking states"),
-                          ('use_inductive_generalizer', BOOL, True, "PDR: (default true) generalize lemmas using induction strengthening"),
-                          ('cache_mode', UINT, 0, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search"),
-                          ('inductive_reachability_check', BOOL, False, "PDR: (default false) assume negation of the cube on the previous level when "
+                          ('unfold_rules', UINT, 0, "PDR: unfold rules statically using iterative squarring"),
+                          ('use_model_generalizer', BOOL, False, "PDR: use model for backwards propagation (instead of symbolic simulation)"),
+                          ('validate_result', BOOL, False, "PDR validate result (by proof checking or model checking)"),
+                          ('simplify_formulas_pre', BOOL, False, "PDR: simplify derived formulas before inductive propagation"),
+                          ('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"),
+                          ('slice', BOOL, True, "PDR: simplify clause set using slicing"),
+                          ('coalesce_rules', BOOL, False, "BMC: coalesce rules"),
+                          ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
+                          ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),
+                          ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"),
+                          ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when "
                                                                         "checking for reachability (not only during cube weakening)"),
-                          ('max_num_contexts', UINT, 500, "PDR: (default 500) maximal number of contexts to create"),
-                          ('try_minimize_core', BOOL, False, "PDR: (default false) try to reduce core size (before inductive minimization)"),
+                          ('max_num_contexts', UINT, 500, "PDR: maximal number of contexts to create"),
+                          ('try_minimize_core', BOOL, False, "PDR: try to reduce core size (before inductive minimization)"),
                           ('profile_timeout_milliseconds', UINT, 0, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"),
                           ('dbg_fpr_nonempty_relation_signature', BOOL, False,
                                      "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index 663f634c4..0482ece05 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -83,7 +83,6 @@ lbool dl_interface::query(expr * query) {
     m_pdr_rules.reset();
     m_refs.reset();
     m_pred2slice.reset();
-    m_ctx.get_rmanager().reset_relations();
     ast_manager& m =                      m_ctx.get_manager();
     datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
     datalog::rule_set        old_rules(m_ctx.get_rules());
diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp
new file mode 100644
index 000000000..1b4042ab9
--- /dev/null
+++ b/src/muz_qe/rel_context.cpp
@@ -0,0 +1,517 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    rel_context.cpp
+
+Abstract:
+
+    context for relational datalog engine.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-12-3.
+
+Revision History:
+
+    Extracted from dl_context
+
+--*/
+#include"rel_context.h"
+#include"dl_context.h"
+#include"dl_compiler.h"
+#include"dl_instruction.h"
+#include"dl_mk_explanations.h"
+#include"dl_mk_magic_sets.h"
+#include"dl_product_relation.h"
+#include"dl_bound_relation.h"
+#include"dl_interval_relation.h"
+#include"dl_finite_product_relation.h"
+#include"dl_sparse_table.h"
+#include"dl_table.h"
+#include"dl_table_relation.h"
+#ifndef _EXTERNAL_RELEASE
+#include"dl_skip_table.h"
+#endif
+
+namespace datalog {
+   
+    rel_context::rel_context(context& ctx)
+        : m_context(ctx), 
+          m(ctx.get_manager()),
+          m_rmanager(ctx),
+          m_answer(m), 
+          m_cancel(false), 
+          m_last_result_relation(0) {
+        get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
+        get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
+        get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
+        get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
+
+#ifndef _EXTERNAL_RELEASE
+        get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager()));
+#endif
+
+        //register plugins for builtin relations
+
+        get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
+        get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
+
+}
+
+    rel_context::~rel_context() {
+        if (m_last_result_relation) {
+            m_last_result_relation->deallocate();
+            m_last_result_relation = 0;
+        }        
+    }
+
+    void rel_context::collect_predicates(decl_set & res) {
+        unsigned rule_cnt = m_context.get_rules().get_num_rules();
+        for (unsigned rindex=0; rindex<rule_cnt; rindex++) {
+            rule * r = m_context.get_rules().get_rule(rindex);
+            res.insert(r->get_head()->get_decl());
+            unsigned tail_len = r->get_uninterpreted_tail_size();
+            for (unsigned tindex=0; tindex<tail_len; tindex++) {
+                res.insert(r->get_tail(tindex)->get_decl());
+            }
+        }
+        decl_set::iterator oit = m_output_preds.begin();
+        decl_set::iterator oend = m_output_preds.end();
+        for (; oit!=oend; ++oit) {
+            res.insert(*oit);
+        }
+        get_rmanager().collect_predicates(res);
+    }
+
+
+    lbool rel_context::saturate() {
+        m_context.ensure_closed();
+        
+        bool time_limit = m_context.soft_timeout()!=0;
+        unsigned remaining_time_limit = m_context.soft_timeout();
+        unsigned restart_time = m_context.initial_restart_timeout();
+        
+        rule_set original_rules(m_context.get_rules());
+        decl_set original_predicates;
+        m_context.collect_predicates(original_predicates);
+                
+        instruction_block rules_code;
+        instruction_block termination_code;
+        execution_context ex_ctx(m_context);
+
+        lbool result;
+
+        TRACE("dl", m_context.display(tout););
+
+        while (true) {
+            model_converter_ref mc; // Ignored in Datalog mode
+            proof_converter_ref pc; // Ignored in Datalog mode
+            m_context.transform_rules(mc, pc);
+            compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code);
+
+            TRACE("dl", rules_code.display(*this, tout); );
+
+            bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
+
+            if (time_limit || restart_time!=0) {
+                unsigned timeout = time_limit ? (restart_time!=0) ? 
+                    std::min(remaining_time_limit, restart_time)
+                    : remaining_time_limit : restart_time;
+                ex_ctx.set_timelimit(timeout);
+            }
+
+            bool early_termination = !rules_code.perform(ex_ctx);
+            ex_ctx.reset_timelimit();
+            VERIFY( termination_code.perform(ex_ctx) );
+
+            rules_code.process_all_costs();
+
+            IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream()););
+        
+            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) {
+                m_context.set_status(TIMEOUT);
+                result = l_undef;
+                break;
+            }
+            SASSERT(restart_time != 0);
+            if (time_limit) {
+                SASSERT(remaining_time_limit>restart_time);
+                remaining_time_limit -= restart_time;
+            }
+            uint64 new_restart_time = static_cast<uint64>(restart_time)*m_context.initial_restart_timeout();
+            if (new_restart_time > UINT_MAX) {
+                restart_time = UINT_MAX;
+            }
+            else {
+                restart_time = static_cast<unsigned>(new_restart_time);
+            }
+
+            rules_code.reset();
+            termination_code.reset();
+            ex_ctx.reset();
+            m_context.reopen();
+            restrict_predicates(original_predicates);
+            m_context.replace_rules(original_rules);
+            m_context.close();
+        }
+        m_context.reopen();
+        restrict_predicates(original_predicates);
+        m_context.replace_rules(original_rules);
+        m_context.close();
+        TRACE("dl", ex_ctx.report_big_relations(100, tout););
+        m_cancel = false;
+        return result;
+    }
+
+#define BEGIN_QUERY()                           \
+    rule_set original_rules(m_context.get_rules());       \
+    decl_set original_preds;                    \
+    m_context.collect_predicates(original_preds);       \
+    bool was_closed = m_context.is_closed();    \
+    if (was_closed) {                           \
+        m_context.reopen();                               \
+    }                                           \
+
+#define END_QUERY()                             \
+    m_context.reopen();                                   \
+    m_context.replace_rules(original_rules);              \
+    restrict_predicates(original_preds);        \
+                                                \
+    if (was_closed) {                           \
+        m_context.close();                                \
+    }                                           \
+ 
+    lbool rel_context::query(unsigned num_rels, func_decl * const* rels) {
+        get_rmanager().reset_saturated_marks();
+        BEGIN_QUERY();
+        for (unsigned i = 0; i < num_rels; ++i) {
+            set_output_predicate(rels[i]);
+        }
+        m_context.close();
+        reset_negated_tables();
+        lbool res = saturate();
+
+        switch(res) {
+        case l_true: {
+            expr_ref_vector ans(m);
+            expr_ref e(m);
+            bool some_non_empty = num_rels == 0;
+            for (unsigned i = 0; i < num_rels; ++i) {
+                relation_base& rel = get_relation(rels[i]);
+                if (!rel.empty()) {
+                    some_non_empty = true;
+                }
+                rel.to_formula(e);
+                ans.push_back(e);
+            }
+            SASSERT(!m_last_result_relation);
+            if (some_non_empty) {
+                m_answer = m.mk_and(ans.size(), ans.c_ptr());
+            }
+            else {
+                m_answer = m.mk_false();
+                res = l_false;
+            }
+            break;
+        }            
+        case l_false:
+            m_answer = m.mk_false();
+            break;
+        case l_undef:
+            break;
+        }
+        END_QUERY();
+        return res;
+    }
+
+    lbool rel_context::query(expr* query) {
+        get_rmanager().reset_saturated_marks();
+        BEGIN_QUERY();
+        rule_manager& rm = m_context.get_rule_manager();
+        rule_ref qrule(rm);
+        rule_ref_vector qrules(rm);
+        func_decl_ref query_pred(m);
+        try {
+            rm.mk_query(query, query_pred, qrules, qrule);
+        }
+        catch(default_exception& exn) {
+            m_context.close();
+            m_context.set_status(INPUT_ERROR);
+            throw exn;
+        }
+        try {            
+            m_context.add_rules(qrules);
+        }
+        catch (default_exception& exn) {
+            m_context.close();
+            m_context.set_status(INPUT_ERROR);
+            throw exn;
+        }
+        
+        set_output_predicate(qrule->get_head()->get_decl());
+        m_context.close();
+        reset_negated_tables();
+        
+        if (m_context.generate_explanations()) {
+            model_converter_ref mc; // ignored in Datalog mode
+            proof_converter_ref pc; // ignored in Datalog mode
+            rule_transformer transformer(m_context);
+            //expl_plugin is deallocated when transformer goes out of scope
+            mk_explanations * expl_plugin = 
+                alloc(mk_explanations, m_context, m_context.explanations_on_relation_level());
+            transformer.register_plugin(expl_plugin);
+            m_context.transform_rules(transformer, mc, pc);
+
+            //we will retrieve the predicate with explanations instead of the original query predicate
+            query_pred = expl_plugin->get_e_decl(query_pred);
+            const rule_vector & query_rules = m_context.get_rules().get_predicate_rules(query_pred);
+            SASSERT(query_rules.size()==1);
+            qrule = query_rules.back();
+        }
+
+        if (m_context.magic_sets_for_queries()) {
+            model_converter_ref mc; // Ignored in Datalog mode
+            proof_converter_ref pc; // Ignored in Datalog mode
+            rule_transformer transformer(m_context);
+            transformer.register_plugin(alloc(mk_magic_sets, m_context, qrule.get()));
+            m_context.transform_rules(transformer, mc, pc);
+        }
+
+        lbool res = saturate();
+        
+        if (res != l_undef) {
+            m_last_result_relation = get_relation(query_pred).clone();
+            if (m_last_result_relation->empty()) {
+                res = l_false;
+                m_answer = m.mk_false();
+            }
+            else {
+                m_last_result_relation->to_formula(m_answer);
+            }
+        }
+        
+        END_QUERY();
+        return res;
+    }
+
+    void rel_context::reset_negated_tables() {
+        rule_set::pred_set_vector const & pred_sets = m_context.get_rules().get_strats();
+        bool non_empty = false;
+        for (unsigned i = 1; i < pred_sets.size(); ++i) {
+            func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
+            for (; it != end; ++it) {
+                func_decl* pred = *it;
+                relation_base & rel = get_relation(pred);
+                if (!rel.empty()) {
+                    non_empty = true;
+                    break;
+                }
+            }
+        }
+        if (!non_empty) {
+            return;
+        }
+        // collect predicates that depend on negation.
+        func_decl_set depends_on_negation;
+        for (unsigned i = 1; i < pred_sets.size(); ++i) {
+            bool change = true;
+            while (change) {
+                change = false;
+                func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
+                for (; it != end; ++it) {
+                    func_decl* pred = *it;
+                    if (depends_on_negation.contains(pred)) {
+                        continue;
+                    }
+                    rule_vector const& rules = m_context.get_rules().get_predicate_rules(pred);
+                    bool inserted = false;
+                    for (unsigned j = 0; !inserted && j < rules.size(); ++j) {
+                        rule* r = rules[j];
+                        unsigned psz = r->get_positive_tail_size();
+                        unsigned tsz = r->get_uninterpreted_tail_size();
+                        if (psz < tsz) {
+                            depends_on_negation.insert(pred);
+                            change = true;
+                            inserted = true;
+                        }
+                        for (unsigned k = 0; !inserted && k < tsz; ++k) {
+                            func_decl* tail_decl = r->get_tail(k)->get_decl();
+                            if (depends_on_negation.contains(tail_decl)) {
+                                depends_on_negation.insert(pred);
+                                change   = true;
+                                inserted = true;
+                            }
+                        }
+                    }
+                }
+            }
+        }        
+        func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end();
+        for (; it != end; ++it) {
+            func_decl* pred = *it;
+            relation_base & rel = get_relation(pred);
+            
+            if (!rel.empty()) {
+                TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";);
+                rel.reset();
+            }
+        }
+    }
+
+    void rel_context::set_output_predicate(func_decl * pred) { 
+        if (!m_output_preds.contains(pred)) {
+            m_output_preds.insert(pred);
+        }
+    }
+
+    void rel_context::restrict_predicates( const decl_set & res ) {
+        set_intersection(m_output_preds, res);
+        get_rmanager().restrict_predicates(res);
+    }
+
+    relation_base & rel_context::get_relation(func_decl * pred)  { return get_rmanager().get_relation(pred); }
+    relation_base * rel_context::try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); }
+
+    relation_manager & rel_context::get_rmanager() { return m_rmanager; }
+
+    const relation_manager & rel_context::get_rmanager() const { return m_rmanager; }
+
+    bool rel_context::output_profile() const { return m_context.output_profile(); }
+
+
+    void rel_context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
+                                                   symbol const * relation_names) {
+
+        relation_manager & rmgr = get_rmanager();
+
+        family_id target_kind = null_family_id;
+        switch (relation_name_cnt) {
+        case 0: 
+            return;
+        case 1:
+            target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
+            break;
+        default: {
+            svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
+            family_id rel_kind;           // the aggregate kind of non-table plugins
+            for (unsigned i = 0; i < relation_name_cnt; i++) {
+                relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
+                rel_kinds.push_back(p.get_kind());                
+            }
+            if (rel_kinds.size() == 1) {
+                rel_kind = rel_kinds[0];
+            }
+            else {
+                relation_signature rel_sig;
+                //rmgr.from_predicate(pred, rel_sig);
+                product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
+                rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
+            }
+            target_kind = rel_kind;
+            break;
+        }       
+        }
+
+        SASSERT(target_kind != null_family_id);
+        get_rmanager().set_predicate_kind(pred, target_kind);
+    }
+
+    relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) {
+        relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
+        if (!plugin) {
+            std::stringstream sstm;
+            sstm << "relation plugin " << relation_name << " does not exist";
+            throw default_exception(sstm.str());
+        }
+        if (plugin->is_product_relation()) {
+            throw default_exception("cannot request product relation directly");
+        }
+        if (plugin->is_sieve_relation()) {
+            throw default_exception("cannot request sieve relation directly");
+        }
+        if (plugin->is_finite_product_relation()) {
+            throw default_exception("cannot request finite product relation directly");
+        }
+        return *plugin;
+    }
+
+    bool rel_context::result_contains_fact(relation_fact const& f) {
+        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));
+    }
+
+    void rel_context::add_fact(func_decl* pred, table_fact const& fact) {
+        get_rmanager().reset_saturated_marks();
+        relation_base & rel0 = get_relation(pred);
+        if (rel0.from_table()) {
+            table_relation & rel = static_cast<table_relation &>(rel0);
+            rel.add_table_fact(fact);
+            // TODO: table facts?
+        }
+        else {
+            relation_fact rfact(m);
+            for (unsigned i = 0; i < fact.size(); ++i) {
+                rfact.push_back(m_context.get_decl_util().mk_numeral(fact[i], pred->get_domain()[i]));
+            }
+            add_fact(pred, rfact);
+        }
+    }
+
+    void rel_context::store_relation(func_decl * pred, relation_base * rel) {
+        get_rmanager().store_relation(pred, rel);
+    }
+
+    void rel_context::inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) {
+        if (orig_pred) {
+            family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred);            
+            if (target_kind != null_family_id) {
+                get_rmanager().set_predicate_kind(new_pred, target_kind);
+            }
+        }
+    }
+
+    void rel_context::display_output_facts(std::ostream & out) const {
+        get_rmanager().display_output_tables(out);
+    }
+
+    void rel_context::display_facts(std::ostream& out) const {
+        get_rmanager().display(out);
+    }
+
+
+};
diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h
new file mode 100644
index 000000000..8e0ea4a16
--- /dev/null
+++ b/src/muz_qe/rel_context.h
@@ -0,0 +1,115 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    rel_context.h
+
+Abstract:
+
+    context for relational datalog engine.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-12-3.
+
+Revision History:
+
+    Extracted from dl_context
+
+--*/
+#ifndef _REL_CONTEXT_H_
+#define _REL_CONTEXT_H_
+#include "ast.h"
+#include "dl_relation_manager.h"
+#include "lbool.h"
+
+namespace datalog {
+
+    class context;
+
+    class rel_context {
+        typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
+
+        context&           m_context;
+        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;
+
+        void reset_negated_tables();
+
+        lbool saturate();
+        
+        relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
+        
+        void reset_tables();
+
+    public:
+        rel_context(context& ctx);
+
+        ~rel_context();
+
+        relation_manager & get_rmanager();
+        const relation_manager & get_rmanager() const;
+        ast_manager& get_manager() { return m; }
+        context&     get_context() { 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; }
+
+        bool output_profile() const;
+
+
+        lbool query(expr* q);
+        lbool query(unsigned num_rels, func_decl * const* rels);
+
+        void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
+                                          symbol const * relation_names);
+        
+        void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred);
+
+        void cancel() { m_cancel = true; }
+
+
+
+        /**
+           \brief Restrict the set of used predicates to \c res.
+
+           The function deallocates unsused relations, it does not deal with rules.
+         */
+        void restrict_predicates(const decl_set & res);
+
+        void collect_predicates(decl_set & res);        
+
+        void set_output_predicate(func_decl * pred);
+        bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
+        const decl_set & get_output_predicates() const { return m_output_preds; }
+
+
+        /**
+           \brief query result if it contains fact.
+         */
+        bool result_contains_fact(relation_fact const& f);
+
+        void add_fact(func_decl* pred, relation_fact const& fact);
+
+        void add_fact(func_decl* pred, table_fact const& fact);
+        
+        /**
+           \brief Store the relation \c rel under the predicate \c pred. The \c context object
+           takes over the ownership of the relation object.
+        */
+        void store_relation(func_decl * pred, relation_base * rel);
+
+        void display_output_facts(std::ostream & out) const;
+        void display_facts(std::ostream & out) const;
+
+
+    };
+};
+
+#endif /* _REL_CONTEXT_H_ */
diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp
index 1d001c349..44a9d9b66 100644
--- a/src/shell/datalog_frontend.cpp
+++ b/src/shell/datalog_frontend.cpp
@@ -86,7 +86,7 @@ static void display_statistics(
 
         out << "--------------\n";
         out << "instructions  \n";
-        code.display(ctx, out);
+        code.display(ctx.get_rel_context(), out);
 
         out << "--------------\n";
         out << "big relations \n";
@@ -94,7 +94,7 @@ static void display_statistics(
     }
     out << "--------------\n";
     out << "relation sizes\n";
-    ctx.get_rmanager().display_relation_sizes(out);
+    ctx.get_rel_context().get_rmanager().display_relation_sizes(out);
 
     if (verbose) {
         out << "--------------\n";
@@ -139,7 +139,7 @@ unsigned read_datalog(char const * file) {
     params.set_bool("default_table_checked", dl_params.m_default_table_checked);
 
     datalog::context ctx(m, s_params, params);
-    datalog::relation_manager & rmgr = ctx.get_rmanager();
+    datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
     datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable"));
     SASSERT(&inner_plg);
     rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr));
@@ -206,7 +206,7 @@ unsigned read_datalog(char const * file) {
             
             datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);
             
-            TRACE("dl_compiler", rules_code.display(ctx, tout););
+            TRACE("dl_compiler", rules_code.display(ctx.get_rel_context(), tout););
             
             rules_code.make_annotations(ex_ctx);
             
@@ -248,10 +248,10 @@ unsigned read_datalog(char const * file) {
         
 
         TRACE("dl_compiler", ctx.display(tout);
-              rules_code.display(ctx, tout););
+              rules_code.display(ctx.get_rel_context(), tout););
         
         if (ctx.get_params().output_tuples()) {
-            ctx.display_output_facts(std::cout);
+            ctx.get_rel_context().display_output_facts(std::cout);
         }
 
         display_statistics(