options/options_handler.h
options/options_listener.h
options/options_public.h
+ # !!! TEMPORARY !!!
+ # We currently add the symbol manager and the symbol table to both libcvc5
+ # and libcvc5parser as a stopgap solution, because the command infrastructure
+ # is still in libcvc5. Once PR #8893 is merged, they can be removed from
+ # libcvc5. We have to add them to libcvc5 because linking a DLL for Windows
+ # requires all symbols to be present. Concretely, because of the commands, we
+ # need the symbols for the symbol manager/table to link libcvc5.
+ parser/api/cpp/symbol_manager.cpp
+ parser/api/cpp/symbol_manager.h
+ parser/symbol_table.cpp
+ parser/symbol_table.h
+ # !!! /TEMPORARY !!!
preprocessing/assertion_pipeline.cpp
preprocessing/assertion_pipeline.h
preprocessing/learned_literal_manager.cpp
* possible.
*/
-#include "cvc5_private.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__CONTEXT__CDHASHMAP_H
#define CVC5__CONTEXT__CDHASHMAP_H
* Context-dependent set class.
*/
-#include "cvc5_private.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__CONTEXT__CDHASHSET_H
#define CVC5__CONTEXT__CDHASHSET_H
* - Does not accept TNodes as keys.
*/
+#include "cvc5parser_public.h"
+
+#ifndef CVC5__CONTEXT__CDINSERT_HASHMAP_H
+#define CVC5__CONTEXT__CDINSERT_HASHMAP_H
+
#include <deque>
#include <functional>
#include <unordered_map>
#include "base/output.h"
#include "context/cdinsert_hashmap_forward.h"
#include "context/context.h"
-#include "cvc5_private.h"
-#include "expr/node.h"
-#pragma once
+namespace cvc5 {
-namespace cvc5::context {
+namespace internal {
+template <bool ref_count>
+class NodeTemplate;
+}
+
+namespace context {
template <class Key, class Data, class HashFcn = std::hash<Key> >
class InsertHashMap {
};/* class CDInsertHashMap<> */
template <class Data, class HashFcn>
-class CDInsertHashMap<internal::TNode, Data, HashFcn> : public ContextObj
+class CDInsertHashMap<internal::NodeTemplate<false>, Data, HashFcn>
+ : public ContextObj
{
/* CDInsertHashMap is challenging to get working with TNode.
* Consider using CDHashMap<TNode,...> instead.
"Cannot create a CDInsertHashMap with TNode keys");
};
-} // namespace cvc5::context
+} // namespace context
+} // namespace cvc5
+
+#endif
* simply shortened.
*/
-#include "cvc5_private.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__CONTEXT__CDLIST_H
#define CVC5__CONTEXT__CDLIST_H
* A context-dependent object.
*/
-#include "cvc5_private.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__CONTEXT__CDO_H
#define CVC5__CONTEXT__CDO_H
* Context class and context manager.
*/
-#include "cvc5_private.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__CONTEXT__CONTEXT_H
#define CVC5__CONTEXT__CONTEXT_H
* ContextMemoryManager. A copy is stored in each Scope object for quick
* access.
*/
-class Context {
-
+class CVC5_EXPORT Context
+{
/**
* Pointer to the ContextMemoryManager for this Context.
*/
*/
void addNotifyObjPost(ContextNotifyObj* pCNO);
-};/* class Context */
-
+}; /* class Context */
/**
* A UserContext is different from a Context only because it's used for
* argument as the special constructor in this class (and pass it
* on to all ContextObj instances).
*/
-class ContextObj {
+class CVC5_EXPORT ContextObj
+{
/**
* Pointer to Scope in which this object was last modified.
*/
*/
void enqueueToGarbageCollect();
-};/* class ContextObj */
+}; /* class ContextObj */
/**
* For more flexible context-dependent behavior than that provided by
* Designed for use by ContextManager.
*/
-#include "cvc5_private.h"
+#include "cvc5parser_public.h"
#ifndef CVC5__CONTEXT__CONTEXT_MM_H
#define CVC5__CONTEXT__CONTEXT_MM_H
#endif
#include <vector>
+#include "cvc5_export.h"
+
namespace cvc5::context {
#ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER
* releases the new region and restores the top region from the stack.
*
*/
-class ContextMemoryManager {
-
+class CVC5_EXPORT ContextMemoryManager
+{
/**
* Memory in regions is allocated in chunks. This is the chunk size
*/
*/
void pop();
-};/* class ContextMemoryManager */
+}; /* class ContextMemoryManager */
#else /* CVC5_DEBUG_CONTEXT_MEMORY_MANAGER */
skolem_manager.h
subtype_elim_node_converter.cpp
subtype_elim_node_converter.h
- symbol_manager.cpp
- symbol_manager.h
- symbol_table.cpp
- symbol_table.h
term_canonize.cpp
term_canonize.h
term_context.cpp
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Mathias Preiner, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * The symbol manager.
- */
-
-#include "expr/symbol_manager.h"
-
-#include "context/cdhashmap.h"
-#include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "context/cdo.h"
-
-using namespace cvc5::context;
-
-namespace cvc5 {
-
-// ---------------------------------------------- SymbolManager::Implementation
-
-class SymbolManager::Implementation
-{
- using TermStringMap =
- CDHashMap<cvc5::Term, std::string, std::hash<cvc5::Term>>;
- using TermSet = CDHashSet<cvc5::Term, std::hash<cvc5::Term>>;
- using SortList = CDList<cvc5::Sort>;
- using TermList = CDList<cvc5::Term>;
-
- public:
- Implementation()
- : d_context(),
- d_names(&d_context),
- d_namedAsserts(&d_context),
- d_declareSorts(&d_context),
- d_declareTerms(&d_context),
- d_funToSynth(&d_context),
- d_hasPushedScope(&d_context, false),
- d_lastSynthName(&d_context)
- {
- // use an outermost push, to be able to clear all definitions
- d_context.push();
- }
-
- ~Implementation() { d_context.pop(); }
- /** set expression name */
- NamingResult setExpressionName(cvc5::Term t,
- const std::string& name,
- bool isAssertion = false);
- /** get expression name */
- bool getExpressionName(cvc5::Term t,
- std::string& name,
- bool isAssertion = false) const;
- /** get expression names */
- void getExpressionNames(const std::vector<cvc5::Term>& ts,
- std::vector<std::string>& names,
- bool areAssertions = false) const;
- /** get expression names */
- std::map<cvc5::Term, std::string> getExpressionNames(
- bool areAssertions) const;
- /** get model declare sorts */
- std::vector<cvc5::Sort> getModelDeclareSorts() const;
- /** get model declare terms */
- std::vector<cvc5::Term> getModelDeclareTerms() const;
- /** get functions to synthesize */
- std::vector<cvc5::Term> getFunctionsToSynthesize() const;
- /** Add declared sort to the list of model declarations. */
- void addModelDeclarationSort(cvc5::Sort s);
- /** Add declared term to the list of model declarations. */
- void addModelDeclarationTerm(cvc5::Term t);
- /** Add function to the list of functions to synthesize. */
- void addFunctionToSynthesize(cvc5::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;
- /** Set the last abduct-to-synthesize had the given name. */
- void setLastSynthName(const std::string& name);
- /** Get the name of the last abduct-to-synthesize */
- const std::string& getLastSynthName() const;
-
- private:
- /** The context manager for the scope maps. */
- Context d_context;
- /** Map terms to names */
- TermStringMap d_names;
- /** The set of terms with assertion names */
- TermSet d_namedAsserts;
- /** Declared sorts (for model printing) */
- SortList d_declareSorts;
- /** Declared terms (for model printing) */
- TermList d_declareTerms;
- /** Functions to synthesize (for response to check-synth) */
- TermList d_funToSynth;
- /**
- * Have we pushed a scope (e.g. a let or quantifier) in the current context?
- */
- CDO<bool> d_hasPushedScope;
- /** The last abduct or interpolant to synthesize name */
- CDO<std::string> d_lastSynthName;
-};
-
-NamingResult SymbolManager::Implementation::setExpressionName(
- cvc5::Term t, const std::string& name, bool isAssertion)
-{
- Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> "
- << name << ", isAssertion=" << isAssertion << std::endl;
- if (d_hasPushedScope.get())
- {
- // cannot name subexpressions under binders
- return NamingResult::ERROR_IN_BINDER;
- }
-
- if (isAssertion)
- {
- d_namedAsserts.insert(t);
- }
- if (d_names.find(t) != d_names.end())
- {
- // already named assertion
- return NamingResult::ERROR_ALREADY_NAMED;
- }
- d_names[t] = name;
- return NamingResult::SUCCESS;
-}
-
-bool SymbolManager::Implementation::getExpressionName(cvc5::Term t,
- std::string& name,
- bool isAssertion) const
-{
- TermStringMap::const_iterator it = d_names.find(t);
- if (it == d_names.end())
- {
- return false;
- }
- if (isAssertion)
- {
- // must be an assertion name
- if (d_namedAsserts.find(t) == d_namedAsserts.end())
- {
- return false;
- }
- }
- name = (*it).second;
- return true;
-}
-
-void SymbolManager::Implementation::getExpressionNames(
- const std::vector<cvc5::Term>& ts,
- std::vector<std::string>& names,
- bool areAssertions) const
-{
- for (const cvc5::Term& t : ts)
- {
- std::string name;
- if (getExpressionName(t, name, areAssertions))
- {
- names.push_back(name);
- }
- }
-}
-
-std::map<cvc5::Term, std::string>
-SymbolManager::Implementation::getExpressionNames(bool areAssertions) const
-{
- std::map<cvc5::Term, std::string> emap;
- for (TermStringMap::const_iterator it = d_names.begin(),
- itend = d_names.end();
- it != itend;
- ++it)
- {
- cvc5::Term t = (*it).first;
- if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end())
- {
- continue;
- }
- emap[t] = (*it).second;
- }
- return emap;
-}
-
-std::vector<cvc5::Sort> SymbolManager::Implementation::getModelDeclareSorts()
- const
-{
- std::vector<cvc5::Sort> declareSorts(d_declareSorts.begin(),
- d_declareSorts.end());
- return declareSorts;
-}
-
-std::vector<cvc5::Term> SymbolManager::Implementation::getModelDeclareTerms()
- const
-{
- std::vector<cvc5::Term> declareTerms(d_declareTerms.begin(),
- d_declareTerms.end());
- return declareTerms;
-}
-
-std::vector<cvc5::Term>
-SymbolManager::Implementation::getFunctionsToSynthesize() const
-{
- return std::vector<cvc5::Term>(d_funToSynth.begin(), d_funToSynth.end());
-}
-
-void SymbolManager::Implementation::addModelDeclarationSort(cvc5::Sort s)
-{
- Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s
- << std::endl;
- d_declareSorts.push_back(s);
-}
-
-void SymbolManager::Implementation::addModelDeclarationTerm(cvc5::Term t)
-{
- Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t
- << std::endl;
- d_declareTerms.push_back(t);
-}
-
-void SymbolManager::Implementation::addFunctionToSynthesize(cvc5::Term f)
-{
- Trace("sym-manager") << "SymbolManager: addFunctionToSynthesize " << f
- << std::endl;
- d_funToSynth.push_back(f);
-}
-
-void SymbolManager::Implementation::pushScope(bool isUserContext)
-{
- 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();
- if (!isUserContext)
- {
- d_hasPushedScope = true;
- }
-}
-
-void SymbolManager::Implementation::popScope()
-{
- Trace("sym-manager") << "SymbolManager: popScope" << std::endl;
- if (d_context.getLevel() == 0)
- {
- throw internal::ScopeException();
- }
- d_context.pop();
- Trace("sym-manager-debug")
- << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
-}
-
-bool SymbolManager::Implementation::hasPushedScope() const
-{
- return d_hasPushedScope.get();
-}
-
-void SymbolManager::Implementation::setLastSynthName(const std::string& name)
-{
- d_lastSynthName = name;
-}
-
-const std::string& SymbolManager::Implementation::getLastSynthName() const
-{
- return d_lastSynthName.get();
-}
-
-void SymbolManager::Implementation::reset()
-{
- 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
-
-SymbolManager::SymbolManager(cvc5::Solver* s)
- : d_solver(s),
- d_implementation(new SymbolManager::Implementation()),
- d_globalDeclarations(false)
-{
-}
-
-SymbolManager::~SymbolManager() {}
-
-internal::SymbolTable* SymbolManager::getSymbolTable()
-{
- return &d_symtabAllocated;
-}
-
-NamingResult SymbolManager::setExpressionName(cvc5::Term t,
- const std::string& name,
- bool isAssertion)
-{
- return d_implementation->setExpressionName(t, name, isAssertion);
-}
-
-bool SymbolManager::getExpressionName(cvc5::Term t,
- std::string& name,
- bool isAssertion) const
-{
- return d_implementation->getExpressionName(t, name, isAssertion);
-}
-
-void SymbolManager::getExpressionNames(const std::vector<cvc5::Term>& ts,
- std::vector<std::string>& names,
- bool areAssertions) const
-{
- return d_implementation->getExpressionNames(ts, names, areAssertions);
-}
-
-std::map<cvc5::Term, std::string> SymbolManager::getExpressionNames(
- bool areAssertions) const
-{
- return d_implementation->getExpressionNames(areAssertions);
-}
-std::vector<cvc5::Sort> SymbolManager::getModelDeclareSorts() const
-{
- return d_implementation->getModelDeclareSorts();
-}
-std::vector<cvc5::Term> SymbolManager::getModelDeclareTerms() const
-{
- return d_implementation->getModelDeclareTerms();
-}
-
-std::vector<cvc5::Term> SymbolManager::getFunctionsToSynthesize() const
-{
- return d_implementation->getFunctionsToSynthesize();
-}
-
-void SymbolManager::addModelDeclarationSort(cvc5::Sort s)
-{
- d_implementation->addModelDeclarationSort(s);
-}
-
-void SymbolManager::addModelDeclarationTerm(cvc5::Term t)
-{
- d_implementation->addModelDeclarationTerm(t);
-}
-
-void SymbolManager::addFunctionToSynthesize(cvc5::Term f)
-{
- d_implementation->addFunctionToSynthesize(f);
-}
-
-size_t SymbolManager::scopeLevel() const
-{
- return d_symtabAllocated.getLevel();
-}
-
-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();
-}
-
-void SymbolManager::setGlobalDeclarations(bool flag)
-{
- d_globalDeclarations = flag;
-}
-
-bool SymbolManager::getGlobalDeclarations() const
-{
- return d_globalDeclarations;
-}
-
-void SymbolManager::setLastSynthName(const std::string& name)
-{
- d_implementation->setLastSynthName(name);
-}
-
-const std::string& SymbolManager::getLastSynthName() const
-{
- return d_implementation->getLastSynthName();
-}
-
-void SymbolManager::reset()
-{
- // reset resets the symbol table even when global declarations are true
- d_symtabAllocated.reset();
- d_implementation->reset();
-}
-
-void SymbolManager::resetAssertions()
-{
- d_implementation->resetAssertions();
- if (!d_globalDeclarations)
- {
- d_symtabAllocated.resetAssertions();
- }
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Mathias Preiner, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * The symbol manager.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__EXPR__SYMBOL_MANAGER_H
-#define CVC5__EXPR__SYMBOL_MANAGER_H
-
-#include <map>
-#include <memory>
-#include <string>
-
-#include "api/cpp/cvc5.h"
-#include "cvc5_export.h"
-#include "expr/symbol_table.h"
-
-namespace cvc5 {
-
-/** Represents the result of a call to `setExpressionName()`. */
-enum class NamingResult
-{
- /** The expression name was set successfully. */
- SUCCESS,
- /** The expression already has a name. */
- ERROR_ALREADY_NAMED,
- /** The expression is in a binder. */
- ERROR_IN_BINDER
-};
-
-/**
- * Symbol manager, which manages:
- * (1) The symbol table used by the parser,
- * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2.
- *
- * Like SymbolTable, this class currently lives in src/expr/ since it uses
- * context-dependent data structures.
- */
-class CVC5_EXPORT SymbolManager
-{
- public:
- SymbolManager(cvc5::Solver* s);
- ~SymbolManager();
- /** Get the underlying symbol table */
- internal::SymbolTable* getSymbolTable();
- //---------------------------- named expressions
- /** Set name of term t to name
- *
- * @param t The term to name
- * @param name The given name
- * @param isAssertion Whether t is being given a name in an assertion
- * context. In particular, this is true if and only if there was an assertion
- * command of the form (assert (! t :named name)).
- * @return true if the name was set. This method may return false if t
- * already has a name.
- */
- NamingResult setExpressionName(cvc5::Term t,
- const std::string& name,
- bool isAssertion = false);
- /** Get name for term t
- *
- * @param t The term
- * @param name The argument to update with the name of t
- * @param isAssertion Whether we only wish to get the assertion name of t
- * @return true if t has a name. If so, name is updated to that name.
- * Otherwise, name is unchanged.
- */
- bool getExpressionName(cvc5::Term t,
- std::string& name,
- bool isAssertion = false) const;
- /**
- * Convert list of terms to list of names. This adds to names the names of
- * all terms in ts that has names. Terms that do not have names are not
- * included.
- *
- * Notice that we do not distinguish what terms among those in ts have names.
- * If the caller of this method wants more fine-grained information about what
- * specific terms had names, then use the more fine grained interface above,
- * per term.
- *
- * @param ts The terms
- * @param names The name list
- * @param areAssertions Whether we only wish to include assertion names
- */
- void getExpressionNames(const std::vector<cvc5::Term>& ts,
- std::vector<std::string>& names,
- bool areAssertions = false) const;
- /**
- * Get a mapping of all expression names.
- *
- * @param areAssertions Whether we only wish to include assertion names
- * @return the mapping containing all expression names.
- */
- std::map<cvc5::Term, std::string> getExpressionNames(
- bool areAssertions = false) const;
- /**
- * @return The sorts we have declared that should be printed in the model.
- */
- std::vector<cvc5::Sort> getModelDeclareSorts() const;
- /**
- * @return The terms we have declared that should be printed in the model.
- */
- std::vector<cvc5::Term> getModelDeclareTerms() const;
- /**
- * @return The functions we have declared that should be printed in a response
- * to check-synth.
- */
- std::vector<cvc5::Term> getFunctionsToSynthesize() const;
- /**
- * Add declared sort to the list of model declarations.
- */
- void addModelDeclarationSort(cvc5::Sort s);
- /**
- * Add declared term to the list of model declarations.
- */
- void addModelDeclarationTerm(cvc5::Term t);
- /**
- * Add a function to synthesize. This ensures the solution for f is printed
- * in a successful response to check-synth.
- */
- void addFunctionToSynthesize(cvc5::Term f);
-
- //---------------------------- end named expressions
- /**
- * Get the scope level of the symbol table.
- */
- size_t scopeLevel() const;
- /**
- * Push a scope in the symbol table.
- *
- * @param isUserContext If true, this push is denoting a push of the user
- * context, e.g. via an smt2 push/pop command. Otherwise, this push is
- * due to a let/quantifier binding.
- */
- void pushScope(bool isUserContext);
- /**
- * Pop a scope in the symbol table.
- */
- void popScope();
- /**
- * 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. */
- bool getGlobalDeclarations() const;
- /**
- * Set the last abduct or interpolant to synthesize had the given name. This
- * is required since e.g. get-abduct-next must know the name of the
- * abduct-to-synthesize to print its result. For example, the sequence:
- * (get-abduct A <conjecture>)
- * (get-abduct-next)
- * The latter command must know the symbol "A".
- */
- void setLastSynthName(const std::string& name);
- /** Get the name of the last abduct or interpolant to synthesize */
- const std::string& getLastSynthName() const;
-
- private:
- /** The API Solver object. */
- cvc5::Solver* d_solver;
- /**
- * The declaration scope that is "owned" by this symbol manager.
- */
- internal::SymbolTable d_symtabAllocated;
- /** The implementation of the symbol manager */
- class Implementation;
- std::unique_ptr<Implementation> d_implementation;
- /**
- * Whether the global declarations option is enabled. This corresponds to the
- * SMT-LIB option :global-declarations. By default, its value is false.
- */
- bool d_globalDeclarations;
-};
-
-} // namespace cvc5
-
-#endif /* CVC5__EXPR__SYMBOL_MANAGER_H */
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Mathias Preiner, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Convenience class for scoping variable and type declarations
- * (implementation).
- */
-
-#include "expr/symbol_table.h"
-
-#include <ostream>
-#include <string>
-#include <unordered_map>
-#include <utility>
-
-#include "api/cpp/cvc5.h"
-#include "context/cdhashmap.h"
-#include "context/cdhashset.h"
-#include "context/context.h"
-
-namespace cvc5::internal {
-
-using context::CDHashMap;
-using context::CDHashSet;
-using context::Context;
-using std::copy;
-using std::endl;
-using std::ostream_iterator;
-using std::pair;
-using std::string;
-using std::vector;
-
-/** Overloaded type trie.
- *
- * This data structure stores a trie of expressions with
- * the same name, and must be distinguished by their argument types.
- * It is context-dependent.
- *
- * Using the argument allowFunVariants,
- * it may either be configured to allow function variants or not,
- * where a function variant is function that expects the same
- * argument types as another.
- *
- * For example, the following definitions introduce function
- * variants for the symbol f:
- *
- * 1. (declare-fun f (Int) Int) and
- * (declare-fun f (Int) Bool)
- *
- * 2. (declare-fun f (Int) Int) and
- * (declare-fun f (Int) Int)
- *
- * 3. (declare-datatypes ((Tup 0)) ((f (data Int)))) and
- * (declare-fun f (Int) Tup)
- *
- * 4. (declare-datatypes ((Tup 0)) ((mkTup (f Int)))) and
- * (declare-fun f (Tup) Bool)
- *
- * If function variants is set to true, we allow function variants
- * but not function redefinition. In examples 2 and 3, f is
- * declared twice as a symbol of identical argument and range
- * types. We never accept these definitions. However, we do
- * allow examples 1 and 4 above when allowFunVariants is true.
- *
- * For 0-argument functions (constants), we always allow
- * function variants. That is, we always accept these examples:
- *
- * 5. (declare-fun c () Int)
- * (declare-fun c () Bool)
- *
- * 6. (declare-datatypes ((Enum 0)) ((c)))
- * (declare-fun c () Int)
- *
- * and always reject constant redefinition such as:
- *
- * 7. (declare-fun c () Int)
- * (declare-fun c () Int)
- *
- * 8. (declare-datatypes ((Enum 0)) ((c))) and
- * (declare-fun c () Enum)
- */
-class OverloadedTypeTrie {
- public:
- OverloadedTypeTrie(Context* c, bool allowFunVariants = false)
- : d_overloaded_symbols(
- new (true) CDHashSet<cvc5::Term, std::hash<cvc5::Term>>(c)),
- d_allowFunctionVariants(allowFunVariants)
- {
- }
- ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); }
-
- /** is this function overloaded? */
- bool isOverloadedFunction(cvc5::Term fun) const;
-
- /** Get overloaded constant for type.
- * If possible, it returns a defined symbol with name
- * that has type t. Otherwise returns null expression.
- */
- cvc5::Term getOverloadedConstantForType(const std::string& name,
- cvc5::Sort t) const;
-
- /**
- * If possible, returns a defined function for a name
- * and a vector of expected argument types. Otherwise returns
- * null expression.
- */
- cvc5::Term getOverloadedFunctionForTypes(
- const std::string& name, const std::vector<cvc5::Sort>& argTypes) const;
- /** called when obj is bound to name, and prev_bound_obj was already bound to
- * name Returns false if the binding is invalid.
- */
- bool bind(const string& name, cvc5::Term prev_bound_obj, cvc5::Term obj);
-
- private:
- /** Marks expression obj with name as overloaded.
- * Adds relevant information to the type arg trie data structure.
- * It returns false if there is already an expression bound to that name
- * whose type expects the same arguments as the type of obj but is not
- * identical to the type of obj. For example, if we declare :
- *
- * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil))))
- * (declare-fun cons (Int List) List)
- *
- * cons : constructor_type( Int, List, List )
- * cons : function_type( Int, List, List )
- *
- * These are put in the same place in the trie but do not have identical type,
- * hence we return false.
- */
- bool markOverloaded(const string& name, cvc5::Term obj);
- /** the null expression */
- cvc5::Term d_nullTerm;
- // The (context-independent) trie storing that maps expected argument
- // vectors to symbols. All expressions stored in d_symbols are only
- // interpreted as active if they also appear in the context-dependent
- // set d_overloaded_symbols.
- class TypeArgTrie {
- public:
- // children of this node
- std::map<cvc5::Sort, TypeArgTrie> d_children;
- // symbols at this node
- std::map<cvc5::Sort, cvc5::Term> d_symbols;
- };
- /** for each string with operator overloading, this stores the data structure
- * above. */
- std::unordered_map<std::string, TypeArgTrie> d_overload_type_arg_trie;
- /** The set of overloaded symbols. */
- CDHashSet<cvc5::Term, std::hash<cvc5::Term>>* d_overloaded_symbols;
- /** allow function variants
- * This is true if we allow overloading (non-constant) functions that expect
- * the same argument types.
- */
- bool d_allowFunctionVariants;
- /** get unique overloaded function
- * If tat->d_symbols contains an active overloaded function, it
- * returns that function, where that function must be unique
- * if reqUnique=true.
- * Otherwise, it returns the null expression.
- */
- cvc5::Term getOverloadedFunctionAt(const TypeArgTrie* tat,
- bool reqUnique = true) const;
-};
-
-bool OverloadedTypeTrie::isOverloadedFunction(cvc5::Term fun) const
-{
- return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end();
-}
-
-cvc5::Term OverloadedTypeTrie::getOverloadedConstantForType(
- const std::string& name, cvc5::Sort t) const
-{
- std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
- d_overload_type_arg_trie.find(name);
- if (it != d_overload_type_arg_trie.end()) {
- std::map<cvc5::Sort, cvc5::Term>::const_iterator its =
- it->second.d_symbols.find(t);
- if (its != it->second.d_symbols.end()) {
- cvc5::Term expr = its->second;
- // must be an active symbol
- if (isOverloadedFunction(expr)) {
- return expr;
- }
- }
- }
- return d_nullTerm;
-}
-
-cvc5::Term OverloadedTypeTrie::getOverloadedFunctionForTypes(
- const std::string& name, const std::vector<cvc5::Sort>& argTypes) const
-{
- std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
- d_overload_type_arg_trie.find(name);
- if (it != d_overload_type_arg_trie.end()) {
- const TypeArgTrie* tat = &it->second;
- for (unsigned i = 0; i < argTypes.size(); i++) {
- std::map<cvc5::Sort, TypeArgTrie>::const_iterator itc =
- tat->d_children.find(argTypes[i]);
- if (itc != tat->d_children.end()) {
- tat = &itc->second;
- } else {
- Trace("parser-overloading")
- << "Could not find overloaded function " << name << std::endl;
-
- // no functions match
- return d_nullTerm;
- }
- }
- // we ensure that there is *only* one active symbol at this node
- return getOverloadedFunctionAt(tat);
- }
- return d_nullTerm;
-}
-
-bool OverloadedTypeTrie::bind(const string& name,
- cvc5::Term prev_bound_obj,
- cvc5::Term obj)
-{
- bool retprev = true;
- if (!isOverloadedFunction(prev_bound_obj)) {
- // mark previous as overloaded
- retprev = markOverloaded(name, prev_bound_obj);
- }
- // mark this as overloaded
- bool retobj = markOverloaded(name, obj);
- return retprev && retobj;
-}
-
-bool OverloadedTypeTrie::markOverloaded(const string& name, cvc5::Term obj)
-{
- Trace("parser-overloading") << "Overloaded function : " << name;
- Trace("parser-overloading") << " with type " << obj.getSort() << std::endl;
- // get the argument types
- cvc5::Sort t = obj.getSort();
- cvc5::Sort rangeType = t;
- std::vector<cvc5::Sort> argTypes;
- if (t.isFunction())
- {
- argTypes = t.getFunctionDomainSorts();
- rangeType = t.getFunctionCodomainSort();
- }
- else if (t.isDatatypeConstructor())
- {
- argTypes = t.getDatatypeConstructorDomainSorts();
- rangeType = t.getDatatypeConstructorCodomainSort();
- }
- else if (t.isDatatypeSelector())
- {
- argTypes.push_back(t.getDatatypeSelectorDomainSort());
- rangeType = t.getDatatypeSelectorCodomainSort();
- }
- // add to the trie
- TypeArgTrie* tat = &d_overload_type_arg_trie[name];
- for (unsigned i = 0; i < argTypes.size(); i++) {
- tat = &(tat->d_children[argTypes[i]]);
- }
-
- // check if function variants are allowed here
- if (d_allowFunctionVariants || argTypes.empty())
- {
- // they are allowed, check for redefinition
- std::map<cvc5::Sort, cvc5::Term>::iterator it =
- tat->d_symbols.find(rangeType);
- if (it != tat->d_symbols.end())
- {
- cvc5::Term prev_obj = it->second;
- // if there is already an active function with the same name and expects
- // the same argument types and has the same return type, we reject the
- // re-declaration here.
- if (isOverloadedFunction(prev_obj))
- {
- return false;
- }
- }
- }
- else
- {
- // they are not allowed, we cannot have any function defined here.
- cvc5::Term existingFun = getOverloadedFunctionAt(tat, false);
- if (!existingFun.isNull())
- {
- return false;
- }
- }
-
- // otherwise, update the symbols
- d_overloaded_symbols->insert(obj);
- tat->d_symbols[rangeType] = obj;
- return true;
-}
-
-cvc5::Term OverloadedTypeTrie::getOverloadedFunctionAt(
- const OverloadedTypeTrie::TypeArgTrie* tat, bool reqUnique) const
-{
- cvc5::Term retExpr;
- for (std::map<cvc5::Sort, cvc5::Term>::const_iterator its =
- tat->d_symbols.begin();
- its != tat->d_symbols.end();
- ++its)
- {
- cvc5::Term expr = its->second;
- if (isOverloadedFunction(expr))
- {
- if (retExpr.isNull())
- {
- if (!reqUnique)
- {
- return expr;
- }
- else
- {
- retExpr = expr;
- }
- }
- else
- {
- // multiple functions match
- return d_nullTerm;
- }
- }
- }
- return retExpr;
-}
-
-class SymbolTable::Implementation {
- public:
- Implementation()
- : d_context(),
- d_exprMap(&d_context),
- d_typeMap(&d_context),
- d_overload_trie(&d_context)
- {
- }
-
- ~Implementation() {}
-
- bool bind(const string& name, cvc5::Term obj, bool doOverload);
- void bindType(const string& name, cvc5::Sort t);
- void bindType(const string& name,
- const vector<cvc5::Sort>& params,
- cvc5::Sort t);
- bool isBound(const string& name) const;
- bool isBoundType(const string& name) const;
- cvc5::Term lookup(const string& name) const;
- cvc5::Sort lookupType(const string& name) const;
- cvc5::Sort lookupType(const string& name,
- const vector<cvc5::Sort>& params) const;
- size_t lookupArity(const string& name);
- void popScope();
- void pushScope();
- size_t getLevel() const;
- void reset();
- void resetAssertions();
- //------------------------ operator overloading
- /** implementation of function from header */
- bool isOverloadedFunction(cvc5::Term fun) const;
-
- /** implementation of function from header */
- cvc5::Term getOverloadedConstantForType(const std::string& name,
- cvc5::Sort t) const;
-
- /** implementation of function from header */
- cvc5::Term getOverloadedFunctionForTypes(
- const std::string& name, const std::vector<cvc5::Sort>& argTypes) const;
- //------------------------ end operator overloading
- private:
- /** The context manager for the scope maps. */
- Context d_context;
-
- /** A map for expressions. */
- CDHashMap<string, cvc5::Term> d_exprMap;
-
- /** A map for types. */
- using TypeMap = CDHashMap<string, std::pair<vector<cvc5::Sort>, cvc5::Sort>>;
- TypeMap d_typeMap;
-
- //------------------------ operator overloading
- // the null expression
- cvc5::Term d_nullTerm;
- // overloaded type trie, stores all information regarding overloading
- OverloadedTypeTrie d_overload_trie;
- /** bind with overloading
- * This is called whenever obj is bound to name where overloading symbols is
- * allowed. If a symbol is previously bound to that name, it marks both as
- * overloaded. Returns false if the binding was invalid.
- */
- bool bindWithOverloading(const string& name, cvc5::Term obj);
- //------------------------ end operator overloading
-}; /* SymbolTable::Implementation */
-
-bool SymbolTable::Implementation::bind(const string& name,
- cvc5::Term obj,
- bool doOverload)
-{
- PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null cvc5::Term");
- Trace("sym-table") << "SymbolTable: bind " << name
- << ", doOverload=" << doOverload << std::endl;
- if (doOverload) {
- if (!bindWithOverloading(name, obj)) {
- return false;
- }
- }
- d_exprMap.insert(name, obj);
-
- return true;
-}
-
-bool SymbolTable::Implementation::isBound(const string& name) const {
- return d_exprMap.find(name) != d_exprMap.end();
-}
-
-cvc5::Term SymbolTable::Implementation::lookup(const string& name) const
-{
- Assert(isBound(name));
- cvc5::Term expr = (*d_exprMap.find(name)).second;
- if (isOverloadedFunction(expr)) {
- return d_nullTerm;
- } else {
- return expr;
- }
-}
-
-void SymbolTable::Implementation::bindType(const string& name, cvc5::Sort t)
-{
- d_typeMap.insert(name, make_pair(vector<cvc5::Sort>(), t));
-}
-
-void SymbolTable::Implementation::bindType(const string& name,
- const vector<cvc5::Sort>& params,
- cvc5::Sort t)
-{
- if (TraceIsOn("sort")) {
- Trace("sort") << "bindType(" << name << ", [";
- if (params.size() > 0) {
- copy(params.begin(),
- params.end() - 1,
- ostream_iterator<cvc5::Sort>(Trace("sort"), ", "));
- Trace("sort") << params.back();
- }
- Trace("sort") << "], " << t << ")" << endl;
- }
-
- d_typeMap.insert(name, make_pair(params, t));
-}
-
-bool SymbolTable::Implementation::isBoundType(const string& name) const {
- return d_typeMap.find(name) != d_typeMap.end();
-}
-
-cvc5::Sort SymbolTable::Implementation::lookupType(const string& name) const
-{
- std::pair<std::vector<cvc5::Sort>, cvc5::Sort> p =
- (*d_typeMap.find(name)).second;
- PrettyCheckArgument(p.first.size() == 0, name,
- "type constructor arity is wrong: "
- "`%s' requires %u parameters but was provided 0",
- name.c_str(), p.first.size());
- return p.second;
-}
-
-cvc5::Sort SymbolTable::Implementation::lookupType(
- const string& name, const vector<cvc5::Sort>& params) const
-{
- std::pair<std::vector<cvc5::Sort>, cvc5::Sort> p =
- (*d_typeMap.find(name)).second;
- PrettyCheckArgument(p.first.size() == params.size(), params,
- "type constructor arity is wrong: "
- "`%s' requires %u parameters but was provided %u",
- name.c_str(), p.first.size(), params.size());
- if (p.first.size() == 0) {
- PrettyCheckArgument(p.second.isUninterpretedSort(), name.c_str());
- return p.second;
- }
- if (p.second.isDatatype())
- {
- PrettyCheckArgument(p.second.getDatatype().isParametric(),
- name,
- "expected parametric datatype");
- return p.second.instantiate(params);
- }
- bool isUninterpretedSortConstructor =
- p.second.isUninterpretedSortConstructor();
- if (TraceIsOn("sort"))
- {
- Trace("sort") << "instantiating using a sort "
- << (isUninterpretedSortConstructor ? "constructor"
- : "substitution")
- << std::endl;
- Trace("sort") << "have formals [";
- copy(p.first.begin(),
- p.first.end() - 1,
- ostream_iterator<cvc5::Sort>(Trace("sort"), ", "));
- Trace("sort") << p.first.back() << "]" << std::endl << "parameters [";
- copy(params.begin(),
- params.end() - 1,
- ostream_iterator<cvc5::Sort>(Trace("sort"), ", "));
- Trace("sort") << params.back() << "]" << endl
- << "type ctor " << name << std::endl
- << "type is " << p.second << std::endl;
- }
- cvc5::Sort instantiation = isUninterpretedSortConstructor
- ? p.second.instantiate(params)
- : p.second.substitute(p.first, params);
- Trace("sort") << "instance is " << instantiation << std::endl;
-
- return instantiation;
-}
-
-size_t SymbolTable::Implementation::lookupArity(const string& name) {
- std::pair<std::vector<cvc5::Sort>, cvc5::Sort> p =
- (*d_typeMap.find(name)).second;
- return p.first.size();
-}
-
-void SymbolTable::Implementation::popScope() {
- // should not pop beyond level one
- if (d_context.getLevel() == 0)
- {
- throw ScopeException();
- }
- d_context.pop();
-}
-
-void SymbolTable::Implementation::pushScope() { d_context.push(); }
-
-size_t SymbolTable::Implementation::getLevel() const {
- return d_context.getLevel();
-}
-
-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(cvc5::Term fun) const
-{
- return d_overload_trie.isOverloadedFunction(fun);
-}
-
-cvc5::Term SymbolTable::Implementation::getOverloadedConstantForType(
- const std::string& name, cvc5::Sort t) const
-{
- return d_overload_trie.getOverloadedConstantForType(name, t);
-}
-
-cvc5::Term SymbolTable::Implementation::getOverloadedFunctionForTypes(
- const std::string& name, const std::vector<cvc5::Sort>& argTypes) const
-{
- return d_overload_trie.getOverloadedFunctionForTypes(name, argTypes);
-}
-
-bool SymbolTable::Implementation::bindWithOverloading(const string& name,
- cvc5::Term obj)
-{
- CDHashMap<string, cvc5::Term>::const_iterator it = d_exprMap.find(name);
- if (it != d_exprMap.end())
- {
- const cvc5::Term& prev_bound_obj = (*it).second;
- if (prev_bound_obj != obj) {
- return d_overload_trie.bind(name, prev_bound_obj, obj);
- }
- }
- return true;
-}
-
-bool SymbolTable::isOverloadedFunction(cvc5::Term fun) const
-{
- return d_implementation->isOverloadedFunction(fun);
-}
-
-cvc5::Term SymbolTable::getOverloadedConstantForType(const std::string& name,
- cvc5::Sort t) const
-{
- return d_implementation->getOverloadedConstantForType(name, t);
-}
-
-cvc5::Term SymbolTable::getOverloadedFunctionForTypes(
- const std::string& name, const std::vector<cvc5::Sort>& argTypes) const
-{
- return d_implementation->getOverloadedFunctionForTypes(name, argTypes);
-}
-
-SymbolTable::SymbolTable() : d_implementation(new SymbolTable::Implementation())
-{
-}
-
-SymbolTable::~SymbolTable() {}
-bool SymbolTable::bind(const string& name, cvc5::Term obj, bool doOverload)
-{
- return d_implementation->bind(name, obj, doOverload);
-}
-
-void SymbolTable::bindType(const string& name, cvc5::Sort t)
-{
- d_implementation->bindType(name, t);
-}
-
-void SymbolTable::bindType(const string& name,
- const vector<cvc5::Sort>& params,
- cvc5::Sort t)
-{
- d_implementation->bindType(name, params, t);
-}
-
-bool SymbolTable::isBound(const string& name) const
-{
- return d_implementation->isBound(name);
-}
-bool SymbolTable::isBoundType(const string& name) const
-{
- return d_implementation->isBoundType(name);
-}
-cvc5::Term SymbolTable::lookup(const string& name) const
-{
- return d_implementation->lookup(name);
-}
-cvc5::Sort SymbolTable::lookupType(const string& name) const
-{
- return d_implementation->lookupType(name);
-}
-
-cvc5::Sort SymbolTable::lookupType(const string& name,
- const vector<cvc5::Sort>& params) const
-{
- return d_implementation->lookupType(name, params);
-}
-size_t SymbolTable::lookupArity(const string& name) {
- return d_implementation->lookupArity(name);
-}
-void SymbolTable::popScope() { d_implementation->popScope(); }
-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 cvc5::internal
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Morgan Deters, Christopher L. Conway
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved. See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Convenience class for scoping variable and type declarations.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__SYMBOL_TABLE_H
-#define CVC5__SYMBOL_TABLE_H
-
-#include <memory>
-#include <string>
-#include <vector>
-
-#include "base/exception.h"
-#include "cvc5_export.h"
-
-namespace cvc5 {
-class Solver;
-class Sort;
-class Term;
-} // namespace cvc5
-
-namespace cvc5::internal {
-
-class CVC5_EXPORT ScopeException : public Exception
-{
-};
-
-/**
- * A convenience class for handling scoped declarations. Implements the usual
- * nested scoping rules for declarations, with separate bindings for expressions
- * and types.
- */
-class CVC5_EXPORT SymbolTable
-{
- public:
- /** Create a symbol table. */
- SymbolTable();
- ~SymbolTable();
-
- /**
- * Bind an expression to a name in the current scope level.
- *
- * When doOverload is false:
- * if <code>name</code> is already bound to an expression in the current
- * level, then the binding is replaced. If <code>name</code> is bound
- * in a previous level, then the binding is "covered" by this one
- * until the current scope is popped.
- * If levelZero is true the name shouldn't be already bound.
- *
- * When doOverload is true:
- * if <code>name</code> is already bound to an expression in the current
- * level, then we mark the previous bound expression and obj as overloaded
- * functions.
- *
- * @param name an identifier
- * @param obj the expression to bind to <code>name</code>
- * @param doOverload set if the binding can overload the function name.
- *
- * Returns false if the binding was invalid.
- */
- bool bind(const std::string& name, cvc5::Term obj, bool doOverload = false);
-
- /**
- * Bind a type to a name in the current scope. If <code>name</code>
- * is already bound to a type in the current level, then the binding
- * is replaced. If <code>name</code> is bound in a previous level,
- * then the binding is "covered" by this one until the current scope
- * is popped.
- *
- * @param name an identifier
- * @param t the type to bind to <code>name</code>
- */
- void bindType(const std::string& name, cvc5::Sort t);
-
- /**
- * Bind a type to a name in the current scope. If <code>name</code>
- * is already bound to a type or type constructor in the current
- * level, then the binding is replaced. If <code>name</code> is
- * bound in a previous level, then the binding is "covered" by this
- * one until the current scope is popped.
- *
- * @param name an identifier
- * @param params the parameters to the type
- * @param t the type to bind to <code>name</code>
- */
- void bindType(const std::string& name,
- const std::vector<cvc5::Sort>& params,
- cvc5::Sort t);
-
- /**
- * Check whether a name is bound to an expression with bind().
- *
- * @param name the identifier to check.
- * @returns true iff name is bound in the current scope.
- */
- bool isBound(const std::string& name) const;
-
- /**
- * Check whether a name is bound to a type (or type constructor).
- *
- * @param name the identifier to check.
- * @returns true iff name is bound to a type in the current scope.
- */
- bool isBoundType(const std::string& name) const;
-
- /**
- * Lookup a bound expression.
- *
- * @param name the identifier to lookup
- * @returns the unique expression bound to <code>name</code> in the current
- * scope.
- * It returns the null expression if there is not a unique expression bound to
- * <code>name</code> in the current scope (i.e. if there is not exactly one).
- */
- cvc5::Term lookup(const std::string& name) const;
-
- /**
- * Lookup a bound type.
- *
- * @param name the type identifier to lookup
- * @returns the type bound to <code>name</code> in the current scope.
- */
- cvc5::Sort lookupType(const std::string& name) const;
-
- /**
- * Lookup a bound parameterized type.
- *
- * @param name the type-constructor identifier to lookup
- * @param params the types to use to parameterize the type
- * @returns the type bound to <code>name(<i>params</i>)</code> in
- * the current scope.
- */
- cvc5::Sort lookupType(const std::string& name,
- const std::vector<cvc5::Sort>& params) const;
-
- /**
- * Lookup the arity of a bound parameterized type.
- */
- size_t lookupArity(const std::string& name);
-
- /**
- * Pop a scope level, deletes all bindings since the last call to pushScope,
- * and decreases the level by 1.
- *
- * @throws ScopeException if the scope level is 0.
- */
- void popScope();
-
- /** Push a scope level and increase the scope level by 1. */
- void pushScope();
-
- /** Get the current level of this symbol table. */
- size_t getLevel() const;
-
- /** Reset everything. */
- void reset();
- /** Reset assertions. */
- void resetAssertions();
-
- //------------------------ operator overloading
- /** is this function overloaded? */
- bool isOverloadedFunction(cvc5::Term fun) const;
-
- /** Get overloaded constant for type.
- * If possible, it returns the defined symbol with name
- * that has type t. Otherwise returns null expression.
- */
- cvc5::Term getOverloadedConstantForType(const std::string& name,
- cvc5::Sort t) const;
-
- /**
- * If possible, returns the unique defined function for a name
- * that expects arguments with types "argTypes".
- * For example, if argTypes = (T1, ..., Tn), then this may return an
- * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn).
- *
- * If there is not a unique defined function for the name and argTypes,
- * this returns the null expression. This can happen either if there are
- * no functions with name and expected argTypes, or alternatively there is
- * more than one function with name and expected argTypes.
- */
- cvc5::Term getOverloadedFunctionForTypes(
- const std::string& name, const std::vector<cvc5::Sort>& argTypes) const;
- //------------------------ end operator overloading
-
- private:
- /** The implementation of the symbol table */
- class Implementation;
- std::unique_ptr<Implementation> d_implementation;
-}; /* class SymbolTable */
-
-} // namespace cvc5::internal
-
-#endif /* CVC5__SYMBOL_TABLE_H */
#include "smt/command.h"
#include "smt/solver_engine.h"
+using namespace cvc5::parser;
+
namespace cvc5::main {
// Function to cancel any (externally-imposed) limit on CPU time.
#include <string>
#include "api/cpp/cvc5.h"
-#include "expr/symbol_manager.h"
+#include "parser/api/cpp/symbol_manager.h"
namespace cvc5 {
* Certain commands (e.g. reset-assertions) have a specific impact on the
* symbol manager.
*/
- std::unique_ptr<SymbolManager> d_symman;
+ std::unique_ptr<parser::SymbolManager> d_symman;
cvc5::Result d_result;
cvc5::Solver* getSolver() { return d_solver.get(); }
/** Get a pointer to the symbol manager owned by this CommandExecutor */
- SymbolManager* getSymbolManager() { return d_symman.get(); }
+ parser::SymbolManager* getSymbolManager() { return d_symman.get(); }
cvc5::Result getResult() const { return d_result; }
void reset();
}; /* class CommandExecutor */
bool solverInvoke(cvc5::Solver* solver,
- SymbolManager* sm,
+ parser::SymbolManager* sm,
Command* cmd,
std::ostream& out);
#include "api/cpp/cvc5.h"
#include "base/check.h"
#include "base/output.h"
-#include "expr/symbol_manager.h"
+#include "parser/api/cpp/symbol_manager.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
class Solver;
-class SymbolManager;
-
namespace parser {
class Parser;
+ class SymbolManager;
} // namespace parser
class Command;
using CmdSeq = std::vector<std::unique_ptr<cvc5::Command>>;
InteractiveShell(Solver* solver,
- SymbolManager* sm,
+ cvc5::parser::SymbolManager* sm,
std::istream& in,
std::ostream& out);
/**
* Return the internal parser being used.
*/
- parser::Parser* getParser() { return d_parser.get(); }
+ cvc5::parser::Parser* getParser() { return d_parser.get(); }
private:
Solver* d_solver;
std::istream& d_in;
std::ostream& d_out;
- std::unique_ptr<parser::Parser> d_parser;
+ std::unique_ptr<cvc5::parser::Parser> d_parser;
bool d_quit;
bool d_usingEditline;
antlr_input_imports.cpp
antlr_line_buffered_input.cpp
antlr_line_buffered_input.h
+ api/cpp/symbol_manager.cpp
+ api/cpp/symbol_manager.h
bounded_token_buffer.cpp
bounded_token_buffer.h
bounded_token_factory.cpp
smt2/smt2_input.h
smt2/sygus_input.cpp
smt2/sygus_input.h
+ symbol_table.cpp
+ symbol_table.h
tptp/tptp.cpp
tptp/tptp.h
tptp/tptp_input.cpp
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Mathias Preiner, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The symbol manager.
+ */
+
+#include "parser/api/cpp/symbol_manager.h"
+
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "parser/symbol_table.h"
+
+using namespace cvc5::context;
+using namespace cvc5::internal::parser;
+
+namespace cvc5::parser {
+
+// ---------------------------------------------- SymbolManager::Implementation
+
+class SymbolManager::Implementation
+{
+ using TermStringMap =
+ CDHashMap<cvc5::Term, std::string, std::hash<cvc5::Term>>;
+ using TermSet = CDHashSet<cvc5::Term, std::hash<cvc5::Term>>;
+ using SortList = CDList<cvc5::Sort>;
+ using TermList = CDList<cvc5::Term>;
+
+ public:
+ Implementation()
+ : d_context(),
+ d_names(&d_context),
+ d_namedAsserts(&d_context),
+ d_declareSorts(&d_context),
+ d_declareTerms(&d_context),
+ d_funToSynth(&d_context),
+ d_hasPushedScope(&d_context, false),
+ d_lastSynthName(&d_context)
+ {
+ // use an outermost push, to be able to clear all definitions
+ d_context.push();
+ }
+
+ ~Implementation() { d_context.pop(); }
+ SymbolTable& getSymbolTable() { return d_symtabAllocated; }
+
+ /** set expression name */
+ NamingResult setExpressionName(cvc5::Term t,
+ const std::string& name,
+ bool isAssertion = false);
+ /** get expression name */
+ bool getExpressionName(cvc5::Term t,
+ std::string& name,
+ bool isAssertion = false) const;
+ /** get expression names */
+ void getExpressionNames(const std::vector<cvc5::Term>& ts,
+ std::vector<std::string>& names,
+ bool areAssertions = false) const;
+ /** get expression names */
+ std::map<cvc5::Term, std::string> getExpressionNames(
+ bool areAssertions) const;
+ /** get model declare sorts */
+ std::vector<cvc5::Sort> getModelDeclareSorts() const;
+ /** get model declare terms */
+ std::vector<cvc5::Term> getModelDeclareTerms() const;
+ /** get functions to synthesize */
+ std::vector<cvc5::Term> getFunctionsToSynthesize() const;
+ /** Add declared sort to the list of model declarations. */
+ void addModelDeclarationSort(cvc5::Sort s);
+ /** Add declared term to the list of model declarations. */
+ void addModelDeclarationTerm(cvc5::Term t);
+ /** Add function to the list of functions to synthesize. */
+ void addFunctionToSynthesize(cvc5::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;
+ /** Set the last abduct-to-synthesize had the given name. */
+ void setLastSynthName(const std::string& name);
+ /** Get the name of the last abduct-to-synthesize */
+ const std::string& getLastSynthName() const;
+
+ private:
+ /**
+ * The declaration scope that is "owned" by this symbol manager.
+ */
+ SymbolTable d_symtabAllocated;
+ /** The context manager for the scope maps. */
+ Context d_context;
+ /** Map terms to names */
+ TermStringMap d_names;
+ /** The set of terms with assertion names */
+ TermSet d_namedAsserts;
+ /** Declared sorts (for model printing) */
+ SortList d_declareSorts;
+ /** Declared terms (for model printing) */
+ TermList d_declareTerms;
+ /** Functions to synthesize (for response to check-synth) */
+ TermList d_funToSynth;
+ /**
+ * Have we pushed a scope (e.g. a let or quantifier) in the current context?
+ */
+ CDO<bool> d_hasPushedScope;
+ /** The last abduct or interpolant to synthesize name */
+ CDO<std::string> d_lastSynthName;
+};
+
+NamingResult SymbolManager::Implementation::setExpressionName(
+ cvc5::Term t, const std::string& name, bool isAssertion)
+{
+ Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> "
+ << name << ", isAssertion=" << isAssertion << std::endl;
+ if (d_hasPushedScope.get())
+ {
+ // cannot name subexpressions under binders
+ return NamingResult::ERROR_IN_BINDER;
+ }
+
+ if (isAssertion)
+ {
+ d_namedAsserts.insert(t);
+ }
+ if (d_names.find(t) != d_names.end())
+ {
+ // already named assertion
+ return NamingResult::ERROR_ALREADY_NAMED;
+ }
+ d_names[t] = name;
+ return NamingResult::SUCCESS;
+}
+
+bool SymbolManager::Implementation::getExpressionName(cvc5::Term t,
+ std::string& name,
+ bool isAssertion) const
+{
+ TermStringMap::const_iterator it = d_names.find(t);
+ if (it == d_names.end())
+ {
+ return false;
+ }
+ if (isAssertion)
+ {
+ // must be an assertion name
+ if (d_namedAsserts.find(t) == d_namedAsserts.end())
+ {
+ return false;
+ }
+ }
+ name = (*it).second;
+ return true;
+}
+
+void SymbolManager::Implementation::getExpressionNames(
+ const std::vector<cvc5::Term>& ts,
+ std::vector<std::string>& names,
+ bool areAssertions) const
+{
+ for (const cvc5::Term& t : ts)
+ {
+ std::string name;
+ if (getExpressionName(t, name, areAssertions))
+ {
+ names.push_back(name);
+ }
+ }
+}
+
+std::map<cvc5::Term, std::string>
+SymbolManager::Implementation::getExpressionNames(bool areAssertions) const
+{
+ std::map<cvc5::Term, std::string> emap;
+ for (TermStringMap::const_iterator it = d_names.begin(),
+ itend = d_names.end();
+ it != itend;
+ ++it)
+ {
+ cvc5::Term t = (*it).first;
+ if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end())
+ {
+ continue;
+ }
+ emap[t] = (*it).second;
+ }
+ return emap;
+}
+
+std::vector<cvc5::Sort> SymbolManager::Implementation::getModelDeclareSorts()
+ const
+{
+ std::vector<cvc5::Sort> declareSorts(d_declareSorts.begin(),
+ d_declareSorts.end());
+ return declareSorts;
+}
+
+std::vector<cvc5::Term> SymbolManager::Implementation::getModelDeclareTerms()
+ const
+{
+ std::vector<cvc5::Term> declareTerms(d_declareTerms.begin(),
+ d_declareTerms.end());
+ return declareTerms;
+}
+
+std::vector<cvc5::Term>
+SymbolManager::Implementation::getFunctionsToSynthesize() const
+{
+ return std::vector<cvc5::Term>(d_funToSynth.begin(), d_funToSynth.end());
+}
+
+void SymbolManager::Implementation::addModelDeclarationSort(cvc5::Sort s)
+{
+ Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s
+ << std::endl;
+ d_declareSorts.push_back(s);
+}
+
+void SymbolManager::Implementation::addModelDeclarationTerm(cvc5::Term t)
+{
+ Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t
+ << std::endl;
+ d_declareTerms.push_back(t);
+}
+
+void SymbolManager::Implementation::addFunctionToSynthesize(cvc5::Term f)
+{
+ Trace("sym-manager") << "SymbolManager: addFunctionToSynthesize " << f
+ << std::endl;
+ d_funToSynth.push_back(f);
+}
+
+void SymbolManager::Implementation::pushScope(bool isUserContext)
+{
+ 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();
+ if (!isUserContext)
+ {
+ d_hasPushedScope = true;
+ }
+ d_symtabAllocated.pushScope();
+}
+
+void SymbolManager::Implementation::popScope()
+{
+ Trace("sym-manager") << "SymbolManager: popScope" << std::endl;
+ d_symtabAllocated.popScope();
+ if (d_context.getLevel() == 0)
+ {
+ throw ScopeException();
+ }
+ d_context.pop();
+ Trace("sym-manager-debug")
+ << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
+}
+
+bool SymbolManager::Implementation::hasPushedScope() const
+{
+ return d_hasPushedScope.get();
+}
+
+void SymbolManager::Implementation::setLastSynthName(const std::string& name)
+{
+ d_lastSynthName = name;
+}
+
+const std::string& SymbolManager::Implementation::getLastSynthName() const
+{
+ return d_lastSynthName.get();
+}
+
+void SymbolManager::Implementation::reset()
+{
+ Trace("sym-manager") << "SymbolManager: reset" << std::endl;
+ // reset resets the symbol table even when global declarations are true
+ d_symtabAllocated.reset();
+ // 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
+
+SymbolManager::SymbolManager(cvc5::Solver* s)
+ : d_solver(s),
+ d_implementation(new SymbolManager::Implementation()),
+ d_globalDeclarations(false)
+{
+}
+
+SymbolManager::~SymbolManager() {}
+
+SymbolTable* SymbolManager::getSymbolTable()
+{
+ return &d_implementation->getSymbolTable();
+}
+
+bool SymbolManager::bind(const std::string& name,
+ cvc5::Term obj,
+ bool doOverload)
+{
+ return d_implementation->getSymbolTable().bind(name, obj, doOverload);
+}
+
+NamingResult SymbolManager::setExpressionName(cvc5::Term t,
+ const std::string& name,
+ bool isAssertion)
+{
+ return d_implementation->setExpressionName(t, name, isAssertion);
+}
+
+bool SymbolManager::getExpressionName(cvc5::Term t,
+ std::string& name,
+ bool isAssertion) const
+{
+ return d_implementation->getExpressionName(t, name, isAssertion);
+}
+
+void SymbolManager::getExpressionNames(const std::vector<cvc5::Term>& ts,
+ std::vector<std::string>& names,
+ bool areAssertions) const
+{
+ return d_implementation->getExpressionNames(ts, names, areAssertions);
+}
+
+std::map<cvc5::Term, std::string> SymbolManager::getExpressionNames(
+ bool areAssertions) const
+{
+ return d_implementation->getExpressionNames(areAssertions);
+}
+std::vector<cvc5::Sort> SymbolManager::getModelDeclareSorts() const
+{
+ return d_implementation->getModelDeclareSorts();
+}
+std::vector<cvc5::Term> SymbolManager::getModelDeclareTerms() const
+{
+ return d_implementation->getModelDeclareTerms();
+}
+
+std::vector<cvc5::Term> SymbolManager::getFunctionsToSynthesize() const
+{
+ return d_implementation->getFunctionsToSynthesize();
+}
+
+void SymbolManager::addModelDeclarationSort(cvc5::Sort s)
+{
+ d_implementation->addModelDeclarationSort(s);
+}
+
+void SymbolManager::addModelDeclarationTerm(cvc5::Term t)
+{
+ d_implementation->addModelDeclarationTerm(t);
+}
+
+void SymbolManager::addFunctionToSynthesize(cvc5::Term f)
+{
+ d_implementation->addFunctionToSynthesize(f);
+}
+
+size_t SymbolManager::scopeLevel() const
+{
+ return d_implementation->getSymbolTable().getLevel();
+}
+
+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);
+}
+
+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_implementation->popScope();
+}
+
+void SymbolManager::setGlobalDeclarations(bool flag)
+{
+ d_globalDeclarations = flag;
+}
+
+bool SymbolManager::getGlobalDeclarations() const
+{
+ return d_globalDeclarations;
+}
+
+void SymbolManager::setLastSynthName(const std::string& name)
+{
+ d_implementation->setLastSynthName(name);
+}
+
+const std::string& SymbolManager::getLastSynthName() const
+{
+ return d_implementation->getLastSynthName();
+}
+
+void SymbolManager::reset()
+{
+ d_implementation->reset();
+}
+
+void SymbolManager::resetAssertions()
+{
+ d_implementation->resetAssertions();
+ if (!d_globalDeclarations)
+ {
+ d_implementation->getSymbolTable().resetAssertions();
+ }
+}
+
+} // namespace cvc5::parser
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Mathias Preiner, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The symbol manager.
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__EXPR__SYMBOL_MANAGER_H
+#define CVC5__EXPR__SYMBOL_MANAGER_H
+
+#include <map>
+#include <memory>
+#include <string>
+
+#include "api/cpp/cvc5.h"
+#include "cvc5_export.h"
+
+namespace cvc5 {
+
+namespace internal::parser {
+class SymbolTable;
+}
+
+namespace parser {
+/** Represents the result of a call to `setExpressionName()`. */
+enum class NamingResult
+{
+ /** The expression name was set successfully. */
+ SUCCESS,
+ /** The expression already has a name. */
+ ERROR_ALREADY_NAMED,
+ /** The expression is in a binder. */
+ ERROR_IN_BINDER
+};
+
+/**
+ * Symbol manager, which manages:
+ * (1) The symbol table used by the parser,
+ * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2.
+ *
+ * Like SymbolTable, this class currently lives in src/expr/ since it uses
+ * context-dependent data structures.
+ */
+class CVC5_EXPORT SymbolManager
+{
+ public:
+ SymbolManager(cvc5::Solver* s);
+ ~SymbolManager();
+ /** Get the underlying symbol table */
+ internal::parser::SymbolTable* getSymbolTable();
+
+ /**
+ * Bind an expression to a name in the current scope level in the underlying
+ * symbol table.
+ *
+ * When doOverload is false:
+ * if <code>name</code> is already bound to an expression in the current
+ * level, then the binding is replaced. If <code>name</code> is bound
+ * in a previous level, then the binding is "covered" by this one
+ * until the current scope is popped.
+ * If levelZero is true the name shouldn't be already bound.
+ *
+ * When doOverload is true:
+ * if <code>name</code> is already bound to an expression in the current
+ * level, then we mark the previous bound expression and obj as overloaded
+ * functions.
+ *
+ * @param name an identifier
+ * @param obj the expression to bind to <code>name</code>
+ * @param doOverload set if the binding can overload the function name.
+ *
+ * Returns false if the binding was invalid.
+ */
+ bool bind(const std::string& name, cvc5::Term obj, bool doOverload = false);
+
+ //---------------------------- named expressions
+ /** Set name of term t to name
+ *
+ * @param t The term to name
+ * @param name The given name
+ * @param isAssertion Whether t is being given a name in an assertion
+ * context. In particular, this is true if and only if there was an assertion
+ * command of the form (assert (! t :named name)).
+ * @return true if the name was set. This method may return false if t
+ * already has a name.
+ */
+ NamingResult setExpressionName(cvc5::Term t,
+ const std::string& name,
+ bool isAssertion = false);
+ /** Get name for term t
+ *
+ * @param t The term
+ * @param name The argument to update with the name of t
+ * @param isAssertion Whether we only wish to get the assertion name of t
+ * @return true if t has a name. If so, name is updated to that name.
+ * Otherwise, name is unchanged.
+ */
+ bool getExpressionName(cvc5::Term t,
+ std::string& name,
+ bool isAssertion = false) const;
+ /**
+ * Convert list of terms to list of names. This adds to names the names of
+ * all terms in ts that has names. Terms that do not have names are not
+ * included.
+ *
+ * Notice that we do not distinguish what terms among those in ts have names.
+ * If the caller of this method wants more fine-grained information about what
+ * specific terms had names, then use the more fine grained interface above,
+ * per term.
+ *
+ * @param ts The terms
+ * @param names The name list
+ * @param areAssertions Whether we only wish to include assertion names
+ */
+ void getExpressionNames(const std::vector<cvc5::Term>& ts,
+ std::vector<std::string>& names,
+ bool areAssertions = false) const;
+ /**
+ * Get a mapping of all expression names.
+ *
+ * @param areAssertions Whether we only wish to include assertion names
+ * @return the mapping containing all expression names.
+ */
+ std::map<cvc5::Term, std::string> getExpressionNames(
+ bool areAssertions = false) const;
+ /**
+ * @return The sorts we have declared that should be printed in the model.
+ */
+ std::vector<cvc5::Sort> getModelDeclareSorts() const;
+ /**
+ * @return The terms we have declared that should be printed in the model.
+ */
+ std::vector<cvc5::Term> getModelDeclareTerms() const;
+ /**
+ * @return The functions we have declared that should be printed in a response
+ * to check-synth.
+ */
+ std::vector<cvc5::Term> getFunctionsToSynthesize() const;
+ /**
+ * Add declared sort to the list of model declarations.
+ */
+ void addModelDeclarationSort(cvc5::Sort s);
+ /**
+ * Add declared term to the list of model declarations.
+ */
+ void addModelDeclarationTerm(cvc5::Term t);
+ /**
+ * Add a function to synthesize. This ensures the solution for f is printed
+ * in a successful response to check-synth.
+ */
+ void addFunctionToSynthesize(cvc5::Term f);
+
+ //---------------------------- end named expressions
+ /**
+ * Get the scope level of the symbol table.
+ */
+ size_t scopeLevel() const;
+ /**
+ * Push a scope in the symbol table.
+ *
+ * @param isUserContext If true, this push is denoting a push of the user
+ * context, e.g. via an smt2 push/pop command. Otherwise, this push is
+ * due to a let/quantifier binding.
+ */
+ void pushScope(bool isUserContext);
+ /**
+ * Pop a scope in the symbol table.
+ */
+ void popScope();
+ /**
+ * 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. */
+ bool getGlobalDeclarations() const;
+ /**
+ * Set the last abduct or interpolant to synthesize had the given name. This
+ * is required since e.g. get-abduct-next must know the name of the
+ * abduct-to-synthesize to print its result. For example, the sequence:
+ * (get-abduct A <conjecture>)
+ * (get-abduct-next)
+ * The latter command must know the symbol "A".
+ */
+ void setLastSynthName(const std::string& name);
+ /** Get the name of the last abduct or interpolant to synthesize */
+ const std::string& getLastSynthName() const;
+
+ private:
+ /** The API Solver object. */
+ cvc5::Solver* d_solver;
+ /** The implementation of the symbol manager */
+ class Implementation;
+ std::unique_ptr<Implementation> d_implementation;
+ /**
+ * Whether the global declarations option is enabled. This corresponds to the
+ * SMT-LIB option :global-declarations. By default, its value is false.
+ */
+ bool d_globalDeclarations;
+};
+
+} // namespace parser
+} // namespace cvc5
+
+#endif /* CVC5__EXPR__SYMBOL_MANAGER_H */
#include "api/cpp/cvc5.h"
#include "cvc5_export.h"
-#include "expr/symbol_manager.h"
-#include "expr/symbol_table.h"
+#include "parser/api/cpp/symbol_manager.h"
#include "parser/input.h"
#include "parser/parse_op.h"
#include "parser/parser_exception.h"
+#include "symbol_table.h"
namespace cvc5 {
/**
* This current symbol table used by this parser, from symbol manager.
*/
- internal::SymbolTable* d_symtab;
+ internal::parser::SymbolTable* d_symtab;
/**
* The level of the assertions in the declaration scope. Things declared
class Solver;
class Options;
-class SymbolManager;
namespace parser {
class Parser;
+class SymbolManager;
/**
* A builder for input language parsers. <code>build()</code> can be
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Mathias Preiner, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Convenience class for scoping variable and type declarations
+ * (implementation).
+ */
+
+#include "parser/symbol_table.h"
+
+#include <ostream>
+#include <string>
+#include <unordered_map>
+#include <utility>
+
+#include "api/cpp/cvc5.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/context.h"
+
+namespace cvc5::internal::parser {
+
+using context::CDHashMap;
+using context::CDHashSet;
+using context::Context;
+using std::copy;
+using std::endl;
+using std::ostream_iterator;
+using std::pair;
+using std::string;
+using std::vector;
+
+/** Overloaded type trie.
+ *
+ * This data structure stores a trie of expressions with
+ * the same name, and must be distinguished by their argument types.
+ * It is context-dependent.
+ *
+ * Using the argument allowFunVariants,
+ * it may either be configured to allow function variants or not,
+ * where a function variant is function that expects the same
+ * argument types as another.
+ *
+ * For example, the following definitions introduce function
+ * variants for the symbol f:
+ *
+ * 1. (declare-fun f (Int) Int) and
+ * (declare-fun f (Int) Bool)
+ *
+ * 2. (declare-fun f (Int) Int) and
+ * (declare-fun f (Int) Int)
+ *
+ * 3. (declare-datatypes ((Tup 0)) ((f (data Int)))) and
+ * (declare-fun f (Int) Tup)
+ *
+ * 4. (declare-datatypes ((Tup 0)) ((mkTup (f Int)))) and
+ * (declare-fun f (Tup) Bool)
+ *
+ * If function variants is set to true, we allow function variants
+ * but not function redefinition. In examples 2 and 3, f is
+ * declared twice as a symbol of identical argument and range
+ * types. We never accept these definitions. However, we do
+ * allow examples 1 and 4 above when allowFunVariants is true.
+ *
+ * For 0-argument functions (constants), we always allow
+ * function variants. That is, we always accept these examples:
+ *
+ * 5. (declare-fun c () Int)
+ * (declare-fun c () Bool)
+ *
+ * 6. (declare-datatypes ((Enum 0)) ((c)))
+ * (declare-fun c () Int)
+ *
+ * and always reject constant redefinition such as:
+ *
+ * 7. (declare-fun c () Int)
+ * (declare-fun c () Int)
+ *
+ * 8. (declare-datatypes ((Enum 0)) ((c))) and
+ * (declare-fun c () Enum)
+ */
+class OverloadedTypeTrie
+{
+ public:
+ OverloadedTypeTrie(Context* c, bool allowFunVariants = false)
+ : d_overloaded_symbols(
+ new (true) CDHashSet<cvc5::Term, std::hash<cvc5::Term>>(c)),
+ d_allowFunctionVariants(allowFunVariants)
+ {
+ }
+ ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); }
+
+ /** is this function overloaded? */
+ bool isOverloadedFunction(cvc5::Term fun) const;
+
+ /** Get overloaded constant for type.
+ * If possible, it returns a defined symbol with name
+ * that has type t. Otherwise returns null expression.
+ */
+ cvc5::Term getOverloadedConstantForType(const std::string& name,
+ cvc5::Sort t) const;
+
+ /**
+ * If possible, returns a defined function for a name
+ * and a vector of expected argument types. Otherwise returns
+ * null expression.
+ */
+ cvc5::Term getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<cvc5::Sort>& argTypes) const;
+ /** called when obj is bound to name, and prev_bound_obj was already bound to
+ * name Returns false if the binding is invalid.
+ */
+ bool bind(const string& name, cvc5::Term prev_bound_obj, cvc5::Term obj);
+
+ private:
+ /** Marks expression obj with name as overloaded.
+ * Adds relevant information to the type arg trie data structure.
+ * It returns false if there is already an expression bound to that name
+ * whose type expects the same arguments as the type of obj but is not
+ * identical to the type of obj. For example, if we declare :
+ *
+ * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil))))
+ * (declare-fun cons (Int List) List)
+ *
+ * cons : constructor_type( Int, List, List )
+ * cons : function_type( Int, List, List )
+ *
+ * These are put in the same place in the trie but do not have identical type,
+ * hence we return false.
+ */
+ bool markOverloaded(const string& name, cvc5::Term obj);
+ /** the null expression */
+ cvc5::Term d_nullTerm;
+ // The (context-independent) trie storing that maps expected argument
+ // vectors to symbols. All expressions stored in d_symbols are only
+ // interpreted as active if they also appear in the context-dependent
+ // set d_overloaded_symbols.
+ class TypeArgTrie
+ {
+ public:
+ // children of this node
+ std::map<cvc5::Sort, TypeArgTrie> d_children;
+ // symbols at this node
+ std::map<cvc5::Sort, cvc5::Term> d_symbols;
+ };
+ /** for each string with operator overloading, this stores the data structure
+ * above. */
+ std::unordered_map<std::string, TypeArgTrie> d_overload_type_arg_trie;
+ /** The set of overloaded symbols. */
+ CDHashSet<cvc5::Term, std::hash<cvc5::Term>>* d_overloaded_symbols;
+ /** allow function variants
+ * This is true if we allow overloading (non-constant) functions that expect
+ * the same argument types.
+ */
+ bool d_allowFunctionVariants;
+ /** get unique overloaded function
+ * If tat->d_symbols contains an active overloaded function, it
+ * returns that function, where that function must be unique
+ * if reqUnique=true.
+ * Otherwise, it returns the null expression.
+ */
+ cvc5::Term getOverloadedFunctionAt(const TypeArgTrie* tat,
+ bool reqUnique = true) const;
+};
+
+bool OverloadedTypeTrie::isOverloadedFunction(cvc5::Term fun) const
+{
+ return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end();
+}
+
+cvc5::Term OverloadedTypeTrie::getOverloadedConstantForType(
+ const std::string& name, cvc5::Sort t) const
+{
+ std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
+ d_overload_type_arg_trie.find(name);
+ if (it != d_overload_type_arg_trie.end())
+ {
+ std::map<cvc5::Sort, cvc5::Term>::const_iterator its =
+ it->second.d_symbols.find(t);
+ if (its != it->second.d_symbols.end())
+ {
+ cvc5::Term expr = its->second;
+ // must be an active symbol
+ if (isOverloadedFunction(expr))
+ {
+ return expr;
+ }
+ }
+ }
+ return d_nullTerm;
+}
+
+cvc5::Term OverloadedTypeTrie::getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<cvc5::Sort>& argTypes) const
+{
+ std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
+ d_overload_type_arg_trie.find(name);
+ if (it != d_overload_type_arg_trie.end())
+ {
+ const TypeArgTrie* tat = &it->second;
+ for (unsigned i = 0; i < argTypes.size(); i++)
+ {
+ std::map<cvc5::Sort, TypeArgTrie>::const_iterator itc =
+ tat->d_children.find(argTypes[i]);
+ if (itc != tat->d_children.end())
+ {
+ tat = &itc->second;
+ }
+ else
+ {
+ Trace("parser-overloading")
+ << "Could not find overloaded function " << name << std::endl;
+
+ // no functions match
+ return d_nullTerm;
+ }
+ }
+ // we ensure that there is *only* one active symbol at this node
+ return getOverloadedFunctionAt(tat);
+ }
+ return d_nullTerm;
+}
+
+bool OverloadedTypeTrie::bind(const string& name,
+ cvc5::Term prev_bound_obj,
+ cvc5::Term obj)
+{
+ bool retprev = true;
+ if (!isOverloadedFunction(prev_bound_obj))
+ {
+ // mark previous as overloaded
+ retprev = markOverloaded(name, prev_bound_obj);
+ }
+ // mark this as overloaded
+ bool retobj = markOverloaded(name, obj);
+ return retprev && retobj;
+}
+
+bool OverloadedTypeTrie::markOverloaded(const string& name, cvc5::Term obj)
+{
+ Trace("parser-overloading") << "Overloaded function : " << name;
+ Trace("parser-overloading") << " with type " << obj.getSort() << std::endl;
+ // get the argument types
+ cvc5::Sort t = obj.getSort();
+ cvc5::Sort rangeType = t;
+ std::vector<cvc5::Sort> argTypes;
+ if (t.isFunction())
+ {
+ argTypes = t.getFunctionDomainSorts();
+ rangeType = t.getFunctionCodomainSort();
+ }
+ else if (t.isDatatypeConstructor())
+ {
+ argTypes = t.getDatatypeConstructorDomainSorts();
+ rangeType = t.getDatatypeConstructorCodomainSort();
+ }
+ else if (t.isDatatypeSelector())
+ {
+ argTypes.push_back(t.getDatatypeSelectorDomainSort());
+ rangeType = t.getDatatypeSelectorCodomainSort();
+ }
+ // add to the trie
+ TypeArgTrie* tat = &d_overload_type_arg_trie[name];
+ for (unsigned i = 0; i < argTypes.size(); i++)
+ {
+ tat = &(tat->d_children[argTypes[i]]);
+ }
+
+ // check if function variants are allowed here
+ if (d_allowFunctionVariants || argTypes.empty())
+ {
+ // they are allowed, check for redefinition
+ std::map<cvc5::Sort, cvc5::Term>::iterator it =
+ tat->d_symbols.find(rangeType);
+ if (it != tat->d_symbols.end())
+ {
+ cvc5::Term prev_obj = it->second;
+ // if there is already an active function with the same name and expects
+ // the same argument types and has the same return type, we reject the
+ // re-declaration here.
+ if (isOverloadedFunction(prev_obj))
+ {
+ return false;
+ }
+ }
+ }
+ else
+ {
+ // they are not allowed, we cannot have any function defined here.
+ cvc5::Term existingFun = getOverloadedFunctionAt(tat, false);
+ if (!existingFun.isNull())
+ {
+ return false;
+ }
+ }
+
+ // otherwise, update the symbols
+ d_overloaded_symbols->insert(obj);
+ tat->d_symbols[rangeType] = obj;
+ return true;
+}
+
+cvc5::Term OverloadedTypeTrie::getOverloadedFunctionAt(
+ const OverloadedTypeTrie::TypeArgTrie* tat, bool reqUnique) const
+{
+ cvc5::Term retExpr;
+ for (std::map<cvc5::Sort, cvc5::Term>::const_iterator its =
+ tat->d_symbols.begin();
+ its != tat->d_symbols.end();
+ ++its)
+ {
+ cvc5::Term expr = its->second;
+ if (isOverloadedFunction(expr))
+ {
+ if (retExpr.isNull())
+ {
+ if (!reqUnique)
+ {
+ return expr;
+ }
+ else
+ {
+ retExpr = expr;
+ }
+ }
+ else
+ {
+ // multiple functions match
+ return d_nullTerm;
+ }
+ }
+ }
+ return retExpr;
+}
+
+class SymbolTable::Implementation
+{
+ public:
+ Implementation()
+ : d_context(),
+ d_exprMap(&d_context),
+ d_typeMap(&d_context),
+ d_overload_trie(&d_context)
+ {
+ }
+
+ ~Implementation() {}
+
+ bool bind(const string& name, cvc5::Term obj, bool doOverload);
+ void bindType(const string& name, cvc5::Sort t);
+ void bindType(const string& name,
+ const vector<cvc5::Sort>& params,
+ cvc5::Sort t);
+ bool isBound(const string& name) const;
+ bool isBoundType(const string& name) const;
+ cvc5::Term lookup(const string& name) const;
+ cvc5::Sort lookupType(const string& name) const;
+ cvc5::Sort lookupType(const string& name,
+ const vector<cvc5::Sort>& params) const;
+ size_t lookupArity(const string& name);
+ void popScope();
+ void pushScope();
+ size_t getLevel() const;
+ void reset();
+ void resetAssertions();
+ //------------------------ operator overloading
+ /** implementation of function from header */
+ bool isOverloadedFunction(cvc5::Term fun) const;
+
+ /** implementation of function from header */
+ cvc5::Term getOverloadedConstantForType(const std::string& name,
+ cvc5::Sort t) const;
+
+ /** implementation of function from header */
+ cvc5::Term getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<cvc5::Sort>& argTypes) const;
+ //------------------------ end operator overloading
+ private:
+ /** The context manager for the scope maps. */
+ Context d_context;
+
+ /** A map for expressions. */
+ CDHashMap<string, cvc5::Term> d_exprMap;
+
+ /** A map for types. */
+ using TypeMap = CDHashMap<string, std::pair<vector<cvc5::Sort>, cvc5::Sort>>;
+ TypeMap d_typeMap;
+
+ //------------------------ operator overloading
+ // the null expression
+ cvc5::Term d_nullTerm;
+ // overloaded type trie, stores all information regarding overloading
+ OverloadedTypeTrie d_overload_trie;
+ /** bind with overloading
+ * This is called whenever obj is bound to name where overloading symbols is
+ * allowed. If a symbol is previously bound to that name, it marks both as
+ * overloaded. Returns false if the binding was invalid.
+ */
+ bool bindWithOverloading(const string& name, cvc5::Term obj);
+ //------------------------ end operator overloading
+}; /* SymbolTable::Implementation */
+
+bool SymbolTable::Implementation::bind(const string& name,
+ cvc5::Term obj,
+ bool doOverload)
+{
+ PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null cvc5::Term");
+ Trace("sym-table") << "SymbolTable: bind " << name
+ << ", doOverload=" << doOverload << std::endl;
+ if (doOverload)
+ {
+ if (!bindWithOverloading(name, obj))
+ {
+ return false;
+ }
+ }
+ d_exprMap.insert(name, obj);
+
+ return true;
+}
+
+bool SymbolTable::Implementation::isBound(const string& name) const
+{
+ return d_exprMap.find(name) != d_exprMap.end();
+}
+
+cvc5::Term SymbolTable::Implementation::lookup(const string& name) const
+{
+ Assert(isBound(name));
+ cvc5::Term expr = (*d_exprMap.find(name)).second;
+ if (isOverloadedFunction(expr))
+ {
+ return d_nullTerm;
+ }
+ else
+ {
+ return expr;
+ }
+}
+
+void SymbolTable::Implementation::bindType(const string& name, cvc5::Sort t)
+{
+ d_typeMap.insert(name, make_pair(vector<cvc5::Sort>(), t));
+}
+
+void SymbolTable::Implementation::bindType(const string& name,
+ const vector<cvc5::Sort>& params,
+ cvc5::Sort t)
+{
+ if (TraceIsOn("sort"))
+ {
+ Trace("sort") << "bindType(" << name << ", [";
+ if (params.size() > 0)
+ {
+ copy(params.begin(),
+ params.end() - 1,
+ ostream_iterator<cvc5::Sort>(Trace("sort"), ", "));
+ Trace("sort") << params.back();
+ }
+ Trace("sort") << "], " << t << ")" << endl;
+ }
+
+ d_typeMap.insert(name, make_pair(params, t));
+}
+
+bool SymbolTable::Implementation::isBoundType(const string& name) const
+{
+ return d_typeMap.find(name) != d_typeMap.end();
+}
+
+cvc5::Sort SymbolTable::Implementation::lookupType(const string& name) const
+{
+ std::pair<std::vector<cvc5::Sort>, cvc5::Sort> p =
+ (*d_typeMap.find(name)).second;
+ PrettyCheckArgument(p.first.size() == 0,
+ name,
+ "type constructor arity is wrong: "
+ "`%s' requires %u parameters but was provided 0",
+ name.c_str(),
+ p.first.size());
+ return p.second;
+}
+
+cvc5::Sort SymbolTable::Implementation::lookupType(
+ const string& name, const vector<cvc5::Sort>& params) const
+{
+ std::pair<std::vector<cvc5::Sort>, cvc5::Sort> p =
+ (*d_typeMap.find(name)).second;
+ PrettyCheckArgument(p.first.size() == params.size(),
+ params,
+ "type constructor arity is wrong: "
+ "`%s' requires %u parameters but was provided %u",
+ name.c_str(),
+ p.first.size(),
+ params.size());
+ if (p.first.size() == 0)
+ {
+ PrettyCheckArgument(p.second.isUninterpretedSort(), name.c_str());
+ return p.second;
+ }
+ if (p.second.isDatatype())
+ {
+ PrettyCheckArgument(p.second.getDatatype().isParametric(),
+ name,
+ "expected parametric datatype");
+ return p.second.instantiate(params);
+ }
+ bool isUninterpretedSortConstructor =
+ p.second.isUninterpretedSortConstructor();
+ if (TraceIsOn("sort"))
+ {
+ Trace("sort") << "instantiating using a sort "
+ << (isUninterpretedSortConstructor ? "constructor"
+ : "substitution")
+ << std::endl;
+ Trace("sort") << "have formals [";
+ copy(p.first.begin(),
+ p.first.end() - 1,
+ ostream_iterator<cvc5::Sort>(Trace("sort"), ", "));
+ Trace("sort") << p.first.back() << "]" << std::endl << "parameters [";
+ copy(params.begin(),
+ params.end() - 1,
+ ostream_iterator<cvc5::Sort>(Trace("sort"), ", "));
+ Trace("sort") << params.back() << "]" << endl
+ << "type ctor " << name << std::endl
+ << "type is " << p.second << std::endl;
+ }
+ cvc5::Sort instantiation = isUninterpretedSortConstructor
+ ? p.second.instantiate(params)
+ : p.second.substitute(p.first, params);
+ Trace("sort") << "instance is " << instantiation << std::endl;
+
+ return instantiation;
+}
+
+size_t SymbolTable::Implementation::lookupArity(const string& name)
+{
+ std::pair<std::vector<cvc5::Sort>, cvc5::Sort> p =
+ (*d_typeMap.find(name)).second;
+ return p.first.size();
+}
+
+void SymbolTable::Implementation::popScope()
+{
+ // should not pop beyond level one
+ if (d_context.getLevel() == 0)
+ {
+ throw ScopeException();
+ }
+ d_context.pop();
+}
+
+void SymbolTable::Implementation::pushScope() { d_context.push(); }
+
+size_t SymbolTable::Implementation::getLevel() const
+{
+ return d_context.getLevel();
+}
+
+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(cvc5::Term fun) const
+{
+ return d_overload_trie.isOverloadedFunction(fun);
+}
+
+cvc5::Term SymbolTable::Implementation::getOverloadedConstantForType(
+ const std::string& name, cvc5::Sort t) const
+{
+ return d_overload_trie.getOverloadedConstantForType(name, t);
+}
+
+cvc5::Term SymbolTable::Implementation::getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<cvc5::Sort>& argTypes) const
+{
+ return d_overload_trie.getOverloadedFunctionForTypes(name, argTypes);
+}
+
+bool SymbolTable::Implementation::bindWithOverloading(const string& name,
+ cvc5::Term obj)
+{
+ CDHashMap<string, cvc5::Term>::const_iterator it = d_exprMap.find(name);
+ if (it != d_exprMap.end())
+ {
+ const cvc5::Term& prev_bound_obj = (*it).second;
+ if (prev_bound_obj != obj)
+ {
+ return d_overload_trie.bind(name, prev_bound_obj, obj);
+ }
+ }
+ return true;
+}
+
+bool SymbolTable::isOverloadedFunction(cvc5::Term fun) const
+{
+ return d_implementation->isOverloadedFunction(fun);
+}
+
+cvc5::Term SymbolTable::getOverloadedConstantForType(const std::string& name,
+ cvc5::Sort t) const
+{
+ return d_implementation->getOverloadedConstantForType(name, t);
+}
+
+cvc5::Term SymbolTable::getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<cvc5::Sort>& argTypes) const
+{
+ return d_implementation->getOverloadedFunctionForTypes(name, argTypes);
+}
+
+SymbolTable::SymbolTable() : d_implementation(new SymbolTable::Implementation())
+{
+}
+
+SymbolTable::~SymbolTable() {}
+bool SymbolTable::bind(const string& name, cvc5::Term obj, bool doOverload)
+{
+ return d_implementation->bind(name, obj, doOverload);
+}
+
+void SymbolTable::bindType(const string& name, cvc5::Sort t)
+{
+ d_implementation->bindType(name, t);
+}
+
+void SymbolTable::bindType(const string& name,
+ const vector<cvc5::Sort>& params,
+ cvc5::Sort t)
+{
+ d_implementation->bindType(name, params, t);
+}
+
+bool SymbolTable::isBound(const string& name) const
+{
+ return d_implementation->isBound(name);
+}
+bool SymbolTable::isBoundType(const string& name) const
+{
+ return d_implementation->isBoundType(name);
+}
+cvc5::Term SymbolTable::lookup(const string& name) const
+{
+ return d_implementation->lookup(name);
+}
+cvc5::Sort SymbolTable::lookupType(const string& name) const
+{
+ return d_implementation->lookupType(name);
+}
+
+cvc5::Sort SymbolTable::lookupType(const string& name,
+ const vector<cvc5::Sort>& params) const
+{
+ return d_implementation->lookupType(name, params);
+}
+size_t SymbolTable::lookupArity(const string& name)
+{
+ return d_implementation->lookupArity(name);
+}
+void SymbolTable::popScope() { d_implementation->popScope(); }
+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 cvc5::internal::parser
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Morgan Deters, Christopher L. Conway
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Convenience class for scoping variable and type declarations.
+ */
+
+#include "cvc5parser_public.h"
+
+#ifndef CVC5__SYMBOL_TABLE_H
+#define CVC5__SYMBOL_TABLE_H
+
+#include <memory>
+#include <string>
+#include <vector>
+
+#include "base/exception.h"
+#include "cvc5_export.h"
+
+namespace cvc5 {
+class Solver;
+class Sort;
+class Term;
+} // namespace cvc5
+
+namespace cvc5::internal::parser {
+
+class CVC5_EXPORT ScopeException : public internal::Exception
+{
+};
+
+/**
+ * A convenience class for handling scoped declarations. Implements the usual
+ * nested scoping rules for declarations, with separate bindings for expressions
+ * and types.
+ */
+class CVC5_EXPORT SymbolTable
+{
+ public:
+ /** Create a symbol table. */
+ SymbolTable();
+ ~SymbolTable();
+
+ /**
+ * Bind an expression to a name in the current scope level.
+ *
+ * When doOverload is false:
+ * if <code>name</code> is already bound to an expression in the current
+ * level, then the binding is replaced. If <code>name</code> is bound
+ * in a previous level, then the binding is "covered" by this one
+ * until the current scope is popped.
+ * If levelZero is true the name shouldn't be already bound.
+ *
+ * When doOverload is true:
+ * if <code>name</code> is already bound to an expression in the current
+ * level, then we mark the previous bound expression and obj as overloaded
+ * functions.
+ *
+ * @param name an identifier
+ * @param obj the expression to bind to <code>name</code>
+ * @param doOverload set if the binding can overload the function name.
+ *
+ * Returns false if the binding was invalid.
+ */
+ bool bind(const std::string& name, cvc5::Term obj, bool doOverload = false);
+
+ /**
+ * Bind a type to a name in the current scope. If <code>name</code>
+ * is already bound to a type in the current level, then the binding
+ * is replaced. If <code>name</code> is bound in a previous level,
+ * then the binding is "covered" by this one until the current scope
+ * is popped.
+ *
+ * @param name an identifier
+ * @param t the type to bind to <code>name</code>
+ */
+ void bindType(const std::string& name, cvc5::Sort t);
+
+ /**
+ * Bind a type to a name in the current scope. If <code>name</code>
+ * is already bound to a type or type constructor in the current
+ * level, then the binding is replaced. If <code>name</code> is
+ * bound in a previous level, then the binding is "covered" by this
+ * one until the current scope is popped.
+ *
+ * @param name an identifier
+ * @param params the parameters to the type
+ * @param t the type to bind to <code>name</code>
+ */
+ void bindType(const std::string& name,
+ const std::vector<cvc5::Sort>& params,
+ cvc5::Sort t);
+
+ /**
+ * Check whether a name is bound to an expression with bind().
+ *
+ * @param name the identifier to check.
+ * @returns true iff name is bound in the current scope.
+ */
+ bool isBound(const std::string& name) const;
+
+ /**
+ * Check whether a name is bound to a type (or type constructor).
+ *
+ * @param name the identifier to check.
+ * @returns true iff name is bound to a type in the current scope.
+ */
+ bool isBoundType(const std::string& name) const;
+
+ /**
+ * Lookup a bound expression.
+ *
+ * @param name the identifier to lookup
+ * @returns the unique expression bound to <code>name</code> in the current
+ * scope.
+ * It returns the null expression if there is not a unique expression bound to
+ * <code>name</code> in the current scope (i.e. if there is not exactly one).
+ */
+ cvc5::Term lookup(const std::string& name) const;
+
+ /**
+ * Lookup a bound type.
+ *
+ * @param name the type identifier to lookup
+ * @returns the type bound to <code>name</code> in the current scope.
+ */
+ cvc5::Sort lookupType(const std::string& name) const;
+
+ /**
+ * Lookup a bound parameterized type.
+ *
+ * @param name the type-constructor identifier to lookup
+ * @param params the types to use to parameterize the type
+ * @returns the type bound to <code>name(<i>params</i>)</code> in
+ * the current scope.
+ */
+ cvc5::Sort lookupType(const std::string& name,
+ const std::vector<cvc5::Sort>& params) const;
+
+ /**
+ * Lookup the arity of a bound parameterized type.
+ */
+ size_t lookupArity(const std::string& name);
+
+ /**
+ * Pop a scope level, deletes all bindings since the last call to pushScope,
+ * and decreases the level by 1.
+ *
+ * @throws ScopeException if the scope level is 0.
+ */
+ void popScope();
+
+ /** Push a scope level and increase the scope level by 1. */
+ void pushScope();
+
+ /** Get the current level of this symbol table. */
+ size_t getLevel() const;
+
+ /** Reset everything. */
+ void reset();
+ /** Reset assertions. */
+ void resetAssertions();
+
+ //------------------------ operator overloading
+ /** is this function overloaded? */
+ bool isOverloadedFunction(cvc5::Term fun) const;
+
+ /** Get overloaded constant for type.
+ * If possible, it returns the defined symbol with name
+ * that has type t. Otherwise returns null expression.
+ */
+ cvc5::Term getOverloadedConstantForType(const std::string& name,
+ cvc5::Sort t) const;
+
+ /**
+ * If possible, returns the unique defined function for a name
+ * that expects arguments with types "argTypes".
+ * For example, if argTypes = (T1, ..., Tn), then this may return an
+ * expression with type function(T1, ..., Tn), or constructor(T1, ...., Tn).
+ *
+ * If there is not a unique defined function for the name and argTypes,
+ * this returns the null expression. This can happen either if there are
+ * no functions with name and expected argTypes, or alternatively there is
+ * more than one function with name and expected argTypes.
+ */
+ cvc5::Term getOverloadedFunctionForTypes(
+ const std::string& name, const std::vector<cvc5::Sort>& argTypes) const;
+ //------------------------ end operator overloading
+
+ private:
+ /** The implementation of the symbol table */
+ class Implementation;
+ std::unique_ptr<Implementation> d_implementation;
+}; /* class SymbolTable */
+
+} // namespace cvc5::internal::parser
+
+#endif /* CVC5__SYMBOL_TABLE_H */
#include "base/modal_exception.h"
#include "base/output.h"
#include "expr/node.h"
-#include "expr/symbol_manager.h"
#include "expr/type_node.h"
#include "options/io_utils.h"
#include "options/main_options.h"
#include "options/options.h"
#include "options/printer_options.h"
#include "options/smt_options.h"
+#include "parser/api/cpp/symbol_manager.h"
#include "printer/printer.h"
#include "proof/unsat_core.h"
#include "util/smt2_quote_string.h"
#include "util/utility.h"
using namespace std;
+using namespace cvc5::parser;
namespace cvc5 {
bool global = sm->getGlobalDeclarations();
cvc5::Term fun =
solver->defineFun(d_symbol, d_formals, d_sort, d_formula, global);
- sm->getSymbolTable()->bind(d_symbol, fun, global);
+ sm->bind(d_symbol, fun, global);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
class Solver;
class Term;
-class SymbolManager;
class Command;
class CommandStatus;
+namespace parser {
+class SymbolManager;
+}
+
namespace smt {
class Model;
}
/**
* Invoke the command on the solver and symbol manager sm.
*/
- virtual void invoke(cvc5::Solver* solver, SymbolManager* sm) = 0;
+ virtual void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) = 0;
/**
* Same as above, and prints the result to output stream out.
*/
virtual void invoke(cvc5::Solver* solver,
- SymbolManager* sm,
+ parser::SymbolManager* sm,
std::ostream& out);
virtual void toStream(std::ostream& out) const = 0;
public:
EmptyCommand(std::string name = "");
std::string getName() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
std::string getOutput() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void invoke(cvc5::Solver* solver,
- SymbolManager* sm,
+ parser::SymbolManager* sm,
std::ostream& out) override;
std::string getCommandName() const override;
cvc5::Term getTerm() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
public:
PushCommand(uint32_t nscopes);
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
public:
PopCommand(uint32_t nscopes);
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
public:
DeclarationDefinitionCommand(const std::string& id);
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override = 0;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override = 0;
std::string getSymbol() const;
}; /* class DeclarationDefinitionCommand */
cvc5::Term getFunction() const;
cvc5::Sort getSort() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class DeclareFunctionCommand */
cvc5::Sort getSort() const;
const std::vector<cvc5::Term>& getInitialValue() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class DeclarePoolCommand */
Sort getSort() const;
const std::string& getBinaryName() const;
- void invoke(Solver* solver, SymbolManager* sm) override;
+ void invoke(Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
size_t getArity() const;
cvc5::Sort getSort() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class DeclareSortCommand */
const std::vector<cvc5::Sort>& getParameters() const;
cvc5::Sort getSort() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class DefineSortCommand */
cvc5::Sort getSort() const;
cvc5::Term getFormula() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
const std::vector<std::vector<cvc5::Term> >& getFormals() const;
const std::vector<cvc5::Term>& getFormulas() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
DeclareHeapCommand(cvc5::Sort locSort, cvc5::Sort dataSort);
cvc5::Sort getLocationSort() const;
cvc5::Sort getDataSort() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
public:
CheckSatCommand();
cvc5::Result getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
const std::vector<cvc5::Term>& getTerms() const;
cvc5::Result getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
* The declared sygus variable is communicated to the SMT engine in case a
* synthesis conjecture is built later on.
*/
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
* The declared function-to-synthesize is communicated to the SMT engine in
* case a synthesis conjecture is built later on.
*/
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
* The declared constraint is communicated to the SMT engine in case a
* synthesis conjecture is built later on.
*/
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
* invariant constraint is built, in case an actual synthesis conjecture is
* built later on.
*/
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
* and then perform a satisfiability check, whose result is stored in
* d_result.
*/
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
cvc5::Term getTerm() const;
cvc5::Term getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
const std::vector<cvc5::Term>& getTerms() const;
cvc5::Term getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
GetAssignmentCommand();
cvc5::Term getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
{
public:
GetModelCommand();
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
public:
BlockModelCommand(modes::BlockModelsMode mode);
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
BlockModelValuesCommand(const std::vector<cvc5::Term>& terms);
const std::vector<cvc5::Term>& getTerms() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
public:
GetProofCommand();
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
GetInstantiationsCommand();
static bool isEnabled(cvc5::Solver* solver, const cvc5::Result& res);
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
* query. */
cvc5::Term getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
*/
cvc5::Term getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
*/
cvc5::Term getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
*/
cvc5::Term getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
cvc5::Term getTerm() const;
bool getDoFull() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
cvc5::Term getResult() const;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
{
public:
GetUnsatAssumptionsCommand();
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::vector<cvc5::Term> getResult() const;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
GetUnsatCoreCommand();
const std::vector<cvc5::Term>& getUnsatCore() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
/** The solver we were invoked with */
cvc5::Solver* d_solver;
/** The symbol manager we were invoked with */
- SymbolManager* d_sm;
+ parser::SymbolManager* d_sm;
/** the result of the unsat core call */
std::vector<cvc5::Term> d_result;
}; /* class GetUnsatCoreCommand */
GetDifficultyCommand();
const std::map<cvc5::Term, cvc5::Term>& getDifficultyMap() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
protected:
/** The symbol manager we were invoked with */
- SymbolManager* d_sm;
+ parser::SymbolManager* d_sm;
/** the result of the get difficulty call */
std::map<cvc5::Term, cvc5::Term> d_result;
};
GetLearnedLiteralsCommand();
const std::vector<cvc5::Term>& getLearnedLiterals() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
public:
GetAssertionsCommand();
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getResult() const;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
SetBenchmarkLogicCommand(std::string logic);
std::string getLogic() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class SetBenchmarkLogicCommand */
const std::string& getFlag() const;
const std::string& getValue() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class SetInfoCommand */
std::string getFlag() const;
std::string getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
const std::string& getFlag() const;
const std::string& getValue() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class SetOptionCommand */
std::string getFlag() const;
std::string getResult() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
void printResult(cvc5::Solver* solver, std::ostream& out) const override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
DatatypeDeclarationCommand(const std::vector<cvc5::Sort>& datatypes);
const std::vector<cvc5::Sort>& getDatatypes() const;
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class DatatypeDeclarationCommand */
{
public:
ResetCommand() {}
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class ResetCommand */
{
public:
ResetAssertionsCommand() {}
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class ResetAssertionsCommand */
{
public:
QuitCommand() {}
- void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
+ void invoke(cvc5::Solver* solver, parser::SymbolManager* sm) override;
std::string getCommandName() const override;
void toStream(std::ostream& out) const override;
}; /* class QuitCommand */
#include <vector>
#include "api/cpp/cvc5.h"
-#include "expr/symbol_manager.h"
#include "main/interactive_shell.h"
#include "options/base_options.h"
#include "options/language.h"
#include "options/options.h"
+#include "parser/api/cpp/symbol_manager.h"
#include "parser/parser_builder.h"
#include "smt/command.h"
#include "test.h"
+using namespace cvc5::parser;
+using namespace cvc5::internal::parser;
+
namespace cvc5::internal {
namespace test {
#include "base/exception.h"
#include "context/context.h"
#include "expr/kind.h"
-#include "expr/symbol_table.h"
+#include "parser/symbol_table.h"
#include "test_api.h"
namespace cvc5::internal {
using namespace kind;
using namespace context;
+using namespace parser;
namespace test {
#include "api/cpp/cvc5.h"
#include "base/output.h"
-#include "expr/symbol_manager.h"
#include "options/base_options.h"
#include "options/language.h"
#include "options/options.h"
+#include "parser/api/cpp/symbol_manager.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/smt2/smt2.h"
#include "smt/command.h"
#include "test.h"
-namespace cvc5::internal {
-
-using namespace parser;
+using namespace cvc5::parser;
+using namespace cvc5::internal::parser;
+namespace cvc5::internal {
namespace test {
class TestParserBlackParser : public TestInternal
#include <iostream>
#include "api/cpp/cvc5.h"
-#include "expr/symbol_manager.h"
#include "options/language.h"
+#include "parser/api/cpp/symbol_manager.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/command.h"
#include "test_api.h"
-namespace cvc5::internal {
-
-using namespace parser;
+using namespace cvc5::parser;
+namespace cvc5::internal {
namespace test {
class TestParseBlackParserBuilder : public TestApi
projects / cvc5.git / commitdiff