diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-18 12:47:07 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-18 12:47:07 +0200 |
commit | fe7a5119d5b48a2546ece43574bc4d07e86c14a7 (patch) | |
tree | e64192933867061c3b215ee02e0d3aafad6b419e /src/parser | |
parent | 18da2141dcddf221f0a40782b02a24766f0ed2c7 (diff) |
Add support for quantifier-specific instantiation levels. Add option for setting inst-level 0 only for input terms.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d512437af..3f8e321dd 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1167,6 +1167,26 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] attr = std::string(":no-pattern"); PARSER_STATE->attributeNotSupported(attr); } + | ATTRIBUTE_INST_LEVEL INTEGER_LITERAL + { + Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); + std::vector<Expr> values; + values.push_back( n ); + std::string attr_name("inst-level"); + Command* c = new SetUserAttributeCommand( attr_name, expr, values ); + c->setMuted(true); + PARSER_STATE->preemptCommand(c); + } + | ATTRIBUTE_RR_PRIORITY_LEVEL INTEGER_LITERAL + { + Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); + std::vector<Expr> values; + values.push_back( n ); + std::string attr_name("rr-priority"); + Command* c = new SetUserAttributeCommand( attr_name, expr, values ); + c->setMuted(true); + PARSER_STATE->preemptCommand(c); + } | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] { attr = std::string(":named"); @@ -1690,6 +1710,8 @@ INCLUDE_TOK : 'include'; ATTRIBUTE_PATTERN_TOK : ':pattern'; ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern'; ATTRIBUTE_NAMED_TOK : ':named'; +ATTRIBUTE_INST_LEVEL : ':inst-level'; +ATTRIBUTE_RR_PRIORITY : ':rr-priority'; // operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; |