Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/candidate_rewrite_filter.cpp	Lines:	115	126	91.3 %
Date:	2021-09-18	Branches:	255	596	42.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, 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.
 * ****************************************************************************
 *
 * Implements techniques for candidate rewrite rule filtering, which
 * filters the output of --sygus-rr-synth. The classes in this file implement
 * filtering based on congruence, variable ordering, and matching.
 */

#include "theory/quantifiers/candidate_rewrite_filter.h"

#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

// the number of d_drewrite objects we have allocated (to avoid name conflicts)
static unsigned drewrite_counter = 0;

CandidateRewriteFilter::CandidateRewriteFilter()
    : d_ss(nullptr),
      d_tds(nullptr),
      d_use_sygus_type(false),
      d_drewrite(nullptr),
      d_ssenm(*this)
{
}

void CandidateRewriteFilter::initialize(SygusSampler* ss,
                                        TermDbSygus* tds,
                                        bool useSygusType)
{
  d_ss = ss;
  d_use_sygus_type = useSygusType;
  d_tds = tds;
  // initialize members of this class
  d_match_trie.clear();
  d_pairs.clear();
  // (re)initialize the dynamic rewriter
  std::stringstream ssn;
  ssn << "_dyn_rewriter_" << drewrite_counter;
  drewrite_counter++;
  d_drewrite = std::unique_ptr<DynamicRewriter>(
      new DynamicRewriter(ssn.str(), &d_fake_context));
}

bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
{
  Node bn = n;
  Node beq_n = eq_n;
  if (d_use_sygus_type)
  {
    bn = d_tds->sygusToBuiltin(n);
    beq_n = d_tds->sygusToBuiltin(eq_n);
  }
  Trace("cr-filter") << "crewriteFilter : " << bn << "..." << beq_n
                     << std::endl;
  // whether we will keep this pair
  bool keep = true;

  // ----- check redundancy based on variables
  if (options::sygusRewSynthFilterOrder()
      || options::sygusRewSynthFilterNonLinear())
  {
    bool nor = d_ss->checkVariables(bn,
                                    options::sygusRewSynthFilterOrder(),
                                    options::sygusRewSynthFilterNonLinear());
    bool eqor = d_ss->checkVariables(beq_n,
                                     options::sygusRewSynthFilterOrder(),
                                     options::sygusRewSynthFilterNonLinear());
    Trace("cr-filter-debug")
        << "Variables ok? : " << nor << " " << eqor << std::endl;
    if (eqor || nor)
    {
      // if only one is ordered, then we require that the ordered one's
      // variables cannot be a strict subset of the variables of the other.
      if (!eqor)
      {
        if (d_ss->containsFreeVariables(beq_n, bn, true))
        {
          keep = false;
        }
        else
        {
          // if the previous value stored was unordered, but n is
          // ordered, we prefer n. Thus, we force its addition to the
          // sampler database.
          d_ss->registerTerm(n, true);
        }
      }
      else if (!nor)
      {
        keep = !d_ss->containsFreeVariables(bn, beq_n, true);
      }
    }
    else
    {
      keep = false;
    }
    if (!keep)
    {
      Trace("cr-filter") << "...redundant (unordered)" << std::endl;
    }
  }

  // ----- check rewriting redundancy
  if (keep && options::sygusRewSynthFilterCong())
  {
    // When using sygus types, this filtering applies to the builtin versions
    // of n and eq_n. This means that we may filter out a rewrite rule for one
    // sygus type based on another, e.g. we won't report x=x+0 for both A and B
    // in:
    //   A -> x | 0 | A+A
    //   B -> x | 0 | B+B
    Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl;
    if (d_drewrite->areEqual(bn, beq_n))
    {
      // must be unique according to the dynamic rewriter
      Trace("cr-filter") << "...redundant (rewritable)" << std::endl;
      keep = false;
    }
  }

  if (keep && options::sygusRewSynthFilterMatch())
  {
    // ----- check matchable
    // check whether the pair is matchable with a previous one
    d_curr_pair_rhs = beq_n;
    Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n
                       << "]..." << std::endl;
    Node bni = d_drewrite->toInternal(bn);
    if (!bni.isNull())
    {
      // as with congruence filtering, we cache based on the builtin type
      TypeNode tn = bn.getType();
      if (!d_match_trie[tn].getMatches(bni, &d_ssenm))
      {
        keep = false;
        Trace("cr-filter") << "...redundant (matchable)" << std::endl;
        // regardless, would help to remember it
        registerRelevantPair(n, eq_n);
      }
    }
    // if bni is null, it may involve non-first-class types that we cannot
    // reason about
  }

  if (keep)
  {
    return false;
  }
  if (Trace.isOn("sygus-rr-filter"))
  {
    std::stringstream ss;
    ss << "(redundant-rewrite ";
    TermDbSygus::toStreamSygus(ss, n);
    ss << " ";
    TermDbSygus::toStreamSygus(ss, eq_n);
    ss << ")";
    Trace("sygus-rr-filter") << ss.str() << std::endl;
  }
  return true;
}

