Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/candidate_generator.cpp	Lines:	177	185	95.7 %
Date:	2021-05-22	Branches:	335	794	42.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of theory uf candidate generator class.
 */

#include "theory/quantifiers/ematching/candidate_generator.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {
namespace inst {

CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr)
    : d_qs(qs), d_treg(tr)
{
}

bool CandidateGenerator::isLegalCandidate( Node n ){
  return d_treg.getTermDatabase()->isTermActive(n)
         && (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n));
}

CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs,
                                           TermRegistry& tr,
                                           Node pat)
    : CandidateGenerator(qs, tr),
      d_term_iter(-1),
      d_term_iter_limit(0),
      d_mode(cand_term_none)
{
  d_op = d_treg.getTermDatabase()->getMatchOperator(pat);
  Assert(!d_op.isNull());
}

void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); }

void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
{
  d_term_iter = 0;
  d_eqc = eqc;
  d_op = op;
  d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op);
  if( eqc.isNull() ){
    d_mode = cand_term_db;
  }else{
    if( isExcludedEqc( eqc ) ){
      d_mode = cand_term_none;
    }else{
      eq::EqualityEngine* ee = d_qs.getEqualityEngine();
      if( ee->hasTerm( eqc ) ){
        TNodeTrie* tat = d_treg.getTermDatabase()->getTermArgTrie(eqc, op);
        if( tat ){
          //create an equivalence class iterator in eq class eqc
          Node rep = ee->getRepresentative( eqc );
          d_eqc_iter = eq::EqClassIterator( rep, ee );
          d_mode = cand_term_eqc;
        }else{
          d_mode = cand_term_none;
        }
      }else{
        //the only match is this term itself
        d_mode = cand_term_ident;
      }
    }
  }
}
bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
  if( n.hasOperator() ){
    if( isLegalCandidate( n ) ){
      return d_treg.getTermDatabase()->getMatchOperator(n) == d_op;
    }
  }
  return false;
}

Node CandidateGeneratorQE::getNextCandidate(){
  return getNextCandidateInternal();
}

Node CandidateGeneratorQE::getNextCandidateInternal()
{
  if( d_mode==cand_term_db ){
    Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
    //get next candidate term in the uf term database
    while( d_term_iter<d_term_iter_limit ){
      Node n = d_treg.getTermDatabase()->getGroundTerm(d_op, d_term_iter);
      d_term_iter++;
      if( isLegalCandidate( n ) ){
        if (d_treg.getTermDatabase()->hasTermCurrent(n))
        {
          if( d_exclude_eqc.empty() ){
            return n;
          }else{
            Node r = d_qs.getRepresentative(n);
            if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
              Debug("cand-gen-qe") << "...returning " << n << std::endl;
              return n;
            }
          }
        }
      }
    }
  }else if( d_mode==cand_term_eqc ){
    Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl;
    while( !d_eqc_iter.isFinished() ){
      Node n = *d_eqc_iter;
      ++d_eqc_iter;
      if( isLegalOpCandidate( n ) ){
        Debug("cand-gen-qe") << "...returning " << n << std::endl;
        return n;
      }
    }
  }else if( d_mode==cand_term_ident ){
    Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
    if (!d_eqc.isNull())
    {
      Node n = d_eqc;
      d_eqc = Node::null();
      if( isLegalOpCandidate( n ) ){
        return n;
      }
    }
  }
  return Node::null();
}

CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(QuantifiersState& qs,
                                                       TermRegistry& tr,
                                                       Node mpat)
    : CandidateGenerator(qs, tr), d_match_pattern(mpat)
{
  Assert(d_match_pattern.getKind() == EQUAL);
  d_match_pattern_type = d_match_pattern[0].getType();
}

void CandidateGeneratorQELitDeq::reset( Node eqc ){
  eq::EqualityEngine* ee = d_qs.getEqualityEngine();
  Node falset = NodeManager::currentNM()->mkConst(false);
  d_eqc_false = eq::EqClassIterator(falset, ee);
}

