GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_conflict_find.h Lines: 18 18 100.0 %
Date: 2021-03-23 Branches: 19 36 52.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_conflict_find.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Morgan Deters
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 quantifiers conflict find class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef QUANT_CONFLICT_FIND
18
#define QUANT_CONFLICT_FIND
19
20
#include <ostream>
21
#include <vector>
22
23
#include "context/cdhashmap.h"
24
#include "context/cdlist.h"
25
#include "expr/node_trie.h"
26
#include "theory/quantifiers/quant_module.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
class QuantConflictFind;
33
class QuantInfo;
34
35
//match generator
36
349923
class MatchGen {
37
  friend class QuantInfo;
38
private:
39
  //current children information
40
  int d_child_counter;
41
  bool d_use_children;
42
  //children of this object
43
  std::vector< int > d_children_order;
44
487409
  unsigned getNumChildren() { return d_children.size(); }
45
2162524
  MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
46
  //MatchGen * getChild( int i ) { return &d_children[i]; }
47
  //current matching information
48
  std::vector<TNodeTrie*> d_qn;
49
  std::vector<std::map<TNode, TNodeTrie>::iterator> d_qni;
50
  bool doMatching( QuantConflictFind * p, QuantInfo * qi );
51
  //for matching : each index is either a variable or a ground term
52
  unsigned d_qni_size;
53
  std::map< int, int > d_qni_var_num;
54
  std::map< int, TNode > d_qni_gterm;
55
  std::map< int, int > d_qni_bound;
56
  std::vector< int > d_qni_bound_except;
57
  std::map< int, TNode > d_qni_bound_cons;
58
  std::map< int, int > d_qni_bound_cons_var;
59
  std::map< int, int >::iterator d_binding_it;
60
  //std::vector< int > d_independent;
61
  bool d_matched_basis;
62
  bool d_binding;
63
  //int getVarBindingVar();
64
  std::map< int, Node > d_ground_eval;
65
  //determine variable order
66
  void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars );
67
  void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars, std::map< Node, bool >& visited, bool& hasNested );
68
public:
69
  //type of the match generator
70
  enum {
71
    typ_invalid,
72
    typ_ground,
73
    typ_pred,
74
    typ_eq,
75
    typ_formula,
76
    typ_var,
77
    typ_bool_var,
78
    typ_tconstraint,
79
    typ_tsym,
80
  };
81
  void debugPrintType( const char * c, short typ, bool isTrace = false );
82
public:
83
  MatchGen();
84
  MatchGen( QuantInfo * qi, Node n, bool isVar = false );
85
  bool d_tgt;
86
  bool d_tgt_orig;
87
  bool d_wasSet;
88
  Node d_n;
89
  std::vector< MatchGen > d_children;
90
  short d_type;
91
  bool d_type_not;
92
  /** reset round
93
   *
94
   * Called once at the beginning of each full/last-call effort, prior to
95
   * processing this match generator. This method returns false if the reset
96
   * failed, e.g. if a conflict was encountered during term indexing.
97
   */
98
  bool reset_round(QuantConflictFind* p);
99
  void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );
100
  bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
101
433497
  bool isValid() { return d_type!=typ_invalid; }
102
  void setInvalid();
103
104
  // is this term treated as UF application?
105
  static bool isHandledBoolConnective( TNode n );
106
  static bool isHandledUfTerm( TNode n );
107
  static Node getMatchOperator( QuantConflictFind * p, Node n );
108
  //can this node be handled by the algorithm
109
  static bool isHandled( TNode n );
110
};
111
112
//info for quantifiers
113
class QuantInfo {
114
private:
115
  void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );
116
  void flatten( Node n, bool beneathQuant );
117
private: //for completing match
118
  std::vector< int > d_unassigned;
119
  std::vector< TypeNode > d_unassigned_tn;
120
  int d_unassigned_nvar;
121
  int d_una_index;
122
  std::vector< int > d_una_eqc_count;
123
  //optimization: track which arguments variables appear under UF terms in
124
  std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom;
125
  void getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
126
  //optimization: number of variables set, to track when we can stop
127
  std::map< int, bool > d_vars_set;
128
  std::vector< Node > d_extra_var;
129
public:
130
  bool isBaseMatchComplete();
131
public:
132
  QuantInfo();
133
  ~QuantInfo();
134
  std::vector< TNode > d_vars;
135
  std::vector< TypeNode > d_var_types;
136
  std::map< TNode, int > d_var_num;
137
  std::vector< int > d_tsym_vars;
138
  std::map< TNode, bool > d_inMatchConstraint;
139
8545383
  int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
140
404148
  bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }
141
4664928
  int getNumVars() { return (int)d_vars.size(); }
142
406
  TNode getVar( int i ) { return d_vars[i]; }
143
144
  typedef std::map< int, MatchGen * > VarMgMap;
145
 private:
146
  MatchGen * d_mg;
147
  VarMgMap d_var_mg;
148
 public:
149
6510097
  VarMgMap::const_iterator var_mg_find(int i) const { return d_var_mg.find(i); }
150
5949217
  VarMgMap::const_iterator var_mg_end() const { return d_var_mg.end(); }
151
2267252
  bool containsVarMg(int i) const { return var_mg_find(i) != var_mg_end(); }
152
153
219569
  bool matchGeneratorIsValid() const { return d_mg->isValid(); }
154
617494
  bool getNextMatch( QuantConflictFind * p ) {
155
617494
    return d_mg->getNextMatch(p, this);
156
  }
157
158
  Node d_q;
159
  bool reset_round( QuantConflictFind * p );
160
public:
161
  //initialize
