Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/candidate_rewrite_filter.h	Lines:	6	6	100.0 %
Date:	2021-09-29	Branches:	2	4	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner
 *
 * 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 "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H

#include <map>
#include "expr/match_trie.h"
#include "theory/quantifiers/dynamic_rewrite.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/sygus_sampler.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

/** candidate rewrite filter
 *
 * This class is responsible for various filtering techniques for candidate
 * rewrite rules, including:
 * (1) filtering based on variable ordering,
 * (2) filtering based on congruence,
 * (3) filtering based on matching.
 * For details, see Reynolds et al "Rewrites for SMT Solvers using Syntax-Guided
 * Enumeration", SMT 2018.
 *
 * In the following, we assume that the registerRelevantPair method of this
 * class been called for some pairs of terms. For each such call to
 * registerRelevantPair( t, s ), we say that (t,s) and (s,t) are "relevant
 * pairs". A relevant pair ( t, s ) typically corresponds to a (candidate)
 * rewrite t = s.
 */
class CandidateRewriteFilter
{
 public:
  CandidateRewriteFilter();

  /** initialize
   *
   * Initializes this class, ss is the sygus sampler that this class is
   * filtering rewrite rule pairs for, and tds is a point to the sygus term
   * database utility class.
   *
   * If useSygusType is false, this means that the terms in filterPair and
   * registerRelevantPair calls should be interpreted as themselves. Otherwise,
   * if useSygusType is true, these terms should be interpreted as their
   * analog according to the deep embedding.
   */
  void initialize(SygusSampler* ss, TermDbSygus* tds, bool useSygusType);
  /** filter pair
   *
   * This method returns true if the pair (n, eq_n) should be filtered. If it
   * is not filtered, then the caller may choose to call
   * registerRelevantPair(n, eq_n) below, although it may not, say if it finds
   * another reason to discard the pair.
   *
   * If this method returns false, then for all previous relevant pairs
   * ( a, eq_a ), we have that n = eq_n is not an instance of a = eq_a
   * modulo symmetry of equality, nor is n = eq_n derivable from the set of
   * all previous relevant pairs. The latter is determined by the d_drewrite
   * utility. For example:
   * [1]  ( t+0, t ) and ( x+0, x )
   * will not both be relevant pairs of this function since t+0=t is
   * an instance of x+0=x.
   * [2]  ( s, t ) and ( s+0, t+0 )
   * will not both be relevant pairs of this function since s+0=t+0 is
   * derivable from s=t.
   * These two criteria may be combined, for example:
   * [3] ( t+0, s ) is not a relevant pair if both ( x+0, x+s ) and ( t+s, s )
   * are relevant pairs, since t+0 is an instance of x+0 where
   * { x |-> t }, and x+s { x |-> t } = s is derivable, via the third pair
   * above (t+s = s).
   */
  bool filterPair(Node n, Node eq_n);
  /** register relevant pair
   *
   * This should be called after filterPair( n, eq_n ) returns false.
   * This registers ( n, eq_n ) as a relevant pair with this class.
   */
  void registerRelevantPair(Node n, Node eq_n);

 private:
  /** pointer to the sygus sampler that this class is filtering rewrites for */
  SygusSampler* d_ss;
  /** pointer to the sygus term database, used if d_use_sygus_type is true */
  TermDbSygus* d_tds;
  /** whether we are registering sygus terms with this class */
  bool d_use_sygus_type;

  //----------------------------congruence filtering
  /** a (dummy) user context, used for d_drewrite */
  context::UserContext d_fake_context;
  /** dynamic rewriter class */
  std::unique_ptr<DynamicRewriter> d_drewrite;
  //----------------------------end congruence filtering

  //----------------------------match filtering
  /**
   * Stores all relevant pairs returned by this sampler (see registerTerm). In
   * detail, if (t,s) is a relevant pair, then t in d_pairs[s].
   */
  std::map<Node, std::unordered_set<Node> > d_pairs;
  /**
   * For each (builtin) type, a match trie storing all terms in the domain of
   * d_pairs.
   *
   * Notice that we store d_drewrite->toInternal(t) instead of t, for each
   * term t, so that polymorphism is handled properly. In particular, this
   * prevents matches between terms select( x, y ) and select( z, y ) where
   * the type of x and z are different.
   */
  std::map<TypeNode, expr::MatchTrie> d_match_trie;
  /** Notify class */
  class CandidateRewriteFilterNotifyMatch : public expr::NotifyMatch
  {
    CandidateRewriteFilter& d_sse;

