1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "ast/ast_pp.h"
8 #include "ast/arith_decl_plugin.h"
9 #include "ast/reg_decl_plugins.h"
10 #include "muz/fp/datalog_parser.h"
11 #include "muz/base/dl_context.h"
12 #include "smt/params/smt_params.h"
13 #include "muz/fp/dl_register_engine.h"
14
15 using namespace datalog;
16
17
tst_dl_context()18 void tst_dl_context() {
19
20 return;
21
22 #if 0
23 symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") };
24
25 const unsigned rel_cnt = sizeof(relations)/sizeof(symbol);
26 const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog";
27
28 params_ref params;
29 for(unsigned rel_index=0; rel_index<rel_cnt; rel_index++) {
30 params.set_sym("default_relation", relations[rel_index]);
31 for(int eager_checking=1; eager_checking>=0; eager_checking--) {
32 params.set_bool("eager_emptiness_checking", eager_checking!=0);
33
34 std::cerr << "Testing " << relations[rel_index] << "\n";
35 std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n";
36 dl_context_simple_query_test(params);
37 dl_context_saturate_file(params, test_file);
38 }
39 }
40 #endif
41
42 }
43
44
45 #if 0
46
47
48 static lbool dl_context_eval_unary_predicate(ast_manager & m, context & ctx, char const* problem_text,
49 const char * pred_name) {
50 parser* p = parser::create(ctx,m);
51 TRUSTME( p->parse_string(problem_text) );
52 dealloc(p);
53
54 func_decl * pred = ctx.try_get_predicate_decl(symbol(pred_name));
55 ENSURE(pred);
56 ENSURE(pred->get_arity()==1);
57 app_ref query_app(m.mk_app(pred, m.mk_var(0, pred->get_domain()[0])), m);
58
59 lbool status = ctx.query(query_app);
60 ENSURE(status != l_undef);
61 return status;
62 }
63
64 static void dl_context_simple_query_test(params_ref & params) {
65 ast_manager m;
66 reg_decl_plugins(m);
67 dl_decl_util decl_util(m);
68 register_engine re;
69 smt_params fparams;
70 context ctx(m, re, fparams);
71 ctx.updt_params(params);
72
73 /* lbool status = */ dl_context_eval_unary_predicate(m, ctx, "Z 64\n\nP(x:Z)\nP(\"a\").", "P");
74
75 #if 0
76 // TBD:
77 //zero corresponds to the first constant the datalog parser encountered, in our case "a"
78 app_ref c_0(decl_util.mk_constant(0, res1->get_signature()[0]), m);
79 app_ref c_1(decl_util.mk_constant(1, res1->get_signature()[0]), m);
80 relation_fact f(m);
81 f.push_back(c_0);
82 ENSURE(res1->contains_fact(f));
83 f[0]=c_1;
84 ENSURE(!res1->contains_fact(f));
85 #endif
86 }
87
88 void dl_context_saturate_file(params_ref & params, const char * f) {
89 ast_manager m;
90 dl_decl_util decl_util(m);
91 smt_params fparams;
92 register_engine re;
93 context ctx(m, re, fparams);
94 ctx.updt_params(params);
95
96 datalog::parser * parser = datalog::parser::create(ctx, m);
97 if (!parser || !parser->parse_file(f)) {
98 warning_msg("ERROR: failed to parse file");
99 dealloc(parser);
100 return;
101 }
102 dealloc(parser);
103 std::cerr << "Saturating...\n";
104 ctx.get_rel_context()->saturate();
105 std::cerr << "Done\n";
106 }
107 #endif
108