search

asolarlez / sketch-frontend

Other
33 stars 7 forks source link

Why sketch returns empty program? #11

Open odats opened 2 years ago

odats commented 2 years ago

I have just started learning sketch. Why synthesizer returns empty program:

Problem statement:

generator int lr(int x, int bnd){ 
    assert bnd > 0;

    int t = ??;

    if(t == 0){return x;} 
    if(t == 1){return ??;} 

    int a = lr(x, bnd-1);
    if(t == 2){return x * a;}
}

harness void test1(){
    assert lr(5, 3) == 25;
    assert lr(7, 3) == 49;
}

Output:

sketch-frontend % ./sketch test1.sk                  
SKETCH version 1.7.6
Benchmark = test1.sk
/* BEGIN PACKAGE ANONYMOUS*/
/*test1.sk:13*/

void test1 ()/*test1.sk:13*/
{ }
/*test1.sk:13*/

void test1__Wrapper ()  implements test1__WrapperNospec/*test1.sk:13*/
{
  test1();
}
/*test1.sk:13*/

void test1__WrapperNospec ()/*test1.sk:13*/
{ }
/* END PACKAGE ANONYMOUS*/
[SKETCH] DONE
Total time = 395