Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/example_infer.cpp	Lines:	103	123	83.7 %
Date:	2021-09-19	Branches:	165	462	35.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, 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 utility for inferring whether a formula is in
 * examples form (functions applied to concrete arguments only).
 */
#include "theory/quantifiers/sygus/example_infer.h"

#include "theory/quantifiers/quant_util.h"

using namespace cvc5;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

ExampleInfer::ExampleInfer(TermDbSygus* tds) : d_tds(tds)
{
  d_isExamples = false;
}

ExampleInfer::~ExampleInfer() {}

bool ExampleInfer::initialize(Node n, const std::vector<Node>& candidates)
{
  Trace("ex-infer") << "Initialize example inference : " << n << std::endl;

  for (const Node& v : candidates)
  {
    d_examples[v].clear();
    d_examplesOut[v].clear();
    d_examplesTerm[v].clear();
  }
  std::map<std::pair<bool, bool>, std::unordered_set<Node>> visited;
  // n is negated conjecture
  if (!collectExamples(n, visited, true, false))
  {
    Trace("ex-infer") << "...conflicting examples" << std::endl;
    return false;
  }

  if (Trace.isOn("ex-infer"))
  {
    for (unsigned i = 0; i < candidates.size(); i++)
    {
      Node v = candidates[i];
      Trace("ex-infer") << "  examples for " << v << " : ";
      if (d_examples_invalid.find(v) != d_examples_invalid.end())
      {
        Trace("ex-infer") << "INVALID" << std::endl;
      }
      else
      {
        Trace("ex-infer") << std::endl;
        for (unsigned j = 0; j < d_examples[v].size(); j++)
        {
          Trace("ex-infer") << "    ";
          for (unsigned k = 0; k < d_examples[v][j].size(); k++)
          {
            Trace("ex-infer") << d_examples[v][j][k] << " ";
          }
          if (!d_examplesOut[v][j].isNull())
          {
            Trace("ex-infer") << " -> " << d_examplesOut[v][j];
          }
          Trace("ex-infer") << std::endl;
        }
      }
      Trace("ex-infer") << "Initialize " << d_examples[v].size()
                        << " example points for " << v << "..." << std::endl;
    }
  }
  return true;
}

bool ExampleInfer::collectExamples(
    Node n,
    std::map<std::pair<bool, bool>, std::unordered_set<Node>>& visited,
    bool hasPol,
    bool pol)
{
  std::pair<bool, bool> cacheIndex = std::pair<bool, bool>(hasPol, pol);
  if (visited[cacheIndex].find(n) != visited[cacheIndex].end())
  {
    // already visited
    return true;
  }
  visited[cacheIndex].insert(n);
  NodeManager* nm = NodeManager::currentNM();
  Node neval;
  Node n_output;
  bool neval_is_evalapp = false;
  if (n.getKind() == DT_SYGUS_EVAL)
  {
    neval = n;
    if (hasPol)
    {
      n_output = nm->mkConst(pol);
    }
    neval_is_evalapp = true;
  }
  else if (n.getKind() == EQUAL && hasPol && pol)
  {
    for (unsigned r = 0; r < 2; r++)
    {
      if (n[r].getKind() == DT_SYGUS_EVAL)
      {
        neval = n[r];
        if (n[1 - r].isConst())
        {
          n_output = n[1 - r];
        }
        neval_is_evalapp = true;
        break;
      }
    }
  }
  // is it an evaluation function?
  if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
  {
    Trace("ex-infer-debug")
        << "Process head: " << n << " == " << n_output << std::endl;
    // If n_output is null, then neval does not have a constant value
    // If n_output is non-null, then neval is constrained to always be
    // that value.
    if (!n_output.isNull())
    {
      std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
      if (itet == d_exampleTermMap.end())
      {
        d_exampleTermMap[neval] = n_output;
      }
      else if (itet->second != n_output)
      {
        // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
        // the conjecture is infeasible.
        return false;
      }
    }
    // get the evaluation head
    Node eh = neval[0];
    std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
    if (itx == d_examples_invalid.end())
    {
      // have we already processed this as an example term?
      if (std::find(d_examplesTerm[eh].begin(), d_examplesTerm[eh].end(), neval)
          == d_examplesTerm[eh].end())
      {
        // collect example
        bool success = true;
        std::vector<Node> ex;
        for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
        {
          if (!neval[j].isConst())
          {
            success = false;
            break;
          }
          ex.push_back(neval[j]);
        }
        if (success)
        {
          d_examples[eh].push_back(ex);
          d_examplesOut[eh].push_back(n_output);
          d_examplesTerm[eh].push_back(neval);
          if (n_output.isNull())
          {
            d_examplesOut_invalid[eh] = true;
          }
          else
          {
            Assert(n_output.isConst());
            // finished processing this node if it was an I/O pair
            return true;
          }
        }
        else
        {
          d_examples_invalid[eh] = true;
          d_examplesOut_invalid[eh] = true;
        }
      }
    }
  }
  for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
  {
    bool newHasPol;
    bool newPol;
    QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
    if (!collectExamples(n[i], visited, newHasPol, newPol))
    {
      return false;
    }
  }
  return true;
}

