mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fixing unit tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-05 12:01:03 -08:00
parent 1cd1a42618
commit aeb3857391
8 changed files with 18 additions and 16 deletions

3
src/muz_qe/rel_context.h
View file

@ -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();
};
};

1
src/smt/params/smt_params.cpp
View file

@ -29,6 +29,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_case_split_strategy = static_cast<case_split_strategy>(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) {

1
src/smt/smt_model_checker.cpp
View file

@ -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;

2
src/test/dl_context.cpp
View file

@ -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";
}

9
src/test/dl_product_relation.cpp
View file

@ -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<sparse_table_plugin &>(*ctx.get_rmanager().get_table_plugin(symbol("sparse")));
static_cast<sparse_table_plugin &>(*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);

10
src/test/dl_query.cpp
View file

@ -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);

4
src/test/dl_relation.cpp
View file

@ -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<interval_relation_plugin&>(*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<bound_relation_plugin&>(*m.get_relation_plugin(symbol("bound_relation")));
SASSERT(&br);

4
src/test/dl_table.cpp
View file

@ -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;