mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 23:26:30 +00:00
Code Activity

ensure engine is datalog for dl_table and dl_util tests

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-31 15:32:23 -07:00
parent 24e5a6ae3f
commit ebdf031c8f
6 changed files with 16 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/test/dl_table.cpp
View file

@ -23,10 +23,13 @@ static void test_table(mk_table_fn mk_table) {
sig.push_back(8);
sig.push_back(4);
smt_params params;
params_ref fp_params;
gparams::set("fp.engine", "datalog");
// fp_params.set_sym("fp.engine", symbol("datalog"));
ast_manager ast_m;
reg_decl_plugins(ast_m);
datalog::register_engine re;
datalog::context ctx(ast_m, re, params);
datalog::context ctx(ast_m, re, params, fp_params);
datalog::relation_manager & m = ctx.get_rel_context()->get_rmanager();
m.register_plugin(alloc(datalog::bitvector_table_plugin, m));
@ -48,13 +51,10 @@ static void test_table(mk_table_fn mk_table) {
table.add_fact(row2);
table.display(std::cout);
datalog::table_base::iterator it = table.begin();
datalog::table_base::iterator end = table.end();
for (; it != end; ++it) {
it->get_fact(row);
for (unsigned j = 0; j < row.size(); ++j) {
std::cout << row[j] << " ";
}
for (auto &r : table) {
r.get_fact(row);
for (auto v : row)
std::cout << v << " ";
std::cout << "\n";
}