bool ExampleInfer::hasExamples(Node f) const
{
  std::map<Node, bool>::const_iterator itx = d_examples_invalid.find(f);
  if (itx == d_examples_invalid.end())
  {
    return d_examples.find(f) != d_examples.end();
  }
  return false;
}

unsigned ExampleInfer::getNumExamples(Node f) const
{
  std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
      d_examples.find(f);
  if (it != d_examples.end())
  {
    return it->second.size();
  }
  return 0;
}

void ExampleInfer::getExample(Node f, unsigned i, std::vector<Node>& ex) const
{
  Assert(!f.isNull());
  std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
      d_examples.find(f);
  if (it != d_examples.end())
  {
    Assert(i < it->second.size());
    ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
  }
  else
  {
    Assert(false);
  }
}

void ExampleInfer::getExampleTerms(Node f, std::vector<Node>& exTerms) const
{
  std::map<Node, std::vector<Node>>::const_iterator itt =
      d_examplesTerm.find(f);
  if (itt == d_examplesTerm.end())
  {
    return;
  }
  exTerms.insert(exTerms.end(), itt->second.begin(), itt->second.end());
}

Node ExampleInfer::getExampleOut(Node f, unsigned i) const
{
  Assert(!f.isNull());
  std::map<Node, std::vector<Node>>::const_iterator it = d_examplesOut.find(f);
  if (it != d_examplesOut.end())
  {
    Assert(i < it->second.size());
    return it->second[i];
  }
  Assert(false);
  return Node::null();
}