   public:
    CandidateRewriteFilterNotifyMatch(CandidateRewriteFilter& sse) : d_sse(sse)
    {
    }
    /** notify match */
    bool notify(Node n,
                Node s,
                std::vector<Node>& vars,
                std::vector<Node>& subs) override
    {
      return d_sse.notify(n, s, vars, subs);
    }
  };
  /** Notify object used for reporting matches from d_match_trie */
  CandidateRewriteFilterNotifyMatch d_ssenm;
  /**
   * Stores the current right hand side of a pair we are considering.
   *
   * In more detail, in registerTerm, we are interested in whether a pair (s,t)
   * is a relevant pair. We do this by:
   * (1) Setting the node d_curr_pair_rhs to t,
   * (2) Using d_match_trie, compute all terms s1...sn that match s.
   * For each si, where s = si * sigma for some substitution sigma, we check
   * whether t = ti * sigma for some previously relevant pair (si,ti), in
   * which case (s,t) is an instance of (si,ti).
   */
  Node d_curr_pair_rhs;
  /**
   * Called by the above class during d_match_trie.getMatches( s ), when we
   * find that si = s * sigma, where si is a term that is stored in
   * d_match_trie.
   *
   * This function returns false if ( s, d_curr_pair_rhs ) is an instance of
   * previously relevant pair.
   */
  bool notify(Node s, Node n, std::vector<Node>& vars, std::vector<Node>& subs);
  //----------------------------end match filtering
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner
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 "cvc5_private.h"
19
20		#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
21		#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
22
23		#include <map>
24		#include "expr/match_trie.h"
25		#include "theory/quantifiers/dynamic_rewrite.h"
26		#include "theory/quantifiers/sygus/term_database_sygus.h"
27		#include "theory/quantifiers/sygus_sampler.h"
28
29		namespace cvc5 {
30		namespace theory {
31		namespace quantifiers {
32
33		/** candidate rewrite filter
34		*
35		* This class is responsible for various filtering techniques for candidate
36		* rewrite rules, including:
37		* (1) filtering based on variable ordering,
38		* (2) filtering based on congruence,
39		* (3) filtering based on matching.
40		* For details, see Reynolds et al "Rewrites for SMT Solvers using Syntax-Guided
41		* Enumeration", SMT 2018.
42		*
43		* In the following, we assume that the registerRelevantPair method of this
44		* class been called for some pairs of terms. For each such call to
45		* registerRelevantPair( t, s ), we say that (t,s) and (s,t) are "relevant
46		* pairs". A relevant pair ( t, s ) typically corresponds to a (candidate)
47		* rewrite t = s.
48		*/
49	62	class CandidateRewriteFilter
50		{
51		public:
52		CandidateRewriteFilter();
53
54		/** initialize
55		*
56		* Initializes this class, ss is the sygus sampler that this class is
57		* filtering rewrite rule pairs for, and tds is a point to the sygus term
58		* database utility class.
59		*
60		* If useSygusType is false, this means that the terms in filterPair and
61		* registerRelevantPair calls should be interpreted as themselves. Otherwise,
62		* if useSygusType is true, these terms should be interpreted as their
63		* analog according to the deep embedding.
64		*/
65		void initialize(SygusSampler* ss, TermDbSygus* tds, bool useSygusType);
66		/** filter pair
67		*
68		* This method returns true if the pair (n, eq_n) should be filtered. If it
69		* is not filtered, then the caller may choose to call
70		* registerRelevantPair(n, eq_n) below, although it may not, say if it finds
71		* another reason to discard the pair.
72		*
73		* If this method returns false, then for all previous relevant pairs
74		* ( a, eq_a ), we have that n = eq_n is not an instance of a = eq_a
75		* modulo symmetry of equality, nor is n = eq_n derivable from the set of
76		* all previous relevant pairs. The latter is determined by the d_drewrite
77		* utility. For example:
78		* [1] ( t+0, t ) and ( x+0, x )
79		* will not both be relevant pairs of this function since t+0=t is
80		* an instance of x+0=x.
81		* [2] ( s, t ) and ( s+0, t+0 )
82		* will not both be relevant pairs of this function since s+0=t+0 is
83		* derivable from s=t.
84		* These two criteria may be combined, for example:
85		* [3] ( t+0, s ) is not a relevant pair if both ( x+0, x+s ) and ( t+s, s )
86		* are relevant pairs, since t+0 is an instance of x+0 where
87		* { x \|-> t }, and x+s { x \|-> t } = s is derivable, via the third pair
88		* above (t+s = s).
89		*/
90		bool filterPair(Node n, Node eq_n);
91		/** register relevant pair
92		*
93		* This should be called after filterPair( n, eq_n ) returns false.
94		* This registers ( n, eq_n ) as a relevant pair with this class.
95		*/
96		void registerRelevantPair(Node n, Node eq_n);
97
98		private:
99		/** pointer to the sygus sampler that this class is filtering rewrites for */
100		SygusSampler* d_ss;
101		/** pointer to the sygus term database, used if d_use_sygus_type is true */
102		TermDbSygus* d_tds;
103		/** whether we are registering sygus terms with this class */
104		bool d_use_sygus_type;
105
106		//----------------------------congruence filtering
107		/** a (dummy) user context, used for d_drewrite */
108		context::UserContext d_fake_context;
109		/** dynamic rewriter class */
110		std::unique_ptr<DynamicRewriter> d_drewrite;
111		//----------------------------end congruence filtering
112
113		//----------------------------match filtering
114		/**
115		* Stores all relevant pairs returned by this sampler (see registerTerm). In
116		* detail, if (t,s) is a relevant pair, then t in d_pairs[s].
117		*/
118		std::map<Node, std::unordered_set<Node> > d_pairs;
119		/**
120		* For each (builtin) type, a match trie storing all terms in the domain of
121		* d_pairs.
122		*
123		* Notice that we store d_drewrite->toInternal(t) instead of t, for each
124		* term t, so that polymorphism is handled properly. In particular, this
125		* prevents matches between terms select( x, y ) and select( z, y ) where
126		* the type of x and z are different.
127		*/
128		std::map<TypeNode, expr::MatchTrie> d_match_trie;
129		/** Notify class */
130	62	class CandidateRewriteFilterNotifyMatch : public expr::NotifyMatch
131		{
132		CandidateRewriteFilter& d_sse;
133
134		public:
135	62	CandidateRewriteFilterNotifyMatch(CandidateRewriteFilter& sse) : d_sse(sse)
136		{
137	62	}
138		/** notify match */
139	80	bool notify(Node n,
140		Node s,
141		std::vector<Node>& vars,
142		std::vector<Node>& subs) override
143		{
144	80	return d_sse.notify(n, s, vars, subs);
145		}
146		};
147		/** Notify object used for reporting matches from d_match_trie */
148		CandidateRewriteFilterNotifyMatch d_ssenm;
149		/**
150		* Stores the current right hand side of a pair we are considering.
151		*
152		* In more detail, in registerTerm, we are interested in whether a pair (s,t)
153		* is a relevant pair. We do this by:
154		* (1) Setting the node d_curr_pair_rhs to t,
155		* (2) Using d_match_trie, compute all terms s1...sn that match s.
156		* For each si, where s = si * sigma for some substitution sigma, we check
157		* whether t = ti * sigma for some previously relevant pair (si,ti), in
158		* which case (s,t) is an instance of (si,ti).
159		*/
160		Node d_curr_pair_rhs;
161		/**
162		* Called by the above class during d_match_trie.getMatches( s ), when we
163		* find that si = s * sigma, where si is a term that is stored in
164		* d_match_trie.
165		*
166		* This function returns false if ( s, d_curr_pair_rhs ) is an instance of
167		* previously relevant pair.
168		*/
169		bool notify(Node s, Node n, std::vector<Node>& vars, std::vector<Node>& subs);
170		//----------------------------end match filtering
171		};
172
173		} // namespace quantifiers
174		} // namespace theory
175		} // namespace cvc5
176
177		#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */