diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-28 14:28:31 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-28 14:28:31 +0100 |
commit | 55323fd7283d758caf31e637be237d2416b86167 (patch) | |
tree | 250940ce676196591ddc35bed7291991545e6271 /src/parser | |
parent | 3ff5a32a45f2830acc4600b38332a287db4cf60a (diff) |
Initial infrastructure for function definition quantifiers, internal parsing format for Smt2.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 39 |
1 files changed, 29 insertions, 10 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0a3773d08..35566be45 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1298,21 +1298,40 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] PARSER_STATE->warning(ss.str()); } // do nothing - } else if(attr==":axiom" || attr==":conjecture" || attr==":sygus" || attr==":synthesis") { + } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" || attr==":sygus" || attr==":synthesis") { if(hasValue) { std::stringstream ss; ss << "warning: Attribute " << attr << " does not take a value (ignoring)"; PARSER_STATE->warning(ss.str()); } - std::string attr_name = attr; - attr_name.erase( attr_name.begin() ); - //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); + bool success = true; + if( attr==":fun-def" ){ + if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || expr[0].getKind()!=kind::APPLY_UF ){ + success = false; + }else{ + for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){ + if( expr[0][i].getKind()!=kind::BOUND_VARIABLE ){ + success = false; + } + } + } + if( !success ){ + std::stringstream ss; + ss << "warning: Function definition should be an equality whose LHS is an uninterpreted function applied to variables."; + PARSER_STATE->warning(ss.str()); + } + } + if( success ){ + std::string attr_name = attr; + attr_name.erase( attr_name.begin() ); + //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 { PARSER_STATE->attributeNotSupported(attr); } |