1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "muz/fp/datalog_parser.h"
8 #include "ast/ast_pp.h"
9 #include "ast/arith_decl_plugin.h"
10 #include "muz/base/dl_context.h"
11 #include "muz/fp/dl_register_engine.h"
12 #include "smt/params/smt_params.h"
13 #include "ast/reg_decl_plugins.h"
14
15 using namespace datalog;
16
17
dparse_string(char const * str)18 static void dparse_string(char const* str) {
19 ast_manager m;
20 smt_params params;
21 reg_decl_plugins(m);
22 register_engine re;
23 context ctx(m, re, params);
24 parser* p = parser::create(ctx,m);
25
26 bool res = p->parse_string(str);
27
28 if (res) {
29 std::cout << "Parsed\n"<<str<<"\n";
30 }
31 else {
32 std::cout << "Parser did not succeed on string\n"<<str<<"\n";
33 }
34 dealloc(p);
35 }
36
dparse_file(char const * file)37 static void dparse_file(char const* file) {
38 ast_manager m;
39 smt_params params;
40 reg_decl_plugins(m);
41 register_engine re;
42
43 context ctx(m, re, params);
44 parser* p = parser::create(ctx,m);
45
46 if (!p->parse_file(file)) {
47 std::cout << "Failed to parse file\n";
48 }
49 dealloc(p);
50 }
51
52
53
tst_datalog_parser()54 void tst_datalog_parser() {
55 dparse_string("\nH :- C1(X,a,b), C2(Y,a,X) .");
56 dparse_string("N 128\n\nH :- C1(X,a,b), C2(Y,a,X) .");
57 dparse_string("N 128\nI 128\n\nC1(x : N, y : N, z : I)\nC2(x : N, y : N, z : N)\nH :- C1(X,a,b), C2(Y,a,X) .");
58 dparse_string("\nH :- C1(X,a,b), nC2(Y,a,X) .");
59 dparse_string("\nH :- C1(X,a,b),nC2(Y,a,X).");
60 dparse_string("\nH :- C1(X,a,b),\\\nC2(Y,a,X).");
61 dparse_string("\nH :- C1(X,a\\,\\b), C2(Y,a,X) .");
62 }
63
tst_datalog_parser_file(char ** argv,int argc,int & i)64 void tst_datalog_parser_file(char** argv, int argc, int & i) {
65 if (i + 1 < argc) {
66 dparse_file(argv[i+1]);
67 i++;
68 }
69 }
70
71
72