mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

factor out relation context for datalog

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-03 15:13:45 -08:00
parent 67183ea08a
commit 72e09759ee
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/muz_qe/dl_cmds.cpp
View file

@ -44,6 +44,11 @@ struct dl_context {
scoped_ptr<datalog::context> m_context; scoped_ptr<datalog::context> m_context;
trail_stack<dl_context> m_trail; trail_stack<dl_context> m_trail;
fixedpoint_params const& get_params() {
init();
return m_context->get_params();
}
dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds): dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds):
m_params(m_params_ref), m_params(m_params_ref),
m_cmd(ctx), m_cmd(ctx),
@ -214,7 +219,7 @@ public:
datalog::context& dlctx = m_dl_ctx->dlctx(); datalog::context& dlctx = m_dl_ctx->dlctx();
set_background(ctx); set_background(ctx);
dlctx.updt_params(m_params); dlctx.updt_params(m_params);
unsigned timeout = m_dl_ctx->m_params.timeout(); unsigned timeout = m_dl_ctx->get_params().timeout();
cancel_eh<datalog::context> eh(dlctx); cancel_eh<datalog::context> eh(dlctx);
lbool status = l_undef; lbool status = l_undef;
{ {
@ -283,7 +288,7 @@ private:
} }
void print_answer(cmd_context& ctx) { void print_answer(cmd_context& ctx) {
if (m_dl_ctx->m_params.print_answer()) { if (m_dl_ctx->get_params().print_answer()) {
datalog::context& dlctx = m_dl_ctx->dlctx(); datalog::context& dlctx = m_dl_ctx->dlctx();
ast_manager& m = ctx.m(); ast_manager& m = ctx.m();
expr_ref query_result(dlctx.get_answer_as_formula(), m); expr_ref query_result(dlctx.get_answer_as_formula(), m);
@ -298,7 +303,7 @@ private:
} }
void print_statistics(cmd_context& ctx) { void print_statistics(cmd_context& ctx) {
if (m_dl_ctx->m_params.print_statistics()) { if (m_dl_ctx->get_params().print_statistics()) {
statistics st; statistics st;
datalog::context& dlctx = m_dl_ctx->dlctx(); datalog::context& dlctx = m_dl_ctx->dlctx();
unsigned long long max_mem = memory::get_max_used_memory(); unsigned long long max_mem = memory::get_max_used_memory();
@ -312,7 +317,7 @@ private:
} }
void print_certificate(cmd_context& ctx) { void print_certificate(cmd_context& ctx) {
if (m_dl_ctx->m_params.print_certificate()) { if (m_dl_ctx->get_params().print_certificate()) {
datalog::context& dlctx = m_dl_ctx->dlctx(); datalog::context& dlctx = m_dl_ctx->dlctx();
if (!dlctx.display_certificate(ctx.regular_stream())) { if (!dlctx.display_certificate(ctx.regular_stream())) {
throw cmd_exception("certificates are not supported for the selected engine"); throw cmd_exception("certificates are not supported for the selected engine");