src/util/ite_removal.h

   1 /*********************                                                        */
   2 /*! \file ite_removal.h
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters
   6  ** Minor contributors (to current version): Clark Barrett
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Removal of term ITEs
  13  **
  14  ** Removal of term ITEs.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #pragma once
  20
  21 #include <vector>
  22 #include "expr/node.h"
  23 #include "util/dump.h"
  24 #include "context/context.h"
  25 #include "context/cdinsert_hashmap.h"
  26 #include "util/hash.h"
  27 #include "util/bool.h"
  28
  29 namespace CVC4 {
  30
  31 namespace theory {
  32   class ContainsTermITEVisitor;
  33 }/* CVC4::theory namespace */
  34
  35 typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
  36
  37 class RemoveITE {
  38   typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache;
  39   ITECache d_iteCache;
  40
  41
  42 public:
  43
  44   RemoveITE(context::UserContext* u);
  45   ~RemoveITE();
  46
  47   /**
  48    * Removes the ITE nodes by introducing skolem variables. All
  49    * additional assertions are pushed into assertions. iteSkolemMap
  50    * contains a map from introduced skolem variables to the index in
  51    * assertions containing the new Boolean ite created in conjunction
  52    * with that skolem variable.
  53    *
  54    * With reportDeps true, report reasoning dependences to the proof
  55    * manager (for unsat cores).
  56    */
  57   void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
  58
  59   /**
  60    * Removes the ITE from the node by introducing skolem
  61    * variables. All additional assertions are pushed into
  62    * assertions. iteSkolemMap contains a map from introduced skolem
  63    * variables to the index in assertions containing the new Boolean
  64    * ite created in conjunction with that skolem variable.
  65    */
  66   Node run(TNode node, std::vector<Node>& additionalAssertions,
  67            IteSkolemMap& iteSkolemMap, bool inQuant);
  68
  69   /**
  70    * Substitute under node using pre-existing cache.  Do not remove
  71    * any ITEs not seen during previous runs.
  72    */
  73   Node replace(TNode node, bool inQuant = false) const;
  74
  75   /** Returns true if e contains a term ite. */
  76   bool containsTermITE(TNode e) const;
  77
  78   /** Returns the collected size of the caches. */
  79   size_t collectedCacheSizes() const;
  80
  81   /** Garbage collects non-context dependent data-structures. */
  82   void garbageCollect();
  83
  84   /** Return the RemoveITE's containsVisitor. */
  85   theory::ContainsTermITEVisitor* getContainsVisitor();
  86
  87 private:
  88   theory::ContainsTermITEVisitor* d_containsVisitor;
  89
  90 };/* class RemoveTTE */
  91
  92 }/* CVC4 namespace */