Re[7]: Z3 theorem prover и вывод типов
От: vdimas Россия  
Дата: 10.10.10 16:34
Оценка:
Здравствуйте, catbert, Вы писали:

Поторопился, там ошибка, в умножении цепочек вывода надо было делать как-то так:
...
        // конкатенируем 2 цепочки вывода, т.е. полностью перемножаем два множества
        foreach(Iterator<Term> parent_N in chainParent) {
            foreach(Iterator<Term> male_M in chainMale) 
                yield return concatenate(parent_N, male_M);
...


где concatenate типа так:
Iterator<T> concatenate(Iterator<T> a, Iterator<T> b) {
    foreach(T ta in a)
        yield return ta;

    foreach(T tb in b)
        yield return tb;
}


Но, в любом случае, это была просто демонстрация для сравнения затрат у интерпретируемого варианта и компиллируемого.
Re[7]: Z3 theorem prover и вывод типов
От: Трурль  
Дата: 19.10.10 05:16
Оценка:
Здравствуйте, catbert, Вы писали:

C>Допустим есть такая программа:

C>
C>father(X, Y) :- parent(X, Y), male(X).
C>mother(X, Y) :- parent(X, Y), female(X).
C>


C>Как может выглядеть откомпилированный псевдокод?

predicate(father/2,1,static,private,user,[
    allocate(1),
    get_variable(y(0),0),
    wake(1),
    put_value(y(0),0),
    call(parent/2),
    wake(1),
    put_value(y(0),0),
    deallocate,
    execute(male/1)]).


predicate(mother/2,2,static,private,user,[
    allocate(1),
    get_variable(y(0),0),
    wake(1),
    put_value(y(0),0),
    call(parent/2),
    wake(1),
    put_value(y(0),0),
    deallocate,
    execute(female/1)]).
Re[8]: Z3 theorem prover и вывод типов
От: catbert  
Дата: 19.10.10 18:44
Оценка: 1 (1)
Здравствуйте, Трурль, Вы писали:

C>>Как может выглядеть откомпилированный псевдокод?

Т>
Т>predicate(father/2,1,static,private,user,[
Т>    allocate(1),
Т>    get_variable(y(0),0),
Т>    wake(1),
Т>    put_value(y(0),0),
Т>    call(parent/2),
Т>    wake(1),
Т>    put_value(y(0),0),
Т>    deallocate,
Т>    execute(male/1)]).


Т>predicate(mother/2,2,static,private,user,[
Т>    allocate(1),
Т>    get_variable(y(0),0),
Т>    wake(1),
Т>    put_value(y(0),0),
Т>    call(parent/2),
Т>    wake(1),
Т>    put_value(y(0),0),
Т>    deallocate,
Т>    execute(female/1)]).
Т>


Подозрительно смахивает на инструкции WAM... если ничего быстрее не удастся получить, то вывод типов будет слишком медленным.
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.