diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.cpp | 16 | ||||
-rw-r--r-- | src/parser/parser.h | 8 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 54 |
3 files changed, 63 insertions, 15 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 045cd4ae1..dc44ed5ba 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -26,9 +26,12 @@ #include "parser/parser_exception.h" #include "expr/command.h" #include "expr/expr.h" +#include "expr/node.h" #include "expr/kind.h" #include "expr/type.h" #include "util/output.h" +#include "util/resource_manager.h" +#include "options/options.h" using namespace std; using namespace CVC4::kind; @@ -38,6 +41,7 @@ namespace parser { Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : d_exprManager(exprManager), + d_resourceManager(d_exprManager->getResourceManager()), d_input(input), d_symtabAllocated(), d_symtab(&d_symtabAllocated), @@ -460,7 +464,7 @@ void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); } -Command* Parser::nextCommand() throw(ParserException) { +Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) { Debug("parser") << "nextCommand()" << std::endl; Command* cmd = NULL; if(!d_commandQueue.empty()) { @@ -483,11 +487,19 @@ Command* Parser::nextCommand() throw(ParserException) { } } Debug("parser") << "nextCommand() => " << cmd << std::endl; + if (cmd != NULL && + dynamic_cast<SetOptionCommand*>(cmd) == NULL && + dynamic_cast<QuitCommand*>(cmd) == NULL) { + // don't count set-option commands as to not get stuck in an infinite + // loop of resourcing out + d_resourceManager->spendResource(); + } return cmd; } -Expr Parser::nextExpression() throw(ParserException) { +Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) { Debug("parser") << "nextExpression()" << std::endl; + d_resourceManager->spendResource(); Expr result; if(!done()) { try { diff --git a/src/parser/parser.h b/src/parser/parser.h index ffe33a980..53241709d 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -30,6 +30,7 @@ #include "expr/symbol_table.h" #include "expr/kind.h" #include "expr/expr_stream.h" +#include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -39,6 +40,7 @@ class ExprManager; class Command; class FunctionType; class Type; +class ResourceManager; namespace parser { @@ -108,6 +110,8 @@ class CVC4_PUBLIC Parser { /** The expression manager */ ExprManager *d_exprManager; + /** The resource manager associated with this expr manager */ + ResourceManager *d_resourceManager; /** The input that we're parsing. */ Input *d_input; @@ -504,10 +508,10 @@ public: bool isPredicate(const std::string& name); /** Parse and return the next command. */ - Command* nextCommand() throw(ParserException); + Command* nextCommand() throw(ParserException, UnsafeInterruptException); /** Parse and return the next expression. */ - Expr nextExpression() throw(ParserException); + Expr nextExpression() throw(ParserException, UnsafeInterruptException); /** Issue a warning to the user. */ inline void warning(const std::string& msg) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0a3773d08..511b67997 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1298,21 +1298,49 @@ 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{ + FunctionType t = (FunctionType)expr[0].getOperator().getType(); + for( unsigned i=0; i<expr[0].getNumChildren(); i++ ){ + if( expr[0][i].getKind()!=kind::BOUND_VARIABLE || expr[0][i].getType()!=t.getArgTypes()[i] ){ + success = false; + break; + }else{ + for( unsigned j=0; j<i; j++ ){ + if( expr[0][j]==expr[0][i] ){ + success = false; + break; + } + } + } + } + } + if( !success ){ + std::stringstream ss; + ss << "warning: Function definition should be an equality whose LHS is an uninterpreted function applied to unique 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); } @@ -1592,6 +1620,8 @@ builtinOp[CVC4::Kind& kind] | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } + + | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } // NOTE: Theory operators go here ; @@ -1856,7 +1886,7 @@ GET_ASSERTIONS_TOK : 'get-assertions'; GET_PROOF_TOK : 'get-proof'; GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; -RESET_TOK : 'reset'; +RESET_TOK : { PARSER_STATE->v2_5() }? 'reset'; RESET_ASSERTIONS_TOK : 'reset-assertions'; ITE_TOK : 'ite'; LET_TOK : 'let'; @@ -1998,6 +2028,8 @@ DTSIZE_TOK : 'dt.size'; FMFCARD_TOK : 'fmf.card'; +INST_CLOSURE_TOK : 'inst-closure'; + EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; // Other set theory operators are not // tokenized and handled directly when |