Problem P
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
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
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 |