0

I'm using Z3 to evaluate datalog programmes write using the bddbddb format (http://bddbddb.sourceforge.net/).

How to express the fact that a relation is acyclic in bddbddb format ?

I mean a rule such this one in datalog

:- rel(X,Y), rel(Y,X).

Josep Ng
  • 43
  • 7
  • 1
    Yet your description is not really clear: Is your example cyclic or not? I would say that it depends on the implementation of `rel`. If you mean cyclic=recursive - bddbddb infers recursive usage and thus has no need to specify it in files. Or do you mean the relation graph - this is one contains cycles, yet this cannot even be inferred by bddbddb because it depends on rules and facts. – CoronA Jun 19 '18 at 10:34
  • i want to express the fact that a graph for instance should not contain a cycle using a datalog rule: :- rel(X,Y), rel(Y,X). My question is how to write it using the bddbddb Format. – Josep Ng Jun 19 '18 at 10:38
  • 1
    you want all tuples that satisfy `rel(X,Y), rel(Y,X)`? This is a query not a rule, isn't it? So it does not make so much sense to include it in a file. Defining a rule deriving all these tuples should not be hard. – CoronA Jun 19 '18 at 11:27
  • 1
    Have you tried `?- rel(X,Y), rel(Y,X).` Unfortunately the documentation of bddbddb is not online, but I remember that it was something similar. – CoronA Jun 19 '18 at 11:58
  • i tried ?- rel(X,Y), rel(Y,X). but it doesn't work. Yes my goal is to detect tuples which satisfy this rule rel(X,Y), rel(Y,X). which means tuples that create a cycle in the relation. – Josep Ng Jun 19 '18 at 12:20
  • i mean a programme like this one in Datalog: Z 64 edge(x: Z) input path(x : Z, y : Z) printtuples path(x,y):- edge(x,y). path(x,z) :- edge(x,y), path(y,z). :- path(x,y), path(y,x). edge(1,2). edge(2,1). edge(3,1). then i want to write it using bddbddb format. – Josep Ng Jun 19 '18 at 12:27
  • Try `rel(X,Y), rel(Y,X)?` or if this does not work with a single goal `goal(x,y)?` where `goal(X,Z) :- rel(X,Y), rel(Y,Z).` You may find inspiring tests [here](https://sourceforge.net/p/secflow/code/HEAD/tree/trunk/net.secflow.bddbddb/src/test/net/secflow/bddbddb/datalog/DatalogParserTest.java) (the bddbddb at this place is slightly modified). – CoronA Jun 19 '18 at 12:41
  • neither rel(X,Y), rel(Y,X)? nor goal(x,y)? where goal(X,Z) :- rel(X,Y), rel(Y,Z). works :/ – Josep Ng Jun 19 '18 at 12:52
  • what about `:- rel(X,Y), rel(Y,X)?` derived from [here](https://sourceforge.net/p/bddbddb/code/HEAD/tree/trunk/bddbddb/net/sf/bddbddb/DatalogParser.java). – CoronA Jun 19 '18 at 12:57
  • No, it gives me this error after executing "z3 file.datalog " : identifier at line 7 '' found ':-' ERROR: failed to parse file – Josep Ng Jun 19 '18 at 13:01
  • Should i just write the query in my file? or how to add queries to bddbddb file? – Josep Ng Jun 19 '18 at 13:20
  • I think the latest syntax was correct, yet it maybe only works outside of files. – CoronA Jun 19 '18 at 13:26
  • How can i write it outside of the file? – Josep Ng Jun 19 '18 at 13:45
  • I my memory the query syntax was part of the bddbddb commandline. But this does certainly not help you. Did you consider to write the tuple to `goal/2` (explained above) and query this relation with the client system? Unfortunately I do not know z3/py_datalog, but I think the solution might be found there. – CoronA Jun 19 '18 at 14:45
  • I would like to express this problem in the SMTLib Format and evaluate it using Z3. edge("som1","som3"). egde("som2","som4"). egde("som4","som1"). egde("som3","som4"). path(x,y) :- edge(x,y). % x and y are strings path(x,z) :- edge(x,y), edge(y,x). :-path(x,y), path(y,x). %cyclic path. My question is how to write the rule (or query) which detect the existence of a cycle in the relation path (this rule in basic datalog : " :- path(x,y), path(y,x)" ). – Josep Ng Jul 09 '18 at 13:14

0 Answers0