BULL

membership_result_t mymemqry (void *info, bitvector *bv){
    membership_result_t res;
    int i;
    res=TRUE;
    for(i=1;i<bv->length;i++){
        if(!bitvector_get(bv, i)){
            res=FALSE;
        }
    }
    return res;
}

In the loop, the query result is set to FALSE if some bit in the bitvector bv is false. Otherwise the query result is TRUE.

equivalence_result_t* myequqry (void *info, uscalar_t num_vars, boolformula_t* c){
 
    equivalence_result_t* res = malloc(sizeof(equivalence_result_t));
 
    //create a formula g(x,y)=~x and test if g(x,y) ∧ c(x,y) is satisfible. 
    //If yes, then the satisfying assignment is a valid counterexample. 
    boolformula_t* g=boolformula_literal_new(-1);
    boolformula_t* g_c=boolformula_conjunction_new(2);
 
    boolformula_set(g_c,0,g);
    boolformula_set(g_c,1,c);
    sat_result_t* r=satisfible(g_c);
 
    boolformula_free(g_c);
    boolformula_free(g);
 
    if(r->is_sat==1){//not equivalent
        res->is_equal=FALSE;
        //call getce function to get a counterexample from r
        res->counterexample=getce(r,num_vars);
        sat_result_free(r);
        return res;
    }
 
    //create another formula g(x,y)=~y and test if g(x,y) ∧ c(x,y) is satisfible. 
    //If yes, then the satisfying assignment is a valid counterexample. 
    g=boolformula_literal_new(-2);
    g_c=boolformula_conjunction_new(2);
 
    boolformula_set(g_c,0,g);
    boolformula_set(g_c,1,c);
    r=satisfible(g_c);
 
    boolformula_free(g_c);
    boolformula_free(g);
 
    if(r->is_sat==1){//not equivalent
        res->is_equal=FALSE;
        //call getce function to get a counterexample from r
        res->counterexample=getce(r,num_vars);
        sat_result_free(r);
        return res;
    }
 
    //test if x ∧ y ∧ c(x,y) is satisfible.
    //If not, then {(x,true), (y,true)} is a valid counterexample. 
    boolformula_t* l1=boolformula_literal_new(1);
    boolformula_t* l2=boolformula_literal_new(2);
    g_c=boolformula_conjunction_new(3);
 
    boolformula_set(g_c,0,l1);
    boolformula_set(g_c,1,l2);
    boolformula_set(g_c,2,c);
    r=satisfible(g_c);
 
    boolformula_free(l1);
    boolformula_free(l2);
    boolformula_free(g_c);
 
    if(r->is_sat==0){
    //{(x,true),(y,true)} is not a satisfying assignment of c and thus is a valid counterexample
        res->is_equal=FALSE;
        res->counterexample=bitvector_new(3);
        bitvector_set(res->counterexample, 1, TRUE);
        bitvector_set(res->counterexample, 2, TRUE);
 
        sat_result_free(r);
        return res;
    }
 
 
    //the conjecture is correct!
    res->is_equal=TRUE;
    return res;
}

Here we use three different tests to ensure that the conjecture is indeed equivalent to f(x,y). The first two checks ensure that assignments with (x,false) or (y,false) are not satisfying ones. The last check ensures that {(x,true),(y,true)} is a satisfying assignment.

int main(int argc, char *argv[]){
        int mode=0;
        boolformula_t* c=learn (NULL, 2,mymemqry,NULL, myequqry, mode);
        printf(stderr,"\nFinished!\nResult:");
        boolformula_print(c);
        boolformula_free(c);
        return 0;
}

After the queries are implemented, we invoke the learning algorithm to obtain a correct conjecture. Since we are using CDNF, only two types of queries are needed. Therefore, 4th argument of the call to the “learn” function is NULL (non-membership queries are not used by CDNF).

To be more specific, we call the function

  boolformula_t *learn (void *info, uscalar_t num_vars, membership_t membership,   
  membership_t comembership, equivalence_t equivalence, int mode);

defined in core/cdnf.h

• info can be used to pass additional information to the learning algorithm. They will be passed to different queries. When you want to have multiple learning instances, it can be used to identify the difference between instances.
• num_vars is the number of variables in the target function
• membership is the implemented membership query
• comembership is the implemented non-membership query
• equivalence is the implemented equivalence query
• mode is the type of learning algorithm in use

For CDNF, set mode to 0 and num_var to the number of variables in the target function.
For CDNF+, set mode to 1 and num_var to 1.
For CDNF++, set mode to 2 and num_var to 1.

Below is a sample output of the program:

Finished! Number of Mem. Q. =2, co-Mem. Q= 0, Equ. Q. = 3
Result:{ { { 2 & 1 } } }

It says that 2 membership queries and 3 equivalence queries are used to get the formula (y ∧ x). Notice that inside BULL, literals are stored in the form of numbers. Here x is mapped to 1 and y is mapped to 2. The result is in the form of CDNF (conjunction of formulae in disjunction normal form). E.g., { { { 2 & 1 } | -1 } & 2} is a possible output.