162
  void initialize( QuantConflictFind * p, Node q, Node qn );
163
  //current constraints
164
  std::vector< TNode > d_match;
165
  std::vector< TNode > d_match_term;
166
  std::map< int, std::map< TNode, int > > d_curr_var_deq;
167
  std::map< Node, bool > d_tconstraints;
168
  int getCurrentRepVar( int v );
169
  TNode getCurrentValue( TNode n );
170
  TNode getCurrentExpValue( TNode n );
171
  bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );
172
  int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );
173
  int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );
174
  bool setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep, bool isGround );
175
  void unsetMatch( QuantConflictFind * p, int v );
176
  bool isMatchSpurious( QuantConflictFind * p );
177
  bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
178
  bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
179
  bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
180
  void revertMatch( QuantConflictFind * p, std::vector< int >& assigned );
181
  void debugPrintMatch( const char * c );
182
  bool isConstrainedVar( int v );
183
public:
184
  void getMatch( std::vector< Node >& terms );
185
};
186
187
7208
class QuantConflictFind : public QuantifiersModule
188
{
189
  friend class MatchGen;
190
  friend class QuantInfo;
191
  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
192
private:
193
  context::CDO< bool > d_conflict;
194
  std::map< Kind, Node > d_zero;
195
  //for storing nodes created during t-constraint solving (prevents memory leaks)
196
  std::vector< Node > d_tempCache;
197
  //optimization: list of quantifiers that depend on ground function applications
198
  std::map< TNode, std::vector< Node > > d_func_rel_dom;
199
  std::map< TNode, bool > d_irr_func;
200
  std::map< Node, bool > d_irr_quant;
201
  void setIrrelevantFunction( TNode f );
202
private:
203
  std::map< Node, Node > d_op_node;
204
  std::map< Node, int > d_fid;
205
public:  //for ground terms
206
  Node d_true;
207
  Node d_false;
208
  TNode getZero( Kind k );
209
private:
210
  std::map< Node, QuantInfo > d_qinfo;
211
private:  //for equivalence classes
212
  // type -> list(eqc)
213
  std::map< TypeNode, std::vector< TNode > > d_eqcs;
214
215
 public:
216
  enum Effort : unsigned {
217
    EFFORT_CONFLICT,
218
    EFFORT_PROP_EQ,
219
    EFFORT_INVALID,
220
  };
221
  void setEffort(Effort e) { d_effort = e; }
222
223
3177204
  inline bool atConflictEffort() const {
224
3177204
    return d_effort == QuantConflictFind::EFFORT_CONFLICT;
225
  }
226
227
 private:
228
  Effort d_effort;
229
230
 public:
231
  bool areMatchEqual( TNode n1, TNode n2 );
232
  bool areMatchDisequal( TNode n1, TNode n2 );
233
234
 public:
235
  QuantConflictFind(QuantifiersEngine* qe,
236
                    QuantifiersState& qs,
237
                    QuantifiersInferenceManager& qim,
238
                    QuantifiersRegistry& qr);
239
240
  /** register quantifier */
241
  void registerQuantifier(Node q) override;
242
243
 public:
244
  /** needs check */
245
  bool needsCheck(Theory::Effort level) override;
246
  /** reset round */
247
  void reset_round(Theory::Effort level) override;
248
  /** check
249
   *
250
   * This method attempts to construct a conflicting or propagating instance.
251
   * If such an instance exists, then it makes a call to
252
   * Instantiation::addInstantiation.
253
   */
254
  void check(Theory::Effort level, QEffort quant_e) override;
255
256
 private:
257
  /** check quantified formula
258
   *
259
   * This method is called by the above check method for each quantified
260
   * formula q. It attempts to find a conflicting or propagating instance for
261
   * q, depending on the effort level (d_effort).
262
   *
263
   * isConflict: this is set to true if we discovered a conflicting instance.
264
   * This flag may be set instead of d_conflict if --qcf-all-conflict is true,
265
   * in which we continuing adding all conflicts.
266
   * addedLemmas: tracks the total number of lemmas added, and is incremented by
267
   * this method when applicable.
268
   */
269
  void checkQuantifiedFormula(Node q, bool& isConflict, unsigned& addedLemmas);
270
271
 private:
272
  void debugPrint( const char * c );
273
  //for debugging
274
  std::vector< Node > d_quants;
275
  std::map< Node, int > d_quant_id;
276
  void debugPrintQuant( const char * c, Node q );
277
  void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true );
278
public:
279
  /** statistics class */
280
  class Statistics {
281
  public:
282
    IntStat d_inst_rounds;
283
    IntStat d_entailment_checks;
284
    Statistics();
285
    ~Statistics();
286
  };
287
  Statistics d_statistics;
288
  /** Identify this module */
289
132763
  std::string identify() const override { return "QcfEngine"; }
290
  /** is n a propagating instance?
291
   *
292
   * A propagating instance is any formula that consists of Boolean connectives,
293
   * equality, quantified formulas, and terms that exist in the current
294
   * context (those in the master equality engine).
295
   *
296
   * Notice the distinction that quantified formulas that do not appear in the
297
   * current context are considered to be legal in propagating instances. This
298
   * choice is significant for TPTP, where a net of ~200 benchmarks are gained
299
   * due to this decision.
300
   *
301
   * Propagating instances are the second most useful kind of instantiation
302
   * after conflicting instances and are used as a second effort in the
303
   * algorithm performed by this class.
304
   */
305
  bool isPropagatingInstance(Node n) const;
306
};
307
308
std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);
309
310
} /* namespace CVC4::theory::quantifiers */
311
} /* namespace CVC4::theory */
312
} /* namespace CVC4 */
313
314
#endif