From aeb385739167b3dc2a676399982a9ac3cf1f7cc2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Dec 2012 12:01:03 -0800 Subject: [PATCH 1/4] fixing unit tests Signed-off-by: Nikolaj Bjorner --- src/muz_qe/rel_context.h | 3 +-- src/smt/params/smt_params.cpp | 1 + src/smt/smt_model_checker.cpp | 1 + src/test/dl_context.cpp | 2 +- src/test/dl_product_relation.cpp | 9 +++++---- src/test/dl_query.cpp | 10 +++++----- src/test/dl_relation.cpp | 4 ++-- src/test/dl_table.cpp | 4 ++-- 8 files changed, 18 insertions(+), 16 deletions(-) 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; From 3b51597dbecd2624410f46bef502e8b68e419ed1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Dec 2012 12:05:07 -0800 Subject: [PATCH 2/4] fixing unit tests Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_checker.cpp | 1 - src/test/dl_query.cpp | 5 ----- 2 files changed, 6 deletions(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index cefdacef5..53f3af961 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -283,7 +283,6 @@ 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_query.cpp b/src/test/dl_query.cpp index a642be9d6..4dc770056 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -49,13 +49,8 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, dl_decl_util decl_util(m); -<<<<<<< HEAD - context ctx_q(m, fparams); - params.set_bool(":magic-sets-for-queries", use_magic_sets); -======= context ctx_q(m, fparams); params.set_bool("magic_sets_for_queries", use_magic_sets); ->>>>>>> 3736c5ea3b97521dad85cdc6262151fae2875ec5 ctx_q.updt_params(params); { parser* p = parser::create(ctx_q,m); From 53cb389398f9492137fd00f198eba1e004872d5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Dec 2012 13:05:14 -0800 Subject: [PATCH 3/4] fixing unit tests Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params.cpp | 49 +++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 src/smt/params/smt_params.cpp diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp new file mode 100644 index 000000000..70f0ad811 --- /dev/null +++ b/src/smt/params/smt_params.cpp @@ -0,0 +1,49 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + smt_params.cpp + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2008-02-20. + +Revision History: + +--*/ +#include"smt_params.h" +#include"smt_params_helper.hpp" + +void smt_params::updt_local_params(params_ref const & _p) { + smt_params_helper p(_p); + m_auto_config = p.auto_config(); + m_ematching = p.ematching(); + m_phase_selection = static_cast(p.phase_selection()); + m_restart_strategy = static_cast(p.restart_strategy()); + m_restart_factor = p.restart_factor(); + m_case_split_strategy = static_cast(p.case_split()); + m_delay_units = p.delay_units(); + m_delay_units_threshold = p.delay_units_threshold(); +} + +void smt_params::updt_params(params_ref const & p) { + preprocessor_params::updt_params(p); + qi_params::updt_params(p); + theory_arith_params::updt_params(p); + theory_bv_params::updt_params(p); + updt_local_params(p); +} + +void smt_params::updt_params(context_params const & p) { + m_auto_config = p.m_auto_config; + m_soft_timeout = p.m_timeout; + m_model = p.m_model; + m_model_validate = p.m_validate_model; + m_proof_mode = p.m_proof ? PGM_FINE : PGM_DISABLED; +} + From 188aea3fb109c0cff5196c57e0e016ba0e014e4f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Dec 2012 13:48:27 -0800 Subject: [PATCH 4/4] fix test Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 70f0ad811..f74798499 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -22,6 +22,8 @@ Revision History: void smt_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); m_auto_config = p.auto_config(); + m_random_seed = p.random_seed(); + m_relevancy_lvl = p.relevancy(); m_ematching = p.ematching(); m_phase_selection = static_cast(p.phase_selection()); m_restart_strategy = static_cast(p.restart_strategy()); @@ -29,6 +31,11 @@ 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_preprocess = _p.get_bool("preprocess", true); // hidden parameter + if (_p.get_bool("arith.greatest_error_pivot", false)) + m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR; + else if (_p.get_bool("arith.least_error_pivot", false)) + m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR; } void smt_params::updt_params(params_ref const & p) { @@ -43,7 +50,5 @@ void smt_params::updt_params(context_params const & p) { m_auto_config = p.m_auto_config; m_soft_timeout = p.m_timeout; m_model = p.m_model; - m_model_validate = p.m_validate_model; - m_proof_mode = p.m_proof ? PGM_FINE : PGM_DISABLED; + m_model_validate = p.m_model_validate; } -