src/proof/skolemization_manager.cpp

   1 /*********************                                                        */
   2 /*! \file skolemization_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Paul Meng, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** [[ Add lengthier description here ]]
  13
  14  ** \todo document this file
  15
  16  **/
  17
  18 #include "proof/skolemization_manager.h"
  19
  20 namespace CVC4 {
  21
  22 void SkolemizationManager::registerSkolem(Node disequality, Node skolem) {
  23   Debug("pf::pm") << "SkolemizationManager: registerSkolem: disequality = " << disequality << ", skolem = " << skolem << std::endl;
  24
  25   if (isSkolem(skolem)) {
  26     Assert(d_skolemToDisequality[skolem] == disequality);
  27     return;
  28   }
  29
  30   d_disequalityToSkolem[disequality] = skolem;
  31   d_skolemToDisequality[skolem] = disequality;
  32 }
  33
  34 bool SkolemizationManager::hasSkolem(Node disequality) {
  35   return (d_disequalityToSkolem.find(disequality) != d_disequalityToSkolem.end());
  36 }
  37
  38 Node SkolemizationManager::getSkolem(Node disequality) {
  39   Debug("pf::pm") << "SkolemizationManager: getSkolem( ";
  40   Assert(d_disequalityToSkolem.find(disequality)
  41          != d_disequalityToSkolem.end());
  42   Debug("pf::pm") << disequality << " ) = " << d_disequalityToSkolem[disequality] << std::endl;
  43   return d_disequalityToSkolem[disequality];
  44 }
  45
  46 Node SkolemizationManager::getDisequality(Node skolem) {
  47   Assert(d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end());
  48   return d_skolemToDisequality[skolem];
  49 }
  50
  51 bool SkolemizationManager::isSkolem(Node skolem) {
  52   return (d_skolemToDisequality.find(skolem) != d_skolemToDisequality.end());
  53 }
  54
  55 void SkolemizationManager::clear() {
  56   Debug("pf::pm") << "SkolemizationManager: clear" << std::endl;
  57   d_disequalityToSkolem.clear();
  58   d_skolemToDisequality.clear();
  59 }
  60
  61 std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::begin() {
  62   return d_disequalityToSkolem.begin();
  63 }
  64
  65 std::unordered_map<Node, Node, NodeHashFunction>::const_iterator SkolemizationManager::end() {
  66   return d_disequalityToSkolem.end();
  67 }
  68
  69 } /* CVC4  namespace */