robustness issues

[soonhokong]

Dear @zenna,

While testing the Julia interface, I've found a robustness problem. When I declare a variable twice, it terminates the whole Julia shell:

julia> x = Var(Int,"x")
opensmt_mk_int_var: x = [-9223372036854775808, 9223372036854775807]
# OpenSMTContext::Declaring function x of sort () Int
# Error: symbol already declared  x (triggered at /usr0/home/soonhok/work/dreal3/src/opensmt/egraph/EgraphStore.C, 653)

I think it should return the previously declared variable, possibly update the domain with new information. Do you agree? If so, I can make this change.

Do you see any other robustness issues? Please feel free to enumerate them here, I'll fix them later.

[zenna]

@soonhokong Yes, this is a known problem. I'll prevent this from terminating the whole shell. On another level, even if you reset the context, you will still get this error. This is what I meant in the earlier email.

ctx = Context(qf_nra)
x = Var(ctx,Int,"x")
reset_ctx!(ctx)
x = Var(ctx,Int,"x")
# Error: symbol already declared  x (triggered at /home/zenna/repos/dreal3/src/opensmt/egraph/EgraphStore.C, 651)

[soonhokong]

@zenna, I see. Could you enumerate examples here for the record? I can fix them one by one and use them as test cases.

[zenna]

@soonhokong I think any example where you define a variable that has been defined before in a context will cause that error. I'm not sure what kind of different examples you mean. There is another kind of bug with deleting a variable, I'll try to isolate that.

I think it should return the previously declared variable, possibly update the domain with new > information. Do you agree? If so, I can make this change.

Yes, and maybe return a warning too. But there does not seem to be anything in the API that would allow me to update an existing variable, is there?

Actually, generally I think the use of strings as variable names is not ideal, and probably it would be better if they were generated randomly and hidden from the user.

[soonhokong]

Actually, generally I think the use of strings as variable names is not ideal, and probably it would be better if they were generated randomly and hidden from the user.

I like this idea. Let me add a new function in C APIs which does not require string argument.

Yes, and maybe return a warning too.

I can change it to print out an warning to std::cerr. Will that be OK? Or do you want to get some different return value for this case?

But there does not seem to be anything in the API that would allow me to update an existing variable, is there?

For now, we don't have one. But we can add it since it's plausible. Let me know if you need it.

[zenna]

I like this idea. Let me add a new function in C APIs which does not require string argument.

I can change it to print out an warning to std::cerr. Will that be OK? Or do you want to get some different return value for this case?

Assuming that dReal actually requires string variable names, we can do what I proposed in either C or Julia. It might be easier in Julia because dealing with std::cerr is cumbersome.

For now, we don't have one. But we can add it since it's plausible. Let me know if you need it.

This may actually be useful, but not so much for the issue we have been describing here. I might open another issue about this.

[soonhokong]

Assuming that dReal actually requires string variable names, we can do what I proposed in either C or Julia. It might be easier in Julia because dealing with std::cerr is cumbersome.

OK. I will leave the decision to you then. Just let me know if you think implementing it in C is better..

This may actually be useful, but not so much for the issue we have been describing here. I might open another issue about this.

I agree.

[zenna]

@soonhokong I've added some checks so that it doesn't fatally error. Any progress on the context resetting problem?

[zenna]

Also deleting contexts causes malloc errors.

See test/optimise.jl for example.

[soonhokong]

@zenna, thank you. I'll fix it later today.

Any progress on the context resetting problem?

Sorry, not yet..

[soonhokong]

@zenna, could you check whether we still have a problem with resetting a context?

[zenna]

Both problems still persist (at least when using the API from the Julia side)

1. symbol already declared errors when adding a previously added variable even after resetting)
2. Error in julia': malloc(): smallbin double linked list corrupted: 0x00000000067af7f0 *** when using opensmt_delete_ctx!

[soonhokong]

@zenna, thanks for checking things!