GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_tuple_enumerator.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file  term_tuple_enumerator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mikolas Janota
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Implementation of an enumeration of tuples of terms for the purpose
13
 *of quantifier instantiation.
14
 **/
15
#ifndef CVC4__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
16
#define CVC4__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
17
#include <vector>
18
19
#include "expr/node.h"
20
21
namespace CVC4 {
22
namespace theory {
23
24
class QuantifiersEngine;
25
26
namespace quantifiers {
27
28
class RelevantDomain;
29
30
/**  Interface for enumeration of tuples of terms.
31
 *
32
 * The interface should be used as follows. Firstly, init is called, then,
33
 * repeatedly,  verify if there are any combinations left by calling hasNext
34
 * and obtaining the next combination by calling next.
35
 *
36
 *  Optionally, if the  most recent combination is determined to be undesirable
37
 * (for whatever reason), the method failureReason is used to indicate which
38
 *  positions of the tuple are responsible for the said failure.
39
 */
40
1965
class TermTupleEnumeratorInterface
41
{
42
 public:
43
  /** Initialize the enumerator. */
44
  virtual void init() = 0;
45
  /** Test if there are any more combinations. */
46
  virtual bool hasNext() = 0;
47
  /** Obtain the next combination, meaningful only if hasNext Returns true. */
48
  virtual void next(/*out*/ std::vector<Node>& terms) = 0;
49
  /** Record which of the terms obtained by the last call of next should not be
50
   * explored again. */
51
  virtual void failureReason(const std::vector<bool>& mask) = 0;
52
1965
  virtual ~TermTupleEnumeratorInterface() = default;
53
};
54
55
/** A struct bundling up parameters for term tuple enumerator.*/
56
struct TermTupleEnumeratorContext
57
{
58
  QuantifiersEngine* d_quantEngine;
59
  RelevantDomain* d_rd;
60
  bool d_fullEffort;
61
  bool d_increaseSum;
62
  bool d_isRd;
63
};
64
65
/**  A function to construct a tuple enumerator.
66
 *
67
 * Currently we support the enumerators based on the following idea.
68
 * The tuples are represented as tuples of
69
 * indices of  terms, where the tuple has as many elements as there are
70
 * quantified variables in the considered quantifier.
71
 *
72
 * Like so, we see a tuple as a number, where the digits may have different
73
 * ranges. The most significant digits are stored first.
74
 *
75
 * Tuples are enumerated  in a lexicographic order in stages. There are 2
76
 * possible strategies, either  all tuples in a given stage have the same sum of
77
 * digits, or, the maximum  over these digits is the same (controlled by
78
 * d_increaseSum).
79
 *
80
 * Further, an enumerator  either draws ground terms from the term database or
81
 * using the relevant domain class  (controlled by d_isRd).
82
 */
83
TermTupleEnumeratorInterface* mkTermTupleEnumerator(
84
    Node quantifier, const TermTupleEnumeratorContext* context);
85
86
}  // namespace quantifiers
87
}  // namespace theory
88
}  // namespace CVC4
89
#endif /* TERM_TUPLE_ENUMERATOR_H_7640 */