diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-07 15:34:56 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-07 15:34:56 +0200 |
commit | 33d0894b7707e3f590404cc51963af7740e7412a (patch) | |
tree | d3861424cc124d6b8919ee99eccf120787986a2c /src/parser | |
parent | c83882c37a5568f887badb22bd24397f7d545b9d (diff) |
Refactor quantifiers attributes.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 28 |
1 files changed, 13 insertions, 15 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e7d614b85..366c76194 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1079,7 +1079,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] ( attribute[expr, attexpr, attr] - { if( ( attr == ":pattern" || attr == ":no-pattern" ) && ! attexpr.isNull()) { + { if( ! attexpr.isNull()) { patexprs.push_back( attexpr ); } } @@ -1199,7 +1199,11 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] } std::string attr_name = attr; attr_name.erase( attr_name.begin() ); - Command* c = new SetUserAttributeCommand( attr_name, expr ); + //will set the attribute on auxiliary var (preserves attribute on formula through rewriting) + Type t = EXPR_MANAGER->booleanType(); + Expr avar = PARSER_STATE->mkVar(attr_name, t); + retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); + Command* c = new SetUserAttributeCommand( attr_name, avar ); c->setMuted(true); PARSER_STATE->preemptCommand(c); } else { @@ -1216,23 +1220,17 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] attr = std::string(":no-pattern"); retExpr = MK_EXPR(kind::INST_NO_PATTERN, patexpr); } - | ATTRIBUTE_INST_LEVEL INTEGER_LITERAL + | tok=( ATTRIBUTE_INST_LEVEL | ATTRIBUTE_RR_PRIORITY ) INTEGER_LITERAL { Expr n = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); std::vector<Expr> values; values.push_back( n ); - std::string attr_name("quant-inst-max-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 ); + std::string attr_name(AntlrInput::tokenText($tok)); + attr_name.erase( attr_name.begin() ); + Type t = EXPR_MANAGER->booleanType(); + Expr avar = PARSER_STATE->mkVar(attr_name, t); + retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); + Command* c = new SetUserAttributeCommand( attr_name, avar, values ); c->setMuted(true); PARSER_STATE->preemptCommand(c); } |