Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/candidate_generator.cpp	Lines:	178	185	96.2 %
Date:	2021-08-04	Branches:	338	794	42.6 %


/******************************************************************************
 * 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	34731	CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr)
36	34731	: d_qs(qs), d_treg(tr)
37		{
38	34731	}
39
40	3307900	bool CandidateGenerator::isLegalCandidate( Node n ){
41	9923700	return d_treg.getTermDatabase()->isTermActive(n)
42	13231600	&& (!options::cegqi() \|\| !quantifiers::TermUtil::hasInstConstAttr(n));
43		}
44
45	34653	CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs,
46		TermRegistry& tr,
47	34653	Node pat)
48		: CandidateGenerator(qs, tr),
49		d_term_iter(-1),
50		d_term_iter_limit(0),
51	34653	d_mode(cand_term_none)
52		{
53	34653	d_op = d_treg.getTermDatabase()->getMatchOperator(pat);
54	34653	Assert(!d_op.isNull());
55	34653	}
56
57	446266	void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); }
58
59	458965	void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
60		{
61	458965	d_term_iter = 0;
62	458965	d_eqc = eqc;
63	458965	d_op = op;
64	458965	d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op);
65	458965	if( eqc.isNull() ){
66	116985	d_mode = cand_term_db;
67		}else{
68	341980	if( isExcludedEqc( eqc ) ){
69		d_mode = cand_term_none;
70		}else{
71	341980	eq::EqualityEngine* ee = d_qs.getEqualityEngine();
72	341980	if( ee->hasTerm( eqc ) ){
73	341980	TNodeTrie* tat = d_treg.getTermDatabase()->getTermArgTrie(eqc, op);
74	341980	if( tat ){
75		//create an equivalence class iterator in eq class eqc
76	292940	Node rep = ee->getRepresentative( eqc );
77	146470	d_eqc_iter = eq::EqClassIterator( rep, ee );
78	146470	d_mode = cand_term_eqc;
79		}else{
80	195510	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	458965	}
89	352650	bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
90	352650	if( n.hasOperator() ){
91	307819	if( isLegalCandidate( n ) ){
92	246102	return d_treg.getTermDatabase()->getMatchOperator(n) == d_op;
93		}
94		}
95	106548	return false;
96		}
97
98	3062389	Node CandidateGeneratorQE::getNextCandidate(){
99	3062389	return getNextCandidateInternal();
100		}
101
102	3089920	Node CandidateGeneratorQE::getNextCandidateInternal()
103		{
104	3089920	if( d_mode==cand_term_db ){
105	2652236	Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
106		//get next candidate term in the uf term database
107	3504708	while( d_term_iter<d_term_iter_limit ){
108	3424350	Node n = d_treg.getTermDatabase()->getGroundTerm(d_op, d_term_iter);
109	2998114	d_term_iter++;
110	2998114	if( isLegalCandidate( n ) ){
111	2595933	if (d_treg.getTermDatabase()->hasTermCurrent(n))
112		{
113	2595933	if( d_exclude_eqc.empty() ){
114	2501886	return n;
115		}else{
116	118102	Node r = d_qs.getRepresentative(n);
117	94047	if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
118	69992	Debug("cand-gen-qe") << "...returning " << n << std::endl;
119	69992	return n;
120		}
121		}
122		}
123		}
124		}
125	437684	}else if( d_mode==cand_term_eqc ){
126	239320	Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl;
127	617386	while( !d_eqc_iter.isFinished() ){
128	541683	Node n = *d_eqc_iter;
129	352650	++d_eqc_iter;
130	352650	if( isLegalOpCandidate( n ) ){
131	163617	Debug("cand-gen-qe") << "...returning " << n << std::endl;
132	163617	return n;
133		}
134		}
135	198364	}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	352589	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	221	CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
286		TermRegistry& tr,
287	221	Node mpat)
288	221	: CandidateGeneratorQE(qs, tr, mpat)
289		{
290	221	Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
291	221	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	442	Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat);
296	221	Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
297	221	if (mpatExp.getKind() == ITE)
298		{
299	209	Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
300	209	Assert(mpatExp[2].getKind() == APPLY_UF);
301	209	d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
302	209	d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]);
303		}
304	12	else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL)
305		{
306		// corner case of datatype with one constructor
307	12	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	221	Assert(d_selOp != d_ufOp);
316	221	}
317
318	8127	void CandidateGeneratorSelector::reset(Node eqc)
319		{
320	8127	Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl;
321		// start with d_selOp, if it exists
322	8127	resetForOperator(eqc, !d_selOp.isNull()? d_selOp : d_ufOp);
323	8127	}
324
325	22321	Node CandidateGeneratorSelector::getNextCandidate()
326		{
327	44642	Node nextc = getNextCandidateInternal();
328	22321	if (!nextc.isNull())
329		{
330	13302	Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl;
331	13302	return nextc;
332		}
333	9019	else if (d_op == d_selOp)
334		{
335	4590	if (d_ufOp.isNull())
336		{
337		// corner case: selector cannot be wrongly applied (1-cons case)
338	18	d_op = Node::null();
339		}
340		else
341		{
342		// finished correctly applied selectors, now try incorrectly applied ones
343	4572	resetForOperator(d_eqc, d_ufOp);
344	4572	return getNextCandidate();
345		}
346		}
347	4447	Trace("sel-trigger-debug") << "...finished" << std::endl;
348		// no more candidates
349	4447	return Node::null();
350		}
351
352		} // namespace inst
353		} // namespace quantifiers
354		} // namespace theory
355	29286	} // namespace cvc5