Question regarding Context + constraints removal

[degrigis]

Hey guys!

I have a couple of quick questions:

[1]
Is there a simple way to create a new Context starting from another?

The idea would be:
1- Create ContextA, assert formulas, check sat, etc...
2- Create ContextB that get initialized with ContextA "state".
3- ContextB from now on has its own lifecycle.

[2]
Is there a way to remove constraints from the Context using the Python APIs? (Besides using push and pop)
I've already checked this, but since I didn't find anything I thought it was worth asking.

Thanks! :)

[ianamason]

Not really. https://yices.csl.sri.com/doc/context-operations.html has all the C operations that we wrap.
But it wouldn't be too hard to do this in python. You would just wrap a context and keep track of the
assertions added (just a list of ints) and cloning would then be easy.

Push and pop are the SMT way.

[degrigis]

@ianamason thanks for the quick answer :D

Regarding [1]: this is how I've already implemented it, however, it seems that the new ContextB loses all the benefit of the incremental solving collected up to that point. Am I doing something wrong, or there is a smarter way for this?

THANKS!

[ianamason]

Yes in your cloned context you would have to re-assert the saved list of ints, thats what you mean by losing
"the incremental solving collected up to that point" right?
If you want true incrementalism you'd need to do push and pop.

[degrigis]

Yep, the issue is exactly the one you pointed out.
I guess I can check, but, since I have an hold on you here (pardon my laziness): is there a limit on the number of pushes we can do?
The problem is we are trying to build a symbolic-executor based on Yices, I'm concerned that pushing at every state forking might not be feasible.

[ianamason]

I don't think so. I think push/pop is the way to go, right @BrunoDutertre ?

[degrigis]

@ianamason @BrunoDutertre actually, on a second thought, I'm afraid push/pop are not enough to accomplish what we wished for. In fact, push/pop cannot really be used when the symbolic-executor forks into 2 different states. What we need here is a full separate clone of the Context. I'll see if this is feasible to implement as a new function in the C library. If there is any major issue you are aware of please let me know :)