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