Counting Satisfying Assignments

Time limit2sMemory limit256 MB

Summary

Parse one logical formula and count how many of the 4096 assignments to twelve variables make it true.

Level: Medium7 of 10
Topics: Implementation, Simulation, Brute force, Recursion
Solved: No attempts yet

Problem

You are given a single logical formula. It is built from the input variables A through L, the constants 0 and 1, and the operators equivalence (⇔), implication (→), disjunction (∨), conjunction (∧), and negation (¬), according to the following grammar.

<expression>  ::= { <implication> ⇔ }* <implication>
<implication> ::= <disjunction> | <disjunction> → <implication>
<disjunction> ::= <conjunction> | <disjunction> ∨ <conjunction>
<conjunction> ::= <term> | <conjunction> ∧ <term>
<term>        ::= A ... L | 0 | 1 | ¬ <term> | ( <expression> )

Here {X}* means repeating X zero or more times. Operator precedence, from lowest to highest, is equivalence, implication, disjunction, conjunction, negation; implication (→) is right-associative.

The semantics of the operators are the usual ones, except for equivalence. A run of several equivalences $a_1 \Leftrightarrow a_2 \Leftrightarrow \cdots \Leftrightarrow a_k$ inside one expression is 1 if and only if all of its arguments have equal values, and 0 otherwise.

There are $2^{12} = 4096$ ways to assign 0 or 1 to each of the twelve variables A through L. Count how many of these 4096 assignments make the formula evaluate to 1.

Input

The first line contains the logical formula, whose length is at most 300,000 characters. Equivalence is written <=>, implication ->, disjunction |, conjunction &, and negation ~. The variables A–L and the constants 0 and 1 stand for themselves. The formula contains no spaces or any other characters outside the grammar.

Output

Print a single integer: the number of the $2^{12} = 4096$ assignments of the twelve variables A through L for which the formula evaluates to 1. Variables that do not appear in the formula may still be 0 or 1 freely, so they are counted as well.

Notes

Because of precedence, B&C|E is read as (B&C)|E. Also, when equal values are chained with equivalence, as in F<=>(F)<=>F, all three arguments are always equal, so the value is always 1. Since implication is right-associative, A->B->C is the same as A->(B->C).

Examples3

Example 1
Input
```
(B&C|E)&(F<=>(F)<=>F)
```
Expected output
```
2560
```
Example 2
Input
```
A&B
```
Expected output
```
1024
```
Example 3
Input
```
A->B->C
```
Expected output
```
3584
```