diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 5fa2486b4..b05532d14 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -41,8 +41,6 @@ namespace datalog { fact_vector m_table_facts; void reset_negated_tables(); - - lbool saturate(); relation_plugin & get_ordinary_relation_plugin(symbol relation_name); @@ -109,6 +107,7 @@ namespace datalog { void display_output_facts(std::ostream & out) const; void display_facts(std::ostream & out) const; + lbool saturate(); }; }; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 70f0ad811..691ec009d 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -29,6 +29,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_case_split_strategy = static_cast(p.case_split()); m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); + m_proof_mode = _p.get_bool("produce_proofs", false)? PGM_FINE : PGM_DISABLED; } void smt_params::updt_params(params_ref const & p) { diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 704c272ee..350ec333f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -283,6 +283,7 @@ namespace smt { if (!m_fparams) { m_fparams = alloc(smt_params, m_context->get_fparams()); m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free + m_fparams->m_proof_mode = m_manager.proof_mode(); } if (!m_aux_context) { symbol logic; diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index c004c531f..cdc9c52d9 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -60,7 +60,7 @@ void dl_context_saturate_file(params_ref & params, const char * f) { } dealloc(parser); std::cerr << "Saturating...\n"; - ctx.dl_saturate(); + ctx.get_rel_context().saturate(); std::cerr << "Done\n"; } diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp index 4b67b32af..3fd81bc81 100644 --- a/src/test/dl_product_relation.cpp +++ b/src/test/dl_product_relation.cpp @@ -22,11 +22,12 @@ namespace datalog { void test_functional_columns(smt_params fparams, params_ref& params) { ast_manager m; context ctx(m, fparams); + rel_context& rctx = ctx.get_rel_context(); ctx.updt_params(params); - relation_manager & rmgr(ctx.get_rmanager()); + relation_manager & rmgr(rctx.get_rmanager()); sparse_table_plugin & plugin = - static_cast(*ctx.get_rmanager().get_table_plugin(symbol("sparse"))); + static_cast(*rctx.get_rmanager().get_table_plugin(symbol("sparse"))); SASSERT(&plugin); table_signature sig2; sig2.push_back(2); @@ -126,9 +127,9 @@ namespace datalog { context ctx(m, fparams); ctx.updt_params(params); dl_decl_util dl_util(m); - relation_manager & rmgr = ctx.get_rmanager(); + relation_manager & rmgr = ctx.get_rel_context().get_rmanager(); - relation_plugin & rel_plugin = *ctx.get_rmanager().get_relation_plugin(params.get_sym("default_relation", symbol("sparse"))); + relation_plugin & rel_plugin = *rmgr.get_relation_plugin(params.get_sym("default_relation", symbol("sparse"))); SASSERT(&rel_plugin); finite_product_relation_plugin plg(rel_plugin, rmgr); diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index 712ae386a..5e61c1836 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -49,7 +49,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, dl_decl_util decl_util(m); - context ctx_q(m, fparams); + context ctx_q(m, fparams); params.set_bool(":magic-sets-for-queries", use_magic_sets); ctx_q.updt_params(params); { @@ -57,7 +57,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, TRUSTME( p->parse_file(problem_file) ); dealloc(p); } - relation_manager & rel_mgr_q = ctx_b.get_rmanager(); + relation_manager & rel_mgr_q = ctx_b.get_rel_context().get_rmanager(); decl_set out_preds = ctx_b.get_output_predicates(); decl_set::iterator it = out_preds.begin(); @@ -68,10 +68,10 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, func_decl * pred_q = ctx_q.try_get_predicate_decl(symbol(pred_b->get_name().bare_str())); SASSERT(pred_q); - relation_base & rel_b = ctx_b.get_relation(pred_b); + relation_base & rel_b = ctx_b.get_rel_context().get_relation(pred_b); relation_signature sig_b = rel_b.get_signature(); - relation_signature sig_q = ctx_q.get_relation(pred_q).get_signature(); + relation_signature sig_q = ctx_q.get_rel_context().get_relation(pred_q).get_signature(); SASSERT(sig_b.size()==sig_q.size()); std::cerr << "Queries on random facts...\n"; @@ -209,7 +209,7 @@ void tst_dl_query() { TRUSTME( p->parse_file(problem_file) ); dealloc(p); } - ctx_base.dl_saturate(); + ctx_base.get_rel_context().saturate(); for(unsigned use_restarts=0; use_restarts<=1; use_restarts++) { params.set_uint(":initial-restart-timeout", use_restarts ? 100 : 0); diff --git a/src/test/dl_relation.cpp b/src/test/dl_relation.cpp index fe8ba1730..5daf3dc9b 100644 --- a/src/test/dl_relation.cpp +++ b/src/test/dl_relation.cpp @@ -12,7 +12,7 @@ namespace datalog { ast_manager ast_m; context ctx(ast_m, params); arith_util autil(ast_m); - relation_manager & m = ctx.get_rmanager(); + relation_manager & m = ctx.get_rel_context().get_rmanager(); m.register_plugin(alloc(interval_relation_plugin, m)); interval_relation_plugin& ip = dynamic_cast(*m.get_relation_plugin(symbol("interval_relation"))); SASSERT(&ip); @@ -115,7 +115,7 @@ namespace datalog { ast_manager ast_m; context ctx(ast_m, params); arith_util autil(ast_m); - relation_manager & m = ctx.get_rmanager(); + relation_manager & m = ctx.get_rel_context().get_rmanager(); m.register_plugin(alloc(bound_relation_plugin, m)); bound_relation_plugin& br = dynamic_cast(*m.get_relation_plugin(symbol("bound_relation"))); SASSERT(&br); diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp index 6383dc1ab..0c8afcdc2 100644 --- a/src/test/dl_table.cpp +++ b/src/test/dl_table.cpp @@ -27,9 +27,9 @@ static void test_table(mk_table_fn mk_table) { smt_params params; ast_manager ast_m; datalog::context ctx(ast_m, params); - datalog::relation_manager & m = ctx.get_rmanager(); + datalog::relation_manager & m = ctx.get_rel_context().get_rmanager(); - ctx.get_rmanager().register_plugin(alloc(datalog::bitvector_table_plugin, ctx.get_rmanager())); + m.register_plugin(alloc(datalog::bitvector_table_plugin, m)); datalog::table_base* _tbl = mk_table(m, sig); datalog::table_base& table = *_tbl;