Re: [iris-reasoner-support] some question about Using IRIS

[Florian F. <flo...@st...>]

Hi,
nice to see that you are trying IRIS.

Since you already know QL I would like to point out
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.5470
which might be a very helpful paper.

Furthermore, an external user of IRIS has created a more in-depth
documentation than the one that we currently have:
http://www.murat-knecht.de/schuerfen/irisdoc/html-multiple/index.html
I cannot guarantee for the correctness of all of this, but it is fairly
useful.

Then to your questions:

1.)
We implemented aggregates on a tool on-top of IRIS a while ago, however
this was for a specific use case and is likely not helpful in your case.
IRIS itself unfortunately does not implement aggregates right at the
moment, although it is something that has been on our todo-list for a while.

2.) Just using  equality like that is fine in general. Watch out for
different data types.


3.) This has to do with the IRIS evaluation model. Per default IRIS
starts with a set of facts and computes new facts in a bottom up fashion
whereas it is also possible to start with the query, decompose that and
gradually compute what is required to answer it. In the particular case
of the Fibonacci example this does not really make a difference in terms
of efficiency.

Now consider the rule:
fib(?n,?f):- ?n > 1, ?n - 2 = ?n2, fib(?n2,?f2), ?n - 1 = ?n1,
fib(?n1,?f1), ?f1 + ?f2 = ?f.
In that case the problem is that IRIS does not know the value of ?n when
it starts computing new values (for more details see
http://www.iris-reasoner.org/saferules)

To fix that you can i.e. do:
number(1).
number(?x) :- number(?y), ?y + 1 = ?x, ?y < 6.
#this just generates a sequence of natural numbers
fib(0,1).
fib(1,1).
fib(?n,?f):- ?n > 1, ?n - 2 = ?n2, fib(?n2,?f2), ?n - 1 = ?n1,
fib(?n1,?f1), ?f1 + ?f2 = ?f, number(?n).
?- fib(5,?x).

The purpose of this is to limit the range of ?n during the computation.

I have also cc'ed this to the official iris support mailing list, which
is the best place for questions.

Best,
Florian

lee youpeng wrote:
> Hi Mr. Fischer
>        I am a Master student from Tsinghua University China. Recently I
> try to use IRIS to build a source code search tool for Java kind like
> .QL from Semmle.
>        During the developement I found some questions about IRIS, could
> you give me some advise.
>       
>        1. Aggregate Function.
>        I need to count the result size of a query,is there some build-in
> aggregate function?
>  
>        2. Assignment.
>        Is there build-in assignment rule? or just use ?x + 0 =?y.
>  
>        3. Fail to do recursion rule.
>        I find a demo from DES(Datalog Education System) which calculate
> Fibonacci numbers. here is the program:
>  
>        fib(0,1).
>        fib(1,1).
>        fib(?n,?f):- ?n > 1, ?n - 2 = ?n2, fib(?n2,?f2), ?n - 1 = ?n1,
> fib(?n1,?f1), ?f1 + ?f2 = ?f.
>       
>        It works fine with DES,however, when run with IRIS, It never halt
> until I got out of memory error.
>        dose IRIS have some bug about such program? or something wrong
> with the program.
>  
>        Thank you for reading this.
>  
>  
>  
> --
> 
>        Best
> Wishes
> 
> YP Lee
> Master Candidate
> School of Software Engineering
> Tsinghua University, Beijing, P.R.China
> Postcode: 100084
> Tel: (86-10) 62778595
> Mobile: (86) 13811782249
> Email: lov...@gm... <mailto:lov...@gm...>
> 
> 黎云
> 清华大学软件学院在读硕士
> 清华大学14号楼155室
> 电话: 010 82330804
> 手机: 13811782249
> 电邮: lov...@gm... <mailto:lov...@gm...>