Constraint Definition Language
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

constraints ::= constraints constraint | constraint

constraint ::= optcrash OPENBRACKET quantifiers CLOSEBRACKET COMMA body SEMICOLON
	    
optcrash ::= CRASH | /* nothing */

quantifiers ::= quantifiers COMMA quantifier | quantifier | /* nothing */
	   
quantifier ::= FORALL ID:var IN set:set 

set ::= ID:setname 
      | OPENBRACE listofliterals CLOSEBRACE
    
listofliterals ::= listofliterals COMMA literal | literal

body ::= body AND body
       | body OR body
       | NOT body
       | OPENPAREN body CLOSEPAREN
       | predicate

predicate ::= SIZEOF OPENPAREN setexpr CLOSEPAREN limitedcompare DECIMAL:dec
            | ID:var IN setexpr
            | ID:var DOT ID:relation compare:compare expr

setexpr ::= ID:var
          | ID:var DOT ID:relation
          | ID:var DOTINV ID:relation

expr ::= ID:var 
       | OPENPAREN expr CLOSEPAREN 
       | LITERAL OPENPAREN literal CLOSEPAREN
       | expr operator expr
       | expr DOT ID:field
       | SIZEOF OPENPAREN setexpr CLOSEPAREN
       | CAST OPENPAREN ID:type COMMA expr CLOSEPAREN 

operator ::= ADD | SUB | MULT | DIV 

literal ::= TRUE | DECIMAL | STRING | CHAR | ID

limitedcompare ::= EQUALS | wGT

compare ::= LT | GT | LE | GE | EQUALS



