GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/dynamic_rewrite.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dynamic_rewrite.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 dynamic_rewriter
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
18
#define CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
19
20
#include <map>
21
22
#include "context/cdlist.h"
23
#include "theory/uf/equality_engine.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
/** DynamicRewriter
30
 *
31
 * This class is given a stream of equalities in calls to addRewrite(...).
32
 * The goal is to show that a subset of these can be inferred from previously
33
 * asserted equalities.  For example, a possible set of return values for
34
 * add rewrite on successive calls is the following:
35
 *
36
 *   addRewrite( x, y ) ---> true
37
 *   addRewrite( f( x ), f( y ) ) ---> false, since we already know x=y
38
 *   addRewrite( x, z ) ---> true
39
 *   addRewrite( x+y, x+z ) ---> false, since we already know y=x=z.
40
 *
41
 * This class can be used to filter out redundant candidate rewrite rules
42
 * when using the option sygusRewSynth().
43
 *
44
 * Currently, this class infers that an equality is redundant using
45
 * an instance of the equality engine that does congruence over all
46
 * operators by mapping all operators to uninterpreted ones and doing
47
 * congruence on APPLY_UF.
48
 *
49
 * TODO (#1591): Add more advanced technique, e.g. by theory rewriting
50
 * to show when terms can already be inferred equal.
51
 */
52
class DynamicRewriter
53
{
54
  typedef context::CDList<Node> NodeList;
55
56
 public:
57
  DynamicRewriter(const std::string& name, context::UserContext* u);
58
8
  ~DynamicRewriter() {}
59
  /** inform this class that the equality a = b holds. */
60
  void addRewrite(Node a, Node b);
61
  /**
62
   * Check whether this class knows that the equality a = b holds.
63
   */
64
  bool areEqual(Node a, Node b);
65
  /**
66
   * Convert node a to its internal representation, which replaces all
67
   * interpreted operators in a by a unique uninterpreted symbol.
68
   */
69
  Node toInternal(Node a);
70
  /**
71
   * Convert internal node ai to its original representation. It is the case
72
   * that toExternal(toInternal(a))=a. If ai is not a term returned by
73
   * toInternal, this method returns null.
74
   */
75
  Node toExternal(Node ai);
76
77
 private:
78
  /** index over argument types to function skolems
79
   *
80
   * The purpose of this trie is to associate a class of interpreted operator
81
   * with uninterpreted symbols. It is necessary to introduce multiple
82
   * uninterpreted symbols per interpreted operator since they may be
83
   * polymorphic. For example, for array select, its associate trie may look
84
   * like this:
85
   *   d_children[array_type_1]
86
   *     d_children[index_type_1] : k1
87
   *     d_children[index_type_2] : k2
88
   *   d_children[array_type_2]
89
   *     d_children[index_type_1] : k3
90
   */
91
262
  class OpInternalSymTrie
92
  {
93
   public:
94
    /**
95
     * Get the uninterpreted function corresponding to the top-most symbol
96
     * of the internal representation of term n. This will return a skolem
97
     * of the same type as n.getOperator() if it has one, or of the same type
98
     * as n itself otherwise.
99
     */
100
    Node getSymbol(Node n);
101
102
   private:
103
    /** the symbol at this node in the trie */
104
    Node d_sym;
105
    /** the children of this node in the trie */
106
    std::map<TypeNode, OpInternalSymTrie> d_children;
107
  };
108
  /** the internal operator symbol trie for this class */
109
  std::map<Node, OpInternalSymTrie> d_ois_trie;
110
  /** cache of the above function */
111
  std::map<Node, Node> d_term_to_internal;
112
  /** inverse of the above map */
113
  std::map<Node, Node> d_internal_to_term;
114
  /** stores congruence closure over terms given to this class. */
115
  eq::EqualityEngine d_equalityEngine;
116
  /** list of all equalities asserted to equality engine */
117
  NodeList d_rewrites;
118
};
119
120
} /* CVC4::theory::quantifiers namespace */
121
} /* CVC4::theory namespace */
122
} /* CVC4 namespace */
123
124
#endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */