GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_bv_instantiator.h Lines: 3 3 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ceg_bv_instantiator.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 ceg_bv_instantiator
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
18
#define CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
19
20
#include <unordered_map>
21
#include "theory/quantifiers/bv_inverter.h"
22
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
/** Bitvector instantiator
29
 *
30
 * This implements an approach for counterexample-guided instantiation
31
 * for bit-vector variables based on word-level inversions. For details,
32
 * see Niemetz et al, "Solving Quantified Bit-Vectors Using Invertibility
33
 * Conditions", CAV 2018. It is enabled by --cbqi-bv.
34
 *
35
 * This class contains all necessary information for instantiating a single
36
 * bit-vector variable of a single quantified formula.
37
 */
38
class BvInstantiator : public Instantiator
39
{
40
 public:
41
  BvInstantiator(TypeNode tn, BvInverter* inv);
42
  ~BvInstantiator() override;
43
  /** reset */
44
  void reset(CegInstantiator* ci,
45
             SolvedForm& sf,
46
             Node pv,
47
             CegInstEffort effort) override;
48
  /** this instantiator processes assertions */
49
  bool hasProcessAssertion(CegInstantiator* ci,
50
                           SolvedForm& sf,
51
                           Node pv,
52
                           CegInstEffort effort) override;
53
  /** this instantiator processes bit-vector equalities and inequalities
54
   *
55
   * Based on the configuration --cbqi-bv-ineq, it may modify the form of lit
56
   * based on a projection. For lit (not) s <> t, this may be one of:
57
   * - eq-slack: s = t + ( s^M - t^M )
58
   * - eq-boundary: s = t + ( s^M > t^M ? 1 : -1 )
59
   * - keep: (not) s <> t, i.e. unchanged.
60
   * Additionally for eq-boundary, inequalities s != t become s < t or t < s.
61
   * This is the method project_* from Figure 3 of Niemetz et al, CAV 2018.
62
   */
63
  Node hasProcessAssertion(CegInstantiator* ci,
64
                           SolvedForm& sf,
65
                           Node pv,
66
                           Node lit,
67
                           CegInstEffort effort) override;
68
  /** process assertion
69
   *
70
   * Computes a solved form for pv in lit based on Figure 1 of Niemetz et al,
71
   * CAV 2018.
72
   */
73
  bool processAssertion(CegInstantiator* ci,
74
                        SolvedForm& sf,
75
                        Node pv,
76
                        Node lit,
77
                        Node alit,
78
                        CegInstEffort effort) override;
79
  /** process assertions
80
   *
81
   * This is called after processAssertion has been called on all currently
82
   * asserted literals that involve pv. This chooses the best solved form for pv
83
   * based on heuristics. Currently, by default, we choose a random solved form.
84
   * We may try multiple or zero bounds based on the options
85
   * --cbqi-multi-inst and --cbqi-bv-interleave-value.
86
   */
87
  bool processAssertions(CegInstantiator* ci,
88
                         SolvedForm& sf,
89
                         Node pv,
90
                         CegInstEffort effort) override;
91
  /** use model value
92
   *
93
   * We allow model values if we have not already tried an assertion,
94
   * and only at levels below full if cbqiFullEffort is false.
95
   */
96
  bool useModelValue(CegInstantiator* ci,
97
                     SolvedForm& sf,
98
                     Node pv,
99
                     CegInstEffort effort) override;
100
  /** identify */
101
3710
  std::string identify() const override { return "Bv"; }
102
103
 private:
104
  /** pointer to the bv inverter class */
105
  BvInverter* d_inverter;
106
  //--------------------------------solved forms
107
  /** identifier counter, used to allocate ids to each solve form */
108
  unsigned d_inst_id_counter;
109
  /** map from variables to list of solved form ids */
110
  std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>
111
      d_var_to_inst_id;
112
  /** for each solved form id, the term for instantiation */
113
  std::unordered_map<unsigned, Node> d_inst_id_to_term;
114
  /** for each solved form id, the corresponding asserted literal */
115
  std::unordered_map<unsigned, Node> d_inst_id_to_alit;
116
  /** map from variable to current id we are processing */
117
  std::unordered_map<Node, unsigned, NodeHashFunction> d_var_to_curr_inst_id;
118
  /** the amount of slack we added for asserted literals */
119
  std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack;
120
  //--------------------------------end solved forms
121
  /** rewrite assertion for solve pv
122
   *
123
   * Returns a literal that is equivalent to lit that leads to best solved form
124
   * for pv.
125
   */
126
  Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit);
