Constraint Handling

[zhanghongce]

Hi I have a question about the part that handles Btor2 constraints.

Suppose that the expression of the constraint is C.
What the code does is: if C does not contain input, then C(V) and C(V') will be added to the transition relation.
But if C contains input, only C(V) will be added to the transition relation.

https://github.com/upscale-project/pono/blob/6d726131aef3179be970570603ab8ca1a38c8f7a/core/ts.cpp#L170

But why is that (I mean why there is such a difference)?

Furthermore, what if C syntactically contains some input variable, but semantically that input variable is reducible (I know that Boolector will do some reduction that may be able to remove it, but I guess there might also be cases where Boolector is not smart enough to do so). Does it matter? Would anything bad happen in this case?

[makaimann]

Good question! This is tricky and we want to revisit this later. Nothing bad should happen in the case that you explained, but it is definitely worth considering for performance and clarity (and is on our list). The main point here is that there is no "next" for inputs. If there are no inputs in C, then it is considered an invariant which means it must hold in both the current and the next states. For unrolling based techniques, this distinction is not that important (although you do have to be careful at the end of the trace). For non-unrolling techniques like IC3 this could actually make a difference.

If there are inputs in the formula, you can't add it to the next state because there's no next version of inputs. There are simple examples where bad things happen if you just prime all the state variables and leave the input unchanged. The assumption here is that the input value only matters in a transition and then only in one place (current). So the constraint does not need to be primed. If the input is actually a definition that should still be true, because definition constraints will still be enforced at a transition (which is the only time the inputs matter).

This is really subtle though and it's quite possible there is a better solution. If you're interested, I can invite you to our next discussion on this (not scheduled yet).

[zhanghongce]

Thanks for your reply! I was actually also wondering why not also make prime variables for inputs.
As @lonsing puts it in #73 that the state variables without next function are essentially input variables, but there they do have their primed counterparts. I guess maybe there will be a uniform way of handling these in the future?
Thanks!

[makaimann]

Right, we're hoping to handle those in a uniform way as well. For performance reasons, it's nice to distinguish between input variables and state variables (for example in the simple path check of k-induction, or even just how states are represented). Of course, we could also give inputs a next state and still keep them separate from state variables. We actually did that originally. It was just the easiest thing to do, but ended up settling on this solution after more thought. This seems like a nicer representation from a formal point of view, because it really captures the intention of an input (although input is kind of a misnomer because it could also be a definition).