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

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_strategy_cegqi.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Tim King
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 counterexample-guided quantifier instantiation
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
18
#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
19
20
#include "theory/decision_manager.h"
21
#include "theory/quantifiers/bv_inverter.h"
22
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
23
#include "theory/quantifiers/cegqi/nested_qe.h"
24
#include "theory/quantifiers/cegqi/vts_term_cache.h"
25
#include "theory/quantifiers/instantiate.h"
26
#include "theory/quantifiers/quant_module.h"
27
#include "util/statistics_registry.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace quantifiers {
32
33
class InstStrategyCegqi;
34
35
/**
36
 * An instantiation rewriter based on the counterexample-guided instantiation
37
 * quantifiers module below.
38
 */
39
class InstRewriterCegqi : public InstantiationRewriter
40
{
41
 public:
42
  InstRewriterCegqi(InstStrategyCegqi* p);
43
11948
  ~InstRewriterCegqi() {}
44
  /**
45
   * Rewrite the instantiation via d_parent, based on virtual term substitution
46
   * and nested quantifier elimination. Returns a TrustNode of kind REWRITE,
47
   * corresponding to the rewrite and its proof generator.
48
   */
49
  TrustNode rewriteInstantiation(Node q,
50
                                 std::vector<Node>& terms,
51
                                 Node inst,
52
                                 bool doVts) override;
53
54
 private:
55
  /** pointer to the parent of this class */
56
  InstStrategyCegqi* d_parent;
57
};
58
59
/**
60
 * Counterexample-guided quantifier instantiation module.
61
 *
62
 * This class manages counterexample-guided instantiation strategies for all
63
 * asserted quantified formulas.
64
 */
