GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/abstraction.h Lines: 7 34 20.6 %
Date: 2021-03-22 Branches: 1 48 2.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file abstraction.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, 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 Bitvector theory.
13
 **
14
 ** Bitvector theory.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BV__ABSTRACTION_H
20
#define CVC4__THEORY__BV__ABSTRACTION_H
21
22
#include <unordered_map>
23
#include <unordered_set>
24
25
#include "expr/node.h"
26
#include "theory/substitutions.h"
27
#include "util/statistics_registry.h"
28
#include "util/stats_timer.h"
29
30
namespace CVC4 {
31
namespace theory {
32
namespace bv {
33
34
typedef std::vector<TNode> ArgsVec;
35
36
8982
class AbstractionModule {
37
38
  struct Statistics {
39
    IntStat d_numFunctionsAbstracted;
40
    IntStat d_numArgsSkolemized;
41
    TimerStat d_abstractionTime;
42
    Statistics(const std::string& name);
43
    ~Statistics();
44
  };
45
46
47
  class ArgsTableEntry {
48
    std::vector<ArgsVec> d_data;
49
    unsigned d_arity;
50
  public:
51
    ArgsTableEntry(unsigned n)
52
      : d_arity(n)
53
    {}
54
    ArgsTableEntry()
55
      : d_arity(0)
56
    {}
57
    void addArguments(const ArgsVec& args);
58
    typedef std::vector<ArgsVec>::iterator iterator;
59
60
    iterator begin() { return d_data.begin(); }
61
    iterator end() { return d_data.end(); }
62
    unsigned getArity() { return d_arity; }
63
    unsigned getNumEntries() { return d_data.size(); }
64
    ArgsVec& getEntry(unsigned i)
65
    {
66
      Assert(i < d_data.size());
67
      return d_data[i];
68
    }
69
  };
70
71
8982
  class ArgsTable {
72
    std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
73
    bool hasEntry(TNode signature) const;
74
  public:
75
    typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
76
8985
    ArgsTable() {}
77
    void addEntry(TNode signature, const ArgsVec& args);
78
    ArgsTableEntry& getEntry(TNode signature);
79
    iterator begin() { return d_data.begin(); }
80
    iterator end() { return d_data.end(); }
81
  };
82
83
  /**
84
   * Checks if one pattern is a generalization of the other
85
   *
86
   * @param s
87
   * @param t
88
   *
89
   * @return 1 if s :> t, 2 if s <: t, 0 if they equivalent and -1 if they are incomparable
90
   */
91
  static int comparePatterns(TNode s, TNode t);
92
93
  class LemmaInstantiatior {
94
    std::vector<TNode> d_functions;
95
    std::vector<int> d_maxMatch;
96
    ArgsTable& d_argsTable;
97
    context::Context* d_ctx;
98
    theory::SubstitutionMap d_subst;
99
    TNode d_conflict;
100
    std::vector<Node> d_lemmas;
101
102
    void backtrack(std::vector<int>& stack);
103
    int next(int val, int index);
104
    bool isConsistent(const std::vector<int>& stack);
105
    bool accept(const std::vector<int>& stack);
106
    void mkLemma();
107
  public:
108
    LemmaInstantiatior(const std::vector<TNode>& functions, ArgsTable& table, TNode conflict)
109
      : d_functions(functions)
110
      , d_argsTable(table)
111
      , d_ctx(new context::Context())
112
      , d_subst(d_ctx)
113
      , d_conflict(conflict)
114
      , d_lemmas()
115
    {
116
      Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n";
117
      // initializing the search space
118
      for (unsigned i = 0; i < functions.size(); ++i) {
119
        TNode func_op = functions[i].getOperator();
120
        // number of matches for this function
121
        unsigned maxCount = table.getEntry(func_op).getNumEntries();
122
        d_maxMatch.push_back(maxCount);
123
      }
124
    }
125
126
    void generateInstantiations(std::vector<Node>& lemmas);
127
128
  };
129
130
  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
131
  typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
132
  typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
133
  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
134
  typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
135
  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
136
  typedef std::unordered_map<unsigned, Node> IntNodeMap;
137
  typedef std::unordered_map<unsigned, unsigned> IndexMap;
138
  typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap;
139
  typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
140
141
  ArgsTable d_argsTable;
142
143
  // mapping between signature and uninterpreted function symbol used to
144
  // abstract the signature
145
  NodeNodeMap d_signatureToFunc;
146
  NodeNodeMap d_funcToSignature;
147
148
  NodeNodeMap d_assertionToSignature;
149
  SignatureMap d_signatures;
150
  NodeNodeMap d_sigToGeneralization;
151
  TNodeSet d_skolems;
152
153
  // skolems maps
154
  IndexMap d_signatureIndices;
155
  SkolemMap d_signatureSkolems;
156
157
  void collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen);
158
  void collectArguments(TNode node, TNode sig, std::vector<Node>& args, TNodeSet& seen);
159
  void finalizeSignatures();
160
  Node abstractSignatures(TNode assertion);
161
  Node computeSignature(TNode node);
162
163
  bool isConjunctionOfAtoms(TNode node, TNodeSet& seen);
164
165
  TNode getGeneralization(TNode term);
166
  void storeGeneralization(TNode s, TNode t);
167
168
  // signature skolem stuff
169
  Node getGeneralizedSignature(Node node);
170
  Node getSignatureSkolem(TNode node);
171
172
  unsigned getBitwidthIndex(unsigned bitwidth);
173
  void resetSignatureIndex();
174
  Node computeSignatureRec(TNode, NodeNodeMap&);
175
  void storeSignature(Node signature, TNode assertion);
176
  bool hasSignature(Node node);
177
178
  Node substituteArguments(TNode signature, TNode apply, unsigned& i, TNodeTNodeMap& seen);
179
180
  // crazy instantiation methods
181
  void generateInstantiations(unsigned current,
182
                              std::vector<ArgsTableEntry>& matches,
183
                              std::vector<std::vector<ArgsVec> >& instantiations,
184
                              std::vector<std::vector<ArgsVec> >& new_instantiations);
185
186
  Node tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict);
187
  void makeFreshArgs(TNode func, std::vector<Node>& fresh_args);
188
  void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map);
189
190
  void skolemizeArguments(std::vector<Node>& assertions);
191
  Node reverseAbstraction(Node assertion, NodeNodeMap& seen);
192
193
  TNodeSet d_addedLemmas;
194
  TNodeSet d_lemmaAtoms;
195
  TNodeSet d_inputAtoms;
196
  void storeLemma(TNode lemma);
197
198
  Statistics d_statistics;
199
200
public:
201
8985
  AbstractionModule(const std::string& name)
202
8985
    : d_argsTable()
203
    , d_signatureToFunc()
204
    , d_funcToSignature()
205
    , d_assertionToSignature()
206
    , d_signatures()
207
    , d_sigToGeneralization()
208
    , d_skolems()
209
    , d_signatureIndices()
210
    , d_signatureSkolems()
211
    , d_addedLemmas()
212
    , d_lemmaAtoms()
213
    , d_inputAtoms()
214
8985
    , d_statistics(name)
215
8985
  {}
216
  /**
217
   * returns true if there are new uninterepreted functions symbols in the output
218
   *
219
   * @param assertions
220
   * @param new_assertions
221
   *
222
   * @return
223
   */
224
  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
225
  /**
226
   * Returns true if the node represents an abstraction predicate.
227
   *
228
   * @param node
229
   *
230
   * @return
231
   */
232
  bool isAbstraction(TNode node);
233
  /**
234
   * Returns the interpretation of the abstraction predicate.
235
   *
236
   * @param node
237
   *
238
   * @return
239
   */
240
  Node getInterpretation(TNode node);
241
  Node simplifyConflict(TNode conflict);
242
  void generalizeConflict(TNode conflict, std::vector<Node>& lemmas);
243
  void addInputAtom(TNode atom);
244
  bool isLemmaAtom(TNode node) const;
245
};
246
247
}
248
}
249
}
250
251
#endif