summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g4
-rw-r--r--src/parser/parser.cpp17
-rw-r--r--src/parser/parser.h3
-rw-r--r--src/parser/smt/Smt.g2
-rw-r--r--src/parser/smt2/Smt2.g6
-rw-r--r--src/parser/tptp/Tptp.g4
6 files changed, 24 insertions, 12 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 05fed15ea..3c4a51ad4 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1254,14 +1254,14 @@ prefixFormula[CVC4::Expr& f]
{ PARSER_STATE->pushScope(); } LPAREN
boundVarDecl[ids,t]
{ for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
- bvs.push_back(PARSER_STATE->mkVar(*i, t));
+ bvs.push_back(PARSER_STATE->mkBoundVar(*i, t));
}
ids.clear();
}
( COMMA boundVarDecl[ids,t]
{
for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
- bvs.push_back(PARSER_STATE->mkVar(*i, t));
+ bvs.push_back(PARSER_STATE->mkBoundVar(*i, t));
}
ids.clear();
}
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 29db640c7..bf7c372b7 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -150,6 +150,14 @@ Parser::mkVar(const std::string& name, const Type& type,
}
Expr
+Parser::mkBoundVar(const std::string& name, const Type& type) {
+ Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
+ Expr expr = d_exprManager->mkBoundVar(name, type);
+ defineVar(name, expr, false);
+ return expr;
+}
+
+Expr
Parser::mkFunction(const std::string& name, const Type& type,
bool levelZero) {
Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
@@ -178,7 +186,8 @@ Parser::mkVars(const std::vector<std::string> names,
void
Parser::defineVar(const std::string& name, const Expr& val,
- bool levelZero) {
+ bool levelZero) {
+ Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;;
d_symtab->bind(name, val, levelZero);
Assert( isDeclared(name) );
}
@@ -300,14 +309,14 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
Expr::printtypes::Scope pts(Debug("parser-idt"), true);
Expr constructor = ctor.getConstructor();
Debug("parser-idt") << "+ define " << constructor << std::endl;
- string constructorName = constructor.toString();
+ string constructorName = ctor.getName();
if(isDeclared(constructorName, SYM_VARIABLE)) {
throw ParserException(constructorName + " already declared");
}
defineVar(constructorName, constructor);
Expr tester = ctor.getTester();
Debug("parser-idt") << "+ define " << tester << std::endl;
- string testerName = tester.toString();
+ string testerName = ctor.getTesterName();
if(isDeclared(testerName, SYM_VARIABLE)) {
throw ParserException(testerName + " already declared");
}
@@ -318,7 +327,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
++k) {
Expr selector = (*k).getSelector();
Debug("parser-idt") << "+++ define " << selector << std::endl;
- string selectorName = selector.toString();
+ string selectorName = (*k).getName();
if(isDeclared(selectorName, SYM_VARIABLE)) {
throw ParserException(selectorName + " already declared");
}
diff --git a/src/parser/parser.h b/src/parser/parser.h
index f3210ae29..7efc4d78c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -347,6 +347,9 @@ public:
mkVars(const std::vector<std::string> names, const Type& type,
bool levelZero = false);
+ /** Create a new CVC4 bound variable expression of the given type. */
+ Expr mkBoundVar(const std::string& name, const Type& type);
+
/** Create a new CVC4 function expression of the given type. */
Expr mkFunction(const std::string& name, const Type& type,
bool levelZero = false);
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index f9c38385f..0298497e9 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -253,7 +253,7 @@ annotatedFormula[CVC4::Expr& expr]
( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } )
{ PARSER_STATE->pushScope(); }
( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
- { args.push_back(PARSER_STATE->mkVar(name, t)); }
+ { args.push_back(PARSER_STATE->mkBoundVar(name, t)); }
)+
annotatedFormula[expr] RPAREN_TOK
{ args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) );
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 456e3c656..d8157acbc 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -407,7 +407,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
sortedVarNames.begin(), iend = sortedVarNames.end();
i != iend;
++i) {
- args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+ args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
}
bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
}
@@ -448,7 +448,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
sortedVarNames.begin(), iend = sortedVarNames.end();
i != iend;
++i) {
- args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+ args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
}
bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
}
@@ -597,7 +597,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
sortedVarNames.begin(), iend = sortedVarNames.end();
i != iend;
++i) {
- args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+ args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
}
Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
args.clear();
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 63774a087..068e92cd7 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -327,7 +327,7 @@ variable[CVC4::Expr & expr]
if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)){
expr = PARSER_STATE->getVariable(name);
} else {
- expr = PARSER_STATE->mkVar(name, PARSER_STATE->d_unsorted);
+ expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
if(PARSER_STATE->cnf) PARSER_STATE->addFreeVar(expr);
}
}
@@ -402,7 +402,7 @@ bindvariable[CVC4::Expr & expr]
: UPPER_WORD
{
std::string name = AntlrInput::tokenText($UPPER_WORD);
- expr = PARSER_STATE->mkVar(name, PARSER_STATE->d_unsorted);
+ expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
}
;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback