When interacting with Yices purely through the API, I think the only way to know which assertions have been added to a Yices context (which in that respect is somewhat of a black box) is to track those assertions externally, recording them when calling primitives like yices_assert_formula (+ track the pushes and pops if need be).
This works fine except for yices_assert_blocking_clause, which I think is the only primitive that adds an assertion to a Yices context without the caller having ever access to the said blocking clause as a Yices term. That throws off the effort to track the assertions in a Yices context.
Since the primitive just returns 0 in case of success, and -1 in case of error, I was wondering if we could make the primitive return the blocking clause instead of 0. This would barely change the use of the primitive, in that the only situation where we technically wouldn't be backward-compatible is if the user was testing the success of the call with v == 0 instead of v >= 0, where v is the returned value. Is this correct?
Is the blocking clause readily available under the hood of the API?
Thoughts?
When interacting with Yices purely through the API, I think the only way to know which assertions have been added to a Yices context (which in that respect is somewhat of a black box) is to track those assertions externally, recording them when calling primitives like yices_assert_formula (+ track the pushes and pops if need be).
This works fine except for yices_assert_blocking_clause, which I think is the only primitive that adds an assertion to a Yices context without the caller having ever access to the said blocking clause as a Yices term. That throws off the effort to track the assertions in a Yices context.
Since the primitive just returns 0 in case of success, and -1 in case of error, I was wondering if we could make the primitive return the blocking clause instead of 0. This would barely change the use of the primitive, in that the only situation where we technically wouldn't be backward-compatible is if the user was testing the success of the call with v == 0 instead of v >= 0, where v is the returned value. Is this correct?
Is the blocking clause readily available under the hood of the API? Thoughts?