Node CandidateGeneratorQELitDeq::getNextCandidate(){
  //get next candidate term in equivalence class
  while( !d_eqc_false.isFinished() ){
    Node n = (*d_eqc_false);
    ++d_eqc_false;
    if( n.getKind()==d_match_pattern.getKind() ){
      if (n[0].getType().isComparableTo(d_match_pattern_type)
          && isLegalCandidate(n))
      {
        //found an iff or equality, try to match it
        //DO_THIS: cache to avoid redundancies?
        //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
        return n;
      }
    }
  }
  return Node::null();
}

CandidateGeneratorQEAll::CandidateGeneratorQEAll(QuantifiersState& qs,
                                                 TermRegistry& tr,
                                                 Node mpat)
    : CandidateGenerator(qs, tr), d_match_pattern(mpat)
{
  d_match_pattern_type = mpat.getType();
  Assert(mpat.getKind() == INST_CONSTANT);
  d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
  d_index = mpat.getAttribute(InstVarNumAttribute());
  d_firstTime = false;
}

void CandidateGeneratorQEAll::reset( Node eqc ) {
  d_eq = eq::EqClassesIterator(d_qs.getEqualityEngine());
  d_firstTime = true;
}

Node CandidateGeneratorQEAll::getNextCandidate() {
  quantifiers::TermDb* tdb = d_treg.getTermDatabase();
  while( !d_eq.isFinished() ){
    TNode n = (*d_eq);
    ++d_eq;
    if( n.getType().isComparableTo( d_match_pattern_type ) ){
      TNode nh = tdb->getEligibleTermInEqc(n);
      if( !nh.isNull() ){
        if (options::instMaxLevel() != -1)
        {
          nh = d_treg.getModel()->getInternalRepresentative(nh, d_f, d_index);
          //don't consider this if already the instantiation is ineligible
          if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
          {
            nh = Node::null();
          }
        }
        if( !nh.isNull() ){
          d_firstTime = false;
          //an equivalence class with the same type as the pattern, return it
          return nh;
        }
      }
    }
  }
  if( d_firstTime ){
    //must return something
    d_firstTime = false;
    return d_treg.getTermForType(d_match_pattern_type);
  }
  return Node::null();
}

CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs,
                                                           TermRegistry& tr,
                                                           Node mpat)
    : CandidateGeneratorQE(qs, tr, mpat)
{
  Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
  d_mpat_type = mpat.getType();
}

void CandidateGeneratorConsExpand::reset(Node eqc)
{
  d_term_iter = 0;
  if (eqc.isNull())
  {
    d_mode = cand_term_db;
  }
  else
  {
    d_eqc = eqc;
    d_mode = cand_term_ident;
    Assert(d_eqc.getType() == d_mpat_type);
  }
}

Node CandidateGeneratorConsExpand::getNextCandidate()
{
  // get the next term from the base class
  Node curr = getNextCandidateInternal();
  if (curr.isNull() || (curr.hasOperator() && curr.getOperator() == d_op))
  {
    return curr;
  }
  // expand it
  NodeManager* nm = NodeManager::currentNM();
  std::vector<Node> children;
  const DType& dt = d_mpat_type.getDType();
  Assert(dt.getNumConstructors() == 1);
  children.push_back(d_op);
  for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
  {
    Node sel = nm->mkNode(
        APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
    children.push_back(sel);
  }
  return nm->mkNode(APPLY_CONSTRUCTOR, children);
}

bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n)
{
  return isLegalCandidate(n);
}

CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
                                                       TermRegistry& tr,
                                                       Node mpat)
    : CandidateGeneratorQE(qs, tr, mpat)
{
  Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
  Assert(mpat.getKind() == APPLY_SELECTOR);
  // NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when
  // expand definitions is eliminated, however, this also requires avoiding
  // term formula removal.
  Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat);
  Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
  if (mpatExp.getKind() == ITE)
  {
    Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
    Assert(mpatExp[2].getKind() == APPLY_UF);
    d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
    d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]);
  }
  else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL)
  {
    // corner case of datatype with one constructor
    d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
  }
  else
  {
    // corner case of a wrongly applied selector as a trigger
    Assert(mpatExp.getKind() == APPLY_UF);
    d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
  }
  Assert(d_selOp != d_ufOp);
}

void CandidateGeneratorSelector::reset(Node eqc)
{
  Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl;
  // start with d_selOp, if it exists
  resetForOperator(eqc, !d_selOp.isNull()? d_selOp : d_ufOp);
}

