This page defines a suggested standard for the input format of quantified Boolean formulas (QBFs) solvers in a non-prenex, non-cnf form.
| <input> | ::= <exp> EOF |
| <exp> | ::= <NOT> <exp> | <q_set> <exp> | <LP> <exp> <op> <exp> <RP> | <LP> <exp> <RP> | <VAR> |
| <q_set> | ::= <quant> <LSP> <var_list> <RSP> |
| <quant> | ::= <EXISTS> | <FORALL> |
| <var_list> | ::= <VAR> <var_list> | <VAR> |
| <op> | ::= <OR> | <AND> |
| <NOT> | ::= "!" |
| <LP> | ::= "(" |
| <RP> | ::= ")" |
| <LSP> | ::= "[" |
| <RSP> | ::= "]" |
| <OR> | ::= "|" |
| <AND> | ::= "&" |
| <EXISTS> | ::= "exists" |
| <FORALL> | ::= "forall" |
| <VAR> | ::= {A sequence of non-special ASCII characters} |