Program = *l "" + List(Expression) - *l "" EOF.
Expression : LetExp | CNF.
LetExp = *l "" +
"" Literal ""
+ Expression - *l "" -.
CNF = *l "" + List(Clause) - *l
[*l "" ClauseCount ""]
[*l "" ClauseCount ""] "".
Clause = *l "" Weight Literals "".
Literals = *l "" + List(Literal) - *l "".
Literal : Pos | Neg.
// expanded: common Variable .
Pos = "" Variable "".
Neg = "" Variable "".
Variable = Ident.
Weight = "" int "".
ClauseCount = "" int "".
List(S) ~ {S} .
Main = String.
// test case for CNF reduction
// shows three programs P1,P2,P3
// where P2 is a reduction of P1 and
// P3 is a reduction of P2.
a
b
2
a
b
3
a
b
5
10
b
3
b
7
10
7
13
// let !b in
// cnf (
// 3 (b))
// sat 2
// cnf ()
// sat 2
// unsat 3