The SMT-LIB Language uses S-expression, which is actually legal Common Lisp syntax. It has three main components: theory declarations, logic declarations, and scripts.
They contain only ASCII characters, not Unicode.
The followings are a preview of the ANTLR v4 grammar of SMTLIB v2.0 by Hanwen Wu, according to [BaST10]. (And, subject to change.)
We are working on integrating two SMT solvers, therefore it is necessary to understand the SMT-LIB 2.0 logic, which can be used as an input language for both solvers (AltErgo, CVC4). Part of the project is to classify formulas which can be solved by one solver, while not by the others. Therefore knowing how theories and logics are defined in SMT-LIB is also important.
- ๐ฎ: Infinite set of sort symbols, containing BOOL.
- ๐ฑ: Infinite set of sort parameters
- ๐ณ: Infinite set of variables
- โฑ: Infinite set of function symbols
- โฌ: Boolean values {true, false}
- ...
Sorts over a set of sort symbols ๐ฎ are defined as Sort (๐ฎ).
- ฯโโโ๐ฎ of arity 0 is a sort
- ฯฯ1,โฯ2,โฯ3,โ...,โฯn is a sort if ฯโโโ๐ฎ of arity n, ฯ1 to ฯn are sorts
Baiscly, ฮฃ defines sort symbols and arities, function symbols and ranks, some variables and their sorts.
- ฮฃ๐ฎโโโ๐ฎ: sort symbols, containing BOOL
- ฮฃโฑโโโโฑ: function symbols, containing equality, conjunction, and negation
- ฮฃ๐ฎ to โ: a total mapping from sort symbol to its arity, including ๐ฑ๐พ๐พ๐ป โจ ๐ถ
- ฮฃโฑ to Sort (ฮฃ๐ฎ)+: a left total mapping from a function symbol to its rank, containing = (ฯ,โฯ ,BOOL), ยฌ (BOOL,BOOL), โง (BOOL,BOOL,BOOL).
- ๐ณ to Sort (ฮฃ๐ฎ): a partial mapping from a variable to its sort.
Well sorted terms of sort BOOL over ฮฃ.
A can be regarded as a model.
- A: the universe (of values) of A, including BOOL A ={true,false}.
- ฯAโโโA: give the sort ฯโ Sort (ฮฃ๐ฎ) a universe ฯAโโโA. For example, BOOL A is {true,flase} โโโA. INT A could be all the integers โคโโโA.
- (fโ:โฯ)AโโโฯA: give the constant symbol fโ:โฯ a value in the universe of ฯ
- (fโ:โฯ1,โฯ2,โ...,โฯn,โฯ)A: define the function symbol as a relation from (ฯ1,โฯ2,โ...,โฯn)A to ฯA. This must include the equality relations (or identity predicate over ฯA, that is =(ฯ,โฯ,BOOL) as standard equality relations from (ฯA,โฯA) to {true,false}).
ฯA is called the extension of ฯ in A.
- Valuations v: a partial mapping v from ๐ณร Sort (ฮฃ๐ฎ) to ฯA. That is to give variable x of sort ฯ a value in ฯA.
- Interpretation โโ:โโโ=โ(A,โv), that is the structure together with the valuations make the ฮฃ-interpretation.
- Semantics: โ will assign a meaning to well-sorted terms by uniquely mapping them into the A.
- Satisfiability:
- If ฯ is mapped to true by some โ, then it is satisfiable.
- If ฯ is not closed, we say โโ=โ(A,โv) makes true ฯ.
- If ฯ is closed, we say the structure A makes true ฯ.(Since it does not matter what valuation it is.)
- If ฯ is closed, we say the structure A a model of ฯ.
- Traditionally, its a set of axioms
Here it consists of three parts
- Signature: ฮฃ
- Axioms:
We think this part is left for the people who implement solvers. Take INT theory as an example, since we have the plus sign in our signature (we just denote it as ADD, so that you know it is only a symbol, not the actual operation), we will have an axiom like โx:๐ธ๐ฝ๐.y:๐ธ๐ฝ๐.โz:๐ธ๐ฝ๐.๐ฐ๐ณ๐ณ(x,y,z)โx+y=z. Therefore, our model (or structure) must contain the correct relations to map ๐ฐ๐ณ๐ณ to the actual addition operation to satisfy this axiom.
Also, some theories like REAL include those axioms as plain text, like associativity, commutativity, etc.
- Models: A set of ฮฃ-structures, all of which are models of the theory.
- Sublogic: it is a sublogic of SMT-LIB logic
- Restrictions:
- fixing a signature ฮฃ and its theory ๐ฏ
- restricting structures to the models of ๐ฏ
- restricting input sentences as subset of ฮฃ-sentences
// Predefined Symbols
SYM_BOOL : 'Bool';
SYM_CONTINUED_EXECUTION : 'continued-execution';
SYM_ERROR : 'error';
SYM_FALSE : 'false';
SYM_IMMEDIATE_EXIT : 'immediate-exit';
SYM_INCOMPLETE : 'incomplete';
SYM_LOGIC : 'logic';
SYM_MEMOUT : 'memout';
SYM_SAT : 'sat';
SYM_SUCCESS : 'success';
SYM_THEORY : 'theory';
SYM_TRUE : 'true';
SYM_UNKNOWN : 'unknown';
SYM_UNSAT : 'unsat';
SYM_UNSUPPORTED : 'unsupported';
// Predefined Keywords
KEYWORD_ALL_STATISTICS : ':all-statistics';
KEYWORD_AUTHORS : ':authors';
KEYWORD_AXIOMS : ':axioms';
KEYWORD_CHAINABLE : ':chainable';
KEYWORD_DEFINITION : ':definition';
KEYWORD_DIAGNOSTIC_OUTPUT_CHANNEL : ':diagnostic-output-channel';
KEYWORD_ERROR_BEHAVIOR : ':error-behavior';
KEYWORD_EXPAND_DEFINITIONS : ':expand-definitions';
KEYWORD_EXTENSIONS : ':extensions';
KEYWORD_FUNS : ':funs';
KEYWORD_FUNS_DESCRIPTION : ':funs-description';
KEYWORD_INTERACTIVE_MODE : ':interactive-mode';
KEYWORD_LANGUAGE : ':language';
KEYWORD_LEFT_ASSOC : ':left-assoc';
KEYWORD_NAME : ':name';
KEYWORD_NAMED : ':named';
KEYWORD_NOTES : ':notes';
KEYWORD_PRINT_SUCCESS : ':print-success';
KEYWORD_PRODUCE_ASSIGNMENTS : ':produce-assignments';
KEYWORD_PRODUCE_MODELS : ':produce-models';
KEYWORD_PRODUCE_PROOFS : ':produce-proofs';
KEYWORD_PRODUCE_UNSAT_CORES : ':produce-unsat-cores';
KEYWORD_RANDOM_SEED : ':random-seed';
KEYWORD_REASON_UNKNOWN : ':reason-unknown';
KEYWORD_REGULAR_OUTPUT_CHANNEL : ':regular-output-channel';
KEYWORD_RIGHT_ASSOC : ':right-assoc';
KEYWORD_SORTS : ':sorts';
KEYWORD_SORTS_DESCRIPTION : ':sorts-description';
KEYWORD_STATUS : ':status';
KEYWORD_THEORIES : ':theories';
KEYWORD_VALUES : ':values';
KEYWORD_VERBOSITY : ':verbosity';
KEYWORD_VERSION : ':version';
// Predifined General Token
TOKEN_BANG : '!';
TOKEN_UNDERSCORE : '_';
TOKEN_AS : 'as';
TOKEN_DECIMAL : 'DECIMAL';
TOKEN_EXISTS : 'exists';
TOKEN_FORALL : 'forall';
TOKEN_LET : 'let';
TOKEN_NUMERAL : 'NUMERAL';
TOKEN_PAR : 'par';
TOKEN_STRING : 'STRING';
// Predefined Command Token
TOKEN_CMD_ASSERT : 'assert';
TOKEN_CMD_CHECK_SAT : 'check-sat';
TOKEN_CMD_DECLARE_SORT : 'declare-sort';
TOKEN_CMD_DECLARE_FUN : 'declare-fun';
TOKEN_CMD_DEFINE_SORT : 'define-sort';
TOKEN_CMD_DEFINE_FUN : 'define-fun';
TOKEN_CMD_EXIT : 'exit';
TOKEN_CMD_GET_ASSERTIONS : 'get-assertions';
TOKEN_CMD_GET_ASSIGNMENT : 'get-assignment';
TOKEN_CMD_GET_INFO : 'get-info';
TOKEN_CMD_GET_OPTION : 'get-option';
TOKEN_CMD_GET_PROOF : 'get-proof';
TOKEN_CMD_GET_UNSAT_CORE : 'get-unsat-core';
TOKEN_CMD_GET_VALUE : 'get-value';
TOKEN_CMD_POP : 'pop';
TOKEN_CMD_PUSH : 'push';
TOKEN_CMD_SET_LOGIC : 'set-logic';
TOKEN_CMD_SET_INFO : 'set-info';
TOKEN_CMD_SET_OPTION : 'set-option';
fragment DIGIT : [0-9];
fragment HEXDIGIT : DIGIT | [a-fA-F];
fragment ALPHA : [a-zA-Z];
fragment ESCAPE : '\\' ('\\' | '"');
fragment SYM_CHAR : [+-/*=%?!.$_~&^<>@];
NUMERAL : '0' | [1-9] DIGIT*;
DECIMAL : NUMERAL '.' [0]* NUMERAL;
HEXADECIMAL : '#x' HEXDIGIT+;
BINARY : '#b' [01]+;
STRING : '"' (ESCAPE | ~('\\' | '"')*) '"';
WS : [\t\r\n\f ]+ {skip();};
SIMPLE_SYM : (ALPHA | SYM_CHAR) (DIGIT | ALPHA | SYM_CHAR)*;
QUOTED_SYM : '|' ~('|' | '\\')* '|';
COMMENT : ';' ~('\n' | '\r')* {skip();};
KEYWORD_TOKEN : ':' (ALPHA | DIGIT | SYM_CHAR)+;
symbol : SIMPLE_SYM
| QUOTED_SYM
| SYM_BOOL
| SYM_CONTINUED_EXECUTION
| SYM_ERROR
| SYM_FALSE
| SYM_IMMEDIATE_EXIT
| SYM_INCOMPLETE
| SYM_LOGIC
| SYM_MEMOUT
| SYM_SAT
| SYM_SUCCESS
| SYM_THEORY
| SYM_TRUE
| SYM_UNKNOWN
| SYM_UNSAT
| SYM_UNSUPPORTED
;
keyword : KEYWORD_TOKEN
| KEYWORD_ALL_STATISTICS
| KEYWORD_AUTHORS
| KEYWORD_AXIOMS
| KEYWORD_CHAINABLE
| KEYWORD_DEFINITION
| KEYWORD_DIAGNOSTIC_OUTPUT_CHANNEL
| KEYWORD_ERROR_BEHAVIOR
| KEYWORD_EXPAND_DEFINITIONS
| KEYWORD_EXTENSIONS
| KEYWORD_FUNS
| KEYWORD_FUNS_DESCRIPTION
| KEYWORD_INTERACTIVE_MODE
| KEYWORD_LANGUAGE
| KEYWORD_LEFT_ASSOC
| KEYWORD_NAME
| KEYWORD_NAMED
| KEYWORD_NOTES
| KEYWORD_PRINT_SUCCESS
| KEYWORD_PRODUCE_ASSIGNMENTS
| KEYWORD_PRODUCE_MODELS
| KEYWORD_PRODUCE_PROOFS
| KEYWORD_PRODUCE_UNSAT_CORES
| KEYWORD_RANDOM_SEED
| KEYWORD_REASON_UNKNOWN
| KEYWORD_REGULAR_OUTPUT_CHANNEL
| KEYWORD_RIGHT_ASSOC
| KEYWORD_SORTS
| KEYWORD_SORTS_DESCRIPTION
| KEYWORD_STATUS
| KEYWORD_THEORIES
| KEYWORD_VALUES
| KEYWORD_VERBOSITY
| KEYWORD_VERSION
;
spec_constant : NUMERAL | DECIMAL | HEXADECIMAL | BINARY | STRING;
s_expr : spec_constant | symbol | keyword | '(' s_expr* ')';
identifier : symbol | '(' TOKEN_UNDERSCORE symbol NUMERAL+ ')';
sort : identifier | '(' identifier sort+ ')';
attribute_value : symbol | spec_constant | '(' s_expr* ')';
attribute : keyword | keyword attribute_value;
qual_identifier : identifier | '(' TOKEN_AS identifier sort ')';
var_binding : '(' symbol term ')';
sorted_var : '(' symbol sort ')';
term
: spec_constant
| qual_identifier
| '(' qual_identifier term+ ')'
| '(' TOKEN_LET '(' var_binding+ ')' term ')'
| '(' TOKEN_FORALL '(' sorted_var+ ')' term ')'
| '(' TOKEN_EXISTS '(' sorted_var+ ')' term ')'
| '(' TOKEN_BANG term attribute+ ')'
;
sort_symbol_decl : '(' identifier NUMERAL attribute* ')';
meta_spec_constant : TOKEN_NUMERAL | TOKEN_DECIMAL | TOKEN_STRING;
fun_symbol_decl
: '(' spec_constant sort attribute* ')'
| '(' meta_spec_constant sort attribute* ')'
| '(' identifier sort+ attribute* ')'
;
par_fun_symbol_decl
: fun_symbol_decl
| '(' TOKEN_PAR '(' symbol+ ')' '(' identifier sort+ attribute* ')' ')'
;
theory_decl : '(' SYM_THEORY symbol? theory_attribute+ ')';
theory_attribute
: KEYWORD_SORTS '(' sort_symbol_decl+ ')'
| KEYWORD_FUNS '(' par_fun_symbol_decl+ ')'
| KEYWORD_SORTS_DESCRIPTION STRING
| KEYWORD_FUNS_DESCRIPTION STRING
| KEYWORD_DEFINITION STRING
| KEYWORD_VALUES STRING
| KEYWORD_NOTES STRING
| attribute
;
logic_attribute
: KEYWORD_THEORIES '(' symbol+ ')'
| KEYWORD_LANGUAGE STRING
| KEYWORD_EXTENSIONS STRING
| KEYWORD_VALUES STRING
| KEYWORD_NOTES STRING
| attribute
;
logic : '(' SYM_LOGIC symbol logic_attribute+ ')';
b_value : SYM_TRUE | SYM_FALSE;
option
: KEYWORD_PRINT_SUCCESS b_value
| KEYWORD_EXPAND_DEFINITIONS b_value
| KEYWORD_INTERACTIVE_MODE b_value
| KEYWORD_PRODUCE_PROOFS b_value
| KEYWORD_PRODUCE_UNSAT_CORES b_value
| KEYWORD_PRODUCE_MODELS b_value
| KEYWORD_PRODUCE_ASSIGNMENTS b_value
| KEYWORD_REGULAR_OUTPUT_CHANNEL STRING
| KEYWORD_DIAGNOSTIC_OUTPUT_CHANNEL STRING
| KEYWORD_RANDOM_SEED NUMERAL
| KEYWORD_VERBOSITY NUMERAL
| attribute
;
info_flag
: KEYWORD_ERROR_BEHAVIOR
| KEYWORD_NAME
| KEYWORD_AUTHORS
| KEYWORD_VERSION
| KEYWORD_STATUS
| KEYWORD_REASON_UNKNOWN
| keyword
| KEYWORD_ALL_STATISTICS
;
command
: '(' TOKEN_CMD_SET_LOGIC symbol ')'
| '(' TOKEN_CMD_SET_OPTION option ')'
| '(' TOKEN_CMD_SET_INFO attribute ')'
| '(' TOKEN_CMD_DECLARE_SORT symbol NUMERAL ')'
| '(' TOKEN_CMD_DEFINE_SORT symbol '(' symbol* ')' sort ')'
| '(' TOKEN_CMD_DECLARE_FUN symbol '(' sort* ')' sort ')'
| '(' TOKEN_CMD_DEFINE_FUN symbol '(' sorted_var* ')' sort term ')'
| '(' TOKEN_CMD_PUSH NUMERAL ')'
| '(' TOKEN_CMD_POP NUMERAL ')'
| '(' TOKEN_CMD_ASSERT term ')'
| '(' TOKEN_CMD_CHECK_SAT ')'
| '(' TOKEN_CMD_GET_ASSERTIONS ')'
| '(' TOKEN_CMD_GET_PROOF ')'
| '(' TOKEN_CMD_GET_UNSAT_CORE ')'
| '(' TOKEN_CMD_GET_VALUE '(' term+ ')' ')'
| '(' TOKEN_CMD_GET_ASSIGNMENT ')'
| '(' TOKEN_CMD_GET_OPTION keyword ')'
| '(' TOKEN_CMD_GET_INFO info_flag ')'
| '(' TOKEN_CMD_EXIT ')'
;
script : command+;
gen_response : SYM_UNSUPPORTED | SYM_SUCCESS | '(' SYM_ERROR STRING ')';
error_behavior : SYM_IMMEDIATE_EXIT | SYM_CONTINUED_EXECUTION;
reason_unknown : SYM_MEMOUT | SYM_INCOMPLETE;
status : SYM_SAT | SYM_UNSAT | SYM_UNKNOWN;
info_response
: KEYWORD_ERROR_BEHAVIOR error_behavior
| KEYWORD_NAME STRING
| KEYWORD_AUTHORS STRING
| KEYWORD_VERSION STRING
| KEYWORD_REASON_UNKNOWN reason_unknown
| attribute
;
get_info_response : '(' info_response+ ')';
check_sat_response : status;
get_assertions_response : '(' term+ ')';
proof : s_expr;
get_proof_response : proof;
get_unsat_core_response : '(' symbol+ ')';
valuation_pair : '(' term term ')';
get_value_response : '(' valuation_pair+ ')';
t_valuation_pair : '(' symbol b_value ')';
get_assignment_response : '(' t_valuation_pair* ')';
get_option_response : attribute_value;