diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/proof/skolemization_manager.cpp | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/proof/skolemization_manager.cpp')
-rw-r--r-- | src/proof/skolemization_manager.cpp | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp new file mode 100644 index 000000000..12fea82ad --- /dev/null +++ b/src/proof/skolemization_manager.cpp @@ -0,0 +1,68 @@ +/********************* */ +/*! \file skolemization_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Guy Katz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 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 + ** + ** [[ Add lengthier description here ]] + + ** \todo document this file + + **/ + +#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 */ |