Hampi

A Solver for String Constraints

Formal Grammar


hampiInput :
     vardeclStmt ( ; statement )+
    
statement : 
     cfgStmt
   | regStmt
   | valDeclStmt
   | assertStmt
            
vardeclStmt :
    var ID : INT
  | var ID : INT .. INT
    
cfgStmt :
    cfg ID := cfgProduction ( | cfgProduction)*

cfgProduction :
    cfgProductionElement*
          
cfgProductionElement :
    cfgTerminal
  | ID
  | ( ID )?
  | ( ID )*     
  | ( ID )+
  | [ CHAR_LIT - CHAR_LIT ]
  | [ CHAR_SEQ - CHAR_SEQ ]
                         
cfgTerminal :
    STR_LIT
  | CHAR_SEQ
  
regStmt :
    reg ID := regDefinition

regDefinition :
    ID
  | STR_LIT
  | CHAR_SEQ
  | [ CHAR_LIT - CHAR_LIT ]
  | [ CHAR_SEQ - CHAR_SEQ ]
  | fix( ID , INT )
  | star(   regDefinition )
  | or(     regDefinition (, regDefinition)* )
  | concat( regDefinition (, regDefinition)* )
    
valDeclStmt :
    val ID := expr
    
expr :
    STR_LIT
  | ID
  | concat( expr (, expr)* )
   
assertStmt :
    assert boolExpr

boolExpr :
    ID ( not )? in ID
  | ID ( not )? contains STR_LIT
               
INT :
    [0-9]+

ID :
    [a-zA-Z] [a-zA-Z0-9_]+

STR_LIT :
    '\"' ( CHAR )* '\"'

CHAR_SEQ :
    '\\' [0-9][0-9][0-9]

CHAR_LIT :
    '\'' CHAR '\''

CHAR :
    EscapeSequence | ~('\"'|'\\')

EscapeSequence :
    '\\' ('n'|'r'|'\"'|'\''|'\\')