diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4a612ce6f..dc9a324bb 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1643,6 +1643,22 @@ identifier[cvc5::ParseOp& p] api::DatatypeConstructor dc = d.getConstructor(f.toString()); p.d_expr = dc.getTesterTerm(); } + | UPDATE_TOK term[f, f2] + { + if (!f.getSort().isSelector()) + { + PARSER_STATE->parseError( + "Bad syntax for test (_ update X), X must be a selector."); + } + std::string sname = f.toString(); + // get the datatype that f belongs to + api::Sort sf = f.getSort().getSelectorDomainSort(); + api::Datatype d = sf.getDatatype(); + // find the selector + api::DatatypeSelector ds = d.getSelector(f.toString()); + // get the updater term + p.d_expr = ds.getUpdaterTerm(); + } | TUPLE_SEL_TOK m=INTEGER_LITERAL { // we adopt a special syntax (_ tupSel n) @@ -2226,6 +2242,7 @@ DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'dec PAR_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'par'; COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension'; TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is'; +UPDATE_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'update'; MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match'; GET_MODEL_TOK : 'get-model'; BLOCK_MODEL_TOK : 'block-model'; |