Problem F
Modelling Problems
Sometimes, Atrebla just wants to know if her code’s assertions can ever be false. Of course, this is somewhat of an undecidable problem in the general case — there is a very simple way to turn any program that solves this problem into one that solves the halting problem.
But Atrebla isn’t concerned with any arbitrary programs, she’s concerned with her own! There are a couple of properties of her code that she thinks might make this easier. First, since it’s for embedded systems, it only deals with integer calculations. Second, since her workplace insists on using a home-grown programming langauge, the programming language is simple — it doesn’t even have loops! Those are apparently coming once Orion over in software tooling gets some free time.
Programs in the language Atrebla is using have three kinds of statements. They are either assignments, conditionals, or assertions.
Variable assignments look like this:
[x=?]
[b=18]
[a=z+c]
Each assignment has a single-character variable name and an equal sign, followed by either a question mark (to denote the value is unknown and either $0$ or $1$), an integer between $0$ and $10\, 000$ inclusive, or a single addition of two variables. If a variable has not yet been set by an assignment, its value should be considered to be zero.
Conditionals look like this:
(a<b{[a=42]})
(u<d{[a=d+e][b=78]})
Here, the {} braces denote a block of other commands to run. The comparison is always a (strict) less-than, and is always made between two variables. The block will never be empty. There will never be another conditional or an unknown variable assignment ([x=?]) within the block.
Assertions look like this:
<a=b>
Assertions are always made between two variables.
Given a program in this language, determine if the assertions will always hold.
Input
The first line contains a single integer $T \leq 5$ giving the number of test cases. Each test case consists of a single line containing a program in the language defined above. The line will contain between $1$ and $1\, 000$ characters inclusive and will contain no more than $10$ unknown variable assignments ([x=?]). There will not be whitespace in the program. It is guaranteed that the value of all variables will never exceed $10\, 000$ during the execution of a program.
Output
For each test case, output a single line containing either “ASSERTIONS ALWAYS HOLD” or “ASSERTIONS INVALID”.
| Sample Input 1 | Sample Output 1 |
|---|---|
5
[a=18][b=24][c=a+b][d=42]<c=d>
[a=18][b=24](a<b{[c=a+b]})[d=42]<c=d>
[a=18][b=24](a<b{[c=a+b]})[d=43]<c=d>
[a=?]<a=b>
[a=?][b=24](a<b{[c=77]})[d=77]<c=d>
|
ASSERTIONS ALWAYS HOLD ASSERTIONS ALWAYS HOLD ASSERTIONS INVALID ASSERTIONS INVALID ASSERTIONS ALWAYS HOLD |