Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/query_generator.cpp	Lines:	2	223	0.9 %
Date:	2021-08-14	Branches:	2	674	0.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Gereon Kremer
 *
 * 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 a class for mining interesting satisfiability
 * queries from a stream of generated expressions.
 */

#include "theory/quantifiers/query_generator.h"

#include <fstream>
#include <sstream>

#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "util/random.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

QueryGenerator::QueryGenerator() : d_queryCount(0) {}
void QueryGenerator::initialize(const std::vector<Node>& vars, SygusSampler* ss)
{
  Assert(ss != nullptr);
  d_queryCount = 0;
  ExprMiner::initialize(vars, ss);
}

void QueryGenerator::setThreshold(unsigned deqThresh)
{
  d_deqThresh = deqThresh;
}

bool QueryGenerator::addTerm(Node n, std::ostream& out)
{
  Node nn = n.getKind() == NOT ? n[0] : n;
  if (d_terms.find(nn) != d_terms.end())
  {
    return false;
  }
  d_terms.insert(nn);

  Trace("sygus-qgen") << "QueryGenerator::addTerm : " << n << std::endl;
  unsigned npts = d_sampler->getNumSamplePoints();
  TypeNode tn = n.getType();
  // TODO : as an optimization, use a shared lazy trie?

  // the queries we generate on this round
  std::vector<Node> queries;
  // For each query in the above vector, this stores the indices of the points
  // for which that query evaluated to true on.
  std::vector<std::vector<unsigned>> queriesPtTrue;
  // the sample point indices for which the above queries are true
  std::unordered_set<unsigned> indices;

  // collect predicate queries (if n is Boolean)
  if (tn.isBoolean())
  {
    std::map<Node, std::vector<unsigned>> ev_to_pt;
    unsigned index = 0;
    unsigned threshCount = 0;
    while (index < npts && threshCount < 2)
    {
      Node v = d_sampler->evaluate(nn, index);
      ev_to_pt[v].push_back(index);
      if (ev_to_pt[v].size() == d_deqThresh + 1)
      {
        threshCount++;
      }
      index++;
    }
    if (threshCount < 2)
    {
      for (const auto& etp : ev_to_pt)
      {
        if (etp.second.size() < d_deqThresh)
        {
          indices.insert(etp.second.begin(), etp.second.end());
          Node qy = nn;
          Assert(etp.first.isConst());
          if (!etp.first.getConst<bool>())
          {
            qy = qy.negate();
          }
          queries.push_back(qy);
          queriesPtTrue.push_back(etp.second);
        }
      }
    }
  }

  // collect equality queries
  findQueries(nn, queries, queriesPtTrue);
  Assert(queries.size() == queriesPtTrue.size());
  if (queries.empty())
  {
    return true;
  }
  Trace("sygus-qgen-debug")
      << "query: Check " << queries.size() << " queries..." << std::endl;
  // literal queries
  for (unsigned i = 0, nqueries = queries.size(); i < nqueries; i++)
  {
    Node qy = queries[i];
    std::vector<unsigned>& tIndices = queriesPtTrue[i];
    // we have an interesting query
    out << "(query " << qy << ")  ; " << tIndices.size() << "/" << npts
        << std::endl;
    AlwaysAssert(!tIndices.empty());
    checkQuery(qy, tIndices[0]);
    // add information
    for (unsigned& ti : tIndices)
    {
      d_ptToQueries[ti].push_back(qy);
      d_qysToPoints[qy].push_back(ti);
      indices.insert(ti);
    }
  }
  // for each new index, we may have a new conjunctive query
  NodeManager* nm = NodeManager::currentNM();
  for (const unsigned& i : indices)
  {
    std::vector<Node>& qsi = d_ptToQueries[i];
    if (qsi.size() > 1)
    {
      // take two random queries
      std::shuffle(qsi.begin(), qsi.end(), Random::getRandom());
      Node qy = nm->mkNode(AND, qsi[0], qsi[1]);
      checkQuery(qy, i);
    }
  }
  Trace("sygus-qgen-check") << "...finished." << std::endl;
  return true;
}

