import edu.neu.ccs.demeter.dj.*;

Formula = List(Clause) EOF.
Clause = Weight ":" Body.
Body : Satisfied | Unsatisfied | Literals.
Literals = List(Literal).
Literal : Positive | Negative common Variable.
Positive = .
Negative = "not".
Variable = Ident.
Satisfied = "sat".
Unsatisfied = "unsat".
List(S) ~ S {S}.
Weight = <v> float.
Main = <s> String.