How to check a subset of a constraint set repeatedly

[xiedingbao]

Suppose I have a a set of constraints and want to check the satisfication of its subset repeatedly until get an expected result. From my experience using z3, I can think of three ways to do that, but not sure whether dreal3 supports them.

• push/pop

opensmt_mk_real_var //declare variables
...
while (condition)
    opensmt_push(ctx);
    opensmt_assert(ctx, expr);
    ...
    opensmt_check(ctx);
    opensmt_pop(ctx)

have tested the code with drel3, seems incorrect.

• check_assump

opensmt_mk_real_var //declare variables
...
for every constraint cons in the constraint set, use a boolean variable to manipulate it.
opensmt_assert(ctx, a -> constaint);

while (condition)
    opensmt_expr assumptions = opensmt_mk_eq(ctx, a, opensmt_mk_true(ctx));
    ...
    opensmt_check_assump(ctx, assumptions);

I get a seg fault when doing opensmt_mk_and_2 multiple times. opensmt's api is different from z3...

• check without reusing the previous knowledge

opensmt_mk_real_var //declare variables
...
while (condition)
    opensmt_reset(ctx); // I want to clear the constraints in the context
    opensmt_assert(ctx, expr);
    ...
    opensmt_check(ctx);

After a quick try, the code does not work, because I can't clear the constraints in the context before starting a new check.

[soonhokong]

@xiedingbao, the first method using push/pop should work but it has some problem in the implementation. I'll let you know when I fix that.

[xiedingbao]

How about the third method? It's the basic way to solve my problem. But I don't know how to clear the constraints in the model. Could you explain the usage of the API opensmt_reset?

[soonhokong]

I think it should work, but it should be much slower than the first method. Anyway, I plan to fix the push/pop problem, so please allow me some time, then I'll get back to you with a fix.

[soonhokong]

@xiedingbao, please try the latest version and check push/pop work as expected. If you find an unexpected result, please share the test case(s).