Convert IntegerFormula Variable to BooleanFormula Variable

[Gykonik]

Hey, I'm wondering if there is an option to convert an IntegerFormula-Variable into a BooleanFormula-Variable somehow. Specifically, I want to have BooleanFormula if possible, but if I have to (e.g. a == 4), convert the variable "a" to an IntegerFormula.

[kfriedberger]

The sort of a variable is fixed, i.e., set in stone with its declaration. If you want to declare variables with different sorts, you should use different names.

Just out of curiosity, could you give some context for your issue? In which case would someone want to switch the sort of a variable?

[Gykonik]

Thanks for the quick reply, sure I can. However, I guess its a bit rare of a use-case. But maybe you have different suggestions on how to do it.

Basically, I have a somewhat more complex system where the user can enter formulas themselves. These are then converted into Java-SMT formulas and should be output in a tree at the end (somewhat simplified). I actually want to simplify the formula as much as possible so that the tree is as simple as possible (I cannot simply use the "simplify", since I also want to extract things like XORs, it's a bit more complicated here :D).

So if the user enters e.g. "if 3 > 2 then X else ", the result should only be "X" - so far so good. But if the user enters "if X > 2 then Y", then we don't really know the result, which is why I would simply output the string "If X GT 2 THEN Y" in the tree. And since I don't really know in advance whether a BooleanFormula (X) or IntegerFormula (3, 2) will come, and I can only do ">" with IntegerFormulas, my idea was to simply transform the BooleanVariable (X) into an IntegerVariable (X) and then store the formula as an Integer Formula.

Thinking about it, one solution could be to first check what the next variables and the mathematical operation are when converting, and automatically take IntegerVariable or BooleanVariable accordingly - but that sounds more complicated than simply converting them (and it would clash with things like "(X && Y) > 2") :D

[kfriedberger]

SMTLIB and JavaSMT does not support things like (x && y) > 2, but only well-typed expressions like ITE(x && y, 1, 0) > 2. Mixing Integer and Boolean logic in undefined way, e.g., aside of already defined operations like ITE, is not intended.

For your case. you would need to know the Sort for each variable before giving it to JavaSMT, which might not be possible if the user inserts his data sequencially and you already parse the existing input. If you want to change the Sort later, you can apply a formula visitor to replace the variable. // untested, just a first thought :-)

[Gykonik]

Thanks for the answer. Indeed I already tried it by creating a new Variable with the correct formula manager. However, I was always getting an error Variable X already exists in the instance which I assume means that X as BooleanVariable already exists, so I cannot re-create it as IntegerVariable (for example). Is there any way around this? Like "deleting" the old one or something similar?

If this is possible somehow, I guess it would be sufficient to just write a simple visitor which repalces the Atom with a new, different atom. But since the variable names are equal, I end up with the error described above. Do you have any suggestions? :)

[PhilippWendler]

Either use different variable names in the result of your simplification (e.g., like you would used "primed" variables when using pen and paper) or create a completely new solver context for the result of the simplification and let the visitor create the formulas in the new context.