src/proof/skolemization_manager.h

   1 /*********************                                                        */
   2 /*! \file skolemization_manager.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Guy Katz, 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 "cvc4_private.h"
  19
  20 #ifndef CVC4__SKOLEMIZATION_MANAGER_H
  21 #define CVC4__SKOLEMIZATION_MANAGER_H
  22
  23 #include <iostream>
  24 #include <unordered_map>
  25
  26 #include "proof/proof.h"
  27 #include "util/proof.h"
  28 #include "expr/node.h"
  29 #include "theory/logic_info.h"
  30 #include "theory/substitutions.h"
  31
  32 namespace CVC4 {
  33
  34 class SkolemizationManager {
  35 public:
  36   void registerSkolem(Node disequality, Node skolem);
  37   bool hasSkolem(Node disequality);
  38   Node getSkolem(Node disequality);
  39   Node getDisequality(Node skolem);
  40   bool isSkolem(Node skolem);
  41   void clear();
  42
  43   std::unordered_map<Node, Node, NodeHashFunction>::const_iterator begin();
  44   std::unordered_map<Node, Node, NodeHashFunction>::const_iterator end();
  45
  46 private:
  47   std::unordered_map<Node, Node, NodeHashFunction> d_disequalityToSkolem;
  48   std::unordered_map<Node, Node, NodeHashFunction> d_skolemToDisequality;
  49 };
  50
  51 }/* CVC4 namespace */
  52
  53
  54
  55 #endif /* CVC4__SKOLEMIZATION_MANAGER_H */