Skip to main content

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

rascal-0.34.0

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 _.$%|:/,?#\[\]];