Background

Gödel numbers are a way of encoding any string with a unique positive integer, using prime factorisations:

First, each symbol in the alphabet is assigned a predetermined integer code.

Then, to encode a string \$ x_1 x_2 x_3 \ldots x_n \$, where each \$ x_i \$ represents an symbol's integer code, the resultant number is

$$ \prod_{i=1}^n p_i^{x_i} = 2^{x_1} \cdot 3^{x_2} \cdot 5^{x_3} \cdot \ldots \cdot p_n^{x_n} $$

where \$ p_i \$ represents the \$ i \$th prime number. By the fundamental theorem of arithmetic, this is guaranteed to produce a unique representation.

For this challenge, we will only consider strings made of the symbols Gödel originally used for his formulae and use their values, which are:

• 0: 1
• s: 3
• ¬: 5
• ∨: 7
• ∀: 9
• (: 11
• ): 13

...although for simplicity the symbols ¬, ∨, and ∀ can be replaced by the ASCII symbols ~, |, and A respectively.

(I don't know why Gödel used only odd numbers for these, but they're what he assigned so we're sticking with it)

Challenge

Given a string consisting only of the symbols above, output its Gödel encoding as an integer.

You may assume the input will consist only of character in the set 0s~|A().

Example

For the string ~s0:

• start with \$ 1 \$, the multiplicative identity
• the first character ~ has code \$ 5 \$; the 1st prime is \$ 2 \$, so multiply by \$ 2 ^ 5 \$; the running product is \$ 32 \$
• the 2nd character s has code \$ 3 \$; the 2nd prime is \$ 3 \$, so multiply by \$ 3 ^ 3 \$; the running product is \$ 864 \$
• the 3rd character 0 has code \$ 1 \$; the 3rd prime is \$ 5 \$, so multiply by \$ 5 ^ 1 \$; the running product is \$ 4320 \$
• so the final answer is \$ 4320 \$

Test-cases

Input Output
"" 1
"A" 512
"~s0" 4320
"0A0" 196830
")(" 1451188224
"sssss0" 160243083000
"~(~0|~s0)" 42214303957706770300186902604046689348928700000
"0s~|A()" 5816705571109335207673649552794052292778133868750

Rules

• Your program does not have to work for strings that would produce larger integers than your programming language can handle, but it must work in theory
• You can accept input as a string, list of characters, or list of code-points
• You may use any reasonable I/O method
• Standard loopholes are forbidden
• This is code-golf, so the shortest code in bytes wins