Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_pbe.cpp	Lines:	122	123	99.2 %
Date:	2021-11-07	Branches:	224	512	43.8 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Utility for processing programming by examples synthesis conjectures.
 */
#include "theory/quantifiers/sygus/sygus_pbe.h"

#include "options/quantifiers_options.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/sygus/example_infer.h"
#include "theory/quantifiers/sygus/sygus_unif_io.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "util/random.h"

using namespace cvc5;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

SygusPbe::SygusPbe(Env& env,
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   TermDbSygus* tds,
                   SynthConjecture* p)
    : SygusModule(env, qs, qim, tds, p)
{
  d_true = NodeManager::currentNM()->mkConst(true);
  d_false = NodeManager::currentNM()->mkConst(false);
  d_is_pbe = false;
}

SygusPbe::~SygusPbe() {}

bool SygusPbe::initialize(Node conj,
                          Node n,
                          const std::vector<Node>& candidates)
{
  Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
  NodeManager* nm = NodeManager::currentNM();

  if (!options::sygusUnifPbe())
  {
    // we are not doing unification
    return false;
  }

  // check if all candidates are valid examples
  ExampleInfer* ei = d_parent->getExampleInfer();
  d_is_pbe = true;
  for (const Node& c : candidates)
  {
    // if it has no examples or the output of the examples is invalid
    if (ei->getNumExamples(c) == 0 || !ei->hasExamplesOut(c))
    {
      d_is_pbe = false;
      return false;
    }
  }
  for (const Node& c : candidates)
  {
    Assert(ei->hasExamples(c));
    d_sygus_unif[c].reset(new SygusUnifIo(d_env, d_parent));
    Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
                       << std::endl;
    std::map<Node, std::vector<Node>> strategy_lemmas;
    d_sygus_unif[c]->initializeCandidate(
        d_tds, c, d_candidate_to_enum[c], strategy_lemmas);
    Assert(!d_candidate_to_enum[c].empty());
    Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
                       << " enumerators for " << c << "..." << std::endl;
    // collect list per type of strategy points with strategy lemmas
    std::map<TypeNode, std::vector<Node>> tn_to_strategy_pt;
    for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
    {
      TypeNode tnsp = p.first.getType();
      tn_to_strategy_pt[tnsp].push_back(p.first);
    }
    // initialize the enumerators
    for (const Node& e : d_candidate_to_enum[c])
    {
      TypeNode etn = e.getType();
      d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL);
      d_enum_to_candidate[e] = c;
      TNode te = e;
      // initialize static symmetry breaking lemmas for it
      // we register only one "master" enumerator per type
      // thus, the strategy lemmas (which are for individual strategy points)
      // are applicable (disjunctively) to the master enumerator
      std::map<TypeNode, std::vector<Node>>::iterator itt =
          tn_to_strategy_pt.find(etn);
      if (itt != tn_to_strategy_pt.end())
      {
        std::vector<Node> disj;
        for (const Node& sp : itt->second)
        {
          std::map<Node, std::vector<Node>>::iterator itsl =
              strategy_lemmas.find(sp);
          Assert(itsl != strategy_lemmas.end());
          if (!itsl->second.empty())
          {
            TNode tsp = sp;
            Node lem = itsl->second.size() == 1 ? itsl->second[0]
                                                : nm->mkNode(AND, itsl->second);
            if (tsp != te)
            {
              lem = lem.substitute(tsp, te);
            }
            if (std::find(disj.begin(), disj.end(), lem) == disj.end())
            {
              disj.push_back(lem);
            }
          }
        }
        // add its active guard
        Node ag = d_tds->getActiveGuardForEnumerator(e);
        Assert(!ag.isNull());
        disj.push_back(ag.negate());
        Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
        // Apply extended rewriting on the lemma. This helps utilities like
        // SygusEnumerator more easily recognize the shape of this lemma, e.g.
        // ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x).
        lem = extendedRewrite(lem);
        Trace("sygus-pbe") << "  static redundant op lemma : " << lem
                           << std::endl;
        // Register as a symmetry breaking lemma with the term database.
        // This will either be processed via a lemma on the output channel
        // of the sygus extension of the datatypes solver, or internally
        // encoded as a constraint to an active enumerator.
        d_tds->registerSymBreakLemma(e, lem, etn, 0, false);
      }
    }
  }
  return true;
}

// ------------------------------------------- solution construction from enumeration