void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
{
  // external query
  if (options::sygusQueryGenDumpFiles()
      == options::SygusQueryDumpFilesMode::ALL)
  {
    dumpQuery(qy, spIndex);
  }

  if (options::sygusQueryGenCheck())
  {
    Trace("sygus-qgen-check") << "  query: check " << qy << "..." << std::endl;
    // make the satisfiability query
    std::unique_ptr<SmtEngine> queryChecker;
    initializeChecker(queryChecker, qy);
    Result r = queryChecker->checkSat();
    Trace("sygus-qgen-check") << "  query: ...got : " << r << std::endl;
    if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
    {
      std::stringstream ss;
      ss << "--sygus-rr-query-gen detected unsoundness in cvc5 on input " << qy
         << "!" << std::endl;
      ss << "This query has a model : " << std::endl;
      std::vector<Node> pt;
      d_sampler->getSamplePoint(spIndex, pt);
      Assert(pt.size() == d_vars.size());
      for (unsigned i = 0, size = pt.size(); i < size; i++)
      {
        ss << "  " << d_vars[i] << " -> " << pt[i] << std::endl;
      }
      ss << "but cvc5 answered unsat!" << std::endl;
      AlwaysAssert(false) << ss.str();
    }
    if (options::sygusQueryGenDumpFiles()
        == options::SygusQueryDumpFilesMode::UNSOLVED)
    {
      if (r.asSatisfiabilityResult().isSat() != Result::SAT)
      {
        dumpQuery(qy, spIndex);
      }
    }
  }

  d_queryCount++;
}

void QueryGenerator::dumpQuery(Node qy, unsigned spIndex)
{
  // Print the query and the query + its model (commented) to queryN.smt2
  std::vector<Node> pt;
  d_sampler->getSamplePoint(spIndex, pt);
  size_t nvars = d_vars.size();
  AlwaysAssert(pt.size() == d_vars.size());
  std::stringstream fname;
  fname << "query" << d_queryCount << ".smt2";
  std::ofstream fs(fname.str(), std::ofstream::out);
  fs << "(set-logic ALL)" << std::endl;
  for (unsigned i = 0; i < 2; i++)
  {
    for (size_t j = 0; j < nvars; j++)
    {
      Node x = d_vars[j];
      if (i == 0)
      {
        fs << "(declare-fun " << x << " () " << x.getType() << ")";
      }
      else
      {
        fs << ";(define-fun " << x << " () " << x.getType() << " " << pt[j]
           << ")";
      }
      fs << std::endl;
    }
  }
  fs << "(assert " << qy << ")" << std::endl;
  fs << "(check-sat)" << std::endl;
  fs.close();
}

void QueryGenerator::findQueries(
    Node n,
    std::vector<Node>& queries,
    std::vector<std::vector<unsigned>>& queriesPtTrue)
{
  // At a high level, this method traverses the LazyTrie for the type of n
  // and tries to find paths to leafs that contain terms n' such that n = n'
  // or n != n' is an interesting query, i.e. satisfied for a small number of
  // points.
  TypeNode tn = n.getType();
  LazyTrie* lt = &d_qgtTrie[tn];
  // These vectors are the set of indices of sample points for which the current
  // node we are considering are { equal, disequal } from n.
  std::vector<unsigned> eqIndex[2];
  Trace("sygus-qgen-debug") << "Compute queries for " << n << "...\n";

  LazyTrieEvaluator* ev = d_sampler;
  unsigned ntotal = d_sampler->getNumSamplePoints();
  unsigned index = 0;
  bool exact = true;
  bool pushEq[2] = {false, false};
  bool pre = true;
  // The following parallel vectors describe the state of the locations in the
  // trie we are currently visiting.
  // Reference to the location in the trie
  std::vector<LazyTrie*> visitTr;
  // The index of the sample point we are testing
  std::vector<unsigned> currIndex;
  // Whether the path to this location exactly matches the evaluation of n
  std::vector<bool> currExact;
  // Whether we are adding to the points that are { equal, disequal } by
  // traversing to this location.
  std::vector<bool> pushIndex[2];
  // Whether we are in a pre-traversal for this location.
  std::vector<bool> preVisit;
  visitTr.push_back(lt);
  currIndex.push_back(0);
  currExact.push_back(true);
  pushIndex[0].push_back(false);
  pushIndex[1].push_back(false);
  preVisit.push_back(true);
  do
  {
    lt = visitTr.back();
    index = currIndex.back();
    exact = currExact.back();
    for (unsigned r = 0; r < 2; r++)
    {
      pushEq[r] = pushIndex[r].back();
    }
    pre = preVisit.back();
    if (!pre)
    {
      visitTr.pop_back();
      currIndex.pop_back();
      currExact.pop_back();
      preVisit.pop_back();
      // clean up the indices of points that are { equal, disequal }
      for (unsigned r = 0; r < 2; r++)
      {
        if (pushEq[r])
        {
          eqIndex[r].pop_back();
        }
        pushIndex[r].pop_back();
      }
    }
    else
    {
      preVisit[preVisit.size() - 1] = false;
      // add to the indices of points that are { equal, disequal }
      for (unsigned r = 0; r < 2; r++)
      {
        if (pushEq[r])
        {
          eqIndex[r].push_back(index - 1);
        }
      }
      int eqAllow = d_deqThresh - eqIndex[0].size();
      int deqAllow = d_deqThresh - eqIndex[1].size();
      Trace("sygus-qgen-debug")
          << "Find queries " << n << " " << index << "/" << ntotal
          << ", deq/eq allow = " << deqAllow << "/" << eqAllow
          << ", exact = " << exact << std::endl;
      if (index == ntotal)
      {
        if (exact)
        {
          // add to the trie
          lt->d_lazy_child = n;
        }
        else
        {
          Node nAlmostEq = lt->d_lazy_child;
          // if made it here, we still should have either a equality or
          // a disequality that is allowed.
          Assert(deqAllow >= 0 || eqAllow >= 0);
          Node query = n.eqNode(nAlmostEq);
          std::vector<unsigned> tIndices;
          if (eqAllow >= 0)
          {
            tIndices.insert(
                tIndices.end(), eqIndex[0].begin(), eqIndex[0].end());
          }
          else if (deqAllow >= 0)
          {
            query = query.negate();
            tIndices.insert(
                tIndices.end(), eqIndex[1].begin(), eqIndex[1].end());
          }
          AlwaysAssert(tIndices.size() <= d_deqThresh);
          if (!tIndices.empty())
          {
            queries.push_back(query);
            queriesPtTrue.push_back(tIndices);
          }
        }
      }
      else
      {
        if (!lt->d_lazy_child.isNull())
        {
          // if there is a lazy child here, push
          Node e_lc = ev->evaluate(lt->d_lazy_child, index);
          // store at next level
          lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
          // replace
          lt->d_lazy_child = Node::null();
        }
        // compute
        Node e_this = ev->evaluate(n, index);

        if (deqAllow >= 0)
        {
          // recursing on disequal points
          deqAllow--;
          // if there is use continuing
          if (deqAllow >= 0 || eqAllow >= 0)
          {
            for (std::pair<const Node, LazyTrie>& ltc : lt->d_children)
            {
              if (ltc.first != e_this)
              {
                visitTr.push_back(&ltc.second);
                currIndex.push_back(index + 1);
                currExact.push_back(false);
                pushIndex[0].push_back(false);
                pushIndex[1].push_back(true);
                preVisit.push_back(true);
              }
            }
          }
          deqAllow++;
        }
        bool pushEqNext = false;
        if (eqAllow >= 0)
        {
          // below, we try recursing (if at all) on equal nodes.
          eqAllow--;
          pushEqNext = true;
        }
        // if we are on the exact path of n
        if (exact)
        {
          if (lt->d_children.empty())
          {
            // if no one has been here before, we are done
            lt->d_lazy_child = n;
          }
          else
          {
            // otherwise, we recurse on the equal point
            visitTr.push_back(&(lt->d_children[e_this]));
            currIndex.push_back(index + 1);
            currExact.push_back(true);
            pushIndex[0].push_back(pushEqNext);
            pushIndex[1].push_back(false);
            preVisit.push_back(true);
          }
        }
        else if (deqAllow >= 0 || eqAllow >= 0)
        {
          // recurse on the equal point if it exists
          std::map<Node, LazyTrie>::iterator iteq = lt->d_children.find(e_this);
          if (iteq != lt->d_children.end())
          {
            visitTr.push_back(&(iteq->second));
            currIndex.push_back(index + 1);
            currExact.push_back(false);
            pushIndex[0].push_back(pushEqNext);
            pushIndex[1].push_back(false);
            preVisit.push_back(true);
          }
        }
      }
    }
  } while (!visitTr.empty());
}

}  // 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, Mathias Preiner, Gereon Kremer
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 a class for mining interesting satisfiability
14		* queries from a stream of generated expressions.
15		*/
16
17		#include "theory/quantifiers/query_generator.h"
18
19		#include <fstream>
20		#include <sstream>
21
22		#include "options/quantifiers_options.h"
23		#include "smt/smt_engine.h"
24		#include "smt/smt_engine_scope.h"
25		#include "util/random.h"
26
27		using namespace std;
28		using namespace cvc5::kind;
29
30		namespace cvc5 {
31		namespace theory {
32		namespace quantifiers {
33
34	9	QueryGenerator::QueryGenerator() : d_queryCount(0) {}
35		void QueryGenerator::initialize(const std::vector<Node>& vars, SygusSampler* ss)
36		{
37		Assert(ss != nullptr);
38		d_queryCount = 0;
39		ExprMiner::initialize(vars, ss);
40		}
41
42		void QueryGenerator::setThreshold(unsigned deqThresh)
43		{
44		d_deqThresh = deqThresh;
45		}
46
47		bool QueryGenerator::addTerm(Node n, std::ostream& out)
48		{
49		Node nn = n.getKind() == NOT ? n[0] : n;
50		if (d_terms.find(nn) != d_terms.end())
51		{
52		return false;
53		}
54		d_terms.insert(nn);
55
56		Trace("sygus-qgen") << "QueryGenerator::addTerm : " << n << std::endl;
57		unsigned npts = d_sampler->getNumSamplePoints();
58		TypeNode tn = n.getType();
59		// TODO : as an optimization, use a shared lazy trie?
60
61		// the queries we generate on this round
62		std::vector<Node> queries;
63		// For each query in the above vector, this stores the indices of the points
64		// for which that query evaluated to true on.
65		std::vector<std::vector<unsigned>> queriesPtTrue;
66		// the sample point indices for which the above queries are true
67		std::unordered_set<unsigned> indices;
68
69		// collect predicate queries (if n is Boolean)
70		if (tn.isBoolean())
71		{
72		std::map<Node, std::vector<unsigned>> ev_to_pt;
73		unsigned index = 0;
74		unsigned threshCount = 0;
75		while (index < npts && threshCount < 2)
76		{
77		Node v = d_sampler->evaluate(nn, index);
78		ev_to_pt[v].push_back(index);
79		if (ev_to_pt[v].size() == d_deqThresh + 1)
80		{
81		threshCount++;
82		}
83		index++;
84		}
85		if (threshCount < 2)
86		{
87		for (const auto& etp : ev_to_pt)
88		{
89		if (etp.second.size() < d_deqThresh)
90		{
91		indices.insert(etp.second.begin(), etp.second.end());
92		Node qy = nn;
93		Assert(etp.first.isConst());
94		if (!etp.first.getConst<bool>())
95		{
96		qy = qy.negate();
97		}
98		queries.push_back(qy);
99		queriesPtTrue.push_back(etp.second);
100		}
101		}
102		}
103		}
104
105		// collect equality queries
106		findQueries(nn, queries, queriesPtTrue);
107		Assert(queries.size() == queriesPtTrue.size());
108		if (queries.empty())
109		{
110		return true;
111		}
112		Trace("sygus-qgen-debug")
113		<< "query: Check " << queries.size() << " queries..." << std::endl;
114		// literal queries
115		for (unsigned i = 0, nqueries = queries.size(); i < nqueries; i++)
116		{
117		Node qy = queries[i];
118		std::vector<unsigned>& tIndices = queriesPtTrue[i];
119		// we have an interesting query
120		out << "(query " << qy << ") ; " << tIndices.size() << "/" << npts
121		<< std::endl;
122		AlwaysAssert(!tIndices.empty());
123		checkQuery(qy, tIndices[0]);
124		// add information
125		for (unsigned& ti : tIndices)
126		{
127		d_ptToQueries[ti].push_back(qy);
128		d_qysToPoints[qy].push_back(ti);
129		indices.insert(ti);
130		}
131		}
132		// for each new index, we may have a new conjunctive query
133		NodeManager* nm = NodeManager::currentNM();
134		for (const unsigned& i : indices)
135		{
136		std::vector<Node>& qsi = d_ptToQueries[i];
137		if (qsi.size() > 1)
138		{
139		// take two random queries
140		std::shuffle(qsi.begin(), qsi.end(), Random::getRandom());
141		Node qy = nm->mkNode(AND, qsi[0], qsi[1]);
142		checkQuery(qy, i);
143		}
144		}
145		Trace("sygus-qgen-check") << "...finished." << std::endl;
146		return true;
147		}
148
149		void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
150		{
151		// external query
152		if (options::sygusQueryGenDumpFiles()
153		== options::SygusQueryDumpFilesMode::ALL)
154		{
155		dumpQuery(qy, spIndex);
156		}
157
158		if (options::sygusQueryGenCheck())
159		{
160		Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl;
161		// make the satisfiability query
162		std::unique_ptr<SmtEngine> queryChecker;
163		initializeChecker(queryChecker, qy);
164		Result r = queryChecker->checkSat();
165		Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl;
166		if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
167		{
168		std::stringstream ss;
169		ss << "--sygus-rr-query-gen detected unsoundness in cvc5 on input " << qy
170		<< "!" << std::endl;
171		ss << "This query has a model : " << std::endl;
172		std::vector<Node> pt;
173		d_sampler->getSamplePoint(spIndex, pt);
174		Assert(pt.size() == d_vars.size());
175		for (unsigned i = 0, size = pt.size(); i < size; i++)
176		{
177		ss << " " << d_vars[i] << " -> " << pt[i] << std::endl;
178		}
179		ss << "but cvc5 answered unsat!" << std::endl;
180		AlwaysAssert(false) << ss.str();
181		}
182		if (options::sygusQueryGenDumpFiles()
183		== options::SygusQueryDumpFilesMode::UNSOLVED)
184		{
185		if (r.asSatisfiabilityResult().isSat() != Result::SAT)
186		{
187		dumpQuery(qy, spIndex);
188		}
189		}
190		}
191
192		d_queryCount++;
193		}
194
195		void QueryGenerator::dumpQuery(Node qy, unsigned spIndex)
196		{
197		// Print the query and the query + its model (commented) to queryN.smt2
198		std::vector<Node> pt;
199		d_sampler->getSamplePoint(spIndex, pt);
200		size_t nvars = d_vars.size();
201		AlwaysAssert(pt.size() == d_vars.size());
202		std::stringstream fname;
203		fname << "query" << d_queryCount << ".smt2";
204		std::ofstream fs(fname.str(), std::ofstream::out);
205		fs << "(set-logic ALL)" << std::endl;
206		for (unsigned i = 0; i < 2; i++)
207		{
208		for (size_t j = 0; j < nvars; j++)
209		{
210		Node x = d_vars[j];
211		if (i == 0)
212		{
213		fs << "(declare-fun " << x << " () " << x.getType() << ")";
214		}
215		else
216		{
217		fs << ";(define-fun " << x << " () " << x.getType() << " " << pt[j]
218		<< ")";
219		}
220		fs << std::endl;
221		}
222		}
223		fs << "(assert " << qy << ")" << std::endl;
224		fs << "(check-sat)" << std::endl;
225		fs.close();
226		}
227
228		void QueryGenerator::findQueries(
229		Node n,
230		std::vector<Node>& queries,
231		std::vector<std::vector<unsigned>>& queriesPtTrue)
232		{
233		// At a high level, this method traverses the LazyTrie for the type of n
234		// and tries to find paths to leafs that contain terms n' such that n = n'
235		// or n != n' is an interesting query, i.e. satisfied for a small number of
236		// points.
237		TypeNode tn = n.getType();
238		LazyTrie* lt = &d_qgtTrie[tn];
239		// These vectors are the set of indices of sample points for which the current
240		// node we are considering are { equal, disequal } from n.
241		std::vector<unsigned> eqIndex[2];
242		Trace("sygus-qgen-debug") << "Compute queries for " << n << "...\n";
243
244		LazyTrieEvaluator* ev = d_sampler;
245		unsigned ntotal = d_sampler->getNumSamplePoints();
246		unsigned index = 0;
247		bool exact = true;
248		bool pushEq[2] = {false, false};
249		bool pre = true;
250		// The following parallel vectors describe the state of the locations in the
251		// trie we are currently visiting.
252		// Reference to the location in the trie
253		std::vector<LazyTrie*> visitTr;
254		// The index of the sample point we are testing
255		std::vector<unsigned> currIndex;
256		// Whether the path to this location exactly matches the evaluation of n
257		std::vector<bool> currExact;
258		// Whether we are adding to the points that are { equal, disequal } by
259		// traversing to this location.
260		std::vector<bool> pushIndex[2];
261		// Whether we are in a pre-traversal for this location.
262		std::vector<bool> preVisit;
263		visitTr.push_back(lt);
264		currIndex.push_back(0);
265		currExact.push_back(true);
266		pushIndex[0].push_back(false);
267		pushIndex[1].push_back(false);
268		preVisit.push_back(true);
269		do
270		{
271		lt = visitTr.back();
272		index = currIndex.back();
273		exact = currExact.back();
274		for (unsigned r = 0; r < 2; r++)
275		{
276		pushEq[r] = pushIndex[r].back();
277		}
278		pre = preVisit.back();
279		if (!pre)
280		{
281		visitTr.pop_back();
282		currIndex.pop_back();
283		currExact.pop_back();
284		preVisit.pop_back();
285		// clean up the indices of points that are { equal, disequal }
286		for (unsigned r = 0; r < 2; r++)
287		{
288		if (pushEq[r])
289		{
290		eqIndex[r].pop_back();
291		}
292		pushIndex[r].pop_back();
293		}
294		}
295		else
296		{
297		preVisit[preVisit.size() - 1] = false;
298		// add to the indices of points that are { equal, disequal }
299		for (unsigned r = 0; r < 2; r++)
300		{
301		if (pushEq[r])
302		{
303		eqIndex[r].push_back(index - 1);
304		}
305		}
306		int eqAllow = d_deqThresh - eqIndex[0].size();
307		int deqAllow = d_deqThresh - eqIndex[1].size();
308		Trace("sygus-qgen-debug")
309		<< "Find queries " << n << " " << index << "/" << ntotal
310		<< ", deq/eq allow = " << deqAllow << "/" << eqAllow
311		<< ", exact = " << exact << std::endl;
312		if (index == ntotal)
313		{
314		if (exact)
315		{
316		// add to the trie
317		lt->d_lazy_child = n;
318		}
319		else
320		{
321		Node nAlmostEq = lt->d_lazy_child;
322		// if made it here, we still should have either a equality or
323		// a disequality that is allowed.
324		Assert(deqAllow >= 0 \|\| eqAllow >= 0);
325		Node query = n.eqNode(nAlmostEq);
326		std::vector<unsigned> tIndices;
327		if (eqAllow >= 0)
328		{
329		tIndices.insert(
330		tIndices.end(), eqIndex[0].begin(), eqIndex[0].end());
331		}
332		else if (deqAllow >= 0)
333		{
334		query = query.negate();
335		tIndices.insert(
336		tIndices.end(), eqIndex[1].begin(), eqIndex[1].end());
337		}
338		AlwaysAssert(tIndices.size() <= d_deqThresh);
339		if (!tIndices.empty())
340		{
341		queries.push_back(query);
342		queriesPtTrue.push_back(tIndices);
343		}
344		}
345		}
346		else
347		{
348		if (!lt->d_lazy_child.isNull())
349		{
350		// if there is a lazy child here, push
351		Node e_lc = ev->evaluate(lt->d_lazy_child, index);
352		// store at next level
353		lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
354		// replace
355		lt->d_lazy_child = Node::null();
356		}
357		// compute
358		Node e_this = ev->evaluate(n, index);
359
360		if (deqAllow >= 0)
361		{
362		// recursing on disequal points
363		deqAllow--;
364		// if there is use continuing
365		if (deqAllow >= 0 \|\| eqAllow >= 0)
366		{
367		for (std::pair<const Node, LazyTrie>& ltc : lt->d_children)
368		{
369		if (ltc.first != e_this)
370		{
371		visitTr.push_back(&ltc.second);
372		currIndex.push_back(index + 1);
373		currExact.push_back(false);
374		pushIndex[0].push_back(false);
375		pushIndex[1].push_back(true);
376		preVisit.push_back(true);
377		}
378		}
379		}
380		deqAllow++;
381		}
382		bool pushEqNext = false;
383		if (eqAllow >= 0)
384		{
385		// below, we try recursing (if at all) on equal nodes.
386		eqAllow--;
387		pushEqNext = true;
388		}
389		// if we are on the exact path of n
390		if (exact)
391		{
392		if (lt->d_children.empty())
393		{
394		// if no one has been here before, we are done
395		lt->d_lazy_child = n;
396		}
397		else
398		{
399		// otherwise, we recurse on the equal point
400		visitTr.push_back(&(lt->d_children[e_this]));
401		currIndex.push_back(index + 1);
402		currExact.push_back(true);
403		pushIndex[0].push_back(pushEqNext);
404		pushIndex[1].push_back(false);
405		preVisit.push_back(true);
406		}
407		}
408		else if (deqAllow >= 0 \|\| eqAllow >= 0)
409		{
410		// recurse on the equal point if it exists
411		std::map<Node, LazyTrie>::iterator iteq = lt->d_children.find(e_this);
412		if (iteq != lt->d_children.end())
413		{
414		visitTr.push_back(&(iteq->second));
415		currIndex.push_back(index + 1);
416		currExact.push_back(false);
417		pushIndex[0].push_back(pushEqNext);
418		pushIndex[1].push_back(false);
419		preVisit.push_back(true);
420		}
421		}
422		}
423		}
424		} while (!visitTr.empty());
425		}
426
427		} // namespace quantifiers
428		} // namespace theory
429	29340	} // namespace cvc5