diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-29 16:06:50 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-08-29 16:06:50 +0200 |
| commit | e9fb730333b2719cddaa0a9209aa7953d7f30b0b (patch) | |
| tree | da178be240ac8121635bed7cdfde8c58449e65a5 /src/parser | |
| parent | 4397bf2a96fabe124ebd18e9ae9957689852afb3 (diff) | |
Set instantiation level on skolemized bodies of quantifiers. Rename inst-level attribute to quant-inst-max-level
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 2adad092e..9f4b19c47 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1182,7 +1182,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); std::vector<Expr> values; values.push_back( n ); - std::string attr_name("inst-level"); + std::string attr_name("quant-inst-max-level"); Command* c = new SetUserAttributeCommand( attr_name, expr, values ); c->setMuted(true); PARSER_STATE->preemptCommand(c); @@ -1722,7 +1722,7 @@ INCLUDE_TOK : 'include'; ATTRIBUTE_PATTERN_TOK : ':pattern'; ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern'; ATTRIBUTE_NAMED_TOK : ':named'; -ATTRIBUTE_INST_LEVEL : ':inst-level'; +ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; ATTRIBUTE_RR_PRIORITY : ':rr-priority'; // operators (NOTE: theory symbols go here) |