1 /********************* */
2 /*! \file abstract_values.h
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
12 ** \brief Utility for constructing and maintaining abstract values.
15 #include "cvc4_private.h"
17 #ifndef CVC4__SMT__ABSTRACT_VALUES_H
18 #define CVC4__SMT__ABSTRACT_VALUES_H
20 #include <unordered_map>
22 #include "context/context.h"
23 #include "expr/node.h"
24 #include "theory/substitutions.h"
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.
36 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeToNodeHashMap
;
38 AbstractValues(NodeManager
* nm
);
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).
45 Node
substituteAbstractValues(TNode n
);
48 * Make a new (or return an existing) abstract value for a node.
49 * Can only use this if options::abstractValues() is on.
51 Node
mkAbstractValue(TNode n
);
54 /** Pointer to the used node manager */
57 * A context that never pushes/pops, for use by CD structures (like
58 * SubstitutionMaps) that should be "global".
60 context::Context d_fakeContext
;
63 * A map of AbsractValues to their actual constants. Only used if
64 * options::abstractValues() is on.
66 theory::SubstitutionMap d_abstractValueMap
;
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.
74 NodeToNodeHashMap d_abstractValues
;