src/smt/abstract_values.h

   1 /*********************                                                        */
   2 /*! \file abstract_values.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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  ** \brief Utility for constructing and maintaining abstract values.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__SMT__ABSTRACT_VALUES_H
  18 #define CVC4__SMT__ABSTRACT_VALUES_H
  19
  20 #include <unordered_map>
  21
  22 #include "context/context.h"
  23 #include "expr/node.h"
  24 #include "theory/substitutions.h"
  25
  26 namespace CVC4 {
  27 namespace smt {
  28
  29 /**
  30  * This utility is responsible for constructing and maintaining abstract
  31  * values, which are used in some responses to e.g. get-value / get-model
  32  * commands. See SMT-LIB standard 2.6 page 65 for details.
  33  */
  34 class AbstractValues
  35 {
  36   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
  37  public:
  38   AbstractValues(NodeManager* nm);
  39   ~AbstractValues();
  40   /**
  41    * Substitute away all AbstractValues in a node, which replaces all
  42    * abstract values with their original definition. For example, if `@a` was
  43    * introduced for term t, then applying this method on f(`@a`) returns f(t).
  44    */
  45   Node substituteAbstractValues(TNode n);
  46
  47   /**
  48    * Make a new (or return an existing) abstract value for a node.
  49    * Can only use this if options::abstractValues() is on.
  50    */
  51   Node mkAbstractValue(TNode n);
  52
  53  private:
  54   /** Pointer to the used node manager */
  55   NodeManager* d_nm;
  56   /**
  57    * A context that never pushes/pops, for use by CD structures (like
  58    * SubstitutionMaps) that should be "global".
  59    */
  60   context::Context d_fakeContext;
  61
  62   /**
  63    * A map of AbsractValues to their actual constants.  Only used if
  64    * options::abstractValues() is on.
  65    */
  66   theory::SubstitutionMap d_abstractValueMap;
  67
  68   /**
  69    * A mapping of all abstract values (actual value |-> abstract) that
  70    * we've handed out.  This is necessary to ensure that we give the
  71    * same AbstractValues for the same real constants.  Only used if
  72    * options::abstractValues() is on.
  73    */
  74   NodeToNodeHashMap d_abstractValues;
  75 };
  76
  77 }  // namespace smt
  78 }  // namespace CVC4
  79
  80 #endif