Skip to content

Commit

Permalink
Update comments
Browse files Browse the repository at this point in the history
  • Loading branch information
Thomas Hader committed Jul 2, 2024
1 parent a362b79 commit df03f4f
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion src/frontend/smt2/smt2_lexer.c
Original file line number Diff line number Diff line change
Expand Up @@ -1187,7 +1187,7 @@ static smt2_symbol_t string_to_ff_constant(const char *s, uint32_t n) {
}


/*
/**
* Convert a string s to a symbol code
* - n = length of s
* - return SMT2_SYM_UNKNOWN if s is not a predefined symbol,
Expand All @@ -1199,6 +1199,13 @@ static smt2_symbol_t string_to_ff_constant(const char *s, uint32_t n) {
* returned id is SMT2_SYM_BV_CONSTANT
* - if the string starts with 'bv' but the rest is not <numeral>, then
* the returned if is SMT2_SYM_INVALID_BV_CONSTANT
*
* Special treatment for finite field constants, when the finite field
* theory is active:
* - if the string is of the form 'ff<numeral>' then the
* returned id is SMT2_SYM_FF_CONSTANT
* - if the string starts with 'ff' but the rest is not <numeral>, then
* the returned if is SMT2_SYM_INVALID_FF_CONSTANT
*/
smt2_symbol_t smt2_string_to_symbol(const char *s, uint32_t n) {
const keyword_t *kw;
Expand Down

0 comments on commit df03f4f

Please sign in to comment.