CORAL

Coral accepts constraints in the following input language of symbolic expressions.

One example expression:

DLT(SIN_(MUL(DVAR(ID_1),DVAR(ID_2))),DCONST(0.0));DGT(COS_(MUL(DVAR(ID_1),DCONST(2.0))),DCONST(0.25))
// pretty-prints as: sin(id_1 * id_2) < 0 && cos(2x) > 0.25

Input Language

/* path condition */
PC  := BE | BE ';' PC

/* boolean expressions */
BE  := BC | BOP | DR | FR | IR | LR

/* boolean constants */
BC  := 'BCONST(true)' | 'BCONST(false)'

/* boolean operations */
BOP := op '(' BE ',' BE ')' where op = {BAND,BOR,BXOR}
     | 'BNOT(' BE ')'

/* double relational */
DR :=  op '(' DE ',' DE ')' where op = {DGT,DLT,DLE,DGE,DEQ,DNE}

/* float relational */
FR :=  op '(' FE ',' FE ')' where op = {FGT,FLT,FLE,FGE,FEQ,FNE}

/* int relational */
IR :=  op '(' IE ',' IE ')' where op = {IGT,ILT,ILE,IGE,IEQ,INE}

/* long relational */
LR :=  op '(' LE ',' LE ')' where op = {LGT,LLT,LLE,LGE,LEQ,LNE}

/* double expression */
DE := DA | DC | DL | DB | DU

/* double arithmetic */
DA := op '(' DE ',' DE ')' where op = {ADD,SUB,MUL,DIV,MOD}

/* double constant */
DC := 'DCONST(' v ')' where v is a double literal

/* double literal */
DL := 'DVAR(' id ')' where id is a string identifier, like "ID_1","ID_2","ID_300"...

/* double binary function */
DB := op '(' DE ',' DE ')' where op = {ATAN2_, POW_}

obs. Mathematical functions with semantics as defined in
http://download-llnw.oracle.com/javase/6/docs/api/java/lang/Math.html

/* double unary function */ 
DU := op '(' DE ')' where op = {SIN_, COS_, TAN_, ASIN_, ACOS_, ATAN_, EXP_,
LOG_, LOG10_, ROUND_, SQRT_}

/* float,int, and long expressions */
FE := FA | FC | FL 
IE := IA | IC | IL 
LE := LA | LC | FL 

/* casts to int and double */
To cast an expression, use ASINT(exp) or ASDOUBLE(exp). 


obs. The definitions of these categories are similar to the category
with corresponding name for doubles.  You replace first 'D' charaters
in tokens with the name of the type.  For example, an int literal is
identified with IVAR.  For example, IVAR(ID_1).