diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-09-22 16:59:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-22 16:59:41 -0500 |
commit | e4a29a6033ecc7ba5ec266f37e8f151f09ead020 (patch) | |
tree | 26dff55bd5121dc311185dcd3071a6e8751f9f5e /src/theory/bags/term_registry.h | |
parent | 524c879720779abc3bc529459da8734f2eb3e3ad (diff) |
Add skeleton for theory of bags (multisets) (#5100)
This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.
Diffstat (limited to 'src/theory/bags/term_registry.h')
-rw-r--r-- | src/theory/bags/term_registry.h | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h new file mode 100644 index 000000000..d284126ee --- /dev/null +++ b/src/theory/bags/term_registry.h @@ -0,0 +1,63 @@ +/********************* */ +/*! \file term_registry.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Bags state object + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAGS__TERM_REGISTRY_H +#define CVC4__THEORY__BAGS__TERM_REGISTRY_H + +#include <map> +#include <vector> + +#include "context/cdhashmap.h" +#include "theory/bags/inference_manager.h" +#include "theory/bags/solver_state.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +/** + * Term registry, the purpose of this class is to maintain a database of + * commonly used terms, and mappings from bags to their "proxy variables". + */ +class TermRegistry +{ + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; + + public: + TermRegistry(SolverState& state, InferenceManager& im); + + /** + * Returns the existing empty bag for type tn + * or creates a new one and returns it. + **/ + Node getEmptyBag(TypeNode tn); + + private: + /** The inference manager */ + InferenceManager& d_im; + /** Map from bag terms to their proxy variables */ + NodeMap d_proxy; + /** Backwards map of above */ + NodeMap d_proxy_to_term; + /** Map from types to empty bag of that type */ + std::map<TypeNode, Node> d_emptybag; +}; /* class Term */ + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */ |