Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/candidate_generator.cpp	Lines:	175	185	94.6 %
Date:	2021-09-29	Branches:	326	782	41.7 %


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