Skip to main content

module lang::smtlib2::command::response::Syntax

rascal-Not specified

Synopsis: Grammar of the SMTLIBv2 response

Usage​

import lang::smtlib2::command::response::Syntax;

Dependencies​

extend lang::std::Layout;

syntax Response​

start syntax Response
    = response: CheckSat sat
    | response: GetValue model
    | response: GetUnsatCore unsatCore
    ;

syntax CheckSat​

syntax CheckSat 
    = sat: "sat" 
    | unsat: "unsat" 
    | unknown: "unknown"
    ;

syntax GetUnsatCore​

syntax GetUnsatCore = unsatCore: "(" Label* labels ")";

syntax GetValue​

syntax GetValue = foundValues:"(" Model* models ")";

syntax Model​

syntax Model = model:"(" Expr var Expr val ")";

syntax Expr​

syntax Expr
    = customFunctionCall: "(" Expr functionName Expr* params ")"
    | lit: Literal lit
    | var: Id varName
    ;

syntax Literal​

syntax Literal
    = intVal:Int int
    | boolVal: Bool b
    ;

syntax Int​

lexical Int = '-'? [0-9]+ !>> [0-9];

syntax Bool​

lexical Bool = "true" | "false";

syntax Keywords​

keyword Keywords = "true" | "false";

syntax Id​

lexical Id = ([a-z A-Z 0-9 _.] !<< [a-z A-Z][a-z A-Z 0-9 _.]* !>> [a-z A-Z 0-9 _.]) \Keywords;

syntax Label​

lexical Label = [a-z A-Z 0-9 _.$%|:/,?#\[\]] !<< [a-z A-Z 0-9 _.$%|:/,?#\[\]]* !>> [a-z A-Z 0-9 _.$%|:/,?#\[\]];