65
class InstStrategyCegqi : public QuantifiersModule
66
{
67
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
68
  typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
69
70
 public:
71
  InstStrategyCegqi(QuantifiersEngine* qe,
72
                    QuantifiersState& qs,
73
                    QuantifiersInferenceManager& qim,
74
                    QuantifiersRegistry& qr);
75
  ~InstStrategyCegqi();
76
77
  /** whether to do counterexample-guided instantiation for quantifier q */
78
  bool doCbqi(Node q);
79
  /** needs check at effort */
80
  bool needsCheck(Theory::Effort e) override;
81
  /** needs model at effort */
82
  QEffort needsModel(Theory::Effort e) override;
83
  /** reset round */
84
  void reset_round(Theory::Effort e) override;
85
  /** check */
86
  void check(Theory::Effort e, QEffort quant_e) override;
87
  /** check complete */
88
  bool checkComplete() override;
89
  /** check complete for quantified formula */
90
  bool checkCompleteFor(Node q) override;
91
  /** check ownership */
92
  void checkOwnership(Node q) override;
93
  /** identify */
94
141415
  std::string identify() const override { return std::string("Cegqi"); }
95
  /** get instantiator for quantifier */
96
  CegInstantiator* getInstantiator(Node q);
97
  /** get the virtual term substitution term cache utility */
98
  VtsTermCache* getVtsTermCache() const;
99
  /** get the BV inverter utility */
100
  BvInverter* getBvInverter() const;
101
  /** pre-register quantifier */
102
  void preRegisterQuantifier(Node q) override;
103
104
  /**
105
   * Rewrite the instantiation inst of quantified formula q for terms; return
106
   * the result.
107
   *
108
   * We rewrite inst based on virtual term substitution and nested quantifier
109
   * elimination. For details, see "Solving Quantified Linear Arithmetic via
110
   * Counterexample-Guided Instantiation" FMSD 2017, Reynolds et al.
111
   *
112
   * Returns a TrustNode of kind REWRITE, corresponding to the rewrite and its
113
   * proof generator.
114
   */
115
  TrustNode rewriteInstantiation(Node q,
116
                                 std::vector<Node>& terms,
117
                                 Node inst,
118
                                 bool doVts);
119
  /** get the instantiation rewriter object */
120
  InstantiationRewriter* getInstRewriter() const;
121
122
  //------------------- interface for CegqiOutputInstStrategy
123
  /** Instantiate the current quantified formula forall x. Q with x -> subs. */
124
  bool doAddInstantiation(std::vector<Node>& subs);
125
  /** Add pending lemma lem via the inference manager of this class. */
126
  bool addPendingLemma(Node lem) const;
127
  //------------------- end interface for CegqiOutputInstStrategy
128
129
 protected:
130
  /** The instantiation rewriter object */
131
  std::unique_ptr<InstRewriterCegqi> d_irew;
132
  /** set quantified formula inactive
133
   *
134
   * This flag is set to true during a full effort check if at least one
135
   * quantified formula is set "inactive", that is, its negation is
136
   * unsatisfiable in the current context.
137
   */
138
  bool d_cbqi_set_quant_inactive;
139
  /** incomplete check
140
   *
141
   * This is set to true during a full effort check if this strategy could
142
   * not find an instantiation for at least one asserted quantified formula.
143
   */
144
  bool d_incomplete_check;
145
  /** whether we have added cbqi lemma */
146
  NodeSet d_added_cbqi_lemma;
147
  /** parent guards */
148
  std::map< Node, std::vector< Node > > d_parent_quant;
149
  std::map< Node, std::vector< Node > > d_children_quant;
150
  std::map< Node, bool > d_active_quant;
151
  /** Whether cegqi handles each quantified formula. */
152
  std::map<Node, CegHandledStatus> d_do_cbqi;
153
  /**
154
   * The instantiator for each quantified formula q registered to this class.
155
   * This object is responsible for finding instantiatons for q.
156
   */
157
  std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
158
  /** virtual term substitution term cache for arithmetic instantiation */
159
  std::unique_ptr<VtsTermCache> d_vtsCache;
160
  /** inversion utility for BV instantiation */
161
  std::unique_ptr<BvInverter> d_bv_invert;
162
  /**
163
   * The decision strategy for each quantified formula q registered to this
164
   * class.
165
   */
166
  std::map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat;
167
  /** the current quantified formula we are processing */
168
  Node d_curr_quant;
169
  //---------------------- for vts delta minimization
170
  /**
171
   * Whether we will use vts delta minimization. If this flag is true, we
172
   * add lemmas on demand of the form delta < c^1, delta < c^2, ... where c
173
   * is a small (< 1) constant. This heuristic is used in strategies where
174
   * vts delta cannot be fully eliminated from assertions (for example, when
175
   * using nested quantifiers and a non-innermost instantiation strategy).
176
   * The same strategy applies for vts infinity, which we add lemmas of the
177
   * form inf > (1/c)^1, inf > (1/c)^2, ....
178
   */
179
  bool d_check_vts_lemma_lc;
180
  /** a small constant, used as a coefficient above */
181
  Node d_small_const;
182
  //---------------------- end for vts delta minimization
183
  /** register ce lemma */
184
  bool registerCbqiLemma( Node q );
185
  /** register counterexample lemma
186
   *
187
   * This is called when we have constructed lem, the negation of the body of
188
   * quantified formula q, skolemized with the instantiation constants of q.
189
   * This function is used for setting up the proper information in the
190
   * instantiator for q.
191
   */
192
  void registerCounterexampleLemma(Node q, Node lem);
193
  /** has added cbqi lemma */
194
1859
  bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
195
  /**
196
   * Return true if q can be processed with nested quantifier elimination.
197
   * This may add a lemma on the output channel of quantifiers engine if so.
198
   *
199
   * @param q The quantified formula to process
200
   * @param isPreregister Whether this method is being called at preregister.
201
   */
202
  bool processNestedQe(Node q, bool isPreregister);
203
  /** process functions */
204
  void process(Node q, Theory::Effort effort, int e);
205
  /**
206
   * Get counterexample literal. This is the fresh Boolean variable whose
207
   * semantics is "there exists a set of values for which the body of
208
   * quantified formula q does not hold". These literals are cached by this
209
   * class.
210
   */
211
  Node getCounterexampleLiteral(Node q);
212
  /** map from universal quantifiers to their counterexample literals */
213
  std::map<Node, Node> d_ce_lit;
214
  /** The nested quantifier elimination utility */
215
  std::unique_ptr<NestedQe> d_nestedQe;
216
};
217
218
}
219
}
220
}
221
222
#endif