bool ExampleInfer::hasExamplesOut(Node f) const
{
  return d_examplesOut_invalid.find(f) == d_examplesOut_invalid.end();
}

}  // 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, Haniel Barbosa, 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 utility for inferring whether a formula is in
14		* examples form (functions applied to concrete arguments only).
15		*/
16		#include "theory/quantifiers/sygus/example_infer.h"
17
18		#include "theory/quantifiers/quant_util.h"
19
20		using namespace cvc5;
21		using namespace cvc5::kind;
22
23		namespace cvc5 {
24		namespace theory {
25		namespace quantifiers {
26
27	1233	ExampleInfer::ExampleInfer(TermDbSygus* tds) : d_tds(tds)
28		{
29	1233	d_isExamples = false;
30	1233	}
31
32	1231	ExampleInfer::~ExampleInfer() {}
33
34	332	bool ExampleInfer::initialize(Node n, const std::vector<Node>& candidates)
35		{
36	332	Trace("ex-infer") << "Initialize example inference : " << n << std::endl;
37
38	895	for (const Node& v : candidates)
39		{
40	563	d_examples[v].clear();
41	563	d_examplesOut[v].clear();
42	563	d_examplesTerm[v].clear();
43		}
44	664	std::map<std::pair<bool, bool>, std::unordered_set<Node>> visited;
45		// n is negated conjecture
46	332	if (!collectExamples(n, visited, true, false))
47		{
48	2	Trace("ex-infer") << "...conflicting examples" << std::endl;
49	2	return false;
50		}
51
52	330	if (Trace.isOn("ex-infer"))
53		{
54		for (unsigned i = 0; i < candidates.size(); i++)
55		{
56		Node v = candidates[i];
57		Trace("ex-infer") << " examples for " << v << " : ";
58		if (d_examples_invalid.find(v) != d_examples_invalid.end())
59		{
60		Trace("ex-infer") << "INVALID" << std::endl;
61		}
62		else
63		{
64		Trace("ex-infer") << std::endl;
65		for (unsigned j = 0; j < d_examples[v].size(); j++)
66		{
67		Trace("ex-infer") << " ";
68		for (unsigned k = 0; k < d_examples[v][j].size(); k++)
69		{
70		Trace("ex-infer") << d_examples[v][j][k] << " ";
71		}
72		if (!d_examplesOut[v][j].isNull())
73		{
74		Trace("ex-infer") << " -> " << d_examplesOut[v][j];
75		}
76		Trace("ex-infer") << std::endl;
77		}
78		}
79		Trace("ex-infer") << "Initialize " << d_examples[v].size()
80		<< " example points for " << v << "..." << std::endl;
81		}
82		}
83	330	return true;
84		}
85
86	20516	bool ExampleInfer::collectExamples(
87		Node n,
88		std::map<std::pair<bool, bool>, std::unordered_set<Node>>& visited,
89		bool hasPol,
90		bool pol)
91		{
92	20516	std::pair<bool, bool> cacheIndex = std::pair<bool, bool>(hasPol, pol);
93	20516	if (visited[cacheIndex].find(n) != visited[cacheIndex].end())
94		{
95		// already visited
96	9237	return true;
97		}
98	11279	visited[cacheIndex].insert(n);
99	11279	NodeManager* nm = NodeManager::currentNM();
100	22558	Node neval;
101	22558	Node n_output;
102	11279	bool neval_is_evalapp = false;
103	11279	if (n.getKind() == DT_SYGUS_EVAL)
104		{
105	624	neval = n;
106	624	if (hasPol)
107		{
108	43	n_output = nm->mkConst(pol);
109		}
110	624	neval_is_evalapp = true;
111		}
112	10655	else if (n.getKind() == EQUAL && hasPol && pol)
113		{
114	677	for (unsigned r = 0; r < 2; r++)
115		{
116	648	if (n[r].getKind() == DT_SYGUS_EVAL)
117		{
118	437	neval = n[r];
119	437	if (n[1 - r].isConst())
120		{
121	420	n_output = n[1 - r];
122		}
123	437	neval_is_evalapp = true;
124	437	break;
125		}
126		}
127		}
128		// is it an evaluation function?
129	11279	if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
130		{
131	2122	Trace("ex-infer-debug")
132	1061	<< "Process head: " << n << " == " << n_output << std::endl;
133		// If n_output is null, then neval does not have a constant value
134		// If n_output is non-null, then neval is constrained to always be
135		// that value.
136	1061	if (!n_output.isNull())
137		{
138	463	std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
139	463	if (itet == d_exampleTermMap.end())
140		{
141	461	d_exampleTermMap[neval] = n_output;
142		}
143	2	else if (itet->second != n_output)
144		{
145		// We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
146		// the conjecture is infeasible.
147	2	return false;
148		}
149		}
150		// get the evaluation head
151	1669	Node eh = neval[0];
152	1059	std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
153	1059	if (itx == d_examples_invalid.end())
154		{
155		// have we already processed this as an example term?
156	2733	if (std::find(d_examplesTerm[eh].begin(), d_examplesTerm[eh].end(), neval)
157	2733	== d_examplesTerm[eh].end())
158		{
159		// collect example
160	891	bool success = true;
161	1333	std::vector<Node> ex;
162	1781	for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
163		{
164	1212	if (!neval[j].isConst())
165		{
166	322	success = false;
167	322	break;
168		}
169	890	ex.push_back(neval[j]);
170		}
171	891	if (success)
172		{
173	569	d_examples[eh].push_back(ex);
174	569	d_examplesOut[eh].push_back(n_output);
175	569	d_examplesTerm[eh].push_back(neval);
176	569	if (n_output.isNull())
177		{
178	120	d_examplesOut_invalid[eh] = true;
179		}
180		else
181		{
182	449	Assert(n_output.isConst());
183		// finished processing this node if it was an I/O pair
184	449	return true;
185		}
186		}
187		else
188		{
189	322	d_examples_invalid[eh] = true;
190	322	d_examplesOut_invalid[eh] = true;
191		}
192		}
193		}
194		}
195	31008	for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
196		{
197		bool newHasPol;
198		bool newPol;
199	20184	QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
200	20184	if (!collectExamples(n[i], visited, newHasPol, newPol))
201		{
202	4	return false;
203		}
204		}
205	10824	return true;
206		}
207
208	426	bool ExampleInfer::hasExamples(Node f) const
209		{
210	426	std::map<Node, bool>::const_iterator itx = d_examples_invalid.find(f);
211	426	if (itx == d_examples_invalid.end())
212		{
213	298	return d_examples.find(f) != d_examples.end();
214		}
215	128	return false;
216		}
217
218	540	unsigned ExampleInfer::getNumExamples(Node f) const
219		{
220		std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
221	540	d_examples.find(f);
222	540	if (it != d_examples.end())
223		{
224	540	return it->second.size();
225		}
226		return 0;
227		}
228
229	958	void ExampleInfer::getExample(Node f, unsigned i, std::vector<Node>& ex) const
230		{
231	958	Assert(!f.isNull());
232		std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
233	958	d_examples.find(f);
234	958	if (it != d_examples.end())
235		{
236	958	Assert(i < it->second.size());
237	958	ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
238		}
239		else
240		{
241		Assert(false);
242		}
243	958	}
244
245	2218	void ExampleInfer::getExampleTerms(Node f, std::vector<Node>& exTerms) const
246		{
247		std::map<Node, std::vector<Node>>::const_iterator itt =
248	2218	d_examplesTerm.find(f);
249	2218	if (itt == d_examplesTerm.end())
250		{
251		return;
252		}
253	2218	exTerms.insert(exTerms.end(), itt->second.begin(), itt->second.end());
254		}
255
256	388	Node ExampleInfer::getExampleOut(Node f, unsigned i) const
257		{
258	388	Assert(!f.isNull());
259	388	std::map<Node, std::vector<Node>>::const_iterator it = d_examplesOut.find(f);
260	388	if (it != d_examplesOut.end())
261		{
262	388	Assert(i < it->second.size());
263	388	return it->second[i];
264		}
265		Assert(false);
266		return Node::null();
267		}
268
269	87	bool ExampleInfer::hasExamplesOut(Node f) const
270		{
271	87	return d_examplesOut_invalid.find(f) == d_examplesOut_invalid.end();
272		}
273
274		} // namespace quantifiers
275		} // namespace theory
276	29577	} // namespace cvc5