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-10	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	35091	CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr)
38	35091	: d_qs(qs), d_treg(tr)
39		{
40	35091	}
41
42	3322754	bool CandidateGenerator::isLegalCandidate( Node n ){
43	9968262	return d_treg.getTermDatabase()->isTermActive(n)
44	13291016	&& (!options::cegqi() \|\| !quantifiers::TermUtil::hasInstConstAttr(n));
45		}
46
47	35013	CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs,
48		TermRegistry& tr,
49	35013	Node pat)
50		: CandidateGenerator(qs, tr),
51		d_term_iter(-1),
52		d_term_iter_limit(0),
53	35013	d_mode(cand_term_none)
54		{
55	35013	d_op = d_treg.getTermDatabase()->getMatchOperator(pat);
56	35013	Assert(!d_op.isNull());
57	35013	}
58
59	452693	void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); }
60
61	462862	void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
62		{
63	462862	d_term_iter = 0;
64	462862	d_eqc = eqc;
65	462862	d_op = op;
66	462862	d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op);
67	462862	if( eqc.isNull() ){
68	118118	d_mode = cand_term_db;
69		}else{
70	344744	if( isExcludedEqc( eqc ) ){
71		d_mode = cand_term_none;
72		}else{
73	344744	eq::EqualityEngine* ee = d_qs.getEqualityEngine();
74	344744	if( ee->hasTerm( eqc ) ){
75	344744	TNodeTrie* tat = d_treg.getTermDatabase()->getTermArgTrie(eqc, op);
76	344744	if( tat ){
77		//create an equivalence class iterator in eq class eqc
78	291366	Node rep = ee->getRepresentative( eqc );
79	145683	d_eqc_iter = eq::EqClassIterator( rep, ee );
80	145683	d_mode = cand_term_eqc;
81		}else{
82	199061	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	462862	}
91	363964	bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
92	363964	if( n.hasOperator() ){
93	324027	if( isLegalCandidate( n ) ){
94	245316	return d_treg.getTermDatabase()->getMatchOperator(n) == d_op;
95		}
96		}
97	118648	return false;
98		}
99
100	3069384	Node CandidateGeneratorQE::getNextCandidate(){
101	3069384	return getNextCandidateInternal();
102		}
103
104	3088578	Node CandidateGeneratorQE::getNextCandidateInternal()
105		{
106	3088578	if( d_mode==cand_term_db ){
107	2653434	Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
108		//get next candidate term in the uf term database
109	3503160	while( d_term_iter<d_term_iter_limit ){
110	3421502	Node n = d_treg.getTermDatabase()->getGroundTerm(d_op, d_term_iter);
111	2996639	d_term_iter++;
112	2996639	if( isLegalCandidate( n ) ){
113	2595694	if (d_treg.getTermDatabase()->hasTermCurrent(n))
114		{
115	2595694	if( d_exclude_eqc.empty() ){
116	2501222	return n;
117		}else{
118	118390	Node r = d_qs.getRepresentative(n);
119	94472	if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
120	70554	Debug("cand-gen-qe") << "...returning " << n << std::endl;
121	70554	return n;
122		}
123		}
124		}
125		}
126		}
127	435144	}else if( d_mode==cand_term_eqc ){
128	233022	Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl;
129	645300	while( !d_eqc_iter.isFinished() ){
130	570103	Node n = *d_eqc_iter;
131	363964	++d_eqc_iter;
132	363964	if( isLegalOpCandidate( n ) ){
133	157825	Debug("cand-gen-qe") << "...returning " << n << std::endl;
134	157825	return n;
135		}
136		}
137	202122	}else if( d_mode==cand_term_ident ){
138	3061	Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
139	3061	if (!d_eqc.isNull())
140		{
141	2139	Node n = d_eqc;
142	2048	d_eqc = Node::null();
143	2048	if( isLegalOpCandidate( n ) ){
144	1957	return n;
145		}
146		}
147		}
148	357020	return Node::null();
149		}
150
151	7	CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(QuantifiersState& qs,
152		TermRegistry& tr,
153	7	Node mpat)
154	7	: CandidateGenerator(qs, tr), d_match_pattern(mpat)
155		{
156	7	Assert(d_match_pattern.getKind() == EQUAL);
157	7	d_match_pattern_type = d_match_pattern[0].getType();
158	7	}
159
160	34	void CandidateGeneratorQELitDeq::reset( Node eqc ){
161	34	eq::EqualityEngine* ee = d_qs.getEqualityEngine();
162	68	Node falset = NodeManager::currentNM()->mkConst(false);
163	34	d_eqc_false = eq::EqClassIterator(falset, ee);
164	34	}
165
166	112	Node CandidateGeneratorQELitDeq::getNextCandidate(){
167		//get next candidate term in equivalence class
168	169	while( !d_eqc_false.isFinished() ){
169	154	Node n = (*d_eqc_false);
170	97	++d_eqc_false;
171	97	if( n.getKind()==d_match_pattern.getKind() ){
172	252	if (n[0].getType().isComparableTo(d_match_pattern_type)
173	252	&& 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	40	return n;
179		}
180		}
181		}
182	15	return Node::null();
183		}
184
185	71	CandidateGeneratorQEAll::CandidateGeneratorQEAll(QuantifiersState& qs,
186		TermRegistry& tr,
187	71	Node mpat)
188	71	: CandidateGenerator(qs, tr), d_match_pattern(mpat)
189		{
190	71	d_match_pattern_type = mpat.getType();
191	71	Assert(mpat.getKind() == INST_CONSTANT);
192	71	d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
193	71	d_index = mpat.getAttribute(InstVarNumAttribute());
194	71	d_firstTime = false;
195	71	}
196
197	177	void CandidateGeneratorQEAll::reset( Node eqc ) {
198	177	d_eq = eq::EqClassesIterator(d_qs.getEqualityEngine());
199	177	d_firstTime = true;
200	177	}
201
202	279	Node CandidateGeneratorQEAll::getNextCandidate() {
203	279	quantifiers::TermDb* tdb = d_treg.getTermDatabase();
204	4659	while( !d_eq.isFinished() ){
205	4556	TNode n = (*d_eq);
206	2366	++d_eq;
207	2366	if( n.getType().isComparableTo( d_match_pattern_type ) ){
208	176	TNode nh = tdb->getEligibleTermInEqc(n);
209	176	if( !nh.isNull() ){
210	176	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	176	if( !nh.isNull() ){
220	176	d_firstTime = false;
221		//an equivalence class with the same type as the pattern, return it
222	176	return nh;
223		}
224		}
225		}
226		}
227	103	if( d_firstTime ){
228		//must return something
229	24	d_firstTime = false;
230	24	return d_treg.getTermForType(d_match_pattern_type);
231		}
232	79	return Node::null();
233		}
234
235	3017	CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs,
236		TermRegistry& tr,
237	3017	Node mpat)
238	3017	: CandidateGeneratorQE(qs, tr, mpat)
239		{
240	3017	Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
241	3017	d_mpat_type = mpat.getType();
242	3017	}
243
244	4113	void CandidateGeneratorConsExpand::reset(Node eqc)
245		{
246	4113	d_term_iter = 0;
247	4113	if (eqc.isNull())
248		{
249	2065	d_mode = cand_term_db;
250		}
251		else
252		{
253	2048	d_eqc = eqc;
254	2048	d_mode = cand_term_ident;
255	2048	Assert(d_eqc.getType() == d_mpat_type);
256		}
257	4113	}
258
259	5126	Node CandidateGeneratorConsExpand::getNextCandidate()
260		{
261		// get the next term from the base class
262	10252	Node curr = getNextCandidateInternal();
263	5126	if (curr.isNull() \|\| (curr.hasOperator() && curr.getOperator() == d_op))
264		{
265	3804	return curr;
266		}
267		// expand it
268	1322	NodeManager* nm = NodeManager::currentNM();
269	2644	std::vector<Node> children;
270	1322	const DType& dt = d_mpat_type.getDType();
271	1322	Assert(dt.getNumConstructors() == 1);
272	1322	children.push_back(d_op);
273	3998	for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
274		{
275		Node sel = nm->mkNode(
276	5352	APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
277	2676	children.push_back(sel);
278		}
279	1322	return nm->mkNode(APPLY_CONSTRUCTOR, children);
280		}
281
282	2048	bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n)
283		{
284	2048	return isLegalCandidate(n);
285		}
286
287	258	CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
288		TermRegistry& tr,
289	258	Node mpat)
290	258	: CandidateGeneratorQE(qs, tr, mpat)
291		{
292	258	Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
293	258	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	516	Node mpatExp = datatypes::DatatypesRewriter::expandApplySelector(mpat);
298	258	Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
299	258	if (mpatExp.getKind() == ITE)
300		{
301	258	Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
302	258	Assert(mpatExp[2].getKind() == APPLY_UF);
303	258	d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
304	258	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	258	Assert(d_selOp != d_ufOp);
318	258	}
319
320	6194	void CandidateGeneratorSelector::reset(Node eqc)
321		{
322	6194	Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl;
323		// start with d_selOp, if it exists
324	6194	resetForOperator(eqc, !d_selOp.isNull()? d_selOp : d_ufOp);
325	6194	}
326
327	14068	Node CandidateGeneratorSelector::getNextCandidate()
328		{
329	28136	Node nextc = getNextCandidateInternal();
330	14068	if (!nextc.isNull())
331		{
332	6242	Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl;
333	6242	return nextc;
334		}
335	7826	else if (d_op == d_selOp)
336		{
337	3975	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	3975	resetForOperator(d_eqc, d_ufOp);
346	3975	return getNextCandidate();
347		}
348		}
349	3851	Trace("sel-trigger-debug") << "...finished" << std::endl;
350		// no more candidates
351	3851	return Node::null();
352		}
353
354		} // namespace inst
355		} // namespace quantifiers
356		} // namespace theory
357	29502	} // namespace cvc5