GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/inst_strategy_enumerative.h Lines: 3 3 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_strategy_enumerative.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 Enumerative instantiation
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H
18
#define CVC4__INST_STRATEGY_ENUMERATIVE_H
19
20
#include "theory/quantifiers/quant_module.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace quantifiers {
25
26
class RelevantDomain;
27
28
/** Enumerative instantiation
29
 *
30
 * This class implements enumerative instantiation described
31
 * in Reynolds et al., "Revisiting Enumerative Instantiation".
32
 *
33
 * It is an instance of QuantifiersModule, whose main
34
 * task is to make calls to QuantifiersEngine during
35
 * calls to QuantifiersModule::check(...).
36
 *
37
 * This class adds instantiations based on enumerating
38
 * well-typed terms that occur in the current context
39
 * based on a heuristically determined ordering on
40
 * tuples of terms. This ordering incorporates
41
 * reasoning about the relevant domain of quantified
42
 * formulas (see theory/quantifiers/relevant_domain.h).
43
 * We consider only ground terms that occur in the
44
 * context due to Theorem 1 of "Revisiting Enumerative
45
 * Instantiation". Notice this theorem holds only for theories
46
 * with compactness. For theories such as arithmetic,
47
 * this class may introduce "default" terms that are
48
 * used in instantiations, say 0 for arithmetic, even
49
 * when the term 0 does not occur in the context.
50
 *
51
 * This strategy is not enabled by default, and
52
 * is enabled by the option:
53
 *   --full-saturate-quant
54
 *
55
 * It is generally called with lower priority than
56
 * other instantiation strategies, although this
57
 * option interleaves it with other strategies
58
 * during quantifier effort level QEFFORT_STANDARD:
59
 *   --fs-interleave
60
 */
61
class InstStrategyEnum : public QuantifiersModule
62
{
63
 public:
64
  InstStrategyEnum(QuantifiersEngine* qe,
65
                   QuantifiersState& qs,
66
                   QuantifiersInferenceManager& qim,
67
                   QuantifiersRegistry& qr,
68
                   RelevantDomain* rd);
69
158
  ~InstStrategyEnum() {}
70
  /** Presolve */
71
  void presolve() override;
72
  /** Needs check. */
73
  bool needsCheck(Theory::Effort e) override;
74
  /** Reset round. */
75
  void reset_round(Theory::Effort e) override;
76
  /** Check.
77
   * Adds instantiations for all currently asserted
78
   * quantified formulas via calls to process(...)
79
   */
80
  void check(Theory::Effort e, QEffort quant_e) override;
81
  /** Identify. */
82
13166
  std::string identify() const override
83
  {
84
13166
    return std::string("InstStrategyEnum");
85
  }
86
87
 private:
88
  /** Pointer to the relevant domain utility of quantifiers engine */
89
  RelevantDomain* d_rd;
90
  /** process quantified formula
91
   *
92
   * q is the quantified formula we are constructing instances for.
93
   * fullEffort is whether we are called at full effort.
94
   *
95
   * If this function returns true, then one instantiation
96
   * (determined by an enumeration) was added via a successful
97
   * call to QuantifiersEngine::addInstantiation(...).
98
   *
99
   * If fullEffort is true, then we may introduce a "default"
100
   * well-typed term *not* occurring in the current context.
101
   * This handles corner cases where there are no well-typed
102
   * ground terms in the current context to instantiate with.
103
   *
104
   * The flag isRd indicates whether we are trying relevant domain
105
   * instantiations. If this flag is false, we are trying arbitrary ground
106
   * term instantiations.
107
   */
108
  bool process(Node q, bool fullEffort, bool isRd);
109
  /**
110
   * A limit on the number of rounds to apply this strategy, where a value < 0
111
   * means no limit. This value is set to the value of fullSaturateLimit()
112
   * during presolve.
113
   */
114
  int32_t d_fullSaturateLimit;
115
}; /* class InstStrategyEnum */
116
117
} /* CVC4::theory::quantifiers namespace */
118
} /* CVC4::theory namespace */
119
} /* CVC4 namespace */
120
121
#endif