GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/vts_term_cache.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file vts_term_cache.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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 Virtual term substitution term cache.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
18
#define CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
19
20
#include <map>
21
#include "expr/attribute.h"
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
/** Attribute to mark Skolems as virtual terms */
28
struct VirtualTermSkolemAttributeId
29
{
30
};
31
typedef expr::Attribute<VirtualTermSkolemAttributeId, bool>
32
    VirtualTermSkolemAttribute;
33
34
namespace quantifiers {
35
36
class QuantifiersInferenceManager;
37
38
/** Virtual term substitution term cache
39
 *
40
 * This class stores skolems corresponding to virtual terms (e.g. delta and
41
 * infinity) and has methods for performing virtual term substitution.
42
 *
43
 * In detail, there are three kinds of virtual terms:
44
 * (1) delta, of Real type, representing a infinitesimally small real value,
45
 * (2) infinity, of Real type, representing an infinitely large real value,
46
 * (3) infinity, of Int type, representing an infinitely large integer value.
47
 *
48
 * For each of the above three virtual terms, we have 2 variants.
49
 *
50
 * The first variant we simply call "virtual terms". These terms are intended
51
 * to never appear in assertions and are simply used by algorithms e.g. CEGQI
52
 * for specifying instantiations. They are eliminated by the standard rules of
53
 * virtual term substitution, e.g.:
54
 *   t < s + delta ---> t <=s
55
 *   t <= s + delta ---> t <= s
56
 *   t < s - delta ----> t < s
57
 *   t <= s - delta -----> t < s
58
 *   t <= s + inf ----> true
59
 *   t <= s - inf ----> false
60
 *
61
 * The second variant we call "free virtual terms". These terms are intended
62
 * to appear in assertions and are constrained to have the semantics of the
63
 * above virtual terms, e.g.:
64
 *   0 < delta_free
65
 *   forall x. x < inf_free
66
 * We use free virtual terms for some instantiation strategies, e.g. those
67
 * that combine instantiating quantified formulas with nested quantifiers
68
 * with terms containing virtual terms.
69
 */
70
class VtsTermCache
71
{
72
 public:
73
  VtsTermCache(QuantifiersInferenceManager& qim);
74
5974
  ~VtsTermCache() {}
75
  /**
76
   * Get vts delta. The argument isFree indicates if we are getting the
77
   * free variant of delta. If create is false, this method returns Node::null
78
   * if the requested delta has not already been created.
79
   */
80
  Node getVtsDelta(bool isFree = false, bool create = true);
81
  /**
82
   * Get vts infinity of type tn, where tn should be Int or Real.
83
   * The argument isFree indicates if we are getting the free variant of
84
   * infinity. If create is false, this method returns Node::null if the
85
   * requested infinity has not already been created.
86
   */
87
  Node getVtsInfinity(TypeNode tn, bool isFree = false, bool create = true);
88
  /**
89
   * Get all vts terms and add them to vector t.
90
   * If the argument isFree is true, we return the free variant of all virtual
91
   * terms. If create is false, we do not add virtual terms that have not
92
   * already been created. If inc_delta is false, we do not include delta.
93
   */
94
  void getVtsTerms(std::vector<Node>& t,
95
                   bool isFree = false,
96
                   bool create = true,
97
                   bool inc_delta = true);
98
  /**
99
   * Rewrite virtual terms in node n. This returns the rewritten form of n
100
   * after virtual term substitution.
101
   *
102
   * This method ensures that the returned node is equivalent to n and does
103
   * not contain free occurrences of the virtual terms.
104
   */
105
  Node rewriteVtsSymbols(Node n);
106
  /**
107
   * This method returns true iff n contains a virtual term. If isFree is true,
108
   * if returns true iff n contains a free virtual term.
109
   */
110
  bool containsVtsTerm(Node n, bool isFree = false);
111
  /**
112
   * This method returns true iff any term in vector n contains a virtual term.
113
   * If isFree is true, if returns true iff any term in vector n contains a
114
   * free virtual term.
115
   */
116
  bool containsVtsTerm(std::vector<Node>& n, bool isFree = false);
117
  /**
118
   * This method returns true iff n contains an occurence of the virtual term
119
   * infinity. If isFree is true, if returns true iff n contains the free
120
   * virtual term infinity.
121
   */
122
  bool containsVtsInfinity(Node n, bool isFree = false);
123
124
 private:
125
  /** Reference to the quantifiers inference manager */
126
  QuantifiersInferenceManager& d_qim;
127
  /** constants */
128
  Node d_zero;
129
  /** The virtual term substitution delta */
130
  Node d_vts_delta;
131
  /** The virtual term substitution "free delta" */
132
  Node d_vts_delta_free;
133
  /** The virtual term substitution infinities for int/real types */
134
  std::map<TypeNode, Node> d_vts_inf;
135
  /** The virtual term substitution "free infinities" for int/real types */
136
  std::map<TypeNode, Node> d_vts_inf_free;
137
  /** substitute vts terms with their corresponding vts free terms */
138
  Node substituteVtsFreeTerms(Node n);
139
}; /* class TermUtil */
140
141
}  // namespace quantifiers
142
}  // namespace theory
143
}  // namespace CVC4
144
145
#endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */