Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/candidate_rewrite_filter.h	Lines:	6	6	100.0 %
Date:	2021-11-07	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 "smt/env_obj.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 : protected EnvObj
{
 public:
  CandidateRewriteFilter(Env& env);

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