This refactors how global declarations are handled in the parser. In particular, we do not push/pop user contexts in the symbol table and manager when global declarations are true, which is an equivalent behavior to declaring symbols globally.
This further refactors to not use ExprManager flags, thus breaking most of the dependencies on the old API.
This is work towards fixing global declarations in the smt2 parser. The parser still does not behave correctly for overloaded symbols + global declarations (e.g. see #4767), which require further refactoring.
This is also work towards migrating the parser not to depend on the old API. There are a few miscellaneous things to change after this PR, but we are very close to breaking this dependency now.
d_declareTerms(&d_context),
d_hasPushedScope(&d_context, false)
{
+ // use an outermost push, to be able to clear all definitions
+ d_context.push();
}
- ~Implementation() {}
+ ~Implementation() { d_context.pop(); }
/** set expression name */
bool setExpressionName(api::Term t,
const std::string& name,
void addModelDeclarationTerm(api::Term t);
/** reset */
void reset();
+ /** reset assertions */
+ void resetAssertions();
/** Push a scope in the expression names. */
void pushScope(bool isUserContext);
/** Pop a scope in the expression names. */
void popScope();
+ /** Have we pushed a scope (e.g. let or quantifier) in the current context? */
+ bool hasPushedScope() const;
private:
/** The context manager for the scope maps. */
const std::string& name,
bool isAssertion)
{
- Trace("sym-manager") << "set expression name: " << t << " -> " << name
- << ", isAssertion=" << isAssertion << std::endl;
+ Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> "
+ << name << ", isAssertion=" << isAssertion << std::endl;
// cannot name subexpressions under quantifiers
PrettyCheckArgument(
!d_hasPushedScope.get(), name, "cannot name function in a scope");
void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s)
{
- Trace("sym-manager") << "addModelDeclarationSort " << s << std::endl;
+ Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s
+ << std::endl;
d_declareSorts.push_back(s);
}
void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t)
{
- Trace("sym-manager") << "addModelDeclarationTerm " << t << std::endl;
+ Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t
+ << std::endl;
d_declareTerms.push_back(t);
}
void SymbolManager::Implementation::pushScope(bool isUserContext)
{
- Trace("sym-manager") << "pushScope, isUserContext = " << isUserContext
- << std::endl;
+ Trace("sym-manager") << "SymbolManager: pushScope, isUserContext = "
+ << isUserContext << std::endl;
PrettyCheckArgument(!d_hasPushedScope.get() || !isUserContext,
"cannot push a user context within a scope context");
d_context.push();
void SymbolManager::Implementation::popScope()
{
- Trace("sym-manager") << "popScope" << std::endl;
+ Trace("sym-manager") << "SymbolManager: popScope" << std::endl;
if (d_context.getLevel() == 0)
{
throw ScopeException();
<< "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
}
+bool SymbolManager::Implementation::hasPushedScope() const
+{
+ return d_hasPushedScope.get();
+}
+
void SymbolManager::Implementation::reset()
{
- // clear names?
+ Trace("sym-manager") << "SymbolManager: reset" << std::endl;
+ // clear names by popping to context level 0
+ while (d_context.getLevel() > 0)
+ {
+ d_context.pop();
+ }
+ // push the outermost context
+ d_context.push();
+}
+
+void SymbolManager::Implementation::resetAssertions()
+{
+ Trace("sym-manager") << "SymbolManager: resetAssertions" << std::endl;
+ // clear names by popping to context level 1
+ while (d_context.getLevel() > 1)
+ {
+ d_context.pop();
+ }
}
// ---------------------------------------------- SymbolManager
void SymbolManager::pushScope(bool isUserContext)
{
+ // we do not push user contexts when global declarations is true. This
+ // policy applies both to the symbol table and to the symbol manager.
+ if (d_globalDeclarations && isUserContext)
+ {
+ return;
+ }
d_implementation->pushScope(isUserContext);
d_symtabAllocated.pushScope();
}
void SymbolManager::popScope()
{
+ // If global declarations is true, then if d_hasPushedScope is false, then
+ // the pop corresponds to a user context, which we did not push. Note this
+ // additionally relies on the fact that user contexts cannot be pushed
+ // within scope contexts. Hence, since we did not push the context, we
+ // do not pop a context here.
+ if (d_globalDeclarations && !d_implementation->hasPushedScope())
+ {
+ return;
+ }
d_symtabAllocated.popScope();
d_implementation->popScope();
}
d_implementation->reset();
}
+void SymbolManager::resetAssertions()
+{
+ d_implementation->resetAssertions();
+ d_symtabAllocated.resetAssertions();
+}
+
} // namespace CVC4
* Reset this symbol manager, which resets the symbol table.
*/
void reset();
+ /**
+ * Reset assertions for this symbol manager, which resets the symbol table.
+ */
+ void resetAssertions();
/** Set global declarations to the value flag. */
void setGlobalDeclarations(bool flag);
/** Get global declarations flag. */
d_typeMap(&d_context),
d_overload_trie(&d_context)
{
+ // use an outermost push, to be able to clear definitions not at level zero
+ d_context.push();
}
- ~Implementation() {
- }
+ ~Implementation() { d_context.pop(); }
bool bind(const string& name, api::Term obj, bool levelZero, bool doOverload);
void bindType(const string& name, api::Sort t, bool levelZero = false);
void pushScope();
size_t getLevel() const;
void reset();
+ void resetAssertions();
//------------------------ operator overloading
/** implementation of function from header */
bool isOverloadedFunction(api::Term fun) const;
bool doOverload)
{
PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null api::Term");
+ Trace("sym-table") << "SymbolTable: bind " << name
+ << ", levelZero=" << levelZero
+ << ", doOverload=" << doOverload << std::endl;
if (doOverload) {
if (!bindWithOverloading(name, obj)) {
return false;
}
void SymbolTable::Implementation::popScope() {
- if (d_context.getLevel() == 0) {
+ // should not pop beyond level one
+ if (d_context.getLevel() == 1)
+ {
throw ScopeException();
}
d_context.pop();
}
void SymbolTable::Implementation::reset() {
+ Trace("sym-table") << "SymbolTable: reset" << std::endl;
this->SymbolTable::Implementation::~Implementation();
new (this) SymbolTable::Implementation();
}
+void SymbolTable::Implementation::resetAssertions()
+{
+ Trace("sym-table") << "SymbolTable: resetAssertions" << std::endl;
+ // pop all contexts
+ while (d_context.getLevel() > 0)
+ {
+ d_context.pop();
+ }
+ d_context.push();
+}
+
bool SymbolTable::Implementation::isOverloadedFunction(api::Term fun) const
{
return d_overload_trie.isOverloadedFunction(fun);
void SymbolTable::pushScope() { d_implementation->pushScope(); }
size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); }
void SymbolTable::reset() { d_implementation->reset(); }
+void SymbolTable::resetAssertions() { d_implementation->resetAssertions(); }
} // namespace CVC4
/** Reset everything. */
void reset();
+ /** Reset assertions. */
+ void resetAssertions();
//------------------------ operator overloading
/** is this function overloaded? */
#include <limits.h>
#include "base/output.h"
-#include "expr/type.h"
#include "parser/antlr_line_buffered_input.h"
#include "parser/bounded_token_buffer.h"
#include "parser/bounded_token_factory.h"
#include <vector>
#include "base/output.h"
-#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/type.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
-
#define REPEAT_COMMAND(k, CommandCtor) \
({ \
unsigned __k = (k); \
{ UNSUPPORTED("POPTO_SCOPE command"); }
| RESET_TOK
- { cmd->reset(new ResetCommand());
+ {
+ cmd->reset(new ResetCommand());
+ // reset the state of the parser, which is independent of the symbol
+ // manager
PARSER_STATE->reset();
}
| RESET_TOK ASSERTIONS_TOK
{ cmd->reset(new ResetAssertionsCommand());
- PARSER_STATE->reset();
}
// Datatypes can be mututally-recursive if they're in the same
idCommaFlag=true;
})?
{
- func = PARSER_STATE->bindVar(id, t, ExprManager::VAR_FLAG_NONE, true);
+ func = PARSER_STATE->bindVar(id, t, false, true);
ids.push_back(id);
types.push_back(t);
funcs.push_back(func);
} else {
Debug("parser") << " " << *i << " not declared" << std::endl;
if(topLevel) {
- api::Term func =
- PARSER_STATE->bindVar(*i, t, ExprManager::VAR_FLAG_GLOBAL);
+ api::Term func = PARSER_STATE->bindVar(*i, t);
Command* decl = new DeclareFunctionCommand(*i, func, t);
seq->addCommand(decl);
} else {
++i) {
Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl;
PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
- api::Term func = PARSER_STATE->mkVar(
- *i,
- t,
- ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
+ api::Term func = SOLVER->mkConst(t, *i);
PARSER_STATE->defineVar(*i, fterm);
Command* decl = new DefineFunctionCommand(*i, func, formals, f, true);
seq->addCommand(decl);
* below. */
: identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
- t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
+ t = PARSER_STATE->mkSort(id2);
params.push_back( t );
}
( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
- t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
+ t = PARSER_STATE->mkSort(id2);
params.push_back( t ); }
)* RBRACKET
)?
#include <antlr3.h>
-#include "expr/expr_manager.h"
#include "parser/antlr_input.h"
#include "parser/parser_exception.h"
#include "parser/cvc/CvcLexer.h"
#include "parser/input.h"
#include "base/output.h"
-#include "expr/type.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
#include <vector>
#include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
#include "options/language.h"
#include "parser/parser_exception.h"
namespace CVC4 {
class Command;
-class Type;
-class FunctionType;
namespace parser {
#include "api/cvc4cpp.h"
#include "base/output.h"
-#include "expr/expr.h"
#include "expr/kind.h"
-#include "expr/type.h"
#include "options/options.h"
#include "parser/input.h"
#include "parser/parser_exception.h"
api::Term Parser::bindVar(const std::string& name,
const api::Sort& type,
- uint32_t flags,
+ bool levelZero,
bool doOverload)
{
- if (d_symman->getGlobalDeclarations())
- {
- flags |= ExprManager::VAR_FLAG_GLOBAL;
- }
+ bool globalDecls = d_symman->getGlobalDeclarations();
Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl;
- api::Term expr = mkVar(name, type, flags);
- defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
+ api::Term expr = d_solver->mkConst(type, name);
+ defineVar(name, expr, globalDecls || levelZero, doOverload);
return expr;
}
Debug("parser") << "bindBoundVar(" << name << ", " << type << ")"
<< std::endl;
api::Term expr = d_solver->mkVar(type, name);
- defineVar(name, expr, false);
+ defineVar(name, expr);
return expr;
}
return vars;
}
-api::Term Parser::mkAnonymousFunction(const std::string& prefix,
- const api::Sort& type,
- uint32_t flags)
-{
- bool globalDecls = d_symman->getGlobalDeclarations();
- if (globalDecls)
- {
- flags |= ExprManager::VAR_FLAG_GLOBAL;
- }
- stringstream name;
- name << prefix << "_anon_" << ++d_anonymousFunctionCount;
- return mkVar(name.str(), type, flags);
-}
-
std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names,
const api::Sort& type,
- uint32_t flags,
+ bool levelZero,
bool doOverload)
{
- bool globalDecls = d_symman->getGlobalDeclarations();
- if (globalDecls)
- {
- flags |= ExprManager::VAR_FLAG_GLOBAL;
- }
std::vector<api::Term> vars;
for (unsigned i = 0; i < names.size(); ++i) {
- vars.push_back(bindVar(names[i], type, flags, doOverload));
+ vars.push_back(bindVar(names[i], type, levelZero, doOverload));
}
return vars;
}
defineType(name, params, type);
}
-api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
+api::Sort Parser::mkSort(const std::string& name)
{
Debug("parser") << "newSort(" << name << ")" << std::endl;
- api::Sort type = d_solver->mkUninterpretedSort(name);
bool globalDecls = d_symman->getGlobalDeclarations();
- defineType(
- name, type, globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
+ api::Sort type = d_solver->mkUninterpretedSort(name);
+ defineType(name, type, globalDecls);
return type;
}
-api::Sort Parser::mkSortConstructor(const std::string& name,
- size_t arity,
- uint32_t flags)
+api::Sort Parser::mkSortConstructor(const std::string& name, size_t arity)
{
Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
<< std::endl;
- api::Sort type = d_solver->mkSortConstructorSort(name, arity);
bool globalDecls = d_symman->getGlobalDeclarations();
- defineType(name,
- vector<api::Sort>(arity),
- type,
- globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
+ api::Sort type = d_solver->mkSortConstructorSort(name, arity);
+ defineType(name, vector<api::Sort>(arity), type, globalDecls);
return type;
}
api::Sort Parser::mkUnresolvedType(const std::string& name)
{
- api::Sort unresolved = mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER);
+ api::Sort unresolved = d_solver->mkUninterpretedSort(name);
+ defineType(name, unresolved);
d_unresolved.insert(unresolved);
return unresolved;
}
api::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name,
size_t arity)
{
- api::Sort unresolved =
- mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER);
+ api::Sort unresolved = d_solver->mkSortConstructorSort(name, arity);
+ defineType(name, vector<api::Sort>(arity), unresolved);
d_unresolved.insert(unresolved);
return unresolved;
}
return t;
}
-//!!!!!!!!!!! temporary
-api::Term Parser::mkVar(const std::string& name,
- const api::Sort& type,
- uint32_t flags)
-{
- return d_solver->mkConst(type, name);
-}
-//!!!!!!!!!!! temporary
-
bool Parser::isDeclared(const std::string& name, SymbolType type) {
switch (type) {
- case SYM_VARIABLE:
- return d_reservedSymbols.find(name) != d_reservedSymbols.end() ||
- d_symtab->isBound(name);
+ case SYM_VARIABLE: return d_symtab->isBound(name);
case SYM_SORT:
return d_symtab->isBoundType(name);
}
return false;
}
-void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) {
- checkDeclaration(varName, CHECK_UNDECLARED, SYM_VARIABLE);
- d_reservedSymbols.insert(varName);
-}
-
void Parser::checkDeclaration(const std::string& varName,
DeclarationCheck check,
SymbolType type,
void Parser::pushScope(bool isUserContext)
{
d_symman->pushScope(isUserContext);
- if (isUserContext)
- {
- d_assertionLevel = scopeLevel();
- }
}
void Parser::popScope()
{
d_symman->popScope();
- if (scopeLevel() < d_assertionLevel)
- {
- d_assertionLevel = scopeLevel();
- d_reservedSymbols.clear();
- }
}
-void Parser::reset() { d_symman->reset(); }
+void Parser::reset() {}
SymbolManager* Parser::getSymbolManager() { return d_symman; }
{
if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage()))
{
- return api::Term(d_solver, d_solver->mkString(s, true).getExpr());
+ return d_solver->mkString(s, true);
}
// otherwise, we must process ad-hoc escape sequences
std::vector<unsigned> str = processAdHocStringEsc(s);
- return api::Term(d_solver, d_solver->mkString(str).getExpr());
+ return d_solver->mkString(str);
}
} /* CVC4::parser namespace */
*/
size_t d_assertionLevel;
- /**
- * Maintains a list of reserved symbols at the assertion level that might
- * not occur in our symbol table. This is necessary to e.g. support the
- * proper behavior of the :named annotation in SMT-LIBv2 when used under
- * a let or a quantifier, since inside a let/quant body the declaration
- * scope is that of the let/quant body, but the defined name should be
- * reserved at the assertion level.
- */
- std::set<std::string> d_reservedSymbols;
-
/** How many anonymous functions we've created. */
size_t d_anonymousFunctionCount;
SymbolType type = SYM_VARIABLE,
std::string notes = "");
- /**
- * Reserve a symbol at the assertion level.
- */
- void reserveSymbolAtAssertionLevel(const std::string& name);
-
/**
* Checks whether the given expression is function-like, i.e.
* it expects arguments. This is checked by looking at the type
*/
void checkFunctionLike(api::Term fun);
- /** Create a new CVC4 variable expression of the given type.
+ /** Create a new CVC4 variable expression of the given type.
*
- * flags specify information about the variable, e.g. whether it is global or defined
- * (see enum in expr_manager_template.h).
+ * It is inserted at context level zero in the symbol table if levelZero is
+ * true, or if we are using global declarations.
*
* If a symbol with name already exists,
* then if doOverload is true, we create overloaded operators.
- * else if doOverload is false, the existing expression is shadowed by the new expression.
+ * else if doOverload is false, the existing expression is shadowed by the
+ * new expression.
*/
api::Term bindVar(const std::string& name,
const api::Sort& type,
- uint32_t flags = ExprManager::VAR_FLAG_NONE,
+ bool levelZero = false,
bool doOverload = false);
/**
* Create a set of new CVC4 variable expressions of the given type.
*
- * flags specify information about the variable, e.g. whether it is global or defined
- * (see enum in expr_manager_template.h).
+ * It is inserted at context level zero in the symbol table if levelZero is
+ * true, or if we are using global declarations.
*
* For each name, if a symbol with name already exists,
* then if doOverload is true, we create overloaded operators.
- * else if doOverload is false, the existing expression is shadowed by the new expression.
+ * else if doOverload is false, the existing expression is shadowed by the
+ * new expression.
*/
std::vector<api::Term> bindVars(const std::vector<std::string> names,
const api::Sort& type,
- uint32_t flags = ExprManager::VAR_FLAG_NONE,
+ bool levelZero = false,
bool doOverload = false);
/**
/**
* Create a set of new CVC4 bound variable expressions of the given type.
*
- * flags specify information about the variable, e.g. whether it is global or defined
- * (see enum in expr_manager_template.h).
- *
* For each name, if a symbol with name already exists,
* then if doOverload is true, we create overloaded operators.
* else if doOverload is false, the existing expression is shadowed by the new expression.
std::vector<api::Term> bindBoundVars(const std::vector<std::string> names,
const api::Sort& type);
- /**
- * Create a new CVC4 function expression of the given type,
- * appending a unique index to its name. (That's the ONLY
- * difference between mkAnonymousFunction() and mkVar()).
- *
- * flags specify information about the variable, e.g. whether it is global or defined
- * (see enum in expr_manager_template.h).
- */
- api::Term mkAnonymousFunction(const std::string& prefix,
- const api::Sort& type,
- uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
/** Create a new variable definition (e.g., from a let binding).
* levelZero is set if the binding must be done at level 0.
* If a symbol with name already exists,
/**
* Creates a new sort with the given name.
*/
- api::Sort mkSort(const std::string& name,
- uint32_t flags = ExprManager::SORT_FLAG_NONE);
+ api::Sort mkSort(const std::string& name);
/**
* Creates a new sort constructor with the given name and arity.
*/
- api::Sort mkSortConstructor(const std::string& name,
- size_t arity,
- uint32_t flags = ExprManager::SORT_FLAG_NONE);
+ api::Sort mkSortConstructor(const std::string& name, size_t arity);
/**
* Creates a new "unresolved type," used only during parsing.
*/
api::Term applyTypeAscription(api::Term t, api::Sort s);
- //!!!!!!!!!!! temporary
- /**
- * Make var, with flags required by the ExprManager, see ExprManager::mkVar.
- */
- api::Term mkVar(const std::string& name,
- const api::Sort& type,
- uint32_t flags);
- //!!!!!!!!!!! temporary
-
/**
* Add an operator to the current legal set.
*
#include "api/cvc4cpp.h"
#include "cvc/cvc.h"
-#include "expr/expr_manager.h"
#include "options/options.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "api/cvc4cpp.h"
#include "base/output.h"
-#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/type.h"
#include "options/set_language.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
else
{
api::Term func =
- PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+ PARSER_STATE->bindVar(name, t, false, true);
cmd->reset(new DeclareFunctionCommand(name, func, t));
}
}
// must not be extended with the name itself; no recursion
// permitted)
// we allow overloading for function definitions
- api::Term func = PARSER_STATE->bindVar(name, t,
- ExprManager::VAR_FLAG_DEFINED, true);
+ api::Term func = PARSER_STATE->bindVar(name, t, false, true);
cmd->reset(new DefineFunctionCommand(
name, func, terms, expr, SYM_MAN->getGlobalDeclarations()));
}
sortSymbol[t,CHECK_DECLARED]
{ // allow overloading here
api::Term c =
- PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+ PARSER_STATE->bindVar(name, t, false, true);
cmd->reset(new DeclareFunctionCommand(name, c, t)); }
/* get model */
/* reset: reset everything, returning solver to initial state.
* Logic and options must be set again. */
| RESET_TOK
- { cmd->reset(new ResetCommand());
+ {
+ cmd->reset(new ResetCommand());
+ // reset the state of the parser, which is independent of the symbol
+ // manager
PARSER_STATE->reset();
}
/* reset-assertions: reset assertions, assertion stack, declarations,
* etc., but the logic and options remain as they were. */
| RESET_ASSERTIONS_TOK
{ cmd->reset(new ResetAssertionsCommand());
- PARSER_STATE->resetAssertions();
}
| DEFINE_FUN_REC_TOK
{ PARSER_STATE->checkThatLogicIsSet(); }
}
// allow overloading
api::Term func =
- PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true);
+ PARSER_STATE->bindVar(name, tt, false, true);
seq->addCommand(new DeclareFunctionCommand(name, func, tt));
sorts.clear();
}
}
// allow overloading
api::Term func =
- PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+ PARSER_STATE->bindVar(name, t, false, true);
seq->addCommand(new DeclareFunctionCommand(name, func, t));
sorts.clear();
}
{ PARSER_STATE->checkUserSymbol(name); }
term[e,e2]
{
- api::Term func = PARSER_STATE->bindVar(name, e.getSort(),
- ExprManager::VAR_FLAG_DEFINED);
+ api::Term func = PARSER_STATE->bindVar(name, e.getSort());
cmd->reset(new DefineFunctionCommand(
name, func, e, SYM_MAN->getGlobalDeclarations()));
}
}
tt = SOLVER->mkFunctionSort(sorts, tt);
}
- api::Term func = PARSER_STATE->bindVar(name, tt,
- ExprManager::VAR_FLAG_DEFINED);
+ api::Term func = PARSER_STATE->bindVar(name, tt);
cmd->reset(new DefineFunctionCommand(
name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
}
// declare the name down here (while parsing term, signature
// must not be extended with the name itself; no recursion
// permitted)
- api::Term func = PARSER_STATE->bindVar(name, t,
- ExprManager::VAR_FLAG_DEFINED);
+ api::Term func = PARSER_STATE->bindVar(name, t);
cmd->reset(new DefineFunctionCommand(
name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
}
LPAREN_TOK /* parametric sorts */
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
{
- sorts.push_back(PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER));
+ sorts.push_back(PARSER_STATE->mkSort(name));
}
)*
RPAREN_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)); }
+ params.push_back( PARSER_STATE->mkSort(name)); }
)*
RPAREN_TOK {
// if the arity was fixed by prelude and is not equal to the number of parameters
#include <algorithm>
#include "base/check.h"
-#include "expr/type.h"
+#include "expr/expr.h"
#include "options/options.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
d_logicSet(false),
d_seenSetLogic(false)
{
- pushScope(true);
}
-Smt2::~Smt2() { popScope(); }
+Smt2::~Smt2() {}
void Smt2::addArithmeticOperators() {
addOperator(api::PLUS, "+");
api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars);
// allow overloading
- return bindVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
+ return bindVar(fname, ft, false, true);
}
void Smt2::pushDefineFunRecScope(
d_logic = LogicInfo();
operatorKindMap.clear();
d_lastNamedTerm = std::pair<api::Term, std::string>();
- this->Parser::reset();
- pushScope(true);
-}
-
-void Smt2::resetAssertions() {
- // Remove all declarations except the ones at level 0.
- while (this->scopeLevel() > 0) {
- this->popScope();
- }
- pushScope(true);
}
std::unique_ptr<Command> Smt2::invConstraint(
else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
{
// tuple selector case
+ std::string indexString = p.d_expr.toString();
Integer x = p.d_expr.getExpr().getConst<Rational>().getNumerator();
if (!x.fitsUnsignedInt())
{
void reset() override;
- void resetAssertions();
-
/**
* Creates a command that adds an invariant constraint.
*
#include <antlr3.h>
-#include "expr/expr_manager.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
#include <antlr3.h>
-#include "expr/expr_manager.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
#include <set>
#include "api/cvc4cpp.h"
-#include "expr/type.h"
#include "options/options.h"
#include "parser/parser.h"
#include "smt/command.h"
{
api::Sort t =
p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
- expr = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
+ expr = bindVar(p.d_name, t, true); // must define at level zero
preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
}
return expr;
api::Sort t =
p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
t = d_solver->mkFunctionSort(sorts, t);
- v = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
+ v = bindVar(p.d_name, t, true); // must define at level zero
preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
}
// args might be rationals, in which case we need to create
#include <antlr3.h>
-#include "expr/expr_manager.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_exception.h"
{
try
{
+ sm->reset();
solver->getSmtEngine()->reset();
d_commandStatus = CommandSuccess::instance();
}
{
try
{
+ sm->resetAssertions();
solver->resetAssertions();
d_commandStatus = CommandSuccess::instance();
}
projects / cvc5.git / commitdiff