void SygusPbe::getTermList(const std::vector<Node>& candidates,
                           std::vector<Node>& terms)
{
  for( unsigned i=0; i<candidates.size(); i++ ){
    Node v = candidates[i];
    std::map<Node, std::vector<Node> >::iterator it =
        d_candidate_to_enum.find(v);
    if (it != d_candidate_to_enum.end())
    {
      terms.insert(terms.end(), it->second.begin(), it->second.end());
    }
  }
}

bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); }

bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
                                   const std::vector<Node>& enum_values,
                                   const std::vector<Node>& candidates,
                                   std::vector<Node>& candidate_values)
{
  Assert(enums.size() == enum_values.size());
  if( !enums.empty() ){
    unsigned min_term_size = 0;
    Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
    std::vector<unsigned> szs;
    for (unsigned i = 0, esize = enums.size(); i < esize; i++)
    {
      Trace("sygus-pbe-enum") << "  " << enums[i] << " -> ";
      TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
      Trace("sygus-pbe-enum") << std::endl;
      if (!enum_values[i].isNull())
      {
        unsigned sz = datatypes::utils::getSygusTermSize(enum_values[i]);
        szs.push_back(sz);
        if (i == 0 || sz < min_term_size)
        {
          min_term_size = sz;
        }
      }
      else
      {
        szs.push_back(0);
      }
    }
    // Assume two enumerators of types T1 and T2.
    // If options::sygusPbeMultiFair() is true,
    // we ensure that all values of type T1 and size n are enumerated before
    // any term of type T2 of size n+d, and vice versa, where d is
    // set by options::sygusPbeMultiFairDiff(). If d is zero, then our
    // enumeration is such that all terms of T1 or T2 of size n are considered
    // before any term of size n+1.
    int diffAllow = options::sygusPbeMultiFairDiff();
    std::vector<unsigned> enum_consider;
    for (unsigned i = 0, esize = enums.size(); i < esize; i++)
    {
      if (!enum_values[i].isNull())
      {
        Assert(szs[i] >= min_term_size);
        int diff = szs[i] - min_term_size;
        if (!options::sygusPbeMultiFair() || diff <= diffAllow)
        {
          enum_consider.push_back(i);
        }
      }
    }

    // only consider the enumerators that are at minimum size (for fairness)
    Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl;
    NodeManager* nm = NodeManager::currentNM();
    for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; i++)
    {
      unsigned j = enum_consider[i];
      Node e = enums[j];
      Node v = enum_values[j];
      Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end());
      Node c = d_enum_to_candidate[e];
      std::vector<Node> enum_lems;
      d_sygus_unif[c]->notifyEnumeration(e, v, enum_lems);
      if (!enum_lems.empty())
      {
        // the lemmas must be guarded by the active guard of the enumerator
        Node g = d_tds->getActiveGuardForEnumerator(e);
        Assert(!g.isNull());
        for (unsigned k = 0, size = enum_lems.size(); k < size; k++)
        {
          Node lem = nm->mkNode(OR, g.negate(), enum_lems[k]);
          d_qim.addPendingLemma(lem,
                                InferenceId::QUANTIFIERS_SYGUS_PBE_EXCLUDE);
        }
      }
    }
  }
  for( unsigned i=0; i<candidates.size(); i++ ){
    Node c = candidates[i];
    //build decision tree for candidate
    std::vector<Node> sol;
    std::vector<Node> lems;
    bool solSuccess = d_sygus_unif[c]->constructSolution(sol, lems);
    for (const Node& lem : lems)
    {
      d_qim.addPendingLemma(lem,
                            InferenceId::QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL);
    }
    if (solSuccess)
    {
      Assert(sol.size() == 1);
      candidate_values.push_back(sol[0]);
    }
    else
    {
      return false;
    }
  }
  return true;
}

}
}
}  // 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		* Utility for processing programming by examples synthesis conjectures.
14		*/
15		#include "theory/quantifiers/sygus/sygus_pbe.h"
16
17		#include "options/quantifiers_options.h"
18		#include "theory/datatypes/sygus_datatype_utils.h"
19		#include "theory/quantifiers/sygus/example_infer.h"
20		#include "theory/quantifiers/sygus/sygus_unif_io.h"
21		#include "theory/quantifiers/sygus/synth_conjecture.h"
22		#include "theory/quantifiers/sygus/term_database_sygus.h"
23		#include "theory/quantifiers/term_util.h"
24		#include "util/random.h"
25
26		using namespace cvc5;
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace quantifiers {
32
33	1900	SygusPbe::SygusPbe(Env& env,
34		QuantifiersState& qs,
35		QuantifiersInferenceManager& qim,
36		TermDbSygus* tds,
37	1900	SynthConjecture* p)
38	1900	: SygusModule(env, qs, qim, tds, p)
39		{
40	1900	d_true = NodeManager::currentNM()->mkConst(true);
41	1900	d_false = NodeManager::currentNM()->mkConst(false);
42	1900	d_is_pbe = false;
43	1900	}
44
45	3792	SygusPbe::~SygusPbe() {}
46
47	409	bool SygusPbe::initialize(Node conj,
48		Node n,
49		const std::vector<Node>& candidates)
50		{
51	409	Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
52	409	NodeManager* nm = NodeManager::currentNM();
53
54	409	if (!options::sygusUnifPbe())
55		{
56		// we are not doing unification
57	68	return false;
58		}
59
60		// check if all candidates are valid examples
61	341	ExampleInfer* ei = d_parent->getExampleInfer();
62	341	d_is_pbe = true;
63	425	for (const Node& c : candidates)
64		{
65		// if it has no examples or the output of the examples is invalid
66	346	if (ei->getNumExamples(c) == 0 \|\| !ei->hasExamplesOut(c))
67		{
68	262	d_is_pbe = false;
69	262	return false;
70		}
71		}
72	163	for (const Node& c : candidates)
73		{
74	84	Assert(ei->hasExamples(c));
75	84	d_sygus_unif[c].reset(new SygusUnifIo(d_env, d_parent));
76	168	Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
77	84	<< std::endl;
78	168	std::map<Node, std::vector<Node>> strategy_lemmas;
79	168	d_sygus_unif[c]->initializeCandidate(
80	84	d_tds, c, d_candidate_to_enum[c], strategy_lemmas);
81	84	Assert(!d_candidate_to_enum[c].empty());
82	168	Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
83	84	<< " enumerators for " << c << "..." << std::endl;
84		// collect list per type of strategy points with strategy lemmas
85	168	std::map<TypeNode, std::vector<Node>> tn_to_strategy_pt;
86	181	for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
87		{
88	194	TypeNode tnsp = p.first.getType();
89	97	tn_to_strategy_pt[tnsp].push_back(p.first);
90		}
91		// initialize the enumerators
92	198	for (const Node& e : d_candidate_to_enum[c])
93		{
94	228	TypeNode etn = e.getType();
95	114	d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL);
96	114	d_enum_to_candidate[e] = c;
97	228	TNode te = e;
98		// initialize static symmetry breaking lemmas for it
99		// we register only one "master" enumerator per type
100		// thus, the strategy lemmas (which are for individual strategy points)
101		// are applicable (disjunctively) to the master enumerator
102		std::map<TypeNode, std::vector<Node>>::iterator itt =
103	114	tn_to_strategy_pt.find(etn);
104	114	if (itt != tn_to_strategy_pt.end())
105		{
106	126	std::vector<Node> disj;
107	156	for (const Node& sp : itt->second)
108		{
109		std::map<Node, std::vector<Node>>::iterator itsl =
110	93	strategy_lemmas.find(sp);
111	93	Assert(itsl != strategy_lemmas.end());
112	93	if (!itsl->second.empty())
113		{
114	186	TNode tsp = sp;
115	174	Node lem = itsl->second.size() == 1 ? itsl->second[0]
116	267	: nm->mkNode(AND, itsl->second);
117	93	if (tsp != te)
118		{
119	30	lem = lem.substitute(tsp, te);
120		}
121	93	if (std::find(disj.begin(), disj.end(), lem) == disj.end())
122		{
123	67	disj.push_back(lem);
124		}
125		}
126		}
127		// add its active guard
128	126	Node ag = d_tds->getActiveGuardForEnumerator(e);
129	63	Assert(!ag.isNull());
130	63	disj.push_back(ag.negate());
131	126	Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
132		// Apply extended rewriting on the lemma. This helps utilities like
133		// SygusEnumerator more easily recognize the shape of this lemma, e.g.
134		// ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x).
135	63	lem = extendedRewrite(lem);
136	126	Trace("sygus-pbe") << " static redundant op lemma : " << lem
137	63	<< std::endl;
138		// Register as a symmetry breaking lemma with the term database.
139		// This will either be processed via a lemma on the output channel
140		// of the sygus extension of the datatypes solver, or internally
141		// encoded as a constraint to an active enumerator.
142	63	d_tds->registerSymBreakLemma(e, lem, etn, 0, false);
143		}
144		}
145		}
146	79	return true;
147		}
148
149		// ------------------------------------------- solution construction from enumeration
150
151	7068	void SygusPbe::getTermList(const std::vector<Node>& candidates,
152		std::vector<Node>& terms)
153		{
154	14283	for( unsigned i=0; i<candidates.size(); i++ ){
155	14430	Node v = candidates[i];
156		std::map<Node, std::vector<Node> >::iterator it =
157	7215	d_candidate_to_enum.find(v);
158	7215	if (it != d_candidate_to_enum.end())
159		{
160	7215	terms.insert(terms.end(), it->second.begin(), it->second.end());
161		}
162		}
163	7068	}
164
165	7068	bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); }
166
167	891	bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
168		const std::vector<Node>& enum_values,
169		const std::vector<Node>& candidates,
170		std::vector<Node>& candidate_values)
171		{
172	891	Assert(enums.size() == enum_values.size());
173	891	if( !enums.empty() ){
174	891	unsigned min_term_size = 0;
175	891	Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
176	1782	std::vector<unsigned> szs;
177	2138	for (unsigned i = 0, esize = enums.size(); i < esize; i++)
178		{
179	1247	Trace("sygus-pbe-enum") << " " << enums[i] << " -> ";
180	1247	TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
181	1247	Trace("sygus-pbe-enum") << std::endl;
182	1247	if (!enum_values[i].isNull())
183		{
184	1006	unsigned sz = datatypes::utils::getSygusTermSize(enum_values[i]);
185	1006	szs.push_back(sz);
186	1006	if (i == 0 \|\| sz < min_term_size)
187		{
188	838	min_term_size = sz;
189		}
190		}
191		else
192		{
193	241	szs.push_back(0);
194		}
195		}
196		// Assume two enumerators of types T1 and T2.
197		// If options::sygusPbeMultiFair() is true,
198		// we ensure that all values of type T1 and size n are enumerated before
199		// any term of type T2 of size n+d, and vice versa, where d is
200		// set by options::sygusPbeMultiFairDiff(). If d is zero, then our
201		// enumeration is such that all terms of T1 or T2 of size n are considered
202		// before any term of size n+1.
203	891	int diffAllow = options::sygusPbeMultiFairDiff();
204	1782	std::vector<unsigned> enum_consider;
205	2138	for (unsigned i = 0, esize = enums.size(); i < esize; i++)
206		{
207	1247	if (!enum_values[i].isNull())
208		{
209	1006	Assert(szs[i] >= min_term_size);
210	1006	int diff = szs[i] - min_term_size;
211	1006	if (!options::sygusPbeMultiFair() \|\| diff <= diffAllow)
212		{
213	1006	enum_consider.push_back(i);
214		}
215		}
216		}
217
218		// only consider the enumerators that are at minimum size (for fairness)
219	891	Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl;
220	891	NodeManager* nm = NodeManager::currentNM();
221	1897	for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; i++)
222		{
223	1006	unsigned j = enum_consider[i];
224	2012	Node e = enums[j];
225	2012	Node v = enum_values[j];
226	1006	Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end());
227	2012	Node c = d_enum_to_candidate[e];
228	2012	std::vector<Node> enum_lems;
229	1006	d_sygus_unif[c]->notifyEnumeration(e, v, enum_lems);
230	1006	if (!enum_lems.empty())
231		{
232		// the lemmas must be guarded by the active guard of the enumerator
233	28	Node g = d_tds->getActiveGuardForEnumerator(e);
234	14	Assert(!g.isNull());
235	28	for (unsigned k = 0, size = enum_lems.size(); k < size; k++)
236		{
237	28	Node lem = nm->mkNode(OR, g.negate(), enum_lems[k]);
238	14	d_qim.addPendingLemma(lem,
239		InferenceId::QUANTIFIERS_SYGUS_PBE_EXCLUDE);
240		}
241		}
242		}
243		}
244	984	for( unsigned i=0; i<candidates.size(); i++ ){
245	999	Node c = candidates[i];
246		//build decision tree for candidate
247	999	std::vector<Node> sol;
248	999	std::vector<Node> lems;
249	906	bool solSuccess = d_sygus_unif[c]->constructSolution(sol, lems);
250	906	for (const Node& lem : lems)
251		{
252		d_qim.addPendingLemma(lem,
253		InferenceId::QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL);
254		}
255	906	if (solSuccess)
256		{
257	93	Assert(sol.size() == 1);
258	93	candidate_values.push_back(sol[0]);
259		}
260		else
261		{
262	813	return false;
263		}
264		}
265	78	return true;
266		}
267
268		}
269		}
270	31137	} // namespace cvc5