summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/parser.cpp6
-rw-r--r--src/parser/parser.h10
-rw-r--r--src/parser/smt2/Smt2.g45
-rw-r--r--src/parser/smt2/smt2.cpp5
-rw-r--r--src/parser/smt2/smt2.h7
5 files changed, 38 insertions, 35 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index def89e6b1..c5746020c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -775,10 +775,10 @@ void Parser::attributeNotSupported(const std::string& attr) {
size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); }
-void Parser::pushScope(bool bindingLevel)
+void Parser::pushScope(bool isUserContext)
{
- d_symman->pushScope(!bindingLevel);
- if (!bindingLevel)
+ d_symman->pushScope(isUserContext);
+ if (isUserContext)
{
d_assertionLevel = scopeLevel();
}
diff --git a/src/parser/parser.h b/src/parser/parser.h
index d30ea7c16..96a16b31f 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -751,11 +751,13 @@ public:
* Pushes a scope. All subsequent symbol declarations made are only valid in
* this scope, i.e. they are deleted on the next call to popScope.
*
- * The argument bindingLevel is true, the assertion level is set to the
- * current scope level. This determines which scope assertions are declared
- * at.
+ * The argument isUserContext is true, when we are pushing a user context
+ * e.g. via the smt2 command (push n). This may also include one initial
+ * pushScope when the parser is initialized. User-context pushes and pops
+ * have an impact on both expression names and the symbol table, whereas
+ * other pushes and pops only have an impact on the symbol table.
*/
- void pushScope(bool bindingLevel = false);
+ void pushScope(bool isUserContext = false);
void popScope();
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a96686135..916e20d9b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -258,7 +258,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
symbol[name,CHECK_UNDECLARED,SYM_SORT]
{ PARSER_STATE->checkUserSymbol(name); }
LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
- { PARSER_STATE->pushScope(true);
+ { PARSER_STATE->pushScope();
for(std::vector<std::string>::const_iterator i = names.begin(),
iend = names.end();
i != iend;
@@ -319,7 +319,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
}
t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
- PARSER_STATE->pushScope(true);
+ PARSER_STATE->pushScope();
terms = PARSER_STATE->bindBoundVars(sortedVarNames);
}
term[expr, expr2]
@@ -365,6 +365,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
// set the expression name, if there was a named term
std::pair<api::Term, std::string> namedTerm =
PARSER_STATE->lastNamedTerm();
+ // TODO (projects-248)
+ // SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
Command* csen =
new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
csen->setMuted(true);
@@ -422,12 +424,12 @@ command [std::unique_ptr<CVC4::Command>* cmd]
if(num == 0) {
cmd->reset(new EmptyCommand());
} else if(num == 1) {
- PARSER_STATE->pushScope();
+ PARSER_STATE->pushScope(true);
cmd->reset(new PushCommand());
} else {
std::unique_ptr<CommandSequence> seq(new CommandSequence());
do {
- PARSER_STATE->pushScope();
+ PARSER_STATE->pushScope(true);
Command* push_cmd = new PushCommand();
push_cmd->setMuted(num > 1);
seq->addCommand(push_cmd);
@@ -441,7 +443,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
"Strict compliance mode demands an integer to be provided to "
"PUSH. Maybe you want (push 1)?");
} else {
- PARSER_STATE->pushScope();
+ PARSER_STATE->pushScope(true);
cmd->reset(new PushCommand());
}
} )
@@ -549,7 +551,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
( sortSymbol[range,CHECK_DECLARED] )?
{
- PARSER_STATE->pushScope(true);
+ PARSER_STATE->pushScope();
sygusVars = PARSER_STATE->bindBoundVars(sortedVarNames);
}
(
@@ -661,7 +663,7 @@ sygusGrammar[CVC4::api::Grammar*& ret,
RPAREN_TOK
{
// non-terminal symbols in the pre-declaration are locally scoped
- PARSER_STATE->pushScope(true);
+ PARSER_STATE->pushScope();
for (std::pair<std::string, api::Sort>& i : sortedVarNames)
{
PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
@@ -818,7 +820,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
func =
PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars);
PARSER_STATE->pushDefineFunRecScope(
- sortedVarNames, func, flattenVars, bvs, true);
+ sortedVarNames, func, flattenVars, bvs);
}
term[expr, expr2]
{ PARSER_STATE->popScope();
@@ -862,7 +864,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
}
bvs.clear();
PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
- flattenVarsList[0], bvs, true);
+ flattenVarsList[0], bvs);
}
(
term[expr,expr2]
@@ -879,7 +881,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
if( func_defs.size()<funcs.size() ){
bvs.clear();
PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j],
- flattenVarsList[j], bvs, true);
+ flattenVarsList[j], bvs);
}
}
)+
@@ -996,7 +998,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
sortedVarList[sortedVarNames] RPAREN_TOK
{ /* add variables to parser state before parsing term */
Debug("parser") << "define fun: '" << name << "'" << std::endl;
- PARSER_STATE->pushScope(true);
+ PARSER_STATE->pushScope();
terms = PARSER_STATE->bindBoundVars(sortedVarNames);
}
term[e,e2]
@@ -1028,7 +1030,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
sortSymbol[t,CHECK_DECLARED]
{ /* add variables to parser state before parsing term */
Debug("parser") << "define const: '" << name << "'" << std::endl;
- PARSER_STATE->pushScope(true);
+ PARSER_STATE->pushScope();
terms = PARSER_STATE->bindBoundVars(sortedVarNames);
}
term[e, e2]
@@ -1104,7 +1106,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
}
: { PARSER_STATE->checkThatLogicIsSet();
/* open a scope to keep the UnresolvedTypes contained */
- PARSER_STATE->pushScope(true); }
+ PARSER_STATE->pushScope(); }
LPAREN_TOK /* parametric sorts */
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
{
@@ -1174,7 +1176,7 @@ datatypesDef[bool isCo,
std::string name;
std::vector<api::Sort> params;
}
- : { PARSER_STATE->pushScope(true);
+ : { PARSER_STATE->pushScope();
// Declare the datatypes that are currently being defined as unresolved
// types. If we do not know the arity of the datatype yet, we wait to
// define it until parsing the preamble of its body, which may optionally
@@ -1201,7 +1203,7 @@ datatypesDef[bool isCo,
PARSER_STATE->parseError("Too many datatypes defined in this block.");
}
}
- ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK
+ ( PAR_TOK { PARSER_STATE->pushScope(); } LPAREN_TOK
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
{
params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); }
@@ -1362,7 +1364,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
{
PARSER_STATE->parseError("Quantifier used in non-quantified logic.");
}
- PARSER_STATE->pushScope(true);
+ PARSER_STATE->pushScope();
}
boundVarList[bvl]
term[f, f2] RPAREN_TOK
@@ -1377,7 +1379,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
expr = MK_TERM(kind, args);
}
| LPAREN_TOK COMPREHENSION_TOK
- { PARSER_STATE->pushScope(true); }
+ { PARSER_STATE->pushScope(); }
boundVarList[bvl]
{
args.push_back(bvl);
@@ -1396,7 +1398,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
| /* a let or sygus let binding */
LPAREN_TOK
LET_TOK LPAREN_TOK
- { PARSER_STATE->pushScope(true); }
+ { PARSER_STATE->pushScope(); }
( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
term[expr, f2]
RPAREN_TOK
@@ -1434,7 +1436,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
// case with non-nullary pattern
LPAREN_TOK LPAREN_TOK term[f, f2] {
args.clear();
- PARSER_STATE->pushScope(true);
+ PARSER_STATE->pushScope();
// f should be a constructor
type = f.getSort();
Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
@@ -1553,7 +1555,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
}
| /* lambda */
LPAREN_TOK HO_LAMBDA_TOK
- { PARSER_STATE->pushScope(true); }
+ { PARSER_STATE->pushScope(); }
boundVarList[bvl]
term[f, f2] RPAREN_TOK
{
@@ -1842,6 +1844,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr);
std::string name = sexpr.getValue();
// bind name to expr with define-fun
+ // TODO (projects-248) SYM_MAN->setExpressionName(func, name, false);
Command* c =
new DefineNamedFunctionCommand(name,
func,
@@ -2180,7 +2183,7 @@ datatypeDef[bool isCo, std::vector<CVC4::api::DatatypeDecl>& datatypes,
* datatypes won't work, because this type will already be
* "defined" as an unresolved type; don't worry, we check
* below. */
- : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
+ : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
{
datatypes.push_back(SOLVER->mkDatatypeDecl(id, params, isCo));
}
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 1decb3b1c..892c628dc 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -452,10 +452,9 @@ void Smt2::pushDefineFunRecScope(
const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
api::Term func,
const std::vector<api::Term>& flattenVars,
- std::vector<api::Term>& bvs,
- bool bindingLevel)
+ std::vector<api::Term>& bvs)
{
- pushScope(bindingLevel);
+ pushScope();
// bound variables are those that are explicitly named in the preamble
// of the define-fun(s)-rec command, we define them here
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index eeedbec55..734b00f92 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -169,7 +169,7 @@ class Smt2 : public Parser
/** Push scope for define-fun-rec
*
- * This calls Parser::pushScope(bindingLevel) and sets up
+ * This calls Parser::pushScope() and sets up
* initial information for reading a body of a function definition
* in the define-fun-rec and define-funs-rec command.
* The input parameters func/flattenVars are the result
@@ -180,7 +180,7 @@ class Smt2 : public Parser
* flattenVars : the implicit variables introduced when defining func.
*
* This function:
- * (1) Calls Parser::pushScope(bindingLevel).
+ * (1) Calls Parser::pushScope().
* (2) Computes the bound variable list for the quantified formula
* that defined this definition and stores it in bvs.
*/
@@ -188,8 +188,7 @@ class Smt2 : public Parser
const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
api::Term func,
const std::vector<api::Term>& flattenVars,
- std::vector<api::Term>& bvs,
- bool bindingLevel = false);
+ std::vector<api::Term>& bvs);
void reset() override;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback