summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/parser.cpp16
-rw-r--r--src/parser/parser.h8
-rw-r--r--src/parser/smt2/Smt2.g54
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback