GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/ext_theory.h Lines: 7 8 87.5 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ext_theory.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Mathias Preiner
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 Extended theory interface.
13
 **
14
 ** This implements a generic module, used by theory solvers, for performing
15
 ** "context-dependent simplification", as described in Reynolds et al
16
 ** "Designing Theory Solvers with Extensions", FroCoS 2017.
17
 **
18
 ** At a high level, this technique implements a generic inference scheme based
19
 ** on the combination of SAT-context-dependent equality reasoning and
20
 ** SAT-context-indepedent rewriting.
21
 **
22
 ** As a simple example, say
23
 ** (1) TheoryStrings tells us that the following facts hold in the SAT context:
24
 **     x = "A" ^ str.contains( str.++( x, z ), "B" ) = true.
25
 ** (2) The Rewriter tells us that:
26
 **     str.contains( str.++( "A", z ), "B" ) ----> str.contains( z, "B" ).
27
 ** From this, this class may infer that the following lemma is T-valid:
28
 **   x = "A" ^ str.contains( str.++( x, z ), "B" ) => str.contains( z, "B" )
29
 **/
30
31
#include "cvc4_private.h"
32
33
#ifndef CVC4__THEORY__EXT_THEORY_H
34
#define CVC4__THEORY__EXT_THEORY_H
35
36
#include <map>
37
38
#include "context/cdhashmap.h"
39
#include "context/cdhashset.h"
40
#include "context/cdo.h"
41
#include "context/context.h"
42
#include "expr/node.h"
43
44
namespace CVC4 {
45
namespace theory {
46
47
class OutputChannel;
48
49
/**
50
 * A callback class for ExtTheory below. This class is responsible for
51
 * determining how to apply context-dependent simplification.
52
 */
53
22336
class ExtTheoryCallback
54
{
55
 public:
56
22327
  virtual ~ExtTheoryCallback() {}
57
  /*
58
   * Get current substitution at an effort
59
   * @param effort The effort identifier
60
   * @param vars The variables to get a substitution for
61
   * @param subs The terms to substitute for variables, in order. This vector
62
   * should be updated to one the same size as vars.
63
   * @param exp The map containing the explanation for each variable. Together
64
   * with subs, we have that:
65
   *   ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
66
   * @return true if any (non-identity) substitution was added to subs.
67
   */
68
  virtual bool getCurrentSubstitution(int effort,
69
                                      const std::vector<Node>& vars,
70
                                      std::vector<Node>& subs,
71
                                      std::map<Node, std::vector<Node> >& exp);
72
73
  /*
74
   * Is extended function n reduced? This returns true if n is reduced to a
75
   * form that requires no further interaction from the theory.
76
   *
77
   * @param effort The effort identifier
78
   * @param n The term to reduce
79
   * @param on The original form of n, before substitution
80
   * @param exp The explanation of on = n
81
   * @return true if n is reduced.
82
   */
83
  virtual bool isExtfReduced(int effort,
84
                             Node n,
85
                             Node on,
86
                             std::vector<Node>& exp);
87
88
  /**
89
   * Get reduction for node n.
90
   * If return value is true, then n is reduced.
91
   * If satDep is updated to false, then n is reduced independent of the
92
   * SAT context (e.g. by a lemma that persists at this
93
   * user-context level).
94
   * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
95
   * and return value of this method should be true.
96
   */
97
  virtual bool getReduction(int effort, Node n, Node& nr, bool& satDep);
98
};
99
100
/** Extended theory class
101
 *
102
 * This class is used for constructing generic extensions to theory solvers.
103
 * In particular, it provides methods for "context-dependent simplification"
104
 * and "model-based refinement". For details, see Reynolds et al "Design
105
 * Theory Solvers with Extensions", FroCoS 2017.
106
 *
107
 * It maintains:
108
 * (1) A set of "extended function" kinds (d_extf_kind),
109
 * (2) A database of active/inactive extended function terms (d_ext_func_terms)
110
 * that have been registered to the class.
111
 *
112
 * This class has methods doInferences/doReductions, which send out lemmas
113
 * based on the current set of active extended function terms. The former
114
 * is based on context-dependent simplification, where this class asks the
115
 * underlying theory for a "derivable substitution", whereby extended functions
116
 * may be reducable.
117
 */
118
class ExtTheory
119
{
120
  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
121
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
122
123
 public:
124
  /** constructor
125
   *
126
   * If cacheEnabled is false, we do not cache results of getSubstitutedTerm.
127
   */
128
  ExtTheory(ExtTheoryCallback& p,
129
            context::Context* c,
130
            context::UserContext* u,
131
            OutputChannel& out,
132
            bool cacheEnabled = false);
133
31276
  virtual ~ExtTheory() {}
134
  /** Tells this class to treat terms with Kind k as extended functions */
135
201759
  void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
136
  /** Is kind k treated as an extended function by this class? */
137
46
  bool hasFunctionKind(Kind k) const
138
  {
139
46
    return d_extf_kind.find(k) != d_extf_kind.end();
140
  }
141
  /** register term
142
   *
143
   * Registers term n with this class. Adds n to the set of extended function
144
   * terms known by this class (d_ext_func_terms) if n is an extended function,
145
   * that is, if addFunctionKind( n.getKind() ) was called.
146
   */
147
  void registerTerm(Node n);
148
  /** set n as reduced/inactive
149
   *
150
   * If satDep = false, then n remains inactive in the duration of this
151
   * user-context level
152
   */
153
  void markReduced(Node n, bool satDep = true);
154
  /**
155
   * Mark that a and b are congruent terms. This sets b inactive, and sets a to
156
   * inactive if b was inactive.
157
   */
158
  void markCongruent(Node a, Node b);
159
  /** getSubstitutedTerms
160
   *
161
   *  input : effort, terms
162
   *  output : sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i.
163
   *
164
   * For each i, sterms[i] = term[i] * sigma for some "derivable substitution"
165
   * sigma. We obtain derivable substitutions and their explanations via calls
166
   * to the underlying theory's Theory::getCurrentSubstitution method. This
167
   * also
168
   *
169
   * If useCache is true, we cache the result in d_gst_cache. This is a context
170
   * independent cache that can be cleared using clearCache() below.
171
   */
172
  void getSubstitutedTerms(int effort,
173
                           const std::vector<Node>& terms,
174
                           std::vector<Node>& sterms,
175
                           std::vector<std::vector<Node> >& exp,
176
                           bool useCache = false);
177
  /**
178
   * Same as above, but for a single term. We return the substituted form of
179
   * term and add its explanation to exp.
180
   */
181
  Node getSubstitutedTerm(int effort,
182
                          Node term,
183
                          std::vector<Node>& exp,
184
                          bool useCache = false);
185
  /** clear the cache for getSubstitutedTerm */
186
  void clearCache();
187
  /** doInferences
188
   *
189
   * This function performs "context-dependent simplification". The method takes
190
   * as input:
191
   *  effort: an identifier used to determine which terms we reduce and the
192
   *          form of the derivable substitution we will use,
193
   *  terms: the set of terms to simplify,
194
   *  batch: if this flag is true, we send lemmas for all terms; if it is false
195
   *         we send a lemma for the first applicable term.
196
   *
197
   * Sends rewriting lemmas of the form ( exp => t = c ) where t is in terms
198
   * and c is a constant, c = rewrite( t*sigma ) where exp |= sigma. These
199
   * lemmas are determined by asking the underlying theory for a derivable
200
   * substitution (through getCurrentSubstitution with getSubstitutedTerm)
201
   * above, applying this substitution to terms in terms, rewriting
202
   * the result and checking with the theory whether the resulting term is
203
   * in reduced form (isExtfReduced).
204
   *
205
   * This method adds the extended terms that are still active to nred, and
206
   * returns true if and only if a lemma of the above form was sent.
207
   */
208
  bool doInferences(int effort,
209
                    const std::vector<Node>& terms,
210
                    std::vector<Node>& nred,
211
                    bool batch = true);
212
  /**
213
   * Calls the above function, where terms is getActive(), the set of currently
214
   * active terms.
215
   */
216
  bool doInferences(int effort, std::vector<Node>& nred, bool batch = true);
217
  /** doReductions
218
   *
219
   * This method has the same interface as doInferences. In contrast to
220
   * doInfereces, this method will send reduction lemmas of the form ( t = t' )
221
   * where t is in terms and t' is an equivalent reduced term.
222
   */
223
  bool doReductions(int effort,
224
                    const std::vector<Node>& terms,
225
                    std::vector<Node>& nred,
226
                    bool batch = true);
227
  bool doReductions(int effort, std::vector<Node>& nred, bool batch = true);
228
229
  /** get the set of all extended function terms from d_ext_func_terms */
230
  void getTerms(std::vector<Node>& terms);
231
  /** is there at least one active extended function term? */
232
  bool hasActiveTerm() const;
233
  /** is n an active extended function term? */
234
  bool isActive(Node n) const;
235
  /** get the set of active terms from d_ext_func_terms */
236
  std::vector<Node> getActive() const;
237
  /** get the set of active terms from d_ext_func_terms of kind k */
238
  std::vector<Node> getActive(Kind k) const;
239
240
 private:
241
  /** returns the set of variable subterms of n */
242
  static std::vector<Node> collectVars(Node n);
243
  /** is n context dependent inactive? */
244
  bool isContextIndependentInactive(Node n) const;
245
  /** do inferences internal */
246
  bool doInferencesInternal(int effort,
247
                            const std::vector<Node>& terms,
248
                            std::vector<Node>& nred,
249
                            bool batch,
250
                            bool isRed);
251
  /** send lemma on the output channel */
252
  bool sendLemma(Node lem, bool preprocess = false);
253
  /** reference to the callback */
254
  ExtTheoryCallback& d_parent;
255
  /** Reference to the output channel we are using */
256
  OutputChannel& d_out;
257
  /** the true node */
258
  Node d_true;
259
  /** extended function terms, map to whether they are active */
260
  NodeBoolMap d_ext_func_terms;
261
  /**
262
   * The set of terms from d_ext_func_terms that are SAT-context-independent
263
   * inactive. For instance, a term t is SAT-context-independent inactive if
264
   * a reduction lemma of the form t = t' was added in this user-context level.
265
   */
266
  NodeSet d_ci_inactive;
267
  /**
268
   * Watched term for checking if any non-reduced extended functions exist.
269
   * This is an arbitrary active member of d_ext_func_terms.
270
   */
271
  context::CDO<Node> d_has_extf;
272
  /** the set of kinds we are treated as extended functions */
273
  std::map<Kind, bool> d_extf_kind;
274
  /** information for each term in d_ext_func_terms */
275
15858
  class ExtfInfo
276
  {
277
   public:
278
    /** all variables in this term */
279
    std::vector<Node> d_vars;
280
  };
281
  std::map<Node, ExtfInfo> d_extf_info;
282
283
  // cache of all lemmas sent
284
  NodeSet d_lemmas;
285
  NodeSet d_pp_lemmas;
286
  /** whether we enable caching for getSubstitutedTerm */
287
  bool d_cacheEnabled;
288
  /** Substituted term info */
289
  class SubsTermInfo
290
  {
291
   public:
292
    /** the substituted term */
293
    Node d_sterm;
294
    /** an explanation */
295
    std::vector<Node> d_exp;
296
  };
297
  /**
298
   * This maps an (effort, term) to the information above. It is used as a
299
   * cache for getSubstitutedTerm when d_cacheEnabled is true.
300
   */
301
  std::map<int, std::map<Node, SubsTermInfo> > d_gst_cache;
302
};
303
304
} /* CVC4::theory namespace */
305
} /* CVC4 namespace */
306
307
#endif /* CVC4__THEORY__EXT_THEORY_H */