mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'nikolaj' into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2012-12-06 07:42:50 -08:00
parent 3cefa0a1f7 dbde71c290
commit 294d40889f
6 changed files with 15 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/muz_qe/rel_context.h
View file

@ -41,8 +41,6 @@ namespace datalog {
fact_vector m_table_facts; fact_vector m_table_facts;
void reset_negated_tables(); void reset_negated_tables();
lbool saturate();
relation_plugin & get_ordinary_relation_plugin(symbol relation_name); 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_output_facts(std::ostream & out) const;
void display_facts(std::ostream & out) const; void display_facts(std::ostream & out) const;
lbool saturate();
}; };
}; };

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); dealloc(parser);
std::cerr << "Saturating...\n"; std::cerr << "Saturating...\n";
ctx.dl_saturate(); ctx.get_rel_context().saturate();
std::cerr << "Done\n"; 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) { void test_functional_columns(smt_params fparams, params_ref& params) {
ast_manager m; ast_manager m;
context ctx(m, fparams); context ctx(m, fparams);
rel_context& rctx = ctx.get_rel_context();
ctx.updt_params(params); ctx.updt_params(params);
relation_manager & rmgr(ctx.get_rmanager()); relation_manager & rmgr(rctx.get_rmanager());
sparse_table_plugin & plugin = 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); SASSERT(&plugin);
table_signature sig2; table_signature sig2;
sig2.push_back(2); sig2.push_back(2);
@ -126,9 +127,9 @@ namespace datalog {
context ctx(m, fparams); context ctx(m, fparams);
ctx.updt_params(params); ctx.updt_params(params);
dl_decl_util dl_util(m); 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); SASSERT(&rel_plugin);
finite_product_relation_plugin plg(rel_plugin, rmgr); finite_product_relation_plugin plg(rel_plugin, rmgr);

8
src/test/dl_query.cpp
View file

@ -57,7 +57,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
TRUSTME( p->parse_file(problem_file) ); TRUSTME( p->parse_file(problem_file) );
dealloc(p); 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 out_preds = ctx_b.get_output_predicates();
decl_set::iterator it = out_preds.begin(); 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())); func_decl * pred_q = ctx_q.try_get_predicate_decl(symbol(pred_b->get_name().bare_str()));
SASSERT(pred_q); 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_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()); SASSERT(sig_b.size()==sig_q.size());
std::cerr << "Queries on random facts...\n"; std::cerr << "Queries on random facts...\n";
@ -209,7 +209,7 @@ void tst_dl_query() {
TRUSTME( p->parse_file(problem_file) ); TRUSTME( p->parse_file(problem_file) );
dealloc(p); dealloc(p);
} }
ctx_base.dl_saturate(); ctx_base.get_rel_context().saturate();
for(unsigned use_restarts=0; use_restarts<=1; use_restarts++) { for(unsigned use_restarts=0; use_restarts<=1; use_restarts++) {
params.set_uint("initial_restart_timeout", use_restarts ? 100 : 0); 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; ast_manager ast_m;
context ctx(ast_m, params); context ctx(ast_m, params);
arith_util autil(ast_m); 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)); m.register_plugin(alloc(interval_relation_plugin, m));
interval_relation_plugin& ip = dynamic_cast<interval_relation_plugin&>(*m.get_relation_plugin(symbol("interval_relation"))); interval_relation_plugin& ip = dynamic_cast<interval_relation_plugin&>(*m.get_relation_plugin(symbol("interval_relation")));
SASSERT(&ip); SASSERT(&ip);
@ -115,7 +115,7 @@ namespace datalog {
ast_manager ast_m; ast_manager ast_m;
context ctx(ast_m, params); context ctx(ast_m, params);
arith_util autil(ast_m); 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)); m.register_plugin(alloc(bound_relation_plugin, m));
bound_relation_plugin& br = dynamic_cast<bound_relation_plugin&>(*m.get_relation_plugin(symbol("bound_relation"))); bound_relation_plugin& br = dynamic_cast<bound_relation_plugin&>(*m.get_relation_plugin(symbol("bound_relation")));
SASSERT(&br); 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; smt_params params;
ast_manager ast_m; ast_manager ast_m;
datalog::context ctx(ast_m, params); 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* _tbl = mk_table(m, sig);
datalog::table_base& table = *_tbl; datalog::table_base& table = *_tbl;