Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/candidate_rewrite_filter.cpp	Lines:	115	126	91.3 %
Date:	2021-11-07	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(Env& env)
    : EnvObj(env),
      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::make_unique<DynamicRewriter>(d_env, &d_fakeContext, ssn.str());
}

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