void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n)
{
  Node bn = n;
  Node beq_n = eq_n;
  if (d_use_sygus_type)
  {
    bn = d_tds->sygusToBuiltin(n);
    beq_n = d_tds->sygusToBuiltin(eq_n);
  }
  // ----- check rewriting redundancy
  if (options::sygusRewSynthFilterCong())
  {
    Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl;
    Assert(!d_drewrite->areEqual(bn, beq_n));
    d_drewrite->addRewrite(bn, beq_n);
  }
  if (options::sygusRewSynthFilterMatch())
  {
    // cache based on the builtin type
    TypeNode tn = bn.getType();
    // add to match information
    for (unsigned r = 0; r < 2; r++)
    {
      Node t = r == 0 ? bn : beq_n;
      Node to = r == 0 ? beq_n : bn;
      // insert in match trie if first time
      if (d_pairs.find(t) == d_pairs.end())
      {
        Trace("crf-match") << "CRF add term : " << t << std::endl;
        Node ti = d_drewrite->toInternal(t);
        if (!ti.isNull())
        {
          d_match_trie[tn].addTerm(ti);
        }
      }
      d_pairs[t].insert(to);
    }
  }
}

bool CandidateRewriteFilter::notify(Node s,
                                    Node n,
                                    std::vector<Node>& vars,
                                    std::vector<Node>& subs)
{
  Trace("crf-match-debug") << "Got : " << s << " matches " << n << std::endl;
  Assert(!d_curr_pair_rhs.isNull());
  // convert back to original forms
  s = d_drewrite->toExternal(s);
  Assert(!s.isNull());
  n = d_drewrite->toExternal(n);
  Assert(!n.isNull());
  std::map<Node, std::unordered_set<Node> >::iterator it = d_pairs.find(n);
  if (Trace.isOn("crf-match"))
  {
    Trace("crf-match") << "  " << s << " matches " << n
                       << " under:" << std::endl;
    for (unsigned i = 0, size = vars.size(); i < size; i++)
    {
      Trace("crf-match") << "    " << vars[i] << " -> " << subs[i] << std::endl;
    }
  }
#ifdef CVC5_ASSERTIONS
  for (unsigned i = 0, size = vars.size(); i < size; i++)
  {
    // By using internal representation of terms, we ensure polymorphism is
    // handled correctly.
    Assert(vars[i].getType().isComparableTo(subs[i].getType()));
  }
#endif
  // must convert the inferred substitution to original form
  std::vector<Node> esubs;
  for (const Node& sb : subs)
  {
    esubs.push_back(d_drewrite->toExternal(sb));
  }
  Assert(it != d_pairs.end());
  for (const Node& nr : it->second)
  {
    Node nrs =
        nr.substitute(vars.begin(), vars.end(), esubs.begin(), esubs.end());
    bool areEqual = (nrs == d_curr_pair_rhs);
    if (!areEqual && options::sygusRewSynthFilterCong())
    {
      // if dynamic rewriter is available, consult it
      areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs);
    }
    if (areEqual)
    {
      Trace("crf-match") << "*** Match, current pair: " << std::endl;
      Trace("crf-match") << "  (" << s << ", " << d_curr_pair_rhs << ")"
                         << std::endl;
      Trace("crf-match") << "is an instance of previous pair:" << std::endl;
      Trace("crf-match") << "  (" << n << ", " << nr << ")" << std::endl;
      return false;
    }
  }
  return true;
}

}  // 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, 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		* Implements techniques for candidate rewrite rule filtering, which
14		* filters the output of --sygus-rr-synth. The classes in this file implement
15		* filtering based on congruence, variable ordering, and matching.
16		*/
17
18		#include "theory/quantifiers/candidate_rewrite_filter.h"
19
20		#include "options/base_options.h"
21		#include "options/quantifiers_options.h"
22		#include "printer/printer.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace quantifiers {
29
30		// the number of d_drewrite objects we have allocated (to avoid name conflicts)
31		static unsigned drewrite_counter = 0;
32
33	62	CandidateRewriteFilter::CandidateRewriteFilter()
34		: d_ss(nullptr),
35		d_tds(nullptr),
36		d_use_sygus_type(false),
37		d_drewrite(nullptr),
38	62	d_ssenm(*this)
39		{
40	62	}
41
42	7	void CandidateRewriteFilter::initialize(SygusSampler* ss,
43		TermDbSygus* tds,
44		bool useSygusType)
45		{
46	7	d_ss = ss;
47	7	d_use_sygus_type = useSygusType;
48	7	d_tds = tds;
49		// initialize members of this class
50	7	d_match_trie.clear();
51	7	d_pairs.clear();
52		// (re)initialize the dynamic rewriter
53	14	std::stringstream ssn;
54	7	ssn << "_dyn_rewriter_" << drewrite_counter;
55	7	drewrite_counter++;
56	21	d_drewrite = std::unique_ptr<DynamicRewriter>(
57	28	new DynamicRewriter(ssn.str(), &d_fake_context));
58	7	}
59
60	229	bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
61		{
62	458	Node bn = n;
63	458	Node beq_n = eq_n;
64	229	if (d_use_sygus_type)
65		{
66	229	bn = d_tds->sygusToBuiltin(n);
67	229	beq_n = d_tds->sygusToBuiltin(eq_n);
68		}
69	458	Trace("cr-filter") << "crewriteFilter : " << bn << "..." << beq_n
70	229	<< std::endl;
71		// whether we will keep this pair
72	229	bool keep = true;
73
74		// ----- check redundancy based on variables
75	458	if (options::sygusRewSynthFilterOrder()
76	229	\|\| options::sygusRewSynthFilterNonLinear())
77		{
78	916	bool nor = d_ss->checkVariables(bn,
79	229	options::sygusRewSynthFilterOrder(),
80	458	options::sygusRewSynthFilterNonLinear());
81	916	bool eqor = d_ss->checkVariables(beq_n,
82	229	options::sygusRewSynthFilterOrder(),
83	458	options::sygusRewSynthFilterNonLinear());
84	458	Trace("cr-filter-debug")
85	229	<< "Variables ok? : " << nor << " " << eqor << std::endl;
86	229	if (eqor \|\| nor)
87		{
88		// if only one is ordered, then we require that the ordered one's
89		// variables cannot be a strict subset of the variables of the other.
90	356	if (!eqor)
91		{
92	3	if (d_ss->containsFreeVariables(beq_n, bn, true))
93		{
94	1	keep = false;
95		}
96		else
97		{
98		// if the previous value stored was unordered, but n is
99		// ordered, we prefer n. Thus, we force its addition to the
100		// sampler database.
101	2	d_ss->registerTerm(n, true);
102		}
103		}
104	175	else if (!nor)
105		{
106	61	keep = !d_ss->containsFreeVariables(bn, beq_n, true);
107		}
108		}
109		else
110		{
111	51	keep = false;
112		}
113	229	if (!keep)
114		{
115	106	Trace("cr-filter") << "...redundant (unordered)" << std::endl;
116		}
117		}
118
119		// ----- check rewriting redundancy
120	229	if (keep && options::sygusRewSynthFilterCong())
121		{
122		// When using sygus types, this filtering applies to the builtin versions
123		// of n and eq_n. This means that we may filter out a rewrite rule for one
124		// sygus type based on another, e.g. we won't report x=x+0 for both A and B
125		// in:
126		// A -> x \| 0 \| A+A
127		// B -> x \| 0 \| B+B
128	123	Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl;
129	123	if (d_drewrite->areEqual(bn, beq_n))
130		{
131		// must be unique according to the dynamic rewriter
132	2	Trace("cr-filter") << "...redundant (rewritable)" << std::endl;
133	2	keep = false;
134		}
135		}
136
137	229	if (keep && options::sygusRewSynthFilterMatch())
138		{
139		// ----- check matchable
140		// check whether the pair is matchable with a previous one
141	121	d_curr_pair_rhs = beq_n;
142	242	Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n
143	121	<< "]..." << std::endl;
144	242	Node bni = d_drewrite->toInternal(bn);
145	121	if (!bni.isNull())
146		{
147		// as with congruence filtering, we cache based on the builtin type
148	242	TypeNode tn = bn.getType();
149	121	if (!d_match_trie[tn].getMatches(bni, &d_ssenm))
150		{
151	2	keep = false;
152	2	Trace("cr-filter") << "...redundant (matchable)" << std::endl;
153		// regardless, would help to remember it
154	2	registerRelevantPair(n, eq_n);
155		}
156		}
157		// if bni is null, it may involve non-first-class types that we cannot
158		// reason about
159		}
160
161	229	if (keep)
162		{
163	119	return false;
164		}
165	110	if (Trace.isOn("sygus-rr-filter"))
166		{
167		std::stringstream ss;
168		ss << "(redundant-rewrite ";
169		TermDbSygus::toStreamSygus(ss, n);
170		ss << " ";
171		TermDbSygus::toStreamSygus(ss, eq_n);
172		ss << ")";
173		Trace("sygus-rr-filter") << ss.str() << std::endl;
174		}
175	110	return true;
176		}
177
178	105	void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n)
179		{
180	210	Node bn = n;
181	210	Node beq_n = eq_n;
182	105	if (d_use_sygus_type)
183		{
184	105	bn = d_tds->sygusToBuiltin(n);
185	105	beq_n = d_tds->sygusToBuiltin(eq_n);
186		}
187		// ----- check rewriting redundancy
188	105	if (options::sygusRewSynthFilterCong())
189		{
190	105	Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl;
191	105	Assert(!d_drewrite->areEqual(bn, beq_n));
192	105	d_drewrite->addRewrite(bn, beq_n);
193		}
194	105	if (options::sygusRewSynthFilterMatch())
195		{
196		// cache based on the builtin type
197	210	TypeNode tn = bn.getType();
198		// add to match information
199	315	for (unsigned r = 0; r < 2; r++)
200		{
201	420	Node t = r == 0 ? bn : beq_n;
202	420	Node to = r == 0 ? beq_n : bn;
203		// insert in match trie if first time
204	210	if (d_pairs.find(t) == d_pairs.end())
205		{
206	148	Trace("crf-match") << "CRF add term : " << t << std::endl;
207	296	Node ti = d_drewrite->toInternal(t);
208	148	if (!ti.isNull())
209		{
210	148	d_match_trie[tn].addTerm(ti);
211		}
212		}
213	210	d_pairs[t].insert(to);
214		}
215		}
216	105	}
217
218	80	bool CandidateRewriteFilter::notify(Node s,
219		Node n,
220		std::vector<Node>& vars,
221		std::vector<Node>& subs)
222		{
223	80	Trace("crf-match-debug") << "Got : " << s << " matches " << n << std::endl;
224	80	Assert(!d_curr_pair_rhs.isNull());
225		// convert back to original forms
226	80	s = d_drewrite->toExternal(s);
227	80	Assert(!s.isNull());
228	80	n = d_drewrite->toExternal(n);
229	80	Assert(!n.isNull());
230	80	std::map<Node, std::unordered_set<Node> >::iterator it = d_pairs.find(n);
231	80	if (Trace.isOn("crf-match"))
232		{
233		Trace("crf-match") << " " << s << " matches " << n
234		<< " under:" << std::endl;
235		for (unsigned i = 0, size = vars.size(); i < size; i++)
236		{
237		Trace("crf-match") << " " << vars[i] << " -> " << subs[i] << std::endl;
238		}
239		}
240		#ifdef CVC5_ASSERTIONS
241	164	for (unsigned i = 0, size = vars.size(); i < size; i++)
242		{
243		// By using internal representation of terms, we ensure polymorphism is
244		// handled correctly.
245	84	Assert(vars[i].getType().isComparableTo(subs[i].getType()));
246		}
247		#endif
248		// must convert the inferred substitution to original form
249	160	std::vector<Node> esubs;
250	164	for (const Node& sb : subs)
251		{
252	84	esubs.push_back(d_drewrite->toExternal(sb));
253		}
254	80	Assert(it != d_pairs.end());
255	656	for (const Node& nr : it->second)
256		{
257		Node nrs =
258	1154	nr.substitute(vars.begin(), vars.end(), esubs.begin(), esubs.end());
259	578	bool areEqual = (nrs == d_curr_pair_rhs);
260	578	if (!areEqual && options::sygusRewSynthFilterCong())
261		{
262		// if dynamic rewriter is available, consult it
263	576	areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs);
264		}
265	578	if (areEqual)
266		{
267	2	Trace("crf-match") << "*** Match, current pair: " << std::endl;
268	4	Trace("crf-match") << " (" << s << ", " << d_curr_pair_rhs << ")"
269	2	<< std::endl;
270	2	Trace("crf-match") << "is an instance of previous pair:" << std::endl;
271	2	Trace("crf-match") << " (" << n << ", " << nr << ")" << std::endl;
272	2	return false;
273		}
274		}
275	78	return true;
276		}
277
278		} // namespace quantifiers
279		} // namespace theory
280	29574	} // namespace cvc5