Node CandidateGeneratorSelector::getNextCandidate()
{
  Node nextc = getNextCandidateInternal();
  if (!nextc.isNull())
  {
    Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl;
    return nextc;
  }
  else if (d_op == d_selOp)
  {
    if (d_ufOp.isNull())
    {
      // corner case: selector cannot be wrongly applied (1-cons case)
      d_op = Node::null();
    }
    else
    {
      // finished correctly applied selectors, now try incorrectly applied ones
      resetForOperator(d_eqc, d_ufOp);
      return getNextCandidate();
    }
  }
  Trace("sel-trigger-debug") << "...finished" << std::endl;
  // no more candidates
  return Node::null();
}

}  // namespace inst
}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* Implementation of theory uf candidate generator class.
14		*/
15
16		#include "theory/quantifiers/ematching/candidate_generator.h"
17		#include "expr/dtype.h"
18		#include "expr/dtype_cons.h"
19		#include "options/quantifiers_options.h"
20		#include "smt/smt_engine.h"
21		#include "smt/smt_engine_scope.h"
22		#include "theory/quantifiers/first_order_model.h"
23		#include "theory/quantifiers/quantifiers_state.h"
24		#include "theory/quantifiers/term_database.h"
25		#include "theory/quantifiers/term_registry.h"
26		#include "theory/quantifiers/term_util.h"
27
28		using namespace cvc5::kind;
29
30		namespace cvc5 {
31		namespace theory {
32		namespace quantifiers {
33		namespace inst {
34
35	36152	CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr)
36	36152	: d_qs(qs), d_treg(tr)
37		{
38	36152	}
39
40	3707153	bool CandidateGenerator::isLegalCandidate( Node n ){
41	11121459	return d_treg.getTermDatabase()->isTermActive(n)
42	14828612	&& (!options::cegqi() \|\| !quantifiers::TermUtil::hasInstConstAttr(n));
43		}
44
45	36074	CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs,
46		TermRegistry& tr,
47	36074	Node pat)
48		: CandidateGenerator(qs, tr),
49		d_term_iter(-1),
50		d_term_iter_limit(0),
51	36074	d_mode(cand_term_none)
52		{
53	36074	d_op = d_treg.getTermDatabase()->getMatchOperator(pat);
54	36074	Assert(!d_op.isNull());
55	36074	}
56
57	545128	void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); }
58
59	548530	void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
60		{
61	548530	d_term_iter = 0;
62	548530	d_eqc = eqc;
63	548530	d_op = op;
64	548530	d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op);
65	548530	if( eqc.isNull() ){
66	119826	d_mode = cand_term_db;
67		}else{
68	428704	if( isExcludedEqc( eqc ) ){
69		d_mode = cand_term_none;
70		}else{
71	428704	eq::EqualityEngine* ee = d_qs.getEqualityEngine();
72	428704	if( ee->hasTerm( eqc ) ){
73	428704	TNodeTrie* tat = d_treg.getTermDatabase()->getTermArgTrie(eqc, op);
74	428704	if( tat ){
75		//create an equivalence class iterator in eq class eqc
76	359732	Node rep = ee->getRepresentative( eqc );
77	179866	d_eqc_iter = eq::EqClassIterator( rep, ee );
78	179866	d_mode = cand_term_eqc;
79		}else{
80	248838	d_mode = cand_term_none;
81		}
82		}else{
83		//the only match is this term itself
84		d_mode = cand_term_ident;
85		}
86		}
87		}
88	548530	}
89	913058	bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
90	913058	if( n.hasOperator() ){
91	638001	if( isLegalCandidate( n ) ){
92	362357	return d_treg.getTermDatabase()->getMatchOperator(n) == d_op;
93		}
94		}
95	550701	return false;
96		}
97
98	3334678	Node CandidateGeneratorQE::getNextCandidate(){
99	3334678	return getNextCandidateInternal();
100		}
101
102	3344215	Node CandidateGeneratorQE::getNextCandidateInternal()
103		{
104	3344215	if( d_mode==cand_term_db ){
105	2711812	Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
106		//get next candidate term in the uf term database
107	3585586	while( d_term_iter<d_term_iter_limit ){
108	3504072	Node n = d_treg.getTermDatabase()->getGroundTerm(d_op, d_term_iter);
109	3067185	d_term_iter++;
110	3067185	if( isLegalCandidate( n ) ){
111	2653993	if (d_treg.getTermDatabase()->hasTermCurrent(n))
112		{
113	2653993	if( d_exclude_eqc.empty() ){
114	2560983	return n;
115		}else{
116	116705	Node r = d_qs.getRepresentative(n);
117	93010	if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
118	69315	Debug("cand-gen-qe") << "...returning " << n << std::endl;
119	69315	return n;
120		}
121		}
122		}
123		}
124		}
125	632403	}else if( d_mode==cand_term_eqc ){
126	380711	Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl;
127	1630289	while( !d_eqc_iter.isFinished() ){
128	1537847	Node n = *d_eqc_iter;
129	913058	++d_eqc_iter;
130	913058	if( isLegalOpCandidate( n ) ){
131	288269	Debug("cand-gen-qe") << "...returning " << n << std::endl;
132	288269	return n;
133		}
134		}
135	251692	}else if( d_mode==cand_term_ident ){
136	2854	Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
137	2854	if (!d_eqc.isNull())
138		{
139	2018	Node n = d_eqc;
140	1927	d_eqc = Node::null();
141	1927	if( isLegalOpCandidate( n ) ){
142	1836	return n;
143		}
144		}
145		}
146	423812	return Node::null();
147		}
148
149	7	CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(QuantifiersState& qs,
150		TermRegistry& tr,
151	7	Node mpat)
152	7	: CandidateGenerator(qs, tr), d_match_pattern(mpat)
153		{
154	7	Assert(d_match_pattern.getKind() == EQUAL);
155	7	d_match_pattern_type = d_match_pattern[0].getType();
156	7	}
157
158	34	void CandidateGeneratorQELitDeq::reset( Node eqc ){
159	34	eq::EqualityEngine* ee = d_qs.getEqualityEngine();
160	68	Node falset = NodeManager::currentNM()->mkConst(false);
161	34	d_eqc_false = eq::EqClassIterator(falset, ee);
162	34	}
163
164	112	Node CandidateGeneratorQELitDeq::getNextCandidate(){
165		//get next candidate term in equivalence class
166	169	while( !d_eqc_false.isFinished() ){
167	154	Node n = (*d_eqc_false);
168	97	++d_eqc_false;
169	97	if( n.getKind()==d_match_pattern.getKind() ){
170	252	if (n[0].getType().isComparableTo(d_match_pattern_type)
171	252	&& isLegalCandidate(n))
172		{
173		//found an iff or equality, try to match it
174		//DO_THIS: cache to avoid redundancies?
175		//DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false?
176	40	return n;
177		}
178		}
179		}
180	15	return Node::null();
181		}
182
183	71	CandidateGeneratorQEAll::CandidateGeneratorQEAll(QuantifiersState& qs,
184		TermRegistry& tr,
185	71	Node mpat)
186	71	: CandidateGenerator(qs, tr), d_match_pattern(mpat)
187		{
188	71	d_match_pattern_type = mpat.getType();
189	71	Assert(mpat.getKind() == INST_CONSTANT);
190	71	d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
191	71	d_index = mpat.getAttribute(InstVarNumAttribute());
192	71	d_firstTime = false;
193	71	}
194
195	177	void CandidateGeneratorQEAll::reset( Node eqc ) {
196	177	d_eq = eq::EqClassesIterator(d_qs.getEqualityEngine());
197	177	d_firstTime = true;
198	177	}
199
200	279	Node CandidateGeneratorQEAll::getNextCandidate() {
201	279	quantifiers::TermDb* tdb = d_treg.getTermDatabase();
202	4659	while( !d_eq.isFinished() ){
203	4556	TNode n = (*d_eq);
204	2366	++d_eq;
205	2366	if( n.getType().isComparableTo( d_match_pattern_type ) ){
206	176	TNode nh = tdb->getEligibleTermInEqc(n);
207	176	if( !nh.isNull() ){
208	176	if (options::instMaxLevel() != -1)
209		{
210		nh = d_treg.getModel()->getInternalRepresentative(nh, d_f, d_index);
211		//don't consider this if already the instantiation is ineligible
212		if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
213		{
214		nh = Node::null();
215		}
216		}
217	176	if( !nh.isNull() ){
218	176	d_firstTime = false;
219		//an equivalence class with the same type as the pattern, return it
220	176	return nh;
221		}
222		}
223		}
224		}
225	103	if( d_firstTime ){
226		//must return something
227	24	d_firstTime = false;
228	24	return d_treg.getTermForType(d_match_pattern_type);
229		}
230	79	return Node::null();
231		}
232
233	2911	CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs,
234		TermRegistry& tr,
235	2911	Node mpat)
236	2911	: CandidateGeneratorQE(qs, tr, mpat)
237		{
238	2911	Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
239	2911	d_mpat_type = mpat.getType();
240	2911	}
241
242	4283	void CandidateGeneratorConsExpand::reset(Node eqc)
243		{
244	4283	d_term_iter = 0;
245	4283	if (eqc.isNull())
246		{
247	2356	d_mode = cand_term_db;
248		}
249		else
250		{
251	1927	d_eqc = eqc;
252	1927	d_mode = cand_term_ident;
253	1927	Assert(d_eqc.getType() == d_mpat_type);
254		}
255	4283	}
256
257	5210	Node CandidateGeneratorConsExpand::getNextCandidate()
258		{
259		// get the next term from the base class
260	10420	Node curr = getNextCandidateInternal();
261	5210	if (curr.isNull() \|\| (curr.hasOperator() && curr.getOperator() == d_op))
262		{
263	3944	return curr;
264		}
265		// expand it
266	1266	NodeManager* nm = NodeManager::currentNM();
267	2532	std::vector<Node> children;
268	1266	const DType& dt = d_mpat_type.getDType();
269	1266	Assert(dt.getNumConstructors() == 1);
270	1266	children.push_back(d_op);
271	3830	for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
272		{
273		Node sel = nm->mkNode(
274	5128	APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
275	2564	children.push_back(sel);
276		}
277	1266	return nm->mkNode(APPLY_CONSTRUCTOR, children);
278		}
279
280	1927	bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n)
281		{
282	1927	return isLegalCandidate(n);
283		}
284
285	165	CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
286		TermRegistry& tr,
287	165	Node mpat)
288	165	: CandidateGeneratorQE(qs, tr, mpat)
289		{
290	165	Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
291	165	Assert(mpat.getKind() == APPLY_SELECTOR);
292		// NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when
293		// expand definitions is eliminated, however, this also requires avoiding
294		// term formula removal.
295	330	Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat);
296	165	Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
297	165	if (mpatExp.getKind() == ITE)
298		{
299	164	Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
300	164	Assert(mpatExp[2].getKind() == APPLY_UF);
301	164	d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
302	164	d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]);
303		}
304	1	else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL)
305		{
306		// corner case of datatype with one constructor
307	1	d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
308		}
309		else
310		{
311		// corner case of a wrongly applied selector as a trigger
312		Assert(mpatExp.getKind() == APPLY_UF);
313		d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
314		}
315	165	Assert(d_selOp != d_ufOp);
316	165	}
317
318	1994	void CandidateGeneratorSelector::reset(Node eqc)
319		{
320	1994	Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl;
321		// start with d_selOp, if it exists
322	1994	resetForOperator(eqc, !d_selOp.isNull()? d_selOp : d_ufOp);
323	1994	}
324
325	4327	Node CandidateGeneratorSelector::getNextCandidate()
326		{
327	8654	Node nextc = getNextCandidateInternal();
328	4327	if (!nextc.isNull())
329		{
330	1533	Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl;
331	1533	return nextc;
332		}
333	2794	else if (d_op == d_selOp)
334		{
335	1408	if (d_ufOp.isNull())
336		{
337		// corner case: selector cannot be wrongly applied (1-cons case)
338		d_op = Node::null();
339		}
340		else
341		{
342		// finished correctly applied selectors, now try incorrectly applied ones
343	1408	resetForOperator(d_eqc, d_ufOp);
344	1408	return getNextCandidate();
345		}
346		}
347	1386	Trace("sel-trigger-debug") << "...finished" << std::endl;
348		// no more candidates
349	1386	return Node::null();
350		}
351
352		} // namespace inst
353		} // namespace quantifiers
354		} // namespace theory
355	28194	} // namespace cvc5