diff options
Diffstat (limited to 'src/proof/skolemization_manager.cpp')
-rw-r--r-- | src/proof/skolemization_manager.cpp | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp new file mode 100644 index 000000000..526ea8dbb --- /dev/null +++ b/src/proof/skolemization_manager.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \file skolemization_manager.cpp + **/ + +#include "proof/skolemization_manager.h" + +namespace CVC4 { + +void SkolemizationManager::registerSkolem(Node disequality, Node skolem) { + Debug("pf::pm") << "SkolemizationManager: registerSkolem: disequality = " << disequality << ", skolem = " << skolem << std::endl; + + if (isSkolem(skolem)) { + Assert(d_skolemToDisequality[skolem] == disequality); + return; + } + + d_disequalityToSkolem[disequality] = skolem; + d_skolemToDisequality[skolem] = disequality; +} + +bool SkolemizationManager::hasSkolem(Node disequality) { + return (d_disequalityToSkolem.find(disequality) != d_disequalityToSkolem.end()); +} + +Node SkolemizationManager::getSkolem(Node disequality) { + Debug("pf::pm") << "SkolemizationManager: getSkolem( "; + Assert (d_disequalityToSkolem.find(disequality) != d_disequalityToSkolem.end()); + Debug("pf::pm") << disequality << " ) = " << d_disequalityToSkolem[disequality] << std::endl; + return d_disequalityToSkolem[disequality]; +} + +Node SkolemizationManager::getDisequality(Node skolem) { + Assert (d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end()); + return d_skolemToDisequality[skolem]; +} + +bool SkolemizationManager::isSkolem(Node skolem) { + return (d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end()); +} + +void SkolemizationManager::clear() { + Debug("pf::pm") << "SkolemizationManager: clear" << std::endl; + d_disequalityToSkolem.clear(); + d_skolemToDisequality.clear(); +} + +std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() { + return d_disequalityToSkolem.begin(); +} + +std::hash_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() { + return d_disequalityToSkolem.end(); +} + +} /* CVC4 namespace */ |