Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/term_tuple_enumerator.h	Lines:	2	2	100.0 %
Date:	2021-11-07	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   MikolasJanota, Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of an enumeration of tuples of terms for the purpose
 * of quantifier instantiation.
 */
#ifndef CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
#define CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H

#include <vector>

#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class TermPools;
class QuantifiersState;
class TermDb;
class RelevantDomain;

/**  Interface for enumeration of tuples of terms.
 *
 * The interface should be used as follows. Firstly, init is called, then,
 * repeatedly, verify if there are any combinations left by calling hasNext
 * and obtaining the next combination by calling next.
 *
 *  Optionally, if the  most recent combination is determined to be undesirable
 * (for whatever reason), the method failureReason is used to indicate which
 *  positions of the tuple are responsible for the said failure.
 */
class TermTupleEnumeratorInterface
{
 public:
  /** Initialize the enumerator. */
  virtual void init() = 0;
  /** Test if there are any more combinations. */
  virtual bool hasNext() = 0;
  /** Obtain the next combination, meaningful only if hasNext Returns true. */
  virtual void next(/*out*/ std::vector<Node>& terms) = 0;
  /** Record which of the terms obtained by the last call of next should not be
   * explored again. */
  virtual void failureReason(const std::vector<bool>& mask) = 0;
  virtual ~TermTupleEnumeratorInterface() = default;
};

/** A struct bundling up parameters for term tuple enumerator.*/
struct TermTupleEnumeratorEnv
{
  /**
   * Whether we should put full effort into finding an instantiation. If this
   * is false, then we allow for incompleteness, e.g. the tuple enumerator
   * may heuristically give up before it has generated all tuples.
   */
  bool d_fullEffort;
  /** Whether we increase tuples based on sum instead of max (see below) */
  bool d_increaseSum;
};

/**  A function to construct a tuple enumerator.
 *
 * In the methods below, we support the enumerators based on the following idea.
 * The tuples are represented as tuples of
 * indices of  terms, where the tuple has as many elements as there are
 * quantified variables in the considered quantifier q.
 *
 * Like so, we see a tuple as a number, where the digits may have different
 * ranges. The most significant digits are stored first.
 *
 * Tuples are enumerated in a lexicographic order in stages. There are 2
 * possible strategies, either all tuples in a given stage have the same sum of
 * digits, or, the maximum over these digits is the same (controlled by
 * TermTupleEnumeratorEnv::d_increaseSum).
 *
 * In this method, the returned enumerator draws ground terms from the term
 * database (provided by td). The quantifiers state (qs) is used to eliminate
 * duplicates modulo equality.
 */
TermTupleEnumeratorInterface* mkTermTupleEnumerator(
    Node q,
    const TermTupleEnumeratorEnv* env,
    QuantifiersState& qs,
    TermDb* td);
/** Same as above, but draws terms from the relevant domain utility (rd). */
TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd(
    Node q, const TermTupleEnumeratorEnv* env, RelevantDomain* rd);

/** Make term pool enumerator */
TermTupleEnumeratorInterface* mkTermTupleEnumeratorPool(
    Node q, const TermTupleEnumeratorEnv* env, TermPools* tp, Node p);

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5
#endif /* TERM_TUPLE_ENUMERATOR_H_7640 */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* MikolasJanota, Andrew Reynolds
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		* Implementation of an enumeration of tuples of terms for the purpose
14		* of quantifier instantiation.
15		*/
16		#ifndef CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
17		#define CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
18
19		#include <vector>
20
21		#include "expr/node.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace quantifiers {
26
27		class TermPools;
28		class QuantifiersState;
29		class TermDb;
30		class RelevantDomain;
31
32		/** Interface for enumeration of tuples of terms.
33		*
34		* The interface should be used as follows. Firstly, init is called, then,
35		* repeatedly, verify if there are any combinations left by calling hasNext
36		* and obtaining the next combination by calling next.
37		*
38		* Optionally, if the most recent combination is determined to be undesirable
39		* (for whatever reason), the method failureReason is used to indicate which
40		* positions of the tuple are responsible for the said failure.
41		*/
42	1723	class TermTupleEnumeratorInterface
43		{
44		public:
45		/** Initialize the enumerator. */
46		virtual void init() = 0;
47		/** Test if there are any more combinations. */
48		virtual bool hasNext() = 0;
49		/** Obtain the next combination, meaningful only if hasNext Returns true. */
50		virtual void next(/out/ std::vector<Node>& terms) = 0;
51		/** Record which of the terms obtained by the last call of next should not be
52		* explored again. */
53		virtual void failureReason(const std::vector<bool>& mask) = 0;
54	1723	virtual ~TermTupleEnumeratorInterface() = default;
55		};
56
57		/** A struct bundling up parameters for term tuple enumerator.*/
58		struct TermTupleEnumeratorEnv
59		{
60		/**
61		* Whether we should put full effort into finding an instantiation. If this
62		* is false, then we allow for incompleteness, e.g. the tuple enumerator
63		* may heuristically give up before it has generated all tuples.
64		*/
65		bool d_fullEffort;
66		/** Whether we increase tuples based on sum instead of max (see below) */
67		bool d_increaseSum;
68		};
69
70		/** A function to construct a tuple enumerator.
71		*
72		* In the methods below, we support the enumerators based on the following idea.
73		* The tuples are represented as tuples of
74		* indices of terms, where the tuple has as many elements as there are
75		* quantified variables in the considered quantifier q.
76		*
77		* Like so, we see a tuple as a number, where the digits may have different
78		* ranges. The most significant digits are stored first.
79		*
80		* Tuples are enumerated in a lexicographic order in stages. There are 2
81		* possible strategies, either all tuples in a given stage have the same sum of
82		* digits, or, the maximum over these digits is the same (controlled by
83		* TermTupleEnumeratorEnv::d_increaseSum).
84		*
85		* In this method, the returned enumerator draws ground terms from the term
86		* database (provided by td). The quantifiers state (qs) is used to eliminate
87		* duplicates modulo equality.
88		*/
89		TermTupleEnumeratorInterface* mkTermTupleEnumerator(
90		Node q,
91		const TermTupleEnumeratorEnv* env,
92		QuantifiersState& qs,
93		TermDb* td);
94		/** Same as above, but draws terms from the relevant domain utility (rd). */
95		TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd(
96		Node q, const TermTupleEnumeratorEnv* env, RelevantDomain* rd);
97
98		/** Make term pool enumerator */
99		TermTupleEnumeratorInterface* mkTermTupleEnumeratorPool(
100		Node q, const TermTupleEnumeratorEnv* env, TermPools* tp, Node p);
101
102		} // namespace quantifiers
103		} // namespace theory
104		} // namespace cvc5
105		#endif /* TERM_TUPLE_ENUMERATOR_H_7640 */