Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_enumerator_callback.h	Lines:	2	4	50.0 %
Date:	2021-09-07	Branches:	0	0	0.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.
 * ****************************************************************************
 *
 * sygus_enumerator
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H

#include <unordered_set>

#include "expr/node.h"
#include "theory/quantifiers/extended_rewrite.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class ExampleEvalCache;
class SygusStatistics;
class SygusSampler;

/**
 * Base class for callbacks in the fast enumerator. This allows a user to
 * provide custom criteria for whether or not enumerated values should be
 * considered.
 */
class SygusEnumeratorCallback
{
 public:
  SygusEnumeratorCallback(Node e, SygusStatistics* s = nullptr);
  virtual ~SygusEnumeratorCallback() {}
  /**
   * Add term, return true if the term should be considered in the enumeration.
   * Notice that returning false indicates that n should not be considered as a
   * subterm of any other term in the enumeration.
   *
   * @param n The SyGuS term
   * @param bterms The (rewritten, builtin) terms we have already enumerated
   * @return true if n should be considered in the enumeration.
   */
  virtual bool addTerm(Node n, std::unordered_set<Node>& bterms);

 protected:
  /**
   * Callback-specific notification of the above
   *
   * @param n The SyGuS term
   * @param bn The builtin version of the enumerated term
   * @param bnr The (extended) rewritten form of bn
   */
  virtual void notifyTermInternal(Node n, Node bn, Node bnr) {}
  /**
   * Callback-specific add term
   *
   * @param n The SyGuS term
   * @param bn The builtin version of the enumerated term
   * @param bnr The (extended) rewritten form of bn
   * @return true if the term should be considered in the enumeration.
   */
  virtual bool addTermInternal(Node n, Node bn, Node bnr) { return true; }
  /** The enumerator */
  Node d_enum;
  /** The type of enum */
  TypeNode d_tn;
  /** extended rewriter */
  ExtendedRewriter d_extr;
  /** pointer to the statistics */
  SygusStatistics* d_stats;
};

class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
{
 public:
  SygusEnumeratorCallbackDefault(Node e,
                                 SygusStatistics* s = nullptr,
                                 ExampleEvalCache* eec = nullptr,
                                 SygusSampler* ssrv = nullptr,
                                 std::ostream* out = nullptr);
  virtual ~SygusEnumeratorCallbackDefault() {}

 protected:
  /** Notify that bn / bnr is an enumerated builtin, rewritten form of a term */
  void notifyTermInternal(Node n, Node bn, Node bnr) override;
  /** Add term, return true if n should be considered in the enumeration */
  bool addTermInternal(Node n, Node bn, Node bnr) override;
  /**
   * Pointer to the example evaluation cache utility (used for symmetry
   * breaking).
   */
  ExampleEvalCache* d_eec;
  /** sampler (for --sygus-rr-verify) */
  SygusSampler* d_samplerRrV;
  /** The output stream to print unsound rewrites for above */
  std::ostream* d_out;
};

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

#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_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		* sygus_enumerator
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
19		#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H
20
21		#include <unordered_set>
22
23		#include "expr/node.h"
24		#include "theory/quantifiers/extended_rewrite.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace quantifiers {
29
30		class ExampleEvalCache;
31		class SygusStatistics;
32		class SygusSampler;
33
34		/**
35		* Base class for callbacks in the fast enumerator. This allows a user to
36		* provide custom criteria for whether or not enumerated values should be
37		* considered.
38		*/
39		class SygusEnumeratorCallback
40		{
41		public:
42		SygusEnumeratorCallback(Node e, SygusStatistics* s = nullptr);
43	166	virtual ~SygusEnumeratorCallback() {}
44		/**
45		* Add term, return true if the term should be considered in the enumeration.
46		* Notice that returning false indicates that n should not be considered as a
47		* subterm of any other term in the enumeration.
48		*
49		* @param n The SyGuS term
50		* @param bterms The (rewritten, builtin) terms we have already enumerated
51		* @return true if n should be considered in the enumeration.
52		*/
53		virtual bool addTerm(Node n, std::unordered_set<Node>& bterms);
54
55		protected:
56		/**
57		* Callback-specific notification of the above
58		*
59		* @param n The SyGuS term
60		* @param bn The builtin version of the enumerated term
61		* @param bnr The (extended) rewritten form of bn
62		*/
63		virtual void notifyTermInternal(Node n, Node bn, Node bnr) {}
64		/**
65		* Callback-specific add term
66		*
67		* @param n The SyGuS term
68		* @param bn The builtin version of the enumerated term
69		* @param bnr The (extended) rewritten form of bn
70		* @return true if the term should be considered in the enumeration.
71		*/
72		virtual bool addTermInternal(Node n, Node bn, Node bnr) { return true; }
73		/** The enumerator */
74		Node d_enum;
75		/** The type of enum */
76		TypeNode d_tn;
77		/** extended rewriter */
78		ExtendedRewriter d_extr;
79		/** pointer to the statistics */
80		SygusStatistics* d_stats;
81		};
82
83		class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
84		{
85		public:
86		SygusEnumeratorCallbackDefault(Node e,
87		SygusStatistics* s = nullptr,
88		ExampleEvalCache* eec = nullptr,
89		SygusSampler* ssrv = nullptr,
90		std::ostream* out = nullptr);
91	332	virtual ~SygusEnumeratorCallbackDefault() {}
92
93		protected:
94		/** Notify that bn / bnr is an enumerated builtin, rewritten form of a term */
95		void notifyTermInternal(Node n, Node bn, Node bnr) override;
96		/** Add term, return true if n should be considered in the enumeration */
97		bool addTermInternal(Node n, Node bn, Node bnr) override;
98		/**
99		* Pointer to the example evaluation cache utility (used for symmetry
100		* breaking).
101		*/
102		ExampleEvalCache* d_eec;
103		/** sampler (for --sygus-rr-verify) */
104		SygusSampler* d_samplerRrV;
105		/** The output stream to print unsound rewrites for above */
106		std::ostream* d_out;
107		};
108
109		} // namespace quantifiers
110		} // namespace theory
111		} // namespace cvc5
112
113		#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H */