127
  /** rewrite term for solve pv
128
   *
129
   * This is a helper function for rewriteAssertionForSolvePv.
130
   * If this returns non-null value ret, then this indicates
131
   * that n should be rewritten to ret. It is called as
132
   * a "post-rewrite", that is, after the children of n
133
   * have been rewritten and stored in the vector children.
134
   *
135
   * contains_pv stores whether certain nodes contain pv.
136
   * where we guarantee that all subterms of terms in children
137
   * appear in the domain of contains_pv.
138
   */
139
  Node rewriteTermForSolvePv(
140
      Node pv,
141
      Node n,
142
      std::vector<Node>& children,
143
      std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
144
  /** process literal, called from processAssertion
145
   *
146
   * lit is the literal to solve for pv that has been rewritten according to
147
   * internal rules here.
148
   * alit is the asserted literal that lit is derived from.
149
   */
150
  void processLiteral(CegInstantiator* ci,
151
                      SolvedForm& sf,
152
                      Node pv,
153
                      Node lit,
154
                      Node alit,
155
                      CegInstEffort effort);
156
};
157
158
/** Bitvector instantiator preprocess
159
 *
160
 * This class implements preprocess techniques that are helpful for
161
 * counterexample-guided instantiation, such as introducing variables
162
 * that refer to disjoint bit-vector extracts.
163
 */
164
class BvInstantiatorPreprocess : public InstantiatorPreprocess
165
{
166
 public:
167
718
  BvInstantiatorPreprocess() {}
168
1436
  ~BvInstantiatorPreprocess() override {}
169
  /** register counterexample lemma
170
   *
171
   * This method adds to auxLems based on the extract terms that lem
172
   * contains when the option --cbqi-bv-rm-extract is enabled. It introduces
173
   * a dummy equality so that segments of terms t under extracts can be solved
174
   * independently.
175
   *
176
   * For example, if lem is:
177
   *   P[ ((extract 7 4) t), ((extract 3 0) t)]
178
   *     then we add:
179
   *   t = concat( x74, x30 )
180
   * to auxLems, where x74 and x30 are fresh variables of type BV_4, which are
181
   * added to ceVars.
182
   *
183
   * Another example, for:
184
   *   P[ ((extract 7 3) t), ((extract 4 0) t)]
185
   *     we add:
186
   *   t = concat( x75, x44, x30 )
187
   * to auxLems where x75, x44 and x30 are fresh variables of type BV_3, BV_1,
188
   * and BV_4 respectively, which are added to ceVars.
189
   *
190
   * Notice we leave the original lem alone. This is done for performance
191
   * since the added equalities ensure we are able to construct the proper
192
   * solved forms for variables in t and for the intermediate variables above.
193
   */
194
  void registerCounterexampleLemma(Node lem,
195
                                   std::vector<Node>& ceVars,
196
                                   std::vector<Node>& auxLems) override;
197
198
 private:
199
  /** collect extracts
200
   *
201
   * This method collects all extract terms in lem
202
   * and stores them in d_extract_map.
203
   * visited is the terms we've already visited.
204
   */
205
  void collectExtracts(Node lem,
206
                       std::map<Node, std::vector<Node> >& extract_map,
207
                       std::unordered_set<TNode, TNodeHashFunction>& visited);
208
};
209
210
}  // namespace quantifiers
211
}  // namespace theory
212
}  // namespace CVC4
213
214
#endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */