CFFI sat

[adelin-b]

Hello, Im trying to use the sat function in c, however it seem that something go wrong each time I try to use it.

int main(void)
{
    void *ctx;
    void *a;
    void *b;
    void *c;
    uint8_t *str;
    void *bxs[4];
    void *bx_sat;

    bx_sat = NULL;

    /**
     *      init
     */
    ctx = boolexpr_Context_new();
    a = (void*)boolexpr_Context_get_var(ctx,"b");
    b = (void*)boolexpr_Context_get_var(ctx,"a");
    bxs[0] = b;
    bxs[1] = a;

    c = (void*)boolexpr_xor(2,(BXS)bxs);

    bx_sat = (void *)boolexpr_BoolExpr_sat(c);
    //  boolexpr_BoolExpr_del(bx_sat);
    boolexpr_String_del((STRING)str);
    boolexpr_BoolExpr_del((BX)a);
    boolexpr_BoolExpr_del((BX)b);
    boolexpr_BoolExpr_del((BX)c);

        return 0;
}

Does the boolexpr_BoolExpr_sat() function need a certain type of expression ?

[cjdrake]

There was a minor bug in the return type of boolexpr_BoolExpr_sat function, which I corrected a couple days ago.

Here's a recipe I just cooked up to demonstrate:

#include <boolexpr/boolexpr.h>

int
main(void)
{
    void * ctx;

    void * a;
    void * b;
    void * F;

    void * bxs [2];
    void * soln;

    ctx = boolexpr_Context_new();

    a = (void *) boolexpr_Context_get_var(ctx, "a");
    b = (void *) boolexpr_Context_get_var(ctx, "b");
    bxs[0] = a;
    bxs[1] = b;

    F = (void *) boolexpr_xor(2, bxs);

    soln = (void *) boolexpr_BoolExpr_sat(F);
    printf("Is F SAT? %d\n", boolexpr_Soln_first(soln));
    boolexpr_Soln_del(soln);

    boolexpr_BoolExpr_del(F);
    boolexpr_BoolExpr_del(a);
    boolexpr_BoolExpr_del(b);

    boolexpr_Context_del(ctx);

    return 0;
}

Compling with g++ --std=c++11 -o foo -Iinclude -Ithird_party/boost-1.54.0 -Ithird_party/glucosamine/src -Lbuild foo.c -lboolexpr, then running the binary should output this:

Is F SAT? 1

You can also get the exact SAT model by calling boolexpr_Soln_snd(soln). That return type is called a "point", and you can iterate over it to get all the variable assignment in the SAT model.